EL001C

lte_coprime_power_difference_quotient

For every exponent not divisible by the actual prime, construct real power differences with a nondivisible geometric quotient; exponent one is handled explicitly.

Alpha v34 checked-use · first admitted v29 · independently kernel and Lean verified; not Stable

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.

All displayed hypotheses are required. Powers and positive differences are actual existential outputs. The proof constructs second-order correction identities and iterates the prime step; no binomial expansion or LTE oracle is assumed. The 2-adic variants remain separate open targets.

Exact theorem in conservative defined notation

∀ p. ∀ a. ∀ b. ∀ d. ∀ n. ¬p = 1 ∧ (∀ x. ∀ y. p = x · y → x = 1 ∨ y = 1) → a = b + d → Dvd(p,d) → ¬Dvd(p,b) → ¬Dvd(p,n) → ∃ x. ∃ y. ∃ z. Pow(a,n,x) ∧ (Pow(b,n,y) ∧ (x = y + d · z ∧ ¬Dvd(p,z)))

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

PowerDifferenceSecondOrder(a,b,d,k,A,B,R,T,Q,C,H) · 1Dvd(d,n) · 4Pow(a,e,z) · 2

Actual proof prerequisites

eq_decidable · checked external prerequisitelte_power_exponent_eq_transportlte_power_one_exactmul_one · checked external prerequisitelte_prime_nondivisor_onelte_nondivisor_nonzerononzero_is_succ · checked external prerequisitelte_power_difference_second_order_existslte_nondivisor_add_multipleprime_nondivisor_mul · checked external prerequisitelte_nondivisor_power
Original expanded first-order statement 
forall p a b d n. (~((p) = 1) /\ forall pvs_left_unit_step_prime pvs_right_unit_step_prime. (p) = pvs_left_unit_step_prime * pvs_right_unit_step_prime -> pvs_left_unit_step_prime = 1 \/ pvs_right_unit_step_prime = 1) -> a = b + d -> (exists olte_factor_unit_step_difference. (d) = (p) * olte_factor_unit_step_difference) -> ~(exists olte_factor_unit_step_base. (b) = (p) * olte_factor_unit_step_base) -> ~(exists olte_factor_unit_step_exponent. (n) = (p) * olte_factor_unit_step_exponent) -> exists A B Q. (((exists pa_b_olte_unit_step_A pa_c_olte_unit_step_A. ((forall pa_i_olte_unit_step_A_repeat. (exists pa_lt_olte_unit_step_A_repeat_bound. pa_lt_olte_unit_step_A_repeat_bound + S pa_i_olte_unit_step_A_repeat = n) -> (((exists pa_h_olte_unit_step_A_repeat_decoded. pa_h_olte_unit_step_A_repeat_decoded + S (a) = S ((S (pa_i_olte_unit_step_A_repeat)) * pa_c_olte_unit_step_A)) /\ exists pa_q_olte_unit_step_A_repeat_decoded. pa_b_olte_unit_step_A = pa_q_olte_unit_step_A_repeat_decoded * S ((S (pa_i_olte_unit_step_A_repeat)) * pa_c_olte_unit_step_A) + (a)))) /\ (exists pa_u_olte_unit_step_A_product pa_v_olte_unit_step_A_product. ((((exists pa_h_olte_unit_step_A_product_start. pa_h_olte_unit_step_A_product_start + S (1) = S ((S (0)) * pa_v_olte_unit_step_A_product)) /\ exists pa_q_olte_unit_step_A_product_start. pa_u_olte_unit_step_A_product = pa_q_olte_unit_step_A_product_start * S ((S (0)) * pa_v_olte_unit_step_A_product) + (1))) /\ ((((exists pa_h_olte_unit_step_A_product_terminal. pa_h_olte_unit_step_A_product_terminal + S (A) = S ((S (n)) * pa_v_olte_unit_step_A_product)) /\ exists pa_q_olte_unit_step_A_product_terminal. pa_u_olte_unit_step_A_product = pa_q_olte_unit_step_A_product_terminal * S ((S (n)) * pa_v_olte_unit_step_A_product) + (A))) /\ forall pa_i_olte_unit_step_A_product. (exists pa_lt_olte_unit_step_A_product_bound. pa_lt_olte_unit_step_A_product_bound + S pa_i_olte_unit_step_A_product = n) -> exists pa_p_olte_unit_step_A_product pa_r_olte_unit_step_A_product pa_s_olte_unit_step_A_product. ((((exists pa_h_olte_unit_step_A_product_factor. pa_h_olte_unit_step_A_product_factor + S (pa_p_olte_unit_step_A_product) = S ((S (pa_i_olte_unit_step_A_product)) * pa_c_olte_unit_step_A)) /\ exists pa_q_olte_unit_step_A_product_factor. pa_b_olte_unit_step_A = pa_q_olte_unit_step_A_product_factor * S ((S (pa_i_olte_unit_step_A_product)) * pa_c_olte_unit_step_A) + (pa_p_olte_unit_step_A_product))) /\ ((((exists pa_h_olte_unit_step_A_product_partial. pa_h_olte_unit_step_A_product_partial + S (pa_r_olte_unit_step_A_product) = S ((S (pa_i_olte_unit_step_A_product)) * pa_v_olte_unit_step_A_product)) /\ exists pa_q_olte_unit_step_A_product_partial. pa_u_olte_unit_step_A_product = pa_q_olte_unit_step_A_product_partial * S ((S (pa_i_olte_unit_step_A_product)) * pa_v_olte_unit_step_A_product) + (pa_r_olte_unit_step_A_product))) /\ ((((exists pa_h_olte_unit_step_A_product_successor. pa_h_olte_unit_step_A_product_successor + S (pa_s_olte_unit_step_A_product) = S ((S (S pa_i_olte_unit_step_A_product)) * pa_v_olte_unit_step_A_product)) /\ exists pa_q_olte_unit_step_A_product_successor. pa_u_olte_unit_step_A_product = pa_q_olte_unit_step_A_product_successor * S ((S (S pa_i_olte_unit_step_A_product)) * pa_v_olte_unit_step_A_product) + (pa_s_olte_unit_step_A_product))) /\ pa_s_olte_unit_step_A_product = pa_r_olte_unit_step_A_product * pa_p_olte_unit_step_A_product)))))))) /\ (((exists pa_b_olte_unit_step_B pa_c_olte_unit_step_B. ((forall pa_i_olte_unit_step_B_repeat. (exists pa_lt_olte_unit_step_B_repeat_bound. pa_lt_olte_unit_step_B_repeat_bound + S pa_i_olte_unit_step_B_repeat = n) -> (((exists pa_h_olte_unit_step_B_repeat_decoded. pa_h_olte_unit_step_B_repeat_decoded + S (b) = S ((S (pa_i_olte_unit_step_B_repeat)) * pa_c_olte_unit_step_B)) /\ exists pa_q_olte_unit_step_B_repeat_decoded. pa_b_olte_unit_step_B = pa_q_olte_unit_step_B_repeat_decoded * S ((S (pa_i_olte_unit_step_B_repeat)) * pa_c_olte_unit_step_B) + (b)))) /\ (exists pa_u_olte_unit_step_B_product pa_v_olte_unit_step_B_product. ((((exists pa_h_olte_unit_step_B_product_start. pa_h_olte_unit_step_B_product_start + S (1) = S ((S (0)) * pa_v_olte_unit_step_B_product)) /\ exists pa_q_olte_unit_step_B_product_start. pa_u_olte_unit_step_B_product = pa_q_olte_unit_step_B_product_start * S ((S (0)) * pa_v_olte_unit_step_B_product) + (1))) /\ ((((exists pa_h_olte_unit_step_B_product_terminal. pa_h_olte_unit_step_B_product_terminal + S (B) = S ((S (n)) * pa_v_olte_unit_step_B_product)) /\ exists pa_q_olte_unit_step_B_product_terminal. pa_u_olte_unit_step_B_product = pa_q_olte_unit_step_B_product_terminal * S ((S (n)) * pa_v_olte_unit_step_B_product) + (B))) /\ forall pa_i_olte_unit_step_B_product. (exists pa_lt_olte_unit_step_B_product_bound. pa_lt_olte_unit_step_B_product_bound + S pa_i_olte_unit_step_B_product = n) -> exists pa_p_olte_unit_step_B_product pa_r_olte_unit_step_B_product pa_s_olte_unit_step_B_product. ((((exists pa_h_olte_unit_step_B_product_factor. pa_h_olte_unit_step_B_product_factor + S (pa_p_olte_unit_step_B_product) = S ((S (pa_i_olte_unit_step_B_product)) * pa_c_olte_unit_step_B)) /\ exists pa_q_olte_unit_step_B_product_factor. pa_b_olte_unit_step_B = pa_q_olte_unit_step_B_product_factor * S ((S (pa_i_olte_unit_step_B_product)) * pa_c_olte_unit_step_B) + (pa_p_olte_unit_step_B_product))) /\ ((((exists pa_h_olte_unit_step_B_product_partial. pa_h_olte_unit_step_B_product_partial + S (pa_r_olte_unit_step_B_product) = S ((S (pa_i_olte_unit_step_B_product)) * pa_v_olte_unit_step_B_product)) /\ exists pa_q_olte_unit_step_B_product_partial. pa_u_olte_unit_step_B_product = pa_q_olte_unit_step_B_product_partial * S ((S (pa_i_olte_unit_step_B_product)) * pa_v_olte_unit_step_B_product) + (pa_r_olte_unit_step_B_product))) /\ ((((exists pa_h_olte_unit_step_B_product_successor. pa_h_olte_unit_step_B_product_successor + S (pa_s_olte_unit_step_B_product) = S ((S (S pa_i_olte_unit_step_B_product)) * pa_v_olte_unit_step_B_product)) /\ exists pa_q_olte_unit_step_B_product_successor. pa_u_olte_unit_step_B_product = pa_q_olte_unit_step_B_product_successor * S ((S (S pa_i_olte_unit_step_B_product)) * pa_v_olte_unit_step_B_product) + (pa_s_olte_unit_step_B_product))) /\ pa_s_olte_unit_step_B_product = pa_r_olte_unit_step_B_product * pa_p_olte_unit_step_B_product)))))))) /\ (((A = B + d * Q) /\ (~(exists olte_factor_unit_step_quotient. (Q) = (p) * olte_factor_unit_step_quotient))))))))

Complete tactic proof in conservative notation

All 150 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

150 script commands · 46 reading checkpoints · 7 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 (7)
lte power exponent eq transportlte power one exactlte prime nondivisor onelte nondivisor nonzerolte power difference second order existslte nondivisor add multiplelte nondivisor power
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro d
  5. L5
    intro n
  6. L6
    intro hp
  7. L7
    intro ha
  8. L8
    intro hd
  9. L9
    intro hb
  10. L10
    intro hn
02Use earlier factsL11–12

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

  1. L11
    specialize eq_decidable n
  2. L12
    specialize eq_decidable 1
03Separate the logical casesL13–13

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

  1. L13
    cases eq_decidable
04Construct an explicit witnessL14–16

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

  1. L14
    exists a
  2. L15
    exists b
  3. L16
    exists 1
05Separate the logical casesL17–17

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

  1. L17
    split
06Use earlier factsL18–22

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

  1. L18
    specialize lte_power_exponent_eq_transport (a)
  2. L19
    specialize lte_power_exponent_eq_transport (1)
  3. L20
    specialize lte_power_exponent_eq_transport (n)
  4. L21
    specialize lte_power_exponent_eq_transport (a)
  5. L22
    apply lte_power_exponent_eq_transport
07Calculate and transport equalitiesL23–23

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

  1. L23
    symm
08Use earlier factsL24–26

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

  1. L24
    exact eq_decidable_left
  2. L25
    specialize lte_power_one_exact (a)
  3. L26
    apply lte_power_one_exact
09Separate the logical casesL27–27

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

  1. L27
    split
10Use earlier factsL28–32

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

  1. L28
    specialize lte_power_exponent_eq_transport (b)
  2. L29
    specialize lte_power_exponent_eq_transport (1)
  3. L30
    specialize lte_power_exponent_eq_transport (n)
  4. L31
    specialize lte_power_exponent_eq_transport (b)
  5. L32
    apply lte_power_exponent_eq_transport
11Calculate and transport equalitiesL33–33

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

  1. L33
    symm
12Use earlier factsL34–36

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

  1. L34
    exact eq_decidable_left
  2. L35
    specialize lte_power_one_exact (b)
  3. L36
    apply lte_power_one_exact
13Separate the logical casesL37–37

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

  1. L37
    split
14Calculate and transport equalitiesL38–38

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

  1. L38
    trans b + d
15Use earlier factsL39–39

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

  1. L39
    exact ha
16Calculate and transport equalitiesL40–42

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

  1. L40
    congr
  2. L41
    refl
  3. L42
    symm
17Use earlier factsL43–43

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

  1. L43
    apply mul_one
18Fix variables and assumptionsL44–44

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

  1. L44
    intro hdiv1
19Use earlier factsL45–48

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

  1. L45
    specialize lte_prime_nondivisor_one (p)
  2. L46
    apply lte_prime_nondivisor_one
  3. L47
    exact hp
  4. L48
    exact hdiv1
20Establish hnzeroL49–55

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

  1. L49
    have hnzero : ~(n = 0)
  2. L50
    intro hz
  3. L51
    specialize lte_nondivisor_nonzero (p)
  4. L52
    specialize lte_nondivisor_nonzero (n)
  5. L53
    apply lte_nondivisor_nonzero
  6. L54
    exact hn
  7. L55
    exact hz
21Establish hfirstindexL56–59

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

  1. L56
    have hfirstindex : exists k. n = S k
  2. L57
    specialize nonzero_is_succ (n)
  3. L58
    apply nonzero_is_succ
  4. L59
    exact hnzero
22Separate the logical casesL60–60

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

  1. L60
    cases hfirstindex
23Establish hindexzeroL61–67

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

  1. L61
    have hindexzero : ~(x = 0)
  2. L62
    intro hxzero
  3. L63
    apply eq_decidable_right
  4. L64
    trans S x
  5. L65
    exact hfirstindex_witness
  6. L66
    rewrite hxzero
  7. L67
    refl
24Establish hsecondindexL68–71

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

  1. L68
    have hsecondindex : exists k. x = S k
  2. L69
    specialize nonzero_is_succ (x)
  3. L70
    apply nonzero_is_succ
  4. L71
    exact hindexzero
25Separate the logical casesL72–72

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

  1. L72
    cases hsecondindex
26Establish hnindexL73–77

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

  1. L73
    have hnindex : n = S (S x1)
  2. L74
    trans S x
  3. L75
    exact hfirstindex_witness
  4. L76
    rewrite hsecondindex_witness
  5. L77
    refl
27Establish hsecondL78–84

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lte power difference second order exists.

  1. L78
    have hsecond : ∃ A. ∃ B. ∃ R. ∃ T. ∃ Q. ∃ C. ∃ H. PowerDifferenceSecondOrder(a,b,d,x1,A,B,R,T,Q,C,H)Definitions: PowerDifferenceSecondOrder(a,b,d,x1,A,B,R,T,Q,C,H)Original native command in the exact edition
  2. L79
    specialize lte_power_difference_second_order_exists (a)
  3. L80
    specialize lte_power_difference_second_order_exists (b)
  4. L81
    specialize lte_power_difference_second_order_exists (d)
  5. L82
    specialize lte_power_difference_second_order_exists (x1)
  6. L83
    apply lte_power_difference_second_order_exists
  7. L84
    exact ha
28Separate the logical casesL85–94

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

  1. L85
    cases hsecond
  2. L86
    cases hsecond_witness
  3. L87
    cases hsecond_witness_witness
  4. L88
    cases hsecond_witness_witness_witness
  5. L89
    cases hsecond_witness_witness_witness_witness
  6. L90
    cases hsecond_witness_witness_witness_witness_witness
  7. L91
    cases hsecond_witness_witness_witness_witness_witness_witness
  8. L92
    cases hsecond_witness_witness_witness_witness_witness_witness_witness
  9. L93
    cases hsecond_witness_witness_witness_witness_witness_witness_witness_right
  10. L94
    cases hsecond_witness_witness_witness_witness_witness_witness_witness_right_right
29Separate the logical casesL95–97

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

  1. L95
    cases hsecond_witness_witness_witness_witness_witness_witness_witness_right_right_right
  2. L96
    cases hsecond_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
  3. L97
    cases hsecond_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right
30Construct an explicit witnessL98–100

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

  1. L98
    exists x2
  2. L99
    exists x3
  3. L100
    exists x6
31Separate the logical casesL101–101

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

  1. L101
    split
32Use earlier factsL102–106

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

  1. L102
    specialize lte_power_exponent_eq_transport (a)
  2. L103
    specialize lte_power_exponent_eq_transport (S (S x1))
  3. L104
    specialize lte_power_exponent_eq_transport (n)
  4. L105
    specialize lte_power_exponent_eq_transport (x2)
  5. L106
    apply lte_power_exponent_eq_transport
33Calculate and transport equalitiesL107–107

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

  1. L107
    symm
34Use earlier factsL108–109

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

  1. L108
    exact hnindex
  2. L109
    exact hsecond_witness_witness_witness_witness_witness_witness_witness_left
35Separate the logical casesL110–110

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

  1. L110
    split
36Use earlier factsL111–115

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

  1. L111
    specialize lte_power_exponent_eq_transport (b)
  2. L112
    specialize lte_power_exponent_eq_transport (S (S x1))
  3. L113
    specialize lte_power_exponent_eq_transport (n)
  4. L114
    specialize lte_power_exponent_eq_transport (x3)
  5. L115
    apply lte_power_exponent_eq_transport
37Calculate and transport equalitiesL116–116

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

  1. L116
    symm
38Use earlier factsL117–118

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

  1. L117
    exact hnindex
  2. L118
    exact hsecond_witness_witness_witness_witness_witness_witness_witness_right_left
39Separate the logical casesL119–119

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

  1. L119
    split
40Use earlier factsL120–120

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

  1. L120
    exact hsecond_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left
41Fix variables and assumptionsL121–121

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

  1. L121
    intro hQdiv
42Establish hfirstL122–131

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

  1. L122
    have hfirst : x6 = n * x4 + d * x7
  2. L123
    rewrite hnindex
  3. L124
    exact hsecond_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_left
  4. L125
    rewrite hfirst at hQdiv
  5. L126
    specialize lte_nondivisor_add_multiple (p)
  6. L127
    specialize lte_nondivisor_add_multiple (n * x4)
  7. L128
    specialize lte_nondivisor_add_multiple (d)
  8. L129
    specialize lte_nondivisor_add_multiple (x7)
  9. L130
    apply lte_nondivisor_add_multiple
  10. L131
    intro hproduct
43Use earlier factsL132–137

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

  1. L132
    specialize prime_nondivisor_mul (p)
  2. L133
    specialize prime_nondivisor_mul (n)
  3. L134
    specialize prime_nondivisor_mul (x4)
  4. L135
    apply prime_nondivisor_mul
  5. L136
    exact hp
  6. L137
    exact hn
44Fix variables and assumptionsL138–138

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

  1. L138
    intro hRdiv
45Use earlier factsL139–148

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

  1. L139
    specialize lte_nondivisor_power (p)
  2. L140
    specialize lte_nondivisor_power (b)
  3. L141
    specialize lte_nondivisor_power (S x1)
  4. L142
    specialize lte_nondivisor_power (x4)
  5. L143
    apply lte_nondivisor_power
  6. L144
    exact hp
  7. L145
    exact hb
  8. L146
    exact hsecond_witness_witness_witness_witness_witness_witness_witness_right_right_left
  9. L147
    exact hRdiv
  10. L148
    exact hproduct
46Use earlier factsL149–150

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

  1. L149
    exact hd
  2. L150
    exact hQdiv

Library-wide reading audit

Original defined command ledger · 150 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro b
  4. 0004intro d
  5. 0005intro n
  6. 0006intro hp
  7. 0007intro ha
  8. 0008intro hd
  9. 0009intro hb
  10. 0010intro hn
  11. 0011specialize eq_decidable n
  12. 0012specialize eq_decidable 1
  13. 0013cases eq_decidable
  14. 0014exists a
  15. 0015exists b
  16. 0016exists 1
  17. 0017split
  18. 0018specialize lte_power_exponent_eq_transport (a)
  19. 0019specialize lte_power_exponent_eq_transport (1)
  20. 0020specialize lte_power_exponent_eq_transport (n)
  21. 0021specialize lte_power_exponent_eq_transport (a)
  22. 0022apply lte_power_exponent_eq_transport
  23. 0023symm
  24. 0024exact eq_decidable_left
  25. 0025specialize lte_power_one_exact (a)
  26. 0026apply lte_power_one_exact
  27. 0027split
  28. 0028specialize lte_power_exponent_eq_transport (b)
  29. 0029specialize lte_power_exponent_eq_transport (1)
  30. 0030specialize lte_power_exponent_eq_transport (n)
  31. 0031specialize lte_power_exponent_eq_transport (b)
  32. 0032apply lte_power_exponent_eq_transport
  33. 0033symm
  34. 0034exact eq_decidable_left
  35. 0035specialize lte_power_one_exact (b)
  36. 0036apply lte_power_one_exact
  37. 0037split
  38. 0038trans b + d
  39. 0039exact ha
  40. 0040congr
  41. 0041refl
  42. 0042symm
  43. 0043apply mul_one
  44. 0044intro hdiv1
  45. 0045specialize lte_prime_nondivisor_one (p)
  46. 0046apply lte_prime_nondivisor_one
  47. 0047exact hp
  48. 0048exact hdiv1
  49. 0049have hnzero : ~(n = 0)
  50. 0050intro hz
  51. 0051specialize lte_nondivisor_nonzero (p)
  52. 0052specialize lte_nondivisor_nonzero (n)
  53. 0053apply lte_nondivisor_nonzero
  54. 0054exact hn
  55. 0055exact hz
  56. 0056have hfirstindex : exists k. n = S k
  57. 0057specialize nonzero_is_succ (n)
  58. 0058apply nonzero_is_succ
  59. 0059exact hnzero
  60. 0060cases hfirstindex
  61. 0061have hindexzero : ~(x = 0)
  62. 0062intro hxzero
  63. 0063apply eq_decidable_right
  64. 0064trans S x
  65. 0065exact hfirstindex_witness
  66. 0066rewrite hxzero
  67. 0067refl
  68. 0068have hsecondindex : exists k. x = S k
  69. 0069specialize nonzero_is_succ (x)
  70. 0070apply nonzero_is_succ
  71. 0071exact hindexzero
  72. 0072cases hsecondindex
  73. 0073have hnindex : n = S (S x1)
  74. 0074trans S x
  75. 0075exact hfirstindex_witness
  76. 0076rewrite hsecondindex_witness
  77. 0077refl
  78. 0078have hsecond : ∃ A. ∃ B. ∃ R. ∃ T. ∃ Q. ∃ C. ∃ H. PowerDifferenceSecondOrder(a,b,d,x1,A,B,R,T,Q,C,H)
  79. 0079specialize lte_power_difference_second_order_exists (a)
  80. 0080specialize lte_power_difference_second_order_exists (b)
  81. 0081specialize lte_power_difference_second_order_exists (d)
  82. 0082specialize lte_power_difference_second_order_exists (x1)
  83. 0083apply lte_power_difference_second_order_exists
  84. 0084exact ha
  85. 0085cases hsecond
  86. 0086cases hsecond_witness
  87. 0087cases hsecond_witness_witness
  88. 0088cases hsecond_witness_witness_witness
  89. 0089cases hsecond_witness_witness_witness_witness
  90. 0090cases hsecond_witness_witness_witness_witness_witness
  91. 0091cases hsecond_witness_witness_witness_witness_witness_witness
  92. 0092cases hsecond_witness_witness_witness_witness_witness_witness_witness
  93. 0093cases hsecond_witness_witness_witness_witness_witness_witness_witness_right
  94. 0094cases hsecond_witness_witness_witness_witness_witness_witness_witness_right_right
  95. 0095cases hsecond_witness_witness_witness_witness_witness_witness_witness_right_right_right
  96. 0096cases hsecond_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
  97. 0097cases hsecond_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right
  98. 0098exists x2
  99. 0099exists x3
  100. 0100exists x6
  101. 0101split
  102. 0102specialize lte_power_exponent_eq_transport (a)
  103. 0103specialize lte_power_exponent_eq_transport (S (S x1))
  104. 0104specialize lte_power_exponent_eq_transport (n)
  105. 0105specialize lte_power_exponent_eq_transport (x2)
  106. 0106apply lte_power_exponent_eq_transport
  107. 0107symm
  108. 0108exact hnindex
  109. 0109exact hsecond_witness_witness_witness_witness_witness_witness_witness_left
  110. 0110split
  111. 0111specialize lte_power_exponent_eq_transport (b)
  112. 0112specialize lte_power_exponent_eq_transport (S (S x1))
  113. 0113specialize lte_power_exponent_eq_transport (n)
  114. 0114specialize lte_power_exponent_eq_transport (x3)
  115. 0115apply lte_power_exponent_eq_transport
  116. 0116symm
  117. 0117exact hnindex
  118. 0118exact hsecond_witness_witness_witness_witness_witness_witness_witness_right_left
  119. 0119split
  120. 0120exact hsecond_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left
  121. 0121intro hQdiv
  122. 0122have hfirst : x6 = n * x4 + d * x7
  123. 0123rewrite hnindex
  124. 0124exact hsecond_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_left
  125. 0125rewrite hfirst at hQdiv
  126. 0126specialize lte_nondivisor_add_multiple (p)
  127. 0127specialize lte_nondivisor_add_multiple (n * x4)
  128. 0128specialize lte_nondivisor_add_multiple (d)
  129. 0129specialize lte_nondivisor_add_multiple (x7)
  130. 0130apply lte_nondivisor_add_multiple
  131. 0131intro hproduct
  132. 0132specialize prime_nondivisor_mul (p)
  133. 0133specialize prime_nondivisor_mul (n)
  134. 0134specialize prime_nondivisor_mul (x4)
  135. 0135apply prime_nondivisor_mul
  136. 0136exact hp
  137. 0137exact hn
  138. 0138intro hRdiv
  139. 0139specialize lte_nondivisor_power (p)
  140. 0140specialize lte_nondivisor_power (b)
  141. 0141specialize lte_nondivisor_power (S x1)
  142. 0142specialize lte_nondivisor_power (x4)
  143. 0143apply lte_nondivisor_power
  144. 0144exact hp
  145. 0145exact hb
  146. 0146exact hsecond_witness_witness_witness_witness_witness_witness_witness_right_right_left
  147. 0147exact hRdiv
  148. 0148exact hproduct
  149. 0149exact hd
  150. 0150exact hQdiv