BT00QG · Bertrand theorem

prime_power_divides_exponent_le_value

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

A dividing prime power has exponent at most the nonzero dividend.

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

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0001 Le PD0004 Prime PD0044 PowerDivides

3 occurrences

In local proof propositions

PD0001 Le

2 occurrences

Exact expanded native-PA statement
forall p e a. ((~(p = 1) /\ forall frm_prime_left_bpvl_prime frm_prime_right_bpvl_prime. p = frm_prime_left_bpvl_prime * frm_prime_right_bpvl_prime -> frm_prime_left_bpvl_prime = 1 \/ frm_prime_right_bpvl_prime = 1)) -> ~(a = 0) -> (exists bpv_result_bpvl_bound_divides. ((exists ff_b_bpvl_bound_divides_power ff_c_bpvl_bound_divides_power. ((forall ff_i_bpvl_bound_divides_power_repeat. (exists ff_lt_bpvl_bound_divides_power_repeat_bound. ff_lt_bpvl_bound_divides_power_repeat_bound + S ff_i_bpvl_bound_divides_power_repeat = e) -> (((exists ff_h_bpvl_bound_divides_power_repeat_decoded. ff_h_bpvl_bound_divides_power_repeat_decoded + S (p) = S ((S (ff_i_bpvl_bound_divides_power_repeat)) * ff_c_bpvl_bound_divides_power)) /\ exists ff_q_bpvl_bound_divides_power_repeat_decoded. ff_b_bpvl_bound_divides_power = ff_q_bpvl_bound_divides_power_repeat_decoded * S ((S (ff_i_bpvl_bound_divides_power_repeat)) * ff_c_bpvl_bound_divides_power) + (p)))) /\ (exists ff_u_bpvl_bound_divides_power_product ff_v_bpvl_bound_divides_power_product. ((((exists ff_h_bpvl_bound_divides_power_product_start. ff_h_bpvl_bound_divides_power_product_start + S (1) = S ((S (0)) * ff_v_bpvl_bound_divides_power_product)) /\ exists ff_q_bpvl_bound_divides_power_product_start. ff_u_bpvl_bound_divides_power_product = ff_q_bpvl_bound_divides_power_product_start * S ((S (0)) * ff_v_bpvl_bound_divides_power_product) + (1))) /\ ((((exists ff_h_bpvl_bound_divides_power_product_terminal. ff_h_bpvl_bound_divides_power_product_terminal + S (bpv_result_bpvl_bound_divides) = S ((S (e)) * ff_v_bpvl_bound_divides_power_product)) /\ exists ff_q_bpvl_bound_divides_power_product_terminal. ff_u_bpvl_bound_divides_power_product = ff_q_bpvl_bound_divides_power_product_terminal * S ((S (e)) * ff_v_bpvl_bound_divides_power_product) + (bpv_result_bpvl_bound_divides))) /\ forall ff_i_bpvl_bound_divides_power_product. (exists ff_lt_bpvl_bound_divides_power_product_bound. ff_lt_bpvl_bound_divides_power_product_bound + S ff_i_bpvl_bound_divides_power_product = e) -> exists ff_p_bpvl_bound_divides_power_product ff_r_bpvl_bound_divides_power_product ff_s_bpvl_bound_divides_power_product. ((((exists ff_h_bpvl_bound_divides_power_product_factor. ff_h_bpvl_bound_divides_power_product_factor + S (ff_p_bpvl_bound_divides_power_product) = S ((S (ff_i_bpvl_bound_divides_power_product)) * ff_c_bpvl_bound_divides_power)) /\ exists ff_q_bpvl_bound_divides_power_product_factor. ff_b_bpvl_bound_divides_power = ff_q_bpvl_bound_divides_power_product_factor * S ((S (ff_i_bpvl_bound_divides_power_product)) * ff_c_bpvl_bound_divides_power) + (ff_p_bpvl_bound_divides_power_product))) /\ ((((exists ff_h_bpvl_bound_divides_power_product_partial. ff_h_bpvl_bound_divides_power_product_partial + S (ff_r_bpvl_bound_divides_power_product) = S ((S (ff_i_bpvl_bound_divides_power_product)) * ff_v_bpvl_bound_divides_power_product)) /\ exists ff_q_bpvl_bound_divides_power_product_partial. ff_u_bpvl_bound_divides_power_product = ff_q_bpvl_bound_divides_power_product_partial * S ((S (ff_i_bpvl_bound_divides_power_product)) * ff_v_bpvl_bound_divides_power_product) + (ff_r_bpvl_bound_divides_power_product))) /\ ((((exists ff_h_bpvl_bound_divides_power_product_successor. ff_h_bpvl_bound_divides_power_product_successor + S (ff_s_bpvl_bound_divides_power_product) = S ((S (S ff_i_bpvl_bound_divides_power_product)) * ff_v_bpvl_bound_divides_power_product)) /\ exists ff_q_bpvl_bound_divides_power_product_successor. ff_u_bpvl_bound_divides_power_product = ff_q_bpvl_bound_divides_power_product_successor * S ((S (S ff_i_bpvl_bound_divides_power_product)) * ff_v_bpvl_bound_divides_power_product) + (ff_s_bpvl_bound_divides_power_product))) /\ ff_s_bpvl_bound_divides_power_product = ff_r_bpvl_bound_divides_power_product * ff_p_bpvl_bound_divides_power_product)))))))) /\ (exists bpv_factor_bpvl_bound_divides_divides. a = bpv_result_bpvl_bound_divides * bpv_factor_bpvl_bound_divides_divides))) -> (exists bpv_gap_divides_exponent_value. bpv_gap_divides_exponent_value + e = a)

Proof neighborhood

Direct theorem prerequisites

BT00QF prime_power_exponent_le BT002D divisor_le_nonzero BT000F le_trans

Direct theorem dependents

BT00QH power_valuation_successor_not_divides BT00QR power_valuation_mul_lower BT00SB prime_power_divides_exponent_le_valuation

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

27 script commands · 5 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 (3)
prime power exponent ledivisor le nonzerole trans
01Fix variables and assumptionsL1–6

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

  1. L1
    intro p
  2. L2
    intro e
  3. L3
    intro a
  4. L4
    intro hp
  5. L5
    intro ha
  6. L6
    intro hdivides
02Separate the logical casesL7–8

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

  1. L7
    cases hdivides
  2. L8
    cases hdivides_witness
03Establish hexponentL9–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime power exponent le.

  1. L9
    have hexponent : Le(e,x)Definitions: Le(e,x)Original native command in the exact edition
  2. L10
    specialize prime_power_exponent_le p
  3. L11
    specialize prime_power_exponent_le e
  4. L12
    specialize prime_power_exponent_le x
  5. L13
    apply prime_power_exponent_le
  6. L14
    exact hp
  7. L15
    exact hdivides_witness_left
04Establish hpower_valueL16–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor le nonzero.

  1. L16
    have hpower_value : Le(x,a)Definitions: Le(x,a)Original native command in the exact edition
  2. L17
    specialize divisor_le_nonzero x
  3. L18
    specialize divisor_le_nonzero a
  4. L19
    apply divisor_le_nonzero
  5. L20
    exact ha
  6. L21
    exact hdivides_witness_right
  7. L22
    specialize le_trans e
  8. L23
    specialize le_trans x
  9. L24
    specialize le_trans a
  10. L25
    apply le_trans
05Use earlier factsL26–27

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

  1. L26
    exact hexponent
  2. L27
    exact hpower_value

Library-wide reading audit

Original defined command ledger · 27 lines
  1. 0001intro p
  2. 0002intro e
  3. 0003intro a
  4. 0004intro hp
  5. 0005intro ha
  6. 0006intro hdivides
  7. 0007cases hdivides
  8. 0008cases hdivides_witness
  9. 0009have hexponent : Le(e,x)
    Exact native replay linehave hexponent : exists k. k + e = x
  10. 0010specialize prime_power_exponent_le p
  11. 0011specialize prime_power_exponent_le e
  12. 0012specialize prime_power_exponent_le x
  13. 0013apply prime_power_exponent_le
  14. 0014exact hp
  15. 0015exact hdivides_witness_left
  16. 0016have hpower_value : Le(x,a)
    Exact native replay linehave hpower_value : exists k. k + x = a
  17. 0017specialize divisor_le_nonzero x
  18. 0018specialize divisor_le_nonzero a
  19. 0019apply divisor_le_nonzero
  20. 0020exact ha
  21. 0021exact hdivides_witness_right
  22. 0022specialize le_trans e
  23. 0023specialize le_trans x
  24. 0024specialize le_trans a
  25. 0025apply le_trans
  26. 0026exact hexponent
  27. 0027exact hpower_value