BT00XJ · Bertrand theorem

pow_le_pow_of_exponent_le

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

Relational powers are monotone in the exponent above base 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. ∀ f. ∀ x. ∀ y. Lt(0,p) → Le(e,f) → Pow(p,e,x) → Pow(p,f,y) → Le(x,y)

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 PD0002 Lt PD0020 Pow

5 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0020 Pow

3 occurrences

Exact expanded native-PA statement
forall p e f x y. (exists bcf_le_gap_bppem_base. bcf_le_gap_bppem_base + (1) = p) -> (exists bcf_le_gap_bppem_exponent. bcf_le_gap_bppem_exponent + (e) = f) -> (exists ff_b_bppem_left_power ff_c_bppem_left_power. ((forall ff_i_bppem_left_power_repeat. (exists ff_lt_bppem_left_power_repeat_bound. ff_lt_bppem_left_power_repeat_bound + S ff_i_bppem_left_power_repeat = e) -> (((exists ff_h_bppem_left_power_repeat_decoded. ff_h_bppem_left_power_repeat_decoded + S (p) = S ((S (ff_i_bppem_left_power_repeat)) * ff_c_bppem_left_power)) /\ exists ff_q_bppem_left_power_repeat_decoded. ff_b_bppem_left_power = ff_q_bppem_left_power_repeat_decoded * S ((S (ff_i_bppem_left_power_repeat)) * ff_c_bppem_left_power) + (p)))) /\ (exists ff_u_bppem_left_power_product ff_v_bppem_left_power_product. ((((exists ff_h_bppem_left_power_product_start. ff_h_bppem_left_power_product_start + S (1) = S ((S (0)) * ff_v_bppem_left_power_product)) /\ exists ff_q_bppem_left_power_product_start. ff_u_bppem_left_power_product = ff_q_bppem_left_power_product_start * S ((S (0)) * ff_v_bppem_left_power_product) + (1))) /\ ((((exists ff_h_bppem_left_power_product_terminal. ff_h_bppem_left_power_product_terminal + S (x) = S ((S (e)) * ff_v_bppem_left_power_product)) /\ exists ff_q_bppem_left_power_product_terminal. ff_u_bppem_left_power_product = ff_q_bppem_left_power_product_terminal * S ((S (e)) * ff_v_bppem_left_power_product) + (x))) /\ forall ff_i_bppem_left_power_product. (exists ff_lt_bppem_left_power_product_bound. ff_lt_bppem_left_power_product_bound + S ff_i_bppem_left_power_product = e) -> exists ff_p_bppem_left_power_product ff_r_bppem_left_power_product ff_s_bppem_left_power_product. ((((exists ff_h_bppem_left_power_product_factor. ff_h_bppem_left_power_product_factor + S (ff_p_bppem_left_power_product) = S ((S (ff_i_bppem_left_power_product)) * ff_c_bppem_left_power)) /\ exists ff_q_bppem_left_power_product_factor. ff_b_bppem_left_power = ff_q_bppem_left_power_product_factor * S ((S (ff_i_bppem_left_power_product)) * ff_c_bppem_left_power) + (ff_p_bppem_left_power_product))) /\ ((((exists ff_h_bppem_left_power_product_partial. ff_h_bppem_left_power_product_partial + S (ff_r_bppem_left_power_product) = S ((S (ff_i_bppem_left_power_product)) * ff_v_bppem_left_power_product)) /\ exists ff_q_bppem_left_power_product_partial. ff_u_bppem_left_power_product = ff_q_bppem_left_power_product_partial * S ((S (ff_i_bppem_left_power_product)) * ff_v_bppem_left_power_product) + (ff_r_bppem_left_power_product))) /\ ((((exists ff_h_bppem_left_power_product_successor. ff_h_bppem_left_power_product_successor + S (ff_s_bppem_left_power_product) = S ((S (S ff_i_bppem_left_power_product)) * ff_v_bppem_left_power_product)) /\ exists ff_q_bppem_left_power_product_successor. ff_u_bppem_left_power_product = ff_q_bppem_left_power_product_successor * S ((S (S ff_i_bppem_left_power_product)) * ff_v_bppem_left_power_product) + (ff_s_bppem_left_power_product))) /\ ff_s_bppem_left_power_product = ff_r_bppem_left_power_product * ff_p_bppem_left_power_product)))))))) -> (exists ff_b_bppem_right_power ff_c_bppem_right_power. ((forall ff_i_bppem_right_power_repeat. (exists ff_lt_bppem_right_power_repeat_bound. ff_lt_bppem_right_power_repeat_bound + S ff_i_bppem_right_power_repeat = f) -> (((exists ff_h_bppem_right_power_repeat_decoded. ff_h_bppem_right_power_repeat_decoded + S (p) = S ((S (ff_i_bppem_right_power_repeat)) * ff_c_bppem_right_power)) /\ exists ff_q_bppem_right_power_repeat_decoded. ff_b_bppem_right_power = ff_q_bppem_right_power_repeat_decoded * S ((S (ff_i_bppem_right_power_repeat)) * ff_c_bppem_right_power) + (p)))) /\ (exists ff_u_bppem_right_power_product ff_v_bppem_right_power_product. ((((exists ff_h_bppem_right_power_product_start. ff_h_bppem_right_power_product_start + S (1) = S ((S (0)) * ff_v_bppem_right_power_product)) /\ exists ff_q_bppem_right_power_product_start. ff_u_bppem_right_power_product = ff_q_bppem_right_power_product_start * S ((S (0)) * ff_v_bppem_right_power_product) + (1))) /\ ((((exists ff_h_bppem_right_power_product_terminal. ff_h_bppem_right_power_product_terminal + S (y) = S ((S (f)) * ff_v_bppem_right_power_product)) /\ exists ff_q_bppem_right_power_product_terminal. ff_u_bppem_right_power_product = ff_q_bppem_right_power_product_terminal * S ((S (f)) * ff_v_bppem_right_power_product) + (y))) /\ forall ff_i_bppem_right_power_product. (exists ff_lt_bppem_right_power_product_bound. ff_lt_bppem_right_power_product_bound + S ff_i_bppem_right_power_product = f) -> exists ff_p_bppem_right_power_product ff_r_bppem_right_power_product ff_s_bppem_right_power_product. ((((exists ff_h_bppem_right_power_product_factor. ff_h_bppem_right_power_product_factor + S (ff_p_bppem_right_power_product) = S ((S (ff_i_bppem_right_power_product)) * ff_c_bppem_right_power)) /\ exists ff_q_bppem_right_power_product_factor. ff_b_bppem_right_power = ff_q_bppem_right_power_product_factor * S ((S (ff_i_bppem_right_power_product)) * ff_c_bppem_right_power) + (ff_p_bppem_right_power_product))) /\ ((((exists ff_h_bppem_right_power_product_partial. ff_h_bppem_right_power_product_partial + S (ff_r_bppem_right_power_product) = S ((S (ff_i_bppem_right_power_product)) * ff_v_bppem_right_power_product)) /\ exists ff_q_bppem_right_power_product_partial. ff_u_bppem_right_power_product = ff_q_bppem_right_power_product_partial * S ((S (ff_i_bppem_right_power_product)) * ff_v_bppem_right_power_product) + (ff_r_bppem_right_power_product))) /\ ((((exists ff_h_bppem_right_power_product_successor. ff_h_bppem_right_power_product_successor + S (ff_s_bppem_right_power_product) = S ((S (S ff_i_bppem_right_power_product)) * ff_v_bppem_right_power_product)) /\ exists ff_q_bppem_right_power_product_successor. ff_u_bppem_right_power_product = ff_q_bppem_right_power_product_successor * S ((S (S ff_i_bppem_right_power_product)) * ff_v_bppem_right_power_product) + (ff_s_bppem_right_power_product))) /\ ff_s_bppem_right_power_product = ff_r_bppem_right_power_product * ff_p_bppem_right_power_product)))))))) -> (exists bcf_le_gap_bppem_result. bcf_le_gap_bppem_result + (x) = y)

Proof neighborhood

Direct theorem prerequisites

BT0080 pow_exists BT0002 add_comm BT009X pow_add BT00Q0 one_le_pow BT00PW le_mul_of_one_le_right

Direct theorem dependents

BT00XK pow_tail_strict_of_square BT00Y5 central_binom_prime_power_contribution_le_double

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 · 9 reading checkpoints · 5 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 existsadd commpow addone le powle mul of one le right
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 x
  5. L5
    intro y
  6. L6
    intro hbase
  7. L7
    intro hexponent
  8. L8
    intro hx
  9. L9
    intro hy
02Separate the logical casesL10–10

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

  1. L10
    cases hexponent
03Establish hgap_powerL11–14

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

  1. L11
    have hgap_power : ∃ z. Pow(p,x1,z)Definitions: Pow(p,x1,z)Original native command in the exact edition
  2. L12
    specialize pow_exists p
  3. L13
    specialize pow_exists x1
  4. L14
    exact pow_exists
04Separate the logical casesL15–15

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

  1. L15
    cases hgap_power
05Establish hsumL16–20

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

  1. L16
    have hsum : f = e + x1
  2. L17
    trans x1 + e
  3. L18
    symm
  4. L19
    exact hexponent_witness
  5. L20
    apply add_comm
06Establish hfactorL21–30

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

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

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

  1. L31
    exact hx
  2. L32
    exact hgap_power_witness
  3. L33
    exact hy
08Establish hgap_orderL34–40

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

  1. L34
    have hgap_order : Lt(0,x2)Definitions: Lt(0,x2)Original native command in the exact edition
  2. L35
    specialize one_le_pow p
  3. L36
    specialize one_le_pow x1
  4. L37
    specialize one_le_pow x2
  5. L38
    apply one_le_pow
  6. L39
    exact hbase
  7. L40
    exact hgap_power_witness
09Establish hproduct_orderL41–47

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. L41
    have hproduct_order : Le(x,x · x2)Definitions: Le(x,x · x2)Original native command in the exact edition
  2. L42
    specialize le_mul_of_one_le_right x
  3. L43
    specialize le_mul_of_one_le_right x2
  4. L44
    apply le_mul_of_one_le_right
  5. L45
    exact hgap_order
  6. L46
    rewrite hfactor
  7. L47
    exact hproduct_order

Library-wide reading audit

Original defined command ledger · 47 lines
  1. 0001intro p
  2. 0002intro e
  3. 0003intro f
  4. 0004intro x
  5. 0005intro y
  6. 0006intro hbase
  7. 0007intro hexponent
  8. 0008intro hx
  9. 0009intro hy
  10. 0010cases hexponent
  11. 0011have hgap_power : ∃ z. Pow(p,x1,z)
    Exact native replay linehave hgap_power : exists z. (exists ff_b_bppem_gap_power ff_c_bppem_gap_power. ((forall ff_i_bppem_gap_power_repeat. (exists ff_lt_bppem_gap_power_repeat_bound. ff_lt_bppem_gap_power_repeat_bound + S ff_i_bppem_gap_power_repeat = x1) -> (((exists ff_h_bppem_gap_power_repeat_decoded. ff_h_bppem_gap_power_repeat_decoded + S (p) = S ((S (ff_i_bppem_gap_power_repeat)) * ff_c_bppem_gap_power)) /\ exists ff_q_bppem_gap_power_repeat_decoded. ff_b_bppem_gap_power = ff_q_bppem_gap_power_repeat_decoded * S ((S (ff_i_bppem_gap_power_repeat)) * ff_c_bppem_gap_power) + (p)))) /\ (exists ff_u_bppem_gap_power_product ff_v_bppem_gap_power_product. ((((exists ff_h_bppem_gap_power_product_start. ff_h_bppem_gap_power_product_start + S (1) = S ((S (0)) * ff_v_bppem_gap_power_product)) /\ exists ff_q_bppem_gap_power_product_start. ff_u_bppem_gap_power_product = ff_q_bppem_gap_power_product_start * S ((S (0)) * ff_v_bppem_gap_power_product) + (1))) /\ ((((exists ff_h_bppem_gap_power_product_terminal. ff_h_bppem_gap_power_product_terminal + S (z) = S ((S (x1)) * ff_v_bppem_gap_power_product)) /\ exists ff_q_bppem_gap_power_product_terminal. ff_u_bppem_gap_power_product = ff_q_bppem_gap_power_product_terminal * S ((S (x1)) * ff_v_bppem_gap_power_product) + (z))) /\ forall ff_i_bppem_gap_power_product. (exists ff_lt_bppem_gap_power_product_bound. ff_lt_bppem_gap_power_product_bound + S ff_i_bppem_gap_power_product = x1) -> exists ff_p_bppem_gap_power_product ff_r_bppem_gap_power_product ff_s_bppem_gap_power_product. ((((exists ff_h_bppem_gap_power_product_factor. ff_h_bppem_gap_power_product_factor + S (ff_p_bppem_gap_power_product) = S ((S (ff_i_bppem_gap_power_product)) * ff_c_bppem_gap_power)) /\ exists ff_q_bppem_gap_power_product_factor. ff_b_bppem_gap_power = ff_q_bppem_gap_power_product_factor * S ((S (ff_i_bppem_gap_power_product)) * ff_c_bppem_gap_power) + (ff_p_bppem_gap_power_product))) /\ ((((exists ff_h_bppem_gap_power_product_partial. ff_h_bppem_gap_power_product_partial + S (ff_r_bppem_gap_power_product) = S ((S (ff_i_bppem_gap_power_product)) * ff_v_bppem_gap_power_product)) /\ exists ff_q_bppem_gap_power_product_partial. ff_u_bppem_gap_power_product = ff_q_bppem_gap_power_product_partial * S ((S (ff_i_bppem_gap_power_product)) * ff_v_bppem_gap_power_product) + (ff_r_bppem_gap_power_product))) /\ ((((exists ff_h_bppem_gap_power_product_successor. ff_h_bppem_gap_power_product_successor + S (ff_s_bppem_gap_power_product) = S ((S (S ff_i_bppem_gap_power_product)) * ff_v_bppem_gap_power_product)) /\ exists ff_q_bppem_gap_power_product_successor. ff_u_bppem_gap_power_product = ff_q_bppem_gap_power_product_successor * S ((S (S ff_i_bppem_gap_power_product)) * ff_v_bppem_gap_power_product) + (ff_s_bppem_gap_power_product))) /\ ff_s_bppem_gap_power_product = ff_r_bppem_gap_power_product * ff_p_bppem_gap_power_product))))))))
  12. 0012specialize pow_exists p
  13. 0013specialize pow_exists x1
  14. 0014exact pow_exists
  15. 0015cases hgap_power
  16. 0016have hsum : f = e + x1
  17. 0017trans x1 + e
  18. 0018symm
  19. 0019exact hexponent_witness
  20. 0020apply add_comm
  21. 0021have hfactor : y = x * x2
  22. 0022specialize pow_add p
  23. 0023specialize pow_add e
  24. 0024specialize pow_add x1
  25. 0025specialize pow_add f
  26. 0026specialize pow_add x
  27. 0027specialize pow_add x2
  28. 0028specialize pow_add y
  29. 0029apply pow_add
  30. 0030exact hsum
  31. 0031exact hx
  32. 0032exact hgap_power_witness
  33. 0033exact hy
  34. 0034have hgap_order : Lt(0,x2)
    Exact native replay linehave hgap_order : exists bcf_le_gap_bppem_gap_power_order. bcf_le_gap_bppem_gap_power_order + (1) = x2
  35. 0035specialize one_le_pow p
  36. 0036specialize one_le_pow x1
  37. 0037specialize one_le_pow x2
  38. 0038apply one_le_pow
  39. 0039exact hbase
  40. 0040exact hgap_power_witness
  41. 0041have hproduct_order : Le(x,x · x2)
    Exact native replay linehave hproduct_order : exists bcf_le_gap_bppem_product_order. bcf_le_gap_bppem_product_order + (x) = x * x2
  42. 0042specialize le_mul_of_one_le_right x
  43. 0043specialize le_mul_of_one_le_right x2
  44. 0044apply le_mul_of_one_le_right
  45. 0045exact hgap_order
  46. 0046rewrite hfactor
  47. 0047exact hproduct_order