BT00YH · Bertrand theorem

floor_sqrt_above_root_power_two_strict

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

A prime above a floor root has square strictly above the 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

∀ x. ∀ s. ∀ p. ∀ t. FloorSqrt(x,s) → Lt(s,p) → Pow(p,2,t) → Lt(x,t)

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

PD0002 Lt PD0020 Pow PD0051 FloorSqrt

4 occurrences

In local proof propositions

PD0001 Le PD0002 Lt

4 occurrences

Exact expanded native-PA statement
forall x s p t. (((exists bcs_sqrt_lower_gap_bfsarpts_source. bcs_sqrt_lower_gap_bfsarpts_source + (s) * (s) = (x)) /\ exists bcs_sqrt_upper_gap_bfsarpts_source. bcs_sqrt_upper_gap_bfsarpts_source + S (x) = S (s) * S (s))) -> (exists bcf_lt_gap_bfsarpts_above. bcf_lt_gap_bfsarpts_above + S (s) = p) -> (exists bpvi_b_bfsarpts_power bpvi_c_bfsarpts_power. ((forall bpvi_i_bfsarpts_power. (exists bpvi_repeat_gap_bfsarpts_power. bpvi_repeat_gap_bfsarpts_power + S bpvi_i_bfsarpts_power = 2) -> (((exists bpvi_h_bfsarpts_power_repeat. bpvi_h_bfsarpts_power_repeat + S (p) = S ((S (bpvi_i_bfsarpts_power)) * bpvi_c_bfsarpts_power)) /\ exists bpvi_q_bfsarpts_power_repeat. bpvi_b_bfsarpts_power = bpvi_q_bfsarpts_power_repeat * S ((S (bpvi_i_bfsarpts_power)) * bpvi_c_bfsarpts_power) + (p)))) /\ (exists bpvi_u_bfsarpts_power bpvi_v_bfsarpts_power. ((((exists bpvi_h_bfsarpts_power_start. bpvi_h_bfsarpts_power_start + S (1) = S ((S (0)) * bpvi_v_bfsarpts_power)) /\ exists bpvi_q_bfsarpts_power_start. bpvi_u_bfsarpts_power = bpvi_q_bfsarpts_power_start * S ((S (0)) * bpvi_v_bfsarpts_power) + (1))) /\ ((((exists bpvi_h_bfsarpts_power_terminal. bpvi_h_bfsarpts_power_terminal + S (t) = S ((S (2)) * bpvi_v_bfsarpts_power)) /\ exists bpvi_q_bfsarpts_power_terminal. bpvi_u_bfsarpts_power = bpvi_q_bfsarpts_power_terminal * S ((S (2)) * bpvi_v_bfsarpts_power) + (t))) /\ forall bpvi_j_bfsarpts_power. (exists bpvi_product_gap_bfsarpts_power. bpvi_product_gap_bfsarpts_power + S bpvi_j_bfsarpts_power = 2) -> exists bpvi_factor_bfsarpts_power bpvi_partial_bfsarpts_power bpvi_successor_bfsarpts_power. ((((exists bpvi_h_bfsarpts_power_factor. bpvi_h_bfsarpts_power_factor + S (bpvi_factor_bfsarpts_power) = S ((S (bpvi_j_bfsarpts_power)) * bpvi_c_bfsarpts_power)) /\ exists bpvi_q_bfsarpts_power_factor. bpvi_b_bfsarpts_power = bpvi_q_bfsarpts_power_factor * S ((S (bpvi_j_bfsarpts_power)) * bpvi_c_bfsarpts_power) + (bpvi_factor_bfsarpts_power))) /\ ((((exists bpvi_h_bfsarpts_power_partial. bpvi_h_bfsarpts_power_partial + S (bpvi_partial_bfsarpts_power) = S ((S (bpvi_j_bfsarpts_power)) * bpvi_v_bfsarpts_power)) /\ exists bpvi_q_bfsarpts_power_partial. bpvi_u_bfsarpts_power = bpvi_q_bfsarpts_power_partial * S ((S (bpvi_j_bfsarpts_power)) * bpvi_v_bfsarpts_power) + (bpvi_partial_bfsarpts_power))) /\ ((((exists bpvi_h_bfsarpts_power_successor. bpvi_h_bfsarpts_power_successor + S (bpvi_successor_bfsarpts_power) = S ((S (S bpvi_j_bfsarpts_power)) * bpvi_v_bfsarpts_power)) /\ exists bpvi_q_bfsarpts_power_successor. bpvi_u_bfsarpts_power = bpvi_q_bfsarpts_power_successor * S ((S (S bpvi_j_bfsarpts_power)) * bpvi_v_bfsarpts_power) + (bpvi_successor_bfsarpts_power))) /\ bpvi_successor_bfsarpts_power = bpvi_partial_bfsarpts_power * bpvi_factor_bfsarpts_power)))))))) -> (exists bcf_lt_gap_bfsarpts_result. bcf_lt_gap_bfsarpts_result + S (x) = t)

Proof neighborhood

Direct theorem prerequisites

BT001M mul_le_mul_right BT001L mul_le_mul_left BT000F le_trans BT001D lt_of_lt_of_le BT009W pow_two

Direct theorem dependents

BT00YI central_binom_prime_above_floor_sqrt_valuation_le_one

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

43 script commands · 7 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)
mul le mul rightmul le mul leftle translt of lt of lepow two
01Fix variables and assumptionsL1–7

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

  1. L1
    intro x
  2. L2
    intro s
  3. L3
    intro p
  4. L4
    intro t
  5. L5
    intro hfloor
  6. L6
    intro habove
  7. L7
    intro hpower
02Separate the logical casesL8–8

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

  1. L8
    cases hfloor
03Establish hfirstL9–14

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

  1. L9
    have hfirst : Le(S s · S s,p · S s)Definitions: Le(S s · S s,p · S s)Original native command in the exact edition
  2. L10
    specialize mul_le_mul_right (S s)
  3. L11
    specialize mul_le_mul_right p
  4. L12
    specialize mul_le_mul_right (S s)
  5. L13
    apply mul_le_mul_right
  6. L14
    exact habove
04Establish hsecondL15–20

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

  1. L15
    have hsecond : Le(p · S s,p · p)Definitions: Le(p · S s,p · p)Original native command in the exact edition
  2. L16
    specialize mul_le_mul_left (S s)
  3. L17
    specialize mul_le_mul_left p
  4. L18
    specialize mul_le_mul_left p
  5. L19
    apply mul_le_mul_left
  6. L20
    exact habove
05Establish hsquareL21–27

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

  1. L21
    have hsquare : Le(S s · S s,p · p)Definitions: Le(S s · S s,p · p)Original native command in the exact edition
  2. L22
    specialize le_trans (S s * S s)
  3. L23
    specialize le_trans (p * S s)
  4. L24
    specialize le_trans (p * p)
  5. L25
    apply le_trans
  6. L26
    exact hfirst
  7. L27
    exact hsecond
06Establish hrawL28–34

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

  1. L28
  2. L29
    specialize lt_of_lt_of_le x
  3. L30
    specialize lt_of_lt_of_le (S s * S s)
  4. L31
    specialize lt_of_lt_of_le (p * p)
  5. L32
    apply lt_of_lt_of_le
  6. L33
    exact hfloor_right
  7. L34
    exact hsquare
07Establish hvalueL35–43

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

  1. L35
    have hvalue : t = p * p
  2. L36
    specialize pow_two p
  3. L37
    specialize pow_two 2
  4. L38
    specialize pow_two t
  5. L39
    apply pow_two
  6. L40
    refl
  7. L41
    exact hpower
  8. L42
    rewrite hvalue
  9. L43
    exact hraw

Library-wide reading audit

Original defined command ledger · 43 lines
  1. 0001intro x
  2. 0002intro s
  3. 0003intro p
  4. 0004intro t
  5. 0005intro hfloor
  6. 0006intro habove
  7. 0007intro hpower
  8. 0008cases hfloor
  9. 0009have hfirst : Le(S s · S s,p · S s)
    Exact native replay linehave hfirst : exists bcf_le_gap_bfsarpts_first. bcf_le_gap_bfsarpts_first + (S s * S s) = p * S s
  10. 0010specialize mul_le_mul_right (S s)
  11. 0011specialize mul_le_mul_right p
  12. 0012specialize mul_le_mul_right (S s)
  13. 0013apply mul_le_mul_right
  14. 0014exact habove
  15. 0015have hsecond : Le(p · S s,p · p)
    Exact native replay linehave hsecond : exists bcf_le_gap_bfsarpts_second. bcf_le_gap_bfsarpts_second + (p * S s) = p * p
  16. 0016specialize mul_le_mul_left (S s)
  17. 0017specialize mul_le_mul_left p
  18. 0018specialize mul_le_mul_left p
  19. 0019apply mul_le_mul_left
  20. 0020exact habove
  21. 0021have hsquare : Le(S s · S s,p · p)
    Exact native replay linehave hsquare : exists bcf_le_gap_bfsarpts_square. bcf_le_gap_bfsarpts_square + (S s * S s) = p * p
  22. 0022specialize le_trans (S s * S s)
  23. 0023specialize le_trans (p * S s)
  24. 0024specialize le_trans (p * p)
  25. 0025apply le_trans
  26. 0026exact hfirst
  27. 0027exact hsecond
  28. 0028have hraw : Lt(x,p · p)
    Exact native replay linehave hraw : exists bcf_lt_gap_bfsarpts_raw_result. bcf_lt_gap_bfsarpts_raw_result + S (x) = p * p
  29. 0029specialize lt_of_lt_of_le x
  30. 0030specialize lt_of_lt_of_le (S s * S s)
  31. 0031specialize lt_of_lt_of_le (p * p)
  32. 0032apply lt_of_lt_of_le
  33. 0033exact hfloor_right
  34. 0034exact hsquare
  35. 0035have hvalue : t = p * p
  36. 0036specialize pow_two p
  37. 0037specialize pow_two 2
  38. 0038specialize pow_two t
  39. 0039apply pow_two
  40. 0040refl
  41. 0041exact hpower
  42. 0042rewrite hvalue
  43. 0043exact hraw