BT00PY · Bertrand theorem

pow_base_monotone

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

Relational powers are monotone in the base at every 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

∀ a. ∀ b. ∀ e. ∀ x. ∀ y. Le(a,b) → Pow(a,e,x) → Pow(b,e,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 PD0020 Pow

4 occurrences

In local proof propositions

PD0001 Le PD0020 Pow

3 occurrences

Exact expanded native-PA statement
forall a b e x y. (exists bpo_gap_pow_base. bpo_gap_pow_base + (a) = (b)) -> (exists ff_b_bpo_left ff_c_bpo_left. ((forall ff_i_bpo_left_repeat. (exists ff_lt_bpo_left_repeat_bound. ff_lt_bpo_left_repeat_bound + S ff_i_bpo_left_repeat = e) -> (((exists ff_h_bpo_left_repeat_decoded. ff_h_bpo_left_repeat_decoded + S (a) = S ((S (ff_i_bpo_left_repeat)) * ff_c_bpo_left)) /\ exists ff_q_bpo_left_repeat_decoded. ff_b_bpo_left = ff_q_bpo_left_repeat_decoded * S ((S (ff_i_bpo_left_repeat)) * ff_c_bpo_left) + (a)))) /\ (exists ff_u_bpo_left_product ff_v_bpo_left_product. ((((exists ff_h_bpo_left_product_start. ff_h_bpo_left_product_start + S (1) = S ((S (0)) * ff_v_bpo_left_product)) /\ exists ff_q_bpo_left_product_start. ff_u_bpo_left_product = ff_q_bpo_left_product_start * S ((S (0)) * ff_v_bpo_left_product) + (1))) /\ ((((exists ff_h_bpo_left_product_terminal. ff_h_bpo_left_product_terminal + S (x) = S ((S (e)) * ff_v_bpo_left_product)) /\ exists ff_q_bpo_left_product_terminal. ff_u_bpo_left_product = ff_q_bpo_left_product_terminal * S ((S (e)) * ff_v_bpo_left_product) + (x))) /\ forall ff_i_bpo_left_product. (exists ff_lt_bpo_left_product_bound. ff_lt_bpo_left_product_bound + S ff_i_bpo_left_product = e) -> exists ff_p_bpo_left_product ff_r_bpo_left_product ff_s_bpo_left_product. ((((exists ff_h_bpo_left_product_factor. ff_h_bpo_left_product_factor + S (ff_p_bpo_left_product) = S ((S (ff_i_bpo_left_product)) * ff_c_bpo_left)) /\ exists ff_q_bpo_left_product_factor. ff_b_bpo_left = ff_q_bpo_left_product_factor * S ((S (ff_i_bpo_left_product)) * ff_c_bpo_left) + (ff_p_bpo_left_product))) /\ ((((exists ff_h_bpo_left_product_partial. ff_h_bpo_left_product_partial + S (ff_r_bpo_left_product) = S ((S (ff_i_bpo_left_product)) * ff_v_bpo_left_product)) /\ exists ff_q_bpo_left_product_partial. ff_u_bpo_left_product = ff_q_bpo_left_product_partial * S ((S (ff_i_bpo_left_product)) * ff_v_bpo_left_product) + (ff_r_bpo_left_product))) /\ ((((exists ff_h_bpo_left_product_successor. ff_h_bpo_left_product_successor + S (ff_s_bpo_left_product) = S ((S (S ff_i_bpo_left_product)) * ff_v_bpo_left_product)) /\ exists ff_q_bpo_left_product_successor. ff_u_bpo_left_product = ff_q_bpo_left_product_successor * S ((S (S ff_i_bpo_left_product)) * ff_v_bpo_left_product) + (ff_s_bpo_left_product))) /\ ff_s_bpo_left_product = ff_r_bpo_left_product * ff_p_bpo_left_product)))))))) -> (exists ff_b_bpo_right ff_c_bpo_right. ((forall ff_i_bpo_right_repeat. (exists ff_lt_bpo_right_repeat_bound. ff_lt_bpo_right_repeat_bound + S ff_i_bpo_right_repeat = e) -> (((exists ff_h_bpo_right_repeat_decoded. ff_h_bpo_right_repeat_decoded + S (b) = S ((S (ff_i_bpo_right_repeat)) * ff_c_bpo_right)) /\ exists ff_q_bpo_right_repeat_decoded. ff_b_bpo_right = ff_q_bpo_right_repeat_decoded * S ((S (ff_i_bpo_right_repeat)) * ff_c_bpo_right) + (b)))) /\ (exists ff_u_bpo_right_product ff_v_bpo_right_product. ((((exists ff_h_bpo_right_product_start. ff_h_bpo_right_product_start + S (1) = S ((S (0)) * ff_v_bpo_right_product)) /\ exists ff_q_bpo_right_product_start. ff_u_bpo_right_product = ff_q_bpo_right_product_start * S ((S (0)) * ff_v_bpo_right_product) + (1))) /\ ((((exists ff_h_bpo_right_product_terminal. ff_h_bpo_right_product_terminal + S (y) = S ((S (e)) * ff_v_bpo_right_product)) /\ exists ff_q_bpo_right_product_terminal. ff_u_bpo_right_product = ff_q_bpo_right_product_terminal * S ((S (e)) * ff_v_bpo_right_product) + (y))) /\ forall ff_i_bpo_right_product. (exists ff_lt_bpo_right_product_bound. ff_lt_bpo_right_product_bound + S ff_i_bpo_right_product = e) -> exists ff_p_bpo_right_product ff_r_bpo_right_product ff_s_bpo_right_product. ((((exists ff_h_bpo_right_product_factor. ff_h_bpo_right_product_factor + S (ff_p_bpo_right_product) = S ((S (ff_i_bpo_right_product)) * ff_c_bpo_right)) /\ exists ff_q_bpo_right_product_factor. ff_b_bpo_right = ff_q_bpo_right_product_factor * S ((S (ff_i_bpo_right_product)) * ff_c_bpo_right) + (ff_p_bpo_right_product))) /\ ((((exists ff_h_bpo_right_product_partial. ff_h_bpo_right_product_partial + S (ff_r_bpo_right_product) = S ((S (ff_i_bpo_right_product)) * ff_v_bpo_right_product)) /\ exists ff_q_bpo_right_product_partial. ff_u_bpo_right_product = ff_q_bpo_right_product_partial * S ((S (ff_i_bpo_right_product)) * ff_v_bpo_right_product) + (ff_r_bpo_right_product))) /\ ((((exists ff_h_bpo_right_product_successor. ff_h_bpo_right_product_successor + S (ff_s_bpo_right_product) = S ((S (S ff_i_bpo_right_product)) * ff_v_bpo_right_product)) /\ exists ff_q_bpo_right_product_successor. ff_u_bpo_right_product = ff_q_bpo_right_product_successor * S ((S (S ff_i_bpo_right_product)) * ff_v_bpo_right_product) + (ff_s_bpo_right_product))) /\ ff_s_bpo_right_product = ff_r_bpo_right_product * ff_p_bpo_right_product)))))))) -> (exists bpo_gap_pow_result. bpo_gap_pow_result + (x) = (y))

Proof neighborhood

Direct theorem prerequisites

BT0081 pow_zero BT0083 pow_successor_decompose BT000E le_refl BT00PV mul_le_mul

Direct theorem dependents

BT00SW bertrand_h_six_step_transport_from_total BT00SX bertrand_j_six_step_transport_from_total BT00W3 pow_block_bound_from_total BT00WF pow_six_six_le_pow_four_eight_from_total BT00WG pow_six_four_le_pow_four_six_from_total BT00WH pow_three_five_block_plus_one_le_pow_four_four_block_plus_one_from_total BT00WJ pow_two_successor_double_le_pow_four_successor_from_total BT00WQ bertrand_h_root_33_from_total BT00WR bertrand_h_root_34_from_total BT00WS bertrand_h_root_35_from_total BT00WT bertrand_h_root_36_from_total BT00WU bertrand_h_root_37_from_total BT00WV bertrand_j_base_thirty_two_window_from_total BT00X4 bertrand_floor_power_product_le_h_from_total

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

68 script commands · 12 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 (4)
pow zeropow successor decomposele reflmul le mul
01Fix variables and assumptionsL1–3

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro e
02Induction on eL4–9

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

  1. L4
    induction e
  2. L5
    intro x
  3. L6
    intro y
  4. L7
    intro hab
  5. L8
    intro hx
  6. L9
    intro hy
03Establish hx1L10–16

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

  1. L10
    have hx1 : x = 1
  2. L11
    specialize pow_zero a
  3. L12
    specialize pow_zero 0
  4. L13
    specialize pow_zero x
  5. L14
    apply pow_zero
  6. L15
    refl
  7. L16
    exact hx
04Establish hy1L17–26

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

  1. L17
    have hy1 : y = 1
  2. L18
    specialize pow_zero b
  3. L19
    specialize pow_zero 0
  4. L20
    specialize pow_zero y
  5. L21
    apply pow_zero
  6. L22
    refl
  7. L23
    exact hy
  8. L24
    rewrite hx1
  9. L25
    rewrite hy1
  10. L26
    specialize le_refl 1
05Use earlier factsL27–27

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

  1. L27
    exact le_refl
06Fix variables and assumptionsL28–32

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

  1. L28
    intro x
  2. L29
    intro y
  3. L30
    intro hab
  4. L31
    intro hx
  5. L32
    intro hy
07Establish hxstepL33–40

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

  1. L33
    have hxstep : ∃ r. Pow(a,e,r) ∧ x = r · aDefinitions: Pow(a,e,r)Original native command in the exact edition
  2. L34
    specialize pow_successor_decompose a
  3. L35
    specialize pow_successor_decompose e
  4. L36
    specialize pow_successor_decompose (S e)
  5. L37
    specialize pow_successor_decompose x
  6. L38
    apply pow_successor_decompose
  7. L39
    refl
  8. L40
    exact hx
08Separate the logical casesL41–42

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

  1. L41
    cases hxstep
  2. L42
    cases hxstep_witness
09Establish hystepL43–50

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

  1. L43
    have hystep : ∃ s. Pow(b,e,s) ∧ y = s · bDefinitions: Pow(b,e,s)Original native command in the exact edition
  2. L44
    specialize pow_successor_decompose b
  3. L45
    specialize pow_successor_decompose e
  4. L46
    specialize pow_successor_decompose (S e)
  5. L47
    specialize pow_successor_decompose y
  6. L48
    apply pow_successor_decompose
  7. L49
    refl
  8. L50
    exact hy
10Separate the logical casesL51–52

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

  1. L51
    cases hystep
  2. L52
    cases hystep_witness
11Establish hprefL53–62

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

  1. L53
  2. L54
    specialize IH x1
  3. L55
    specialize IH x2
  4. L56
    apply IH
  5. L57
    exact hab
  6. L58
    exact hxstep_witness_left
  7. L59
    exact hystep_witness_left
  8. L60
    rewrite hxstep_witness_right
  9. L61
    rewrite hystep_witness_right
  10. L62
    specialize mul_le_mul x1
12Use earlier factsL63–68

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

  1. L63
    specialize mul_le_mul x2
  2. L64
    specialize mul_le_mul a
  3. L65
    specialize mul_le_mul b
  4. L66
    apply mul_le_mul
  5. L67
    exact hpref
  6. L68
    exact hab

Library-wide reading audit

Original defined command ledger · 68 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro e
  4. 0004induction e
  5. 0005intro x
  6. 0006intro y
  7. 0007intro hab
  8. 0008intro hx
  9. 0009intro hy
  10. 0010have hx1 : x = 1
  11. 0011specialize pow_zero a
  12. 0012specialize pow_zero 0
  13. 0013specialize pow_zero x
  14. 0014apply pow_zero
  15. 0015refl
  16. 0016exact hx
  17. 0017have hy1 : y = 1
  18. 0018specialize pow_zero b
  19. 0019specialize pow_zero 0
  20. 0020specialize pow_zero y
  21. 0021apply pow_zero
  22. 0022refl
  23. 0023exact hy
  24. 0024rewrite hx1
  25. 0025rewrite hy1
  26. 0026specialize le_refl 1
  27. 0027exact le_refl
  28. 0028intro x
  29. 0029intro y
  30. 0030intro hab
  31. 0031intro hx
  32. 0032intro hy
  33. 0033have hxstep : ∃ r. Pow(a,e,r) ∧ x = r · a
    Exact native replay linehave hxstep : exists r. (exists ff_b_bpo_left_prefix ff_c_bpo_left_prefix. ((forall ff_i_bpo_left_prefix_repeat. (exists ff_lt_bpo_left_prefix_repeat_bound. ff_lt_bpo_left_prefix_repeat_bound + S ff_i_bpo_left_prefix_repeat = e) -> (((exists ff_h_bpo_left_prefix_repeat_decoded. ff_h_bpo_left_prefix_repeat_decoded + S (a) = S ((S (ff_i_bpo_left_prefix_repeat)) * ff_c_bpo_left_prefix)) /\ exists ff_q_bpo_left_prefix_repeat_decoded. ff_b_bpo_left_prefix = ff_q_bpo_left_prefix_repeat_decoded * S ((S (ff_i_bpo_left_prefix_repeat)) * ff_c_bpo_left_prefix) + (a)))) /\ (exists ff_u_bpo_left_prefix_product ff_v_bpo_left_prefix_product. ((((exists ff_h_bpo_left_prefix_product_start. ff_h_bpo_left_prefix_product_start + S (1) = S ((S (0)) * ff_v_bpo_left_prefix_product)) /\ exists ff_q_bpo_left_prefix_product_start. ff_u_bpo_left_prefix_product = ff_q_bpo_left_prefix_product_start * S ((S (0)) * ff_v_bpo_left_prefix_product) + (1))) /\ ((((exists ff_h_bpo_left_prefix_product_terminal. ff_h_bpo_left_prefix_product_terminal + S (r) = S ((S (e)) * ff_v_bpo_left_prefix_product)) /\ exists ff_q_bpo_left_prefix_product_terminal. ff_u_bpo_left_prefix_product = ff_q_bpo_left_prefix_product_terminal * S ((S (e)) * ff_v_bpo_left_prefix_product) + (r))) /\ forall ff_i_bpo_left_prefix_product. (exists ff_lt_bpo_left_prefix_product_bound. ff_lt_bpo_left_prefix_product_bound + S ff_i_bpo_left_prefix_product = e) -> exists ff_p_bpo_left_prefix_product ff_r_bpo_left_prefix_product ff_s_bpo_left_prefix_product. ((((exists ff_h_bpo_left_prefix_product_factor. ff_h_bpo_left_prefix_product_factor + S (ff_p_bpo_left_prefix_product) = S ((S (ff_i_bpo_left_prefix_product)) * ff_c_bpo_left_prefix)) /\ exists ff_q_bpo_left_prefix_product_factor. ff_b_bpo_left_prefix = ff_q_bpo_left_prefix_product_factor * S ((S (ff_i_bpo_left_prefix_product)) * ff_c_bpo_left_prefix) + (ff_p_bpo_left_prefix_product))) /\ ((((exists ff_h_bpo_left_prefix_product_partial. ff_h_bpo_left_prefix_product_partial + S (ff_r_bpo_left_prefix_product) = S ((S (ff_i_bpo_left_prefix_product)) * ff_v_bpo_left_prefix_product)) /\ exists ff_q_bpo_left_prefix_product_partial. ff_u_bpo_left_prefix_product = ff_q_bpo_left_prefix_product_partial * S ((S (ff_i_bpo_left_prefix_product)) * ff_v_bpo_left_prefix_product) + (ff_r_bpo_left_prefix_product))) /\ ((((exists ff_h_bpo_left_prefix_product_successor. ff_h_bpo_left_prefix_product_successor + S (ff_s_bpo_left_prefix_product) = S ((S (S ff_i_bpo_left_prefix_product)) * ff_v_bpo_left_prefix_product)) /\ exists ff_q_bpo_left_prefix_product_successor. ff_u_bpo_left_prefix_product = ff_q_bpo_left_prefix_product_successor * S ((S (S ff_i_bpo_left_prefix_product)) * ff_v_bpo_left_prefix_product) + (ff_s_bpo_left_prefix_product))) /\ ff_s_bpo_left_prefix_product = ff_r_bpo_left_prefix_product * ff_p_bpo_left_prefix_product)))))))) /\ x = r * a
  34. 0034specialize pow_successor_decompose a
  35. 0035specialize pow_successor_decompose e
  36. 0036specialize pow_successor_decompose (S e)
  37. 0037specialize pow_successor_decompose x
  38. 0038apply pow_successor_decompose
  39. 0039refl
  40. 0040exact hx
  41. 0041cases hxstep
  42. 0042cases hxstep_witness
  43. 0043have hystep : ∃ s. Pow(b,e,s) ∧ y = s · b
    Exact native replay linehave hystep : exists s. (exists ff_b_bpo_right_prefix ff_c_bpo_right_prefix. ((forall ff_i_bpo_right_prefix_repeat. (exists ff_lt_bpo_right_prefix_repeat_bound. ff_lt_bpo_right_prefix_repeat_bound + S ff_i_bpo_right_prefix_repeat = e) -> (((exists ff_h_bpo_right_prefix_repeat_decoded. ff_h_bpo_right_prefix_repeat_decoded + S (b) = S ((S (ff_i_bpo_right_prefix_repeat)) * ff_c_bpo_right_prefix)) /\ exists ff_q_bpo_right_prefix_repeat_decoded. ff_b_bpo_right_prefix = ff_q_bpo_right_prefix_repeat_decoded * S ((S (ff_i_bpo_right_prefix_repeat)) * ff_c_bpo_right_prefix) + (b)))) /\ (exists ff_u_bpo_right_prefix_product ff_v_bpo_right_prefix_product. ((((exists ff_h_bpo_right_prefix_product_start. ff_h_bpo_right_prefix_product_start + S (1) = S ((S (0)) * ff_v_bpo_right_prefix_product)) /\ exists ff_q_bpo_right_prefix_product_start. ff_u_bpo_right_prefix_product = ff_q_bpo_right_prefix_product_start * S ((S (0)) * ff_v_bpo_right_prefix_product) + (1))) /\ ((((exists ff_h_bpo_right_prefix_product_terminal. ff_h_bpo_right_prefix_product_terminal + S (s) = S ((S (e)) * ff_v_bpo_right_prefix_product)) /\ exists ff_q_bpo_right_prefix_product_terminal. ff_u_bpo_right_prefix_product = ff_q_bpo_right_prefix_product_terminal * S ((S (e)) * ff_v_bpo_right_prefix_product) + (s))) /\ forall ff_i_bpo_right_prefix_product. (exists ff_lt_bpo_right_prefix_product_bound. ff_lt_bpo_right_prefix_product_bound + S ff_i_bpo_right_prefix_product = e) -> exists ff_p_bpo_right_prefix_product ff_r_bpo_right_prefix_product ff_s_bpo_right_prefix_product. ((((exists ff_h_bpo_right_prefix_product_factor. ff_h_bpo_right_prefix_product_factor + S (ff_p_bpo_right_prefix_product) = S ((S (ff_i_bpo_right_prefix_product)) * ff_c_bpo_right_prefix)) /\ exists ff_q_bpo_right_prefix_product_factor. ff_b_bpo_right_prefix = ff_q_bpo_right_prefix_product_factor * S ((S (ff_i_bpo_right_prefix_product)) * ff_c_bpo_right_prefix) + (ff_p_bpo_right_prefix_product))) /\ ((((exists ff_h_bpo_right_prefix_product_partial. ff_h_bpo_right_prefix_product_partial + S (ff_r_bpo_right_prefix_product) = S ((S (ff_i_bpo_right_prefix_product)) * ff_v_bpo_right_prefix_product)) /\ exists ff_q_bpo_right_prefix_product_partial. ff_u_bpo_right_prefix_product = ff_q_bpo_right_prefix_product_partial * S ((S (ff_i_bpo_right_prefix_product)) * ff_v_bpo_right_prefix_product) + (ff_r_bpo_right_prefix_product))) /\ ((((exists ff_h_bpo_right_prefix_product_successor. ff_h_bpo_right_prefix_product_successor + S (ff_s_bpo_right_prefix_product) = S ((S (S ff_i_bpo_right_prefix_product)) * ff_v_bpo_right_prefix_product)) /\ exists ff_q_bpo_right_prefix_product_successor. ff_u_bpo_right_prefix_product = ff_q_bpo_right_prefix_product_successor * S ((S (S ff_i_bpo_right_prefix_product)) * ff_v_bpo_right_prefix_product) + (ff_s_bpo_right_prefix_product))) /\ ff_s_bpo_right_prefix_product = ff_r_bpo_right_prefix_product * ff_p_bpo_right_prefix_product)))))))) /\ y = s * b
  44. 0044specialize pow_successor_decompose b
  45. 0045specialize pow_successor_decompose e
  46. 0046specialize pow_successor_decompose (S e)
  47. 0047specialize pow_successor_decompose y
  48. 0048apply pow_successor_decompose
  49. 0049refl
  50. 0050exact hy
  51. 0051cases hystep
  52. 0052cases hystep_witness
  53. 0053have hpref : Le(x1,x2)
    Exact native replay linehave hpref : exists k. k + x1 = x2
  54. 0054specialize IH x1
  55. 0055specialize IH x2
  56. 0056apply IH
  57. 0057exact hab
  58. 0058exact hxstep_witness_left
  59. 0059exact hystep_witness_left
  60. 0060rewrite hxstep_witness_right
  61. 0061rewrite hystep_witness_right
  62. 0062specialize mul_le_mul x1
  63. 0063specialize mul_le_mul x2
  64. 0064specialize mul_le_mul a
  65. 0065specialize mul_le_mul b
  66. 0066apply mul_le_mul
  67. 0067exact hpref
  68. 0068exact hab