BT00QM · Bertrand theorem

power_divides_successor_of_cofactor

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

Divisibility of a power cofactor by its base raises the exponent by one.

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. ∀ r. ∀ q. Pow(p,e,r) → a = r · q → Dvd(p,q) → PowerDivides(p,S 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

PD0003 Dvd PD0020 Pow PD0044 PowerDivides

3 occurrences

In local proof propositions

PD0020 Pow

1 occurrences

Exact expanded native-PA statement
forall p e a r q. (exists ff_b_bpd_successor_prefix ff_c_bpd_successor_prefix. ((forall ff_i_bpd_successor_prefix_repeat. (exists ff_lt_bpd_successor_prefix_repeat_bound. ff_lt_bpd_successor_prefix_repeat_bound + S ff_i_bpd_successor_prefix_repeat = e) -> (((exists ff_h_bpd_successor_prefix_repeat_decoded. ff_h_bpd_successor_prefix_repeat_decoded + S (p) = S ((S (ff_i_bpd_successor_prefix_repeat)) * ff_c_bpd_successor_prefix)) /\ exists ff_q_bpd_successor_prefix_repeat_decoded. ff_b_bpd_successor_prefix = ff_q_bpd_successor_prefix_repeat_decoded * S ((S (ff_i_bpd_successor_prefix_repeat)) * ff_c_bpd_successor_prefix) + (p)))) /\ (exists ff_u_bpd_successor_prefix_product ff_v_bpd_successor_prefix_product. ((((exists ff_h_bpd_successor_prefix_product_start. ff_h_bpd_successor_prefix_product_start + S (1) = S ((S (0)) * ff_v_bpd_successor_prefix_product)) /\ exists ff_q_bpd_successor_prefix_product_start. ff_u_bpd_successor_prefix_product = ff_q_bpd_successor_prefix_product_start * S ((S (0)) * ff_v_bpd_successor_prefix_product) + (1))) /\ ((((exists ff_h_bpd_successor_prefix_product_terminal. ff_h_bpd_successor_prefix_product_terminal + S (r) = S ((S (e)) * ff_v_bpd_successor_prefix_product)) /\ exists ff_q_bpd_successor_prefix_product_terminal. ff_u_bpd_successor_prefix_product = ff_q_bpd_successor_prefix_product_terminal * S ((S (e)) * ff_v_bpd_successor_prefix_product) + (r))) /\ forall ff_i_bpd_successor_prefix_product. (exists ff_lt_bpd_successor_prefix_product_bound. ff_lt_bpd_successor_prefix_product_bound + S ff_i_bpd_successor_prefix_product = e) -> exists ff_p_bpd_successor_prefix_product ff_r_bpd_successor_prefix_product ff_s_bpd_successor_prefix_product. ((((exists ff_h_bpd_successor_prefix_product_factor. ff_h_bpd_successor_prefix_product_factor + S (ff_p_bpd_successor_prefix_product) = S ((S (ff_i_bpd_successor_prefix_product)) * ff_c_bpd_successor_prefix)) /\ exists ff_q_bpd_successor_prefix_product_factor. ff_b_bpd_successor_prefix = ff_q_bpd_successor_prefix_product_factor * S ((S (ff_i_bpd_successor_prefix_product)) * ff_c_bpd_successor_prefix) + (ff_p_bpd_successor_prefix_product))) /\ ((((exists ff_h_bpd_successor_prefix_product_partial. ff_h_bpd_successor_prefix_product_partial + S (ff_r_bpd_successor_prefix_product) = S ((S (ff_i_bpd_successor_prefix_product)) * ff_v_bpd_successor_prefix_product)) /\ exists ff_q_bpd_successor_prefix_product_partial. ff_u_bpd_successor_prefix_product = ff_q_bpd_successor_prefix_product_partial * S ((S (ff_i_bpd_successor_prefix_product)) * ff_v_bpd_successor_prefix_product) + (ff_r_bpd_successor_prefix_product))) /\ ((((exists ff_h_bpd_successor_prefix_product_successor. ff_h_bpd_successor_prefix_product_successor + S (ff_s_bpd_successor_prefix_product) = S ((S (S ff_i_bpd_successor_prefix_product)) * ff_v_bpd_successor_prefix_product)) /\ exists ff_q_bpd_successor_prefix_product_successor. ff_u_bpd_successor_prefix_product = ff_q_bpd_successor_prefix_product_successor * S ((S (S ff_i_bpd_successor_prefix_product)) * ff_v_bpd_successor_prefix_product) + (ff_s_bpd_successor_prefix_product))) /\ ff_s_bpd_successor_prefix_product = ff_r_bpd_successor_prefix_product * ff_p_bpd_successor_prefix_product)))))))) -> a = r * q -> (exists bpd_factor_successor_cofactor. q = (p) * bpd_factor_successor_cofactor) -> (exists bpvi_result_successor_result. ((exists bpvi_b_successor_result_power bpvi_c_successor_result_power. ((forall bpvi_i_successor_result_power. (exists bpvi_repeat_gap_successor_result_power. bpvi_repeat_gap_successor_result_power + S bpvi_i_successor_result_power = S e) -> (((exists bpvi_h_successor_result_power_repeat. bpvi_h_successor_result_power_repeat + S (p) = S ((S (bpvi_i_successor_result_power)) * bpvi_c_successor_result_power)) /\ exists bpvi_q_successor_result_power_repeat. bpvi_b_successor_result_power = bpvi_q_successor_result_power_repeat * S ((S (bpvi_i_successor_result_power)) * bpvi_c_successor_result_power) + (p)))) /\ (exists bpvi_u_successor_result_power bpvi_v_successor_result_power. ((((exists bpvi_h_successor_result_power_start. bpvi_h_successor_result_power_start + S (1) = S ((S (0)) * bpvi_v_successor_result_power)) /\ exists bpvi_q_successor_result_power_start. bpvi_u_successor_result_power = bpvi_q_successor_result_power_start * S ((S (0)) * bpvi_v_successor_result_power) + (1))) /\ ((((exists bpvi_h_successor_result_power_terminal. bpvi_h_successor_result_power_terminal + S (bpvi_result_successor_result) = S ((S (S e)) * bpvi_v_successor_result_power)) /\ exists bpvi_q_successor_result_power_terminal. bpvi_u_successor_result_power = bpvi_q_successor_result_power_terminal * S ((S (S e)) * bpvi_v_successor_result_power) + (bpvi_result_successor_result))) /\ forall bpvi_j_successor_result_power. (exists bpvi_product_gap_successor_result_power. bpvi_product_gap_successor_result_power + S bpvi_j_successor_result_power = S e) -> exists bpvi_factor_successor_result_power bpvi_partial_successor_result_power bpvi_successor_successor_result_power. ((((exists bpvi_h_successor_result_power_factor. bpvi_h_successor_result_power_factor + S (bpvi_factor_successor_result_power) = S ((S (bpvi_j_successor_result_power)) * bpvi_c_successor_result_power)) /\ exists bpvi_q_successor_result_power_factor. bpvi_b_successor_result_power = bpvi_q_successor_result_power_factor * S ((S (bpvi_j_successor_result_power)) * bpvi_c_successor_result_power) + (bpvi_factor_successor_result_power))) /\ ((((exists bpvi_h_successor_result_power_partial. bpvi_h_successor_result_power_partial + S (bpvi_partial_successor_result_power) = S ((S (bpvi_j_successor_result_power)) * bpvi_v_successor_result_power)) /\ exists bpvi_q_successor_result_power_partial. bpvi_u_successor_result_power = bpvi_q_successor_result_power_partial * S ((S (bpvi_j_successor_result_power)) * bpvi_v_successor_result_power) + (bpvi_partial_successor_result_power))) /\ ((((exists bpvi_h_successor_result_power_successor. bpvi_h_successor_result_power_successor + S (bpvi_successor_successor_result_power) = S ((S (S bpvi_j_successor_result_power)) * bpvi_v_successor_result_power)) /\ exists bpvi_q_successor_result_power_successor. bpvi_u_successor_result_power = bpvi_q_successor_result_power_successor * S ((S (S bpvi_j_successor_result_power)) * bpvi_v_successor_result_power) + (bpvi_successor_successor_result_power))) /\ bpvi_successor_successor_result_power = bpvi_partial_successor_result_power * bpvi_factor_successor_result_power)))))))) /\ exists bpvi_divisor_factor_successor_result. a = bpvi_result_successor_result * bpvi_divisor_factor_successor_result))

Proof neighborhood

Direct theorem prerequisites

BT0080 pow_exists BT0095 pow_successor_pair_mul BT0008 mul_assoc

Direct theorem dependents

BT00QP power_valuation_exact_cofactor BT0101 prime_contribution_selected_successor_divides

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

38 script commands · 16 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)
pow existspow successor pair mulmul assoc
01Fix variables and assumptionsL1–8

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 r
  5. L5
    intro q
  6. L6
    intro hr
  7. L7
    intro ha
  8. L8
    intro hq
02Separate the logical casesL9–9

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

  1. L9
    cases hq
03Establish hsuccessorL10–13

Establish this local claim before using it. It is not an additional assumption.

  1. L10
    have hsuccessor : ∃ s. Pow(p,S e,s)Definitions: Pow(p,S e,s)Original native command in the exact edition
  2. L11
    specialize pow_exists p
  3. L12
    specialize pow_exists (S e)
  4. L13
    exact pow_exists
04Separate the logical casesL14–14

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

  1. L14
    cases hsuccessor
05Establish hsL15–24

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

  1. L15
    have hs : x1 = r * p
  2. L16
    specialize pow_successor_pair_mul p
  3. L17
    specialize pow_successor_pair_mul e
  4. L18
    specialize pow_successor_pair_mul (S e)
  5. L19
    specialize pow_successor_pair_mul r
  6. L20
    specialize pow_successor_pair_mul x1
  7. L21
    apply pow_successor_pair_mul
  8. L22
    refl
  9. L23
    exact hr
  10. L24
    exact hsuccessor_witness
06Construct an explicit witnessL25–25

Supply the displayed value, then prove that it has the required property.

  1. L25
    exists x1
07Separate the logical casesL26–26

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

  1. L26
    split
08Use earlier factsL27–27

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

  1. L27
    exact hsuccessor_witness
09Construct an explicit witnessL28–28

Supply the displayed value, then prove that it has the required property.

  1. L28
    exists x
10Calculate and transport equalitiesL29–29

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L29
    trans r * q
11Use earlier factsL30–30

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

  1. L30
    exact ha
12Calculate and transport equalitiesL31–33

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L31
    rewrite hq_witness
  2. L32
    trans (r * p) * x
  3. L33
    symm
13Use earlier factsL34–34

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

  1. L34
    apply mul_assoc
14Calculate and transport equalitiesL35–36

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L35
    congr
  2. L36
    symm
15Use earlier factsL37–37

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

  1. L37
    exact hs
16Calculate and transport equalitiesL38–38

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L38
    refl

Library-wide reading audit

Original defined command ledger · 38 lines
  1. 0001intro p
  2. 0002intro e
  3. 0003intro a
  4. 0004intro r
  5. 0005intro q
  6. 0006intro hr
  7. 0007intro ha
  8. 0008intro hq
  9. 0009cases hq
  10. 0010have hsuccessor : ∃ s. Pow(p,S e,s)
    Exact native replay linehave hsuccessor : exists s. (exists bpvi_b_bpd_successor_witness bpvi_c_bpd_successor_witness. ((forall bpvi_i_bpd_successor_witness. (exists bpvi_repeat_gap_bpd_successor_witness. bpvi_repeat_gap_bpd_successor_witness + S bpvi_i_bpd_successor_witness = S e) -> (((exists bpvi_h_bpd_successor_witness_repeat. bpvi_h_bpd_successor_witness_repeat + S (p) = S ((S (bpvi_i_bpd_successor_witness)) * bpvi_c_bpd_successor_witness)) /\ exists bpvi_q_bpd_successor_witness_repeat. bpvi_b_bpd_successor_witness = bpvi_q_bpd_successor_witness_repeat * S ((S (bpvi_i_bpd_successor_witness)) * bpvi_c_bpd_successor_witness) + (p)))) /\ (exists bpvi_u_bpd_successor_witness bpvi_v_bpd_successor_witness. ((((exists bpvi_h_bpd_successor_witness_start. bpvi_h_bpd_successor_witness_start + S (1) = S ((S (0)) * bpvi_v_bpd_successor_witness)) /\ exists bpvi_q_bpd_successor_witness_start. bpvi_u_bpd_successor_witness = bpvi_q_bpd_successor_witness_start * S ((S (0)) * bpvi_v_bpd_successor_witness) + (1))) /\ ((((exists bpvi_h_bpd_successor_witness_terminal. bpvi_h_bpd_successor_witness_terminal + S (s) = S ((S (S e)) * bpvi_v_bpd_successor_witness)) /\ exists bpvi_q_bpd_successor_witness_terminal. bpvi_u_bpd_successor_witness = bpvi_q_bpd_successor_witness_terminal * S ((S (S e)) * bpvi_v_bpd_successor_witness) + (s))) /\ forall bpvi_j_bpd_successor_witness. (exists bpvi_product_gap_bpd_successor_witness. bpvi_product_gap_bpd_successor_witness + S bpvi_j_bpd_successor_witness = S e) -> exists bpvi_factor_bpd_successor_witness bpvi_partial_bpd_successor_witness bpvi_successor_bpd_successor_witness. ((((exists bpvi_h_bpd_successor_witness_factor. bpvi_h_bpd_successor_witness_factor + S (bpvi_factor_bpd_successor_witness) = S ((S (bpvi_j_bpd_successor_witness)) * bpvi_c_bpd_successor_witness)) /\ exists bpvi_q_bpd_successor_witness_factor. bpvi_b_bpd_successor_witness = bpvi_q_bpd_successor_witness_factor * S ((S (bpvi_j_bpd_successor_witness)) * bpvi_c_bpd_successor_witness) + (bpvi_factor_bpd_successor_witness))) /\ ((((exists bpvi_h_bpd_successor_witness_partial. bpvi_h_bpd_successor_witness_partial + S (bpvi_partial_bpd_successor_witness) = S ((S (bpvi_j_bpd_successor_witness)) * bpvi_v_bpd_successor_witness)) /\ exists bpvi_q_bpd_successor_witness_partial. bpvi_u_bpd_successor_witness = bpvi_q_bpd_successor_witness_partial * S ((S (bpvi_j_bpd_successor_witness)) * bpvi_v_bpd_successor_witness) + (bpvi_partial_bpd_successor_witness))) /\ ((((exists bpvi_h_bpd_successor_witness_successor. bpvi_h_bpd_successor_witness_successor + S (bpvi_successor_bpd_successor_witness) = S ((S (S bpvi_j_bpd_successor_witness)) * bpvi_v_bpd_successor_witness)) /\ exists bpvi_q_bpd_successor_witness_successor. bpvi_u_bpd_successor_witness = bpvi_q_bpd_successor_witness_successor * S ((S (S bpvi_j_bpd_successor_witness)) * bpvi_v_bpd_successor_witness) + (bpvi_successor_bpd_successor_witness))) /\ bpvi_successor_bpd_successor_witness = bpvi_partial_bpd_successor_witness * bpvi_factor_bpd_successor_witness))))))))
  11. 0011specialize pow_exists p
  12. 0012specialize pow_exists (S e)
  13. 0013exact pow_exists
  14. 0014cases hsuccessor
  15. 0015have hs : x1 = r * p
  16. 0016specialize pow_successor_pair_mul p
  17. 0017specialize pow_successor_pair_mul e
  18. 0018specialize pow_successor_pair_mul (S e)
  19. 0019specialize pow_successor_pair_mul r
  20. 0020specialize pow_successor_pair_mul x1
  21. 0021apply pow_successor_pair_mul
  22. 0022refl
  23. 0023exact hr
  24. 0024exact hsuccessor_witness
  25. 0025exists x1
  26. 0026split
  27. 0027exact hsuccessor_witness
  28. 0028exists x
  29. 0029trans r * q
  30. 0030exact ha
  31. 0031rewrite hq_witness
  32. 0032trans (r * p) * x
  33. 0033symm
  34. 0034apply mul_assoc
  35. 0035congr
  36. 0036symm
  37. 0037exact hs
  38. 0038refl