TS002X · theorem body

distinct_prime_power_valuation_zero

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

The prime-power valuation of a distinct prime factor is exactly zero.

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. ∀ e. Prime(p) → Prime(q) → ¬p = q → PowerValuation(p,q,e) → e = 0

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0004 Prime PD0046 PowerValuation

In local proof propositions

PD0003 Dvd
Exact expanded first-order statement
forall p q e. ((~(p = 1) /\ forall frm_prime_left_ftsp_p frm_prime_right_ftsp_p. p = frm_prime_left_ftsp_p * frm_prime_right_ftsp_p -> frm_prime_left_ftsp_p = 1 \/ frm_prime_right_ftsp_p = 1)) -> ((~(q = 1) /\ forall frm_prime_left_ftsp_q frm_prime_right_ftsp_q. q = frm_prime_left_ftsp_q * frm_prime_right_ftsp_q -> frm_prime_left_ftsp_q = 1 \/ frm_prime_right_ftsp_q = 1)) -> ~(p = q) -> (((exists bpv_gap_ftsp_distinct_exponent_bound. bpv_gap_ftsp_distinct_exponent_bound + e = q) /\ (exists bpv_result_ftsp_distinct_selected. ((exists ff_b_ftsp_distinct_selected_power ff_c_ftsp_distinct_selected_power. ((forall ff_i_ftsp_distinct_selected_power_repeat. (exists ff_lt_ftsp_distinct_selected_power_repeat_bound. ff_lt_ftsp_distinct_selected_power_repeat_bound + S ff_i_ftsp_distinct_selected_power_repeat = e) -> (((exists ff_h_ftsp_distinct_selected_power_repeat_decoded. ff_h_ftsp_distinct_selected_power_repeat_decoded + S (p) = S ((S (ff_i_ftsp_distinct_selected_power_repeat)) * ff_c_ftsp_distinct_selected_power)) /\ exists ff_q_ftsp_distinct_selected_power_repeat_decoded. ff_b_ftsp_distinct_selected_power = ff_q_ftsp_distinct_selected_power_repeat_decoded * S ((S (ff_i_ftsp_distinct_selected_power_repeat)) * ff_c_ftsp_distinct_selected_power) + (p)))) /\ (exists ff_u_ftsp_distinct_selected_power_product ff_v_ftsp_distinct_selected_power_product. ((((exists ff_h_ftsp_distinct_selected_power_product_start. ff_h_ftsp_distinct_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_distinct_selected_power_product)) /\ exists ff_q_ftsp_distinct_selected_power_product_start. ff_u_ftsp_distinct_selected_power_product = ff_q_ftsp_distinct_selected_power_product_start * S ((S (0)) * ff_v_ftsp_distinct_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_distinct_selected_power_product_terminal. ff_h_ftsp_distinct_selected_power_product_terminal + S (bpv_result_ftsp_distinct_selected) = S ((S (e)) * ff_v_ftsp_distinct_selected_power_product)) /\ exists ff_q_ftsp_distinct_selected_power_product_terminal. ff_u_ftsp_distinct_selected_power_product = ff_q_ftsp_distinct_selected_power_product_terminal * S ((S (e)) * ff_v_ftsp_distinct_selected_power_product) + (bpv_result_ftsp_distinct_selected))) /\ forall ff_i_ftsp_distinct_selected_power_product. (exists ff_lt_ftsp_distinct_selected_power_product_bound. ff_lt_ftsp_distinct_selected_power_product_bound + S ff_i_ftsp_distinct_selected_power_product = e) -> exists ff_p_ftsp_distinct_selected_power_product ff_r_ftsp_distinct_selected_power_product ff_s_ftsp_distinct_selected_power_product. ((((exists ff_h_ftsp_distinct_selected_power_product_factor. ff_h_ftsp_distinct_selected_power_product_factor + S (ff_p_ftsp_distinct_selected_power_product) = S ((S (ff_i_ftsp_distinct_selected_power_product)) * ff_c_ftsp_distinct_selected_power)) /\ exists ff_q_ftsp_distinct_selected_power_product_factor. ff_b_ftsp_distinct_selected_power = ff_q_ftsp_distinct_selected_power_product_factor * S ((S (ff_i_ftsp_distinct_selected_power_product)) * ff_c_ftsp_distinct_selected_power) + (ff_p_ftsp_distinct_selected_power_product))) /\ ((((exists ff_h_ftsp_distinct_selected_power_product_partial. ff_h_ftsp_distinct_selected_power_product_partial + S (ff_r_ftsp_distinct_selected_power_product) = S ((S (ff_i_ftsp_distinct_selected_power_product)) * ff_v_ftsp_distinct_selected_power_product)) /\ exists ff_q_ftsp_distinct_selected_power_product_partial. ff_u_ftsp_distinct_selected_power_product = ff_q_ftsp_distinct_selected_power_product_partial * S ((S (ff_i_ftsp_distinct_selected_power_product)) * ff_v_ftsp_distinct_selected_power_product) + (ff_r_ftsp_distinct_selected_power_product))) /\ ((((exists ff_h_ftsp_distinct_selected_power_product_successor. ff_h_ftsp_distinct_selected_power_product_successor + S (ff_s_ftsp_distinct_selected_power_product) = S ((S (S ff_i_ftsp_distinct_selected_power_product)) * ff_v_ftsp_distinct_selected_power_product)) /\ exists ff_q_ftsp_distinct_selected_power_product_successor. ff_u_ftsp_distinct_selected_power_product = ff_q_ftsp_distinct_selected_power_product_successor * S ((S (S ff_i_ftsp_distinct_selected_power_product)) * ff_v_ftsp_distinct_selected_power_product) + (ff_s_ftsp_distinct_selected_power_product))) /\ ff_s_ftsp_distinct_selected_power_product = ff_r_ftsp_distinct_selected_power_product * ff_p_ftsp_distinct_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_distinct_selected_divides. q = bpv_result_ftsp_distinct_selected * bpv_factor_ftsp_distinct_selected_divides)))) /\ forall bpv_candidate_ftsp_distinct. (exists bpv_gap_ftsp_distinct_candidate_bound. bpv_gap_ftsp_distinct_candidate_bound + bpv_candidate_ftsp_distinct = q) -> (exists bpv_result_ftsp_distinct_candidate. ((exists ff_b_ftsp_distinct_candidate_power ff_c_ftsp_distinct_candidate_power. ((forall ff_i_ftsp_distinct_candidate_power_repeat. (exists ff_lt_ftsp_distinct_candidate_power_repeat_bound. ff_lt_ftsp_distinct_candidate_power_repeat_bound + S ff_i_ftsp_distinct_candidate_power_repeat = bpv_candidate_ftsp_distinct) -> (((exists ff_h_ftsp_distinct_candidate_power_repeat_decoded. ff_h_ftsp_distinct_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_ftsp_distinct_candidate_power_repeat)) * ff_c_ftsp_distinct_candidate_power)) /\ exists ff_q_ftsp_distinct_candidate_power_repeat_decoded. ff_b_ftsp_distinct_candidate_power = ff_q_ftsp_distinct_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_distinct_candidate_power_repeat)) * ff_c_ftsp_distinct_candidate_power) + (p)))) /\ (exists ff_u_ftsp_distinct_candidate_power_product ff_v_ftsp_distinct_candidate_power_product. ((((exists ff_h_ftsp_distinct_candidate_power_product_start. ff_h_ftsp_distinct_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_distinct_candidate_power_product)) /\ exists ff_q_ftsp_distinct_candidate_power_product_start. ff_u_ftsp_distinct_candidate_power_product = ff_q_ftsp_distinct_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_distinct_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_distinct_candidate_power_product_terminal. ff_h_ftsp_distinct_candidate_power_product_terminal + S (bpv_result_ftsp_distinct_candidate) = S ((S (bpv_candidate_ftsp_distinct)) * ff_v_ftsp_distinct_candidate_power_product)) /\ exists ff_q_ftsp_distinct_candidate_power_product_terminal. ff_u_ftsp_distinct_candidate_power_product = ff_q_ftsp_distinct_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_distinct)) * ff_v_ftsp_distinct_candidate_power_product) + (bpv_result_ftsp_distinct_candidate))) /\ forall ff_i_ftsp_distinct_candidate_power_product. (exists ff_lt_ftsp_distinct_candidate_power_product_bound. ff_lt_ftsp_distinct_candidate_power_product_bound + S ff_i_ftsp_distinct_candidate_power_product = bpv_candidate_ftsp_distinct) -> exists ff_p_ftsp_distinct_candidate_power_product ff_r_ftsp_distinct_candidate_power_product ff_s_ftsp_distinct_candidate_power_product. ((((exists ff_h_ftsp_distinct_candidate_power_product_factor. ff_h_ftsp_distinct_candidate_power_product_factor + S (ff_p_ftsp_distinct_candidate_power_product) = S ((S (ff_i_ftsp_distinct_candidate_power_product)) * ff_c_ftsp_distinct_candidate_power)) /\ exists ff_q_ftsp_distinct_candidate_power_product_factor. ff_b_ftsp_distinct_candidate_power = ff_q_ftsp_distinct_candidate_power_product_factor * S ((S (ff_i_ftsp_distinct_candidate_power_product)) * ff_c_ftsp_distinct_candidate_power) + (ff_p_ftsp_distinct_candidate_power_product))) /\ ((((exists ff_h_ftsp_distinct_candidate_power_product_partial. ff_h_ftsp_distinct_candidate_power_product_partial + S (ff_r_ftsp_distinct_candidate_power_product) = S ((S (ff_i_ftsp_distinct_candidate_power_product)) * ff_v_ftsp_distinct_candidate_power_product)) /\ exists ff_q_ftsp_distinct_candidate_power_product_partial. ff_u_ftsp_distinct_candidate_power_product = ff_q_ftsp_distinct_candidate_power_product_partial * S ((S (ff_i_ftsp_distinct_candidate_power_product)) * ff_v_ftsp_distinct_candidate_power_product) + (ff_r_ftsp_distinct_candidate_power_product))) /\ ((((exists ff_h_ftsp_distinct_candidate_power_product_successor. ff_h_ftsp_distinct_candidate_power_product_successor + S (ff_s_ftsp_distinct_candidate_power_product) = S ((S (S ff_i_ftsp_distinct_candidate_power_product)) * ff_v_ftsp_distinct_candidate_power_product)) /\ exists ff_q_ftsp_distinct_candidate_power_product_successor. ff_u_ftsp_distinct_candidate_power_product = ff_q_ftsp_distinct_candidate_power_product_successor * S ((S (S ff_i_ftsp_distinct_candidate_power_product)) * ff_v_ftsp_distinct_candidate_power_product) + (ff_s_ftsp_distinct_candidate_power_product))) /\ ff_s_ftsp_distinct_candidate_power_product = ff_r_ftsp_distinct_candidate_power_product * ff_p_ftsp_distinct_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_distinct_candidate_divides. q = bpv_result_ftsp_distinct_candidate * bpv_factor_ftsp_distinct_candidate_divides))) -> (exists bpv_gap_ftsp_distinct_maximal. bpv_gap_ftsp_distinct_maximal + bpv_candidate_ftsp_distinct = e)) -> e = 0

Proof neighborhood

Direct theorem prerequisites

eq_decidable · Stable closed power_valuation_nonzero_exponent_divides_base · Alpha closed TS002W prime_divisor_of_prime_forces_equality

Direct theorem dependents

TS0035 distinct_prime_factor_even_valuation_reflects_prefix

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

26 script commands · 7 reading checkpoints · 1 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)
prime divisor of prime forces equality
01Fix variables and assumptionsL1–7

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

  1. L1
    intro p
  2. L2
    intro q
  3. L3
    intro e
  4. L4
    intro hp
  5. L5
    intro hq
  6. L6
    intro hdistinct
  7. L7
    intro hvaluation
02Use earlier factsL8–9

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

  1. L8
    specialize eq_decidable e
  2. L9
    specialize eq_decidable 0
03Separate the logical casesL10–10

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

  1. L10
    cases eq_decidable
04Use earlier factsL11–11

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

  1. L11
    exact eq_decidable_left
05Separate the logical casesL12–12

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

  1. L12
    exfalso
06Establish hdividesL13–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply power valuation nonzero exponent divides base.

  1. L13
    have hdivides : Dvd(p,q)Definitions: Dvd(p,q)Original native command in the exact edition
  2. L14
    specialize power_valuation_nonzero_exponent_divides_base p
  3. L15
    specialize power_valuation_nonzero_exponent_divides_base q
  4. L16
    specialize power_valuation_nonzero_exponent_divides_base e
  5. L17
    apply power_valuation_nonzero_exponent_divides_base
  6. L18
    exact hvaluation
  7. L19
    exact eq_decidable_right
  8. L20
    apply hdistinct
  9. L21
    specialize prime_divisor_of_prime_forces_equality p
  10. L22
    specialize prime_divisor_of_prime_forces_equality q
07Use earlier factsL23–26

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

  1. L23
    apply prime_divisor_of_prime_forces_equality
  2. L24
    exact hp
  3. L25
    exact hq
  4. L26
    exact hdivides

Library-wide reading audit

Original defined command ledger · 26 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro e
  4. 0004intro hp
  5. 0005intro hq
  6. 0006intro hdistinct
  7. 0007intro hvaluation
  8. 0008specialize eq_decidable e
  9. 0009specialize eq_decidable 0
  10. 0010cases eq_decidable
  11. 0011exact eq_decidable_left
  12. 0012exfalso
  13. 0013have hdivides : Dvd(p,q)
    Exact native replay linehave hdivides : exists ftcn_factor_ftsp_prime_divides_prime. (q) = (p) * ftcn_factor_ftsp_prime_divides_prime
  14. 0014specialize power_valuation_nonzero_exponent_divides_base p
  15. 0015specialize power_valuation_nonzero_exponent_divides_base q
  16. 0016specialize power_valuation_nonzero_exponent_divides_base e
  17. 0017apply power_valuation_nonzero_exponent_divides_base
  18. 0018exact hvaluation
  19. 0019exact eq_decidable_right
  20. 0020apply hdistinct
  21. 0021specialize prime_divisor_of_prime_forces_equality p
  22. 0022specialize prime_divisor_of_prime_forces_equality q
  23. 0023apply prime_divisor_of_prime_forces_equality
  24. 0024exact hp
  25. 0025exact hq
  26. 0026exact hdivides