BT00X7 · Bertrand theorem

bertrand_main_inequality_factorized

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

The factorized B6 inequality discharges relational-power totality exactly once.

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

∀ n. ∀ s. ∀ q. ∀ r. ∀ A. ∀ B. ∀ F. Le(16 · 32,n) → FloorSqrt(2 · n,s) → DivRem(2 · n,3,q,r) → Pow(2 · n,s,A) → Pow(4,q,B) → Pow(4,n,F) → Le(n · A · B,F)

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 PD0007 DivRem PD0020 Pow PD0051 FloorSqrt

7 occurrences

In local proof propositions

PD0020 Pow

1 occurrences

Exact expanded native-PA statement
forall n s q r A B F. (exists bqb_le_gap_b6_main_thin_threshold. bqb_le_gap_b6_main_thin_threshold + (16 * 32) = (n)) -> (((exists bcs_sqrt_lower_gap_b6_main_thin_floor. bcs_sqrt_lower_gap_b6_main_thin_floor + (s) * (s) = (2 * n)) /\ exists bcs_sqrt_upper_gap_b6_main_thin_floor. bcs_sqrt_upper_gap_b6_main_thin_floor + S (2 * n) = S (s) * S (s))) -> ((((2 * n) = 3 * (q) + (r)) /\ exists bmi_remainder_gap_b6_main_thin_division. bmi_remainder_gap_b6_main_thin_division + S (r) = 3)) -> (exists pa_b_b6_main_thin_a pa_c_b6_main_thin_a. ((forall pa_i_b6_main_thin_a_repeat. (exists pa_lt_b6_main_thin_a_repeat_bound. pa_lt_b6_main_thin_a_repeat_bound + S pa_i_b6_main_thin_a_repeat = s) -> (((exists pa_h_b6_main_thin_a_repeat_decoded. pa_h_b6_main_thin_a_repeat_decoded + S (2 * n) = S ((S (pa_i_b6_main_thin_a_repeat)) * pa_c_b6_main_thin_a)) /\ exists pa_q_b6_main_thin_a_repeat_decoded. pa_b_b6_main_thin_a = pa_q_b6_main_thin_a_repeat_decoded * S ((S (pa_i_b6_main_thin_a_repeat)) * pa_c_b6_main_thin_a) + (2 * n)))) /\ (exists pa_u_b6_main_thin_a_product pa_v_b6_main_thin_a_product. ((((exists pa_h_b6_main_thin_a_product_start. pa_h_b6_main_thin_a_product_start + S (1) = S ((S (0)) * pa_v_b6_main_thin_a_product)) /\ exists pa_q_b6_main_thin_a_product_start. pa_u_b6_main_thin_a_product = pa_q_b6_main_thin_a_product_start * S ((S (0)) * pa_v_b6_main_thin_a_product) + (1))) /\ ((((exists pa_h_b6_main_thin_a_product_terminal. pa_h_b6_main_thin_a_product_terminal + S (A) = S ((S (s)) * pa_v_b6_main_thin_a_product)) /\ exists pa_q_b6_main_thin_a_product_terminal. pa_u_b6_main_thin_a_product = pa_q_b6_main_thin_a_product_terminal * S ((S (s)) * pa_v_b6_main_thin_a_product) + (A))) /\ forall pa_i_b6_main_thin_a_product. (exists pa_lt_b6_main_thin_a_product_bound. pa_lt_b6_main_thin_a_product_bound + S pa_i_b6_main_thin_a_product = s) -> exists pa_p_b6_main_thin_a_product pa_r_b6_main_thin_a_product pa_s_b6_main_thin_a_product. ((((exists pa_h_b6_main_thin_a_product_factor. pa_h_b6_main_thin_a_product_factor + S (pa_p_b6_main_thin_a_product) = S ((S (pa_i_b6_main_thin_a_product)) * pa_c_b6_main_thin_a)) /\ exists pa_q_b6_main_thin_a_product_factor. pa_b_b6_main_thin_a = pa_q_b6_main_thin_a_product_factor * S ((S (pa_i_b6_main_thin_a_product)) * pa_c_b6_main_thin_a) + (pa_p_b6_main_thin_a_product))) /\ ((((exists pa_h_b6_main_thin_a_product_partial. pa_h_b6_main_thin_a_product_partial + S (pa_r_b6_main_thin_a_product) = S ((S (pa_i_b6_main_thin_a_product)) * pa_v_b6_main_thin_a_product)) /\ exists pa_q_b6_main_thin_a_product_partial. pa_u_b6_main_thin_a_product = pa_q_b6_main_thin_a_product_partial * S ((S (pa_i_b6_main_thin_a_product)) * pa_v_b6_main_thin_a_product) + (pa_r_b6_main_thin_a_product))) /\ ((((exists pa_h_b6_main_thin_a_product_successor. pa_h_b6_main_thin_a_product_successor + S (pa_s_b6_main_thin_a_product) = S ((S (S pa_i_b6_main_thin_a_product)) * pa_v_b6_main_thin_a_product)) /\ exists pa_q_b6_main_thin_a_product_successor. pa_u_b6_main_thin_a_product = pa_q_b6_main_thin_a_product_successor * S ((S (S pa_i_b6_main_thin_a_product)) * pa_v_b6_main_thin_a_product) + (pa_s_b6_main_thin_a_product))) /\ pa_s_b6_main_thin_a_product = pa_r_b6_main_thin_a_product * pa_p_b6_main_thin_a_product)))))))) -> (exists pa_b_b6_main_thin_b pa_c_b6_main_thin_b. ((forall pa_i_b6_main_thin_b_repeat. (exists pa_lt_b6_main_thin_b_repeat_bound. pa_lt_b6_main_thin_b_repeat_bound + S pa_i_b6_main_thin_b_repeat = q) -> (((exists pa_h_b6_main_thin_b_repeat_decoded. pa_h_b6_main_thin_b_repeat_decoded + S (4) = S ((S (pa_i_b6_main_thin_b_repeat)) * pa_c_b6_main_thin_b)) /\ exists pa_q_b6_main_thin_b_repeat_decoded. pa_b_b6_main_thin_b = pa_q_b6_main_thin_b_repeat_decoded * S ((S (pa_i_b6_main_thin_b_repeat)) * pa_c_b6_main_thin_b) + (4)))) /\ (exists pa_u_b6_main_thin_b_product pa_v_b6_main_thin_b_product. ((((exists pa_h_b6_main_thin_b_product_start. pa_h_b6_main_thin_b_product_start + S (1) = S ((S (0)) * pa_v_b6_main_thin_b_product)) /\ exists pa_q_b6_main_thin_b_product_start. pa_u_b6_main_thin_b_product = pa_q_b6_main_thin_b_product_start * S ((S (0)) * pa_v_b6_main_thin_b_product) + (1))) /\ ((((exists pa_h_b6_main_thin_b_product_terminal. pa_h_b6_main_thin_b_product_terminal + S (B) = S ((S (q)) * pa_v_b6_main_thin_b_product)) /\ exists pa_q_b6_main_thin_b_product_terminal. pa_u_b6_main_thin_b_product = pa_q_b6_main_thin_b_product_terminal * S ((S (q)) * pa_v_b6_main_thin_b_product) + (B))) /\ forall pa_i_b6_main_thin_b_product. (exists pa_lt_b6_main_thin_b_product_bound. pa_lt_b6_main_thin_b_product_bound + S pa_i_b6_main_thin_b_product = q) -> exists pa_p_b6_main_thin_b_product pa_r_b6_main_thin_b_product pa_s_b6_main_thin_b_product. ((((exists pa_h_b6_main_thin_b_product_factor. pa_h_b6_main_thin_b_product_factor + S (pa_p_b6_main_thin_b_product) = S ((S (pa_i_b6_main_thin_b_product)) * pa_c_b6_main_thin_b)) /\ exists pa_q_b6_main_thin_b_product_factor. pa_b_b6_main_thin_b = pa_q_b6_main_thin_b_product_factor * S ((S (pa_i_b6_main_thin_b_product)) * pa_c_b6_main_thin_b) + (pa_p_b6_main_thin_b_product))) /\ ((((exists pa_h_b6_main_thin_b_product_partial. pa_h_b6_main_thin_b_product_partial + S (pa_r_b6_main_thin_b_product) = S ((S (pa_i_b6_main_thin_b_product)) * pa_v_b6_main_thin_b_product)) /\ exists pa_q_b6_main_thin_b_product_partial. pa_u_b6_main_thin_b_product = pa_q_b6_main_thin_b_product_partial * S ((S (pa_i_b6_main_thin_b_product)) * pa_v_b6_main_thin_b_product) + (pa_r_b6_main_thin_b_product))) /\ ((((exists pa_h_b6_main_thin_b_product_successor. pa_h_b6_main_thin_b_product_successor + S (pa_s_b6_main_thin_b_product) = S ((S (S pa_i_b6_main_thin_b_product)) * pa_v_b6_main_thin_b_product)) /\ exists pa_q_b6_main_thin_b_product_successor. pa_u_b6_main_thin_b_product = pa_q_b6_main_thin_b_product_successor * S ((S (S pa_i_b6_main_thin_b_product)) * pa_v_b6_main_thin_b_product) + (pa_s_b6_main_thin_b_product))) /\ pa_s_b6_main_thin_b_product = pa_r_b6_main_thin_b_product * pa_p_b6_main_thin_b_product)))))))) -> (exists pa_b_b6_main_thin_f pa_c_b6_main_thin_f. ((forall pa_i_b6_main_thin_f_repeat. (exists pa_lt_b6_main_thin_f_repeat_bound. pa_lt_b6_main_thin_f_repeat_bound + S pa_i_b6_main_thin_f_repeat = n) -> (((exists pa_h_b6_main_thin_f_repeat_decoded. pa_h_b6_main_thin_f_repeat_decoded + S (4) = S ((S (pa_i_b6_main_thin_f_repeat)) * pa_c_b6_main_thin_f)) /\ exists pa_q_b6_main_thin_f_repeat_decoded. pa_b_b6_main_thin_f = pa_q_b6_main_thin_f_repeat_decoded * S ((S (pa_i_b6_main_thin_f_repeat)) * pa_c_b6_main_thin_f) + (4)))) /\ (exists pa_u_b6_main_thin_f_product pa_v_b6_main_thin_f_product. ((((exists pa_h_b6_main_thin_f_product_start. pa_h_b6_main_thin_f_product_start + S (1) = S ((S (0)) * pa_v_b6_main_thin_f_product)) /\ exists pa_q_b6_main_thin_f_product_start. pa_u_b6_main_thin_f_product = pa_q_b6_main_thin_f_product_start * S ((S (0)) * pa_v_b6_main_thin_f_product) + (1))) /\ ((((exists pa_h_b6_main_thin_f_product_terminal. pa_h_b6_main_thin_f_product_terminal + S (F) = S ((S (n)) * pa_v_b6_main_thin_f_product)) /\ exists pa_q_b6_main_thin_f_product_terminal. pa_u_b6_main_thin_f_product = pa_q_b6_main_thin_f_product_terminal * S ((S (n)) * pa_v_b6_main_thin_f_product) + (F))) /\ forall pa_i_b6_main_thin_f_product. (exists pa_lt_b6_main_thin_f_product_bound. pa_lt_b6_main_thin_f_product_bound + S pa_i_b6_main_thin_f_product = n) -> exists pa_p_b6_main_thin_f_product pa_r_b6_main_thin_f_product pa_s_b6_main_thin_f_product. ((((exists pa_h_b6_main_thin_f_product_factor. pa_h_b6_main_thin_f_product_factor + S (pa_p_b6_main_thin_f_product) = S ((S (pa_i_b6_main_thin_f_product)) * pa_c_b6_main_thin_f)) /\ exists pa_q_b6_main_thin_f_product_factor. pa_b_b6_main_thin_f = pa_q_b6_main_thin_f_product_factor * S ((S (pa_i_b6_main_thin_f_product)) * pa_c_b6_main_thin_f) + (pa_p_b6_main_thin_f_product))) /\ ((((exists pa_h_b6_main_thin_f_product_partial. pa_h_b6_main_thin_f_product_partial + S (pa_r_b6_main_thin_f_product) = S ((S (pa_i_b6_main_thin_f_product)) * pa_v_b6_main_thin_f_product)) /\ exists pa_q_b6_main_thin_f_product_partial. pa_u_b6_main_thin_f_product = pa_q_b6_main_thin_f_product_partial * S ((S (pa_i_b6_main_thin_f_product)) * pa_v_b6_main_thin_f_product) + (pa_r_b6_main_thin_f_product))) /\ ((((exists pa_h_b6_main_thin_f_product_successor. pa_h_b6_main_thin_f_product_successor + S (pa_s_b6_main_thin_f_product) = S ((S (S pa_i_b6_main_thin_f_product)) * pa_v_b6_main_thin_f_product)) /\ exists pa_q_b6_main_thin_f_product_successor. pa_u_b6_main_thin_f_product = pa_q_b6_main_thin_f_product_successor * S ((S (S pa_i_b6_main_thin_f_product)) * pa_v_b6_main_thin_f_product) + (pa_s_b6_main_thin_f_product))) /\ pa_s_b6_main_thin_f_product = pa_r_b6_main_thin_f_product * pa_p_b6_main_thin_f_product)))))))) -> (exists bqb_le_gap_b6_main_thin_result. bqb_le_gap_b6_main_thin_result + (n * A * B) = (F))

Proof neighborhood

Direct theorem prerequisites

BT0080 pow_exists BT00X6 bertrand_main_inequality_factorized_from_total

Direct theorem dependents

BT00X8 bertrand_main_inequality_nat

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

34 script commands · 5 reading checkpoints · 1 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 (2)
pow existsbertrand main inequality factorized from total
01Fix variables and assumptionsL1–10

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

  1. L1
    intro n
  2. L2
    intro s
  3. L3
    intro q
  4. L4
    intro r
  5. L5
    intro A
  6. L6
    intro B
  7. L7
    intro F
  8. L8
    intro hthreshold
  9. L9
    intro hfloor
  10. L10
    intro hdiv
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hA
  2. L12
    intro hB
  3. L13
    intro hF
03Establish htotalL14–23

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

  1. L14
    have htotal : ∀ bpt_a_b6_main_thin_total. ∀ bpt_e_b6_main_thin_total. ∃ bpt_x_b6_main_thin_total. Pow(bpt_a_b6_main_thin_total,bpt_e_b6_main_thin_total,bpt_x_b6_main_thin_total)Definitions: Pow(bpt_a_b6_main_thin_total,bpt_e_b6_main_thin_total,bpt_x_b6_main_thin_total)Original native command in the exact edition
  2. L15
    intro a
  3. L16
    intro e
  4. L17
    specialize pow_exists a
  5. L18
    specialize pow_exists e
  6. L19
    exact pow_exists
  7. L20
    specialize bertrand_main_inequality_factorized_from_total n
  8. L21
    specialize bertrand_main_inequality_factorized_from_total s
  9. L22
    specialize bertrand_main_inequality_factorized_from_total q
  10. L23
    specialize bertrand_main_inequality_factorized_from_total r
04Use earlier factsL24–33

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

  1. L24
    specialize bertrand_main_inequality_factorized_from_total A
  2. L25
    specialize bertrand_main_inequality_factorized_from_total B
  3. L26
    specialize bertrand_main_inequality_factorized_from_total F
  4. L27
    apply bertrand_main_inequality_factorized_from_total
  5. L28
    exact htotal
  6. L29
    exact hthreshold
  7. L30
    exact hfloor
  8. L31
    exact hdiv
  9. L32
    exact hA
  10. L33
    exact hB
05Use earlier factsL34–34

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

  1. L34
    exact hF

Library-wide reading audit

Original defined command ledger · 34 lines
  1. 0001intro n
  2. 0002intro s
  3. 0003intro q
  4. 0004intro r
  5. 0005intro A
  6. 0006intro B
  7. 0007intro F
  8. 0008intro hthreshold
  9. 0009intro hfloor
  10. 0010intro hdiv
  11. 0011intro hA
  12. 0012intro hB
  13. 0013intro hF
  14. 0014have htotal : ∀ bpt_a_b6_main_thin_total. ∀ bpt_e_b6_main_thin_total. ∃ bpt_x_b6_main_thin_total. Pow(bpt_a_b6_main_thin_total,bpt_e_b6_main_thin_total,bpt_x_b6_main_thin_total)
    Exact native replay linehave htotal : forall bpt_a_b6_main_thin_total bpt_e_b6_main_thin_total. exists bpt_x_b6_main_thin_total. (exists ff_b_bpt_value_b6_main_thin_total ff_c_bpt_value_b6_main_thin_total. ((forall ff_i_bpt_value_b6_main_thin_total_repeat. (exists ff_lt_bpt_value_b6_main_thin_total_repeat_bound. ff_lt_bpt_value_b6_main_thin_total_repeat_bound + S ff_i_bpt_value_b6_main_thin_total_repeat = bpt_e_b6_main_thin_total) -> (((exists ff_h_bpt_value_b6_main_thin_total_repeat_decoded. ff_h_bpt_value_b6_main_thin_total_repeat_decoded + S (bpt_a_b6_main_thin_total) = S ((S (ff_i_bpt_value_b6_main_thin_total_repeat)) * ff_c_bpt_value_b6_main_thin_total)) /\ exists ff_q_bpt_value_b6_main_thin_total_repeat_decoded. ff_b_bpt_value_b6_main_thin_total = ff_q_bpt_value_b6_main_thin_total_repeat_decoded * S ((S (ff_i_bpt_value_b6_main_thin_total_repeat)) * ff_c_bpt_value_b6_main_thin_total) + (bpt_a_b6_main_thin_total)))) /\ (exists ff_u_bpt_value_b6_main_thin_total_product ff_v_bpt_value_b6_main_thin_total_product. ((((exists ff_h_bpt_value_b6_main_thin_total_product_start. ff_h_bpt_value_b6_main_thin_total_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_b6_main_thin_total_product)) /\ exists ff_q_bpt_value_b6_main_thin_total_product_start. ff_u_bpt_value_b6_main_thin_total_product = ff_q_bpt_value_b6_main_thin_total_product_start * S ((S (0)) * ff_v_bpt_value_b6_main_thin_total_product) + (1))) /\ ((((exists ff_h_bpt_value_b6_main_thin_total_product_terminal. ff_h_bpt_value_b6_main_thin_total_product_terminal + S (bpt_x_b6_main_thin_total) = S ((S (bpt_e_b6_main_thin_total)) * ff_v_bpt_value_b6_main_thin_total_product)) /\ exists ff_q_bpt_value_b6_main_thin_total_product_terminal. ff_u_bpt_value_b6_main_thin_total_product = ff_q_bpt_value_b6_main_thin_total_product_terminal * S ((S (bpt_e_b6_main_thin_total)) * ff_v_bpt_value_b6_main_thin_total_product) + (bpt_x_b6_main_thin_total))) /\ forall ff_i_bpt_value_b6_main_thin_total_product. (exists ff_lt_bpt_value_b6_main_thin_total_product_bound. ff_lt_bpt_value_b6_main_thin_total_product_bound + S ff_i_bpt_value_b6_main_thin_total_product = bpt_e_b6_main_thin_total) -> exists ff_p_bpt_value_b6_main_thin_total_product ff_r_bpt_value_b6_main_thin_total_product ff_s_bpt_value_b6_main_thin_total_product. ((((exists ff_h_bpt_value_b6_main_thin_total_product_factor. ff_h_bpt_value_b6_main_thin_total_product_factor + S (ff_p_bpt_value_b6_main_thin_total_product) = S ((S (ff_i_bpt_value_b6_main_thin_total_product)) * ff_c_bpt_value_b6_main_thin_total)) /\ exists ff_q_bpt_value_b6_main_thin_total_product_factor. ff_b_bpt_value_b6_main_thin_total = ff_q_bpt_value_b6_main_thin_total_product_factor * S ((S (ff_i_bpt_value_b6_main_thin_total_product)) * ff_c_bpt_value_b6_main_thin_total) + (ff_p_bpt_value_b6_main_thin_total_product))) /\ ((((exists ff_h_bpt_value_b6_main_thin_total_product_partial. ff_h_bpt_value_b6_main_thin_total_product_partial + S (ff_r_bpt_value_b6_main_thin_total_product) = S ((S (ff_i_bpt_value_b6_main_thin_total_product)) * ff_v_bpt_value_b6_main_thin_total_product)) /\ exists ff_q_bpt_value_b6_main_thin_total_product_partial. ff_u_bpt_value_b6_main_thin_total_product = ff_q_bpt_value_b6_main_thin_total_product_partial * S ((S (ff_i_bpt_value_b6_main_thin_total_product)) * ff_v_bpt_value_b6_main_thin_total_product) + (ff_r_bpt_value_b6_main_thin_total_product))) /\ ((((exists ff_h_bpt_value_b6_main_thin_total_product_successor. ff_h_bpt_value_b6_main_thin_total_product_successor + S (ff_s_bpt_value_b6_main_thin_total_product) = S ((S (S ff_i_bpt_value_b6_main_thin_total_product)) * ff_v_bpt_value_b6_main_thin_total_product)) /\ exists ff_q_bpt_value_b6_main_thin_total_product_successor. ff_u_bpt_value_b6_main_thin_total_product = ff_q_bpt_value_b6_main_thin_total_product_successor * S ((S (S ff_i_bpt_value_b6_main_thin_total_product)) * ff_v_bpt_value_b6_main_thin_total_product) + (ff_s_bpt_value_b6_main_thin_total_product))) /\ ff_s_bpt_value_b6_main_thin_total_product = ff_r_bpt_value_b6_main_thin_total_product * ff_p_bpt_value_b6_main_thin_total_product))))))))
  15. 0015intro a
  16. 0016intro e
  17. 0017specialize pow_exists a
  18. 0018specialize pow_exists e
  19. 0019exact pow_exists
  20. 0020specialize bertrand_main_inequality_factorized_from_total n
  21. 0021specialize bertrand_main_inequality_factorized_from_total s
  22. 0022specialize bertrand_main_inequality_factorized_from_total q
  23. 0023specialize bertrand_main_inequality_factorized_from_total r
  24. 0024specialize bertrand_main_inequality_factorized_from_total A
  25. 0025specialize bertrand_main_inequality_factorized_from_total B
  26. 0026specialize bertrand_main_inequality_factorized_from_total F
  27. 0027apply bertrand_main_inequality_factorized_from_total
  28. 0028exact htotal
  29. 0029exact hthreshold
  30. 0030exact hfloor
  31. 0031exact hdiv
  32. 0032exact hA
  33. 0033exact hB
  34. 0034exact hF