BT00QF · Bertrand theorem

prime_power_exponent_le

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

The exponent of a relational power at a prime base is bounded by its value.

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. ∀ x. Prime(p) → Pow(p,e,x) → Le(e,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

PD0001 Le PD0004 Prime PD0020 Pow

3 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0020 Pow

6 occurrences

Exact expanded native-PA statement
forall p e x. ((~(p = 1) /\ forall frm_prime_left_bpvl_prime frm_prime_right_bpvl_prime. p = frm_prime_left_bpvl_prime * frm_prime_right_bpvl_prime -> frm_prime_left_bpvl_prime = 1 \/ frm_prime_right_bpvl_prime = 1)) -> (exists ff_b_bpvl_exponent_bound ff_c_bpvl_exponent_bound. ((forall ff_i_bpvl_exponent_bound_repeat. (exists ff_lt_bpvl_exponent_bound_repeat_bound. ff_lt_bpvl_exponent_bound_repeat_bound + S ff_i_bpvl_exponent_bound_repeat = e) -> (((exists ff_h_bpvl_exponent_bound_repeat_decoded. ff_h_bpvl_exponent_bound_repeat_decoded + S (p) = S ((S (ff_i_bpvl_exponent_bound_repeat)) * ff_c_bpvl_exponent_bound)) /\ exists ff_q_bpvl_exponent_bound_repeat_decoded. ff_b_bpvl_exponent_bound = ff_q_bpvl_exponent_bound_repeat_decoded * S ((S (ff_i_bpvl_exponent_bound_repeat)) * ff_c_bpvl_exponent_bound) + (p)))) /\ (exists ff_u_bpvl_exponent_bound_product ff_v_bpvl_exponent_bound_product. ((((exists ff_h_bpvl_exponent_bound_product_start. ff_h_bpvl_exponent_bound_product_start + S (1) = S ((S (0)) * ff_v_bpvl_exponent_bound_product)) /\ exists ff_q_bpvl_exponent_bound_product_start. ff_u_bpvl_exponent_bound_product = ff_q_bpvl_exponent_bound_product_start * S ((S (0)) * ff_v_bpvl_exponent_bound_product) + (1))) /\ ((((exists ff_h_bpvl_exponent_bound_product_terminal. ff_h_bpvl_exponent_bound_product_terminal + S (x) = S ((S (e)) * ff_v_bpvl_exponent_bound_product)) /\ exists ff_q_bpvl_exponent_bound_product_terminal. ff_u_bpvl_exponent_bound_product = ff_q_bpvl_exponent_bound_product_terminal * S ((S (e)) * ff_v_bpvl_exponent_bound_product) + (x))) /\ forall ff_i_bpvl_exponent_bound_product. (exists ff_lt_bpvl_exponent_bound_product_bound. ff_lt_bpvl_exponent_bound_product_bound + S ff_i_bpvl_exponent_bound_product = e) -> exists ff_p_bpvl_exponent_bound_product ff_r_bpvl_exponent_bound_product ff_s_bpvl_exponent_bound_product. ((((exists ff_h_bpvl_exponent_bound_product_factor. ff_h_bpvl_exponent_bound_product_factor + S (ff_p_bpvl_exponent_bound_product) = S ((S (ff_i_bpvl_exponent_bound_product)) * ff_c_bpvl_exponent_bound)) /\ exists ff_q_bpvl_exponent_bound_product_factor. ff_b_bpvl_exponent_bound = ff_q_bpvl_exponent_bound_product_factor * S ((S (ff_i_bpvl_exponent_bound_product)) * ff_c_bpvl_exponent_bound) + (ff_p_bpvl_exponent_bound_product))) /\ ((((exists ff_h_bpvl_exponent_bound_product_partial. ff_h_bpvl_exponent_bound_product_partial + S (ff_r_bpvl_exponent_bound_product) = S ((S (ff_i_bpvl_exponent_bound_product)) * ff_v_bpvl_exponent_bound_product)) /\ exists ff_q_bpvl_exponent_bound_product_partial. ff_u_bpvl_exponent_bound_product = ff_q_bpvl_exponent_bound_product_partial * S ((S (ff_i_bpvl_exponent_bound_product)) * ff_v_bpvl_exponent_bound_product) + (ff_r_bpvl_exponent_bound_product))) /\ ((((exists ff_h_bpvl_exponent_bound_product_successor. ff_h_bpvl_exponent_bound_product_successor + S (ff_s_bpvl_exponent_bound_product) = S ((S (S ff_i_bpvl_exponent_bound_product)) * ff_v_bpvl_exponent_bound_product)) /\ exists ff_q_bpvl_exponent_bound_product_successor. ff_u_bpvl_exponent_bound_product = ff_q_bpvl_exponent_bound_product_successor * S ((S (S ff_i_bpvl_exponent_bound_product)) * ff_v_bpvl_exponent_bound_product) + (ff_s_bpvl_exponent_bound_product))) /\ ff_s_bpvl_exponent_bound_product = ff_r_bpvl_exponent_bound_product * ff_p_bpvl_exponent_bound_product)))))))) -> (exists bpv_gap_power_exponent. bpv_gap_power_exponent + e = x)

Proof neighborhood

Direct theorem prerequisites

BT0083 pow_successor_decompose BT000W zero_le BT003G prime_nonzero BT0010 one_le_of_ne_zero BT00Q1 pow_nonzero_of_one_le BT00QD prime_two_le BT0016 succ_le_succ BT00QE succ_le_mul_of_two_le_right BT000F le_trans

Direct theorem dependents

BT00QG prime_power_divides_exponent_le_value BT00SA prime_power_quotient_tail_zero BT00XO prime_power_quotient_zero_of_exponent_gt

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

67 script commands · 12 reading checkpoints · 8 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 (9)
pow successor decomposezero leprime nonzeroone le of ne zeropow nonzero of one leprime two lesucc le succsucc le mul of two le rightle trans
01Fix variables and assumptionsL1–2

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

  1. L1
    intro p
  2. L2
    intro e
02Induction on eL3–11

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 hp
  4. L6
    intro hx
  5. L7
    specialize zero_le x
  6. L8
    exact zero_le
  7. L9
    intro x
  8. L10
    intro hp
  9. L11
    intro hx
03Establish hstepL12–19

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

  1. L12
    have hstep : ∃ r. Pow(p,e,r) ∧ x = r · pDefinitions: Pow(p,e,r)Original native command in the exact edition
  2. L13
    specialize pow_successor_decompose p
  3. L14
    specialize pow_successor_decompose e
  4. L15
    specialize pow_successor_decompose (S e)
  5. L16
    specialize pow_successor_decompose x
  6. L17
    apply pow_successor_decompose
  7. L18
    refl
  8. L19
    exact hx
04Separate the logical casesL20–21

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

  1. L20
    cases hstep
  2. L21
    cases hstep_witness
05Establish he_prefixL22–26

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

  1. L22
    have he_prefix : Le(e,x1)Definitions: Le(e,x1)Original native command in the exact edition
  2. L23
    specialize IH x1
  3. L24
    apply IH
  4. L25
    exact hp
  5. L26
    exact hstep_witness_left
06Establish hp0L27–32

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

  1. L27
    have hp0 : ~(p = 0)
  2. L28
    intro hpzero
  3. L29
    specialize prime_nonzero p
  4. L30
    apply prime_nonzero
  5. L31
    exact hp
  6. L32
    exact hpzero
07Establish hp1L33–36

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

  1. L33
  2. L34
    specialize one_le_of_ne_zero p
  3. L35
    apply one_le_of_ne_zero
  4. L36
    exact hp0
08Establish hprefix0L37–45

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

  1. L37
    have hprefix0 : ~(x1 = 0)
  2. L38
    intro hprefixzero
  3. L39
    specialize pow_nonzero_of_one_le p
  4. L40
    specialize pow_nonzero_of_one_le e
  5. L41
    specialize pow_nonzero_of_one_le x1
  6. L42
    apply pow_nonzero_of_one_le
  7. L43
    exact hp1
  8. L44
    exact hstep_witness_left
  9. L45
    exact hprefixzero
09Establish hp2L46–49

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

  1. L46
  2. L47
    specialize prime_two_le p
  3. L48
    apply prime_two_le
  4. L49
    exact hp
10Establish hprefix_stepL50–55

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

  1. L50
    have hprefix_step : Lt(x1,x1 · p)Definitions: Lt(x1,x1 · p)Original native command in the exact edition
  2. L51
    specialize succ_le_mul_of_two_le_right x1
  3. L52
    specialize succ_le_mul_of_two_le_right p
  4. L53
    apply succ_le_mul_of_two_le_right
  5. L54
    exact hprefix0
  6. L55
    exact hp2
11Establish he_stepL56–65

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

  1. L56
    have he_step : Lt(e,S x1)Definitions: Lt(e,S x1)Original native command in the exact edition
  2. L57
    specialize succ_le_succ e
  3. L58
    specialize succ_le_succ x1
  4. L59
    apply succ_le_succ
  5. L60
    exact he_prefix
  6. L61
    rewrite hstep_witness_right
  7. L62
    specialize le_trans (S e)
  8. L63
    specialize le_trans (S x1)
  9. L64
    specialize le_trans (x1 * p)
  10. L65
    apply le_trans
12Use earlier factsL66–67

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

  1. L66
    exact he_step
  2. L67
    exact hprefix_step

Library-wide reading audit

Original defined command ledger · 67 lines
  1. 0001intro p
  2. 0002intro e
  3. 0003induction e
  4. 0004intro x
  5. 0005intro hp
  6. 0006intro hx
  7. 0007specialize zero_le x
  8. 0008exact zero_le
  9. 0009intro x
  10. 0010intro hp
  11. 0011intro hx
  12. 0012have hstep : ∃ r. Pow(p,e,r) ∧ x = r · p
    Exact native replay linehave hstep : exists r. (exists ff_b_bpvl_prefix ff_c_bpvl_prefix. ((forall ff_i_bpvl_prefix_repeat. (exists ff_lt_bpvl_prefix_repeat_bound. ff_lt_bpvl_prefix_repeat_bound + S ff_i_bpvl_prefix_repeat = e) -> (((exists ff_h_bpvl_prefix_repeat_decoded. ff_h_bpvl_prefix_repeat_decoded + S (p) = S ((S (ff_i_bpvl_prefix_repeat)) * ff_c_bpvl_prefix)) /\ exists ff_q_bpvl_prefix_repeat_decoded. ff_b_bpvl_prefix = ff_q_bpvl_prefix_repeat_decoded * S ((S (ff_i_bpvl_prefix_repeat)) * ff_c_bpvl_prefix) + (p)))) /\ (exists ff_u_bpvl_prefix_product ff_v_bpvl_prefix_product. ((((exists ff_h_bpvl_prefix_product_start. ff_h_bpvl_prefix_product_start + S (1) = S ((S (0)) * ff_v_bpvl_prefix_product)) /\ exists ff_q_bpvl_prefix_product_start. ff_u_bpvl_prefix_product = ff_q_bpvl_prefix_product_start * S ((S (0)) * ff_v_bpvl_prefix_product) + (1))) /\ ((((exists ff_h_bpvl_prefix_product_terminal. ff_h_bpvl_prefix_product_terminal + S (r) = S ((S (e)) * ff_v_bpvl_prefix_product)) /\ exists ff_q_bpvl_prefix_product_terminal. ff_u_bpvl_prefix_product = ff_q_bpvl_prefix_product_terminal * S ((S (e)) * ff_v_bpvl_prefix_product) + (r))) /\ forall ff_i_bpvl_prefix_product. (exists ff_lt_bpvl_prefix_product_bound. ff_lt_bpvl_prefix_product_bound + S ff_i_bpvl_prefix_product = e) -> exists ff_p_bpvl_prefix_product ff_r_bpvl_prefix_product ff_s_bpvl_prefix_product. ((((exists ff_h_bpvl_prefix_product_factor. ff_h_bpvl_prefix_product_factor + S (ff_p_bpvl_prefix_product) = S ((S (ff_i_bpvl_prefix_product)) * ff_c_bpvl_prefix)) /\ exists ff_q_bpvl_prefix_product_factor. ff_b_bpvl_prefix = ff_q_bpvl_prefix_product_factor * S ((S (ff_i_bpvl_prefix_product)) * ff_c_bpvl_prefix) + (ff_p_bpvl_prefix_product))) /\ ((((exists ff_h_bpvl_prefix_product_partial. ff_h_bpvl_prefix_product_partial + S (ff_r_bpvl_prefix_product) = S ((S (ff_i_bpvl_prefix_product)) * ff_v_bpvl_prefix_product)) /\ exists ff_q_bpvl_prefix_product_partial. ff_u_bpvl_prefix_product = ff_q_bpvl_prefix_product_partial * S ((S (ff_i_bpvl_prefix_product)) * ff_v_bpvl_prefix_product) + (ff_r_bpvl_prefix_product))) /\ ((((exists ff_h_bpvl_prefix_product_successor. ff_h_bpvl_prefix_product_successor + S (ff_s_bpvl_prefix_product) = S ((S (S ff_i_bpvl_prefix_product)) * ff_v_bpvl_prefix_product)) /\ exists ff_q_bpvl_prefix_product_successor. ff_u_bpvl_prefix_product = ff_q_bpvl_prefix_product_successor * S ((S (S ff_i_bpvl_prefix_product)) * ff_v_bpvl_prefix_product) + (ff_s_bpvl_prefix_product))) /\ ff_s_bpvl_prefix_product = ff_r_bpvl_prefix_product * ff_p_bpvl_prefix_product)))))))) /\ x = r * p
  13. 0013specialize pow_successor_decompose p
  14. 0014specialize pow_successor_decompose e
  15. 0015specialize pow_successor_decompose (S e)
  16. 0016specialize pow_successor_decompose x
  17. 0017apply pow_successor_decompose
  18. 0018refl
  19. 0019exact hx
  20. 0020cases hstep
  21. 0021cases hstep_witness
  22. 0022have he_prefix : Le(e,x1)
    Exact native replay linehave he_prefix : exists k. k + e = x1
  23. 0023specialize IH x1
  24. 0024apply IH
  25. 0025exact hp
  26. 0026exact hstep_witness_left
  27. 0027have hp0 : ~(p = 0)
  28. 0028intro hpzero
  29. 0029specialize prime_nonzero p
  30. 0030apply prime_nonzero
  31. 0031exact hp
  32. 0032exact hpzero
  33. 0033have hp1 : Lt(0,p)
    Exact native replay linehave hp1 : exists k. k + 1 = p
  34. 0034specialize one_le_of_ne_zero p
  35. 0035apply one_le_of_ne_zero
  36. 0036exact hp0
  37. 0037have hprefix0 : ~(x1 = 0)
  38. 0038intro hprefixzero
  39. 0039specialize pow_nonzero_of_one_le p
  40. 0040specialize pow_nonzero_of_one_le e
  41. 0041specialize pow_nonzero_of_one_le x1
  42. 0042apply pow_nonzero_of_one_le
  43. 0043exact hp1
  44. 0044exact hstep_witness_left
  45. 0045exact hprefixzero
  46. 0046have hp2 : Lt(1,p)
    Exact native replay linehave hp2 : exists k. k + 2 = p
  47. 0047specialize prime_two_le p
  48. 0048apply prime_two_le
  49. 0049exact hp
  50. 0050have hprefix_step : Lt(x1,x1 · p)
    Exact native replay linehave hprefix_step : exists k. k + S x1 = x1 * p
  51. 0051specialize succ_le_mul_of_two_le_right x1
  52. 0052specialize succ_le_mul_of_two_le_right p
  53. 0053apply succ_le_mul_of_two_le_right
  54. 0054exact hprefix0
  55. 0055exact hp2
  56. 0056have he_step : Lt(e,S x1)
    Exact native replay linehave he_step : exists k. k + S e = S x1
  57. 0057specialize succ_le_succ e
  58. 0058specialize succ_le_succ x1
  59. 0059apply succ_le_succ
  60. 0060exact he_prefix
  61. 0061rewrite hstep_witness_right
  62. 0062specialize le_trans (S e)
  63. 0063specialize le_trans (S x1)
  64. 0064specialize le_trans (x1 * p)
  65. 0065apply le_trans
  66. 0066exact he_step
  67. 0067exact hprefix_step