EL0010

lte_nondivisor_power

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

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

Exact expanded first-order arithmetic 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)

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 4 declared prerequisites and contains 51 exact native proof lines.

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

Proof neighborhood

Direct dependencies

pow_zero Stable theorem; checked-use authorized EL000C lte_prime_nondivisor_one pow_successor_decompose Stable theorem; checked-use authorized prime_nondivisor_mul Alpha theorem; checked-use authorized

Direct dependents

EL001B lte_odd_prime_power_difference_quotient EL001C lte_coprime_power_difference_quotient EL001D lte_power_difference_valuation_step

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

Named ingredients (1)
lte prime nondivisor one

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

01Fix variables and assumptionsL1–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
  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 exact 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 : exists r. (exists pa_b_olte_power_previous pa_c_olte_power_previous. ((forall pa_i_olte_power_previous_repeat. (exists pa_lt_olte_power_previous_repeat_bound. pa_lt_olte_power_previous_repeat_bound + S pa_i_olte_power_previous_repeat = n) -> (((exists pa_h_olte_power_previous_repeat_decoded. pa_h_olte_power_previous_repeat_decoded + S (b) = S ((S (pa_i_olte_power_previous_repeat)) * pa_c_olte_power_previous)) /\ exists pa_q_olte_power_previous_repeat_decoded. pa_b_olte_power_previous = pa_q_olte_power_previous_repeat_decoded * S ((S (pa_i_olte_power_previous_repeat)) * pa_c_olte_power_previous) + (b)))) /\ (exists pa_u_olte_power_previous_product pa_v_olte_power_previous_product. ((((exists pa_h_olte_power_previous_product_start. pa_h_olte_power_previous_product_start + S (1) = S ((S (0)) * pa_v_olte_power_previous_product)) /\ exists pa_q_olte_power_previous_product_start. pa_u_olte_power_previous_product = pa_q_olte_power_previous_product_start * S ((S (0)) * pa_v_olte_power_previous_product) + (1))) /\ ((((exists pa_h_olte_power_previous_product_terminal. pa_h_olte_power_previous_product_terminal + S (r) = S ((S (n)) * pa_v_olte_power_previous_product)) /\ exists pa_q_olte_power_previous_product_terminal. pa_u_olte_power_previous_product = pa_q_olte_power_previous_product_terminal * S ((S (n)) * pa_v_olte_power_previous_product) + (r))) /\ forall pa_i_olte_power_previous_product. (exists pa_lt_olte_power_previous_product_bound. pa_lt_olte_power_previous_product_bound + S pa_i_olte_power_previous_product = n) -> exists pa_p_olte_power_previous_product pa_r_olte_power_previous_product pa_s_olte_power_previous_product. ((((exists pa_h_olte_power_previous_product_factor. pa_h_olte_power_previous_product_factor + S (pa_p_olte_power_previous_product) = S ((S (pa_i_olte_power_previous_product)) * pa_c_olte_power_previous)) /\ exists pa_q_olte_power_previous_product_factor. pa_b_olte_power_previous = pa_q_olte_power_previous_product_factor * S ((S (pa_i_olte_power_previous_product)) * pa_c_olte_power_previous) + (pa_p_olte_power_previous_product))) /\ ((((exists pa_h_olte_power_previous_product_partial. pa_h_olte_power_previous_product_partial + S (pa_r_olte_power_previous_product) = S ((S (pa_i_olte_power_previous_product)) * pa_v_olte_power_previous_product)) /\ exists pa_q_olte_power_previous_product_partial. pa_u_olte_power_previous_product = pa_q_olte_power_previous_product_partial * S ((S (pa_i_olte_power_previous_product)) * pa_v_olte_power_previous_product) + (pa_r_olte_power_previous_product))) /\ ((((exists pa_h_olte_power_previous_product_successor. pa_h_olte_power_previous_product_successor + S (pa_s_olte_power_previous_product) = S ((S (S pa_i_olte_power_previous_product)) * pa_v_olte_power_previous_product)) /\ exists pa_q_olte_power_previous_product_successor. pa_u_olte_power_previous_product = pa_q_olte_power_previous_product_successor * S ((S (S pa_i_olte_power_previous_product)) * pa_v_olte_power_previous_product) + (pa_s_olte_power_previous_product))) /\ pa_s_olte_power_previous_product = pa_r_olte_power_previous_product * pa_p_olte_power_previous_product)))))))) /\ 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