BT0122 · Bertrand theorem

bertrand_cover_three_hundred_seventeen_five_hundred_twenty_one

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

The compact checked cover from 317 to 521.

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

Le(2 · (11 · 22) + 37,18 · 17 + 11 + (18 · 17 + 11))

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

1 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
exists bpr_le_gap_bb8c_three_seventeen_five_twenty_one. bpr_le_gap_bb8c_three_seventeen_five_twenty_one + (2 * (11 * 22) + 37) = (18 * 17 + 11 + (18 * 17 + 11))

Proof neighborhood

Direct theorem prerequisites

BT000B add_mul BT0007 mul_add BT0008 mul_assoc BT0006 mul_comm BT0003 add_assoc BT0002 add_comm BT0009 one_mul BT011P bertrand_add_six_permute

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

162 script commands · 54 reading checkpoints · 17 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 mulmul addmul assocmul commadd assocadd commone mulbertrand add six permute
01Establish h22L1–2

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

  1. L1
    have h22 : 22 = 17 + 5
  2. L2
    norm_num
02Establish htwoelevenL3–4

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

  1. L3
    have htwoeleven : 2 * 11 = 22
  2. L4
    norm_num
03Establish hsquareL5–8

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

  1. L5
    have hsquare : 22 * 22 = (17 + 5) * (17 + 5)
  2. L6
    congr
  3. L7
    exact h22
  4. L8
    exact h22
04Establish hproductL9–18

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

  1. L9
    have hproduct : (17 + 5) * (17 + 5) = (17 * 17 + 17 * 5) + (17 * 5 + 5 * 5)
  2. L10
    trans 17 * (17 + 5) + 5 * (17 + 5)
  3. L11
    apply add_mul
  4. L12
    trans (17 * 17 + 17 * 5) + (5 * 17 + 5 * 5)
  5. L13
    congr
  6. L14
    apply mul_add
  7. L15
    apply mul_add
  8. L16
    trans (17 * 17 + 17 * 5) + (17 * 5 + 5 * 5)
  9. L17
    congr
  10. L18
    refl
05Calculate and transport equalitiesL19–19

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

  1. L19
    congr
06Use earlier factsL20–20

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

  1. L20
    apply mul_comm
07Calculate and transport equalitiesL21–22

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

  1. L21
    refl
  2. L22
    refl
08Establish hBnormL23–32

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

  1. L23
    have hBnorm : 2 * (11 * 22) + 37 = 17 * 17 + (17 * 5 + (17 * 5 + 2 * 31))
  2. L24
    trans (2 * 11) * 22 + 37
  3. L25
    congr
  4. L26
    symm
  5. L27
    apply mul_assoc
  6. L28
    refl
  7. L29
    rewrite htwoeleven
  8. L30
    rewrite hsquare
  9. L31
    rewrite hproduct
  10. L32
    trans (17 * 17 + 17 * 5) + ((17 * 5 + 5 * 5) + 37)
09Use earlier factsL33–33

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

  1. L33
    apply add_assoc
10Calculate and transport equalitiesL34–34

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

  1. L34
    trans 17 * 17 + (17 * 5 + ((17 * 5 + 5 * 5) + 37))
11Use earlier factsL35–35

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

  1. L35
    apply add_assoc
12Calculate and transport equalitiesL36–40

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

  1. L36
    trans 17 * 17 + (17 * 5 + (17 * 5 + (5 * 5 + 37)))
  2. L37
    congr
  3. L38
    refl
  4. L39
    congr
  5. L40
    refl
13Use earlier factsL41–41

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

  1. L41
    apply add_assoc
14Establish htail_bL42–45

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

  1. L42
    have htail_b : 5 * 5 + 37 = 2 * 31
  2. L43
    norm_num
  3. L44
    rewrite htail_b
  4. L45
    refl
15Establish h18L46–47

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

  1. L46
    have h18 : 18 = 17 + 1
  2. L47
    norm_num
16Establish hAexpandL48–57

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

  1. L48
    have hAexpand : 18 * 17 + 11 = (17 * 17 + 17) + 11
  2. L49
    trans (17 + 1) * 17 + 11
  3. L50
    congr
  4. L51
    congr
  5. L52
    exact h18
  6. L53
    refl
  7. L54
    refl
  8. L55
    trans (17 * 17 + 1 * 17) + 11
  9. L56
    congr
  10. L57
    apply add_mul
17Calculate and transport equalitiesL58–58

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

  1. L58
    refl
18Establish honeL59–62

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

  1. L59
    have hone : 1 * 17 = 17
  2. L60
    apply one_mul
  3. L61
    rewrite hone
  4. L62
    refl
19Establish h12L63–64

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

  1. L63
    have h12 : 12 = 5 + 7
  2. L64
    norm_num
20Establish h7L65–66

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

  1. L65
    have h7 : 7 = 5 + 2
  2. L66
    norm_num
21Establish hRexpandL67–76

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

  1. L67
    have hRexpand : 17 * 12 = 17 * 5 + (17 * 5 + 17 * 2)
  2. L68
    trans 17 * (5 + 7)
  3. L69
    congr
  4. L70
    refl
  5. L71
    exact h12
  6. L72
    trans 17 * 5 + 17 * 7
  7. L73
    apply mul_add
  8. L74
    trans 17 * 5 + 17 * (5 + 2)
  9. L75
    congr
  10. L76
    refl
22Calculate and transport equalitiesL77–78

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

  1. L77
    congr
  2. L78
    refl
23Use earlier factsL79–79

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

  1. L79
    exact h7
24Calculate and transport equalitiesL80–82

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

  1. L80
    trans 17 * 5 + (17 * 5 + 17 * 2)
  2. L81
    congr
  3. L82
    refl
25Use earlier factsL83–83

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

  1. L83
    apply mul_add
26Calculate and transport equalitiesL84–84

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

  1. L84
    refl
27Establish hRnormL85–94

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

  1. L85
    have hRnorm : (18 * 17 + 11) + (17 * 12) = 17 * 17 + (17 * 5 + (17 * 5 + 2 * 31))
  2. L86
    rewrite hRexpand
  3. L87
    rewrite hAexpand
  4. L88
    trans (((17 * 17 + 17) + 11) + 17 * 5) + (17 * 5 + 17 * 2)
  5. L89
    symm
  6. L90
    apply add_assoc
  7. L91
    trans ((17 * 17 + 17) + (11 + 17 * 5)) + (17 * 5 + 17 * 2)
  8. L92
    congr
  9. L93
    apply add_assoc
  10. L94
    refl
28Calculate and transport equalitiesL95–95

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

  1. L95
    trans (17 * 17 + 17 * 5) + ((17 + 11) + (17 * 5 + 17 * 2))
29Use earlier factsL96–96

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

  1. L96
    apply bertrand_add_six_permute
30Calculate and transport equalitiesL97–97

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

  1. L97
    trans 17 * 17 + (17 * 5 + ((17 + 11) + (17 * 5 + 17 * 2)))
31Use earlier factsL98–98

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

  1. L98
    apply add_assoc
32Calculate and transport equalitiesL99–105

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

  1. L99
    trans 17 * 17 + (17 * 5 + (17 * 5 + ((17 + 11) + 17 * 2)))
  2. L100
    congr
  3. L101
    refl
  4. L102
    congr
  5. L103
    refl
  6. L104
    trans ((17 + 11) + 17 * 5) + 17 * 2
  7. L105
    symm
33Use earlier factsL106–106

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

  1. L106
    apply add_assoc
34Calculate and transport equalitiesL107–108

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

  1. L107
    trans (17 * 5 + (17 + 11)) + 17 * 2
  2. L108
    congr
35Use earlier factsL109–109

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

  1. L109
    apply add_comm
36Calculate and transport equalitiesL110–110

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

  1. L110
    refl
37Use earlier factsL111–111

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

  1. L111
    apply add_assoc
38Establish htail_rL112–115

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

  1. L112
    have htail_r : (17 + 11) + 17 * 2 = 2 * 31
  2. L113
    norm_num
  3. L114
    rewrite htail_r
  4. L115
    refl
39Establish hcarrierL116–120

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

  1. L116
    have hcarrier : 2 * (11 * 22) + 37 = (18 * 17 + 11) + (17 * 12)
  2. L117
    trans 17 * 17 + (17 * 5 + (17 * 5 + 2 * 31))
  3. L118
    exact hBnorm
  4. L119
    symm
  5. L120
    exact hRnorm
40Establish hgapL121–130

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

  1. L121
    have hgap : (6 * 17 + 11) + (17 * 12) = 18 * 17 + 11
  2. L122
    trans 6 * 17 + (11 + (17 * 12))
  3. L123
    apply add_assoc
  4. L124
    trans 6 * 17 + ((17 * 12) + 11)
  5. L125
    congr
  6. L126
    refl
  7. L127
    apply add_comm
  8. L128
    trans (6 * 17 + (17 * 12)) + 11
  9. L129
    symm
  10. L130
    apply add_assoc
41Calculate and transport equalitiesL131–133

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

  1. L131
    trans (17 * 6 + (17 * 12)) + 11
  2. L132
    congr
  3. L133
    congr
42Use earlier factsL134–134

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

  1. L134
    apply mul_comm
43Calculate and transport equalitiesL135–139

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

  1. L135
    refl
  2. L136
    refl
  3. L137
    trans 17 * (6 + 12) + 11
  4. L138
    congr
  5. L139
    symm
44Use earlier factsL140–140

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

  1. L140
    apply mul_add
45Calculate and transport equalitiesL141–141

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

  1. L141
    refl
46Establish hsumL142–149

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

  1. L142
    have hsum : 6 + 12 = 18
  2. L143
    norm_num
  3. L144
    rewrite hsum
  4. L145
    trans 18 * 17 + 11
  5. L146
    congr
  6. L147
    apply mul_comm
  7. L148
    refl
  8. L149
    refl
47Construct an explicit witnessL150–150

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

  1. L150
    exists 6 * 17 + 11
48Calculate and transport equalitiesL151–153

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

  1. L151
    rewrite hcarrier
  2. L152
    trans ((6 * 17 + 11) + (18 * 17 + 11)) + (17 * 12)
  3. L153
    symm
49Use earlier factsL154–154

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

  1. L154
    apply add_assoc
50Calculate and transport equalitiesL155–156

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

  1. L155
    trans ((18 * 17 + 11) + (6 * 17 + 11)) + (17 * 12)
  2. L156
    congr
51Use earlier factsL157–157

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

  1. L157
    apply add_comm
52Calculate and transport equalitiesL158–159

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

  1. L158
    refl
  2. L159
    trans (18 * 17 + 11) + ((6 * 17 + 11) + (17 * 12))
53Use earlier factsL160–160

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

  1. L160
    apply add_assoc
54Calculate and transport equalitiesL161–162

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

  1. L161
    rewrite hgap
  2. L162
    refl

Library-wide reading audit

Original defined command ledger · 162 lines
  1. 0001have h22 : 22 = 17 + 5
  2. 0002norm_num
  3. 0003have htwoeleven : 2 * 11 = 22
  4. 0004norm_num
  5. 0005have hsquare : 22 * 22 = (17 + 5) * (17 + 5)
  6. 0006congr
  7. 0007exact h22
  8. 0008exact h22
  9. 0009have hproduct : (17 + 5) * (17 + 5) = (17 * 17 + 17 * 5) + (17 * 5 + 5 * 5)
  10. 0010trans 17 * (17 + 5) + 5 * (17 + 5)
  11. 0011apply add_mul
  12. 0012trans (17 * 17 + 17 * 5) + (5 * 17 + 5 * 5)
  13. 0013congr
  14. 0014apply mul_add
  15. 0015apply mul_add
  16. 0016trans (17 * 17 + 17 * 5) + (17 * 5 + 5 * 5)
  17. 0017congr
  18. 0018refl
  19. 0019congr
  20. 0020apply mul_comm
  21. 0021refl
  22. 0022refl
  23. 0023have hBnorm : 2 * (11 * 22) + 37 = 17 * 17 + (17 * 5 + (17 * 5 + 2 * 31))
  24. 0024trans (2 * 11) * 22 + 37
  25. 0025congr
  26. 0026symm
  27. 0027apply mul_assoc
  28. 0028refl
  29. 0029rewrite htwoeleven
  30. 0030rewrite hsquare
  31. 0031rewrite hproduct
  32. 0032trans (17 * 17 + 17 * 5) + ((17 * 5 + 5 * 5) + 37)
  33. 0033apply add_assoc
  34. 0034trans 17 * 17 + (17 * 5 + ((17 * 5 + 5 * 5) + 37))
  35. 0035apply add_assoc
  36. 0036trans 17 * 17 + (17 * 5 + (17 * 5 + (5 * 5 + 37)))
  37. 0037congr
  38. 0038refl
  39. 0039congr
  40. 0040refl
  41. 0041apply add_assoc
  42. 0042have htail_b : 5 * 5 + 37 = 2 * 31
  43. 0043norm_num
  44. 0044rewrite htail_b
  45. 0045refl
  46. 0046have h18 : 18 = 17 + 1
  47. 0047norm_num
  48. 0048have hAexpand : 18 * 17 + 11 = (17 * 17 + 17) + 11
  49. 0049trans (17 + 1) * 17 + 11
  50. 0050congr
  51. 0051congr
  52. 0052exact h18
  53. 0053refl
  54. 0054refl
  55. 0055trans (17 * 17 + 1 * 17) + 11
  56. 0056congr
  57. 0057apply add_mul
  58. 0058refl
  59. 0059have hone : 1 * 17 = 17
  60. 0060apply one_mul
  61. 0061rewrite hone
  62. 0062refl
  63. 0063have h12 : 12 = 5 + 7
  64. 0064norm_num
  65. 0065have h7 : 7 = 5 + 2
  66. 0066norm_num
  67. 0067have hRexpand : 17 * 12 = 17 * 5 + (17 * 5 + 17 * 2)
  68. 0068trans 17 * (5 + 7)
  69. 0069congr
  70. 0070refl
  71. 0071exact h12
  72. 0072trans 17 * 5 + 17 * 7
  73. 0073apply mul_add
  74. 0074trans 17 * 5 + 17 * (5 + 2)
  75. 0075congr
  76. 0076refl
  77. 0077congr
  78. 0078refl
  79. 0079exact h7
  80. 0080trans 17 * 5 + (17 * 5 + 17 * 2)
  81. 0081congr
  82. 0082refl
  83. 0083apply mul_add
  84. 0084refl
  85. 0085have hRnorm : (18 * 17 + 11) + (17 * 12) = 17 * 17 + (17 * 5 + (17 * 5 + 2 * 31))
  86. 0086rewrite hRexpand
  87. 0087rewrite hAexpand
  88. 0088trans (((17 * 17 + 17) + 11) + 17 * 5) + (17 * 5 + 17 * 2)
  89. 0089symm
  90. 0090apply add_assoc
  91. 0091trans ((17 * 17 + 17) + (11 + 17 * 5)) + (17 * 5 + 17 * 2)
  92. 0092congr
  93. 0093apply add_assoc
  94. 0094refl
  95. 0095trans (17 * 17 + 17 * 5) + ((17 + 11) + (17 * 5 + 17 * 2))
  96. 0096apply bertrand_add_six_permute
  97. 0097trans 17 * 17 + (17 * 5 + ((17 + 11) + (17 * 5 + 17 * 2)))
  98. 0098apply add_assoc
  99. 0099trans 17 * 17 + (17 * 5 + (17 * 5 + ((17 + 11) + 17 * 2)))
  100. 0100congr
  101. 0101refl
  102. 0102congr
  103. 0103refl
  104. 0104trans ((17 + 11) + 17 * 5) + 17 * 2
  105. 0105symm
  106. 0106apply add_assoc
  107. 0107trans (17 * 5 + (17 + 11)) + 17 * 2
  108. 0108congr
  109. 0109apply add_comm
  110. 0110refl
  111. 0111apply add_assoc
  112. 0112have htail_r : (17 + 11) + 17 * 2 = 2 * 31
  113. 0113norm_num
  114. 0114rewrite htail_r
  115. 0115refl
  116. 0116have hcarrier : 2 * (11 * 22) + 37 = (18 * 17 + 11) + (17 * 12)
  117. 0117trans 17 * 17 + (17 * 5 + (17 * 5 + 2 * 31))
  118. 0118exact hBnorm
  119. 0119symm
  120. 0120exact hRnorm
  121. 0121have hgap : (6 * 17 + 11) + (17 * 12) = 18 * 17 + 11
  122. 0122trans 6 * 17 + (11 + (17 * 12))
  123. 0123apply add_assoc
  124. 0124trans 6 * 17 + ((17 * 12) + 11)
  125. 0125congr
  126. 0126refl
  127. 0127apply add_comm
  128. 0128trans (6 * 17 + (17 * 12)) + 11
  129. 0129symm
  130. 0130apply add_assoc
  131. 0131trans (17 * 6 + (17 * 12)) + 11
  132. 0132congr
  133. 0133congr
  134. 0134apply mul_comm
  135. 0135refl
  136. 0136refl
  137. 0137trans 17 * (6 + 12) + 11
  138. 0138congr
  139. 0139symm
  140. 0140apply mul_add
  141. 0141refl
  142. 0142have hsum : 6 + 12 = 18
  143. 0143norm_num
  144. 0144rewrite hsum
  145. 0145trans 18 * 17 + 11
  146. 0146congr
  147. 0147apply mul_comm
  148. 0148refl
  149. 0149refl
  150. 0150exists 6 * 17 + 11
  151. 0151rewrite hcarrier
  152. 0152trans ((6 * 17 + 11) + (18 * 17 + 11)) + (17 * 12)
  153. 0153symm
  154. 0154apply add_assoc
  155. 0155trans ((18 * 17 + 11) + (6 * 17 + 11)) + (17 * 12)
  156. 0156congr
  157. 0157apply add_comm
  158. 0158refl
  159. 0159trans (18 * 17 + 11) + ((6 * 17 + 11) + (17 * 12))
  160. 0160apply add_assoc
  161. 0161rewrite hgap
  162. 0162refl