EL0010

lte_nondivisor_power

Every witnessed power of a nondivisor remains a nondivisor of the actual prime, including the zeroth power.

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. ∀ b. ∀ n. ∀ B. ¬p = 1 ∧ (∀ x. ∀ y. p = x · y → x = 1 ∨ y = 1) → ¬Dvd(p,b) → Pow(b,n,B) → ¬Dvd(p,B)

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

Definition DAG

Dvd(d,n) · 2Pow(a,e,z) · 2

Actual proof prerequisites

pow_zero · checked external prerequisitelte_prime_nondivisor_onepow_successor_decompose · checked external prerequisiteprime_nondivisor_mul · checked external prerequisite
Original expanded first-order statement 
forall p b n B. (~((p) = 1) /\ forall pvs_left_power_prime pvs_right_power_prime. (p) = pvs_left_power_prime * pvs_right_power_prime -> pvs_left_power_prime = 1 \/ pvs_right_power_prime = 1) -> ~(exists olte_factor_power_base. (b) = (p) * olte_factor_power_base) -> (exists pa_b_olte_power_source pa_c_olte_power_source. ((forall pa_i_olte_power_source_repeat. (exists pa_lt_olte_power_source_repeat_bound. pa_lt_olte_power_source_repeat_bound + S pa_i_olte_power_source_repeat = n) -> (((exists pa_h_olte_power_source_repeat_decoded. pa_h_olte_power_source_repeat_decoded + S (b) = S ((S (pa_i_olte_power_source_repeat)) * pa_c_olte_power_source)) /\ exists pa_q_olte_power_source_repeat_decoded. pa_b_olte_power_source = pa_q_olte_power_source_repeat_decoded * S ((S (pa_i_olte_power_source_repeat)) * pa_c_olte_power_source) + (b)))) /\ (exists pa_u_olte_power_source_product pa_v_olte_power_source_product. ((((exists pa_h_olte_power_source_product_start. pa_h_olte_power_source_product_start + S (1) = S ((S (0)) * pa_v_olte_power_source_product)) /\ exists pa_q_olte_power_source_product_start. pa_u_olte_power_source_product = pa_q_olte_power_source_product_start * S ((S (0)) * pa_v_olte_power_source_product) + (1))) /\ ((((exists pa_h_olte_power_source_product_terminal. pa_h_olte_power_source_product_terminal + S (B) = S ((S (n)) * pa_v_olte_power_source_product)) /\ exists pa_q_olte_power_source_product_terminal. pa_u_olte_power_source_product = pa_q_olte_power_source_product_terminal * S ((S (n)) * pa_v_olte_power_source_product) + (B))) /\ forall pa_i_olte_power_source_product. (exists pa_lt_olte_power_source_product_bound. pa_lt_olte_power_source_product_bound + S pa_i_olte_power_source_product = n) -> exists pa_p_olte_power_source_product pa_r_olte_power_source_product pa_s_olte_power_source_product. ((((exists pa_h_olte_power_source_product_factor. pa_h_olte_power_source_product_factor + S (pa_p_olte_power_source_product) = S ((S (pa_i_olte_power_source_product)) * pa_c_olte_power_source)) /\ exists pa_q_olte_power_source_product_factor. pa_b_olte_power_source = pa_q_olte_power_source_product_factor * S ((S (pa_i_olte_power_source_product)) * pa_c_olte_power_source) + (pa_p_olte_power_source_product))) /\ ((((exists pa_h_olte_power_source_product_partial. pa_h_olte_power_source_product_partial + S (pa_r_olte_power_source_product) = S ((S (pa_i_olte_power_source_product)) * pa_v_olte_power_source_product)) /\ exists pa_q_olte_power_source_product_partial. pa_u_olte_power_source_product = pa_q_olte_power_source_product_partial * S ((S (pa_i_olte_power_source_product)) * pa_v_olte_power_source_product) + (pa_r_olte_power_source_product))) /\ ((((exists pa_h_olte_power_source_product_successor. pa_h_olte_power_source_product_successor + S (pa_s_olte_power_source_product) = S ((S (S pa_i_olte_power_source_product)) * pa_v_olte_power_source_product)) /\ exists pa_q_olte_power_source_product_successor. pa_u_olte_power_source_product = pa_q_olte_power_source_product_successor * S ((S (S pa_i_olte_power_source_product)) * pa_v_olte_power_source_product) + (pa_s_olte_power_source_product))) /\ pa_s_olte_power_source_product = pa_r_olte_power_source_product * pa_p_olte_power_source_product)))))))) -> ~(exists olte_factor_power_result. (B) = (p) * olte_factor_power_result)

Complete tactic proof in conservative notation

All 51 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

51 script commands · 13 reading checkpoints · 2 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 (1)
lte prime nondivisor one
01Fix variables and assumptionsL1–3

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

  1. L1
    intro p
  2. L2
    intro b
  3. L3
    intro n
02Induction on nL4–9

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L4
    induction n
  2. L5
    intro B
  3. L6
    intro hp
  4. L7
    intro hnot
  5. L8
    intro hpow
  6. L9
    intro hdiv
03Establish hBL10–19

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

  1. L10
    have hB : B = 1
  2. L11
    specialize pow_zero (b)
  3. L12
    specialize pow_zero (0)
  4. L13
    specialize pow_zero (B)
  5. L14
    apply pow_zero
  6. L15
    refl
  7. L16
    exact hpow
  8. L17
    specialize lte_prime_nondivisor_one (p)
  9. L18
    apply lte_prime_nondivisor_one
  10. L19
    exact hp
04Calculate and transport equalitiesL20–20

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

  1. L20
    rewrite hB at hdiv
05Use earlier factsL21–21

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

  1. L21
    exact hdiv
06Fix variables and assumptionsL22–26

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

  1. L22
    intro B
  2. L23
    intro hp
  3. L24
    intro hnot
  4. L25
    intro hpow
  5. L26
    intro hdiv
07Establish hprevL27–34

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

  1. L27
    have hprev : ∃ r. Pow(b,n,r) ∧ B = r · bDefinitions: Pow(b,n,r)Original native command in the exact edition
  2. L28
    specialize pow_successor_decompose (b)
  3. L29
    specialize pow_successor_decompose (n)
  4. L30
    specialize pow_successor_decompose (S n)
  5. L31
    specialize pow_successor_decompose (B)
  6. L32
    apply pow_successor_decompose
  7. L33
    refl
  8. L34
    exact hpow
08Separate the logical casesL35–36

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

  1. L35
    cases hprev
  2. L36
    cases hprev_witness
09Use earlier factsL37–41

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

  1. L37
    specialize prime_nondivisor_mul (p)
  2. L38
    specialize prime_nondivisor_mul (x)
  3. L39
    specialize prime_nondivisor_mul (b)
  4. L40
    apply prime_nondivisor_mul
  5. L41
    exact hp
10Fix variables and assumptionsL42–42

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

  1. L42
    intro hfactor
11Use earlier factsL43–49

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

  1. L43
    specialize IH (x)
  2. L44
    apply IH
  3. L45
    exact hp
  4. L46
    exact hnot
  5. L47
    exact hprev_witness_left
  6. L48
    exact hfactor
  7. L49
    exact hnot
12Calculate and transport equalitiesL50–50

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

  1. L50
    rewrite hprev_witness_right at hdiv
13Use earlier factsL51–51

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

  1. L51
    exact hdiv

Library-wide reading audit

Original defined command ledger · 51 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro n
  4. 0004induction n
  5. 0005intro B
  6. 0006intro hp
  7. 0007intro hnot
  8. 0008intro hpow
  9. 0009intro hdiv
  10. 0010have hB : B = 1
  11. 0011specialize pow_zero (b)
  12. 0012specialize pow_zero (0)
  13. 0013specialize pow_zero (B)
  14. 0014apply pow_zero
  15. 0015refl
  16. 0016exact hpow
  17. 0017specialize lte_prime_nondivisor_one (p)
  18. 0018apply lte_prime_nondivisor_one
  19. 0019exact hp
  20. 0020rewrite hB at hdiv
  21. 0021exact hdiv
  22. 0022intro B
  23. 0023intro hp
  24. 0024intro hnot
  25. 0025intro hpow
  26. 0026intro hdiv
  27. 0027have hprev : ∃ r. Pow(b,n,r) ∧ B = r · b
  28. 0028specialize pow_successor_decompose (b)
  29. 0029specialize pow_successor_decompose (n)
  30. 0030specialize pow_successor_decompose (S n)
  31. 0031specialize pow_successor_decompose (B)
  32. 0032apply pow_successor_decompose
  33. 0033refl
  34. 0034exact hpow
  35. 0035cases hprev
  36. 0036cases hprev_witness
  37. 0037specialize prime_nondivisor_mul (p)
  38. 0038specialize prime_nondivisor_mul (x)
  39. 0039specialize prime_nondivisor_mul (b)
  40. 0040apply prime_nondivisor_mul
  41. 0041exact hp
  42. 0042intro hfactor
  43. 0043specialize IH (x)
  44. 0044apply IH
  45. 0045exact hp
  46. 0046exact hnot
  47. 0047exact hprev_witness_left
  48. 0048exact hfactor
  49. 0049exact hnot
  50. 0050rewrite hprev_witness_right at hdiv
  51. 0051exact hdiv