BT0101 · Bertrand theorem

prime_contribution_selected_successor_divides

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

A prime in the remaining cofactor raises a selected 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.

Statement with defined notation

∀ p. ∀ e. ∀ a. ∀ z. ∀ q. ∀ n. Pow(p,e,a) → Dvd(a,z) → Dvd(p,q) → n = z · q → PowerDivides(p,S e,n)

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

PD0003 Dvd PD0020 Pow PD0044 PowerDivides

4 occurrences

In local proof propositions

PD0003 Dvd

1 occurrences

Exact expanded native-PA statement
forall p e a z q n. (exists bpr_power_code_bpcssd_power bpr_power_scale_bpcssd_power. ((forall bpr_power_index_bpcssd_power. (exists bpr_gap_bpcssd_power_repeat_bound. bpr_gap_bpcssd_power_repeat_bound + S (bpr_power_index_bpcssd_power) = e) -> (((exists bpr_height_bpcssd_power_repeat_entry. bpr_height_bpcssd_power_repeat_entry + S (p) = S ((S (bpr_power_index_bpcssd_power)) * bpr_power_scale_bpcssd_power)) /\ exists bpr_quotient_bpcssd_power_repeat_entry. bpr_power_code_bpcssd_power = bpr_quotient_bpcssd_power_repeat_entry * S ((S (bpr_power_index_bpcssd_power)) * bpr_power_scale_bpcssd_power) + (p)))) /\ (exists ff_u_bpcssd_power_product ff_v_bpcssd_power_product. ((((exists ff_h_bpcssd_power_product_start. ff_h_bpcssd_power_product_start + S (1) = S ((S (0)) * ff_v_bpcssd_power_product)) /\ exists ff_q_bpcssd_power_product_start. ff_u_bpcssd_power_product = ff_q_bpcssd_power_product_start * S ((S (0)) * ff_v_bpcssd_power_product) + (1))) /\ ((((exists ff_h_bpcssd_power_product_terminal. ff_h_bpcssd_power_product_terminal + S (a) = S ((S (e)) * ff_v_bpcssd_power_product)) /\ exists ff_q_bpcssd_power_product_terminal. ff_u_bpcssd_power_product = ff_q_bpcssd_power_product_terminal * S ((S (e)) * ff_v_bpcssd_power_product) + (a))) /\ forall ff_i_bpcssd_power_product. (exists ff_lt_bpcssd_power_product_bound. ff_lt_bpcssd_power_product_bound + S ff_i_bpcssd_power_product = e) -> exists ff_p_bpcssd_power_product ff_r_bpcssd_power_product ff_s_bpcssd_power_product. ((((exists ff_h_bpcssd_power_product_factor. ff_h_bpcssd_power_product_factor + S (ff_p_bpcssd_power_product) = S ((S (ff_i_bpcssd_power_product)) * bpr_power_scale_bpcssd_power)) /\ exists ff_q_bpcssd_power_product_factor. bpr_power_code_bpcssd_power = ff_q_bpcssd_power_product_factor * S ((S (ff_i_bpcssd_power_product)) * bpr_power_scale_bpcssd_power) + (ff_p_bpcssd_power_product))) /\ ((((exists ff_h_bpcssd_power_product_partial. ff_h_bpcssd_power_product_partial + S (ff_r_bpcssd_power_product) = S ((S (ff_i_bpcssd_power_product)) * ff_v_bpcssd_power_product)) /\ exists ff_q_bpcssd_power_product_partial. ff_u_bpcssd_power_product = ff_q_bpcssd_power_product_partial * S ((S (ff_i_bpcssd_power_product)) * ff_v_bpcssd_power_product) + (ff_r_bpcssd_power_product))) /\ ((((exists ff_h_bpcssd_power_product_successor. ff_h_bpcssd_power_product_successor + S (ff_s_bpcssd_power_product) = S ((S (S ff_i_bpcssd_power_product)) * ff_v_bpcssd_power_product)) /\ exists ff_q_bpcssd_power_product_successor. ff_u_bpcssd_power_product = ff_q_bpcssd_power_product_successor * S ((S (S ff_i_bpcssd_power_product)) * ff_v_bpcssd_power_product) + (ff_s_bpcssd_power_product))) /\ ff_s_bpcssd_power_product = ff_r_bpcssd_power_product * ff_p_bpcssd_power_product)))))))) -> (exists bpr_divides_quotient_bpcssd_factor. z = (a) * bpr_divides_quotient_bpcssd_factor) -> (exists bpr_divides_quotient_bpcssd_prime_factor. q = (p) * bpr_divides_quotient_bpcssd_prime_factor) -> n = z * q -> (exists bpr_power_value_bpcssd_result. ((exists bpr_power_code_bpcssd_result_power bpr_power_scale_bpcssd_result_power. ((forall bpr_power_index_bpcssd_result_power. (exists bpr_gap_bpcssd_result_power_repeat_bound. bpr_gap_bpcssd_result_power_repeat_bound + S (bpr_power_index_bpcssd_result_power) = S e) -> (((exists bpr_height_bpcssd_result_power_repeat_entry. bpr_height_bpcssd_result_power_repeat_entry + S (p) = S ((S (bpr_power_index_bpcssd_result_power)) * bpr_power_scale_bpcssd_result_power)) /\ exists bpr_quotient_bpcssd_result_power_repeat_entry. bpr_power_code_bpcssd_result_power = bpr_quotient_bpcssd_result_power_repeat_entry * S ((S (bpr_power_index_bpcssd_result_power)) * bpr_power_scale_bpcssd_result_power) + (p)))) /\ (exists ff_u_bpcssd_result_power_product ff_v_bpcssd_result_power_product. ((((exists ff_h_bpcssd_result_power_product_start. ff_h_bpcssd_result_power_product_start + S (1) = S ((S (0)) * ff_v_bpcssd_result_power_product)) /\ exists ff_q_bpcssd_result_power_product_start. ff_u_bpcssd_result_power_product = ff_q_bpcssd_result_power_product_start * S ((S (0)) * ff_v_bpcssd_result_power_product) + (1))) /\ ((((exists ff_h_bpcssd_result_power_product_terminal. ff_h_bpcssd_result_power_product_terminal + S (bpr_power_value_bpcssd_result) = S ((S (S e)) * ff_v_bpcssd_result_power_product)) /\ exists ff_q_bpcssd_result_power_product_terminal. ff_u_bpcssd_result_power_product = ff_q_bpcssd_result_power_product_terminal * S ((S (S e)) * ff_v_bpcssd_result_power_product) + (bpr_power_value_bpcssd_result))) /\ forall ff_i_bpcssd_result_power_product. (exists ff_lt_bpcssd_result_power_product_bound. ff_lt_bpcssd_result_power_product_bound + S ff_i_bpcssd_result_power_product = S e) -> exists ff_p_bpcssd_result_power_product ff_r_bpcssd_result_power_product ff_s_bpcssd_result_power_product. ((((exists ff_h_bpcssd_result_power_product_factor. ff_h_bpcssd_result_power_product_factor + S (ff_p_bpcssd_result_power_product) = S ((S (ff_i_bpcssd_result_power_product)) * bpr_power_scale_bpcssd_result_power)) /\ exists ff_q_bpcssd_result_power_product_factor. bpr_power_code_bpcssd_result_power = ff_q_bpcssd_result_power_product_factor * S ((S (ff_i_bpcssd_result_power_product)) * bpr_power_scale_bpcssd_result_power) + (ff_p_bpcssd_result_power_product))) /\ ((((exists ff_h_bpcssd_result_power_product_partial. ff_h_bpcssd_result_power_product_partial + S (ff_r_bpcssd_result_power_product) = S ((S (ff_i_bpcssd_result_power_product)) * ff_v_bpcssd_result_power_product)) /\ exists ff_q_bpcssd_result_power_product_partial. ff_u_bpcssd_result_power_product = ff_q_bpcssd_result_power_product_partial * S ((S (ff_i_bpcssd_result_power_product)) * ff_v_bpcssd_result_power_product) + (ff_r_bpcssd_result_power_product))) /\ ((((exists ff_h_bpcssd_result_power_product_successor. ff_h_bpcssd_result_power_product_successor + S (ff_s_bpcssd_result_power_product) = S ((S (S ff_i_bpcssd_result_power_product)) * ff_v_bpcssd_result_power_product)) /\ exists ff_q_bpcssd_result_power_product_successor. ff_u_bpcssd_result_power_product = ff_q_bpcssd_result_power_product_successor * S ((S (S ff_i_bpcssd_result_power_product)) * ff_v_bpcssd_result_power_product) + (ff_s_bpcssd_result_power_product))) /\ ff_s_bpcssd_result_power_product = ff_r_bpcssd_result_power_product * ff_p_bpcssd_result_power_product)))))))) /\ (exists bpr_divides_quotient_bpcssd_result_divides. n = (bpr_power_value_bpcssd_result) * bpr_divides_quotient_bpcssd_result_divides)))

Proof neighborhood

Direct theorem prerequisites

BT0008 mul_assoc BT002B multiple_mul_left BT00QM power_divides_successor_of_cofactor

Direct theorem dependents

BT0102 prime_contribution_cofactor_prime_contradiction

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

31 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)
mul assocmultiple mul leftpower divides successor of cofactor
01Fix variables and assumptionsL1–10

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 z
  5. L5
    intro q
  6. L6
    intro n
  7. L7
    intro hpower
  8. L8
    intro hfactor
  9. L9
    intro hprime
  10. L10
    intro htotal
02Separate the logical casesL11–11

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

  1. L11
    cases hfactor
03Establish hcofactorL12–17

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply multiple mul left.

  1. L12
    have hcofactor : Dvd(p,x · q)Definitions: Dvd(p,x · q)Original native command in the exact edition
  2. L13
    specialize multiple_mul_left p
  3. L14
    specialize multiple_mul_left q
  4. L15
    specialize multiple_mul_left x
  5. L16
    apply multiple_mul_left
  6. L17
    exact hprime
04Establish halignedL18–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul assoc.

  1. L18
    have haligned : n = a * (x * q)
  2. L19
    trans z * q
  3. L20
    exact htotal
  4. L21
    rewrite hfactor_witness
  5. L22
    apply mul_assoc
  6. L23
    specialize power_divides_successor_of_cofactor p
  7. L24
    specialize power_divides_successor_of_cofactor e
  8. L25
    specialize power_divides_successor_of_cofactor n
  9. L26
    specialize power_divides_successor_of_cofactor a
  10. L27
    specialize power_divides_successor_of_cofactor (x * q)
05Use earlier factsL28–31

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

  1. L28
    apply power_divides_successor_of_cofactor
  2. L29
    exact hpower
  3. L30
    exact haligned
  4. L31
    exact hcofactor

Library-wide reading audit

Original defined command ledger · 31 lines
  1. 0001intro p
  2. 0002intro e
  3. 0003intro a
  4. 0004intro z
  5. 0005intro q
  6. 0006intro n
  7. 0007intro hpower
  8. 0008intro hfactor
  9. 0009intro hprime
  10. 0010intro htotal
  11. 0011cases hfactor
  12. 0012have hcofactor : Dvd(p,x · q)
    Exact native replay linehave hcofactor : exists bpr_divides_quotient_bpcssd_cofactor. x * q = (p) * bpr_divides_quotient_bpcssd_cofactor
  13. 0013specialize multiple_mul_left p
  14. 0014specialize multiple_mul_left q
  15. 0015specialize multiple_mul_left x
  16. 0016apply multiple_mul_left
  17. 0017exact hprime
  18. 0018have haligned : n = a * (x * q)
  19. 0019trans z * q
  20. 0020exact htotal
  21. 0021rewrite hfactor_witness
  22. 0022apply mul_assoc
  23. 0023specialize power_divides_successor_of_cofactor p
  24. 0024specialize power_divides_successor_of_cofactor e
  25. 0025specialize power_divides_successor_of_cofactor n
  26. 0026specialize power_divides_successor_of_cofactor a
  27. 0027specialize power_divides_successor_of_cofactor (x * q)
  28. 0028apply power_divides_successor_of_cofactor
  29. 0029exact hpower
  30. 0030exact haligned
  31. 0031exact hcofactor