BT0124 · Bertrand theorem

bertrand_small_closed_upper

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

Every nonzero input below 16*32 has a closed Bertrand witness.

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. ¬n = 0 → Lt(n,16 · 32) → ∃ x. Prime(x) ∧ (Lt(n,x) ∧ Le(x,n + n))

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 PD0002 Lt PD0004 Prime

4 occurrences

In local proof propositions

PD0001 Le PD0002 Lt

32 occurrences

Exact expanded native-PA statement
forall n. ~(n = 0) -> (exists bpr_gap_bb8s_cutoff_bound. bpr_gap_bb8s_cutoff_bound + S (n) = 16 * 32) -> (exists p. ((~(p = 1) /\ forall bpr_left_bb8s_result_prime bpr_right_bb8s_result_prime. p = bpr_left_bb8s_result_prime * bpr_right_bb8s_result_prime -> bpr_left_bb8s_result_prime = 1 \/ bpr_right_bb8s_result_prime = 1)) /\ ((exists bpr_gap_bb8s_result_lower. bpr_gap_bb8s_result_lower + S (n) = p) /\ (exists bpr_le_gap_bb8s_result_upper. bpr_le_gap_bb8s_result_upper + (p) = (n + n))))

Proof neighborhood

Direct theorem prerequisites

BT000R nonzero_is_succ BT001G le_or_lt BT001F lt_trans BT0123 bertrand_cutoff_lt_final_prime BT011Q bertrand_covering_interval BT011N prime_five_hundred_twenty_one BT0122 bertrand_cover_three_hundred_seventeen_five_hundred_twenty_one BT011M prime_three_hundred_seventeen BT0121 bertrand_cover_one_hundred_sixty_three_three_hundred_seventeen BT011L prime_one_hundred_sixty_three BT0120 bertrand_cover_eighty_three_one_hundred_sixty_three BT011K prime_eighty_three BT011Y bertrand_cover_forty_three_eighty_three BT011J prime_forty_three BT011X bertrand_cover_twenty_three_forty_three BT011I prime_twenty_three BT011W bertrand_cover_thirteen_twenty_three BT011H prime_thirteen BT011V bertrand_cover_seven_thirteen BT011G prime_seven BT011U bertrand_cover_five_seven BT011F prime_five BT011T bertrand_cover_three_five BT006N prime_three BT011S bertrand_cover_two_three BT0025 prime_two BT011R bertrand_cover_one_two

Direct theorem dependents

BT0125 bertrand_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

179 script commands · 46 reading checkpoints · 23 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 (27)
nonzero is succle or ltlt transbertrand cutoff lt final primebertrand covering intervalprime five hundred twenty onebertrand cover three hundred seventeen five hundred twenty oneprime three hundred seventeenbertrand cover one hundred sixty three three hundred seventeenprime one hundred sixty threebertrand cover eighty three one hundred sixty threeprime eighty threebertrand cover forty three eighty threeprime forty threebertrand cover twenty three forty threeprime twenty threebertrand cover thirteen twenty threeprime thirteenbertrand cover seven thirteenprime sevenbertrand cover five sevenprime fivebertrand cover three fiveprime threebertrand cover two threeprime twobertrand cover one two
01Fix variables and assumptionsL1–3

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

  1. L1
    intro n
  2. L2
    intro hnonzero
  3. L3
    intro hcutoff
02Establish hshapeL4–7

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

  1. L4
    have hshape : exists k. n = S k
  2. L5
    specialize nonzero_is_succ n
  3. L6
    apply nonzero_is_succ
  4. L7
    exact hnonzero
03Separate the logical casesL8–8

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

  1. L8
    cases hshape
04Establish hlower_1L9–9

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

  1. L9
    have hlower_1 : Lt(0,n)Definitions: Lt(0,n)Original native command in the exact edition
05Construct an explicit witnessL10–10

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

  1. L10
    exists x
06Calculate and transport equalitiesL11–14

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

  1. L11
    rewrite hshape_witness
  2. L12
    rewrite PA4
  3. L13
    rewrite PA3
  4. L14
    refl
07Establish hsplit_1L15–18

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

  1. L15
    have hsplit_1 : Lt(1,n) ∨ Lt(n,2)Definitions: Lt(1,n)Lt(n,2)Original native command in the exact edition
  2. L16
    specialize le_or_lt (2)
  3. L17
    specialize le_or_lt n
  4. L18
    exact le_or_lt
08Separate the logical casesL19–19

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

  1. L19
    cases hsplit_1
09Establish hlower_2L20–21

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

  1. L20
    have hlower_2 : Lt(1,n)Definitions: Lt(1,n)Original native command in the exact edition
  2. L21
    exact hsplit_1_left
10Establish hsplit_2L22–25

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

  1. L22
    have hsplit_2 : Lt(2,n) ∨ Lt(n,3)Definitions: Lt(2,n)Lt(n,3)Original native command in the exact edition
  2. L23
    specialize le_or_lt (3)
  3. L24
    specialize le_or_lt n
  4. L25
    exact le_or_lt
11Separate the logical casesL26–26

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

  1. L26
    cases hsplit_2
12Establish hlower_3L27–28

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

  1. L27
    have hlower_3 : Lt(2,n)Definitions: Lt(2,n)Original native command in the exact edition
  2. L28
    exact hsplit_2_left
13Establish hsplit_3L29–32

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

  1. L29
    have hsplit_3 : Lt(4,n) ∨ Lt(n,5)Definitions: Lt(4,n)Lt(n,5)Original native command in the exact edition
  2. L30
    specialize le_or_lt (5)
  3. L31
    specialize le_or_lt n
  4. L32
    exact le_or_lt
14Separate the logical casesL33–33

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

  1. L33
    cases hsplit_3
15Establish hlower_4L34–35

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

  1. L34
    have hlower_4 : Lt(4,n)Definitions: Lt(4,n)Original native command in the exact edition
  2. L35
    exact hsplit_3_left
16Establish hsplit_4L36–39

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

  1. L36
    have hsplit_4 : Lt(6,n) ∨ Lt(n,7)Definitions: Lt(6,n)Lt(n,7)Original native command in the exact edition
  2. L37
    specialize le_or_lt (7)
  3. L38
    specialize le_or_lt n
  4. L39
    exact le_or_lt
17Separate the logical casesL40–40

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

  1. L40
    cases hsplit_4
18Establish hlower_5L41–42

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

  1. L41
    have hlower_5 : Lt(6,n)Definitions: Lt(6,n)Original native command in the exact edition
  2. L42
    exact hsplit_4_left
19Establish hsplit_5L43–46

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

  1. L43
    have hsplit_5 : Lt(12,n) ∨ Lt(n,13)Definitions: Lt(12,n)Lt(n,13)Original native command in the exact edition
  2. L44
    specialize le_or_lt (13)
  3. L45
    specialize le_or_lt n
  4. L46
    exact le_or_lt
20Separate the logical casesL47–47

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

  1. L47
    cases hsplit_5
21Establish hlower_6L48–49

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

  1. L48
    have hlower_6 : Lt(12,n)Definitions: Lt(12,n)Original native command in the exact edition
  2. L49
    exact hsplit_5_left
22Establish hsplit_6L50–53

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

  1. L50
    have hsplit_6 : Lt(22,n) ∨ Lt(n,23)Definitions: Lt(22,n)Lt(n,23)Original native command in the exact edition
  2. L51
    specialize le_or_lt (23)
  3. L52
    specialize le_or_lt n
  4. L53
    exact le_or_lt
23Separate the logical casesL54–54

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

  1. L54
    cases hsplit_6
24Establish hlower_7L55–56

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

  1. L55
    have hlower_7 : Lt(22,n)Definitions: Lt(22,n)Original native command in the exact edition
  2. L56
    exact hsplit_6_left
25Establish hsplit_7L57–60

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

  1. L57
    have hsplit_7 : Lt(42,n) ∨ Lt(n,43)Definitions: Lt(42,n)Lt(n,43)Original native command in the exact edition
  2. L58
    specialize le_or_lt (43)
  3. L59
    specialize le_or_lt n
  4. L60
    exact le_or_lt
26Separate the logical casesL61–61

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

  1. L61
    cases hsplit_7
27Establish hlower_8L62–63

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

  1. L62
    have hlower_8 : Lt(42,n)Definitions: Lt(42,n)Original native command in the exact edition
  2. L63
    exact hsplit_7_left
28Establish hsplit_8L64–67

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

  1. L64
    have hsplit_8 : Le(9 · 9 + 2,n) ∨ Lt(n,9 · 9 + 2)Definitions: Le(9 · 9 + 2,n)Lt(n,9 · 9 + 2)Original native command in the exact edition
  2. L65
    specialize le_or_lt (9 * 9 + 2)
  3. L66
    specialize le_or_lt n
  4. L67
    exact le_or_lt
29Separate the logical casesL68–68

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

  1. L68
    cases hsplit_8
30Establish hlower_9L69–70

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

  1. L69
    have hlower_9 : Le(9 · 9 + 2,n)Definitions: Le(9 · 9 + 2,n)Original native command in the exact edition
  2. L70
    exact hsplit_8_left
31Establish hsplit_9L71–74

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

  1. L71
    have hsplit_9 : Le(13 · 12 + 7,n) ∨ Lt(n,13 · 12 + 7)Definitions: Le(13 · 12 + 7,n)Lt(n,13 · 12 + 7)Original native command in the exact edition
  2. L72
    specialize le_or_lt (13 * 12 + 7)
  3. L73
    specialize le_or_lt n
  4. L74
    exact le_or_lt
32Separate the logical casesL75–75

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

  1. L75
    cases hsplit_9
33Establish hlower_10L76–77

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

  1. L76
    have hlower_10 : Le(13 · 12 + 7,n)Definitions: Le(13 · 12 + 7,n)Original native command in the exact edition
  2. L77
    exact hsplit_9_left
34Establish hsplit_10L78–81

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

  1. L78
    have hsplit_10 : Le(18 · 17 + 11,n) ∨ Lt(n,18 · 17 + 11)Definitions: Le(18 · 17 + 11,n)Lt(n,18 · 17 + 11)Original native command in the exact edition
  2. L79
    specialize le_or_lt (18 * 17 + 11)
  3. L80
    specialize le_or_lt n
  4. L81
    exact le_or_lt
35Separate the logical casesL82–82

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

  1. L82
    cases hsplit_10
36Establish hlower_11L83–84

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

  1. L83
    have hlower_11 : Le(18 · 17 + 11,n)Definitions: Le(18 · 17 + 11,n)Original native command in the exact edition
  2. L84
    exact hsplit_10_left
37Establish hfinal_strictL85–94

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

  1. L85
    have hfinal_strict : Lt(n,2 · (11 · 22) + 37)Definitions: Lt(n,2 · (11 · 22) + 37)Original native command in the exact edition
  2. L86
    specialize lt_trans n
  3. L87
    specialize lt_trans (16 * 32)
  4. L88
    specialize lt_trans (2 * (11 * 22) + 37)
  5. L89
    apply lt_trans
  6. L90
    exact hcutoff
  7. L91
    exact bertrand_cutoff_lt_final_prime
  8. L92
    specialize bertrand_covering_interval (18 * 17 + 11)
  9. L93
    specialize bertrand_covering_interval (2 * (11 * 22) + 37)
  10. L94
    specialize bertrand_covering_interval n
38Use earlier factsL95–104

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

  1. L95
    apply bertrand_covering_interval
  2. L96
    exact prime_five_hundred_twenty_one
  3. L97
    exact hlower_11
  4. L98
    exact hfinal_strict
  5. L99
    exact bertrand_cover_three_hundred_seventeen_five_hundred_twenty_one
  6. L100
    specialize bertrand_covering_interval (13 * 12 + 7)
  7. L101
    specialize bertrand_covering_interval (18 * 17 + 11)
  8. L102
    specialize bertrand_covering_interval n
  9. L103
    apply bertrand_covering_interval
  10. L104
    exact prime_three_hundred_seventeen
39Use earlier factsL105–114

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

  1. L105
    exact hlower_10
  2. L106
    exact hsplit_10_right
  3. L107
    exact bertrand_cover_one_hundred_sixty_three_three_hundred_seventeen
  4. L108
    specialize bertrand_covering_interval (9 * 9 + 2)
  5. L109
    specialize bertrand_covering_interval (13 * 12 + 7)
  6. L110
    specialize bertrand_covering_interval n
  7. L111
    apply bertrand_covering_interval
  8. L112
    exact prime_one_hundred_sixty_three
  9. L113
    exact hlower_9
  10. L114
    exact hsplit_9_right
40Use earlier factsL115–124

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

  1. L115
    exact bertrand_cover_eighty_three_one_hundred_sixty_three
  2. L116
    specialize bertrand_covering_interval (43)
  3. L117
    specialize bertrand_covering_interval (9 * 9 + 2)
  4. L118
    specialize bertrand_covering_interval n
  5. L119
    apply bertrand_covering_interval
  6. L120
    exact prime_eighty_three
  7. L121
    exact hlower_8
  8. L122
    exact hsplit_8_right
  9. L123
    exact bertrand_cover_forty_three_eighty_three
  10. L124
    specialize bertrand_covering_interval (23)
41Use earlier factsL125–134

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

  1. L125
    specialize bertrand_covering_interval (43)
  2. L126
    specialize bertrand_covering_interval n
  3. L127
    apply bertrand_covering_interval
  4. L128
    exact prime_forty_three
  5. L129
    exact hlower_7
  6. L130
    exact hsplit_7_right
  7. L131
    exact bertrand_cover_twenty_three_forty_three
  8. L132
    specialize bertrand_covering_interval (13)
  9. L133
    specialize bertrand_covering_interval (23)
  10. L134
    specialize bertrand_covering_interval n
42Use earlier factsL135–144

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

  1. L135
    apply bertrand_covering_interval
  2. L136
    exact prime_twenty_three
  3. L137
    exact hlower_6
  4. L138
    exact hsplit_6_right
  5. L139
    exact bertrand_cover_thirteen_twenty_three
  6. L140
    specialize bertrand_covering_interval (7)
  7. L141
    specialize bertrand_covering_interval (13)
  8. L142
    specialize bertrand_covering_interval n
  9. L143
    apply bertrand_covering_interval
  10. L144
    exact prime_thirteen
43Use earlier factsL145–154

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

  1. L145
    exact hlower_5
  2. L146
    exact hsplit_5_right
  3. L147
    exact bertrand_cover_seven_thirteen
  4. L148
    specialize bertrand_covering_interval (5)
  5. L149
    specialize bertrand_covering_interval (7)
  6. L150
    specialize bertrand_covering_interval n
  7. L151
    apply bertrand_covering_interval
  8. L152
    exact prime_seven
  9. L153
    exact hlower_4
  10. L154
    exact hsplit_4_right
44Use earlier factsL155–164

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

  1. L155
    exact bertrand_cover_five_seven
  2. L156
    specialize bertrand_covering_interval (3)
  3. L157
    specialize bertrand_covering_interval (5)
  4. L158
    specialize bertrand_covering_interval n
  5. L159
    apply bertrand_covering_interval
  6. L160
    exact prime_five
  7. L161
    exact hlower_3
  8. L162
    exact hsplit_3_right
  9. L163
    exact bertrand_cover_three_five
  10. L164
    specialize bertrand_covering_interval (2)
45Use earlier factsL165–174

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

  1. L165
    specialize bertrand_covering_interval (3)
  2. L166
    specialize bertrand_covering_interval n
  3. L167
    apply bertrand_covering_interval
  4. L168
    exact prime_three
  5. L169
    exact hlower_2
  6. L170
    exact hsplit_2_right
  7. L171
    exact bertrand_cover_two_three
  8. L172
    specialize bertrand_covering_interval (1)
  9. L173
    specialize bertrand_covering_interval (2)
  10. L174
    specialize bertrand_covering_interval n
46Use earlier factsL175–179

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

  1. L175
    apply bertrand_covering_interval
  2. L176
    exact prime_two
  3. L177
    exact hlower_1
  4. L178
    exact hsplit_1_right
  5. L179
    exact bertrand_cover_one_two

Library-wide reading audit

Original defined command ledger · 179 lines
  1. 0001intro n
  2. 0002intro hnonzero
  3. 0003intro hcutoff
  4. 0004have hshape : exists k. n = S k
  5. 0005specialize nonzero_is_succ n
  6. 0006apply nonzero_is_succ
  7. 0007exact hnonzero
  8. 0008cases hshape
  9. 0009have hlower_1 : Lt(0,n)
    Exact native replay linehave hlower_1 : exists k. k + 1 = n
  10. 0010exists x
  11. 0011rewrite hshape_witness
  12. 0012rewrite PA4
  13. 0013rewrite PA3
  14. 0014refl
  15. 0015have hsplit_1 : Lt(1,n) ∨ Lt(n,2)
    Exact native replay linehave hsplit_1 : (exists k. k + (2) = n) \/ (exists k. k + S n = (2))
  16. 0016specialize le_or_lt (2)
  17. 0017specialize le_or_lt n
  18. 0018exact le_or_lt
  19. 0019cases hsplit_1
  20. 0020have hlower_2 : Lt(1,n)
    Exact native replay linehave hlower_2 : exists k. k + (2) = n
  21. 0021exact hsplit_1_left
  22. 0022have hsplit_2 : Lt(2,n) ∨ Lt(n,3)
    Exact native replay linehave hsplit_2 : (exists k. k + (3) = n) \/ (exists k. k + S n = (3))
  23. 0023specialize le_or_lt (3)
  24. 0024specialize le_or_lt n
  25. 0025exact le_or_lt
  26. 0026cases hsplit_2
  27. 0027have hlower_3 : Lt(2,n)
    Exact native replay linehave hlower_3 : exists k. k + (3) = n
  28. 0028exact hsplit_2_left
  29. 0029have hsplit_3 : Lt(4,n) ∨ Lt(n,5)
    Exact native replay linehave hsplit_3 : (exists k. k + (5) = n) \/ (exists k. k + S n = (5))
  30. 0030specialize le_or_lt (5)
  31. 0031specialize le_or_lt n
  32. 0032exact le_or_lt
  33. 0033cases hsplit_3
  34. 0034have hlower_4 : Lt(4,n)
    Exact native replay linehave hlower_4 : exists k. k + (5) = n
  35. 0035exact hsplit_3_left
  36. 0036have hsplit_4 : Lt(6,n) ∨ Lt(n,7)
    Exact native replay linehave hsplit_4 : (exists k. k + (7) = n) \/ (exists k. k + S n = (7))
  37. 0037specialize le_or_lt (7)
  38. 0038specialize le_or_lt n
  39. 0039exact le_or_lt
  40. 0040cases hsplit_4
  41. 0041have hlower_5 : Lt(6,n)
    Exact native replay linehave hlower_5 : exists k. k + (7) = n
  42. 0042exact hsplit_4_left
  43. 0043have hsplit_5 : Lt(12,n) ∨ Lt(n,13)
    Exact native replay linehave hsplit_5 : (exists k. k + (13) = n) \/ (exists k. k + S n = (13))
  44. 0044specialize le_or_lt (13)
  45. 0045specialize le_or_lt n
  46. 0046exact le_or_lt
  47. 0047cases hsplit_5
  48. 0048have hlower_6 : Lt(12,n)
    Exact native replay linehave hlower_6 : exists k. k + (13) = n
  49. 0049exact hsplit_5_left
  50. 0050have hsplit_6 : Lt(22,n) ∨ Lt(n,23)
    Exact native replay linehave hsplit_6 : (exists k. k + (23) = n) \/ (exists k. k + S n = (23))
  51. 0051specialize le_or_lt (23)
  52. 0052specialize le_or_lt n
  53. 0053exact le_or_lt
  54. 0054cases hsplit_6
  55. 0055have hlower_7 : Lt(22,n)
    Exact native replay linehave hlower_7 : exists k. k + (23) = n
  56. 0056exact hsplit_6_left
  57. 0057have hsplit_7 : Lt(42,n) ∨ Lt(n,43)
    Exact native replay linehave hsplit_7 : (exists k. k + (43) = n) \/ (exists k. k + S n = (43))
  58. 0058specialize le_or_lt (43)
  59. 0059specialize le_or_lt n
  60. 0060exact le_or_lt
  61. 0061cases hsplit_7
  62. 0062have hlower_8 : Lt(42,n)
    Exact native replay linehave hlower_8 : exists k. k + (43) = n
  63. 0063exact hsplit_7_left
  64. 0064have hsplit_8 : Le(9 · 9 + 2,n) ∨ Lt(n,9 · 9 + 2)
    Exact native replay linehave hsplit_8 : (exists k. k + (9 * 9 + 2) = n) \/ (exists k. k + S n = (9 * 9 + 2))
  65. 0065specialize le_or_lt (9 * 9 + 2)
  66. 0066specialize le_or_lt n
  67. 0067exact le_or_lt
  68. 0068cases hsplit_8
  69. 0069have hlower_9 : Le(9 · 9 + 2,n)
    Exact native replay linehave hlower_9 : exists k. k + (9 * 9 + 2) = n
  70. 0070exact hsplit_8_left
  71. 0071have hsplit_9 : Le(13 · 12 + 7,n) ∨ Lt(n,13 · 12 + 7)
    Exact native replay linehave hsplit_9 : (exists k. k + (13 * 12 + 7) = n) \/ (exists k. k + S n = (13 * 12 + 7))
  72. 0072specialize le_or_lt (13 * 12 + 7)
  73. 0073specialize le_or_lt n
  74. 0074exact le_or_lt
  75. 0075cases hsplit_9
  76. 0076have hlower_10 : Le(13 · 12 + 7,n)
    Exact native replay linehave hlower_10 : exists k. k + (13 * 12 + 7) = n
  77. 0077exact hsplit_9_left
  78. 0078have hsplit_10 : Le(18 · 17 + 11,n) ∨ Lt(n,18 · 17 + 11)
    Exact native replay linehave hsplit_10 : (exists k. k + (18 * 17 + 11) = n) \/ (exists k. k + S n = (18 * 17 + 11))
  79. 0079specialize le_or_lt (18 * 17 + 11)
  80. 0080specialize le_or_lt n
  81. 0081exact le_or_lt
  82. 0082cases hsplit_10
  83. 0083have hlower_11 : Le(18 · 17 + 11,n)
    Exact native replay linehave hlower_11 : exists k. k + (18 * 17 + 11) = n
  84. 0084exact hsplit_10_left
  85. 0085have hfinal_strict : Lt(n,2 · (11 · 22) + 37)
    Exact native replay linehave hfinal_strict : exists k. k + S n = (2 * (11 * 22) + 37)
  86. 0086specialize lt_trans n
  87. 0087specialize lt_trans (16 * 32)
  88. 0088specialize lt_trans (2 * (11 * 22) + 37)
  89. 0089apply lt_trans
  90. 0090exact hcutoff
  91. 0091exact bertrand_cutoff_lt_final_prime
  92. 0092specialize bertrand_covering_interval (18 * 17 + 11)
  93. 0093specialize bertrand_covering_interval (2 * (11 * 22) + 37)
  94. 0094specialize bertrand_covering_interval n
  95. 0095apply bertrand_covering_interval
  96. 0096exact prime_five_hundred_twenty_one
  97. 0097exact hlower_11
  98. 0098exact hfinal_strict
  99. 0099exact bertrand_cover_three_hundred_seventeen_five_hundred_twenty_one
  100. 0100specialize bertrand_covering_interval (13 * 12 + 7)
  101. 0101specialize bertrand_covering_interval (18 * 17 + 11)
  102. 0102specialize bertrand_covering_interval n
  103. 0103apply bertrand_covering_interval
  104. 0104exact prime_three_hundred_seventeen
  105. 0105exact hlower_10
  106. 0106exact hsplit_10_right
  107. 0107exact bertrand_cover_one_hundred_sixty_three_three_hundred_seventeen
  108. 0108specialize bertrand_covering_interval (9 * 9 + 2)
  109. 0109specialize bertrand_covering_interval (13 * 12 + 7)
  110. 0110specialize bertrand_covering_interval n
  111. 0111apply bertrand_covering_interval
  112. 0112exact prime_one_hundred_sixty_three
  113. 0113exact hlower_9
  114. 0114exact hsplit_9_right
  115. 0115exact bertrand_cover_eighty_three_one_hundred_sixty_three
  116. 0116specialize bertrand_covering_interval (43)
  117. 0117specialize bertrand_covering_interval (9 * 9 + 2)
  118. 0118specialize bertrand_covering_interval n
  119. 0119apply bertrand_covering_interval
  120. 0120exact prime_eighty_three
  121. 0121exact hlower_8
  122. 0122exact hsplit_8_right
  123. 0123exact bertrand_cover_forty_three_eighty_three
  124. 0124specialize bertrand_covering_interval (23)
  125. 0125specialize bertrand_covering_interval (43)
  126. 0126specialize bertrand_covering_interval n
  127. 0127apply bertrand_covering_interval
  128. 0128exact prime_forty_three
  129. 0129exact hlower_7
  130. 0130exact hsplit_7_right
  131. 0131exact bertrand_cover_twenty_three_forty_three
  132. 0132specialize bertrand_covering_interval (13)
  133. 0133specialize bertrand_covering_interval (23)
  134. 0134specialize bertrand_covering_interval n
  135. 0135apply bertrand_covering_interval
  136. 0136exact prime_twenty_three
  137. 0137exact hlower_6
  138. 0138exact hsplit_6_right
  139. 0139exact bertrand_cover_thirteen_twenty_three
  140. 0140specialize bertrand_covering_interval (7)
  141. 0141specialize bertrand_covering_interval (13)
  142. 0142specialize bertrand_covering_interval n
  143. 0143apply bertrand_covering_interval
  144. 0144exact prime_thirteen
  145. 0145exact hlower_5
  146. 0146exact hsplit_5_right
  147. 0147exact bertrand_cover_seven_thirteen
  148. 0148specialize bertrand_covering_interval (5)
  149. 0149specialize bertrand_covering_interval (7)
  150. 0150specialize bertrand_covering_interval n
  151. 0151apply bertrand_covering_interval
  152. 0152exact prime_seven
  153. 0153exact hlower_4
  154. 0154exact hsplit_4_right
  155. 0155exact bertrand_cover_five_seven
  156. 0156specialize bertrand_covering_interval (3)
  157. 0157specialize bertrand_covering_interval (5)
  158. 0158specialize bertrand_covering_interval n
  159. 0159apply bertrand_covering_interval
  160. 0160exact prime_five
  161. 0161exact hlower_3
  162. 0162exact hsplit_3_right
  163. 0163exact bertrand_cover_three_five
  164. 0164specialize bertrand_covering_interval (2)
  165. 0165specialize bertrand_covering_interval (3)
  166. 0166specialize bertrand_covering_interval n
  167. 0167apply bertrand_covering_interval
  168. 0168exact prime_three
  169. 0169exact hlower_2
  170. 0170exact hsplit_2_right
  171. 0171exact bertrand_cover_two_three
  172. 0172specialize bertrand_covering_interval (1)
  173. 0173specialize bertrand_covering_interval (2)
  174. 0174specialize bertrand_covering_interval n
  175. 0175apply bertrand_covering_interval
  176. 0176exact prime_two
  177. 0177exact hlower_1
  178. 0178exact hsplit_1_right
  179. 0179exact bertrand_cover_one_two