PA00BV · theorem

arbitrary_gauss_lemma_complete

Alpha v34 checked-use theorem · independently closed; not Stable

An arbitrary prime unit is a quadratic residue exactly when its Gauss reflection count is even, and a nonresidue exactly when it is odd.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ p. ∀ h. ∀ a. ∀ b. ∀ c. p = 2 · h + 1 → Prime(p) → ¬Dvd(p,a) → Range(b,c,1,h) → ∃ x. (∃ y. ∃ z. ∃ n. ∃ m. (∀ k. Lt(k,h) → ∃ i. ∃ j. ∃ u. BetaAt(b,c,k,i) ∧ (BetaAt(y,z,k,j) ∧ (BetaAt(n,m,k,u) ∧ (Lt(0,j) ∧ (Le(j,h) ∧ ((u = 0 ∨ u = 1) ∧ (u = 0 ∧ ModEq(p,a · i,j) ∨ u = 1 ∧ ModEq(p,a · i,2 · h · j)))))))) ∧ BitCount(n,m,h,x)) ∧ ((QRes(p,a) → Even(x)) ∧ (Even(x) → QRes(p,a)) ∧ ((¬QRes(p,a) → Odd(x)) ∧ (Odd(x) → ¬QRes(p,a))))

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0001 Le PD0002 Lt PD0003 Dvd PD0004 Prime PD0008 ModEq PD0009 Even PD0010 Odd PD0013 BetaAt PD0017 BitCount PD0018 Range PD0021 QRes

20 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0008 ModEq PD0009 Even PD0010 Odd PD0013 BetaAt PD0017 BitCount PD0020 Pow PD0021 QRes

45 occurrences

Exact expanded native-PA statement
forall p h a b c. p = 2 * h + 1 -> ((~(p = 1) /\ forall esi_prime_left_gla_prime esi_prime_right_gla_prime. p = esi_prime_left_gla_prime * esi_prime_right_gla_prime -> esi_prime_left_gla_prime = 1 \/ esi_prime_right_gla_prime = 1)) -> (~(exists frm_factor_gla_nondivisor. a = p * frm_factor_gla_nondivisor)) -> (forall gsp_range_index_gla_half_range. (exists gsp_lt_gap_gla_half_range_range_bound. gsp_lt_gap_gla_half_range_range_bound + S gsp_range_index_gla_half_range = h) -> (((exists gsp_beta_height_gla_half_range_range_entry. gsp_beta_height_gla_half_range_range_entry + S (1 + gsp_range_index_gla_half_range) = S ((S (gsp_range_index_gla_half_range)) * c)) /\ exists gsp_beta_quotient_gla_half_range_range_entry. b = gsp_beta_quotient_gla_half_range_range_entry * S ((S (gsp_range_index_gla_half_range)) * c) + (1 + gsp_range_index_gla_half_range)))) -> (exists e. ((exists mb mc sb sc. ((forall gsp_index_gla_signed_prefix. (exists gsp_lt_gap_gla_signed_prefix_index_bound. gsp_lt_gap_gla_signed_prefix_index_bound + S gsp_index_gla_signed_prefix = h) -> (exists gsp_value_gla_signed_prefix_entry gsp_magnitude_gla_signed_prefix_entry gsp_sign_gla_signed_prefix_entry. (((exists ff_h_gsp_gla_signed_prefix_entry_source. ff_h_gsp_gla_signed_prefix_entry_source + S (gsp_value_gla_signed_prefix_entry) = S ((S (gsp_index_gla_signed_prefix)) * c)) /\ exists ff_q_gsp_gla_signed_prefix_entry_source. b = ff_q_gsp_gla_signed_prefix_entry_source * S ((S (gsp_index_gla_signed_prefix)) * c) + (gsp_value_gla_signed_prefix_entry))) /\ ((((exists ff_h_gsp_gla_signed_prefix_entry_magnitude. ff_h_gsp_gla_signed_prefix_entry_magnitude + S (gsp_magnitude_gla_signed_prefix_entry) = S ((S (gsp_index_gla_signed_prefix)) * mc)) /\ exists ff_q_gsp_gla_signed_prefix_entry_magnitude. mb = ff_q_gsp_gla_signed_prefix_entry_magnitude * S ((S (gsp_index_gla_signed_prefix)) * mc) + (gsp_magnitude_gla_signed_prefix_entry))) /\ ((((exists ff_h_gsp_gla_signed_prefix_entry_sign. ff_h_gsp_gla_signed_prefix_entry_sign + S (gsp_sign_gla_signed_prefix_entry) = S ((S (gsp_index_gla_signed_prefix)) * sc)) /\ exists ff_q_gsp_gla_signed_prefix_entry_sign. sb = ff_q_gsp_gla_signed_prefix_entry_sign * S ((S (gsp_index_gla_signed_prefix)) * sc) + (gsp_sign_gla_signed_prefix_entry))) /\ ((exists gsp_lt_gap_gla_signed_prefix_entry_positive. gsp_lt_gap_gla_signed_prefix_entry_positive + S 0 = gsp_magnitude_gla_signed_prefix_entry) /\ ((exists gsp_le_gap_gla_signed_prefix_entry_bounded. gsp_le_gap_gla_signed_prefix_entry_bounded + gsp_magnitude_gla_signed_prefix_entry = h) /\ ((gsp_sign_gla_signed_prefix_entry = 0 \/ gsp_sign_gla_signed_prefix_entry = 1) /\ (((gsp_sign_gla_signed_prefix_entry = 0 /\ (exists gsp_mod_left_gla_signed_prefix_entry_lower gsp_mod_right_gla_signed_prefix_entry_lower. (a * gsp_value_gla_signed_prefix_entry) + p * gsp_mod_left_gla_signed_prefix_entry_lower = (gsp_magnitude_gla_signed_prefix_entry) + p * gsp_mod_right_gla_signed_prefix_entry_lower)) \/ (gsp_sign_gla_signed_prefix_entry = 1 /\ (exists gsp_mod_left_gla_signed_prefix_entry_reflected gsp_mod_right_gla_signed_prefix_entry_reflected. (a * gsp_value_gla_signed_prefix_entry) + p * gsp_mod_left_gla_signed_prefix_entry_reflected = ((2 * h) * gsp_magnitude_gla_signed_prefix_entry) + p * gsp_mod_right_gla_signed_prefix_entry_reflected))))))))))) /\ (((exists ff_u_gla_count_sum ff_v_gla_count_sum. ((((exists ff_h_gla_count_sum_start. ff_h_gla_count_sum_start + S (0) = S ((S (0)) * ff_v_gla_count_sum)) /\ exists ff_q_gla_count_sum_start. ff_u_gla_count_sum = ff_q_gla_count_sum_start * S ((S (0)) * ff_v_gla_count_sum) + (0))) /\ ((((exists ff_h_gla_count_sum_terminal. ff_h_gla_count_sum_terminal + S (e) = S ((S (h)) * ff_v_gla_count_sum)) /\ exists ff_q_gla_count_sum_terminal. ff_u_gla_count_sum = ff_q_gla_count_sum_terminal * S ((S (h)) * ff_v_gla_count_sum) + (e))) /\ forall ff_i_gla_count_sum. (exists ff_lt_gla_count_sum_bound. ff_lt_gla_count_sum_bound + S ff_i_gla_count_sum = h) -> exists ff_a_gla_count_sum ff_r_gla_count_sum ff_s_gla_count_sum. ((((exists ff_h_gla_count_sum_summand. ff_h_gla_count_sum_summand + S (ff_a_gla_count_sum) = S ((S (ff_i_gla_count_sum)) * sc)) /\ exists ff_q_gla_count_sum_summand. sb = ff_q_gla_count_sum_summand * S ((S (ff_i_gla_count_sum)) * sc) + (ff_a_gla_count_sum))) /\ ((((exists ff_h_gla_count_sum_partial. ff_h_gla_count_sum_partial + S (ff_r_gla_count_sum) = S ((S (ff_i_gla_count_sum)) * ff_v_gla_count_sum)) /\ exists ff_q_gla_count_sum_partial. ff_u_gla_count_sum = ff_q_gla_count_sum_partial * S ((S (ff_i_gla_count_sum)) * ff_v_gla_count_sum) + (ff_r_gla_count_sum))) /\ ((((exists ff_h_gla_count_sum_successor. ff_h_gla_count_sum_successor + S (ff_s_gla_count_sum) = S ((S (S ff_i_gla_count_sum)) * ff_v_gla_count_sum)) /\ exists ff_q_gla_count_sum_successor. ff_u_gla_count_sum = ff_q_gla_count_sum_successor * S ((S (S ff_i_gla_count_sum)) * ff_v_gla_count_sum) + (ff_s_gla_count_sum))) /\ ff_s_gla_count_sum = ff_r_gla_count_sum + ff_a_gla_count_sum)))))) /\ (forall ff_i_gla_count_bits. (exists ff_lt_gla_count_bits_bound. ff_lt_gla_count_bits_bound + S ff_i_gla_count_bits = h) -> exists ff_bit_gla_count_bits. ((((exists ff_h_gla_count_bits_decoded. ff_h_gla_count_bits_decoded + S (ff_bit_gla_count_bits) = S ((S (ff_i_gla_count_bits)) * sc)) /\ exists ff_q_gla_count_bits_decoded. sb = ff_q_gla_count_bits_decoded * S ((S (ff_i_gla_count_bits)) * sc) + (ff_bit_gla_count_bits))) /\ (ff_bit_gla_count_bits = 0 \/ ff_bit_gla_count_bits = 1))))))) /\ (((((exists qr_x_gla_qres. exists qr_u_gla_qres qr_v_gla_qres. qr_x_gla_qres * qr_x_gla_qres + p * qr_u_gla_qres = a + p * qr_v_gla_qres) -> (exists gs_even_gla_even. e = 2 * gs_even_gla_even)) /\ ((exists gs_even_gla_even. e = 2 * gs_even_gla_even) -> (exists qr_x_gla_qres. exists qr_u_gla_qres qr_v_gla_qres. qr_x_gla_qres * qr_x_gla_qres + p * qr_u_gla_qres = a + p * qr_v_gla_qres)))) /\ (((~(exists qr_x_gla_qres. exists qr_u_gla_qres qr_v_gla_qres. qr_x_gla_qres * qr_x_gla_qres + p * qr_u_gla_qres = a + p * qr_v_gla_qres) -> (exists gs_odd_gla_odd. e = 2 * gs_odd_gla_odd + 1)) /\ ((exists gs_odd_gla_odd. e = 2 * gs_odd_gla_odd + 1) -> ~(exists qr_x_gla_qres. exists qr_u_gla_qres qr_v_gla_qres. qr_x_gla_qres * qr_x_gla_qres + p * qr_u_gla_qres = a + p * qr_v_gla_qres)))))))

Proof neighborhood

Direct theorem prerequisites

PA0085 gauss_lemma_power_congruence_exists PA005E pow_predecessor_parity_mod PA00BU arbitrary_euler_criterion_complete PA0057 parity_cases PA00BP odd_prime_one_not_mod_predecessor PA003L mod_eq_symm PA0024 mod_eq_trans PA000H mul_comm PA0001 zero_add

Direct theorem dependents

PA00D7 odd_prime_gauss_eisenstein_orientation_data_exists

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

188 script commands · 51 reading checkpoints · 22 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (8)
gauss lemma power congruence existspow predecessor parity modarbitrary euler criterion completeparity casesodd prime one not mod predecessormod eq symmmod eq transmul comm
01Fix variables and assumptionsL1–9

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro h
  3. L3
    intro a
  4. L4
    intro b
  5. L5
    intro c
  6. L6
    intro hpodd
  7. L7
    intro hprime
  8. L8
    intro hnotdiv
  9. L9
    intro hhalf
02Establish hpsuccL10–13

Establish this local claim before using it. It is not an additional assumption.

  1. L10
    have hpsucc : p = S (2 * h)
  2. L11
    trans 2 * h + 1
  3. L12
    exact hpodd
  4. L13
    simp
03Establish hdoubleL14–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul comm.

  1. L14
    have hdouble : h + h = 2 * h
  2. L15
    trans h * 2
  3. L16
    simp [zero_add]
  4. L17
    specialize mul_comm h
  5. L18
    specialize mul_comm 2
  6. L19
    apply mul_comm
04Establish hgaussL20–29

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gauss lemma power congruence exists.

  1. L20
    have hgauss : ∃ e. ∃ A. ∃ R. Pow(a,h,A) ∧ (Pow(2 · h,e,R) ∧ ((∃ x. ∃ y. ∃ z. ∃ n. (∀ m. Lt(m,h) → ∃ k. ∃ i. ∃ j. BetaAt(b,c,m,k) ∧ (BetaAt(x,y,m,i) ∧ (BetaAt(z,n,m,j) ∧ (Lt(0,i) ∧ (Le(i,h) ∧ ((j = 0 ∨ j = 1) ∧ (j = 0 ∧ ModEq(p,a · k,i) ∨ j = 1 ∧ ModEq(p,a · k,2 · h · i)))))))) ∧ BitCount(z,n,h,e)) ∧ ModEq(p,A,R)))Definitions: Pow(a,h,A)Pow(2 · h,e,R)Lt(m,h)BetaAt(b,c,m,k)BetaAt(x,y,m,i)BetaAt(z,n,m,j)Lt(0,i)Le(i,h)ModEq(p,a · k,i)ModEq(p,a · k,2 · h · i)BitCount(z,n,h,e)ModEq(p,A,R)Original native command in the exact edition
  2. L21
    specialize gauss_lemma_power_congruence_exists p
  3. L22
    specialize gauss_lemma_power_congruence_exists h
  4. L23
    specialize gauss_lemma_power_congruence_exists a
  5. L24
    specialize gauss_lemma_power_congruence_exists b
  6. L25
    specialize gauss_lemma_power_congruence_exists c
  7. L26
    apply gauss_lemma_power_congruence_exists
  8. L27
    exact hpodd
  9. L28
    exact hprime
  10. L29
    exact hnotdiv
05Use earlier factsL30–30

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L30
    exact hhalf
06Separate the logical casesL31–36

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L31
    cases hgauss
  2. L32
    cases hgauss_witness
  3. L33
    cases hgauss_witness_witness
  4. L34
    cases hgauss_witness_witness_witness
  5. L35
    cases hgauss_witness_witness_witness_right
  6. L36
    cases hgauss_witness_witness_witness_right_right
07Establish heulerL37–46

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply arbitrary euler criterion complete.

  1. L37
    have heuler : (QRes(p,a) → ModEq(p,x1,1)) ∧ (ModEq(p,x1,1) → QRes(p,a)) ∧ ((¬QRes(p,a) → ModEq(p,x1,2 · h)) ∧ (ModEq(p,x1,2 · h) → ¬QRes(p,a)))Definitions: QRes(p,a)ModEq(p,x1,1)ModEq(p,x1,2 · h)Original native command in the exact edition
  2. L38
    specialize arbitrary_euler_criterion_complete p
  3. L39
    specialize arbitrary_euler_criterion_complete a
  4. L40
    specialize arbitrary_euler_criterion_complete (2 * h)
  5. L41
    specialize arbitrary_euler_criterion_complete h
  6. L42
    specialize arbitrary_euler_criterion_complete x1
  7. L43
    apply arbitrary_euler_criterion_complete
  8. L44
    exact hpsucc
  9. L45
    exact hprime
  10. L46
    exact hnotdiv
08Calculate and transport equalitiesL47–47

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L47
    symm
09Use earlier factsL48–49

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L48
    exact hdouble
  2. L49
    exact hgauss_witness_witness_witness_left
10Separate the logical casesL50–52

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L50
    cases heuler
  2. L51
    cases heuler_left
  3. L52
    cases heuler_right
11Establish hbridgeL53–60

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow predecessor parity mod.

  1. L53
    have hbridge : (Even(x) → ModEq(p,x2,1)) ∧ (Odd(x) → ModEq(p,x2,2 · h))Definitions: Even(x)ModEq(p,x2,1)Odd(x)ModEq(p,x2,2 · h)Original native command in the exact edition
  2. L54
    specialize pow_predecessor_parity_mod p
  3. L55
    specialize pow_predecessor_parity_mod (2 * h)
  4. L56
    specialize pow_predecessor_parity_mod x
  5. L57
    specialize pow_predecessor_parity_mod x2
  6. L58
    apply pow_predecessor_parity_mod
  7. L59
    exact hpsucc
  8. L60
    exact hgauss_witness_witness_witness_right_left
12Separate the logical casesL61–61

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L61
    cases hbridge
13Establish hseparationL62–71

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd prime one not mod predecessor.

  1. L62
    have hseparation : ¬ModEq(p,1,2 · h)Definitions: ModEq(p,1,2 · h)Original native command in the exact edition
  2. L63
    intro hcollision
  3. L64
    specialize odd_prime_one_not_mod_predecessor p
  4. L65
    specialize odd_prime_one_not_mod_predecessor (2 * h)
  5. L66
    specialize odd_prime_one_not_mod_predecessor h
  6. L67
    apply odd_prime_one_not_mod_predecessor
  7. L68
    exact hpsucc
  8. L69
    exact hprime
  9. L70
    symm
  10. L71
    exact hdouble
14Use earlier factsL72–72

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L72
    exact hcollision
15Establish hqres_evenL73–75

Establish this local claim before using it. It is not an additional assumption.

  1. L73
    have hqres_even : QRes(p,a) → Even(x)Definitions: QRes(p,a)Even(x)Original native command in the exact edition
  2. L74
    intro hqres
  3. L75
    specialize parity_cases x
16Separate the logical casesL76–77

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L76
    cases parity_cases
  2. L77
    cases parity_cases_witness
17Construct an explicit witnessL78–78

Supply the displayed value, then prove that it has the required property.

  1. L78
    exists x3
18Use earlier factsL79–79

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L79
    exact parity_cases_witness_left
19Separate the logical casesL80–80

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L80
    exfalso
20Use earlier factsL81–81

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L81
    apply hseparation
21Establish hAoneL82–84

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply heuler left left.

  1. L82
    have hAone : ModEq(p,x1,1)Definitions: ModEq(p,x1,1)Original native command in the exact edition
  2. L83
    apply heuler_left_left
  3. L84
    exact hqres
22Establish honeAL85–90

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq symm.

  1. L85
    have honeA : ModEq(p,1,x1)Definitions: ModEq(p,1,x1)Original native command in the exact edition
  2. L86
    specialize mod_eq_symm p
  3. L87
    specialize mod_eq_symm x1
  4. L88
    specialize mod_eq_symm 1
  5. L89
    apply mod_eq_symm
  6. L90
    exact hAone
23Establish honeRL91–98

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq trans.

  1. L91
    have honeR : ModEq(p,1,x2)Definitions: ModEq(p,1,x2)Original native command in the exact edition
  2. L92
    specialize mod_eq_trans p
  3. L93
    specialize mod_eq_trans 1
  4. L94
    specialize mod_eq_trans x1
  5. L95
    specialize mod_eq_trans x2
  6. L96
    apply mod_eq_trans
  7. L97
    exact honeA
  8. L98
    exact hgauss_witness_witness_witness_right_right_right
24Establish hRpredL99–100

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hbridge right.

  1. L99
    have hRpred : ModEq(p,x2,2 · h)Definitions: ModEq(p,x2,2 · h)Original native command in the exact edition
  2. L100
    apply hbridge_right
25Construct an explicit witnessL101–101

Supply the displayed value, then prove that it has the required property.

  1. L101
    exists x3
26Use earlier factsL102–109

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L102
    exact parity_cases_witness_right
  2. L103
    specialize mod_eq_trans p
  3. L104
    specialize mod_eq_trans 1
  4. L105
    specialize mod_eq_trans x2
  5. L106
    specialize mod_eq_trans (2 * h)
  6. L107
    apply mod_eq_trans
  7. L108
    exact honeR
  8. L109
    exact hRpred
27Establish heven_qresL110–111

Establish this local claim before using it. It is not an additional assumption.

  1. L110
    have heven_qres : Even(x) → QRes(p,a)Definitions: Even(x)QRes(p,a)Original native command in the exact edition
  2. L111
    intro heven
28Establish hRoneL112–114

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hbridge left.

  1. L112
    have hRone : ModEq(p,x2,1)Definitions: ModEq(p,x2,1)Original native command in the exact edition
  2. L113
    apply hbridge_left
  3. L114
    exact heven
29Establish hAoneL115–124

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq trans.

  1. L115
    have hAone : ModEq(p,x1,1)Definitions: ModEq(p,x1,1)Original native command in the exact edition
  2. L116
    specialize mod_eq_trans p
  3. L117
    specialize mod_eq_trans x1
  4. L118
    specialize mod_eq_trans x2
  5. L119
    specialize mod_eq_trans 1
  6. L120
    apply mod_eq_trans
  7. L121
    exact hgauss_witness_witness_witness_right_right_right
  8. L122
    exact hRone
  9. L123
    apply heuler_left_right
  10. L124
    exact hAone
30Establish hnonres_oddL125–127

Establish this local claim before using it. It is not an additional assumption.

  1. L125
    have hnonres_odd : ¬QRes(p,a) → Odd(x)Definitions: QRes(p,a)Odd(x)Original native command in the exact edition
  2. L126
    intro hnonres
  3. L127
    specialize parity_cases x
31Separate the logical casesL128–130

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L128
    cases parity_cases
  2. L129
    cases parity_cases_witness
  3. L130
    exfalso
32Use earlier factsL131–131

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L131
    apply hseparation
33Establish hRoneL132–133

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hbridge left.

  1. L132
    have hRone : ModEq(p,x2,1)Definitions: ModEq(p,x2,1)Original native command in the exact edition
  2. L133
    apply hbridge_left
34Construct an explicit witnessL134–134

Supply the displayed value, then prove that it has the required property.

  1. L134
    exists x3
35Use earlier factsL135–135

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L135
    exact parity_cases_witness_left
36Establish hAoneL136–143

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq trans.

  1. L136
    have hAone : ModEq(p,x1,1)Definitions: ModEq(p,x1,1)Original native command in the exact edition
  2. L137
    specialize mod_eq_trans p
  3. L138
    specialize mod_eq_trans x1
  4. L139
    specialize mod_eq_trans x2
  5. L140
    specialize mod_eq_trans 1
  6. L141
    apply mod_eq_trans
  7. L142
    exact hgauss_witness_witness_witness_right_right_right
  8. L143
    exact hRone
37Establish honeAL144–149

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq symm.

  1. L144
    have honeA : ModEq(p,1,x1)Definitions: ModEq(p,1,x1)Original native command in the exact edition
  2. L145
    specialize mod_eq_symm p
  3. L146
    specialize mod_eq_symm x1
  4. L147
    specialize mod_eq_symm 1
  5. L148
    apply mod_eq_symm
  6. L149
    exact hAone
38Establish hApredL150–159

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply heuler right left.

  1. L150
    have hApred : ModEq(p,x1,2 · h)Definitions: ModEq(p,x1,2 · h)Original native command in the exact edition
  2. L151
    apply heuler_right_left
  3. L152
    exact hnonres
  4. L153
    specialize mod_eq_trans p
  5. L154
    specialize mod_eq_trans 1
  6. L155
    specialize mod_eq_trans x1
  7. L156
    specialize mod_eq_trans (2 * h)
  8. L157
    apply mod_eq_trans
  9. L158
    exact honeA
  10. L159
    exact hApred
39Construct an explicit witnessL160–160

Supply the displayed value, then prove that it has the required property.

  1. L160
    exists x3
40Use earlier factsL161–161

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L161
    exact parity_cases_witness_right
41Establish hodd_nonresL162–163

Establish this local claim before using it. It is not an additional assumption.

  1. L162
    have hodd_nonres : Odd(x) → ¬QRes(p,a)Definitions: Odd(x)QRes(p,a)Original native command in the exact edition
  2. L163
    intro hodd
42Establish hRpredL164–166

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hbridge right.

  1. L164
    have hRpred : ModEq(p,x2,2 · h)Definitions: ModEq(p,x2,2 · h)Original native command in the exact edition
  2. L165
    apply hbridge_right
  3. L166
    exact hodd
43Establish hApredL167–176

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq trans.

  1. L167
    have hApred : ModEq(p,x1,2 · h)Definitions: ModEq(p,x1,2 · h)Original native command in the exact edition
  2. L168
    specialize mod_eq_trans p
  3. L169
    specialize mod_eq_trans x1
  4. L170
    specialize mod_eq_trans x2
  5. L171
    specialize mod_eq_trans (2 * h)
  6. L172
    apply mod_eq_trans
  7. L173
    exact hgauss_witness_witness_witness_right_right_right
  8. L174
    exact hRpred
  9. L175
    intro hqres
  10. L176
    apply heuler_right_right
44Use earlier factsL177–178

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L177
    exact hApred
  2. L178
    exact hqres
45Construct an explicit witnessL179–179

Supply the displayed value, then prove that it has the required property.

  1. L179
    exists x
46Separate the logical casesL180–180

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L180
    split
47Use earlier factsL181–181

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L181
    exact hgauss_witness_witness_witness_right_right_left
48Separate the logical casesL182–183

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L182
    split
  2. L183
    split
49Use earlier factsL184–185

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L184
    exact hqres_even
  2. L185
    exact heven_qres
50Separate the logical casesL186–186

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L186
    split
51Use earlier factsL187–188

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L187
    exact hnonres_odd
  2. L188
    exact hodd_nonres

Library-wide reading audit

Original defined command ledger · 188 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro a
  4. 0004intro b
  5. 0005intro c
  6. 0006intro hpodd
  7. 0007intro hprime
  8. 0008intro hnotdiv
  9. 0009intro hhalf
  10. 0010have hpsucc : p = S (2 * h)
  11. 0011trans 2 * h + 1
  12. 0012exact hpodd
  13. 0013simp
  14. 0014have hdouble : h + h = 2 * h
  15. 0015trans h * 2
  16. 0016simp [zero_add]
  17. 0017specialize mul_comm h
  18. 0018specialize mul_comm 2
  19. 0019apply mul_comm
  20. 0020have hgauss : ∃ e. ∃ A. ∃ R. Pow(a,h,A) ∧ (Pow(2 · h,e,R) ∧ ((∃ x. ∃ y. ∃ z. ∃ n. (∀ m. Lt(m,h) → ∃ k. ∃ i. ∃ j. BetaAt(b,c,m,k) ∧ (BetaAt(x,y,m,i) ∧ (BetaAt(z,n,m,j) ∧ (Lt(0,i) ∧ (Le(i,h) ∧ ((j = 0 ∨ j = 1) ∧ (j = 0 ∧ ModEq(p,a · k,i) ∨ j = 1 ∧ ModEq(p,a · k,2 · h · i)))))))) ∧ BitCount(z,n,h,e)) ∧ ModEq(p,A,R)))
    Exact native replay linehave hgauss : exists e A R. ((exists ff_b_glb_multiplier_power ff_c_glb_multiplier_power. ((forall ff_i_glb_multiplier_power_repeat. (exists ff_lt_glb_multiplier_power_repeat_bound. ff_lt_glb_multiplier_power_repeat_bound + S ff_i_glb_multiplier_power_repeat = h) -> (((exists ff_h_glb_multiplier_power_repeat_decoded. ff_h_glb_multiplier_power_repeat_decoded + S (a) = S ((S (ff_i_glb_multiplier_power_repeat)) * ff_c_glb_multiplier_power)) /\ exists ff_q_glb_multiplier_power_repeat_decoded. ff_b_glb_multiplier_power = ff_q_glb_multiplier_power_repeat_decoded * S ((S (ff_i_glb_multiplier_power_repeat)) * ff_c_glb_multiplier_power) + (a)))) /\ (exists ff_u_glb_multiplier_power_product ff_v_glb_multiplier_power_product. ((((exists ff_h_glb_multiplier_power_product_start. ff_h_glb_multiplier_power_product_start + S (1) = S ((S (0)) * ff_v_glb_multiplier_power_product)) /\ exists ff_q_glb_multiplier_power_product_start. ff_u_glb_multiplier_power_product = ff_q_glb_multiplier_power_product_start * S ((S (0)) * ff_v_glb_multiplier_power_product) + (1))) /\ ((((exists ff_h_glb_multiplier_power_product_terminal. ff_h_glb_multiplier_power_product_terminal + S (A) = S ((S (h)) * ff_v_glb_multiplier_power_product)) /\ exists ff_q_glb_multiplier_power_product_terminal. ff_u_glb_multiplier_power_product = ff_q_glb_multiplier_power_product_terminal * S ((S (h)) * ff_v_glb_multiplier_power_product) + (A))) /\ forall ff_i_glb_multiplier_power_product. (exists ff_lt_glb_multiplier_power_product_bound. ff_lt_glb_multiplier_power_product_bound + S ff_i_glb_multiplier_power_product = h) -> exists ff_p_glb_multiplier_power_product ff_r_glb_multiplier_power_product ff_s_glb_multiplier_power_product. ((((exists ff_h_glb_multiplier_power_product_factor. ff_h_glb_multiplier_power_product_factor + S (ff_p_glb_multiplier_power_product) = S ((S (ff_i_glb_multiplier_power_product)) * ff_c_glb_multiplier_power)) /\ exists ff_q_glb_multiplier_power_product_factor. ff_b_glb_multiplier_power = ff_q_glb_multiplier_power_product_factor * S ((S (ff_i_glb_multiplier_power_product)) * ff_c_glb_multiplier_power) + (ff_p_glb_multiplier_power_product))) /\ ((((exists ff_h_glb_multiplier_power_product_partial. ff_h_glb_multiplier_power_product_partial + S (ff_r_glb_multiplier_power_product) = S ((S (ff_i_glb_multiplier_power_product)) * ff_v_glb_multiplier_power_product)) /\ exists ff_q_glb_multiplier_power_product_partial. ff_u_glb_multiplier_power_product = ff_q_glb_multiplier_power_product_partial * S ((S (ff_i_glb_multiplier_power_product)) * ff_v_glb_multiplier_power_product) + (ff_r_glb_multiplier_power_product))) /\ ((((exists ff_h_glb_multiplier_power_product_successor. ff_h_glb_multiplier_power_product_successor + S (ff_s_glb_multiplier_power_product) = S ((S (S ff_i_glb_multiplier_power_product)) * ff_v_glb_multiplier_power_product)) /\ exists ff_q_glb_multiplier_power_product_successor. ff_u_glb_multiplier_power_product = ff_q_glb_multiplier_power_product_successor * S ((S (S ff_i_glb_multiplier_power_product)) * ff_v_glb_multiplier_power_product) + (ff_s_glb_multiplier_power_product))) /\ ff_s_glb_multiplier_power_product = ff_r_glb_multiplier_power_product * ff_p_glb_multiplier_power_product)))))))) /\ ((exists ff_b_glb_sign_power_expanded ff_c_glb_sign_power_expanded. ((forall ff_i_glb_sign_power_expanded_repeat. (exists ff_lt_glb_sign_power_expanded_repeat_bound. ff_lt_glb_sign_power_expanded_repeat_bound + S ff_i_glb_sign_power_expanded_repeat = e) -> (((exists ff_h_glb_sign_power_expanded_repeat_decoded. ff_h_glb_sign_power_expanded_repeat_decoded + S ((2 * h)) = S ((S (ff_i_glb_sign_power_expanded_repeat)) * ff_c_glb_sign_power_expanded)) /\ exists ff_q_glb_sign_power_expanded_repeat_decoded. ff_b_glb_sign_power_expanded = ff_q_glb_sign_power_expanded_repeat_decoded * S ((S (ff_i_glb_sign_power_expanded_repeat)) * ff_c_glb_sign_power_expanded) + ((2 * h))))) /\ (exists ff_u_glb_sign_power_expanded_product ff_v_glb_sign_power_expanded_product. ((((exists ff_h_glb_sign_power_expanded_product_start. ff_h_glb_sign_power_expanded_product_start + S (1) = S ((S (0)) * ff_v_glb_sign_power_expanded_product)) /\ exists ff_q_glb_sign_power_expanded_product_start. ff_u_glb_sign_power_expanded_product = ff_q_glb_sign_power_expanded_product_start * S ((S (0)) * ff_v_glb_sign_power_expanded_product) + (1))) /\ ((((exists ff_h_glb_sign_power_expanded_product_terminal. ff_h_glb_sign_power_expanded_product_terminal + S (R) = S ((S (e)) * ff_v_glb_sign_power_expanded_product)) /\ exists ff_q_glb_sign_power_expanded_product_terminal. ff_u_glb_sign_power_expanded_product = ff_q_glb_sign_power_expanded_product_terminal * S ((S (e)) * ff_v_glb_sign_power_expanded_product) + (R))) /\ forall ff_i_glb_sign_power_expanded_product. (exists ff_lt_glb_sign_power_expanded_product_bound. ff_lt_glb_sign_power_expanded_product_bound + S ff_i_glb_sign_power_expanded_product = e) -> exists ff_p_glb_sign_power_expanded_product ff_r_glb_sign_power_expanded_product ff_s_glb_sign_power_expanded_product. ((((exists ff_h_glb_sign_power_expanded_product_factor. ff_h_glb_sign_power_expanded_product_factor + S (ff_p_glb_sign_power_expanded_product) = S ((S (ff_i_glb_sign_power_expanded_product)) * ff_c_glb_sign_power_expanded)) /\ exists ff_q_glb_sign_power_expanded_product_factor. ff_b_glb_sign_power_expanded = ff_q_glb_sign_power_expanded_product_factor * S ((S (ff_i_glb_sign_power_expanded_product)) * ff_c_glb_sign_power_expanded) + (ff_p_glb_sign_power_expanded_product))) /\ ((((exists ff_h_glb_sign_power_expanded_product_partial. ff_h_glb_sign_power_expanded_product_partial + S (ff_r_glb_sign_power_expanded_product) = S ((S (ff_i_glb_sign_power_expanded_product)) * ff_v_glb_sign_power_expanded_product)) /\ exists ff_q_glb_sign_power_expanded_product_partial. ff_u_glb_sign_power_expanded_product = ff_q_glb_sign_power_expanded_product_partial * S ((S (ff_i_glb_sign_power_expanded_product)) * ff_v_glb_sign_power_expanded_product) + (ff_r_glb_sign_power_expanded_product))) /\ ((((exists ff_h_glb_sign_power_expanded_product_successor. ff_h_glb_sign_power_expanded_product_successor + S (ff_s_glb_sign_power_expanded_product) = S ((S (S ff_i_glb_sign_power_expanded_product)) * ff_v_glb_sign_power_expanded_product)) /\ exists ff_q_glb_sign_power_expanded_product_successor. ff_u_glb_sign_power_expanded_product = ff_q_glb_sign_power_expanded_product_successor * S ((S (S ff_i_glb_sign_power_expanded_product)) * ff_v_glb_sign_power_expanded_product) + (ff_s_glb_sign_power_expanded_product))) /\ ff_s_glb_sign_power_expanded_product = ff_r_glb_sign_power_expanded_product * ff_p_glb_sign_power_expanded_product)))))))) /\ ((exists mb mc sb sc. ((forall gsp_index_glb_signed_prefix. (exists gsp_lt_gap_glb_signed_prefix_index_bound. gsp_lt_gap_glb_signed_prefix_index_bound + S gsp_index_glb_signed_prefix = h) -> (exists gsp_value_glb_signed_prefix_entry gsp_magnitude_glb_signed_prefix_entry gsp_sign_glb_signed_prefix_entry. (((exists ff_h_gsp_glb_signed_prefix_entry_source. ff_h_gsp_glb_signed_prefix_entry_source + S (gsp_value_glb_signed_prefix_entry) = S ((S (gsp_index_glb_signed_prefix)) * c)) /\ exists ff_q_gsp_glb_signed_prefix_entry_source. b = ff_q_gsp_glb_signed_prefix_entry_source * S ((S (gsp_index_glb_signed_prefix)) * c) + (gsp_value_glb_signed_prefix_entry))) /\ ((((exists ff_h_gsp_glb_signed_prefix_entry_magnitude. ff_h_gsp_glb_signed_prefix_entry_magnitude + S (gsp_magnitude_glb_signed_prefix_entry) = S ((S (gsp_index_glb_signed_prefix)) * mc)) /\ exists ff_q_gsp_glb_signed_prefix_entry_magnitude. mb = ff_q_gsp_glb_signed_prefix_entry_magnitude * S ((S (gsp_index_glb_signed_prefix)) * mc) + (gsp_magnitude_glb_signed_prefix_entry))) /\ ((((exists ff_h_gsp_glb_signed_prefix_entry_sign. ff_h_gsp_glb_signed_prefix_entry_sign + S (gsp_sign_glb_signed_prefix_entry) = S ((S (gsp_index_glb_signed_prefix)) * sc)) /\ exists ff_q_gsp_glb_signed_prefix_entry_sign. sb = ff_q_gsp_glb_signed_prefix_entry_sign * S ((S (gsp_index_glb_signed_prefix)) * sc) + (gsp_sign_glb_signed_prefix_entry))) /\ ((exists gsp_lt_gap_glb_signed_prefix_entry_positive. gsp_lt_gap_glb_signed_prefix_entry_positive + S 0 = gsp_magnitude_glb_signed_prefix_entry) /\ ((exists gsp_le_gap_glb_signed_prefix_entry_bounded. gsp_le_gap_glb_signed_prefix_entry_bounded + gsp_magnitude_glb_signed_prefix_entry = h) /\ ((gsp_sign_glb_signed_prefix_entry = 0 \/ gsp_sign_glb_signed_prefix_entry = 1) /\ (((gsp_sign_glb_signed_prefix_entry = 0 /\ (exists gsp_mod_left_glb_signed_prefix_entry_lower gsp_mod_right_glb_signed_prefix_entry_lower. (a * gsp_value_glb_signed_prefix_entry) + p * gsp_mod_left_glb_signed_prefix_entry_lower = (gsp_magnitude_glb_signed_prefix_entry) + p * gsp_mod_right_glb_signed_prefix_entry_lower)) \/ (gsp_sign_glb_signed_prefix_entry = 1 /\ (exists gsp_mod_left_glb_signed_prefix_entry_reflected gsp_mod_right_glb_signed_prefix_entry_reflected. (a * gsp_value_glb_signed_prefix_entry) + p * gsp_mod_left_glb_signed_prefix_entry_reflected = ((2 * h) * gsp_magnitude_glb_signed_prefix_entry) + p * gsp_mod_right_glb_signed_prefix_entry_reflected))))))))))) /\ (((exists ff_u_glb_count_sum ff_v_glb_count_sum. ((((exists ff_h_glb_count_sum_start. ff_h_glb_count_sum_start + S (0) = S ((S (0)) * ff_v_glb_count_sum)) /\ exists ff_q_glb_count_sum_start. ff_u_glb_count_sum = ff_q_glb_count_sum_start * S ((S (0)) * ff_v_glb_count_sum) + (0))) /\ ((((exists ff_h_glb_count_sum_terminal. ff_h_glb_count_sum_terminal + S (e) = S ((S (h)) * ff_v_glb_count_sum)) /\ exists ff_q_glb_count_sum_terminal. ff_u_glb_count_sum = ff_q_glb_count_sum_terminal * S ((S (h)) * ff_v_glb_count_sum) + (e))) /\ forall ff_i_glb_count_sum. (exists ff_lt_glb_count_sum_bound. ff_lt_glb_count_sum_bound + S ff_i_glb_count_sum = h) -> exists ff_a_glb_count_sum ff_r_glb_count_sum ff_s_glb_count_sum. ((((exists ff_h_glb_count_sum_summand. ff_h_glb_count_sum_summand + S (ff_a_glb_count_sum) = S ((S (ff_i_glb_count_sum)) * sc)) /\ exists ff_q_glb_count_sum_summand. sb = ff_q_glb_count_sum_summand * S ((S (ff_i_glb_count_sum)) * sc) + (ff_a_glb_count_sum))) /\ ((((exists ff_h_glb_count_sum_partial. ff_h_glb_count_sum_partial + S (ff_r_glb_count_sum) = S ((S (ff_i_glb_count_sum)) * ff_v_glb_count_sum)) /\ exists ff_q_glb_count_sum_partial. ff_u_glb_count_sum = ff_q_glb_count_sum_partial * S ((S (ff_i_glb_count_sum)) * ff_v_glb_count_sum) + (ff_r_glb_count_sum))) /\ ((((exists ff_h_glb_count_sum_successor. ff_h_glb_count_sum_successor + S (ff_s_glb_count_sum) = S ((S (S ff_i_glb_count_sum)) * ff_v_glb_count_sum)) /\ exists ff_q_glb_count_sum_successor. ff_u_glb_count_sum = ff_q_glb_count_sum_successor * S ((S (S ff_i_glb_count_sum)) * ff_v_glb_count_sum) + (ff_s_glb_count_sum))) /\ ff_s_glb_count_sum = ff_r_glb_count_sum + ff_a_glb_count_sum)))))) /\ (forall ff_i_glb_count_bits. (exists ff_lt_glb_count_bits_bound. ff_lt_glb_count_bits_bound + S ff_i_glb_count_bits = h) -> exists ff_bit_glb_count_bits. ((((exists ff_h_glb_count_bits_decoded. ff_h_glb_count_bits_decoded + S (ff_bit_glb_count_bits) = S ((S (ff_i_glb_count_bits)) * sc)) /\ exists ff_q_glb_count_bits_decoded. sb = ff_q_glb_count_bits_decoded * S ((S (ff_i_glb_count_bits)) * sc) + (ff_bit_glb_count_bits))) /\ (ff_bit_glb_count_bits = 0 \/ ff_bit_glb_count_bits = 1))))))) /\ (exists wpp_mod_left_glb_a_mod_r wpp_mod_right_glb_a_mod_r. (A) + p * wpp_mod_left_glb_a_mod_r = (R) + p * wpp_mod_right_glb_a_mod_r))))
  21. 0021specialize gauss_lemma_power_congruence_exists p
  22. 0022specialize gauss_lemma_power_congruence_exists h
  23. 0023specialize gauss_lemma_power_congruence_exists a
  24. 0024specialize gauss_lemma_power_congruence_exists b
  25. 0025specialize gauss_lemma_power_congruence_exists c
  26. 0026apply gauss_lemma_power_congruence_exists
  27. 0027exact hpodd
  28. 0028exact hprime
  29. 0029exact hnotdiv
  30. 0030exact hhalf
  31. 0031cases hgauss
  32. 0032cases hgauss_witness
  33. 0033cases hgauss_witness_witness
  34. 0034cases hgauss_witness_witness_witness
  35. 0035cases hgauss_witness_witness_witness_right
  36. 0036cases hgauss_witness_witness_witness_right_right
  37. 0037have heuler : (QRes(p,a) → ModEq(p,x1,1)) ∧ (ModEq(p,x1,1) → QRes(p,a)) ∧ ((¬QRes(p,a) → ModEq(p,x1,2 · h)) ∧ (ModEq(p,x1,2 · h) → ¬QRes(p,a)))
    Exact native replay linehave heuler : (((((exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres) -> (exists wpp_mod_left_glb_local_a_mod_one wpp_mod_right_glb_local_a_mod_one. (x1) + p * wpp_mod_left_glb_local_a_mod_one = (1) + p * wpp_mod_right_glb_local_a_mod_one)) /\ ((exists wpp_mod_left_glb_local_a_mod_one wpp_mod_right_glb_local_a_mod_one. (x1) + p * wpp_mod_left_glb_local_a_mod_one = (1) + p * wpp_mod_right_glb_local_a_mod_one) -> (exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres)))) /\ ((~(exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres) -> (exists wpp_mod_left_glb_local_a_mod_predecessor wpp_mod_right_glb_local_a_mod_predecessor. (x1) + p * wpp_mod_left_glb_local_a_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_local_a_mod_predecessor)) /\ ((exists wpp_mod_left_glb_local_a_mod_predecessor wpp_mod_right_glb_local_a_mod_predecessor. (x1) + p * wpp_mod_left_glb_local_a_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_local_a_mod_predecessor) -> ~(exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres))))
  38. 0038specialize arbitrary_euler_criterion_complete p
  39. 0039specialize arbitrary_euler_criterion_complete a
  40. 0040specialize arbitrary_euler_criterion_complete (2 * h)
  41. 0041specialize arbitrary_euler_criterion_complete h
  42. 0042specialize arbitrary_euler_criterion_complete x1
  43. 0043apply arbitrary_euler_criterion_complete
  44. 0044exact hpsucc
  45. 0045exact hprime
  46. 0046exact hnotdiv
  47. 0047symm
  48. 0048exact hdouble
  49. 0049exact hgauss_witness_witness_witness_left
  50. 0050cases heuler
  51. 0051cases heuler_left
  52. 0052cases heuler_right
  53. 0053have hbridge : (Even(x) → ModEq(p,x2,1)) ∧ (Odd(x) → ModEq(p,x2,2 · h))
    Exact native replay linehave hbridge : (((exists gs_even_glb_local_even. x = 2 * gs_even_glb_local_even) -> (exists wpp_mod_left_glb_local_r_mod_one wpp_mod_right_glb_local_r_mod_one. (x2) + p * wpp_mod_left_glb_local_r_mod_one = (1) + p * wpp_mod_right_glb_local_r_mod_one)) /\ ((exists gs_odd_glb_local_odd. x = 2 * gs_odd_glb_local_odd + 1) -> (exists wpp_mod_left_glb_local_r_mod_predecessor wpp_mod_right_glb_local_r_mod_predecessor. (x2) + p * wpp_mod_left_glb_local_r_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_local_r_mod_predecessor)))
  54. 0054specialize pow_predecessor_parity_mod p
  55. 0055specialize pow_predecessor_parity_mod (2 * h)
  56. 0056specialize pow_predecessor_parity_mod x
  57. 0057specialize pow_predecessor_parity_mod x2
  58. 0058apply pow_predecessor_parity_mod
  59. 0059exact hpsucc
  60. 0060exact hgauss_witness_witness_witness_right_left
  61. 0061cases hbridge
  62. 0062have hseparation : ¬ModEq(p,1,2 · h)
    Exact native replay linehave hseparation : ~(exists wpp_mod_left_glb_one_mod_predecessor wpp_mod_right_glb_one_mod_predecessor. (1) + p * wpp_mod_left_glb_one_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_one_mod_predecessor)
  63. 0063intro hcollision
  64. 0064specialize odd_prime_one_not_mod_predecessor p
  65. 0065specialize odd_prime_one_not_mod_predecessor (2 * h)
  66. 0066specialize odd_prime_one_not_mod_predecessor h
  67. 0067apply odd_prime_one_not_mod_predecessor
  68. 0068exact hpsucc
  69. 0069exact hprime
  70. 0070symm
  71. 0071exact hdouble
  72. 0072exact hcollision
  73. 0073have hqres_even : QRes(p,a) → Even(x)
    Exact native replay linehave hqres_even : (exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres) -> (exists gs_even_glb_local_even. x = 2 * gs_even_glb_local_even)
  74. 0074intro hqres
  75. 0075specialize parity_cases x
  76. 0076cases parity_cases
  77. 0077cases parity_cases_witness
  78. 0078exists x3
  79. 0079exact parity_cases_witness_left
  80. 0080exfalso
  81. 0081apply hseparation
  82. 0082have hAone : ModEq(p,x1,1)
    Exact native replay linehave hAone : exists wpp_mod_left_glb_local_a_mod_one wpp_mod_right_glb_local_a_mod_one. (x1) + p * wpp_mod_left_glb_local_a_mod_one = (1) + p * wpp_mod_right_glb_local_a_mod_one
  83. 0083apply heuler_left_left
  84. 0084exact hqres
  85. 0085have honeA : ModEq(p,1,x1)
    Exact native replay linehave honeA : exists wpp_mod_left_glb_local_one_mod_a wpp_mod_right_glb_local_one_mod_a. (1) + p * wpp_mod_left_glb_local_one_mod_a = (x1) + p * wpp_mod_right_glb_local_one_mod_a
  86. 0086specialize mod_eq_symm p
  87. 0087specialize mod_eq_symm x1
  88. 0088specialize mod_eq_symm 1
  89. 0089apply mod_eq_symm
  90. 0090exact hAone
  91. 0091have honeR : ModEq(p,1,x2)
    Exact native replay linehave honeR : exists wpp_mod_left_glb_local_one_mod_r wpp_mod_right_glb_local_one_mod_r. (1) + p * wpp_mod_left_glb_local_one_mod_r = (x2) + p * wpp_mod_right_glb_local_one_mod_r
  92. 0092specialize mod_eq_trans p
  93. 0093specialize mod_eq_trans 1
  94. 0094specialize mod_eq_trans x1
  95. 0095specialize mod_eq_trans x2
  96. 0096apply mod_eq_trans
  97. 0097exact honeA
  98. 0098exact hgauss_witness_witness_witness_right_right_right
  99. 0099have hRpred : ModEq(p,x2,2 · h)
    Exact native replay linehave hRpred : exists wpp_mod_left_glb_local_r_mod_predecessor wpp_mod_right_glb_local_r_mod_predecessor. (x2) + p * wpp_mod_left_glb_local_r_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_local_r_mod_predecessor
  100. 0100apply hbridge_right
  101. 0101exists x3
  102. 0102exact parity_cases_witness_right
  103. 0103specialize mod_eq_trans p
  104. 0104specialize mod_eq_trans 1
  105. 0105specialize mod_eq_trans x2
  106. 0106specialize mod_eq_trans (2 * h)
  107. 0107apply mod_eq_trans
  108. 0108exact honeR
  109. 0109exact hRpred
  110. 0110have heven_qres : Even(x) → QRes(p,a)
    Exact native replay linehave heven_qres : (exists gs_even_glb_local_even. x = 2 * gs_even_glb_local_even) -> (exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres)
  111. 0111intro heven
  112. 0112have hRone : ModEq(p,x2,1)
    Exact native replay linehave hRone : exists wpp_mod_left_glb_local_r_mod_one wpp_mod_right_glb_local_r_mod_one. (x2) + p * wpp_mod_left_glb_local_r_mod_one = (1) + p * wpp_mod_right_glb_local_r_mod_one
  113. 0113apply hbridge_left
  114. 0114exact heven
  115. 0115have hAone : ModEq(p,x1,1)
    Exact native replay linehave hAone : exists wpp_mod_left_glb_local_a_mod_one wpp_mod_right_glb_local_a_mod_one. (x1) + p * wpp_mod_left_glb_local_a_mod_one = (1) + p * wpp_mod_right_glb_local_a_mod_one
  116. 0116specialize mod_eq_trans p
  117. 0117specialize mod_eq_trans x1
  118. 0118specialize mod_eq_trans x2
  119. 0119specialize mod_eq_trans 1
  120. 0120apply mod_eq_trans
  121. 0121exact hgauss_witness_witness_witness_right_right_right
  122. 0122exact hRone
  123. 0123apply heuler_left_right
  124. 0124exact hAone
  125. 0125have hnonres_odd : ¬QRes(p,a) → Odd(x)
    Exact native replay linehave hnonres_odd : ~(exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres) -> (exists gs_odd_glb_local_odd. x = 2 * gs_odd_glb_local_odd + 1)
  126. 0126intro hnonres
  127. 0127specialize parity_cases x
  128. 0128cases parity_cases
  129. 0129cases parity_cases_witness
  130. 0130exfalso
  131. 0131apply hseparation
  132. 0132have hRone : ModEq(p,x2,1)
    Exact native replay linehave hRone : exists wpp_mod_left_glb_local_r_mod_one wpp_mod_right_glb_local_r_mod_one. (x2) + p * wpp_mod_left_glb_local_r_mod_one = (1) + p * wpp_mod_right_glb_local_r_mod_one
  133. 0133apply hbridge_left
  134. 0134exists x3
  135. 0135exact parity_cases_witness_left
  136. 0136have hAone : ModEq(p,x1,1)
    Exact native replay linehave hAone : exists wpp_mod_left_glb_local_a_mod_one wpp_mod_right_glb_local_a_mod_one. (x1) + p * wpp_mod_left_glb_local_a_mod_one = (1) + p * wpp_mod_right_glb_local_a_mod_one
  137. 0137specialize mod_eq_trans p
  138. 0138specialize mod_eq_trans x1
  139. 0139specialize mod_eq_trans x2
  140. 0140specialize mod_eq_trans 1
  141. 0141apply mod_eq_trans
  142. 0142exact hgauss_witness_witness_witness_right_right_right
  143. 0143exact hRone
  144. 0144have honeA : ModEq(p,1,x1)
    Exact native replay linehave honeA : exists wpp_mod_left_glb_local_one_mod_a wpp_mod_right_glb_local_one_mod_a. (1) + p * wpp_mod_left_glb_local_one_mod_a = (x1) + p * wpp_mod_right_glb_local_one_mod_a
  145. 0145specialize mod_eq_symm p
  146. 0146specialize mod_eq_symm x1
  147. 0147specialize mod_eq_symm 1
  148. 0148apply mod_eq_symm
  149. 0149exact hAone
  150. 0150have hApred : ModEq(p,x1,2 · h)
    Exact native replay linehave hApred : exists wpp_mod_left_glb_local_a_mod_predecessor wpp_mod_right_glb_local_a_mod_predecessor. (x1) + p * wpp_mod_left_glb_local_a_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_local_a_mod_predecessor
  151. 0151apply heuler_right_left
  152. 0152exact hnonres
  153. 0153specialize mod_eq_trans p
  154. 0154specialize mod_eq_trans 1
  155. 0155specialize mod_eq_trans x1
  156. 0156specialize mod_eq_trans (2 * h)
  157. 0157apply mod_eq_trans
  158. 0158exact honeA
  159. 0159exact hApred
  160. 0160exists x3
  161. 0161exact parity_cases_witness_right
  162. 0162have hodd_nonres : Odd(x) → ¬QRes(p,a)
    Exact native replay linehave hodd_nonres : (exists gs_odd_glb_local_odd. x = 2 * gs_odd_glb_local_odd + 1) -> ~(exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres)
  163. 0163intro hodd
  164. 0164have hRpred : ModEq(p,x2,2 · h)
    Exact native replay linehave hRpred : exists wpp_mod_left_glb_local_r_mod_predecessor wpp_mod_right_glb_local_r_mod_predecessor. (x2) + p * wpp_mod_left_glb_local_r_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_local_r_mod_predecessor
  165. 0165apply hbridge_right
  166. 0166exact hodd
  167. 0167have hApred : ModEq(p,x1,2 · h)
    Exact native replay linehave hApred : exists wpp_mod_left_glb_local_a_mod_predecessor wpp_mod_right_glb_local_a_mod_predecessor. (x1) + p * wpp_mod_left_glb_local_a_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_local_a_mod_predecessor
  168. 0168specialize mod_eq_trans p
  169. 0169specialize mod_eq_trans x1
  170. 0170specialize mod_eq_trans x2
  171. 0171specialize mod_eq_trans (2 * h)
  172. 0172apply mod_eq_trans
  173. 0173exact hgauss_witness_witness_witness_right_right_right
  174. 0174exact hRpred
  175. 0175intro hqres
  176. 0176apply heuler_right_right
  177. 0177exact hApred
  178. 0178exact hqres
  179. 0179exists x
  180. 0180split
  181. 0181exact hgauss_witness_witness_witness_right_right_left
  182. 0182split
  183. 0183split
  184. 0184exact hqres_even
  185. 0185exact heven_qres
  186. 0186split
  187. 0187exact hnonres_odd
  188. 0188exact hodd_nonres