BT0123 · Bertrand theorem

bertrand_cutoff_lt_final_prime

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

The factorized production cutoff lies below the final prime.

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

Lt(16 · 32,2 · (11 · 22) + 37)

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

1 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
exists bpr_gap_bb8s_cutoff_final. bpr_gap_bb8s_cutoff_final + S (16 * 32) = 2 * (11 * 22) + 37

Proof neighborhood

Direct theorem prerequisites

BT0001 add_succ_left BT0007 mul_add BT011O bertrand_add_swap_nested BT0006 mul_comm BT000B add_mul BT0003 add_assoc BT0002 add_comm BT0008 mul_assoc

Direct theorem dependents

BT0124 bertrand_small_closed_upper

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

103 script commands · 32 reading checkpoints · 12 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 (8)
add succ leftmul addbertrand add swap nestedmul commadd muladd assocadd commmul assoc
01Construct an explicit witnessL1–1

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

  1. L1
    exists 8
02Establish hsuccL2–6

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

  1. L2
    have hsucc : 8 + S (16 * 32) = 9 + (16 * 32)
  2. L3
    trans S (8 + (16 * 32))
  3. L4
    apply PA4
  4. L5
    symm
  5. L6
    apply add_succ_left
03Establish h32L7–8

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

  1. L7
    have h32 : 32 = 22 + 10
  2. L8
    norm_num
04Establish hleftL9–18

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

  1. L9
    have hleft : 9 + (16 * 32) = 22 * 16 + (10 * 6 + (9 + 10 * 10))
  2. L10
    rewrite h32
  3. L11
    trans 9 + (16 * 22 + 16 * 10)
  4. L12
    congr
  5. L13
    refl
  6. L14
    apply mul_add
  7. L15
    trans 16 * 22 + (9 + 16 * 10)
  8. L16
    apply bertrand_add_swap_nested
  9. L17
    trans 22 * 16 + (9 + 16 * 10)
  10. L18
    congr
05Use earlier factsL19–19

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

  1. L19
    apply mul_comm
06Calculate and transport equalitiesL20–20

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

  1. L20
    refl
07Establish h16L21–22

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

  1. L21
    have h16 : 16 = 10 + 6
  2. L22
    norm_num
08Establish htail16L23–32

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

  1. L23
    have htail16 : 16 * 10 = (10 + 6) * 10
  2. L24
    congr
  3. L25
    exact h16
  4. L26
    refl
  5. L27
    rewrite htail16
  6. L28
    trans 22 * 16 + (9 + (10 * 10 + 6 * 10))
  7. L29
    congr
  8. L30
    refl
  9. L31
    congr
  10. L32
    refl
09Use earlier factsL33–33

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

  1. L33
    apply add_mul
10Calculate and transport equalitiesL34–40

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

  1. L34
    trans 22 * 16 + (9 + (10 * 10 + 10 * 6))
  2. L35
    congr
  3. L36
    refl
  4. L37
    congr
  5. L38
    refl
  6. L39
    congr
  7. L40
    refl
11Use earlier factsL41–41

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

  1. L41
    apply mul_comm
12Calculate and transport equalitiesL42–45

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

  1. L42
    trans 22 * 16 + ((9 + 10 * 10) + 10 * 6)
  2. L43
    congr
  3. L44
    refl
  4. L45
    symm
13Use earlier factsL46–46

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

  1. L46
    apply add_assoc
14Calculate and transport equalitiesL47–49

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

  1. L47
    trans 22 * 16 + (10 * 6 + (9 + 10 * 10))
  2. L48
    congr
  3. L49
    refl
15Use earlier factsL50–50

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

  1. L50
    apply add_comm
16Calculate and transport equalitiesL51–51

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

  1. L51
    refl
17Establish htwoelevenL52–53

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

  1. L52
    have htwoeleven : 2 * 11 = 22
  2. L53
    norm_num
18Establish h22sixteenL54–55

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

  1. L54
    have h22sixteen : 22 = 16 + 6
  2. L55
    norm_num
19Establish h22twelveL56–57

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

  1. L56
    have h22twelve : 22 = 10 + 12
  2. L57
    norm_num
20Establish hrightL58–67

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

  1. L58
    have hright : (2 * (11 * 22) + 37) = 22 * 16 + (10 * 6 + (12 * 6 + 37))
  2. L59
    trans (2 * 11) * 22 + 37
  3. L60
    congr
  4. L61
    symm
  5. L62
    apply mul_assoc
  6. L63
    refl
  7. L64
    rewrite htwoeleven
  8. L65
    trans 22 * (16 + 6) + 37
  9. L66
    congr
  10. L67
    congr
21Calculate and transport equalitiesL68–68

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

  1. L68
    refl
22Use earlier factsL69–69

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

  1. L69
    exact h22sixteen
23Calculate and transport equalitiesL70–72

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

  1. L70
    refl
  2. L71
    trans (22 * 16 + 22 * 6) + 37
  3. L72
    congr
24Use earlier factsL73–73

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

  1. L73
    apply mul_add
25Calculate and transport equalitiesL74–75

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

  1. L74
    refl
  2. L75
    trans 22 * 16 + (22 * 6 + 37)
26Use earlier factsL76–76

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

  1. L76
    apply add_assoc
27Establish htail22L77–86

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

  1. L77
    have htail22 : 22 * 6 = (10 + 12) * 6
  2. L78
    congr
  3. L79
    exact h22twelve
  4. L80
    refl
  5. L81
    rewrite htail22
  6. L82
    trans 22 * 16 + ((10 * 6 + 12 * 6) + 37)
  7. L83
    congr
  8. L84
    refl
  9. L85
    congr
  10. L86
    apply add_mul
28Calculate and transport equalitiesL87–90

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

  1. L87
    refl
  2. L88
    trans 22 * 16 + (10 * 6 + (12 * 6 + 37))
  3. L89
    congr
  4. L90
    refl
29Use earlier factsL91–91

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

  1. L91
    apply add_assoc
30Calculate and transport equalitiesL92–92

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

  1. L92
    refl
31Establish htailL93–95

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

  1. L93
    have htail : 9 + 10 * 10 = 12 * 6 + 37
  2. L94
    norm_num
  3. L95
    rewrite htail at hleft
32Establish hcarrierL96–103

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

  1. L96
    have hcarrier : 9 + (16 * 32) = (2 * (11 * 22) + 37)
  2. L97
    trans 22 * 16 + (10 * 6 + (12 * 6 + 37))
  3. L98
    exact hleft
  4. L99
    symm
  5. L100
    exact hright
  6. L101
    trans 9 + (16 * 32)
  7. L102
    exact hsucc
  8. L103
    exact hcarrier

Library-wide reading audit

Original defined command ledger · 103 lines
  1. 0001exists 8
  2. 0002have hsucc : 8 + S (16 * 32) = 9 + (16 * 32)
  3. 0003trans S (8 + (16 * 32))
  4. 0004apply PA4
  5. 0005symm
  6. 0006apply add_succ_left
  7. 0007have h32 : 32 = 22 + 10
  8. 0008norm_num
  9. 0009have hleft : 9 + (16 * 32) = 22 * 16 + (10 * 6 + (9 + 10 * 10))
  10. 0010rewrite h32
  11. 0011trans 9 + (16 * 22 + 16 * 10)
  12. 0012congr
  13. 0013refl
  14. 0014apply mul_add
  15. 0015trans 16 * 22 + (9 + 16 * 10)
  16. 0016apply bertrand_add_swap_nested
  17. 0017trans 22 * 16 + (9 + 16 * 10)
  18. 0018congr
  19. 0019apply mul_comm
  20. 0020refl
  21. 0021have h16 : 16 = 10 + 6
  22. 0022norm_num
  23. 0023have htail16 : 16 * 10 = (10 + 6) * 10
  24. 0024congr
  25. 0025exact h16
  26. 0026refl
  27. 0027rewrite htail16
  28. 0028trans 22 * 16 + (9 + (10 * 10 + 6 * 10))
  29. 0029congr
  30. 0030refl
  31. 0031congr
  32. 0032refl
  33. 0033apply add_mul
  34. 0034trans 22 * 16 + (9 + (10 * 10 + 10 * 6))
  35. 0035congr
  36. 0036refl
  37. 0037congr
  38. 0038refl
  39. 0039congr
  40. 0040refl
  41. 0041apply mul_comm
  42. 0042trans 22 * 16 + ((9 + 10 * 10) + 10 * 6)
  43. 0043congr
  44. 0044refl
  45. 0045symm
  46. 0046apply add_assoc
  47. 0047trans 22 * 16 + (10 * 6 + (9 + 10 * 10))
  48. 0048congr
  49. 0049refl
  50. 0050apply add_comm
  51. 0051refl
  52. 0052have htwoeleven : 2 * 11 = 22
  53. 0053norm_num
  54. 0054have h22sixteen : 22 = 16 + 6
  55. 0055norm_num
  56. 0056have h22twelve : 22 = 10 + 12
  57. 0057norm_num
  58. 0058have hright : (2 * (11 * 22) + 37) = 22 * 16 + (10 * 6 + (12 * 6 + 37))
  59. 0059trans (2 * 11) * 22 + 37
  60. 0060congr
  61. 0061symm
  62. 0062apply mul_assoc
  63. 0063refl
  64. 0064rewrite htwoeleven
  65. 0065trans 22 * (16 + 6) + 37
  66. 0066congr
  67. 0067congr
  68. 0068refl
  69. 0069exact h22sixteen
  70. 0070refl
  71. 0071trans (22 * 16 + 22 * 6) + 37
  72. 0072congr
  73. 0073apply mul_add
  74. 0074refl
  75. 0075trans 22 * 16 + (22 * 6 + 37)
  76. 0076apply add_assoc
  77. 0077have htail22 : 22 * 6 = (10 + 12) * 6
  78. 0078congr
  79. 0079exact h22twelve
  80. 0080refl
  81. 0081rewrite htail22
  82. 0082trans 22 * 16 + ((10 * 6 + 12 * 6) + 37)
  83. 0083congr
  84. 0084refl
  85. 0085congr
  86. 0086apply add_mul
  87. 0087refl
  88. 0088trans 22 * 16 + (10 * 6 + (12 * 6 + 37))
  89. 0089congr
  90. 0090refl
  91. 0091apply add_assoc
  92. 0092refl
  93. 0093have htail : 9 + 10 * 10 = 12 * 6 + 37
  94. 0094norm_num
  95. 0095rewrite htail at hleft
  96. 0096have hcarrier : 9 + (16 * 32) = (2 * (11 * 22) + 37)
  97. 0097trans 22 * 16 + (10 * 6 + (12 * 6 + 37))
  98. 0098exact hleft
  99. 0099symm
  100. 0100exact hright
  101. 0101trans 9 + (16 * 32)
  102. 0102exact hsucc
  103. 0103exact hcarrier