BT00Q0 · Bertrand theorem

one_le_pow

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

Every relational power of a base at least one is at least 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

∀ a. ∀ e. ∀ x. Lt(0,a) → Pow(a,e,x) → Lt(0,x)

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

PD0002 Lt PD0020 Pow

3 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0020 Pow

3 occurrences

Exact expanded native-PA statement
forall a e x. (exists bpg_gap_base. bpg_gap_base + (1) = (a)) -> (exists ff_b_bpg_value ff_c_bpg_value. ((forall ff_i_bpg_value_repeat. (exists ff_lt_bpg_value_repeat_bound. ff_lt_bpg_value_repeat_bound + S ff_i_bpg_value_repeat = e) -> (((exists ff_h_bpg_value_repeat_decoded. ff_h_bpg_value_repeat_decoded + S (a) = S ((S (ff_i_bpg_value_repeat)) * ff_c_bpg_value)) /\ exists ff_q_bpg_value_repeat_decoded. ff_b_bpg_value = ff_q_bpg_value_repeat_decoded * S ((S (ff_i_bpg_value_repeat)) * ff_c_bpg_value) + (a)))) /\ (exists ff_u_bpg_value_product ff_v_bpg_value_product. ((((exists ff_h_bpg_value_product_start. ff_h_bpg_value_product_start + S (1) = S ((S (0)) * ff_v_bpg_value_product)) /\ exists ff_q_bpg_value_product_start. ff_u_bpg_value_product = ff_q_bpg_value_product_start * S ((S (0)) * ff_v_bpg_value_product) + (1))) /\ ((((exists ff_h_bpg_value_product_terminal. ff_h_bpg_value_product_terminal + S (x) = S ((S (e)) * ff_v_bpg_value_product)) /\ exists ff_q_bpg_value_product_terminal. ff_u_bpg_value_product = ff_q_bpg_value_product_terminal * S ((S (e)) * ff_v_bpg_value_product) + (x))) /\ forall ff_i_bpg_value_product. (exists ff_lt_bpg_value_product_bound. ff_lt_bpg_value_product_bound + S ff_i_bpg_value_product = e) -> exists ff_p_bpg_value_product ff_r_bpg_value_product ff_s_bpg_value_product. ((((exists ff_h_bpg_value_product_factor. ff_h_bpg_value_product_factor + S (ff_p_bpg_value_product) = S ((S (ff_i_bpg_value_product)) * ff_c_bpg_value)) /\ exists ff_q_bpg_value_product_factor. ff_b_bpg_value = ff_q_bpg_value_product_factor * S ((S (ff_i_bpg_value_product)) * ff_c_bpg_value) + (ff_p_bpg_value_product))) /\ ((((exists ff_h_bpg_value_product_partial. ff_h_bpg_value_product_partial + S (ff_r_bpg_value_product) = S ((S (ff_i_bpg_value_product)) * ff_v_bpg_value_product)) /\ exists ff_q_bpg_value_product_partial. ff_u_bpg_value_product = ff_q_bpg_value_product_partial * S ((S (ff_i_bpg_value_product)) * ff_v_bpg_value_product) + (ff_r_bpg_value_product))) /\ ((((exists ff_h_bpg_value_product_successor. ff_h_bpg_value_product_successor + S (ff_s_bpg_value_product) = S ((S (S ff_i_bpg_value_product)) * ff_v_bpg_value_product)) /\ exists ff_q_bpg_value_product_successor. ff_u_bpg_value_product = ff_q_bpg_value_product_successor * S ((S (S ff_i_bpg_value_product)) * ff_v_bpg_value_product) + (ff_s_bpg_value_product))) /\ ff_s_bpg_value_product = ff_r_bpg_value_product * ff_p_bpg_value_product)))))))) -> (exists bpg_gap_value. bpg_gap_value + (1) = (x))

Proof neighborhood

Direct theorem prerequisites

BT0081 pow_zero BT0083 pow_successor_decompose BT000E le_refl BT00PW le_mul_of_one_le_right BT000F le_trans

Direct theorem dependents

BT00Q1 pow_nonzero_of_one_le BT00SN pow_exponent_monotone_from_total BT00XJ pow_le_pow_of_exponent_le

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

46 script commands · 9 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 (5)
pow zeropow successor decomposele reflle mul of one le rightle trans
01Fix variables and assumptionsL1–2

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

  1. L1
    intro a
  2. L2
    intro e
02Induction on eL3–6

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L3
    induction e
  2. L4
    intro x
  3. L5
    intro ha
  4. L6
    intro hx
03Establish hx1L7–16

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

  1. L7
    have hx1 : x = 1
  2. L8
    specialize pow_zero a
  3. L9
    specialize pow_zero 0
  4. L10
    specialize pow_zero x
  5. L11
    apply pow_zero
  6. L12
    refl
  7. L13
    exact hx
  8. L14
    rewrite hx1
  9. L15
    specialize le_refl 1
  10. L16
    exact le_refl
04Fix variables and assumptionsL17–19

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

  1. L17
    intro x
  2. L18
    intro ha
  3. L19
    intro hx
05Establish hstepL20–27

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

  1. L20
    have hstep : ∃ r. Pow(a,e,r) ∧ x = r · aDefinitions: Pow(a,e,r)Original native command in the exact edition
  2. L21
    specialize pow_successor_decompose a
  3. L22
    specialize pow_successor_decompose e
  4. L23
    specialize pow_successor_decompose (S e)
  5. L24
    specialize pow_successor_decompose x
  6. L25
    apply pow_successor_decompose
  7. L26
    refl
  8. L27
    exact hx
06Separate the logical casesL28–29

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

  1. L28
    cases hstep
  2. L29
    cases hstep_witness
07Establish hrL30–34

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

  1. L30
  2. L31
    specialize IH x1
  3. L32
    apply IH
  4. L33
    exact ha
  5. L34
    exact hstep_witness_left
08Establish hrproductL35–44

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

  1. L35
    have hrproduct : Le(x1,x1 · a)Definitions: Le(x1,x1 · a)Original native command in the exact edition
  2. L36
    specialize le_mul_of_one_le_right x1
  3. L37
    specialize le_mul_of_one_le_right a
  4. L38
    apply le_mul_of_one_le_right
  5. L39
    exact ha
  6. L40
    rewrite hstep_witness_right
  7. L41
    specialize le_trans 1
  8. L42
    specialize le_trans x1
  9. L43
    specialize le_trans (x1 * a)
  10. L44
    apply le_trans
09Use earlier factsL45–46

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

  1. L45
    exact hr
  2. L46
    exact hrproduct

Library-wide reading audit

Original defined command ledger · 46 lines
  1. 0001intro a
  2. 0002intro e
  3. 0003induction e
  4. 0004intro x
  5. 0005intro ha
  6. 0006intro hx
  7. 0007have hx1 : x = 1
  8. 0008specialize pow_zero a
  9. 0009specialize pow_zero 0
  10. 0010specialize pow_zero x
  11. 0011apply pow_zero
  12. 0012refl
  13. 0013exact hx
  14. 0014rewrite hx1
  15. 0015specialize le_refl 1
  16. 0016exact le_refl
  17. 0017intro x
  18. 0018intro ha
  19. 0019intro hx
  20. 0020have hstep : ∃ r. Pow(a,e,r) ∧ x = r · a
    Exact native replay linehave hstep : exists r. (exists ff_b_bpg_prefix ff_c_bpg_prefix. ((forall ff_i_bpg_prefix_repeat. (exists ff_lt_bpg_prefix_repeat_bound. ff_lt_bpg_prefix_repeat_bound + S ff_i_bpg_prefix_repeat = e) -> (((exists ff_h_bpg_prefix_repeat_decoded. ff_h_bpg_prefix_repeat_decoded + S (a) = S ((S (ff_i_bpg_prefix_repeat)) * ff_c_bpg_prefix)) /\ exists ff_q_bpg_prefix_repeat_decoded. ff_b_bpg_prefix = ff_q_bpg_prefix_repeat_decoded * S ((S (ff_i_bpg_prefix_repeat)) * ff_c_bpg_prefix) + (a)))) /\ (exists ff_u_bpg_prefix_product ff_v_bpg_prefix_product. ((((exists ff_h_bpg_prefix_product_start. ff_h_bpg_prefix_product_start + S (1) = S ((S (0)) * ff_v_bpg_prefix_product)) /\ exists ff_q_bpg_prefix_product_start. ff_u_bpg_prefix_product = ff_q_bpg_prefix_product_start * S ((S (0)) * ff_v_bpg_prefix_product) + (1))) /\ ((((exists ff_h_bpg_prefix_product_terminal. ff_h_bpg_prefix_product_terminal + S (r) = S ((S (e)) * ff_v_bpg_prefix_product)) /\ exists ff_q_bpg_prefix_product_terminal. ff_u_bpg_prefix_product = ff_q_bpg_prefix_product_terminal * S ((S (e)) * ff_v_bpg_prefix_product) + (r))) /\ forall ff_i_bpg_prefix_product. (exists ff_lt_bpg_prefix_product_bound. ff_lt_bpg_prefix_product_bound + S ff_i_bpg_prefix_product = e) -> exists ff_p_bpg_prefix_product ff_r_bpg_prefix_product ff_s_bpg_prefix_product. ((((exists ff_h_bpg_prefix_product_factor. ff_h_bpg_prefix_product_factor + S (ff_p_bpg_prefix_product) = S ((S (ff_i_bpg_prefix_product)) * ff_c_bpg_prefix)) /\ exists ff_q_bpg_prefix_product_factor. ff_b_bpg_prefix = ff_q_bpg_prefix_product_factor * S ((S (ff_i_bpg_prefix_product)) * ff_c_bpg_prefix) + (ff_p_bpg_prefix_product))) /\ ((((exists ff_h_bpg_prefix_product_partial. ff_h_bpg_prefix_product_partial + S (ff_r_bpg_prefix_product) = S ((S (ff_i_bpg_prefix_product)) * ff_v_bpg_prefix_product)) /\ exists ff_q_bpg_prefix_product_partial. ff_u_bpg_prefix_product = ff_q_bpg_prefix_product_partial * S ((S (ff_i_bpg_prefix_product)) * ff_v_bpg_prefix_product) + (ff_r_bpg_prefix_product))) /\ ((((exists ff_h_bpg_prefix_product_successor. ff_h_bpg_prefix_product_successor + S (ff_s_bpg_prefix_product) = S ((S (S ff_i_bpg_prefix_product)) * ff_v_bpg_prefix_product)) /\ exists ff_q_bpg_prefix_product_successor. ff_u_bpg_prefix_product = ff_q_bpg_prefix_product_successor * S ((S (S ff_i_bpg_prefix_product)) * ff_v_bpg_prefix_product) + (ff_s_bpg_prefix_product))) /\ ff_s_bpg_prefix_product = ff_r_bpg_prefix_product * ff_p_bpg_prefix_product)))))))) /\ x = r * a
  21. 0021specialize pow_successor_decompose a
  22. 0022specialize pow_successor_decompose e
  23. 0023specialize pow_successor_decompose (S e)
  24. 0024specialize pow_successor_decompose x
  25. 0025apply pow_successor_decompose
  26. 0026refl
  27. 0027exact hx
  28. 0028cases hstep
  29. 0029cases hstep_witness
  30. 0030have hr : Lt(0,x1)
    Exact native replay linehave hr : exists k. k + 1 = x1
  31. 0031specialize IH x1
  32. 0032apply IH
  33. 0033exact ha
  34. 0034exact hstep_witness_left
  35. 0035have hrproduct : Le(x1,x1 · a)
    Exact native replay linehave hrproduct : exists k. k + x1 = x1 * a
  36. 0036specialize le_mul_of_one_le_right x1
  37. 0037specialize le_mul_of_one_le_right a
  38. 0038apply le_mul_of_one_le_right
  39. 0039exact ha
  40. 0040rewrite hstep_witness_right
  41. 0041specialize le_trans 1
  42. 0042specialize le_trans x1
  43. 0043specialize le_trans (x1 * a)
  44. 0044apply le_trans
  45. 0045exact hr
  46. 0046exact hrproduct