BT00SN · Bertrand theorem

pow_exponent_monotone_from_total

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

Exponent monotonicity reuses one supplied power-totality proof.

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. ∀ f. ∀ x. ∀ y. (∀ z. ∀ n. ∃ m. Pow(z,n,m)) → Lt(0,a) → Le(e,f) → Pow(a,e,x) → Pow(a,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

6 occurrences

In local proof propositions

PD0002 Lt PD0020 Pow

2 occurrences

Exact expanded native-PA statement
forall a e f x y. (forall bpt_a_exponent bpt_e_exponent. exists bpt_x_exponent. (exists ff_b_bpt_value_exponent ff_c_bpt_value_exponent. ((forall ff_i_bpt_value_exponent_repeat. (exists ff_lt_bpt_value_exponent_repeat_bound. ff_lt_bpt_value_exponent_repeat_bound + S ff_i_bpt_value_exponent_repeat = bpt_e_exponent) -> (((exists ff_h_bpt_value_exponent_repeat_decoded. ff_h_bpt_value_exponent_repeat_decoded + S (bpt_a_exponent) = S ((S (ff_i_bpt_value_exponent_repeat)) * ff_c_bpt_value_exponent)) /\ exists ff_q_bpt_value_exponent_repeat_decoded. ff_b_bpt_value_exponent = ff_q_bpt_value_exponent_repeat_decoded * S ((S (ff_i_bpt_value_exponent_repeat)) * ff_c_bpt_value_exponent) + (bpt_a_exponent)))) /\ (exists ff_u_bpt_value_exponent_product ff_v_bpt_value_exponent_product. ((((exists ff_h_bpt_value_exponent_product_start. ff_h_bpt_value_exponent_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_exponent_product)) /\ exists ff_q_bpt_value_exponent_product_start. ff_u_bpt_value_exponent_product = ff_q_bpt_value_exponent_product_start * S ((S (0)) * ff_v_bpt_value_exponent_product) + (1))) /\ ((((exists ff_h_bpt_value_exponent_product_terminal. ff_h_bpt_value_exponent_product_terminal + S (bpt_x_exponent) = S ((S (bpt_e_exponent)) * ff_v_bpt_value_exponent_product)) /\ exists ff_q_bpt_value_exponent_product_terminal. ff_u_bpt_value_exponent_product = ff_q_bpt_value_exponent_product_terminal * S ((S (bpt_e_exponent)) * ff_v_bpt_value_exponent_product) + (bpt_x_exponent))) /\ forall ff_i_bpt_value_exponent_product. (exists ff_lt_bpt_value_exponent_product_bound. ff_lt_bpt_value_exponent_product_bound + S ff_i_bpt_value_exponent_product = bpt_e_exponent) -> exists ff_p_bpt_value_exponent_product ff_r_bpt_value_exponent_product ff_s_bpt_value_exponent_product. ((((exists ff_h_bpt_value_exponent_product_factor. ff_h_bpt_value_exponent_product_factor + S (ff_p_bpt_value_exponent_product) = S ((S (ff_i_bpt_value_exponent_product)) * ff_c_bpt_value_exponent)) /\ exists ff_q_bpt_value_exponent_product_factor. ff_b_bpt_value_exponent = ff_q_bpt_value_exponent_product_factor * S ((S (ff_i_bpt_value_exponent_product)) * ff_c_bpt_value_exponent) + (ff_p_bpt_value_exponent_product))) /\ ((((exists ff_h_bpt_value_exponent_product_partial. ff_h_bpt_value_exponent_product_partial + S (ff_r_bpt_value_exponent_product) = S ((S (ff_i_bpt_value_exponent_product)) * ff_v_bpt_value_exponent_product)) /\ exists ff_q_bpt_value_exponent_product_partial. ff_u_bpt_value_exponent_product = ff_q_bpt_value_exponent_product_partial * S ((S (ff_i_bpt_value_exponent_product)) * ff_v_bpt_value_exponent_product) + (ff_r_bpt_value_exponent_product))) /\ ((((exists ff_h_bpt_value_exponent_product_successor. ff_h_bpt_value_exponent_product_successor + S (ff_s_bpt_value_exponent_product) = S ((S (S ff_i_bpt_value_exponent_product)) * ff_v_bpt_value_exponent_product)) /\ exists ff_q_bpt_value_exponent_product_successor. ff_u_bpt_value_exponent_product = ff_q_bpt_value_exponent_product_successor * S ((S (S ff_i_bpt_value_exponent_product)) * ff_v_bpt_value_exponent_product) + (ff_s_bpt_value_exponent_product))) /\ ff_s_bpt_value_exponent_product = ff_r_bpt_value_exponent_product * ff_p_bpt_value_exponent_product))))))))) -> (exists bpt_gap_exponent_base. bpt_gap_exponent_base + 1 = a) -> (exists bpt_gap_exponent_order. bpt_gap_exponent_order + e = f) -> (exists ff_b_bpt_exp_left ff_c_bpt_exp_left. ((forall ff_i_bpt_exp_left_repeat. (exists ff_lt_bpt_exp_left_repeat_bound. ff_lt_bpt_exp_left_repeat_bound + S ff_i_bpt_exp_left_repeat = e) -> (((exists ff_h_bpt_exp_left_repeat_decoded. ff_h_bpt_exp_left_repeat_decoded + S (a) = S ((S (ff_i_bpt_exp_left_repeat)) * ff_c_bpt_exp_left)) /\ exists ff_q_bpt_exp_left_repeat_decoded. ff_b_bpt_exp_left = ff_q_bpt_exp_left_repeat_decoded * S ((S (ff_i_bpt_exp_left_repeat)) * ff_c_bpt_exp_left) + (a)))) /\ (exists ff_u_bpt_exp_left_product ff_v_bpt_exp_left_product. ((((exists ff_h_bpt_exp_left_product_start. ff_h_bpt_exp_left_product_start + S (1) = S ((S (0)) * ff_v_bpt_exp_left_product)) /\ exists ff_q_bpt_exp_left_product_start. ff_u_bpt_exp_left_product = ff_q_bpt_exp_left_product_start * S ((S (0)) * ff_v_bpt_exp_left_product) + (1))) /\ ((((exists ff_h_bpt_exp_left_product_terminal. ff_h_bpt_exp_left_product_terminal + S (x) = S ((S (e)) * ff_v_bpt_exp_left_product)) /\ exists ff_q_bpt_exp_left_product_terminal. ff_u_bpt_exp_left_product = ff_q_bpt_exp_left_product_terminal * S ((S (e)) * ff_v_bpt_exp_left_product) + (x))) /\ forall ff_i_bpt_exp_left_product. (exists ff_lt_bpt_exp_left_product_bound. ff_lt_bpt_exp_left_product_bound + S ff_i_bpt_exp_left_product = e) -> exists ff_p_bpt_exp_left_product ff_r_bpt_exp_left_product ff_s_bpt_exp_left_product. ((((exists ff_h_bpt_exp_left_product_factor. ff_h_bpt_exp_left_product_factor + S (ff_p_bpt_exp_left_product) = S ((S (ff_i_bpt_exp_left_product)) * ff_c_bpt_exp_left)) /\ exists ff_q_bpt_exp_left_product_factor. ff_b_bpt_exp_left = ff_q_bpt_exp_left_product_factor * S ((S (ff_i_bpt_exp_left_product)) * ff_c_bpt_exp_left) + (ff_p_bpt_exp_left_product))) /\ ((((exists ff_h_bpt_exp_left_product_partial. ff_h_bpt_exp_left_product_partial + S (ff_r_bpt_exp_left_product) = S ((S (ff_i_bpt_exp_left_product)) * ff_v_bpt_exp_left_product)) /\ exists ff_q_bpt_exp_left_product_partial. ff_u_bpt_exp_left_product = ff_q_bpt_exp_left_product_partial * S ((S (ff_i_bpt_exp_left_product)) * ff_v_bpt_exp_left_product) + (ff_r_bpt_exp_left_product))) /\ ((((exists ff_h_bpt_exp_left_product_successor. ff_h_bpt_exp_left_product_successor + S (ff_s_bpt_exp_left_product) = S ((S (S ff_i_bpt_exp_left_product)) * ff_v_bpt_exp_left_product)) /\ exists ff_q_bpt_exp_left_product_successor. ff_u_bpt_exp_left_product = ff_q_bpt_exp_left_product_successor * S ((S (S ff_i_bpt_exp_left_product)) * ff_v_bpt_exp_left_product) + (ff_s_bpt_exp_left_product))) /\ ff_s_bpt_exp_left_product = ff_r_bpt_exp_left_product * ff_p_bpt_exp_left_product)))))))) -> (exists ff_b_bpt_exp_right ff_c_bpt_exp_right. ((forall ff_i_bpt_exp_right_repeat. (exists ff_lt_bpt_exp_right_repeat_bound. ff_lt_bpt_exp_right_repeat_bound + S ff_i_bpt_exp_right_repeat = f) -> (((exists ff_h_bpt_exp_right_repeat_decoded. ff_h_bpt_exp_right_repeat_decoded + S (a) = S ((S (ff_i_bpt_exp_right_repeat)) * ff_c_bpt_exp_right)) /\ exists ff_q_bpt_exp_right_repeat_decoded. ff_b_bpt_exp_right = ff_q_bpt_exp_right_repeat_decoded * S ((S (ff_i_bpt_exp_right_repeat)) * ff_c_bpt_exp_right) + (a)))) /\ (exists ff_u_bpt_exp_right_product ff_v_bpt_exp_right_product. ((((exists ff_h_bpt_exp_right_product_start. ff_h_bpt_exp_right_product_start + S (1) = S ((S (0)) * ff_v_bpt_exp_right_product)) /\ exists ff_q_bpt_exp_right_product_start. ff_u_bpt_exp_right_product = ff_q_bpt_exp_right_product_start * S ((S (0)) * ff_v_bpt_exp_right_product) + (1))) /\ ((((exists ff_h_bpt_exp_right_product_terminal. ff_h_bpt_exp_right_product_terminal + S (y) = S ((S (f)) * ff_v_bpt_exp_right_product)) /\ exists ff_q_bpt_exp_right_product_terminal. ff_u_bpt_exp_right_product = ff_q_bpt_exp_right_product_terminal * S ((S (f)) * ff_v_bpt_exp_right_product) + (y))) /\ forall ff_i_bpt_exp_right_product. (exists ff_lt_bpt_exp_right_product_bound. ff_lt_bpt_exp_right_product_bound + S ff_i_bpt_exp_right_product = f) -> exists ff_p_bpt_exp_right_product ff_r_bpt_exp_right_product ff_s_bpt_exp_right_product. ((((exists ff_h_bpt_exp_right_product_factor. ff_h_bpt_exp_right_product_factor + S (ff_p_bpt_exp_right_product) = S ((S (ff_i_bpt_exp_right_product)) * ff_c_bpt_exp_right)) /\ exists ff_q_bpt_exp_right_product_factor. ff_b_bpt_exp_right = ff_q_bpt_exp_right_product_factor * S ((S (ff_i_bpt_exp_right_product)) * ff_c_bpt_exp_right) + (ff_p_bpt_exp_right_product))) /\ ((((exists ff_h_bpt_exp_right_product_partial. ff_h_bpt_exp_right_product_partial + S (ff_r_bpt_exp_right_product) = S ((S (ff_i_bpt_exp_right_product)) * ff_v_bpt_exp_right_product)) /\ exists ff_q_bpt_exp_right_product_partial. ff_u_bpt_exp_right_product = ff_q_bpt_exp_right_product_partial * S ((S (ff_i_bpt_exp_right_product)) * ff_v_bpt_exp_right_product) + (ff_r_bpt_exp_right_product))) /\ ((((exists ff_h_bpt_exp_right_product_successor. ff_h_bpt_exp_right_product_successor + S (ff_s_bpt_exp_right_product) = S ((S (S ff_i_bpt_exp_right_product)) * ff_v_bpt_exp_right_product)) /\ exists ff_q_bpt_exp_right_product_successor. ff_u_bpt_exp_right_product = ff_q_bpt_exp_right_product_successor * S ((S (S ff_i_bpt_exp_right_product)) * ff_v_bpt_exp_right_product) + (ff_s_bpt_exp_right_product))) /\ ff_s_bpt_exp_right_product = ff_r_bpt_exp_right_product * ff_p_bpt_exp_right_product)))))))) -> (exists bpt_gap_exponent_result. bpt_gap_exponent_result + x = y)

Proof neighborhood

Direct theorem prerequisites

BT009X pow_add BT00Q0 one_le_pow BT00PW le_mul_of_one_le_right BT0002 add_comm

Direct theorem dependents

BT00WP bertrand_h_root_32_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 BT00X5 bertrand_four_power_product_le_of_sum_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

48 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 (4)
pow addone le powle mul of one le rightadd comm
01Fix variables and assumptionsL1–10

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

  1. L1
    intro a
  2. L2
    intro e
  3. L3
    intro f
  4. L4
    intro x
  5. L5
    intro y
  6. L6
    intro htotal
  7. L7
    intro ha
  8. L8
    intro hef
  9. L9
    intro hx
  10. L10
    intro hy
02Separate the logical casesL11–11

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

  1. L11
    cases hef
03Establish hsumL12–18

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

  1. L12
    have hsum : f = e + x1
  2. L13
    trans x1 + e
  3. L14
    symm
  4. L15
    exact hef_witness
  5. L16
    specialize add_comm x1
  6. L17
    specialize add_comm e
  7. L18
    exact add_comm
04Establish hgapL19–22

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

  1. L19
    have hgap : ∃ z. Pow(a,x1,z)Definitions: Pow(a,x1,z)Original native command in the exact edition
  2. L20
    specialize htotal a
  3. L21
    specialize htotal x1
  4. L22
    exact htotal
05Separate the logical casesL23–23

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

  1. L23
    cases hgap
06Establish hyfactorL24–33

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

  1. L24
    have hyfactor : y = x * x2
  2. L25
    specialize pow_add a
  3. L26
    specialize pow_add e
  4. L27
    specialize pow_add x1
  5. L28
    specialize pow_add f
  6. L29
    specialize pow_add x
  7. L30
    specialize pow_add x2
  8. L31
    specialize pow_add y
  9. L32
    apply pow_add
  10. L33
    exact hsum
07Use earlier factsL34–36

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

  1. L34
    exact hx
  2. L35
    exact hgap_witness
  3. L36
    exact hy
08Establish hgap1L37–46

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

  1. L37
  2. L38
    specialize one_le_pow a
  3. L39
    specialize one_le_pow x1
  4. L40
    specialize one_le_pow x2
  5. L41
    apply one_le_pow
  6. L42
    exact ha
  7. L43
    exact hgap_witness
  8. L44
    rewrite hyfactor
  9. L45
    specialize le_mul_of_one_le_right x
  10. L46
    specialize le_mul_of_one_le_right x2
09Use earlier factsL47–48

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

  1. L47
    apply le_mul_of_one_le_right
  2. L48
    exact hgap1

Library-wide reading audit

Original defined command ledger · 48 lines
  1. 0001intro a
  2. 0002intro e
  3. 0003intro f
  4. 0004intro x
  5. 0005intro y
  6. 0006intro htotal
  7. 0007intro ha
  8. 0008intro hef
  9. 0009intro hx
  10. 0010intro hy
  11. 0011cases hef
  12. 0012have hsum : f = e + x1
  13. 0013trans x1 + e
  14. 0014symm
  15. 0015exact hef_witness
  16. 0016specialize add_comm x1
  17. 0017specialize add_comm e
  18. 0018exact add_comm
  19. 0019have hgap : ∃ z. Pow(a,x1,z)
    Exact native replay linehave hgap : exists z. (exists ff_b_bpt_exp_gap ff_c_bpt_exp_gap. ((forall ff_i_bpt_exp_gap_repeat. (exists ff_lt_bpt_exp_gap_repeat_bound. ff_lt_bpt_exp_gap_repeat_bound + S ff_i_bpt_exp_gap_repeat = x1) -> (((exists ff_h_bpt_exp_gap_repeat_decoded. ff_h_bpt_exp_gap_repeat_decoded + S (a) = S ((S (ff_i_bpt_exp_gap_repeat)) * ff_c_bpt_exp_gap)) /\ exists ff_q_bpt_exp_gap_repeat_decoded. ff_b_bpt_exp_gap = ff_q_bpt_exp_gap_repeat_decoded * S ((S (ff_i_bpt_exp_gap_repeat)) * ff_c_bpt_exp_gap) + (a)))) /\ (exists ff_u_bpt_exp_gap_product ff_v_bpt_exp_gap_product. ((((exists ff_h_bpt_exp_gap_product_start. ff_h_bpt_exp_gap_product_start + S (1) = S ((S (0)) * ff_v_bpt_exp_gap_product)) /\ exists ff_q_bpt_exp_gap_product_start. ff_u_bpt_exp_gap_product = ff_q_bpt_exp_gap_product_start * S ((S (0)) * ff_v_bpt_exp_gap_product) + (1))) /\ ((((exists ff_h_bpt_exp_gap_product_terminal. ff_h_bpt_exp_gap_product_terminal + S (z) = S ((S (x1)) * ff_v_bpt_exp_gap_product)) /\ exists ff_q_bpt_exp_gap_product_terminal. ff_u_bpt_exp_gap_product = ff_q_bpt_exp_gap_product_terminal * S ((S (x1)) * ff_v_bpt_exp_gap_product) + (z))) /\ forall ff_i_bpt_exp_gap_product. (exists ff_lt_bpt_exp_gap_product_bound. ff_lt_bpt_exp_gap_product_bound + S ff_i_bpt_exp_gap_product = x1) -> exists ff_p_bpt_exp_gap_product ff_r_bpt_exp_gap_product ff_s_bpt_exp_gap_product. ((((exists ff_h_bpt_exp_gap_product_factor. ff_h_bpt_exp_gap_product_factor + S (ff_p_bpt_exp_gap_product) = S ((S (ff_i_bpt_exp_gap_product)) * ff_c_bpt_exp_gap)) /\ exists ff_q_bpt_exp_gap_product_factor. ff_b_bpt_exp_gap = ff_q_bpt_exp_gap_product_factor * S ((S (ff_i_bpt_exp_gap_product)) * ff_c_bpt_exp_gap) + (ff_p_bpt_exp_gap_product))) /\ ((((exists ff_h_bpt_exp_gap_product_partial. ff_h_bpt_exp_gap_product_partial + S (ff_r_bpt_exp_gap_product) = S ((S (ff_i_bpt_exp_gap_product)) * ff_v_bpt_exp_gap_product)) /\ exists ff_q_bpt_exp_gap_product_partial. ff_u_bpt_exp_gap_product = ff_q_bpt_exp_gap_product_partial * S ((S (ff_i_bpt_exp_gap_product)) * ff_v_bpt_exp_gap_product) + (ff_r_bpt_exp_gap_product))) /\ ((((exists ff_h_bpt_exp_gap_product_successor. ff_h_bpt_exp_gap_product_successor + S (ff_s_bpt_exp_gap_product) = S ((S (S ff_i_bpt_exp_gap_product)) * ff_v_bpt_exp_gap_product)) /\ exists ff_q_bpt_exp_gap_product_successor. ff_u_bpt_exp_gap_product = ff_q_bpt_exp_gap_product_successor * S ((S (S ff_i_bpt_exp_gap_product)) * ff_v_bpt_exp_gap_product) + (ff_s_bpt_exp_gap_product))) /\ ff_s_bpt_exp_gap_product = ff_r_bpt_exp_gap_product * ff_p_bpt_exp_gap_product))))))))
  20. 0020specialize htotal a
  21. 0021specialize htotal x1
  22. 0022exact htotal
  23. 0023cases hgap
  24. 0024have hyfactor : y = x * x2
  25. 0025specialize pow_add a
  26. 0026specialize pow_add e
  27. 0027specialize pow_add x1
  28. 0028specialize pow_add f
  29. 0029specialize pow_add x
  30. 0030specialize pow_add x2
  31. 0031specialize pow_add y
  32. 0032apply pow_add
  33. 0033exact hsum
  34. 0034exact hx
  35. 0035exact hgap_witness
  36. 0036exact hy
  37. 0037have hgap1 : Lt(0,x2)
    Exact native replay linehave hgap1 : exists k. k + 1 = x2
  38. 0038specialize one_le_pow a
  39. 0039specialize one_le_pow x1
  40. 0040specialize one_le_pow x2
  41. 0041apply one_le_pow
  42. 0042exact ha
  43. 0043exact hgap_witness
  44. 0044rewrite hyfactor
  45. 0045specialize le_mul_of_one_le_right x
  46. 0046specialize le_mul_of_one_le_right x2
  47. 0047apply le_mul_of_one_le_right
  48. 0048exact hgap1