BT00QK · Bertrand theorem

power_divides_exponent_antitone

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

Divisibility by a higher relational power entails every lower exponent.

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. ∀ a. Le(e,f) → PowerDivides(p,f,a) → PowerDivides(p,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 PD0044 PowerDivides

3 occurrences

In local proof propositions

PD0020 Pow

2 occurrences

Exact expanded native-PA statement
forall p e f a. (exists bpd_gap_antitone_exponents. bpd_gap_antitone_exponents + (e) = (f)) -> (exists bpv_result_antitone_high. ((exists ff_b_antitone_high_power ff_c_antitone_high_power. ((forall ff_i_antitone_high_power_repeat. (exists ff_lt_antitone_high_power_repeat_bound. ff_lt_antitone_high_power_repeat_bound + S ff_i_antitone_high_power_repeat = f) -> (((exists ff_h_antitone_high_power_repeat_decoded. ff_h_antitone_high_power_repeat_decoded + S (p) = S ((S (ff_i_antitone_high_power_repeat)) * ff_c_antitone_high_power)) /\ exists ff_q_antitone_high_power_repeat_decoded. ff_b_antitone_high_power = ff_q_antitone_high_power_repeat_decoded * S ((S (ff_i_antitone_high_power_repeat)) * ff_c_antitone_high_power) + (p)))) /\ (exists ff_u_antitone_high_power_product ff_v_antitone_high_power_product. ((((exists ff_h_antitone_high_power_product_start. ff_h_antitone_high_power_product_start + S (1) = S ((S (0)) * ff_v_antitone_high_power_product)) /\ exists ff_q_antitone_high_power_product_start. ff_u_antitone_high_power_product = ff_q_antitone_high_power_product_start * S ((S (0)) * ff_v_antitone_high_power_product) + (1))) /\ ((((exists ff_h_antitone_high_power_product_terminal. ff_h_antitone_high_power_product_terminal + S (bpv_result_antitone_high) = S ((S (f)) * ff_v_antitone_high_power_product)) /\ exists ff_q_antitone_high_power_product_terminal. ff_u_antitone_high_power_product = ff_q_antitone_high_power_product_terminal * S ((S (f)) * ff_v_antitone_high_power_product) + (bpv_result_antitone_high))) /\ forall ff_i_antitone_high_power_product. (exists ff_lt_antitone_high_power_product_bound. ff_lt_antitone_high_power_product_bound + S ff_i_antitone_high_power_product = f) -> exists ff_p_antitone_high_power_product ff_r_antitone_high_power_product ff_s_antitone_high_power_product. ((((exists ff_h_antitone_high_power_product_factor. ff_h_antitone_high_power_product_factor + S (ff_p_antitone_high_power_product) = S ((S (ff_i_antitone_high_power_product)) * ff_c_antitone_high_power)) /\ exists ff_q_antitone_high_power_product_factor. ff_b_antitone_high_power = ff_q_antitone_high_power_product_factor * S ((S (ff_i_antitone_high_power_product)) * ff_c_antitone_high_power) + (ff_p_antitone_high_power_product))) /\ ((((exists ff_h_antitone_high_power_product_partial. ff_h_antitone_high_power_product_partial + S (ff_r_antitone_high_power_product) = S ((S (ff_i_antitone_high_power_product)) * ff_v_antitone_high_power_product)) /\ exists ff_q_antitone_high_power_product_partial. ff_u_antitone_high_power_product = ff_q_antitone_high_power_product_partial * S ((S (ff_i_antitone_high_power_product)) * ff_v_antitone_high_power_product) + (ff_r_antitone_high_power_product))) /\ ((((exists ff_h_antitone_high_power_product_successor. ff_h_antitone_high_power_product_successor + S (ff_s_antitone_high_power_product) = S ((S (S ff_i_antitone_high_power_product)) * ff_v_antitone_high_power_product)) /\ exists ff_q_antitone_high_power_product_successor. ff_u_antitone_high_power_product = ff_q_antitone_high_power_product_successor * S ((S (S ff_i_antitone_high_power_product)) * ff_v_antitone_high_power_product) + (ff_s_antitone_high_power_product))) /\ ff_s_antitone_high_power_product = ff_r_antitone_high_power_product * ff_p_antitone_high_power_product)))))))) /\ (exists bpv_factor_antitone_high_divides. a = bpv_result_antitone_high * bpv_factor_antitone_high_divides))) -> (exists bpv_result_antitone_low. ((exists ff_b_antitone_low_power ff_c_antitone_low_power. ((forall ff_i_antitone_low_power_repeat. (exists ff_lt_antitone_low_power_repeat_bound. ff_lt_antitone_low_power_repeat_bound + S ff_i_antitone_low_power_repeat = e) -> (((exists ff_h_antitone_low_power_repeat_decoded. ff_h_antitone_low_power_repeat_decoded + S (p) = S ((S (ff_i_antitone_low_power_repeat)) * ff_c_antitone_low_power)) /\ exists ff_q_antitone_low_power_repeat_decoded. ff_b_antitone_low_power = ff_q_antitone_low_power_repeat_decoded * S ((S (ff_i_antitone_low_power_repeat)) * ff_c_antitone_low_power) + (p)))) /\ (exists ff_u_antitone_low_power_product ff_v_antitone_low_power_product. ((((exists ff_h_antitone_low_power_product_start. ff_h_antitone_low_power_product_start + S (1) = S ((S (0)) * ff_v_antitone_low_power_product)) /\ exists ff_q_antitone_low_power_product_start. ff_u_antitone_low_power_product = ff_q_antitone_low_power_product_start * S ((S (0)) * ff_v_antitone_low_power_product) + (1))) /\ ((((exists ff_h_antitone_low_power_product_terminal. ff_h_antitone_low_power_product_terminal + S (bpv_result_antitone_low) = S ((S (e)) * ff_v_antitone_low_power_product)) /\ exists ff_q_antitone_low_power_product_terminal. ff_u_antitone_low_power_product = ff_q_antitone_low_power_product_terminal * S ((S (e)) * ff_v_antitone_low_power_product) + (bpv_result_antitone_low))) /\ forall ff_i_antitone_low_power_product. (exists ff_lt_antitone_low_power_product_bound. ff_lt_antitone_low_power_product_bound + S ff_i_antitone_low_power_product = e) -> exists ff_p_antitone_low_power_product ff_r_antitone_low_power_product ff_s_antitone_low_power_product. ((((exists ff_h_antitone_low_power_product_factor. ff_h_antitone_low_power_product_factor + S (ff_p_antitone_low_power_product) = S ((S (ff_i_antitone_low_power_product)) * ff_c_antitone_low_power)) /\ exists ff_q_antitone_low_power_product_factor. ff_b_antitone_low_power = ff_q_antitone_low_power_product_factor * S ((S (ff_i_antitone_low_power_product)) * ff_c_antitone_low_power) + (ff_p_antitone_low_power_product))) /\ ((((exists ff_h_antitone_low_power_product_partial. ff_h_antitone_low_power_product_partial + S (ff_r_antitone_low_power_product) = S ((S (ff_i_antitone_low_power_product)) * ff_v_antitone_low_power_product)) /\ exists ff_q_antitone_low_power_product_partial. ff_u_antitone_low_power_product = ff_q_antitone_low_power_product_partial * S ((S (ff_i_antitone_low_power_product)) * ff_v_antitone_low_power_product) + (ff_r_antitone_low_power_product))) /\ ((((exists ff_h_antitone_low_power_product_successor. ff_h_antitone_low_power_product_successor + S (ff_s_antitone_low_power_product) = S ((S (S ff_i_antitone_low_power_product)) * ff_v_antitone_low_power_product)) /\ exists ff_q_antitone_low_power_product_successor. ff_u_antitone_low_power_product = ff_q_antitone_low_power_product_successor * S ((S (S ff_i_antitone_low_power_product)) * ff_v_antitone_low_power_product) + (ff_s_antitone_low_power_product))) /\ ff_s_antitone_low_power_product = ff_r_antitone_low_power_product * ff_p_antitone_low_power_product)))))))) /\ (exists bpv_factor_antitone_low_divides. a = bpv_result_antitone_low * bpv_factor_antitone_low_divides)))

Proof neighborhood

Direct theorem prerequisites

BT0080 pow_exists BT009X pow_add BT0002 add_comm BT0008 mul_assoc

Direct theorem dependents

BT00QS power_valuation_mul_upper BT00SC power_divides_of_exponent_le_valuation BT00W0 power_valuation_nonzero_exponent_divides_base

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

51 script commands · 19 reading checkpoints · 4 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 (4)
pow existspow addadd commmul assoc
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 f
  4. L4
    intro a
  5. L5
    intro hef
  6. L6
    intro hhigh
02Separate the logical casesL7–10

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

  1. L7
    cases hef
  2. L8
    cases hhigh
  3. L9
    cases hhigh_witness
  4. L10
    cases hhigh_witness_right
03Establish hsumL11–17

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

  1. L11
    have hsum : f = e + x
  2. L12
    trans x + e
  3. L13
    symm
  4. L14
    exact hef_witness
  5. L15
    specialize add_comm x
  6. L16
    specialize add_comm e
  7. L17
    exact add_comm
04Establish hlow_powerL18–21

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

  1. L18
    have hlow_power : ∃ r. Pow(p,e,r)Definitions: Pow(p,e,r)Original native command in the exact edition
  2. L19
    specialize pow_exists p
  3. L20
    specialize pow_exists e
  4. L21
    exact pow_exists
05Separate the logical casesL22–22

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

  1. L22
    cases hlow_power
06Establish hgap_powerL23–26

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

  1. L23
    have hgap_power : ∃ r. Pow(p,x,r)Definitions: Pow(p,x,r)Original native command in the exact edition
  2. L24
    specialize pow_exists p
  3. L25
    specialize pow_exists x
  4. L26
    exact pow_exists
07Separate the logical casesL27–27

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

  1. L27
    cases hgap_power
08Establish hfactorL28–37

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

  1. L28
    have hfactor : x1 = x3 * x4
  2. L29
    specialize pow_add p
  3. L30
    specialize pow_add e
  4. L31
    specialize pow_add x
  5. L32
    specialize pow_add f
  6. L33
    specialize pow_add x3
  7. L34
    specialize pow_add x4
  8. L35
    specialize pow_add x1
  9. L36
    apply pow_add
  10. L37
    exact hsum
09Use earlier factsL38–40

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

  1. L38
    exact hlow_power_witness
  2. L39
    exact hgap_power_witness
  3. L40
    exact hhigh_witness_left
10Construct an explicit witnessL41–41

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

  1. L41
    exists x3
11Separate the logical casesL42–42

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

  1. L42
    split
12Use earlier factsL43–43

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

  1. L43
    exact hlow_power_witness
13Construct an explicit witnessL44–44

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

  1. L44
    exists x4 * x2
14Calculate and transport equalitiesL45–45

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

  1. L45
    trans x1 * x2
15Use earlier factsL46–46

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

  1. L46
    exact hhigh_witness_right_witness
16Calculate and transport equalitiesL47–48

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

  1. L47
    trans (x3 * x4) * x2
  2. L48
    congr
17Use earlier factsL49–49

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

  1. L49
    exact hfactor
18Calculate and transport equalitiesL50–50

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

  1. L50
    refl
19Use earlier factsL51–51

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

  1. L51
    apply mul_assoc

Library-wide reading audit

Original defined command ledger · 51 lines
  1. 0001intro p
  2. 0002intro e
  3. 0003intro f
  4. 0004intro a
  5. 0005intro hef
  6. 0006intro hhigh
  7. 0007cases hef
  8. 0008cases hhigh
  9. 0009cases hhigh_witness
  10. 0010cases hhigh_witness_right
  11. 0011have hsum : f = e + x
  12. 0012trans x + e
  13. 0013symm
  14. 0014exact hef_witness
  15. 0015specialize add_comm x
  16. 0016specialize add_comm e
  17. 0017exact add_comm
  18. 0018have hlow_power : ∃ r. Pow(p,e,r)
    Exact native replay linehave hlow_power : exists r. (exists ff_b_bpd_antitone_low_witness ff_c_bpd_antitone_low_witness. ((forall ff_i_bpd_antitone_low_witness_repeat. (exists ff_lt_bpd_antitone_low_witness_repeat_bound. ff_lt_bpd_antitone_low_witness_repeat_bound + S ff_i_bpd_antitone_low_witness_repeat = e) -> (((exists ff_h_bpd_antitone_low_witness_repeat_decoded. ff_h_bpd_antitone_low_witness_repeat_decoded + S (p) = S ((S (ff_i_bpd_antitone_low_witness_repeat)) * ff_c_bpd_antitone_low_witness)) /\ exists ff_q_bpd_antitone_low_witness_repeat_decoded. ff_b_bpd_antitone_low_witness = ff_q_bpd_antitone_low_witness_repeat_decoded * S ((S (ff_i_bpd_antitone_low_witness_repeat)) * ff_c_bpd_antitone_low_witness) + (p)))) /\ (exists ff_u_bpd_antitone_low_witness_product ff_v_bpd_antitone_low_witness_product. ((((exists ff_h_bpd_antitone_low_witness_product_start. ff_h_bpd_antitone_low_witness_product_start + S (1) = S ((S (0)) * ff_v_bpd_antitone_low_witness_product)) /\ exists ff_q_bpd_antitone_low_witness_product_start. ff_u_bpd_antitone_low_witness_product = ff_q_bpd_antitone_low_witness_product_start * S ((S (0)) * ff_v_bpd_antitone_low_witness_product) + (1))) /\ ((((exists ff_h_bpd_antitone_low_witness_product_terminal. ff_h_bpd_antitone_low_witness_product_terminal + S (r) = S ((S (e)) * ff_v_bpd_antitone_low_witness_product)) /\ exists ff_q_bpd_antitone_low_witness_product_terminal. ff_u_bpd_antitone_low_witness_product = ff_q_bpd_antitone_low_witness_product_terminal * S ((S (e)) * ff_v_bpd_antitone_low_witness_product) + (r))) /\ forall ff_i_bpd_antitone_low_witness_product. (exists ff_lt_bpd_antitone_low_witness_product_bound. ff_lt_bpd_antitone_low_witness_product_bound + S ff_i_bpd_antitone_low_witness_product = e) -> exists ff_p_bpd_antitone_low_witness_product ff_r_bpd_antitone_low_witness_product ff_s_bpd_antitone_low_witness_product. ((((exists ff_h_bpd_antitone_low_witness_product_factor. ff_h_bpd_antitone_low_witness_product_factor + S (ff_p_bpd_antitone_low_witness_product) = S ((S (ff_i_bpd_antitone_low_witness_product)) * ff_c_bpd_antitone_low_witness)) /\ exists ff_q_bpd_antitone_low_witness_product_factor. ff_b_bpd_antitone_low_witness = ff_q_bpd_antitone_low_witness_product_factor * S ((S (ff_i_bpd_antitone_low_witness_product)) * ff_c_bpd_antitone_low_witness) + (ff_p_bpd_antitone_low_witness_product))) /\ ((((exists ff_h_bpd_antitone_low_witness_product_partial. ff_h_bpd_antitone_low_witness_product_partial + S (ff_r_bpd_antitone_low_witness_product) = S ((S (ff_i_bpd_antitone_low_witness_product)) * ff_v_bpd_antitone_low_witness_product)) /\ exists ff_q_bpd_antitone_low_witness_product_partial. ff_u_bpd_antitone_low_witness_product = ff_q_bpd_antitone_low_witness_product_partial * S ((S (ff_i_bpd_antitone_low_witness_product)) * ff_v_bpd_antitone_low_witness_product) + (ff_r_bpd_antitone_low_witness_product))) /\ ((((exists ff_h_bpd_antitone_low_witness_product_successor. ff_h_bpd_antitone_low_witness_product_successor + S (ff_s_bpd_antitone_low_witness_product) = S ((S (S ff_i_bpd_antitone_low_witness_product)) * ff_v_bpd_antitone_low_witness_product)) /\ exists ff_q_bpd_antitone_low_witness_product_successor. ff_u_bpd_antitone_low_witness_product = ff_q_bpd_antitone_low_witness_product_successor * S ((S (S ff_i_bpd_antitone_low_witness_product)) * ff_v_bpd_antitone_low_witness_product) + (ff_s_bpd_antitone_low_witness_product))) /\ ff_s_bpd_antitone_low_witness_product = ff_r_bpd_antitone_low_witness_product * ff_p_bpd_antitone_low_witness_product))))))))
  19. 0019specialize pow_exists p
  20. 0020specialize pow_exists e
  21. 0021exact pow_exists
  22. 0022cases hlow_power
  23. 0023have hgap_power : ∃ r. Pow(p,x,r)
    Exact native replay linehave hgap_power : exists r. (exists bpvi_b_bpd_antitone_gap_witness bpvi_c_bpd_antitone_gap_witness. ((forall bpvi_i_bpd_antitone_gap_witness. (exists bpvi_repeat_gap_bpd_antitone_gap_witness. bpvi_repeat_gap_bpd_antitone_gap_witness + S bpvi_i_bpd_antitone_gap_witness = x) -> (((exists bpvi_h_bpd_antitone_gap_witness_repeat. bpvi_h_bpd_antitone_gap_witness_repeat + S (p) = S ((S (bpvi_i_bpd_antitone_gap_witness)) * bpvi_c_bpd_antitone_gap_witness)) /\ exists bpvi_q_bpd_antitone_gap_witness_repeat. bpvi_b_bpd_antitone_gap_witness = bpvi_q_bpd_antitone_gap_witness_repeat * S ((S (bpvi_i_bpd_antitone_gap_witness)) * bpvi_c_bpd_antitone_gap_witness) + (p)))) /\ (exists bpvi_u_bpd_antitone_gap_witness bpvi_v_bpd_antitone_gap_witness. ((((exists bpvi_h_bpd_antitone_gap_witness_start. bpvi_h_bpd_antitone_gap_witness_start + S (1) = S ((S (0)) * bpvi_v_bpd_antitone_gap_witness)) /\ exists bpvi_q_bpd_antitone_gap_witness_start. bpvi_u_bpd_antitone_gap_witness = bpvi_q_bpd_antitone_gap_witness_start * S ((S (0)) * bpvi_v_bpd_antitone_gap_witness) + (1))) /\ ((((exists bpvi_h_bpd_antitone_gap_witness_terminal. bpvi_h_bpd_antitone_gap_witness_terminal + S (r) = S ((S (x)) * bpvi_v_bpd_antitone_gap_witness)) /\ exists bpvi_q_bpd_antitone_gap_witness_terminal. bpvi_u_bpd_antitone_gap_witness = bpvi_q_bpd_antitone_gap_witness_terminal * S ((S (x)) * bpvi_v_bpd_antitone_gap_witness) + (r))) /\ forall bpvi_j_bpd_antitone_gap_witness. (exists bpvi_product_gap_bpd_antitone_gap_witness. bpvi_product_gap_bpd_antitone_gap_witness + S bpvi_j_bpd_antitone_gap_witness = x) -> exists bpvi_factor_bpd_antitone_gap_witness bpvi_partial_bpd_antitone_gap_witness bpvi_successor_bpd_antitone_gap_witness. ((((exists bpvi_h_bpd_antitone_gap_witness_factor. bpvi_h_bpd_antitone_gap_witness_factor + S (bpvi_factor_bpd_antitone_gap_witness) = S ((S (bpvi_j_bpd_antitone_gap_witness)) * bpvi_c_bpd_antitone_gap_witness)) /\ exists bpvi_q_bpd_antitone_gap_witness_factor. bpvi_b_bpd_antitone_gap_witness = bpvi_q_bpd_antitone_gap_witness_factor * S ((S (bpvi_j_bpd_antitone_gap_witness)) * bpvi_c_bpd_antitone_gap_witness) + (bpvi_factor_bpd_antitone_gap_witness))) /\ ((((exists bpvi_h_bpd_antitone_gap_witness_partial. bpvi_h_bpd_antitone_gap_witness_partial + S (bpvi_partial_bpd_antitone_gap_witness) = S ((S (bpvi_j_bpd_antitone_gap_witness)) * bpvi_v_bpd_antitone_gap_witness)) /\ exists bpvi_q_bpd_antitone_gap_witness_partial. bpvi_u_bpd_antitone_gap_witness = bpvi_q_bpd_antitone_gap_witness_partial * S ((S (bpvi_j_bpd_antitone_gap_witness)) * bpvi_v_bpd_antitone_gap_witness) + (bpvi_partial_bpd_antitone_gap_witness))) /\ ((((exists bpvi_h_bpd_antitone_gap_witness_successor. bpvi_h_bpd_antitone_gap_witness_successor + S (bpvi_successor_bpd_antitone_gap_witness) = S ((S (S bpvi_j_bpd_antitone_gap_witness)) * bpvi_v_bpd_antitone_gap_witness)) /\ exists bpvi_q_bpd_antitone_gap_witness_successor. bpvi_u_bpd_antitone_gap_witness = bpvi_q_bpd_antitone_gap_witness_successor * S ((S (S bpvi_j_bpd_antitone_gap_witness)) * bpvi_v_bpd_antitone_gap_witness) + (bpvi_successor_bpd_antitone_gap_witness))) /\ bpvi_successor_bpd_antitone_gap_witness = bpvi_partial_bpd_antitone_gap_witness * bpvi_factor_bpd_antitone_gap_witness))))))))
  24. 0024specialize pow_exists p
  25. 0025specialize pow_exists x
  26. 0026exact pow_exists
  27. 0027cases hgap_power
  28. 0028have hfactor : x1 = x3 * x4
  29. 0029specialize pow_add p
  30. 0030specialize pow_add e
  31. 0031specialize pow_add x
  32. 0032specialize pow_add f
  33. 0033specialize pow_add x3
  34. 0034specialize pow_add x4
  35. 0035specialize pow_add x1
  36. 0036apply pow_add
  37. 0037exact hsum
  38. 0038exact hlow_power_witness
  39. 0039exact hgap_power_witness
  40. 0040exact hhigh_witness_left
  41. 0041exists x3
  42. 0042split
  43. 0043exact hlow_power_witness
  44. 0044exists x4 * x2
  45. 0045trans x1 * x2
  46. 0046exact hhigh_witness_right_witness
  47. 0047trans (x3 * x4) * x2
  48. 0048congr
  49. 0049exact hfactor
  50. 0050refl
  51. 0051apply mul_assoc