KU000D · theorem body

prime_power_valuation_zero_iff_not_divides

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

At a prime base and nonzero value, valuation zero is equivalent to nondivisibility.

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

PD0003 Dvd PD0004 Prime PD0046 PowerValuation

In local proof propositions

none
Exact expanded first-order statement
forall p c e. ((~(p = 1) /\ forall frm_prime_left_kmcvznd_prime frm_prime_right_kmcvznd_prime. p = frm_prime_left_kmcvznd_prime * frm_prime_right_kmcvznd_prime -> frm_prime_left_kmcvznd_prime = 1 \/ frm_prime_right_kmcvznd_prime = 1)) -> ~(c = 0) -> (((exists bpv_gap_kmcvznd_valuation_exponent_bound. bpv_gap_kmcvznd_valuation_exponent_bound + e = c) /\ (exists bpv_result_kmcvznd_valuation_selected. ((exists ff_b_kmcvznd_valuation_selected_power ff_c_kmcvznd_valuation_selected_power. ((forall ff_i_kmcvznd_valuation_selected_power_repeat. (exists ff_lt_kmcvznd_valuation_selected_power_repeat_bound. ff_lt_kmcvznd_valuation_selected_power_repeat_bound + S ff_i_kmcvznd_valuation_selected_power_repeat = e) -> (((exists ff_h_kmcvznd_valuation_selected_power_repeat_decoded. ff_h_kmcvznd_valuation_selected_power_repeat_decoded + S (p) = S ((S (ff_i_kmcvznd_valuation_selected_power_repeat)) * ff_c_kmcvznd_valuation_selected_power)) /\ exists ff_q_kmcvznd_valuation_selected_power_repeat_decoded. ff_b_kmcvznd_valuation_selected_power = ff_q_kmcvznd_valuation_selected_power_repeat_decoded * S ((S (ff_i_kmcvznd_valuation_selected_power_repeat)) * ff_c_kmcvznd_valuation_selected_power) + (p)))) /\ (exists ff_u_kmcvznd_valuation_selected_power_product ff_v_kmcvznd_valuation_selected_power_product. ((((exists ff_h_kmcvznd_valuation_selected_power_product_start. ff_h_kmcvznd_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_kmcvznd_valuation_selected_power_product)) /\ exists ff_q_kmcvznd_valuation_selected_power_product_start. ff_u_kmcvznd_valuation_selected_power_product = ff_q_kmcvznd_valuation_selected_power_product_start * S ((S (0)) * ff_v_kmcvznd_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_kmcvznd_valuation_selected_power_product_terminal. ff_h_kmcvznd_valuation_selected_power_product_terminal + S (bpv_result_kmcvznd_valuation_selected) = S ((S (e)) * ff_v_kmcvznd_valuation_selected_power_product)) /\ exists ff_q_kmcvznd_valuation_selected_power_product_terminal. ff_u_kmcvznd_valuation_selected_power_product = ff_q_kmcvznd_valuation_selected_power_product_terminal * S ((S (e)) * ff_v_kmcvznd_valuation_selected_power_product) + (bpv_result_kmcvznd_valuation_selected))) /\ forall ff_i_kmcvznd_valuation_selected_power_product. (exists ff_lt_kmcvznd_valuation_selected_power_product_bound. ff_lt_kmcvznd_valuation_selected_power_product_bound + S ff_i_kmcvznd_valuation_selected_power_product = e) -> exists ff_p_kmcvznd_valuation_selected_power_product ff_r_kmcvznd_valuation_selected_power_product ff_s_kmcvznd_valuation_selected_power_product. ((((exists ff_h_kmcvznd_valuation_selected_power_product_factor. ff_h_kmcvznd_valuation_selected_power_product_factor + S (ff_p_kmcvznd_valuation_selected_power_product) = S ((S (ff_i_kmcvznd_valuation_selected_power_product)) * ff_c_kmcvznd_valuation_selected_power)) /\ exists ff_q_kmcvznd_valuation_selected_power_product_factor. ff_b_kmcvznd_valuation_selected_power = ff_q_kmcvznd_valuation_selected_power_product_factor * S ((S (ff_i_kmcvznd_valuation_selected_power_product)) * ff_c_kmcvznd_valuation_selected_power) + (ff_p_kmcvznd_valuation_selected_power_product))) /\ ((((exists ff_h_kmcvznd_valuation_selected_power_product_partial. ff_h_kmcvznd_valuation_selected_power_product_partial + S (ff_r_kmcvznd_valuation_selected_power_product) = S ((S (ff_i_kmcvznd_valuation_selected_power_product)) * ff_v_kmcvznd_valuation_selected_power_product)) /\ exists ff_q_kmcvznd_valuation_selected_power_product_partial. ff_u_kmcvznd_valuation_selected_power_product = ff_q_kmcvznd_valuation_selected_power_product_partial * S ((S (ff_i_kmcvznd_valuation_selected_power_product)) * ff_v_kmcvznd_valuation_selected_power_product) + (ff_r_kmcvznd_valuation_selected_power_product))) /\ ((((exists ff_h_kmcvznd_valuation_selected_power_product_successor. ff_h_kmcvznd_valuation_selected_power_product_successor + S (ff_s_kmcvznd_valuation_selected_power_product) = S ((S (S ff_i_kmcvznd_valuation_selected_power_product)) * ff_v_kmcvznd_valuation_selected_power_product)) /\ exists ff_q_kmcvznd_valuation_selected_power_product_successor. ff_u_kmcvznd_valuation_selected_power_product = ff_q_kmcvznd_valuation_selected_power_product_successor * S ((S (S ff_i_kmcvznd_valuation_selected_power_product)) * ff_v_kmcvznd_valuation_selected_power_product) + (ff_s_kmcvznd_valuation_selected_power_product))) /\ ff_s_kmcvznd_valuation_selected_power_product = ff_r_kmcvznd_valuation_selected_power_product * ff_p_kmcvznd_valuation_selected_power_product)))))))) /\ (exists bpv_factor_kmcvznd_valuation_selected_divides. c = bpv_result_kmcvznd_valuation_selected * bpv_factor_kmcvznd_valuation_selected_divides)))) /\ forall bpv_candidate_kmcvznd_valuation. (exists bpv_gap_kmcvznd_valuation_candidate_bound. bpv_gap_kmcvznd_valuation_candidate_bound + bpv_candidate_kmcvznd_valuation = c) -> (exists bpv_result_kmcvznd_valuation_candidate. ((exists ff_b_kmcvznd_valuation_candidate_power ff_c_kmcvznd_valuation_candidate_power. ((forall ff_i_kmcvznd_valuation_candidate_power_repeat. (exists ff_lt_kmcvznd_valuation_candidate_power_repeat_bound. ff_lt_kmcvznd_valuation_candidate_power_repeat_bound + S ff_i_kmcvznd_valuation_candidate_power_repeat = bpv_candidate_kmcvznd_valuation) -> (((exists ff_h_kmcvznd_valuation_candidate_power_repeat_decoded. ff_h_kmcvznd_valuation_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_kmcvznd_valuation_candidate_power_repeat)) * ff_c_kmcvznd_valuation_candidate_power)) /\ exists ff_q_kmcvznd_valuation_candidate_power_repeat_decoded. ff_b_kmcvznd_valuation_candidate_power = ff_q_kmcvznd_valuation_candidate_power_repeat_decoded * S ((S (ff_i_kmcvznd_valuation_candidate_power_repeat)) * ff_c_kmcvznd_valuation_candidate_power) + (p)))) /\ (exists ff_u_kmcvznd_valuation_candidate_power_product ff_v_kmcvznd_valuation_candidate_power_product. ((((exists ff_h_kmcvznd_valuation_candidate_power_product_start. ff_h_kmcvznd_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_kmcvznd_valuation_candidate_power_product)) /\ exists ff_q_kmcvznd_valuation_candidate_power_product_start. ff_u_kmcvznd_valuation_candidate_power_product = ff_q_kmcvznd_valuation_candidate_power_product_start * S ((S (0)) * ff_v_kmcvznd_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_kmcvznd_valuation_candidate_power_product_terminal. ff_h_kmcvznd_valuation_candidate_power_product_terminal + S (bpv_result_kmcvznd_valuation_candidate) = S ((S (bpv_candidate_kmcvznd_valuation)) * ff_v_kmcvznd_valuation_candidate_power_product)) /\ exists ff_q_kmcvznd_valuation_candidate_power_product_terminal. ff_u_kmcvznd_valuation_candidate_power_product = ff_q_kmcvznd_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_kmcvznd_valuation)) * ff_v_kmcvznd_valuation_candidate_power_product) + (bpv_result_kmcvznd_valuation_candidate))) /\ forall ff_i_kmcvznd_valuation_candidate_power_product. (exists ff_lt_kmcvznd_valuation_candidate_power_product_bound. ff_lt_kmcvznd_valuation_candidate_power_product_bound + S ff_i_kmcvznd_valuation_candidate_power_product = bpv_candidate_kmcvznd_valuation) -> exists ff_p_kmcvznd_valuation_candidate_power_product ff_r_kmcvznd_valuation_candidate_power_product ff_s_kmcvznd_valuation_candidate_power_product. ((((exists ff_h_kmcvznd_valuation_candidate_power_product_factor. ff_h_kmcvznd_valuation_candidate_power_product_factor + S (ff_p_kmcvznd_valuation_candidate_power_product) = S ((S (ff_i_kmcvznd_valuation_candidate_power_product)) * ff_c_kmcvznd_valuation_candidate_power)) /\ exists ff_q_kmcvznd_valuation_candidate_power_product_factor. ff_b_kmcvznd_valuation_candidate_power = ff_q_kmcvznd_valuation_candidate_power_product_factor * S ((S (ff_i_kmcvznd_valuation_candidate_power_product)) * ff_c_kmcvznd_valuation_candidate_power) + (ff_p_kmcvznd_valuation_candidate_power_product))) /\ ((((exists ff_h_kmcvznd_valuation_candidate_power_product_partial. ff_h_kmcvznd_valuation_candidate_power_product_partial + S (ff_r_kmcvznd_valuation_candidate_power_product) = S ((S (ff_i_kmcvznd_valuation_candidate_power_product)) * ff_v_kmcvznd_valuation_candidate_power_product)) /\ exists ff_q_kmcvznd_valuation_candidate_power_product_partial. ff_u_kmcvznd_valuation_candidate_power_product = ff_q_kmcvznd_valuation_candidate_power_product_partial * S ((S (ff_i_kmcvznd_valuation_candidate_power_product)) * ff_v_kmcvznd_valuation_candidate_power_product) + (ff_r_kmcvznd_valuation_candidate_power_product))) /\ ((((exists ff_h_kmcvznd_valuation_candidate_power_product_successor. ff_h_kmcvznd_valuation_candidate_power_product_successor + S (ff_s_kmcvznd_valuation_candidate_power_product) = S ((S (S ff_i_kmcvznd_valuation_candidate_power_product)) * ff_v_kmcvznd_valuation_candidate_power_product)) /\ exists ff_q_kmcvznd_valuation_candidate_power_product_successor. ff_u_kmcvznd_valuation_candidate_power_product = ff_q_kmcvznd_valuation_candidate_power_product_successor * S ((S (S ff_i_kmcvznd_valuation_candidate_power_product)) * ff_v_kmcvznd_valuation_candidate_power_product) + (ff_s_kmcvznd_valuation_candidate_power_product))) /\ ff_s_kmcvznd_valuation_candidate_power_product = ff_r_kmcvznd_valuation_candidate_power_product * ff_p_kmcvznd_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_kmcvznd_valuation_candidate_divides. c = bpv_result_kmcvznd_valuation_candidate * bpv_factor_kmcvznd_valuation_candidate_divides))) -> (exists bpv_gap_kmcvznd_valuation_maximal. bpv_gap_kmcvznd_valuation_maximal + bpv_candidate_kmcvznd_valuation = e)) -> ((e = 0 -> ~(exists bpv_factor_kmcvznd_divides. c = p * bpv_factor_kmcvznd_divides)) /\ (~(exists bpv_factor_kmcvznd_divides. c = p * bpv_factor_kmcvznd_divides) -> e = 0))

Proof neighborhood

Direct theorem prerequisites

prime_divisor_power_valuation_nonzero · Alpha closed power_valuation_nonzero_exponent_divides_base · Alpha closed eq_decidable · Stable closed

Direct theorem dependents

KU000E kummer_carry_free_iff_not_divides

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

31 script commands · 10 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.

01Fix variables and assumptionsL1–6

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

  1. L1
    intro p
  2. L2
    intro c
  3. L3
    intro e
  4. L4
    intro hp
  5. L5
    intro hc
  6. L6
    intro hvaluation
02Separate the logical casesL7–7

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

  1. L7
    split
03Fix variables and assumptionsL8–9

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

  1. L8
    intro hzero
  2. L9
    intro hdivides
04Use earlier factsL10–18

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

  1. L10
    specialize prime_divisor_power_valuation_nonzero p
  2. L11
    specialize prime_divisor_power_valuation_nonzero c
  3. L12
    specialize prime_divisor_power_valuation_nonzero e
  4. L13
    apply prime_divisor_power_valuation_nonzero
  5. L14
    exact hp
  6. L15
    exact hc
  7. L16
    exact hvaluation
  8. L17
    exact hdivides
  9. L18
    exact hzero
05Fix variables and assumptionsL19–19

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

  1. L19
    intro hnotdivides
06Use earlier factsL20–21

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

  1. L20
    specialize eq_decidable e
  2. L21
    specialize eq_decidable 0
07Separate the logical casesL22–22

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

  1. L22
    cases eq_decidable
08Use earlier factsL23–23

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

  1. L23
    exact eq_decidable_left
09Separate the logical casesL24–24

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

  1. L24
    exfalso
10Use earlier factsL25–31

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

  1. L25
    apply hnotdivides
  2. L26
    specialize power_valuation_nonzero_exponent_divides_base p
  3. L27
    specialize power_valuation_nonzero_exponent_divides_base c
  4. L28
    specialize power_valuation_nonzero_exponent_divides_base e
  5. L29
    apply power_valuation_nonzero_exponent_divides_base
  6. L30
    exact hvaluation
  7. L31
    exact eq_decidable_right

Library-wide reading audit

Original defined command ledger · 31 lines
  1. 0001intro p
  2. 0002intro c
  3. 0003intro e
  4. 0004intro hp
  5. 0005intro hc
  6. 0006intro hvaluation
  7. 0007split
  8. 0008intro hzero
  9. 0009intro hdivides
  10. 0010specialize prime_divisor_power_valuation_nonzero p
  11. 0011specialize prime_divisor_power_valuation_nonzero c
  12. 0012specialize prime_divisor_power_valuation_nonzero e
  13. 0013apply prime_divisor_power_valuation_nonzero
  14. 0014exact hp
  15. 0015exact hc
  16. 0016exact hvaluation
  17. 0017exact hdivides
  18. 0018exact hzero
  19. 0019intro hnotdivides
  20. 0020specialize eq_decidable e
  21. 0021specialize eq_decidable 0
  22. 0022cases eq_decidable
  23. 0023exact eq_decidable_left
  24. 0024exfalso
  25. 0025apply hnotdivides
  26. 0026specialize power_valuation_nonzero_exponent_divides_base p
  27. 0027specialize power_valuation_nonzero_exponent_divides_base c
  28. 0028specialize power_valuation_nonzero_exponent_divides_base e
  29. 0029apply power_valuation_nonzero_exponent_divides_base
  30. 0030exact hvaluation
  31. 0031exact eq_decidable_right