BT010B · Bertrand theorem

floor_sqrt_two_le_of_two_lt

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

The floor root of twice a natural above two is at least two.

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. Lt(2,n) → FloorSqrt(n + n,s) → Lt(1,s)

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 PD0051 FloorSqrt

3 occurrences

In local proof propositions

PD0001 Le PD0002 Lt

10 occurrences

Exact expanded native-PA statement
forall n s. (exists bcf_lt_gap_b5rbfstl_positive. bcf_lt_gap_b5rbfstl_positive + S (2) = n) -> (((exists bcs_sqrt_lower_gap_b5rbfstl_floor. bcs_sqrt_lower_gap_b5rbfstl_floor + (s) * (s) = (n + n)) /\ exists bcs_sqrt_upper_gap_b5rbfstl_floor. bcs_sqrt_upper_gap_b5rbfstl_floor + S (n + n) = S (s) * S (s))) -> (exists bcf_le_gap_b5rbfstl_result. bcf_le_gap_b5rbfstl_result + (2) = s)

Proof neighborhood

Direct theorem prerequisites

BT001G le_or_lt BT000E le_refl BT0018 le_succ BT001D lt_of_lt_of_le BT0097 lt_three_cases BT00R7 floor_sqrt_strict_upper_bound BT010A two_lt_double_lower_six BT000F le_trans BT001I lt_not_le BT001B lt_irrefl_expanded

Direct theorem dependents

BT010D floor_sqrt_three_mul_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

79 script commands · 27 reading checkpoints · 10 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 (10)
le or ltle reflle succlt of lt of lelt three casesfloor sqrt strict upper boundtwo lt double lower sixle translt not lelt irrefl expanded
01Fix variables and assumptionsL1–4

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

  1. L1
    intro n
  2. L2
    intro s
  3. L3
    intro hpositive
  4. L4
    intro hfloor
02Establish hcasesL5–8

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

  1. L5
    have hcases : Lt(1,s) ∨ Lt(s,2)Definitions: Lt(1,s)Lt(s,2)Original native command in the exact edition
  2. L6
    specialize le_or_lt 2
  3. L7
    specialize le_or_lt s
  4. L8
    exact le_or_lt
03Separate the logical casesL9–9

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

  1. L9
    cases hcases
04Use earlier factsL10–10

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

  1. L10
    exact hcases_left
05Establish htwo_threeL11–16

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

  1. L11
    have htwo_three : Lt(1,3)Definitions: Lt(1,3)Original native command in the exact edition
  2. L12
    specialize le_refl 2
  3. L13
    specialize le_succ 2
  4. L14
    specialize le_succ 2
  5. L15
    apply le_succ
  6. L16
    exact le_refl
06Establish hthreeL17–23

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

  1. L17
    have hthree : Lt(s,3)Definitions: Lt(s,3)Original native command in the exact edition
  2. L18
    specialize lt_of_lt_of_le s
  3. L19
    specialize lt_of_lt_of_le 2
  4. L20
    specialize lt_of_lt_of_le 3
  5. L21
    apply lt_of_lt_of_le
  6. L22
    exact hcases_right
  7. L23
    exact htwo_three
07Establish hsmall_casesL24–27

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

  1. L24
    have hsmall_cases : s = 0 \/ s = 1 \/ s = 2
  2. L25
    specialize lt_three_cases s
  3. L26
    apply lt_three_cases
  4. L27
    exact hthree
08Establish hupperL28–32

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply floor sqrt strict upper bound.

  1. L28
    have hupper : Lt(n + n,S s · S s)Definitions: Lt(n + n,S s · S s)Original native command in the exact edition
  2. L29
    specialize floor_sqrt_strict_upper_bound (n + n)
  3. L30
    specialize floor_sqrt_strict_upper_bound s
  4. L31
    apply floor_sqrt_strict_upper_bound
  5. L32
    exact hfloor
09Establish hlowerL33–36

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

  1. L33
    have hlower : Le(3 + 3,n + n)Definitions: Le(3 + 3,n + n)Original native command in the exact edition
  2. L34
    specialize two_lt_double_lower_six n
  3. L35
    apply two_lt_double_lower_six
  4. L36
    exact hpositive
10Separate the logical casesL37–38

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

  1. L37
    cases hsmall_cases
  2. L38
    cases hsmall_cases_left
11Calculate and transport equalitiesL39–40

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L39
    rewrite hsmall_cases_left_left at hupper
  2. L40
    rewrite hsmall_cases_left_left at hupper
12Establish hsmallL41–41

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

  1. L41
    have hsmall : Le(1 · 1,3 + 3)Definitions: Le(1 · 1,3 + 3)Original native command in the exact edition
13Construct an explicit witnessL42–42

Supply the displayed value, then prove that it has the required property.

  1. L42
    exists 5
14Calculate and transport equalitiesL43–43

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L43
    norm_num
15Establish hreverseL44–50

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

  1. L44
    have hreverse : Le(1 · 1,n + n)Definitions: Le(1 · 1,n + n)Original native command in the exact edition
  2. L45
    specialize le_trans (S 0 * S 0)
  3. L46
    specialize le_trans (3 + 3)
  4. L47
    specialize le_trans (n + n)
  5. L48
    apply le_trans
  6. L49
    exact hsmall
  7. L50
    exact hlower
16Separate the logical casesL51–51

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

  1. L51
    exfalso
17Use earlier factsL52–56

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

  1. L52
    specialize lt_not_le (n + n)
  2. L53
    specialize lt_not_le (S 0 * S 0)
  3. L54
    apply lt_not_le
  4. L55
    exact hupper
  5. L56
    exact hreverse
18Calculate and transport equalitiesL57–58

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L57
    rewrite hsmall_cases_left_right at hupper
  2. L58
    rewrite hsmall_cases_left_right at hupper
19Establish hsmallL59–59

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

  1. L59
    have hsmall : Le(2 · 2,3 + 3)Definitions: Le(2 · 2,3 + 3)Original native command in the exact edition
20Construct an explicit witnessL60–60

Supply the displayed value, then prove that it has the required property.

  1. L60
    exists 2
21Calculate and transport equalitiesL61–61

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L61
    norm_num
22Establish hreverseL62–68

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

  1. L62
    have hreverse : Le(2 · 2,n + n)Definitions: Le(2 · 2,n + n)Original native command in the exact edition
  2. L63
    specialize le_trans (S 1 * S 1)
  3. L64
    specialize le_trans (3 + 3)
  4. L65
    specialize le_trans (n + n)
  5. L66
    apply le_trans
  6. L67
    exact hsmall
  7. L68
    exact hlower
23Separate the logical casesL69–69

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

  1. L69
    exfalso
24Use earlier factsL70–74

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

  1. L70
    specialize lt_not_le (n + n)
  2. L71
    specialize lt_not_le (S 1 * S 1)
  3. L72
    apply lt_not_le
  4. L73
    exact hupper
  5. L74
    exact hreverse
25Calculate and transport equalitiesL75–75

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L75
    rewrite hsmall_cases_right at hcases_right
26Separate the logical casesL76–76

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

  1. L76
    exfalso
27Use earlier factsL77–79

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

  1. L77
    specialize lt_irrefl_expanded 2
  2. L78
    apply lt_irrefl_expanded
  3. L79
    exact hcases_right

Library-wide reading audit

Original defined command ledger · 79 lines
  1. 0001intro n
  2. 0002intro s
  3. 0003intro hpositive
  4. 0004intro hfloor
  5. 0005have hcases : Lt(1,s) ∨ Lt(s,2)
    Exact native replay linehave hcases : (exists bcf_le_gap_b5rbfstl_result. bcf_le_gap_b5rbfstl_result + (2) = s) \/ (exists bcf_lt_gap_b5rbfstl_reverse. bcf_lt_gap_b5rbfstl_reverse + S (s) = 2)
  6. 0006specialize le_or_lt 2
  7. 0007specialize le_or_lt s
  8. 0008exact le_or_lt
  9. 0009cases hcases
  10. 0010exact hcases_left
  11. 0011have htwo_three : Lt(1,3)
    Exact native replay linehave htwo_three : exists k. k + 2 = 3
  12. 0012specialize le_refl 2
  13. 0013specialize le_succ 2
  14. 0014specialize le_succ 2
  15. 0015apply le_succ
  16. 0016exact le_refl
  17. 0017have hthree : Lt(s,3)
    Exact native replay linehave hthree : exists bcf_lt_gap_b5rbfstl_three. bcf_lt_gap_b5rbfstl_three + S (s) = 3
  18. 0018specialize lt_of_lt_of_le s
  19. 0019specialize lt_of_lt_of_le 2
  20. 0020specialize lt_of_lt_of_le 3
  21. 0021apply lt_of_lt_of_le
  22. 0022exact hcases_right
  23. 0023exact htwo_three
  24. 0024have hsmall_cases : s = 0 \/ s = 1 \/ s = 2
  25. 0025specialize lt_three_cases s
  26. 0026apply lt_three_cases
  27. 0027exact hthree
  28. 0028have hupper : Lt(n + n,S s · S s)
    Exact native replay linehave hupper : exists bcf_lt_gap_b5rbfstl_upper. bcf_lt_gap_b5rbfstl_upper + S (n + n) = S s * S s
  29. 0029specialize floor_sqrt_strict_upper_bound (n + n)
  30. 0030specialize floor_sqrt_strict_upper_bound s
  31. 0031apply floor_sqrt_strict_upper_bound
  32. 0032exact hfloor
  33. 0033have hlower : Le(3 + 3,n + n)
    Exact native replay linehave hlower : exists bcf_le_gap_b5rbfstl_lower_six. bcf_le_gap_b5rbfstl_lower_six + (3 + 3) = n + n
  34. 0034specialize two_lt_double_lower_six n
  35. 0035apply two_lt_double_lower_six
  36. 0036exact hpositive
  37. 0037cases hsmall_cases
  38. 0038cases hsmall_cases_left
  39. 0039rewrite hsmall_cases_left_left at hupper
  40. 0040rewrite hsmall_cases_left_left at hupper
  41. 0041have hsmall : Le(1 · 1,3 + 3)
    Exact native replay linehave hsmall : exists bcf_le_gap_b5rbfstl_zero_small. bcf_le_gap_b5rbfstl_zero_small + (S 0 * S 0) = 3 + 3
  42. 0042exists 5
  43. 0043norm_num
  44. 0044have hreverse : Le(1 · 1,n + n)
    Exact native replay linehave hreverse : exists bcf_le_gap_b5rbfstl_zero_reverse. bcf_le_gap_b5rbfstl_zero_reverse + (S 0 * S 0) = n + n
  45. 0045specialize le_trans (S 0 * S 0)
  46. 0046specialize le_trans (3 + 3)
  47. 0047specialize le_trans (n + n)
  48. 0048apply le_trans
  49. 0049exact hsmall
  50. 0050exact hlower
  51. 0051exfalso
  52. 0052specialize lt_not_le (n + n)
  53. 0053specialize lt_not_le (S 0 * S 0)
  54. 0054apply lt_not_le
  55. 0055exact hupper
  56. 0056exact hreverse
  57. 0057rewrite hsmall_cases_left_right at hupper
  58. 0058rewrite hsmall_cases_left_right at hupper
  59. 0059have hsmall : Le(2 · 2,3 + 3)
    Exact native replay linehave hsmall : exists bcf_le_gap_b5rbfstl_one_small. bcf_le_gap_b5rbfstl_one_small + (S 1 * S 1) = 3 + 3
  60. 0060exists 2
  61. 0061norm_num
  62. 0062have hreverse : Le(2 · 2,n + n)
    Exact native replay linehave hreverse : exists bcf_le_gap_b5rbfstl_one_reverse. bcf_le_gap_b5rbfstl_one_reverse + (S 1 * S 1) = n + n
  63. 0063specialize le_trans (S 1 * S 1)
  64. 0064specialize le_trans (3 + 3)
  65. 0065specialize le_trans (n + n)
  66. 0066apply le_trans
  67. 0067exact hsmall
  68. 0068exact hlower
  69. 0069exfalso
  70. 0070specialize lt_not_le (n + n)
  71. 0071specialize lt_not_le (S 1 * S 1)
  72. 0072apply lt_not_le
  73. 0073exact hupper
  74. 0074exact hreverse
  75. 0075rewrite hsmall_cases_right at hcases_right
  76. 0076exfalso
  77. 0077specialize lt_irrefl_expanded 2
  78. 0078apply lt_irrefl_expanded
  79. 0079exact hcases_right