PA008M

quadratic_residue_half_power_mod_one

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

A nonzero quadratic residue has half power one modulo an odd prime.

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.

Exact expanded PA statement

forall p h a A. p = 2 * h + 1 -> ((~(p = 1) /\ forall frm_prime_left_euler_residue_prime frm_prime_right_euler_residue_prime. p = frm_prime_left_euler_residue_prime * frm_prime_right_euler_residue_prime -> frm_prime_left_euler_residue_prime = 1 \/ frm_prime_right_euler_residue_prime = 1)) -> (~(exists frm_factor_euler_residue_value. a = p * frm_factor_euler_residue_value)) -> (exists qr_x_euler_residue. exists qr_u_euler_residue qr_v_euler_residue. qr_x_euler_residue * qr_x_euler_residue + p * qr_u_euler_residue = a + p * qr_v_euler_residue) -> (exists ff_b_euler_residue_half ff_c_euler_residue_half. ((forall ff_i_euler_residue_half_repeat. (exists ff_lt_euler_residue_half_repeat_bound. ff_lt_euler_residue_half_repeat_bound + S ff_i_euler_residue_half_repeat = h) -> (((exists ff_h_euler_residue_half_repeat_decoded. ff_h_euler_residue_half_repeat_decoded + S (a) = S ((S (ff_i_euler_residue_half_repeat)) * ff_c_euler_residue_half)) /\ exists ff_q_euler_residue_half_repeat_decoded. ff_b_euler_residue_half = ff_q_euler_residue_half_repeat_decoded * S ((S (ff_i_euler_residue_half_repeat)) * ff_c_euler_residue_half) + (a)))) /\ (exists ff_u_euler_residue_half_product ff_v_euler_residue_half_product. ((((exists ff_h_euler_residue_half_product_start. ff_h_euler_residue_half_product_start + S (1) = S ((S (0)) * ff_v_euler_residue_half_product)) /\ exists ff_q_euler_residue_half_product_start. ff_u_euler_residue_half_product = ff_q_euler_residue_half_product_start * S ((S (0)) * ff_v_euler_residue_half_product) + (1))) /\ ((((exists ff_h_euler_residue_half_product_terminal. ff_h_euler_residue_half_product_terminal + S (A) = S ((S (h)) * ff_v_euler_residue_half_product)) /\ exists ff_q_euler_residue_half_product_terminal. ff_u_euler_residue_half_product = ff_q_euler_residue_half_product_terminal * S ((S (h)) * ff_v_euler_residue_half_product) + (A))) /\ forall ff_i_euler_residue_half_product. (exists ff_lt_euler_residue_half_product_bound. ff_lt_euler_residue_half_product_bound + S ff_i_euler_residue_half_product = h) -> exists ff_p_euler_residue_half_product ff_r_euler_residue_half_product ff_s_euler_residue_half_product. ((((exists ff_h_euler_residue_half_product_factor. ff_h_euler_residue_half_product_factor + S (ff_p_euler_residue_half_product) = S ((S (ff_i_euler_residue_half_product)) * ff_c_euler_residue_half)) /\ exists ff_q_euler_residue_half_product_factor. ff_b_euler_residue_half = ff_q_euler_residue_half_product_factor * S ((S (ff_i_euler_residue_half_product)) * ff_c_euler_residue_half) + (ff_p_euler_residue_half_product))) /\ ((((exists ff_h_euler_residue_half_product_partial. ff_h_euler_residue_half_product_partial + S (ff_r_euler_residue_half_product) = S ((S (ff_i_euler_residue_half_product)) * ff_v_euler_residue_half_product)) /\ exists ff_q_euler_residue_half_product_partial. ff_u_euler_residue_half_product = ff_q_euler_residue_half_product_partial * S ((S (ff_i_euler_residue_half_product)) * ff_v_euler_residue_half_product) + (ff_r_euler_residue_half_product))) /\ ((((exists ff_h_euler_residue_half_product_successor. ff_h_euler_residue_half_product_successor + S (ff_s_euler_residue_half_product) = S ((S (S ff_i_euler_residue_half_product)) * ff_v_euler_residue_half_product)) /\ exists ff_q_euler_residue_half_product_successor. ff_u_euler_residue_half_product = ff_q_euler_residue_half_product_successor * S ((S (S ff_i_euler_residue_half_product)) * ff_v_euler_residue_half_product) + (ff_s_euler_residue_half_product))) /\ ff_s_euler_residue_half_product = ff_r_euler_residue_half_product * ff_p_euler_residue_half_product)))))))) -> (exists wpp_mod_left_euler_residue_result wpp_mod_right_euler_residue_result. (A) + p * wpp_mod_left_euler_residue_result = (1) + p * wpp_mod_right_euler_residue_result)

Structural proof guide

Generated structural guide

A nonzero quadratic residue has half power one modulo an odd prime.

Use the direct prerequisites mod_eq_zero_to_dvd_nonzero, prime_nonzero, multiple_mul_right, dvd_to_mod_zero, mod_eq_symm, mod_eq_trans, pow_exists, pow_two, pow_mul_exp, fermat_predecessor_exponent_mod_one, pow_mod_congruent as previously established PA formulas.

The proof proceeds by case analysis (4), intermediate claims (21), equality transport (2), certified simplification (1).

Referenced ingredients

PA008A mod_eq_zero_to_dvd_nonzero PA0031 prime_nonzero PA000C multiple_mul_right PA0021 dvd_to_mod_zero PA003L mod_eq_symm PA0024 mod_eq_trans PA0046 pow_exists PA005W pow_two PA005Y pow_mul_exp PA008L fermat_predecessor_exponent_mod_one PA005I pow_mod_congruent

Proof neighborhood

Direct dependencies

PA008A mod_eq_zero_to_dvd_nonzero PA0031 prime_nonzero PA000C multiple_mul_right PA0021 dvd_to_mod_zero PA003L mod_eq_symm PA0024 mod_eq_trans PA0046 pow_exists PA005W pow_two PA005Y pow_mul_exp PA008L fermat_predecessor_exponent_mod_one PA005I pow_mod_congruent

Direct dependents

PA00BN bounded_euler_criterion_dichotomy

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

136 script commands · 28 reading checkpoints · 21 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.

Named ingredients (11)
mod eq zero to dvd nonzeroprime nonzeromultiple mul rightdvd to mod zeromod eq symmmod eq transpow existspow twopow mul expfermat predecessor exponent mod onepow mod congruent

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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 A
  5. L5
    intro hshape
  6. L6
    intro hp
  7. L7
    intro hnonzero
  8. L8
    intro hresidue
  9. L9
    intro hA
02Separate the logical casesL10–10

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

  1. L10
    cases hresidue
03Establish hp0L11–16

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

  1. L11
    have hp0 : ~(p = 0)
  2. L12
    intro hpzero
  3. L13
    specialize prime_nonzero p
  4. L14
    apply prime_nonzero
  5. L15
    exact hp
  6. L16
    exact hpzero
04Establish hroot_nonzeroL17–18

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

  1. L17
    have hroot_nonzero : ~(exists k. x = p * k)
  2. L18
    intro hroot_divides
05Establish hsquare_dividesL19–24

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

  1. L19
    have hsquare_divides : exists k. x * x = p * k
  2. L20
    specialize multiple_mul_right p
  3. L21
    specialize multiple_mul_right x
  4. L22
    specialize multiple_mul_right x
  5. L23
    apply multiple_mul_right
  6. L24
    exact hroot_divides
06Establish hsquare_zeroL25–29

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

  1. L25
    have hsquare_zero : exists wpp_mod_left_euler_root_square_zero wpp_mod_right_euler_root_square_zero. (x * x) + p * wpp_mod_left_euler_root_square_zero = (0) + p * wpp_mod_right_euler_root_square_zero
  2. L26
    specialize dvd_to_mod_zero p
  3. L27
    specialize dvd_to_mod_zero (x * x)
  4. L28
    apply dvd_to_mod_zero
  5. L29
    exact hsquare_divides
07Establish hvalue_squareL30–35

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

  1. L30
    have hvalue_square : exists wpp_mod_left_euler_value_square wpp_mod_right_euler_value_square. (a) + p * wpp_mod_left_euler_value_square = (x * x) + p * wpp_mod_right_euler_value_square
  2. L31
    specialize mod_eq_symm p
  3. L32
    specialize mod_eq_symm (x * x)
  4. L33
    specialize mod_eq_symm a
  5. L34
    apply mod_eq_symm
  6. L35
    exact hresidue_witness
08Establish hvalue_zeroL36–43

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

  1. L36
    have hvalue_zero : exists wpp_mod_left_euler_value_zero wpp_mod_right_euler_value_zero. (a) + p * wpp_mod_left_euler_value_zero = (0) + p * wpp_mod_right_euler_value_zero
  2. L37
    specialize mod_eq_trans p
  3. L38
    specialize mod_eq_trans a
  4. L39
    specialize mod_eq_trans (x * x)
  5. L40
    specialize mod_eq_trans 0
  6. L41
    apply mod_eq_trans
  7. L42
    exact hvalue_square
  8. L43
    exact hsquare_zero
09Establish hvalue_dividesL44–51

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

  1. L44
    have hvalue_divides : exists k. a = p * k
  2. L45
    specialize mod_eq_zero_to_dvd_nonzero p
  3. L46
    specialize mod_eq_zero_to_dvd_nonzero a
  4. L47
    apply mod_eq_zero_to_dvd_nonzero
  5. L48
    exact hp0
  6. L49
    exact hvalue_zero
  7. L50
    apply hnonzero
  8. L51
    exact hvalue_divides
10Establish hroot_two_existsL52–55

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

  1. L52
    have hroot_two_exists : ∃ R. Pow(x,2,R)Definitions: Pow
  2. L53
    specialize pow_exists x
  3. L54
    specialize pow_exists 2
  4. L55
    exact pow_exists
11Separate the logical casesL56–56

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

  1. L56
    cases hroot_two_exists
12Establish hroot_twoL57–58

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

  1. L57
    have hroot_two : Pow(x,2,x1)Definitions: Pow
  2. L58
    exact hroot_two_exists_witness
13Establish hroot_two_eqL59–65

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

  1. L59
    have hroot_two_eq : x1 = x * x
  2. L60
    specialize pow_two x
  3. L61
    specialize pow_two 2
  4. L62
    specialize pow_two x1
  5. L63
    apply pow_two
  6. L64
    refl
  7. L65
    exact hroot_two
14Establish hsquare_half_existsL66–69

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

  1. L66
    have hsquare_half_exists : ∃ R. Pow(x1,h,R)Definitions: Pow
  2. L67
    specialize pow_exists x1
  3. L68
    specialize pow_exists h
  4. L69
    exact pow_exists
15Separate the logical casesL70–70

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

  1. L70
    cases hsquare_half_exists
16Establish hsquare_halfL71–72

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

  1. L71
    have hsquare_half : Pow(x1,h,x2)Definitions: Pow
  2. L72
    exact hsquare_half_exists_witness
17Establish hroot_total_existsL73–76

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

  1. L73
    have hroot_total_exists : ∃ R. Pow(x,2 · h,R)Definitions: Pow
  2. L74
    specialize pow_exists x
  3. L75
    specialize pow_exists (2 * h)
  4. L76
    exact pow_exists
18Separate the logical casesL77–77

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

  1. L77
    cases hroot_total_exists
19Establish hroot_totalL78–79

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

  1. L78
    have hroot_total : Pow(x,2 · h,x3)Definitions: Pow
  2. L79
    exact hroot_total_exists_witness
20Establish hiteratedL80–89

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

  1. L80
    have hiterated : x2 = x3
  2. L81
    specialize pow_mul_exp x
  3. L82
    specialize pow_mul_exp 2
  4. L83
    specialize pow_mul_exp h
  5. L84
    specialize pow_mul_exp (2 * h)
  6. L85
    specialize pow_mul_exp x1
  7. L86
    specialize pow_mul_exp x2
  8. L87
    specialize pow_mul_exp x3
  9. L88
    apply pow_mul_exp
  10. L89
    refl
21Use earlier factsL90–92

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

  1. L90
    exact hroot_two
  2. L91
    exact hsquare_half
  3. L92
    exact hroot_total
22Establish hpredecessorL93–96

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

  1. L93
    have hpredecessor : p = S (2 * h)
  2. L94
    trans 2 * h + 1
  3. L95
    exact hshape
  4. L96
    simp
23Establish hfermatL97–106

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

  1. L97
    have hfermat : exists wpp_mod_left_euler_root_fermat wpp_mod_right_euler_root_fermat. (x3) + p * wpp_mod_left_euler_root_fermat = (1) + p * wpp_mod_right_euler_root_fermat
  2. L98
    specialize fermat_predecessor_exponent_mod_one p
  3. L99
    specialize fermat_predecessor_exponent_mod_one (2 * h)
  4. L100
    specialize fermat_predecessor_exponent_mod_one x
  5. L101
    specialize fermat_predecessor_exponent_mod_one x3
  6. L102
    apply fermat_predecessor_exponent_mod_one
  7. L103
    exact hpredecessor
  8. L104
    exact hp
  9. L105
    exact hroot_nonzero
  10. L106
    exact hroot_total
24Establish hsquare_valueL107–109

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

  1. L107
    have hsquare_value : exists wpp_mod_left_euler_square_value wpp_mod_right_euler_square_value. (x1) + p * wpp_mod_left_euler_square_value = (a) + p * wpp_mod_right_euler_square_value
  2. L108
    rewrite hroot_two_eq
  3. L109
    exact hresidue_witness
25Establish hpowersL110–119

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

  1. L110
    have hpowers : exists wpp_mod_left_euler_powers_congruent wpp_mod_right_euler_powers_congruent. (x2) + p * wpp_mod_left_euler_powers_congruent = (A) + p * wpp_mod_right_euler_powers_congruent
  2. L111
    specialize pow_mod_congruent p
  3. L112
    specialize pow_mod_congruent x1
  4. L113
    specialize pow_mod_congruent a
  5. L114
    specialize pow_mod_congruent h
  6. L115
    specialize pow_mod_congruent x2
  7. L116
    specialize pow_mod_congruent A
  8. L117
    apply pow_mod_congruent
  9. L118
    exact hsquare_value
  10. L119
    exact hsquare_half
26Use earlier factsL120–120

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

  1. L120
    exact hA
27Establish hbackL121–126

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

  1. L121
    have hback : exists wpp_mod_left_euler_value_power_back wpp_mod_right_euler_value_power_back. (A) + p * wpp_mod_left_euler_value_power_back = (x2) + p * wpp_mod_right_euler_value_power_back
  2. L122
    specialize mod_eq_symm p
  3. L123
    specialize mod_eq_symm x2
  4. L124
    specialize mod_eq_symm A
  5. L125
    apply mod_eq_symm
  6. L126
    exact hpowers
28Establish hhalf_oneL127–136

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

  1. L127
    have hhalf_one : exists wpp_mod_left_euler_root_half_one wpp_mod_right_euler_root_half_one. (x2) + p * wpp_mod_left_euler_root_half_one = (1) + p * wpp_mod_right_euler_root_half_one
  2. L128
    rewrite hiterated
  3. L129
    exact hfermat
  4. L130
    specialize mod_eq_trans p
  5. L131
    specialize mod_eq_trans A
  6. L132
    specialize mod_eq_trans x2
  7. L133
    specialize mod_eq_trans 1
  8. L134
    apply mod_eq_trans
  9. L135
    exact hback
  10. L136
    exact hhalf_one

Library-wide reading audit

Original exact command ledger · 136 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro a
  4. 0004intro A
  5. 0005intro hshape
  6. 0006intro hp
  7. 0007intro hnonzero
  8. 0008intro hresidue
  9. 0009intro hA
  10. 0010cases hresidue
  11. 0011have hp0 : ~(p = 0)
  12. 0012intro hpzero
  13. 0013specialize prime_nonzero p
  14. 0014apply prime_nonzero
  15. 0015exact hp
  16. 0016exact hpzero
  17. 0017have hroot_nonzero : ~(exists k. x = p * k)
  18. 0018intro hroot_divides
  19. 0019have hsquare_divides : exists k. x * x = p * k
  20. 0020specialize multiple_mul_right p
  21. 0021specialize multiple_mul_right x
  22. 0022specialize multiple_mul_right x
  23. 0023apply multiple_mul_right
  24. 0024exact hroot_divides
  25. 0025have hsquare_zero : exists wpp_mod_left_euler_root_square_zero wpp_mod_right_euler_root_square_zero. (x * x) + p * wpp_mod_left_euler_root_square_zero = (0) + p * wpp_mod_right_euler_root_square_zero
  26. 0026specialize dvd_to_mod_zero p
  27. 0027specialize dvd_to_mod_zero (x * x)
  28. 0028apply dvd_to_mod_zero
  29. 0029exact hsquare_divides
  30. 0030have hvalue_square : exists wpp_mod_left_euler_value_square wpp_mod_right_euler_value_square. (a) + p * wpp_mod_left_euler_value_square = (x * x) + p * wpp_mod_right_euler_value_square
  31. 0031specialize mod_eq_symm p
  32. 0032specialize mod_eq_symm (x * x)
  33. 0033specialize mod_eq_symm a
  34. 0034apply mod_eq_symm
  35. 0035exact hresidue_witness
  36. 0036have hvalue_zero : exists wpp_mod_left_euler_value_zero wpp_mod_right_euler_value_zero. (a) + p * wpp_mod_left_euler_value_zero = (0) + p * wpp_mod_right_euler_value_zero
  37. 0037specialize mod_eq_trans p
  38. 0038specialize mod_eq_trans a
  39. 0039specialize mod_eq_trans (x * x)
  40. 0040specialize mod_eq_trans 0
  41. 0041apply mod_eq_trans
  42. 0042exact hvalue_square
  43. 0043exact hsquare_zero
  44. 0044have hvalue_divides : exists k. a = p * k
  45. 0045specialize mod_eq_zero_to_dvd_nonzero p
  46. 0046specialize mod_eq_zero_to_dvd_nonzero a
  47. 0047apply mod_eq_zero_to_dvd_nonzero
  48. 0048exact hp0
  49. 0049exact hvalue_zero
  50. 0050apply hnonzero
  51. 0051exact hvalue_divides
  52. 0052have hroot_two_exists : exists R. (exists pa_b_euler_root_two_exists pa_c_euler_root_two_exists. ((forall pa_i_euler_root_two_exists_repeat. (exists pa_lt_euler_root_two_exists_repeat_bound. pa_lt_euler_root_two_exists_repeat_bound + S pa_i_euler_root_two_exists_repeat = 2) -> (((exists pa_h_euler_root_two_exists_repeat_decoded. pa_h_euler_root_two_exists_repeat_decoded + S (x) = S ((S (pa_i_euler_root_two_exists_repeat)) * pa_c_euler_root_two_exists)) /\ exists pa_q_euler_root_two_exists_repeat_decoded. pa_b_euler_root_two_exists = pa_q_euler_root_two_exists_repeat_decoded * S ((S (pa_i_euler_root_two_exists_repeat)) * pa_c_euler_root_two_exists) + (x)))) /\ (exists pa_u_euler_root_two_exists_product pa_v_euler_root_two_exists_product. ((((exists pa_h_euler_root_two_exists_product_start. pa_h_euler_root_two_exists_product_start + S (1) = S ((S (0)) * pa_v_euler_root_two_exists_product)) /\ exists pa_q_euler_root_two_exists_product_start. pa_u_euler_root_two_exists_product = pa_q_euler_root_two_exists_product_start * S ((S (0)) * pa_v_euler_root_two_exists_product) + (1))) /\ ((((exists pa_h_euler_root_two_exists_product_terminal. pa_h_euler_root_two_exists_product_terminal + S (R) = S ((S (2)) * pa_v_euler_root_two_exists_product)) /\ exists pa_q_euler_root_two_exists_product_terminal. pa_u_euler_root_two_exists_product = pa_q_euler_root_two_exists_product_terminal * S ((S (2)) * pa_v_euler_root_two_exists_product) + (R))) /\ forall pa_i_euler_root_two_exists_product. (exists pa_lt_euler_root_two_exists_product_bound. pa_lt_euler_root_two_exists_product_bound + S pa_i_euler_root_two_exists_product = 2) -> exists pa_p_euler_root_two_exists_product pa_r_euler_root_two_exists_product pa_s_euler_root_two_exists_product. ((((exists pa_h_euler_root_two_exists_product_factor. pa_h_euler_root_two_exists_product_factor + S (pa_p_euler_root_two_exists_product) = S ((S (pa_i_euler_root_two_exists_product)) * pa_c_euler_root_two_exists)) /\ exists pa_q_euler_root_two_exists_product_factor. pa_b_euler_root_two_exists = pa_q_euler_root_two_exists_product_factor * S ((S (pa_i_euler_root_two_exists_product)) * pa_c_euler_root_two_exists) + (pa_p_euler_root_two_exists_product))) /\ ((((exists pa_h_euler_root_two_exists_product_partial. pa_h_euler_root_two_exists_product_partial + S (pa_r_euler_root_two_exists_product) = S ((S (pa_i_euler_root_two_exists_product)) * pa_v_euler_root_two_exists_product)) /\ exists pa_q_euler_root_two_exists_product_partial. pa_u_euler_root_two_exists_product = pa_q_euler_root_two_exists_product_partial * S ((S (pa_i_euler_root_two_exists_product)) * pa_v_euler_root_two_exists_product) + (pa_r_euler_root_two_exists_product))) /\ ((((exists pa_h_euler_root_two_exists_product_successor. pa_h_euler_root_two_exists_product_successor + S (pa_s_euler_root_two_exists_product) = S ((S (S pa_i_euler_root_two_exists_product)) * pa_v_euler_root_two_exists_product)) /\ exists pa_q_euler_root_two_exists_product_successor. pa_u_euler_root_two_exists_product = pa_q_euler_root_two_exists_product_successor * S ((S (S pa_i_euler_root_two_exists_product)) * pa_v_euler_root_two_exists_product) + (pa_s_euler_root_two_exists_product))) /\ pa_s_euler_root_two_exists_product = pa_r_euler_root_two_exists_product * pa_p_euler_root_two_exists_product))))))))
  53. 0053specialize pow_exists x
  54. 0054specialize pow_exists 2
  55. 0055exact pow_exists
  56. 0056cases hroot_two_exists
  57. 0057have hroot_two : exists pa_b_euler_root_two pa_c_euler_root_two. ((forall pa_i_euler_root_two_repeat. (exists pa_lt_euler_root_two_repeat_bound. pa_lt_euler_root_two_repeat_bound + S pa_i_euler_root_two_repeat = 2) -> (((exists pa_h_euler_root_two_repeat_decoded. pa_h_euler_root_two_repeat_decoded + S (x) = S ((S (pa_i_euler_root_two_repeat)) * pa_c_euler_root_two)) /\ exists pa_q_euler_root_two_repeat_decoded. pa_b_euler_root_two = pa_q_euler_root_two_repeat_decoded * S ((S (pa_i_euler_root_two_repeat)) * pa_c_euler_root_two) + (x)))) /\ (exists pa_u_euler_root_two_product pa_v_euler_root_two_product. ((((exists pa_h_euler_root_two_product_start. pa_h_euler_root_two_product_start + S (1) = S ((S (0)) * pa_v_euler_root_two_product)) /\ exists pa_q_euler_root_two_product_start. pa_u_euler_root_two_product = pa_q_euler_root_two_product_start * S ((S (0)) * pa_v_euler_root_two_product) + (1))) /\ ((((exists pa_h_euler_root_two_product_terminal. pa_h_euler_root_two_product_terminal + S (x1) = S ((S (2)) * pa_v_euler_root_two_product)) /\ exists pa_q_euler_root_two_product_terminal. pa_u_euler_root_two_product = pa_q_euler_root_two_product_terminal * S ((S (2)) * pa_v_euler_root_two_product) + (x1))) /\ forall pa_i_euler_root_two_product. (exists pa_lt_euler_root_two_product_bound. pa_lt_euler_root_two_product_bound + S pa_i_euler_root_two_product = 2) -> exists pa_p_euler_root_two_product pa_r_euler_root_two_product pa_s_euler_root_two_product. ((((exists pa_h_euler_root_two_product_factor. pa_h_euler_root_two_product_factor + S (pa_p_euler_root_two_product) = S ((S (pa_i_euler_root_two_product)) * pa_c_euler_root_two)) /\ exists pa_q_euler_root_two_product_factor. pa_b_euler_root_two = pa_q_euler_root_two_product_factor * S ((S (pa_i_euler_root_two_product)) * pa_c_euler_root_two) + (pa_p_euler_root_two_product))) /\ ((((exists pa_h_euler_root_two_product_partial. pa_h_euler_root_two_product_partial + S (pa_r_euler_root_two_product) = S ((S (pa_i_euler_root_two_product)) * pa_v_euler_root_two_product)) /\ exists pa_q_euler_root_two_product_partial. pa_u_euler_root_two_product = pa_q_euler_root_two_product_partial * S ((S (pa_i_euler_root_two_product)) * pa_v_euler_root_two_product) + (pa_r_euler_root_two_product))) /\ ((((exists pa_h_euler_root_two_product_successor. pa_h_euler_root_two_product_successor + S (pa_s_euler_root_two_product) = S ((S (S pa_i_euler_root_two_product)) * pa_v_euler_root_two_product)) /\ exists pa_q_euler_root_two_product_successor. pa_u_euler_root_two_product = pa_q_euler_root_two_product_successor * S ((S (S pa_i_euler_root_two_product)) * pa_v_euler_root_two_product) + (pa_s_euler_root_two_product))) /\ pa_s_euler_root_two_product = pa_r_euler_root_two_product * pa_p_euler_root_two_product)))))))
  58. 0058exact hroot_two_exists_witness
  59. 0059have hroot_two_eq : x1 = x * x
  60. 0060specialize pow_two x
  61. 0061specialize pow_two 2
  62. 0062specialize pow_two x1
  63. 0063apply pow_two
  64. 0064refl
  65. 0065exact hroot_two
  66. 0066have hsquare_half_exists : exists R. (exists ff_b_euler_square_half_exists ff_c_euler_square_half_exists. ((forall ff_i_euler_square_half_exists_repeat. (exists ff_lt_euler_square_half_exists_repeat_bound. ff_lt_euler_square_half_exists_repeat_bound + S ff_i_euler_square_half_exists_repeat = h) -> (((exists ff_h_euler_square_half_exists_repeat_decoded. ff_h_euler_square_half_exists_repeat_decoded + S (x1) = S ((S (ff_i_euler_square_half_exists_repeat)) * ff_c_euler_square_half_exists)) /\ exists ff_q_euler_square_half_exists_repeat_decoded. ff_b_euler_square_half_exists = ff_q_euler_square_half_exists_repeat_decoded * S ((S (ff_i_euler_square_half_exists_repeat)) * ff_c_euler_square_half_exists) + (x1)))) /\ (exists ff_u_euler_square_half_exists_product ff_v_euler_square_half_exists_product. ((((exists ff_h_euler_square_half_exists_product_start. ff_h_euler_square_half_exists_product_start + S (1) = S ((S (0)) * ff_v_euler_square_half_exists_product)) /\ exists ff_q_euler_square_half_exists_product_start. ff_u_euler_square_half_exists_product = ff_q_euler_square_half_exists_product_start * S ((S (0)) * ff_v_euler_square_half_exists_product) + (1))) /\ ((((exists ff_h_euler_square_half_exists_product_terminal. ff_h_euler_square_half_exists_product_terminal + S (R) = S ((S (h)) * ff_v_euler_square_half_exists_product)) /\ exists ff_q_euler_square_half_exists_product_terminal. ff_u_euler_square_half_exists_product = ff_q_euler_square_half_exists_product_terminal * S ((S (h)) * ff_v_euler_square_half_exists_product) + (R))) /\ forall ff_i_euler_square_half_exists_product. (exists ff_lt_euler_square_half_exists_product_bound. ff_lt_euler_square_half_exists_product_bound + S ff_i_euler_square_half_exists_product = h) -> exists ff_p_euler_square_half_exists_product ff_r_euler_square_half_exists_product ff_s_euler_square_half_exists_product. ((((exists ff_h_euler_square_half_exists_product_factor. ff_h_euler_square_half_exists_product_factor + S (ff_p_euler_square_half_exists_product) = S ((S (ff_i_euler_square_half_exists_product)) * ff_c_euler_square_half_exists)) /\ exists ff_q_euler_square_half_exists_product_factor. ff_b_euler_square_half_exists = ff_q_euler_square_half_exists_product_factor * S ((S (ff_i_euler_square_half_exists_product)) * ff_c_euler_square_half_exists) + (ff_p_euler_square_half_exists_product))) /\ ((((exists ff_h_euler_square_half_exists_product_partial. ff_h_euler_square_half_exists_product_partial + S (ff_r_euler_square_half_exists_product) = S ((S (ff_i_euler_square_half_exists_product)) * ff_v_euler_square_half_exists_product)) /\ exists ff_q_euler_square_half_exists_product_partial. ff_u_euler_square_half_exists_product = ff_q_euler_square_half_exists_product_partial * S ((S (ff_i_euler_square_half_exists_product)) * ff_v_euler_square_half_exists_product) + (ff_r_euler_square_half_exists_product))) /\ ((((exists ff_h_euler_square_half_exists_product_successor. ff_h_euler_square_half_exists_product_successor + S (ff_s_euler_square_half_exists_product) = S ((S (S ff_i_euler_square_half_exists_product)) * ff_v_euler_square_half_exists_product)) /\ exists ff_q_euler_square_half_exists_product_successor. ff_u_euler_square_half_exists_product = ff_q_euler_square_half_exists_product_successor * S ((S (S ff_i_euler_square_half_exists_product)) * ff_v_euler_square_half_exists_product) + (ff_s_euler_square_half_exists_product))) /\ ff_s_euler_square_half_exists_product = ff_r_euler_square_half_exists_product * ff_p_euler_square_half_exists_product))))))))
  67. 0067specialize pow_exists x1
  68. 0068specialize pow_exists h
  69. 0069exact pow_exists
  70. 0070cases hsquare_half_exists
  71. 0071have hsquare_half : exists ff_b_euler_square_half ff_c_euler_square_half. ((forall ff_i_euler_square_half_repeat. (exists ff_lt_euler_square_half_repeat_bound. ff_lt_euler_square_half_repeat_bound + S ff_i_euler_square_half_repeat = h) -> (((exists ff_h_euler_square_half_repeat_decoded. ff_h_euler_square_half_repeat_decoded + S (x1) = S ((S (ff_i_euler_square_half_repeat)) * ff_c_euler_square_half)) /\ exists ff_q_euler_square_half_repeat_decoded. ff_b_euler_square_half = ff_q_euler_square_half_repeat_decoded * S ((S (ff_i_euler_square_half_repeat)) * ff_c_euler_square_half) + (x1)))) /\ (exists ff_u_euler_square_half_product ff_v_euler_square_half_product. ((((exists ff_h_euler_square_half_product_start. ff_h_euler_square_half_product_start + S (1) = S ((S (0)) * ff_v_euler_square_half_product)) /\ exists ff_q_euler_square_half_product_start. ff_u_euler_square_half_product = ff_q_euler_square_half_product_start * S ((S (0)) * ff_v_euler_square_half_product) + (1))) /\ ((((exists ff_h_euler_square_half_product_terminal. ff_h_euler_square_half_product_terminal + S (x2) = S ((S (h)) * ff_v_euler_square_half_product)) /\ exists ff_q_euler_square_half_product_terminal. ff_u_euler_square_half_product = ff_q_euler_square_half_product_terminal * S ((S (h)) * ff_v_euler_square_half_product) + (x2))) /\ forall ff_i_euler_square_half_product. (exists ff_lt_euler_square_half_product_bound. ff_lt_euler_square_half_product_bound + S ff_i_euler_square_half_product = h) -> exists ff_p_euler_square_half_product ff_r_euler_square_half_product ff_s_euler_square_half_product. ((((exists ff_h_euler_square_half_product_factor. ff_h_euler_square_half_product_factor + S (ff_p_euler_square_half_product) = S ((S (ff_i_euler_square_half_product)) * ff_c_euler_square_half)) /\ exists ff_q_euler_square_half_product_factor. ff_b_euler_square_half = ff_q_euler_square_half_product_factor * S ((S (ff_i_euler_square_half_product)) * ff_c_euler_square_half) + (ff_p_euler_square_half_product))) /\ ((((exists ff_h_euler_square_half_product_partial. ff_h_euler_square_half_product_partial + S (ff_r_euler_square_half_product) = S ((S (ff_i_euler_square_half_product)) * ff_v_euler_square_half_product)) /\ exists ff_q_euler_square_half_product_partial. ff_u_euler_square_half_product = ff_q_euler_square_half_product_partial * S ((S (ff_i_euler_square_half_product)) * ff_v_euler_square_half_product) + (ff_r_euler_square_half_product))) /\ ((((exists ff_h_euler_square_half_product_successor. ff_h_euler_square_half_product_successor + S (ff_s_euler_square_half_product) = S ((S (S ff_i_euler_square_half_product)) * ff_v_euler_square_half_product)) /\ exists ff_q_euler_square_half_product_successor. ff_u_euler_square_half_product = ff_q_euler_square_half_product_successor * S ((S (S ff_i_euler_square_half_product)) * ff_v_euler_square_half_product) + (ff_s_euler_square_half_product))) /\ ff_s_euler_square_half_product = ff_r_euler_square_half_product * ff_p_euler_square_half_product)))))))
  72. 0072exact hsquare_half_exists_witness
  73. 0073have hroot_total_exists : exists R. (exists pa_b_euler_root_total_exists pa_c_euler_root_total_exists. ((forall pa_i_euler_root_total_exists_repeat. (exists pa_lt_euler_root_total_exists_repeat_bound. pa_lt_euler_root_total_exists_repeat_bound + S pa_i_euler_root_total_exists_repeat = 2 * h) -> (((exists pa_h_euler_root_total_exists_repeat_decoded. pa_h_euler_root_total_exists_repeat_decoded + S (x) = S ((S (pa_i_euler_root_total_exists_repeat)) * pa_c_euler_root_total_exists)) /\ exists pa_q_euler_root_total_exists_repeat_decoded. pa_b_euler_root_total_exists = pa_q_euler_root_total_exists_repeat_decoded * S ((S (pa_i_euler_root_total_exists_repeat)) * pa_c_euler_root_total_exists) + (x)))) /\ (exists pa_u_euler_root_total_exists_product pa_v_euler_root_total_exists_product. ((((exists pa_h_euler_root_total_exists_product_start. pa_h_euler_root_total_exists_product_start + S (1) = S ((S (0)) * pa_v_euler_root_total_exists_product)) /\ exists pa_q_euler_root_total_exists_product_start. pa_u_euler_root_total_exists_product = pa_q_euler_root_total_exists_product_start * S ((S (0)) * pa_v_euler_root_total_exists_product) + (1))) /\ ((((exists pa_h_euler_root_total_exists_product_terminal. pa_h_euler_root_total_exists_product_terminal + S (R) = S ((S (2 * h)) * pa_v_euler_root_total_exists_product)) /\ exists pa_q_euler_root_total_exists_product_terminal. pa_u_euler_root_total_exists_product = pa_q_euler_root_total_exists_product_terminal * S ((S (2 * h)) * pa_v_euler_root_total_exists_product) + (R))) /\ forall pa_i_euler_root_total_exists_product. (exists pa_lt_euler_root_total_exists_product_bound. pa_lt_euler_root_total_exists_product_bound + S pa_i_euler_root_total_exists_product = 2 * h) -> exists pa_p_euler_root_total_exists_product pa_r_euler_root_total_exists_product pa_s_euler_root_total_exists_product. ((((exists pa_h_euler_root_total_exists_product_factor. pa_h_euler_root_total_exists_product_factor + S (pa_p_euler_root_total_exists_product) = S ((S (pa_i_euler_root_total_exists_product)) * pa_c_euler_root_total_exists)) /\ exists pa_q_euler_root_total_exists_product_factor. pa_b_euler_root_total_exists = pa_q_euler_root_total_exists_product_factor * S ((S (pa_i_euler_root_total_exists_product)) * pa_c_euler_root_total_exists) + (pa_p_euler_root_total_exists_product))) /\ ((((exists pa_h_euler_root_total_exists_product_partial. pa_h_euler_root_total_exists_product_partial + S (pa_r_euler_root_total_exists_product) = S ((S (pa_i_euler_root_total_exists_product)) * pa_v_euler_root_total_exists_product)) /\ exists pa_q_euler_root_total_exists_product_partial. pa_u_euler_root_total_exists_product = pa_q_euler_root_total_exists_product_partial * S ((S (pa_i_euler_root_total_exists_product)) * pa_v_euler_root_total_exists_product) + (pa_r_euler_root_total_exists_product))) /\ ((((exists pa_h_euler_root_total_exists_product_successor. pa_h_euler_root_total_exists_product_successor + S (pa_s_euler_root_total_exists_product) = S ((S (S pa_i_euler_root_total_exists_product)) * pa_v_euler_root_total_exists_product)) /\ exists pa_q_euler_root_total_exists_product_successor. pa_u_euler_root_total_exists_product = pa_q_euler_root_total_exists_product_successor * S ((S (S pa_i_euler_root_total_exists_product)) * pa_v_euler_root_total_exists_product) + (pa_s_euler_root_total_exists_product))) /\ pa_s_euler_root_total_exists_product = pa_r_euler_root_total_exists_product * pa_p_euler_root_total_exists_product))))))))
  74. 0074specialize pow_exists x
  75. 0075specialize pow_exists (2 * h)
  76. 0076exact pow_exists
  77. 0077cases hroot_total_exists
  78. 0078have hroot_total : exists pa_b_euler_root_double_half pa_c_euler_root_double_half. ((forall pa_i_euler_root_double_half_repeat. (exists pa_lt_euler_root_double_half_repeat_bound. pa_lt_euler_root_double_half_repeat_bound + S pa_i_euler_root_double_half_repeat = 2 * h) -> (((exists pa_h_euler_root_double_half_repeat_decoded. pa_h_euler_root_double_half_repeat_decoded + S (x) = S ((S (pa_i_euler_root_double_half_repeat)) * pa_c_euler_root_double_half)) /\ exists pa_q_euler_root_double_half_repeat_decoded. pa_b_euler_root_double_half = pa_q_euler_root_double_half_repeat_decoded * S ((S (pa_i_euler_root_double_half_repeat)) * pa_c_euler_root_double_half) + (x)))) /\ (exists pa_u_euler_root_double_half_product pa_v_euler_root_double_half_product. ((((exists pa_h_euler_root_double_half_product_start. pa_h_euler_root_double_half_product_start + S (1) = S ((S (0)) * pa_v_euler_root_double_half_product)) /\ exists pa_q_euler_root_double_half_product_start. pa_u_euler_root_double_half_product = pa_q_euler_root_double_half_product_start * S ((S (0)) * pa_v_euler_root_double_half_product) + (1))) /\ ((((exists pa_h_euler_root_double_half_product_terminal. pa_h_euler_root_double_half_product_terminal + S (x3) = S ((S (2 * h)) * pa_v_euler_root_double_half_product)) /\ exists pa_q_euler_root_double_half_product_terminal. pa_u_euler_root_double_half_product = pa_q_euler_root_double_half_product_terminal * S ((S (2 * h)) * pa_v_euler_root_double_half_product) + (x3))) /\ forall pa_i_euler_root_double_half_product. (exists pa_lt_euler_root_double_half_product_bound. pa_lt_euler_root_double_half_product_bound + S pa_i_euler_root_double_half_product = 2 * h) -> exists pa_p_euler_root_double_half_product pa_r_euler_root_double_half_product pa_s_euler_root_double_half_product. ((((exists pa_h_euler_root_double_half_product_factor. pa_h_euler_root_double_half_product_factor + S (pa_p_euler_root_double_half_product) = S ((S (pa_i_euler_root_double_half_product)) * pa_c_euler_root_double_half)) /\ exists pa_q_euler_root_double_half_product_factor. pa_b_euler_root_double_half = pa_q_euler_root_double_half_product_factor * S ((S (pa_i_euler_root_double_half_product)) * pa_c_euler_root_double_half) + (pa_p_euler_root_double_half_product))) /\ ((((exists pa_h_euler_root_double_half_product_partial. pa_h_euler_root_double_half_product_partial + S (pa_r_euler_root_double_half_product) = S ((S (pa_i_euler_root_double_half_product)) * pa_v_euler_root_double_half_product)) /\ exists pa_q_euler_root_double_half_product_partial. pa_u_euler_root_double_half_product = pa_q_euler_root_double_half_product_partial * S ((S (pa_i_euler_root_double_half_product)) * pa_v_euler_root_double_half_product) + (pa_r_euler_root_double_half_product))) /\ ((((exists pa_h_euler_root_double_half_product_successor. pa_h_euler_root_double_half_product_successor + S (pa_s_euler_root_double_half_product) = S ((S (S pa_i_euler_root_double_half_product)) * pa_v_euler_root_double_half_product)) /\ exists pa_q_euler_root_double_half_product_successor. pa_u_euler_root_double_half_product = pa_q_euler_root_double_half_product_successor * S ((S (S pa_i_euler_root_double_half_product)) * pa_v_euler_root_double_half_product) + (pa_s_euler_root_double_half_product))) /\ pa_s_euler_root_double_half_product = pa_r_euler_root_double_half_product * pa_p_euler_root_double_half_product)))))))
  79. 0079exact hroot_total_exists_witness
  80. 0080have hiterated : x2 = x3
  81. 0081specialize pow_mul_exp x
  82. 0082specialize pow_mul_exp 2
  83. 0083specialize pow_mul_exp h
  84. 0084specialize pow_mul_exp (2 * h)
  85. 0085specialize pow_mul_exp x1
  86. 0086specialize pow_mul_exp x2
  87. 0087specialize pow_mul_exp x3
  88. 0088apply pow_mul_exp
  89. 0089refl
  90. 0090exact hroot_two
  91. 0091exact hsquare_half
  92. 0092exact hroot_total
  93. 0093have hpredecessor : p = S (2 * h)
  94. 0094trans 2 * h + 1
  95. 0095exact hshape
  96. 0096simp
  97. 0097have hfermat : exists wpp_mod_left_euler_root_fermat wpp_mod_right_euler_root_fermat. (x3) + p * wpp_mod_left_euler_root_fermat = (1) + p * wpp_mod_right_euler_root_fermat
  98. 0098specialize fermat_predecessor_exponent_mod_one p
  99. 0099specialize fermat_predecessor_exponent_mod_one (2 * h)
  100. 0100specialize fermat_predecessor_exponent_mod_one x
  101. 0101specialize fermat_predecessor_exponent_mod_one x3
  102. 0102apply fermat_predecessor_exponent_mod_one
  103. 0103exact hpredecessor
  104. 0104exact hp
  105. 0105exact hroot_nonzero
  106. 0106exact hroot_total
  107. 0107have hsquare_value : exists wpp_mod_left_euler_square_value wpp_mod_right_euler_square_value. (x1) + p * wpp_mod_left_euler_square_value = (a) + p * wpp_mod_right_euler_square_value
  108. 0108rewrite hroot_two_eq
  109. 0109exact hresidue_witness
  110. 0110have hpowers : exists wpp_mod_left_euler_powers_congruent wpp_mod_right_euler_powers_congruent. (x2) + p * wpp_mod_left_euler_powers_congruent = (A) + p * wpp_mod_right_euler_powers_congruent
  111. 0111specialize pow_mod_congruent p
  112. 0112specialize pow_mod_congruent x1
  113. 0113specialize pow_mod_congruent a
  114. 0114specialize pow_mod_congruent h
  115. 0115specialize pow_mod_congruent x2
  116. 0116specialize pow_mod_congruent A
  117. 0117apply pow_mod_congruent
  118. 0118exact hsquare_value
  119. 0119exact hsquare_half
  120. 0120exact hA
  121. 0121have hback : exists wpp_mod_left_euler_value_power_back wpp_mod_right_euler_value_power_back. (A) + p * wpp_mod_left_euler_value_power_back = (x2) + p * wpp_mod_right_euler_value_power_back
  122. 0122specialize mod_eq_symm p
  123. 0123specialize mod_eq_symm x2
  124. 0124specialize mod_eq_symm A
  125. 0125apply mod_eq_symm
  126. 0126exact hpowers
  127. 0127have hhalf_one : exists wpp_mod_left_euler_root_half_one wpp_mod_right_euler_root_half_one. (x2) + p * wpp_mod_left_euler_root_half_one = (1) + p * wpp_mod_right_euler_root_half_one
  128. 0128rewrite hiterated
  129. 0129exact hfermat
  130. 0130specialize mod_eq_trans p
  131. 0131specialize mod_eq_trans A
  132. 0132specialize mod_eq_trans x2
  133. 0133specialize mod_eq_trans 1
  134. 0134apply mod_eq_trans
  135. 0135exact hback
  136. 0136exact hhalf_one