PV0008

prime_divisor_of_prime_power

Every actual prime divisor of a witnessed prime power is its base prime.

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.

This is a shared constructive tool, not an additional major blueprint goal. The list covers every prime divisor, has no repeated primes, and contains actual prime-power values. One uses the empty support; zero is excluded.

Exact theorem in conservative defined notation

∀ p. ∀ q. ∀ k. ∀ z. Prime(p) → Prime(q) → Pow(p,k,z) → Dvd(q,z) → q = p

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

Definition DAG

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

Actual proof prerequisites

eq_decidable · checked external prerequisiteprime_nonzero · checked external prerequisiteone_le_of_ne_zero · checked external prerequisitepow_nonzero_of_one_le · checked external prerequisiteprime_valuation_distinct_prime_power_zeroprime_valuation_nondivisor_of_zero
Original expanded first-order statement 
forall p q k z. (~((p) = 1) /\ forall pvs_left_prime_power_base pvs_right_prime_power_base. (p) = pvs_left_prime_power_base * pvs_right_prime_power_base -> pvs_left_prime_power_base = 1 \/ pvs_right_prime_power_base = 1) -> (~((q) = 1) /\ forall pvs_left_prime_power_divisor pvs_right_prime_power_divisor. (q) = pvs_left_prime_power_divisor * pvs_right_prime_power_divisor -> pvs_left_prime_power_divisor = 1 \/ pvs_right_prime_power_divisor = 1) -> (exists pa_b_pvs_prime_power_value pa_c_pvs_prime_power_value. ((forall pa_i_pvs_prime_power_value_repeat. (exists pa_lt_pvs_prime_power_value_repeat_bound. pa_lt_pvs_prime_power_value_repeat_bound + S pa_i_pvs_prime_power_value_repeat = k) -> (((exists pa_h_pvs_prime_power_value_repeat_decoded. pa_h_pvs_prime_power_value_repeat_decoded + S (p) = S ((S (pa_i_pvs_prime_power_value_repeat)) * pa_c_pvs_prime_power_value)) /\ exists pa_q_pvs_prime_power_value_repeat_decoded. pa_b_pvs_prime_power_value = pa_q_pvs_prime_power_value_repeat_decoded * S ((S (pa_i_pvs_prime_power_value_repeat)) * pa_c_pvs_prime_power_value) + (p)))) /\ (exists pa_u_pvs_prime_power_value_product pa_v_pvs_prime_power_value_product. ((((exists pa_h_pvs_prime_power_value_product_start. pa_h_pvs_prime_power_value_product_start + S (1) = S ((S (0)) * pa_v_pvs_prime_power_value_product)) /\ exists pa_q_pvs_prime_power_value_product_start. pa_u_pvs_prime_power_value_product = pa_q_pvs_prime_power_value_product_start * S ((S (0)) * pa_v_pvs_prime_power_value_product) + (1))) /\ ((((exists pa_h_pvs_prime_power_value_product_terminal. pa_h_pvs_prime_power_value_product_terminal + S (z) = S ((S (k)) * pa_v_pvs_prime_power_value_product)) /\ exists pa_q_pvs_prime_power_value_product_terminal. pa_u_pvs_prime_power_value_product = pa_q_pvs_prime_power_value_product_terminal * S ((S (k)) * pa_v_pvs_prime_power_value_product) + (z))) /\ forall pa_i_pvs_prime_power_value_product. (exists pa_lt_pvs_prime_power_value_product_bound. pa_lt_pvs_prime_power_value_product_bound + S pa_i_pvs_prime_power_value_product = k) -> exists pa_p_pvs_prime_power_value_product pa_r_pvs_prime_power_value_product pa_s_pvs_prime_power_value_product. ((((exists pa_h_pvs_prime_power_value_product_factor. pa_h_pvs_prime_power_value_product_factor + S (pa_p_pvs_prime_power_value_product) = S ((S (pa_i_pvs_prime_power_value_product)) * pa_c_pvs_prime_power_value)) /\ exists pa_q_pvs_prime_power_value_product_factor. pa_b_pvs_prime_power_value = pa_q_pvs_prime_power_value_product_factor * S ((S (pa_i_pvs_prime_power_value_product)) * pa_c_pvs_prime_power_value) + (pa_p_pvs_prime_power_value_product))) /\ ((((exists pa_h_pvs_prime_power_value_product_partial. pa_h_pvs_prime_power_value_product_partial + S (pa_r_pvs_prime_power_value_product) = S ((S (pa_i_pvs_prime_power_value_product)) * pa_v_pvs_prime_power_value_product)) /\ exists pa_q_pvs_prime_power_value_product_partial. pa_u_pvs_prime_power_value_product = pa_q_pvs_prime_power_value_product_partial * S ((S (pa_i_pvs_prime_power_value_product)) * pa_v_pvs_prime_power_value_product) + (pa_r_pvs_prime_power_value_product))) /\ ((((exists pa_h_pvs_prime_power_value_product_successor. pa_h_pvs_prime_power_value_product_successor + S (pa_s_pvs_prime_power_value_product) = S ((S (S pa_i_pvs_prime_power_value_product)) * pa_v_pvs_prime_power_value_product)) /\ exists pa_q_pvs_prime_power_value_product_successor. pa_u_pvs_prime_power_value_product = pa_q_pvs_prime_power_value_product_successor * S ((S (S pa_i_pvs_prime_power_value_product)) * pa_v_pvs_prime_power_value_product) + (pa_s_pvs_prime_power_value_product))) /\ pa_s_pvs_prime_power_value_product = pa_r_pvs_prime_power_value_product * pa_p_pvs_prime_power_value_product)))))))) -> (exists pvs_factor_prime_power_divides. (z) = (q) * pvs_factor_prime_power_divides) -> q = p

Complete tactic proof in conservative notation

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

41 script commands · 11 reading checkpoints · 0 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 (2)
prime valuation nondivisor of zeroprime valuation distinct prime power zero
01Fix variables and assumptionsL1–8

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

  1. L1
    intro p
  2. L2
    intro q
  3. L3
    intro k
  4. L4
    intro z
  5. L5
    intro hp
  6. L6
    intro hq
  7. L7
    intro hpow
  8. L8
    intro hdiv
02Use earlier factsL9–10

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

  1. L9
    specialize eq_decidable q
  2. L10
    specialize eq_decidable p
03Separate the logical casesL11–11

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

  1. L11
    cases eq_decidable
04Use earlier factsL12–12

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

  1. L12
    exact eq_decidable_left
05Separate the logical casesL13–13

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

  1. L13
    exfalso
06Use earlier factsL14–17

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

  1. L14
    specialize prime_valuation_nondivisor_of_zero (q)
  2. L15
    specialize prime_valuation_nondivisor_of_zero (z)
  3. L16
    apply prime_valuation_nondivisor_of_zero
  4. L17
    exact hq
07Fix variables and assumptionsL18–18

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

  1. L18
    intro hz
08Use earlier factsL19–24

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

  1. L19
    specialize pow_nonzero_of_one_le (p)
  2. L20
    specialize pow_nonzero_of_one_le (k)
  3. L21
    specialize pow_nonzero_of_one_le (z)
  4. L22
    apply pow_nonzero_of_one_le
  5. L23
    specialize one_le_of_ne_zero (p)
  6. L24
    apply one_le_of_ne_zero
09Fix variables and assumptionsL25–25

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

  1. L25
    intro hpzero
10Use earlier factsL26–35

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

  1. L26
    specialize prime_nonzero (p)
  2. L27
    apply prime_nonzero
  3. L28
    exact hp
  4. L29
    exact hpzero
  5. L30
    exact hpow
  6. L31
    exact hz
  7. L32
    specialize prime_valuation_distinct_prime_power_zero (p)
  8. L33
    specialize prime_valuation_distinct_prime_power_zero (q)
  9. L34
    specialize prime_valuation_distinct_prime_power_zero (k)
  10. L35
    specialize prime_valuation_distinct_prime_power_zero (z)
11Use earlier factsL36–41

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

  1. L36
    apply prime_valuation_distinct_prime_power_zero
  2. L37
    exact hp
  3. L38
    exact hq
  4. L39
    exact eq_decidable_right
  5. L40
    exact hpow
  6. L41
    exact hdiv

Library-wide reading audit

Original defined command ledger · 41 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro k
  4. 0004intro z
  5. 0005intro hp
  6. 0006intro hq
  7. 0007intro hpow
  8. 0008intro hdiv
  9. 0009specialize eq_decidable q
  10. 0010specialize eq_decidable p
  11. 0011cases eq_decidable
  12. 0012exact eq_decidable_left
  13. 0013exfalso
  14. 0014specialize prime_valuation_nondivisor_of_zero (q)
  15. 0015specialize prime_valuation_nondivisor_of_zero (z)
  16. 0016apply prime_valuation_nondivisor_of_zero
  17. 0017exact hq
  18. 0018intro hz
  19. 0019specialize pow_nonzero_of_one_le (p)
  20. 0020specialize pow_nonzero_of_one_le (k)
  21. 0021specialize pow_nonzero_of_one_le (z)
  22. 0022apply pow_nonzero_of_one_le
  23. 0023specialize one_le_of_ne_zero (p)
  24. 0024apply one_le_of_ne_zero
  25. 0025intro hpzero
  26. 0026specialize prime_nonzero (p)
  27. 0027apply prime_nonzero
  28. 0028exact hp
  29. 0029exact hpzero
  30. 0030exact hpow
  31. 0031exact hz
  32. 0032specialize prime_valuation_distinct_prime_power_zero (p)
  33. 0033specialize prime_valuation_distinct_prime_power_zero (q)
  34. 0034specialize prime_valuation_distinct_prime_power_zero (k)
  35. 0035specialize prime_valuation_distinct_prime_power_zero (z)
  36. 0036apply prime_valuation_distinct_prime_power_zero
  37. 0037exact hp
  38. 0038exact hq
  39. 0039exact eq_decidable_right
  40. 0040exact hpow
  41. 0041exact hdiv