PA00FG · theorem

distinct_odd_primes_gauss_eisenstein_data_exists

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

Distinct odd primes admit both Gauss classification counts, their mod-two quotient sums, and the exact Eisenstein sum identity.

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. ∀ q. ∀ h. ∀ k. p = 2 · h + 1 → q = 2 · k + 1 → Prime(p) → Prime(q) → ¬p = q → ∃ x. ∃ y. ∃ z. ∃ n. (QRes(p,q) → Even(x)) ∧ (Even(x) → QRes(p,q)) ∧ ((¬QRes(p,q) → Odd(x)) ∧ (Odd(x) → ¬QRes(p,q))) ∧ ((QRes(q,p) → Even(y)) ∧ (Even(y) → QRes(q,p)) ∧ ((¬QRes(q,p) → Odd(y)) ∧ (Odd(y) → ¬QRes(q,p)))) ∧ (ModEq(2,x,z) ∧ ModEq(2,y,n) ∧ z + n = h · k)

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

PD0004 Prime PD0008 ModEq PD0009 Even PD0010 Odd PD0021 QRes

20 occurrences

In local proof propositions

PD0002 Lt PD0003 Dvd PD0008 ModEq PD0009 Even PD0010 Odd PD0013 BetaAt PD0015 Sum PD0017 BitCount PD0021 QRes PD0040 DivisionPrefix

50 occurrences

Exact expanded native-PA statement
forall p q h k. p = 2 * h + 1 -> q = 2 * k + 1 -> ((~(p = 1) /\ forall gsp_prime_left_ged_pair_prime_p gsp_prime_right_ged_pair_prime_p. p = gsp_prime_left_ged_pair_prime_p * gsp_prime_right_ged_pair_prime_p -> gsp_prime_left_ged_pair_prime_p = 1 \/ gsp_prime_right_ged_pair_prime_p = 1)) -> ((~(q = 1) /\ forall gsp_prime_left_ged_pair_prime_q gsp_prime_right_ged_pair_prime_q. q = gsp_prime_left_ged_pair_prime_q * gsp_prime_right_ged_pair_prime_q -> gsp_prime_left_ged_pair_prime_q = 1 \/ gsp_prime_right_ged_pair_prime_q = 1)) -> ~(p = q) -> (exists e f Q U. ((((((((exists qr_x_ged_pair_first_classification_qres. exists qr_u_ged_pair_first_classification_qres qr_v_ged_pair_first_classification_qres. qr_x_ged_pair_first_classification_qres * qr_x_ged_pair_first_classification_qres + p * qr_u_ged_pair_first_classification_qres = q + p * qr_v_ged_pair_first_classification_qres) -> (exists gs_even_ged_pair_first_classification_even. e = 2 * gs_even_ged_pair_first_classification_even)) /\ ((exists gs_even_ged_pair_first_classification_even. e = 2 * gs_even_ged_pair_first_classification_even) -> (exists qr_x_ged_pair_first_classification_qres. exists qr_u_ged_pair_first_classification_qres qr_v_ged_pair_first_classification_qres. qr_x_ged_pair_first_classification_qres * qr_x_ged_pair_first_classification_qres + p * qr_u_ged_pair_first_classification_qres = q + p * qr_v_ged_pair_first_classification_qres)))) /\ (((~(exists qr_x_ged_pair_first_classification_qres. exists qr_u_ged_pair_first_classification_qres qr_v_ged_pair_first_classification_qres. qr_x_ged_pair_first_classification_qres * qr_x_ged_pair_first_classification_qres + p * qr_u_ged_pair_first_classification_qres = q + p * qr_v_ged_pair_first_classification_qres) -> (exists gs_odd_ged_pair_first_classification_odd. e = 2 * gs_odd_ged_pair_first_classification_odd + 1)) /\ ((exists gs_odd_ged_pair_first_classification_odd. e = 2 * gs_odd_ged_pair_first_classification_odd + 1) -> ~(exists qr_x_ged_pair_first_classification_qres. exists qr_u_ged_pair_first_classification_qres qr_v_ged_pair_first_classification_qres. qr_x_ged_pair_first_classification_qres * qr_x_ged_pair_first_classification_qres + p * qr_u_ged_pair_first_classification_qres = q + p * qr_v_ged_pair_first_classification_qres)))))) /\ ((((((exists qr_x_ged_pair_second_classification_qres. exists qr_u_ged_pair_second_classification_qres qr_v_ged_pair_second_classification_qres. qr_x_ged_pair_second_classification_qres * qr_x_ged_pair_second_classification_qres + q * qr_u_ged_pair_second_classification_qres = p + q * qr_v_ged_pair_second_classification_qres) -> (exists gs_even_ged_pair_second_classification_even. f = 2 * gs_even_ged_pair_second_classification_even)) /\ ((exists gs_even_ged_pair_second_classification_even. f = 2 * gs_even_ged_pair_second_classification_even) -> (exists qr_x_ged_pair_second_classification_qres. exists qr_u_ged_pair_second_classification_qres qr_v_ged_pair_second_classification_qres. qr_x_ged_pair_second_classification_qres * qr_x_ged_pair_second_classification_qres + q * qr_u_ged_pair_second_classification_qres = p + q * qr_v_ged_pair_second_classification_qres)))) /\ (((~(exists qr_x_ged_pair_second_classification_qres. exists qr_u_ged_pair_second_classification_qres qr_v_ged_pair_second_classification_qres. qr_x_ged_pair_second_classification_qres * qr_x_ged_pair_second_classification_qres + q * qr_u_ged_pair_second_classification_qres = p + q * qr_v_ged_pair_second_classification_qres) -> (exists gs_odd_ged_pair_second_classification_odd. f = 2 * gs_odd_ged_pair_second_classification_odd + 1)) /\ ((exists gs_odd_ged_pair_second_classification_odd. f = 2 * gs_odd_ged_pair_second_classification_odd + 1) -> ~(exists qr_x_ged_pair_second_classification_qres. exists qr_u_ged_pair_second_classification_qres qr_v_ged_pair_second_classification_qres. qr_x_ged_pair_second_classification_qres * qr_x_ged_pair_second_classification_qres + q * qr_u_ged_pair_second_classification_qres = p + q * qr_v_ged_pair_second_classification_qres))))))) /\ (((exists fspm_u_ged_pair_first_mod fspm_v_ged_pair_first_mod. (e) + 2 * fspm_u_ged_pair_first_mod = (Q) + 2 * fspm_v_ged_pair_first_mod) /\ (exists fspm_u_ged_pair_second_mod fspm_v_ged_pair_second_mod. (f) + 2 * fspm_u_ged_pair_second_mod = (U) + 2 * fspm_v_ged_pair_second_mod)) /\ Q + U = h * k)))

Proof neighborhood

Direct theorem prerequisites

PA006X distinct_primes_mutually_nondivisible PA00D7 odd_prime_gauss_eisenstein_orientation_data_exists PA00DM distinct_odd_prime_half_rectangle_total_exists PA00FF distinct_odd_prime_eisenstein_quotient_sum_identity

Direct theorem dependents

PA00FW quadratic_reciprocity_combined

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

150 script commands · 31 reading checkpoints · 9 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 (4)
distinct primes mutually nondivisibleodd prime gauss eisenstein orientation data existsdistinct odd prime half rectangle total existsdistinct odd prime eisenstein quotient sum identity
01Fix variables and assumptionsL1–9

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

  1. L1
    intro p
  2. L2
    intro q
  3. L3
    intro h
  4. L4
    intro k
  5. L5
    intro hpodd
  6. L6
    intro hqodd
  7. L7
    intro hp
  8. L8
    intro hq
  9. L9
    intro hpq
02Establish hmutualL10–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply distinct primes mutually nondivisible.

  1. L10
    have hmutual : ¬Dvd(p,q) ∧ ¬Dvd(q,p)Definitions: Dvd(p,q)Dvd(q,p)Original native command in the exact edition
  2. L11
    specialize distinct_primes_mutually_nondivisible p
  3. L12
    specialize distinct_primes_mutually_nondivisible q
  4. L13
    apply distinct_primes_mutually_nondivisible
  5. L14
    exact hp
  6. L15
    exact hq
  7. L16
    exact hpq
03Separate the logical casesL17–17

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

  1. L17
    cases hmutual
04Establish hq_oddL18–18

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

  1. L18
05Construct an explicit witnessL19–19

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

  1. L19
    exists k
06Use earlier factsL20–20

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

  1. L20
    exact hqodd
07Establish hp_oddL21–21

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

  1. L21
08Construct an explicit witnessL22–22

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

  1. L22
    exists h
09Use earlier factsL23–23

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

  1. L23
    exact hpodd
10Establish hfirstL24–32

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd prime gauss eisenstein orientation data exists.

  1. L24
    have hfirst : ∃ tb. ∃ tc. ∃ qb. ∃ qc. ∃ rb. ∃ rc. ∃ e. ∃ Q. (∀ x. ∀ y. Lt(x,h) → BetaAt(tb,tc,x,y) → y = q · (1 + x)) ∧ (DivisionPrefix(p,tb,tc,qb,qc,rb,rc,h) ∧ (Sum(qb,qc,h,Q) ∧ ((QRes(p,q) → Even(e)) ∧ (Even(e) → QRes(p,q)) ∧ ((¬QRes(p,q) → Odd(e)) ∧ (Odd(e) → ¬QRes(p,q))) ∧ ModEq(2,e,Q))))Definitions: Lt(x,h)BetaAt(tb,tc,x,y)DivisionPrefix(p,tb,tc,qb,qc,rb,rc,h)Sum(qb,qc,h,Q)QRes(p,q)Even(e)Odd(e)ModEq(2,e,Q)Original native command in the exact edition
  2. L25
    specialize odd_prime_gauss_eisenstein_orientation_data_exists p
  3. L26
    specialize odd_prime_gauss_eisenstein_orientation_data_exists h
  4. L27
    specialize odd_prime_gauss_eisenstein_orientation_data_exists q
  5. L28
    apply odd_prime_gauss_eisenstein_orientation_data_exists
  6. L29
    exact hpodd
  7. L30
    exact hq_odd
  8. L31
    exact hp
  9. L32
    exact hmutual_left
11Separate the logical casesL33–42

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

  1. L33
    cases hfirst
  2. L34
    cases hfirst_witness
  3. L35
    cases hfirst_witness_witness
  4. L36
    cases hfirst_witness_witness_witness
  5. L37
    cases hfirst_witness_witness_witness_witness
  6. L38
    cases hfirst_witness_witness_witness_witness_witness
  7. L39
    cases hfirst_witness_witness_witness_witness_witness_witness
  8. L40
    cases hfirst_witness_witness_witness_witness_witness_witness_witness
  9. L41
    cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness
  10. L42
    cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right
12Separate the logical casesL43–44

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

  1. L43
    cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right
  2. L44
    cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right
13Establish hsecondL45–53

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd prime gauss eisenstein orientation data exists.

  1. L45
    have hsecond : ∃ tb. ∃ tc. ∃ qb. ∃ qc. ∃ rb. ∃ rc. ∃ e. ∃ Q. (∀ x. ∀ y. Lt(x,k) → BetaAt(tb,tc,x,y) → y = p · (1 + x)) ∧ (DivisionPrefix(q,tb,tc,qb,qc,rb,rc,k) ∧ (Sum(qb,qc,k,Q) ∧ ((QRes(q,p) → Even(e)) ∧ (Even(e) → QRes(q,p)) ∧ ((¬QRes(q,p) → Odd(e)) ∧ (Odd(e) → ¬QRes(q,p))) ∧ ModEq(2,e,Q))))Definitions: Lt(x,k)BetaAt(tb,tc,x,y)DivisionPrefix(q,tb,tc,qb,qc,rb,rc,k)Sum(qb,qc,k,Q)QRes(q,p)Even(e)Odd(e)ModEq(2,e,Q)Original native command in the exact edition
  2. L46
    specialize odd_prime_gauss_eisenstein_orientation_data_exists q
  3. L47
    specialize odd_prime_gauss_eisenstein_orientation_data_exists k
  4. L48
    specialize odd_prime_gauss_eisenstein_orientation_data_exists p
  5. L49
    apply odd_prime_gauss_eisenstein_orientation_data_exists
  6. L50
    exact hqodd
  7. L51
    exact hp_odd
  8. L52
    exact hq
  9. L53
    exact hmutual_right
14Separate the logical casesL54–63

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

  1. L54
    cases hsecond
  2. L55
    cases hsecond_witness
  3. L56
    cases hsecond_witness_witness
  4. L57
    cases hsecond_witness_witness_witness
  5. L58
    cases hsecond_witness_witness_witness_witness
  6. L59
    cases hsecond_witness_witness_witness_witness_witness
  7. L60
    cases hsecond_witness_witness_witness_witness_witness_witness
  8. L61
    cases hsecond_witness_witness_witness_witness_witness_witness_witness
  9. L62
    cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness
  10. L63
    cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right
15Separate the logical casesL64–65

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

  1. L64
    cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right
  2. L65
    cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right
16Establish hqpL66–70

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

  1. L66
    have hqp : ~(q = p)
  2. L67
    intro hqp_eq
  3. L68
    apply hpq
  4. L69
    symm
  5. L70
    exact hqp_eq
17Establish hfirst_rectangleL71–80

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply distinct odd prime half rectangle total exists.

  1. L71
    have hfirst_rectangle : ∃ cb. ∃ cc. ∃ total. (∀ x. Lt(x,h) → ∃ y. BetaAt(cb,cc,x,y) ∧ (∃ z. ∃ n. (∀ m. Lt(m,k) → ∃ i. BetaAt(z,n,m,i) ∧ (i = 0 ∧ (Lt(q · S x,p · S m) ∧ ¬Lt(p · S m,q · S x)) ∨ i = 1 ∧ (Lt(p · S m,q · S x) ∧ ¬Lt(q · S x,p · S m)))) ∧ BitCount(z,n,k,y))) ∧ Sum(cb,cc,h,total)Definitions: Lt(x,h)BetaAt(cb,cc,x,y)Lt(m,k)BetaAt(z,n,m,i)Lt(q · S x,p · S m)Lt(p · S m,q · S x)BitCount(z,n,k,y)Sum(cb,cc,h,total)Original native command in the exact edition
  2. L72
    specialize distinct_odd_prime_half_rectangle_total_exists p
  3. L73
    specialize distinct_odd_prime_half_rectangle_total_exists q
  4. L74
    specialize distinct_odd_prime_half_rectangle_total_exists h
  5. L75
    specialize distinct_odd_prime_half_rectangle_total_exists k
  6. L76
    apply distinct_odd_prime_half_rectangle_total_exists
  7. L77
    exact hpodd
  8. L78
    exact hqodd
  9. L79
    exact hp
  10. L80
    exact hq
18Use earlier factsL81–81

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

  1. L81
    exact hpq
19Separate the logical casesL82–85

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

  1. L82
    cases hfirst_rectangle
  2. L83
    cases hfirst_rectangle_witness
  3. L84
    cases hfirst_rectangle_witness_witness
  4. L85
    cases hfirst_rectangle_witness_witness_witness
20Establish hsecond_rectangleL86–95

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply distinct odd prime half rectangle total exists.

  1. L86
    have hsecond_rectangle : ∃ cb. ∃ cc. ∃ total. (∀ x. Lt(x,k) → ∃ y. BetaAt(cb,cc,x,y) ∧ (∃ z. ∃ n. (∀ m. Lt(m,h) → ∃ i. BetaAt(z,n,m,i) ∧ (i = 0 ∧ (Lt(p · S x,q · S m) ∧ ¬Lt(q · S m,p · S x)) ∨ i = 1 ∧ (Lt(q · S m,p · S x) ∧ ¬Lt(p · S x,q · S m)))) ∧ BitCount(z,n,h,y))) ∧ Sum(cb,cc,k,total)Definitions: Lt(x,k)BetaAt(cb,cc,x,y)Lt(m,h)BetaAt(z,n,m,i)Lt(p · S x,q · S m)Lt(q · S m,p · S x)BitCount(z,n,h,y)Sum(cb,cc,k,total)Original native command in the exact edition
  2. L87
    specialize distinct_odd_prime_half_rectangle_total_exists q
  3. L88
    specialize distinct_odd_prime_half_rectangle_total_exists p
  4. L89
    specialize distinct_odd_prime_half_rectangle_total_exists k
  5. L90
    specialize distinct_odd_prime_half_rectangle_total_exists h
  6. L91
    apply distinct_odd_prime_half_rectangle_total_exists
  7. L92
    exact hqodd
  8. L93
    exact hpodd
  9. L94
    exact hq
  10. L95
    exact hp
21Use earlier factsL96–96

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

  1. L96
    exact hqp
22Separate the logical casesL97–100

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

  1. L97
    cases hsecond_rectangle
  2. L98
    cases hsecond_rectangle_witness
  3. L99
    cases hsecond_rectangle_witness_witness
  4. L100
    cases hsecond_rectangle_witness_witness_witness
23Establish hsum_identityL101–110

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

  1. L101
    have hsum_identity : x7 + x15 = h * k
  2. L102
    specialize distinct_odd_prime_eisenstein_quotient_sum_identity p
  3. L103
    specialize distinct_odd_prime_eisenstein_quotient_sum_identity q
  4. L104
    specialize distinct_odd_prime_eisenstein_quotient_sum_identity h
  5. L105
    specialize distinct_odd_prime_eisenstein_quotient_sum_identity k
  6. L106
    specialize distinct_odd_prime_eisenstein_quotient_sum_identity x
  7. L107
    specialize distinct_odd_prime_eisenstein_quotient_sum_identity x1
  8. L108
    specialize distinct_odd_prime_eisenstein_quotient_sum_identity x2
  9. L109
    specialize distinct_odd_prime_eisenstein_quotient_sum_identity x3
  10. L110
    specialize distinct_odd_prime_eisenstein_quotient_sum_identity x4
24Use earlier factsL111–120

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

  1. L111
    specialize distinct_odd_prime_eisenstein_quotient_sum_identity x5
  2. L112
    specialize distinct_odd_prime_eisenstein_quotient_sum_identity x8
  3. L113
    specialize distinct_odd_prime_eisenstein_quotient_sum_identity x9
  4. L114
    specialize distinct_odd_prime_eisenstein_quotient_sum_identity x10
  5. L115
    specialize distinct_odd_prime_eisenstein_quotient_sum_identity x11
  6. L116
    specialize distinct_odd_prime_eisenstein_quotient_sum_identity x12
  7. L117
    specialize distinct_odd_prime_eisenstein_quotient_sum_identity x13
  8. L118
    specialize distinct_odd_prime_eisenstein_quotient_sum_identity x16
  9. L119
    specialize distinct_odd_prime_eisenstein_quotient_sum_identity x17
  10. L120
    specialize distinct_odd_prime_eisenstein_quotient_sum_identity x19
25Use earlier factsL121–130

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

  1. L121
    specialize distinct_odd_prime_eisenstein_quotient_sum_identity x20
  2. L122
    specialize distinct_odd_prime_eisenstein_quotient_sum_identity x7
  3. L123
    specialize distinct_odd_prime_eisenstein_quotient_sum_identity x15
  4. L124
    apply distinct_odd_prime_eisenstein_quotient_sum_identity
  5. L125
    exact hpodd
  6. L126
    exact hqodd
  7. L127
    exact hp
  8. L128
    exact hq
  9. L129
    exact hpq
  10. L130
    exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_left
26Use earlier factsL131–137

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

  1. L131
    exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_left
  2. L132
    exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_left
  3. L133
    exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_left
  4. L134
    exact hfirst_rectangle_witness_witness_witness_left
  5. L135
    exact hsecond_rectangle_witness_witness_witness_left
  6. L136
    exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left
  7. L137
    exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left
27Construct an explicit witnessL138–141

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

  1. L138
    exists x6
  2. L139
    exists x14
  3. L140
    exists x7
  4. L141
    exists x15
28Separate the logical casesL142–143

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

  1. L142
    split
  2. L143
    split
29Use earlier factsL144–145

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

  1. L144
    exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left
  2. L145
    exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left
30Separate the logical casesL146–147

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

  1. L146
    split
  2. L147
    split
31Use earlier factsL148–150

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

  1. L148
    exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
  2. L149
    exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
  3. L150
    exact hsum_identity

Library-wide reading audit

Original defined command ledger · 150 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro h
  4. 0004intro k
  5. 0005intro hpodd
  6. 0006intro hqodd
  7. 0007intro hp
  8. 0008intro hq
  9. 0009intro hpq
  10. 0010have hmutual : ¬Dvd(p,q) ∧ ¬Dvd(q,p)
    Exact native replay linehave hmutual : ((~(exists gsp_divisor_factor_ged_pair_p_not_q. q = p * gsp_divisor_factor_ged_pair_p_not_q)) /\ (~(exists gsp_divisor_factor_ged_pair_q_not_p. p = q * gsp_divisor_factor_ged_pair_q_not_p)))
  11. 0011specialize distinct_primes_mutually_nondivisible p
  12. 0012specialize distinct_primes_mutually_nondivisible q
  13. 0013apply distinct_primes_mutually_nondivisible
  14. 0014exact hp
  15. 0015exact hq
  16. 0016exact hpq
  17. 0017cases hmutual
  18. 0018have hq_odd : Odd(q)
    Exact native replay linehave hq_odd : exists gs_odd_ged_pair_q_odd. q = 2 * gs_odd_ged_pair_q_odd + 1
  19. 0019exists k
  20. 0020exact hqodd
  21. 0021have hp_odd : Odd(p)
    Exact native replay linehave hp_odd : exists gs_odd_ged_pair_p_odd. p = 2 * gs_odd_ged_pair_p_odd + 1
  22. 0022exists h
  23. 0023exact hpodd
  24. 0024have hfirst : ∃ tb. ∃ tc. ∃ qb. ∃ qc. ∃ rb. ∃ rc. ∃ e. ∃ Q. (∀ x. ∀ y. Lt(x,h) → BetaAt(tb,tc,x,y) → y = q · (1 + x)) ∧ (DivisionPrefix(p,tb,tc,qb,qc,rb,rc,h) ∧ (Sum(qb,qc,h,Q) ∧ ((QRes(p,q) → Even(e)) ∧ (Even(e) → QRes(p,q)) ∧ ((¬QRes(p,q) → Odd(e)) ∧ (Odd(e) → ¬QRes(p,q))) ∧ ModEq(2,e,Q))))
    Exact native replay linehave hfirst : exists tb tc qb qc rb rc e Q. ((forall esd_index_ged_pair_first_scaled esd_value_ged_pair_first_scaled. (exists esd_gap_ged_pair_first_scaled. esd_gap_ged_pair_first_scaled + S esd_index_ged_pair_first_scaled = h) -> (((exists ff_h_esd_ged_pair_first_scaled_decoded. ff_h_esd_ged_pair_first_scaled_decoded + S (esd_value_ged_pair_first_scaled) = S ((S (esd_index_ged_pair_first_scaled)) * tc)) /\ exists ff_q_esd_ged_pair_first_scaled_decoded. tb = ff_q_esd_ged_pair_first_scaled_decoded * S ((S (esd_index_ged_pair_first_scaled)) * tc) + (esd_value_ged_pair_first_scaled))) -> esd_value_ged_pair_first_scaled = q * (1 + esd_index_ged_pair_first_scaled)) /\ ((forall fdp_index_ged_pair_first_division. (exists gsp_lt_gap_ged_pair_first_division_index_bound. gsp_lt_gap_ged_pair_first_division_index_bound + S fdp_index_ged_pair_first_division = h) -> exists fdp_value_ged_pair_first_division fdp_quotient_ged_pair_first_division fdp_remainder_ged_pair_first_division. (((exists ff_h_fdp_ged_pair_first_division_source. ff_h_fdp_ged_pair_first_division_source + S (fdp_value_ged_pair_first_division) = S ((S (fdp_index_ged_pair_first_division)) * tc)) /\ exists ff_q_fdp_ged_pair_first_division_source. tb = ff_q_fdp_ged_pair_first_division_source * S ((S (fdp_index_ged_pair_first_division)) * tc) + (fdp_value_ged_pair_first_division))) /\ ((((exists ff_h_fdp_ged_pair_first_division_quotient_entry. ff_h_fdp_ged_pair_first_division_quotient_entry + S (fdp_quotient_ged_pair_first_division) = S ((S (fdp_index_ged_pair_first_division)) * qc)) /\ exists ff_q_fdp_ged_pair_first_division_quotient_entry. qb = ff_q_fdp_ged_pair_first_division_quotient_entry * S ((S (fdp_index_ged_pair_first_division)) * qc) + (fdp_quotient_ged_pair_first_division))) /\ ((((exists ff_h_fdp_ged_pair_first_division_remainder_entry. ff_h_fdp_ged_pair_first_division_remainder_entry + S (fdp_remainder_ged_pair_first_division) = S ((S (fdp_index_ged_pair_first_division)) * rc)) /\ exists ff_q_fdp_ged_pair_first_division_remainder_entry. rb = ff_q_fdp_ged_pair_first_division_remainder_entry * S ((S (fdp_index_ged_pair_first_division)) * rc) + (fdp_remainder_ged_pair_first_division))) /\ (fdp_value_ged_pair_first_division = p * fdp_quotient_ged_pair_first_division + fdp_remainder_ged_pair_first_division /\ (exists gsp_lt_gap_ged_pair_first_division_remainder_bound. gsp_lt_gap_ged_pair_first_division_remainder_bound + S fdp_remainder_ged_pair_first_division = p))))) /\ ((exists ff_u_ged_pair_first_sum ff_v_ged_pair_first_sum. ((((exists ff_h_ged_pair_first_sum_start. ff_h_ged_pair_first_sum_start + S (0) = S ((S (0)) * ff_v_ged_pair_first_sum)) /\ exists ff_q_ged_pair_first_sum_start. ff_u_ged_pair_first_sum = ff_q_ged_pair_first_sum_start * S ((S (0)) * ff_v_ged_pair_first_sum) + (0))) /\ ((((exists ff_h_ged_pair_first_sum_terminal. ff_h_ged_pair_first_sum_terminal + S (Q) = S ((S (h)) * ff_v_ged_pair_first_sum)) /\ exists ff_q_ged_pair_first_sum_terminal. ff_u_ged_pair_first_sum = ff_q_ged_pair_first_sum_terminal * S ((S (h)) * ff_v_ged_pair_first_sum) + (Q))) /\ forall ff_i_ged_pair_first_sum. (exists ff_lt_ged_pair_first_sum_bound. ff_lt_ged_pair_first_sum_bound + S ff_i_ged_pair_first_sum = h) -> exists ff_a_ged_pair_first_sum ff_r_ged_pair_first_sum ff_s_ged_pair_first_sum. ((((exists ff_h_ged_pair_first_sum_summand. ff_h_ged_pair_first_sum_summand + S (ff_a_ged_pair_first_sum) = S ((S (ff_i_ged_pair_first_sum)) * qc)) /\ exists ff_q_ged_pair_first_sum_summand. qb = ff_q_ged_pair_first_sum_summand * S ((S (ff_i_ged_pair_first_sum)) * qc) + (ff_a_ged_pair_first_sum))) /\ ((((exists ff_h_ged_pair_first_sum_partial. ff_h_ged_pair_first_sum_partial + S (ff_r_ged_pair_first_sum) = S ((S (ff_i_ged_pair_first_sum)) * ff_v_ged_pair_first_sum)) /\ exists ff_q_ged_pair_first_sum_partial. ff_u_ged_pair_first_sum = ff_q_ged_pair_first_sum_partial * S ((S (ff_i_ged_pair_first_sum)) * ff_v_ged_pair_first_sum) + (ff_r_ged_pair_first_sum))) /\ ((((exists ff_h_ged_pair_first_sum_successor. ff_h_ged_pair_first_sum_successor + S (ff_s_ged_pair_first_sum) = S ((S (S ff_i_ged_pair_first_sum)) * ff_v_ged_pair_first_sum)) /\ exists ff_q_ged_pair_first_sum_successor. ff_u_ged_pair_first_sum = ff_q_ged_pair_first_sum_successor * S ((S (S ff_i_ged_pair_first_sum)) * ff_v_ged_pair_first_sum) + (ff_s_ged_pair_first_sum))) /\ ff_s_ged_pair_first_sum = ff_r_ged_pair_first_sum + ff_a_ged_pair_first_sum)))))) /\ (((((((exists qr_x_ged_pair_first_hidden_classification_qres. exists qr_u_ged_pair_first_hidden_classification_qres qr_v_ged_pair_first_hidden_classification_qres. qr_x_ged_pair_first_hidden_classification_qres * qr_x_ged_pair_first_hidden_classification_qres + p * qr_u_ged_pair_first_hidden_classification_qres = q + p * qr_v_ged_pair_first_hidden_classification_qres) -> (exists gs_even_ged_pair_first_hidden_classification_even. e = 2 * gs_even_ged_pair_first_hidden_classification_even)) /\ ((exists gs_even_ged_pair_first_hidden_classification_even. e = 2 * gs_even_ged_pair_first_hidden_classification_even) -> (exists qr_x_ged_pair_first_hidden_classification_qres. exists qr_u_ged_pair_first_hidden_classification_qres qr_v_ged_pair_first_hidden_classification_qres. qr_x_ged_pair_first_hidden_classification_qres * qr_x_ged_pair_first_hidden_classification_qres + p * qr_u_ged_pair_first_hidden_classification_qres = q + p * qr_v_ged_pair_first_hidden_classification_qres)))) /\ (((~(exists qr_x_ged_pair_first_hidden_classification_qres. exists qr_u_ged_pair_first_hidden_classification_qres qr_v_ged_pair_first_hidden_classification_qres. qr_x_ged_pair_first_hidden_classification_qres * qr_x_ged_pair_first_hidden_classification_qres + p * qr_u_ged_pair_first_hidden_classification_qres = q + p * qr_v_ged_pair_first_hidden_classification_qres) -> (exists gs_odd_ged_pair_first_hidden_classification_odd. e = 2 * gs_odd_ged_pair_first_hidden_classification_odd + 1)) /\ ((exists gs_odd_ged_pair_first_hidden_classification_odd. e = 2 * gs_odd_ged_pair_first_hidden_classification_odd + 1) -> ~(exists qr_x_ged_pair_first_hidden_classification_qres. exists qr_u_ged_pair_first_hidden_classification_qres qr_v_ged_pair_first_hidden_classification_qres. qr_x_ged_pair_first_hidden_classification_qres * qr_x_ged_pair_first_hidden_classification_qres + p * qr_u_ged_pair_first_hidden_classification_qres = q + p * qr_v_ged_pair_first_hidden_classification_qres)))))) /\ (exists fspm_u_ged_pair_first_hidden_mod fspm_v_ged_pair_first_hidden_mod. (e) + 2 * fspm_u_ged_pair_first_hidden_mod = (Q) + 2 * fspm_v_ged_pair_first_hidden_mod)))))
  25. 0025specialize odd_prime_gauss_eisenstein_orientation_data_exists p
  26. 0026specialize odd_prime_gauss_eisenstein_orientation_data_exists h
  27. 0027specialize odd_prime_gauss_eisenstein_orientation_data_exists q
  28. 0028apply odd_prime_gauss_eisenstein_orientation_data_exists
  29. 0029exact hpodd
  30. 0030exact hq_odd
  31. 0031exact hp
  32. 0032exact hmutual_left
  33. 0033cases hfirst
  34. 0034cases hfirst_witness
  35. 0035cases hfirst_witness_witness
  36. 0036cases hfirst_witness_witness_witness
  37. 0037cases hfirst_witness_witness_witness_witness
  38. 0038cases hfirst_witness_witness_witness_witness_witness
  39. 0039cases hfirst_witness_witness_witness_witness_witness_witness
  40. 0040cases hfirst_witness_witness_witness_witness_witness_witness_witness
  41. 0041cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness
  42. 0042cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right
  43. 0043cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right
  44. 0044cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right
  45. 0045have hsecond : ∃ tb. ∃ tc. ∃ qb. ∃ qc. ∃ rb. ∃ rc. ∃ e. ∃ Q. (∀ x. ∀ y. Lt(x,k) → BetaAt(tb,tc,x,y) → y = p · (1 + x)) ∧ (DivisionPrefix(q,tb,tc,qb,qc,rb,rc,k) ∧ (Sum(qb,qc,k,Q) ∧ ((QRes(q,p) → Even(e)) ∧ (Even(e) → QRes(q,p)) ∧ ((¬QRes(q,p) → Odd(e)) ∧ (Odd(e) → ¬QRes(q,p))) ∧ ModEq(2,e,Q))))
    Exact native replay linehave hsecond : exists tb tc qb qc rb rc e Q. ((forall esd_index_ged_pair_second_scaled esd_value_ged_pair_second_scaled. (exists esd_gap_ged_pair_second_scaled. esd_gap_ged_pair_second_scaled + S esd_index_ged_pair_second_scaled = k) -> (((exists ff_h_esd_ged_pair_second_scaled_decoded. ff_h_esd_ged_pair_second_scaled_decoded + S (esd_value_ged_pair_second_scaled) = S ((S (esd_index_ged_pair_second_scaled)) * tc)) /\ exists ff_q_esd_ged_pair_second_scaled_decoded. tb = ff_q_esd_ged_pair_second_scaled_decoded * S ((S (esd_index_ged_pair_second_scaled)) * tc) + (esd_value_ged_pair_second_scaled))) -> esd_value_ged_pair_second_scaled = p * (1 + esd_index_ged_pair_second_scaled)) /\ ((forall fdp_index_ged_pair_second_division. (exists gsp_lt_gap_ged_pair_second_division_index_bound. gsp_lt_gap_ged_pair_second_division_index_bound + S fdp_index_ged_pair_second_division = k) -> exists fdp_value_ged_pair_second_division fdp_quotient_ged_pair_second_division fdp_remainder_ged_pair_second_division. (((exists ff_h_fdp_ged_pair_second_division_source. ff_h_fdp_ged_pair_second_division_source + S (fdp_value_ged_pair_second_division) = S ((S (fdp_index_ged_pair_second_division)) * tc)) /\ exists ff_q_fdp_ged_pair_second_division_source. tb = ff_q_fdp_ged_pair_second_division_source * S ((S (fdp_index_ged_pair_second_division)) * tc) + (fdp_value_ged_pair_second_division))) /\ ((((exists ff_h_fdp_ged_pair_second_division_quotient_entry. ff_h_fdp_ged_pair_second_division_quotient_entry + S (fdp_quotient_ged_pair_second_division) = S ((S (fdp_index_ged_pair_second_division)) * qc)) /\ exists ff_q_fdp_ged_pair_second_division_quotient_entry. qb = ff_q_fdp_ged_pair_second_division_quotient_entry * S ((S (fdp_index_ged_pair_second_division)) * qc) + (fdp_quotient_ged_pair_second_division))) /\ ((((exists ff_h_fdp_ged_pair_second_division_remainder_entry. ff_h_fdp_ged_pair_second_division_remainder_entry + S (fdp_remainder_ged_pair_second_division) = S ((S (fdp_index_ged_pair_second_division)) * rc)) /\ exists ff_q_fdp_ged_pair_second_division_remainder_entry. rb = ff_q_fdp_ged_pair_second_division_remainder_entry * S ((S (fdp_index_ged_pair_second_division)) * rc) + (fdp_remainder_ged_pair_second_division))) /\ (fdp_value_ged_pair_second_division = q * fdp_quotient_ged_pair_second_division + fdp_remainder_ged_pair_second_division /\ (exists gsp_lt_gap_ged_pair_second_division_remainder_bound. gsp_lt_gap_ged_pair_second_division_remainder_bound + S fdp_remainder_ged_pair_second_division = q))))) /\ ((exists ff_u_ged_pair_second_sum ff_v_ged_pair_second_sum. ((((exists ff_h_ged_pair_second_sum_start. ff_h_ged_pair_second_sum_start + S (0) = S ((S (0)) * ff_v_ged_pair_second_sum)) /\ exists ff_q_ged_pair_second_sum_start. ff_u_ged_pair_second_sum = ff_q_ged_pair_second_sum_start * S ((S (0)) * ff_v_ged_pair_second_sum) + (0))) /\ ((((exists ff_h_ged_pair_second_sum_terminal. ff_h_ged_pair_second_sum_terminal + S (Q) = S ((S (k)) * ff_v_ged_pair_second_sum)) /\ exists ff_q_ged_pair_second_sum_terminal. ff_u_ged_pair_second_sum = ff_q_ged_pair_second_sum_terminal * S ((S (k)) * ff_v_ged_pair_second_sum) + (Q))) /\ forall ff_i_ged_pair_second_sum. (exists ff_lt_ged_pair_second_sum_bound. ff_lt_ged_pair_second_sum_bound + S ff_i_ged_pair_second_sum = k) -> exists ff_a_ged_pair_second_sum ff_r_ged_pair_second_sum ff_s_ged_pair_second_sum. ((((exists ff_h_ged_pair_second_sum_summand. ff_h_ged_pair_second_sum_summand + S (ff_a_ged_pair_second_sum) = S ((S (ff_i_ged_pair_second_sum)) * qc)) /\ exists ff_q_ged_pair_second_sum_summand. qb = ff_q_ged_pair_second_sum_summand * S ((S (ff_i_ged_pair_second_sum)) * qc) + (ff_a_ged_pair_second_sum))) /\ ((((exists ff_h_ged_pair_second_sum_partial. ff_h_ged_pair_second_sum_partial + S (ff_r_ged_pair_second_sum) = S ((S (ff_i_ged_pair_second_sum)) * ff_v_ged_pair_second_sum)) /\ exists ff_q_ged_pair_second_sum_partial. ff_u_ged_pair_second_sum = ff_q_ged_pair_second_sum_partial * S ((S (ff_i_ged_pair_second_sum)) * ff_v_ged_pair_second_sum) + (ff_r_ged_pair_second_sum))) /\ ((((exists ff_h_ged_pair_second_sum_successor. ff_h_ged_pair_second_sum_successor + S (ff_s_ged_pair_second_sum) = S ((S (S ff_i_ged_pair_second_sum)) * ff_v_ged_pair_second_sum)) /\ exists ff_q_ged_pair_second_sum_successor. ff_u_ged_pair_second_sum = ff_q_ged_pair_second_sum_successor * S ((S (S ff_i_ged_pair_second_sum)) * ff_v_ged_pair_second_sum) + (ff_s_ged_pair_second_sum))) /\ ff_s_ged_pair_second_sum = ff_r_ged_pair_second_sum + ff_a_ged_pair_second_sum)))))) /\ (((((((exists qr_x_ged_pair_second_hidden_classification_qres. exists qr_u_ged_pair_second_hidden_classification_qres qr_v_ged_pair_second_hidden_classification_qres. qr_x_ged_pair_second_hidden_classification_qres * qr_x_ged_pair_second_hidden_classification_qres + q * qr_u_ged_pair_second_hidden_classification_qres = p + q * qr_v_ged_pair_second_hidden_classification_qres) -> (exists gs_even_ged_pair_second_hidden_classification_even. e = 2 * gs_even_ged_pair_second_hidden_classification_even)) /\ ((exists gs_even_ged_pair_second_hidden_classification_even. e = 2 * gs_even_ged_pair_second_hidden_classification_even) -> (exists qr_x_ged_pair_second_hidden_classification_qres. exists qr_u_ged_pair_second_hidden_classification_qres qr_v_ged_pair_second_hidden_classification_qres. qr_x_ged_pair_second_hidden_classification_qres * qr_x_ged_pair_second_hidden_classification_qres + q * qr_u_ged_pair_second_hidden_classification_qres = p + q * qr_v_ged_pair_second_hidden_classification_qres)))) /\ (((~(exists qr_x_ged_pair_second_hidden_classification_qres. exists qr_u_ged_pair_second_hidden_classification_qres qr_v_ged_pair_second_hidden_classification_qres. qr_x_ged_pair_second_hidden_classification_qres * qr_x_ged_pair_second_hidden_classification_qres + q * qr_u_ged_pair_second_hidden_classification_qres = p + q * qr_v_ged_pair_second_hidden_classification_qres) -> (exists gs_odd_ged_pair_second_hidden_classification_odd. e = 2 * gs_odd_ged_pair_second_hidden_classification_odd + 1)) /\ ((exists gs_odd_ged_pair_second_hidden_classification_odd. e = 2 * gs_odd_ged_pair_second_hidden_classification_odd + 1) -> ~(exists qr_x_ged_pair_second_hidden_classification_qres. exists qr_u_ged_pair_second_hidden_classification_qres qr_v_ged_pair_second_hidden_classification_qres. qr_x_ged_pair_second_hidden_classification_qres * qr_x_ged_pair_second_hidden_classification_qres + q * qr_u_ged_pair_second_hidden_classification_qres = p + q * qr_v_ged_pair_second_hidden_classification_qres)))))) /\ (exists fspm_u_ged_pair_second_hidden_mod fspm_v_ged_pair_second_hidden_mod. (e) + 2 * fspm_u_ged_pair_second_hidden_mod = (Q) + 2 * fspm_v_ged_pair_second_hidden_mod)))))
  46. 0046specialize odd_prime_gauss_eisenstein_orientation_data_exists q
  47. 0047specialize odd_prime_gauss_eisenstein_orientation_data_exists k
  48. 0048specialize odd_prime_gauss_eisenstein_orientation_data_exists p
  49. 0049apply odd_prime_gauss_eisenstein_orientation_data_exists
  50. 0050exact hqodd
  51. 0051exact hp_odd
  52. 0052exact hq
  53. 0053exact hmutual_right
  54. 0054cases hsecond
  55. 0055cases hsecond_witness
  56. 0056cases hsecond_witness_witness
  57. 0057cases hsecond_witness_witness_witness
  58. 0058cases hsecond_witness_witness_witness_witness
  59. 0059cases hsecond_witness_witness_witness_witness_witness
  60. 0060cases hsecond_witness_witness_witness_witness_witness_witness
  61. 0061cases hsecond_witness_witness_witness_witness_witness_witness_witness
  62. 0062cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness
  63. 0063cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right
  64. 0064cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right
  65. 0065cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right
  66. 0066have hqp : ~(q = p)
  67. 0067intro hqp_eq
  68. 0068apply hpq
  69. 0069symm
  70. 0070exact hqp_eq
  71. 0071have hfirst_rectangle : ∃ cb. ∃ cc. ∃ total. (∀ x. Lt(x,h) → ∃ y. BetaAt(cb,cc,x,y) ∧ (∃ z. ∃ n. (∀ m. Lt(m,k) → ∃ i. BetaAt(z,n,m,i) ∧ (i = 0 ∧ (Lt(q · S x,p · S m) ∧ ¬Lt(p · S m,q · S x)) ∨ i = 1 ∧ (Lt(p · S m,q · S x) ∧ ¬Lt(q · S x,p · S m)))) ∧ BitCount(z,n,k,y))) ∧ Sum(cb,cc,h,total)
    Exact native replay linehave hfirst_rectangle : exists cb cc total. ((forall erc_row_ged_pair_first_rectangle. (exists erc_lt_gap_ged_pair_first_rectangle_bound. erc_lt_gap_ged_pair_first_rectangle_bound + S (erc_row_ged_pair_first_rectangle) = h) -> exists erc_count_ged_pair_first_rectangle. ((((exists ff_h_erc_ged_pair_first_rectangle_decoded. ff_h_erc_ged_pair_first_rectangle_decoded + S (erc_count_ged_pair_first_rectangle) = S ((S (erc_row_ged_pair_first_rectangle)) * cc)) /\ exists ff_q_erc_ged_pair_first_rectangle_decoded. cb = ff_q_erc_ged_pair_first_rectangle_decoded * S ((S (erc_row_ged_pair_first_rectangle)) * cc) + (erc_count_ged_pair_first_rectangle))) /\ (exists erc_row_code_ged_pair_first_rectangle_witness erc_row_scale_ged_pair_first_rectangle_witness. ((forall eri_column_erc_ged_pair_first_rectangle_witness_row. (exists eri_gap_erc_ged_pair_first_rectangle_witness_row_bound. eri_gap_erc_ged_pair_first_rectangle_witness_row_bound + S (eri_column_erc_ged_pair_first_rectangle_witness_row) = k) -> exists eri_bit_erc_ged_pair_first_rectangle_witness_row. ((((exists ff_h_eri_erc_ged_pair_first_rectangle_witness_row_decoded. ff_h_eri_erc_ged_pair_first_rectangle_witness_row_decoded + S (eri_bit_erc_ged_pair_first_rectangle_witness_row) = S ((S (eri_column_erc_ged_pair_first_rectangle_witness_row)) * erc_row_scale_ged_pair_first_rectangle_witness)) /\ exists ff_q_eri_erc_ged_pair_first_rectangle_witness_row_decoded. erc_row_code_ged_pair_first_rectangle_witness = ff_q_eri_erc_ged_pair_first_rectangle_witness_row_decoded * S ((S (eri_column_erc_ged_pair_first_rectangle_witness_row)) * erc_row_scale_ged_pair_first_rectangle_witness) + (eri_bit_erc_ged_pair_first_rectangle_witness_row))) /\ (((eri_bit_erc_ged_pair_first_rectangle_witness_row = 0 /\ ((exists eri_gap_erc_ged_pair_first_rectangle_witness_row_choice_left. eri_gap_erc_ged_pair_first_rectangle_witness_row_choice_left + S (q * S erc_row_ged_pair_first_rectangle) = p * S eri_column_erc_ged_pair_first_rectangle_witness_row) /\ ~(exists eri_gap_erc_ged_pair_first_rectangle_witness_row_choice_right. eri_gap_erc_ged_pair_first_rectangle_witness_row_choice_right + S (p * S eri_column_erc_ged_pair_first_rectangle_witness_row) = q * S erc_row_ged_pair_first_rectangle))) \/ (eri_bit_erc_ged_pair_first_rectangle_witness_row = 1 /\ ((exists eri_gap_erc_ged_pair_first_rectangle_witness_row_choice_right. eri_gap_erc_ged_pair_first_rectangle_witness_row_choice_right + S (p * S eri_column_erc_ged_pair_first_rectangle_witness_row) = q * S erc_row_ged_pair_first_rectangle) /\ ~(exists eri_gap_erc_ged_pair_first_rectangle_witness_row_choice_left. eri_gap_erc_ged_pair_first_rectangle_witness_row_choice_left + S (q * S erc_row_ged_pair_first_rectangle) = p * S eri_column_erc_ged_pair_first_rectangle_witness_row))))))) /\ (((exists ff_u_erc_ged_pair_first_rectangle_witness_count_sum ff_v_erc_ged_pair_first_rectangle_witness_count_sum. ((((exists ff_h_erc_ged_pair_first_rectangle_witness_count_sum_start. ff_h_erc_ged_pair_first_rectangle_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_ged_pair_first_rectangle_witness_count_sum)) /\ exists ff_q_erc_ged_pair_first_rectangle_witness_count_sum_start. ff_u_erc_ged_pair_first_rectangle_witness_count_sum = ff_q_erc_ged_pair_first_rectangle_witness_count_sum_start * S ((S (0)) * ff_v_erc_ged_pair_first_rectangle_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_ged_pair_first_rectangle_witness_count_sum_terminal. ff_h_erc_ged_pair_first_rectangle_witness_count_sum_terminal + S (erc_count_ged_pair_first_rectangle) = S ((S (k)) * ff_v_erc_ged_pair_first_rectangle_witness_count_sum)) /\ exists ff_q_erc_ged_pair_first_rectangle_witness_count_sum_terminal. ff_u_erc_ged_pair_first_rectangle_witness_count_sum = ff_q_erc_ged_pair_first_rectangle_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_ged_pair_first_rectangle_witness_count_sum) + (erc_count_ged_pair_first_rectangle))) /\ forall ff_i_erc_ged_pair_first_rectangle_witness_count_sum. (exists ff_lt_erc_ged_pair_first_rectangle_witness_count_sum_bound. ff_lt_erc_ged_pair_first_rectangle_witness_count_sum_bound + S ff_i_erc_ged_pair_first_rectangle_witness_count_sum = k) -> exists ff_a_erc_ged_pair_first_rectangle_witness_count_sum ff_r_erc_ged_pair_first_rectangle_witness_count_sum ff_s_erc_ged_pair_first_rectangle_witness_count_sum. ((((exists ff_h_erc_ged_pair_first_rectangle_witness_count_sum_summand. ff_h_erc_ged_pair_first_rectangle_witness_count_sum_summand + S (ff_a_erc_ged_pair_first_rectangle_witness_count_sum) = S ((S (ff_i_erc_ged_pair_first_rectangle_witness_count_sum)) * erc_row_scale_ged_pair_first_rectangle_witness)) /\ exists ff_q_erc_ged_pair_first_rectangle_witness_count_sum_summand. erc_row_code_ged_pair_first_rectangle_witness = ff_q_erc_ged_pair_first_rectangle_witness_count_sum_summand * S ((S (ff_i_erc_ged_pair_first_rectangle_witness_count_sum)) * erc_row_scale_ged_pair_first_rectangle_witness) + (ff_a_erc_ged_pair_first_rectangle_witness_count_sum))) /\ ((((exists ff_h_erc_ged_pair_first_rectangle_witness_count_sum_partial. ff_h_erc_ged_pair_first_rectangle_witness_count_sum_partial + S (ff_r_erc_ged_pair_first_rectangle_witness_count_sum) = S ((S (ff_i_erc_ged_pair_first_rectangle_witness_count_sum)) * ff_v_erc_ged_pair_first_rectangle_witness_count_sum)) /\ exists ff_q_erc_ged_pair_first_rectangle_witness_count_sum_partial. ff_u_erc_ged_pair_first_rectangle_witness_count_sum = ff_q_erc_ged_pair_first_rectangle_witness_count_sum_partial * S ((S (ff_i_erc_ged_pair_first_rectangle_witness_count_sum)) * ff_v_erc_ged_pair_first_rectangle_witness_count_sum) + (ff_r_erc_ged_pair_first_rectangle_witness_count_sum))) /\ ((((exists ff_h_erc_ged_pair_first_rectangle_witness_count_sum_successor. ff_h_erc_ged_pair_first_rectangle_witness_count_sum_successor + S (ff_s_erc_ged_pair_first_rectangle_witness_count_sum) = S ((S (S ff_i_erc_ged_pair_first_rectangle_witness_count_sum)) * ff_v_erc_ged_pair_first_rectangle_witness_count_sum)) /\ exists ff_q_erc_ged_pair_first_rectangle_witness_count_sum_successor. ff_u_erc_ged_pair_first_rectangle_witness_count_sum = ff_q_erc_ged_pair_first_rectangle_witness_count_sum_successor * S ((S (S ff_i_erc_ged_pair_first_rectangle_witness_count_sum)) * ff_v_erc_ged_pair_first_rectangle_witness_count_sum) + (ff_s_erc_ged_pair_first_rectangle_witness_count_sum))) /\ ff_s_erc_ged_pair_first_rectangle_witness_count_sum = ff_r_erc_ged_pair_first_rectangle_witness_count_sum + ff_a_erc_ged_pair_first_rectangle_witness_count_sum)))))) /\ (forall ff_i_erc_ged_pair_first_rectangle_witness_count_bits. (exists ff_lt_erc_ged_pair_first_rectangle_witness_count_bits_bound. ff_lt_erc_ged_pair_first_rectangle_witness_count_bits_bound + S ff_i_erc_ged_pair_first_rectangle_witness_count_bits = k) -> exists ff_bit_erc_ged_pair_first_rectangle_witness_count_bits. ((((exists ff_h_erc_ged_pair_first_rectangle_witness_count_bits_decoded. ff_h_erc_ged_pair_first_rectangle_witness_count_bits_decoded + S (ff_bit_erc_ged_pair_first_rectangle_witness_count_bits) = S ((S (ff_i_erc_ged_pair_first_rectangle_witness_count_bits)) * erc_row_scale_ged_pair_first_rectangle_witness)) /\ exists ff_q_erc_ged_pair_first_rectangle_witness_count_bits_decoded. erc_row_code_ged_pair_first_rectangle_witness = ff_q_erc_ged_pair_first_rectangle_witness_count_bits_decoded * S ((S (ff_i_erc_ged_pair_first_rectangle_witness_count_bits)) * erc_row_scale_ged_pair_first_rectangle_witness) + (ff_bit_erc_ged_pair_first_rectangle_witness_count_bits))) /\ (ff_bit_erc_ged_pair_first_rectangle_witness_count_bits = 0 \/ ff_bit_erc_ged_pair_first_rectangle_witness_count_bits = 1))))))))) /\ (exists ff_u_ged_pair_first_rectangle_sum ff_v_ged_pair_first_rectangle_sum. ((((exists ff_h_ged_pair_first_rectangle_sum_start. ff_h_ged_pair_first_rectangle_sum_start + S (0) = S ((S (0)) * ff_v_ged_pair_first_rectangle_sum)) /\ exists ff_q_ged_pair_first_rectangle_sum_start. ff_u_ged_pair_first_rectangle_sum = ff_q_ged_pair_first_rectangle_sum_start * S ((S (0)) * ff_v_ged_pair_first_rectangle_sum) + (0))) /\ ((((exists ff_h_ged_pair_first_rectangle_sum_terminal. ff_h_ged_pair_first_rectangle_sum_terminal + S (total) = S ((S (h)) * ff_v_ged_pair_first_rectangle_sum)) /\ exists ff_q_ged_pair_first_rectangle_sum_terminal. ff_u_ged_pair_first_rectangle_sum = ff_q_ged_pair_first_rectangle_sum_terminal * S ((S (h)) * ff_v_ged_pair_first_rectangle_sum) + (total))) /\ forall ff_i_ged_pair_first_rectangle_sum. (exists ff_lt_ged_pair_first_rectangle_sum_bound. ff_lt_ged_pair_first_rectangle_sum_bound + S ff_i_ged_pair_first_rectangle_sum = h) -> exists ff_a_ged_pair_first_rectangle_sum ff_r_ged_pair_first_rectangle_sum ff_s_ged_pair_first_rectangle_sum. ((((exists ff_h_ged_pair_first_rectangle_sum_summand. ff_h_ged_pair_first_rectangle_sum_summand + S (ff_a_ged_pair_first_rectangle_sum) = S ((S (ff_i_ged_pair_first_rectangle_sum)) * cc)) /\ exists ff_q_ged_pair_first_rectangle_sum_summand. cb = ff_q_ged_pair_first_rectangle_sum_summand * S ((S (ff_i_ged_pair_first_rectangle_sum)) * cc) + (ff_a_ged_pair_first_rectangle_sum))) /\ ((((exists ff_h_ged_pair_first_rectangle_sum_partial. ff_h_ged_pair_first_rectangle_sum_partial + S (ff_r_ged_pair_first_rectangle_sum) = S ((S (ff_i_ged_pair_first_rectangle_sum)) * ff_v_ged_pair_first_rectangle_sum)) /\ exists ff_q_ged_pair_first_rectangle_sum_partial. ff_u_ged_pair_first_rectangle_sum = ff_q_ged_pair_first_rectangle_sum_partial * S ((S (ff_i_ged_pair_first_rectangle_sum)) * ff_v_ged_pair_first_rectangle_sum) + (ff_r_ged_pair_first_rectangle_sum))) /\ ((((exists ff_h_ged_pair_first_rectangle_sum_successor. ff_h_ged_pair_first_rectangle_sum_successor + S (ff_s_ged_pair_first_rectangle_sum) = S ((S (S ff_i_ged_pair_first_rectangle_sum)) * ff_v_ged_pair_first_rectangle_sum)) /\ exists ff_q_ged_pair_first_rectangle_sum_successor. ff_u_ged_pair_first_rectangle_sum = ff_q_ged_pair_first_rectangle_sum_successor * S ((S (S ff_i_ged_pair_first_rectangle_sum)) * ff_v_ged_pair_first_rectangle_sum) + (ff_s_ged_pair_first_rectangle_sum))) /\ ff_s_ged_pair_first_rectangle_sum = ff_r_ged_pair_first_rectangle_sum + ff_a_ged_pair_first_rectangle_sum)))))))
  72. 0072specialize distinct_odd_prime_half_rectangle_total_exists p
  73. 0073specialize distinct_odd_prime_half_rectangle_total_exists q
  74. 0074specialize distinct_odd_prime_half_rectangle_total_exists h
  75. 0075specialize distinct_odd_prime_half_rectangle_total_exists k
  76. 0076apply distinct_odd_prime_half_rectangle_total_exists
  77. 0077exact hpodd
  78. 0078exact hqodd
  79. 0079exact hp
  80. 0080exact hq
  81. 0081exact hpq
  82. 0082cases hfirst_rectangle
  83. 0083cases hfirst_rectangle_witness
  84. 0084cases hfirst_rectangle_witness_witness
  85. 0085cases hfirst_rectangle_witness_witness_witness
  86. 0086have hsecond_rectangle : ∃ cb. ∃ cc. ∃ total. (∀ x. Lt(x,k) → ∃ y. BetaAt(cb,cc,x,y) ∧ (∃ z. ∃ n. (∀ m. Lt(m,h) → ∃ i. BetaAt(z,n,m,i) ∧ (i = 0 ∧ (Lt(p · S x,q · S m) ∧ ¬Lt(q · S m,p · S x)) ∨ i = 1 ∧ (Lt(q · S m,p · S x) ∧ ¬Lt(p · S x,q · S m)))) ∧ BitCount(z,n,h,y))) ∧ Sum(cb,cc,k,total)
    Exact native replay linehave hsecond_rectangle : exists cb cc total. ((forall erc_row_ged_pair_second_rectangle. (exists erc_lt_gap_ged_pair_second_rectangle_bound. erc_lt_gap_ged_pair_second_rectangle_bound + S (erc_row_ged_pair_second_rectangle) = k) -> exists erc_count_ged_pair_second_rectangle. ((((exists ff_h_erc_ged_pair_second_rectangle_decoded. ff_h_erc_ged_pair_second_rectangle_decoded + S (erc_count_ged_pair_second_rectangle) = S ((S (erc_row_ged_pair_second_rectangle)) * cc)) /\ exists ff_q_erc_ged_pair_second_rectangle_decoded. cb = ff_q_erc_ged_pair_second_rectangle_decoded * S ((S (erc_row_ged_pair_second_rectangle)) * cc) + (erc_count_ged_pair_second_rectangle))) /\ (exists erc_row_code_ged_pair_second_rectangle_witness erc_row_scale_ged_pair_second_rectangle_witness. ((forall eri_column_erc_ged_pair_second_rectangle_witness_row. (exists eri_gap_erc_ged_pair_second_rectangle_witness_row_bound. eri_gap_erc_ged_pair_second_rectangle_witness_row_bound + S (eri_column_erc_ged_pair_second_rectangle_witness_row) = h) -> exists eri_bit_erc_ged_pair_second_rectangle_witness_row. ((((exists ff_h_eri_erc_ged_pair_second_rectangle_witness_row_decoded. ff_h_eri_erc_ged_pair_second_rectangle_witness_row_decoded + S (eri_bit_erc_ged_pair_second_rectangle_witness_row) = S ((S (eri_column_erc_ged_pair_second_rectangle_witness_row)) * erc_row_scale_ged_pair_second_rectangle_witness)) /\ exists ff_q_eri_erc_ged_pair_second_rectangle_witness_row_decoded. erc_row_code_ged_pair_second_rectangle_witness = ff_q_eri_erc_ged_pair_second_rectangle_witness_row_decoded * S ((S (eri_column_erc_ged_pair_second_rectangle_witness_row)) * erc_row_scale_ged_pair_second_rectangle_witness) + (eri_bit_erc_ged_pair_second_rectangle_witness_row))) /\ (((eri_bit_erc_ged_pair_second_rectangle_witness_row = 0 /\ ((exists eri_gap_erc_ged_pair_second_rectangle_witness_row_choice_left. eri_gap_erc_ged_pair_second_rectangle_witness_row_choice_left + S (p * S erc_row_ged_pair_second_rectangle) = q * S eri_column_erc_ged_pair_second_rectangle_witness_row) /\ ~(exists eri_gap_erc_ged_pair_second_rectangle_witness_row_choice_right. eri_gap_erc_ged_pair_second_rectangle_witness_row_choice_right + S (q * S eri_column_erc_ged_pair_second_rectangle_witness_row) = p * S erc_row_ged_pair_second_rectangle))) \/ (eri_bit_erc_ged_pair_second_rectangle_witness_row = 1 /\ ((exists eri_gap_erc_ged_pair_second_rectangle_witness_row_choice_right. eri_gap_erc_ged_pair_second_rectangle_witness_row_choice_right + S (q * S eri_column_erc_ged_pair_second_rectangle_witness_row) = p * S erc_row_ged_pair_second_rectangle) /\ ~(exists eri_gap_erc_ged_pair_second_rectangle_witness_row_choice_left. eri_gap_erc_ged_pair_second_rectangle_witness_row_choice_left + S (p * S erc_row_ged_pair_second_rectangle) = q * S eri_column_erc_ged_pair_second_rectangle_witness_row))))))) /\ (((exists ff_u_erc_ged_pair_second_rectangle_witness_count_sum ff_v_erc_ged_pair_second_rectangle_witness_count_sum. ((((exists ff_h_erc_ged_pair_second_rectangle_witness_count_sum_start. ff_h_erc_ged_pair_second_rectangle_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_ged_pair_second_rectangle_witness_count_sum)) /\ exists ff_q_erc_ged_pair_second_rectangle_witness_count_sum_start. ff_u_erc_ged_pair_second_rectangle_witness_count_sum = ff_q_erc_ged_pair_second_rectangle_witness_count_sum_start * S ((S (0)) * ff_v_erc_ged_pair_second_rectangle_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_ged_pair_second_rectangle_witness_count_sum_terminal. ff_h_erc_ged_pair_second_rectangle_witness_count_sum_terminal + S (erc_count_ged_pair_second_rectangle) = S ((S (h)) * ff_v_erc_ged_pair_second_rectangle_witness_count_sum)) /\ exists ff_q_erc_ged_pair_second_rectangle_witness_count_sum_terminal. ff_u_erc_ged_pair_second_rectangle_witness_count_sum = ff_q_erc_ged_pair_second_rectangle_witness_count_sum_terminal * S ((S (h)) * ff_v_erc_ged_pair_second_rectangle_witness_count_sum) + (erc_count_ged_pair_second_rectangle))) /\ forall ff_i_erc_ged_pair_second_rectangle_witness_count_sum. (exists ff_lt_erc_ged_pair_second_rectangle_witness_count_sum_bound. ff_lt_erc_ged_pair_second_rectangle_witness_count_sum_bound + S ff_i_erc_ged_pair_second_rectangle_witness_count_sum = h) -> exists ff_a_erc_ged_pair_second_rectangle_witness_count_sum ff_r_erc_ged_pair_second_rectangle_witness_count_sum ff_s_erc_ged_pair_second_rectangle_witness_count_sum. ((((exists ff_h_erc_ged_pair_second_rectangle_witness_count_sum_summand. ff_h_erc_ged_pair_second_rectangle_witness_count_sum_summand + S (ff_a_erc_ged_pair_second_rectangle_witness_count_sum) = S ((S (ff_i_erc_ged_pair_second_rectangle_witness_count_sum)) * erc_row_scale_ged_pair_second_rectangle_witness)) /\ exists ff_q_erc_ged_pair_second_rectangle_witness_count_sum_summand. erc_row_code_ged_pair_second_rectangle_witness = ff_q_erc_ged_pair_second_rectangle_witness_count_sum_summand * S ((S (ff_i_erc_ged_pair_second_rectangle_witness_count_sum)) * erc_row_scale_ged_pair_second_rectangle_witness) + (ff_a_erc_ged_pair_second_rectangle_witness_count_sum))) /\ ((((exists ff_h_erc_ged_pair_second_rectangle_witness_count_sum_partial. ff_h_erc_ged_pair_second_rectangle_witness_count_sum_partial + S (ff_r_erc_ged_pair_second_rectangle_witness_count_sum) = S ((S (ff_i_erc_ged_pair_second_rectangle_witness_count_sum)) * ff_v_erc_ged_pair_second_rectangle_witness_count_sum)) /\ exists ff_q_erc_ged_pair_second_rectangle_witness_count_sum_partial. ff_u_erc_ged_pair_second_rectangle_witness_count_sum = ff_q_erc_ged_pair_second_rectangle_witness_count_sum_partial * S ((S (ff_i_erc_ged_pair_second_rectangle_witness_count_sum)) * ff_v_erc_ged_pair_second_rectangle_witness_count_sum) + (ff_r_erc_ged_pair_second_rectangle_witness_count_sum))) /\ ((((exists ff_h_erc_ged_pair_second_rectangle_witness_count_sum_successor. ff_h_erc_ged_pair_second_rectangle_witness_count_sum_successor + S (ff_s_erc_ged_pair_second_rectangle_witness_count_sum) = S ((S (S ff_i_erc_ged_pair_second_rectangle_witness_count_sum)) * ff_v_erc_ged_pair_second_rectangle_witness_count_sum)) /\ exists ff_q_erc_ged_pair_second_rectangle_witness_count_sum_successor. ff_u_erc_ged_pair_second_rectangle_witness_count_sum = ff_q_erc_ged_pair_second_rectangle_witness_count_sum_successor * S ((S (S ff_i_erc_ged_pair_second_rectangle_witness_count_sum)) * ff_v_erc_ged_pair_second_rectangle_witness_count_sum) + (ff_s_erc_ged_pair_second_rectangle_witness_count_sum))) /\ ff_s_erc_ged_pair_second_rectangle_witness_count_sum = ff_r_erc_ged_pair_second_rectangle_witness_count_sum + ff_a_erc_ged_pair_second_rectangle_witness_count_sum)))))) /\ (forall ff_i_erc_ged_pair_second_rectangle_witness_count_bits. (exists ff_lt_erc_ged_pair_second_rectangle_witness_count_bits_bound. ff_lt_erc_ged_pair_second_rectangle_witness_count_bits_bound + S ff_i_erc_ged_pair_second_rectangle_witness_count_bits = h) -> exists ff_bit_erc_ged_pair_second_rectangle_witness_count_bits. ((((exists ff_h_erc_ged_pair_second_rectangle_witness_count_bits_decoded. ff_h_erc_ged_pair_second_rectangle_witness_count_bits_decoded + S (ff_bit_erc_ged_pair_second_rectangle_witness_count_bits) = S ((S (ff_i_erc_ged_pair_second_rectangle_witness_count_bits)) * erc_row_scale_ged_pair_second_rectangle_witness)) /\ exists ff_q_erc_ged_pair_second_rectangle_witness_count_bits_decoded. erc_row_code_ged_pair_second_rectangle_witness = ff_q_erc_ged_pair_second_rectangle_witness_count_bits_decoded * S ((S (ff_i_erc_ged_pair_second_rectangle_witness_count_bits)) * erc_row_scale_ged_pair_second_rectangle_witness) + (ff_bit_erc_ged_pair_second_rectangle_witness_count_bits))) /\ (ff_bit_erc_ged_pair_second_rectangle_witness_count_bits = 0 \/ ff_bit_erc_ged_pair_second_rectangle_witness_count_bits = 1))))))))) /\ (exists ff_u_ged_pair_second_rectangle_sum ff_v_ged_pair_second_rectangle_sum. ((((exists ff_h_ged_pair_second_rectangle_sum_start. ff_h_ged_pair_second_rectangle_sum_start + S (0) = S ((S (0)) * ff_v_ged_pair_second_rectangle_sum)) /\ exists ff_q_ged_pair_second_rectangle_sum_start. ff_u_ged_pair_second_rectangle_sum = ff_q_ged_pair_second_rectangle_sum_start * S ((S (0)) * ff_v_ged_pair_second_rectangle_sum) + (0))) /\ ((((exists ff_h_ged_pair_second_rectangle_sum_terminal. ff_h_ged_pair_second_rectangle_sum_terminal + S (total) = S ((S (k)) * ff_v_ged_pair_second_rectangle_sum)) /\ exists ff_q_ged_pair_second_rectangle_sum_terminal. ff_u_ged_pair_second_rectangle_sum = ff_q_ged_pair_second_rectangle_sum_terminal * S ((S (k)) * ff_v_ged_pair_second_rectangle_sum) + (total))) /\ forall ff_i_ged_pair_second_rectangle_sum. (exists ff_lt_ged_pair_second_rectangle_sum_bound. ff_lt_ged_pair_second_rectangle_sum_bound + S ff_i_ged_pair_second_rectangle_sum = k) -> exists ff_a_ged_pair_second_rectangle_sum ff_r_ged_pair_second_rectangle_sum ff_s_ged_pair_second_rectangle_sum. ((((exists ff_h_ged_pair_second_rectangle_sum_summand. ff_h_ged_pair_second_rectangle_sum_summand + S (ff_a_ged_pair_second_rectangle_sum) = S ((S (ff_i_ged_pair_second_rectangle_sum)) * cc)) /\ exists ff_q_ged_pair_second_rectangle_sum_summand. cb = ff_q_ged_pair_second_rectangle_sum_summand * S ((S (ff_i_ged_pair_second_rectangle_sum)) * cc) + (ff_a_ged_pair_second_rectangle_sum))) /\ ((((exists ff_h_ged_pair_second_rectangle_sum_partial. ff_h_ged_pair_second_rectangle_sum_partial + S (ff_r_ged_pair_second_rectangle_sum) = S ((S (ff_i_ged_pair_second_rectangle_sum)) * ff_v_ged_pair_second_rectangle_sum)) /\ exists ff_q_ged_pair_second_rectangle_sum_partial. ff_u_ged_pair_second_rectangle_sum = ff_q_ged_pair_second_rectangle_sum_partial * S ((S (ff_i_ged_pair_second_rectangle_sum)) * ff_v_ged_pair_second_rectangle_sum) + (ff_r_ged_pair_second_rectangle_sum))) /\ ((((exists ff_h_ged_pair_second_rectangle_sum_successor. ff_h_ged_pair_second_rectangle_sum_successor + S (ff_s_ged_pair_second_rectangle_sum) = S ((S (S ff_i_ged_pair_second_rectangle_sum)) * ff_v_ged_pair_second_rectangle_sum)) /\ exists ff_q_ged_pair_second_rectangle_sum_successor. ff_u_ged_pair_second_rectangle_sum = ff_q_ged_pair_second_rectangle_sum_successor * S ((S (S ff_i_ged_pair_second_rectangle_sum)) * ff_v_ged_pair_second_rectangle_sum) + (ff_s_ged_pair_second_rectangle_sum))) /\ ff_s_ged_pair_second_rectangle_sum = ff_r_ged_pair_second_rectangle_sum + ff_a_ged_pair_second_rectangle_sum)))))))
  87. 0087specialize distinct_odd_prime_half_rectangle_total_exists q
  88. 0088specialize distinct_odd_prime_half_rectangle_total_exists p
  89. 0089specialize distinct_odd_prime_half_rectangle_total_exists k
  90. 0090specialize distinct_odd_prime_half_rectangle_total_exists h
  91. 0091apply distinct_odd_prime_half_rectangle_total_exists
  92. 0092exact hqodd
  93. 0093exact hpodd
  94. 0094exact hq
  95. 0095exact hp
  96. 0096exact hqp
  97. 0097cases hsecond_rectangle
  98. 0098cases hsecond_rectangle_witness
  99. 0099cases hsecond_rectangle_witness_witness
  100. 0100cases hsecond_rectangle_witness_witness_witness
  101. 0101have hsum_identity : x7 + x15 = h * k
  102. 0102specialize distinct_odd_prime_eisenstein_quotient_sum_identity p
  103. 0103specialize distinct_odd_prime_eisenstein_quotient_sum_identity q
  104. 0104specialize distinct_odd_prime_eisenstein_quotient_sum_identity h
  105. 0105specialize distinct_odd_prime_eisenstein_quotient_sum_identity k
  106. 0106specialize distinct_odd_prime_eisenstein_quotient_sum_identity x
  107. 0107specialize distinct_odd_prime_eisenstein_quotient_sum_identity x1
  108. 0108specialize distinct_odd_prime_eisenstein_quotient_sum_identity x2
  109. 0109specialize distinct_odd_prime_eisenstein_quotient_sum_identity x3
  110. 0110specialize distinct_odd_prime_eisenstein_quotient_sum_identity x4
  111. 0111specialize distinct_odd_prime_eisenstein_quotient_sum_identity x5
  112. 0112specialize distinct_odd_prime_eisenstein_quotient_sum_identity x8
  113. 0113specialize distinct_odd_prime_eisenstein_quotient_sum_identity x9
  114. 0114specialize distinct_odd_prime_eisenstein_quotient_sum_identity x10
  115. 0115specialize distinct_odd_prime_eisenstein_quotient_sum_identity x11
  116. 0116specialize distinct_odd_prime_eisenstein_quotient_sum_identity x12
  117. 0117specialize distinct_odd_prime_eisenstein_quotient_sum_identity x13
  118. 0118specialize distinct_odd_prime_eisenstein_quotient_sum_identity x16
  119. 0119specialize distinct_odd_prime_eisenstein_quotient_sum_identity x17
  120. 0120specialize distinct_odd_prime_eisenstein_quotient_sum_identity x19
  121. 0121specialize distinct_odd_prime_eisenstein_quotient_sum_identity x20
  122. 0122specialize distinct_odd_prime_eisenstein_quotient_sum_identity x7
  123. 0123specialize distinct_odd_prime_eisenstein_quotient_sum_identity x15
  124. 0124apply distinct_odd_prime_eisenstein_quotient_sum_identity
  125. 0125exact hpodd
  126. 0126exact hqodd
  127. 0127exact hp
  128. 0128exact hq
  129. 0129exact hpq
  130. 0130exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_left
  131. 0131exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_left
  132. 0132exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_left
  133. 0133exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_left
  134. 0134exact hfirst_rectangle_witness_witness_witness_left
  135. 0135exact hsecond_rectangle_witness_witness_witness_left
  136. 0136exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left
  137. 0137exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left
  138. 0138exists x6
  139. 0139exists x14
  140. 0140exists x7
  141. 0141exists x15
  142. 0142split
  143. 0143split
  144. 0144exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left
  145. 0145exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left
  146. 0146split
  147. 0147split
  148. 0148exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
  149. 0149exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
  150. 0150exact hsum_identity