BT00QL · Bertrand theorem

power_divides_add_mul

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

Multiplying power divisors adds their exponents.

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. ∀ f. ∀ s. ∀ a. ∀ b. s = e + f → PowerDivides(p,e,a) → PowerDivides(p,f,b) → PowerDivides(p,s,a · b)

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

PD0044 PowerDivides

3 occurrences

In local proof propositions

PD0020 Pow

1 occurrences

Exact expanded native-PA statement
forall p e f s a b. s = e + f -> (exists bpv_result_add_mul_left. ((exists ff_b_add_mul_left_power ff_c_add_mul_left_power. ((forall ff_i_add_mul_left_power_repeat. (exists ff_lt_add_mul_left_power_repeat_bound. ff_lt_add_mul_left_power_repeat_bound + S ff_i_add_mul_left_power_repeat = e) -> (((exists ff_h_add_mul_left_power_repeat_decoded. ff_h_add_mul_left_power_repeat_decoded + S (p) = S ((S (ff_i_add_mul_left_power_repeat)) * ff_c_add_mul_left_power)) /\ exists ff_q_add_mul_left_power_repeat_decoded. ff_b_add_mul_left_power = ff_q_add_mul_left_power_repeat_decoded * S ((S (ff_i_add_mul_left_power_repeat)) * ff_c_add_mul_left_power) + (p)))) /\ (exists ff_u_add_mul_left_power_product ff_v_add_mul_left_power_product. ((((exists ff_h_add_mul_left_power_product_start. ff_h_add_mul_left_power_product_start + S (1) = S ((S (0)) * ff_v_add_mul_left_power_product)) /\ exists ff_q_add_mul_left_power_product_start. ff_u_add_mul_left_power_product = ff_q_add_mul_left_power_product_start * S ((S (0)) * ff_v_add_mul_left_power_product) + (1))) /\ ((((exists ff_h_add_mul_left_power_product_terminal. ff_h_add_mul_left_power_product_terminal + S (bpv_result_add_mul_left) = S ((S (e)) * ff_v_add_mul_left_power_product)) /\ exists ff_q_add_mul_left_power_product_terminal. ff_u_add_mul_left_power_product = ff_q_add_mul_left_power_product_terminal * S ((S (e)) * ff_v_add_mul_left_power_product) + (bpv_result_add_mul_left))) /\ forall ff_i_add_mul_left_power_product. (exists ff_lt_add_mul_left_power_product_bound. ff_lt_add_mul_left_power_product_bound + S ff_i_add_mul_left_power_product = e) -> exists ff_p_add_mul_left_power_product ff_r_add_mul_left_power_product ff_s_add_mul_left_power_product. ((((exists ff_h_add_mul_left_power_product_factor. ff_h_add_mul_left_power_product_factor + S (ff_p_add_mul_left_power_product) = S ((S (ff_i_add_mul_left_power_product)) * ff_c_add_mul_left_power)) /\ exists ff_q_add_mul_left_power_product_factor. ff_b_add_mul_left_power = ff_q_add_mul_left_power_product_factor * S ((S (ff_i_add_mul_left_power_product)) * ff_c_add_mul_left_power) + (ff_p_add_mul_left_power_product))) /\ ((((exists ff_h_add_mul_left_power_product_partial. ff_h_add_mul_left_power_product_partial + S (ff_r_add_mul_left_power_product) = S ((S (ff_i_add_mul_left_power_product)) * ff_v_add_mul_left_power_product)) /\ exists ff_q_add_mul_left_power_product_partial. ff_u_add_mul_left_power_product = ff_q_add_mul_left_power_product_partial * S ((S (ff_i_add_mul_left_power_product)) * ff_v_add_mul_left_power_product) + (ff_r_add_mul_left_power_product))) /\ ((((exists ff_h_add_mul_left_power_product_successor. ff_h_add_mul_left_power_product_successor + S (ff_s_add_mul_left_power_product) = S ((S (S ff_i_add_mul_left_power_product)) * ff_v_add_mul_left_power_product)) /\ exists ff_q_add_mul_left_power_product_successor. ff_u_add_mul_left_power_product = ff_q_add_mul_left_power_product_successor * S ((S (S ff_i_add_mul_left_power_product)) * ff_v_add_mul_left_power_product) + (ff_s_add_mul_left_power_product))) /\ ff_s_add_mul_left_power_product = ff_r_add_mul_left_power_product * ff_p_add_mul_left_power_product)))))))) /\ (exists bpv_factor_add_mul_left_divides. a = bpv_result_add_mul_left * bpv_factor_add_mul_left_divides))) -> (exists bpv_result_add_mul_right. ((exists ff_b_add_mul_right_power ff_c_add_mul_right_power. ((forall ff_i_add_mul_right_power_repeat. (exists ff_lt_add_mul_right_power_repeat_bound. ff_lt_add_mul_right_power_repeat_bound + S ff_i_add_mul_right_power_repeat = f) -> (((exists ff_h_add_mul_right_power_repeat_decoded. ff_h_add_mul_right_power_repeat_decoded + S (p) = S ((S (ff_i_add_mul_right_power_repeat)) * ff_c_add_mul_right_power)) /\ exists ff_q_add_mul_right_power_repeat_decoded. ff_b_add_mul_right_power = ff_q_add_mul_right_power_repeat_decoded * S ((S (ff_i_add_mul_right_power_repeat)) * ff_c_add_mul_right_power) + (p)))) /\ (exists ff_u_add_mul_right_power_product ff_v_add_mul_right_power_product. ((((exists ff_h_add_mul_right_power_product_start. ff_h_add_mul_right_power_product_start + S (1) = S ((S (0)) * ff_v_add_mul_right_power_product)) /\ exists ff_q_add_mul_right_power_product_start. ff_u_add_mul_right_power_product = ff_q_add_mul_right_power_product_start * S ((S (0)) * ff_v_add_mul_right_power_product) + (1))) /\ ((((exists ff_h_add_mul_right_power_product_terminal. ff_h_add_mul_right_power_product_terminal + S (bpv_result_add_mul_right) = S ((S (f)) * ff_v_add_mul_right_power_product)) /\ exists ff_q_add_mul_right_power_product_terminal. ff_u_add_mul_right_power_product = ff_q_add_mul_right_power_product_terminal * S ((S (f)) * ff_v_add_mul_right_power_product) + (bpv_result_add_mul_right))) /\ forall ff_i_add_mul_right_power_product. (exists ff_lt_add_mul_right_power_product_bound. ff_lt_add_mul_right_power_product_bound + S ff_i_add_mul_right_power_product = f) -> exists ff_p_add_mul_right_power_product ff_r_add_mul_right_power_product ff_s_add_mul_right_power_product. ((((exists ff_h_add_mul_right_power_product_factor. ff_h_add_mul_right_power_product_factor + S (ff_p_add_mul_right_power_product) = S ((S (ff_i_add_mul_right_power_product)) * ff_c_add_mul_right_power)) /\ exists ff_q_add_mul_right_power_product_factor. ff_b_add_mul_right_power = ff_q_add_mul_right_power_product_factor * S ((S (ff_i_add_mul_right_power_product)) * ff_c_add_mul_right_power) + (ff_p_add_mul_right_power_product))) /\ ((((exists ff_h_add_mul_right_power_product_partial. ff_h_add_mul_right_power_product_partial + S (ff_r_add_mul_right_power_product) = S ((S (ff_i_add_mul_right_power_product)) * ff_v_add_mul_right_power_product)) /\ exists ff_q_add_mul_right_power_product_partial. ff_u_add_mul_right_power_product = ff_q_add_mul_right_power_product_partial * S ((S (ff_i_add_mul_right_power_product)) * ff_v_add_mul_right_power_product) + (ff_r_add_mul_right_power_product))) /\ ((((exists ff_h_add_mul_right_power_product_successor. ff_h_add_mul_right_power_product_successor + S (ff_s_add_mul_right_power_product) = S ((S (S ff_i_add_mul_right_power_product)) * ff_v_add_mul_right_power_product)) /\ exists ff_q_add_mul_right_power_product_successor. ff_u_add_mul_right_power_product = ff_q_add_mul_right_power_product_successor * S ((S (S ff_i_add_mul_right_power_product)) * ff_v_add_mul_right_power_product) + (ff_s_add_mul_right_power_product))) /\ ff_s_add_mul_right_power_product = ff_r_add_mul_right_power_product * ff_p_add_mul_right_power_product)))))))) /\ (exists bpv_factor_add_mul_right_divides. b = bpv_result_add_mul_right * bpv_factor_add_mul_right_divides))) -> (exists bpvi_result_add_mul_result. ((exists bpvi_b_add_mul_result_power bpvi_c_add_mul_result_power. ((forall bpvi_i_add_mul_result_power. (exists bpvi_repeat_gap_add_mul_result_power. bpvi_repeat_gap_add_mul_result_power + S bpvi_i_add_mul_result_power = s) -> (((exists bpvi_h_add_mul_result_power_repeat. bpvi_h_add_mul_result_power_repeat + S (p) = S ((S (bpvi_i_add_mul_result_power)) * bpvi_c_add_mul_result_power)) /\ exists bpvi_q_add_mul_result_power_repeat. bpvi_b_add_mul_result_power = bpvi_q_add_mul_result_power_repeat * S ((S (bpvi_i_add_mul_result_power)) * bpvi_c_add_mul_result_power) + (p)))) /\ (exists bpvi_u_add_mul_result_power bpvi_v_add_mul_result_power. ((((exists bpvi_h_add_mul_result_power_start. bpvi_h_add_mul_result_power_start + S (1) = S ((S (0)) * bpvi_v_add_mul_result_power)) /\ exists bpvi_q_add_mul_result_power_start. bpvi_u_add_mul_result_power = bpvi_q_add_mul_result_power_start * S ((S (0)) * bpvi_v_add_mul_result_power) + (1))) /\ ((((exists bpvi_h_add_mul_result_power_terminal. bpvi_h_add_mul_result_power_terminal + S (bpvi_result_add_mul_result) = S ((S (s)) * bpvi_v_add_mul_result_power)) /\ exists bpvi_q_add_mul_result_power_terminal. bpvi_u_add_mul_result_power = bpvi_q_add_mul_result_power_terminal * S ((S (s)) * bpvi_v_add_mul_result_power) + (bpvi_result_add_mul_result))) /\ forall bpvi_j_add_mul_result_power. (exists bpvi_product_gap_add_mul_result_power. bpvi_product_gap_add_mul_result_power + S bpvi_j_add_mul_result_power = s) -> exists bpvi_factor_add_mul_result_power bpvi_partial_add_mul_result_power bpvi_successor_add_mul_result_power. ((((exists bpvi_h_add_mul_result_power_factor. bpvi_h_add_mul_result_power_factor + S (bpvi_factor_add_mul_result_power) = S ((S (bpvi_j_add_mul_result_power)) * bpvi_c_add_mul_result_power)) /\ exists bpvi_q_add_mul_result_power_factor. bpvi_b_add_mul_result_power = bpvi_q_add_mul_result_power_factor * S ((S (bpvi_j_add_mul_result_power)) * bpvi_c_add_mul_result_power) + (bpvi_factor_add_mul_result_power))) /\ ((((exists bpvi_h_add_mul_result_power_partial. bpvi_h_add_mul_result_power_partial + S (bpvi_partial_add_mul_result_power) = S ((S (bpvi_j_add_mul_result_power)) * bpvi_v_add_mul_result_power)) /\ exists bpvi_q_add_mul_result_power_partial. bpvi_u_add_mul_result_power = bpvi_q_add_mul_result_power_partial * S ((S (bpvi_j_add_mul_result_power)) * bpvi_v_add_mul_result_power) + (bpvi_partial_add_mul_result_power))) /\ ((((exists bpvi_h_add_mul_result_power_successor. bpvi_h_add_mul_result_power_successor + S (bpvi_successor_add_mul_result_power) = S ((S (S bpvi_j_add_mul_result_power)) * bpvi_v_add_mul_result_power)) /\ exists bpvi_q_add_mul_result_power_successor. bpvi_u_add_mul_result_power = bpvi_q_add_mul_result_power_successor * S ((S (S bpvi_j_add_mul_result_power)) * bpvi_v_add_mul_result_power) + (bpvi_successor_add_mul_result_power))) /\ bpvi_successor_add_mul_result_power = bpvi_partial_add_mul_result_power * bpvi_factor_add_mul_result_power)))))))) /\ exists bpvi_divisor_factor_add_mul_result. a * b = bpvi_result_add_mul_result * bpvi_divisor_factor_add_mul_result))

Proof neighborhood

Direct theorem prerequisites

BT0080 pow_exists BT009X pow_add BT00QJ mul_shuffle_four

Direct theorem dependents

BT00QR power_valuation_mul_lower

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

47 script commands · 17 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 addmul shuffle four
01Fix variables and assumptionsL1–9

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

  1. L1
    intro p
  2. L2
    intro e
  3. L3
    intro f
  4. L4
    intro s
  5. L5
    intro a
  6. L6
    intro b
  7. L7
    intro hsum
  8. L8
    intro hleft
  9. L9
    intro hright
02Separate the logical casesL10–15

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

  1. L10
    cases hleft
  2. L11
    cases hleft_witness
  3. L12
    cases hleft_witness_right
  4. L13
    cases hright
  5. L14
    cases hright_witness
  6. L15
    cases hright_witness_right
03Establish htotalL16–19

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

  1. L16
    have htotal : ∃ r. Pow(p,s,r)Definitions: Pow(p,s,r)Original native command in the exact edition
  2. L17
    specialize pow_exists p
  3. L18
    specialize pow_exists s
  4. L19
    exact pow_exists
04Separate the logical casesL20–20

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

  1. L20
    cases htotal
05Establish hpower_productL21–30

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

  1. L21
    have hpower_product : x4 = x * x2
  2. L22
    specialize pow_add p
  3. L23
    specialize pow_add e
  4. L24
    specialize pow_add f
  5. L25
    specialize pow_add s
  6. L26
    specialize pow_add x
  7. L27
    specialize pow_add x2
  8. L28
    specialize pow_add x4
  9. L29
    apply pow_add
  10. L30
    exact hsum
06Use earlier factsL31–33

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

  1. L31
    exact hleft_witness_left
  2. L32
    exact hright_witness_left
  3. L33
    exact htotal_witness
07Construct an explicit witnessL34–34

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

  1. L34
    exists x4
08Separate the logical casesL35–35

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

  1. L35
    split
09Use earlier factsL36–36

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

  1. L36
    exact htotal_witness
10Construct an explicit witnessL37–37

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

  1. L37
    exists x1 * x3
11Calculate and transport equalitiesL38–39

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

  1. L38
    trans (x * x1) * (x2 * x3)
  2. L39
    congr
12Use earlier factsL40–41

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

  1. L40
    exact hleft_witness_right_witness
  2. L41
    exact hright_witness_right_witness
13Calculate and transport equalitiesL42–42

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

  1. L42
    trans (x * x2) * (x1 * x3)
14Use earlier factsL43–43

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

  1. L43
    apply mul_shuffle_four
15Calculate and transport equalitiesL44–45

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

  1. L44
    congr
  2. L45
    symm
16Use earlier factsL46–46

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

  1. L46
    exact hpower_product
17Calculate and transport equalitiesL47–47

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

  1. L47
    refl

Library-wide reading audit

Original defined command ledger · 47 lines
  1. 0001intro p
  2. 0002intro e
  3. 0003intro f
  4. 0004intro s
  5. 0005intro a
  6. 0006intro b
  7. 0007intro hsum
  8. 0008intro hleft
  9. 0009intro hright
  10. 0010cases hleft
  11. 0011cases hleft_witness
  12. 0012cases hleft_witness_right
  13. 0013cases hright
  14. 0014cases hright_witness
  15. 0015cases hright_witness_right
  16. 0016have htotal : ∃ r. Pow(p,s,r)
    Exact native replay linehave htotal : exists r. (exists ff_b_bpd_add_mul_total_witness ff_c_bpd_add_mul_total_witness. ((forall ff_i_bpd_add_mul_total_witness_repeat. (exists ff_lt_bpd_add_mul_total_witness_repeat_bound. ff_lt_bpd_add_mul_total_witness_repeat_bound + S ff_i_bpd_add_mul_total_witness_repeat = s) -> (((exists ff_h_bpd_add_mul_total_witness_repeat_decoded. ff_h_bpd_add_mul_total_witness_repeat_decoded + S (p) = S ((S (ff_i_bpd_add_mul_total_witness_repeat)) * ff_c_bpd_add_mul_total_witness)) /\ exists ff_q_bpd_add_mul_total_witness_repeat_decoded. ff_b_bpd_add_mul_total_witness = ff_q_bpd_add_mul_total_witness_repeat_decoded * S ((S (ff_i_bpd_add_mul_total_witness_repeat)) * ff_c_bpd_add_mul_total_witness) + (p)))) /\ (exists ff_u_bpd_add_mul_total_witness_product ff_v_bpd_add_mul_total_witness_product. ((((exists ff_h_bpd_add_mul_total_witness_product_start. ff_h_bpd_add_mul_total_witness_product_start + S (1) = S ((S (0)) * ff_v_bpd_add_mul_total_witness_product)) /\ exists ff_q_bpd_add_mul_total_witness_product_start. ff_u_bpd_add_mul_total_witness_product = ff_q_bpd_add_mul_total_witness_product_start * S ((S (0)) * ff_v_bpd_add_mul_total_witness_product) + (1))) /\ ((((exists ff_h_bpd_add_mul_total_witness_product_terminal. ff_h_bpd_add_mul_total_witness_product_terminal + S (r) = S ((S (s)) * ff_v_bpd_add_mul_total_witness_product)) /\ exists ff_q_bpd_add_mul_total_witness_product_terminal. ff_u_bpd_add_mul_total_witness_product = ff_q_bpd_add_mul_total_witness_product_terminal * S ((S (s)) * ff_v_bpd_add_mul_total_witness_product) + (r))) /\ forall ff_i_bpd_add_mul_total_witness_product. (exists ff_lt_bpd_add_mul_total_witness_product_bound. ff_lt_bpd_add_mul_total_witness_product_bound + S ff_i_bpd_add_mul_total_witness_product = s) -> exists ff_p_bpd_add_mul_total_witness_product ff_r_bpd_add_mul_total_witness_product ff_s_bpd_add_mul_total_witness_product. ((((exists ff_h_bpd_add_mul_total_witness_product_factor. ff_h_bpd_add_mul_total_witness_product_factor + S (ff_p_bpd_add_mul_total_witness_product) = S ((S (ff_i_bpd_add_mul_total_witness_product)) * ff_c_bpd_add_mul_total_witness)) /\ exists ff_q_bpd_add_mul_total_witness_product_factor. ff_b_bpd_add_mul_total_witness = ff_q_bpd_add_mul_total_witness_product_factor * S ((S (ff_i_bpd_add_mul_total_witness_product)) * ff_c_bpd_add_mul_total_witness) + (ff_p_bpd_add_mul_total_witness_product))) /\ ((((exists ff_h_bpd_add_mul_total_witness_product_partial. ff_h_bpd_add_mul_total_witness_product_partial + S (ff_r_bpd_add_mul_total_witness_product) = S ((S (ff_i_bpd_add_mul_total_witness_product)) * ff_v_bpd_add_mul_total_witness_product)) /\ exists ff_q_bpd_add_mul_total_witness_product_partial. ff_u_bpd_add_mul_total_witness_product = ff_q_bpd_add_mul_total_witness_product_partial * S ((S (ff_i_bpd_add_mul_total_witness_product)) * ff_v_bpd_add_mul_total_witness_product) + (ff_r_bpd_add_mul_total_witness_product))) /\ ((((exists ff_h_bpd_add_mul_total_witness_product_successor. ff_h_bpd_add_mul_total_witness_product_successor + S (ff_s_bpd_add_mul_total_witness_product) = S ((S (S ff_i_bpd_add_mul_total_witness_product)) * ff_v_bpd_add_mul_total_witness_product)) /\ exists ff_q_bpd_add_mul_total_witness_product_successor. ff_u_bpd_add_mul_total_witness_product = ff_q_bpd_add_mul_total_witness_product_successor * S ((S (S ff_i_bpd_add_mul_total_witness_product)) * ff_v_bpd_add_mul_total_witness_product) + (ff_s_bpd_add_mul_total_witness_product))) /\ ff_s_bpd_add_mul_total_witness_product = ff_r_bpd_add_mul_total_witness_product * ff_p_bpd_add_mul_total_witness_product))))))))
  17. 0017specialize pow_exists p
  18. 0018specialize pow_exists s
  19. 0019exact pow_exists
  20. 0020cases htotal
  21. 0021have hpower_product : x4 = x * x2
  22. 0022specialize pow_add p
  23. 0023specialize pow_add e
  24. 0024specialize pow_add f
  25. 0025specialize pow_add s
  26. 0026specialize pow_add x
  27. 0027specialize pow_add x2
  28. 0028specialize pow_add x4
  29. 0029apply pow_add
  30. 0030exact hsum
  31. 0031exact hleft_witness_left
  32. 0032exact hright_witness_left
  33. 0033exact htotal_witness
  34. 0034exists x4
  35. 0035split
  36. 0036exact htotal_witness
  37. 0037exists x1 * x3
  38. 0038trans (x * x1) * (x2 * x3)
  39. 0039congr
  40. 0040exact hleft_witness_right_witness
  41. 0041exact hright_witness_right_witness
  42. 0042trans (x * x2) * (x1 * x3)
  43. 0043apply mul_shuffle_four
  44. 0044congr
  45. 0045symm
  46. 0046exact hpower_product
  47. 0047refl