BT011K · Bertrand theorem

prime_eighty_three

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

A native checked trial-division certificate for 83.

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

Prime(9 · 9 + 2)

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

PD0004 Prime

1 occurrences

In local proof propositions

PD0001 Le PD0002 Lt

9 occurrences

Exact expanded native-PA statement
(~(9 * 9 + 2 = 1) /\ forall bpr_left_bb8cert_prime_eighty_three bpr_right_bb8cert_prime_eighty_three. 9 * 9 + 2 = bpr_left_bb8cert_prime_eighty_three * bpr_right_bb8cert_prime_eighty_three -> bpr_left_bb8cert_prime_eighty_three = 1 \/ bpr_right_bb8cert_prime_eighty_three = 1)

Proof neighborhood

Direct theorem prerequisites

BT000L add_eq_zero_right BT001J le_not_lt BT0003 add_assoc BT0002 add_comm BT0005 mul_succ_left BT011C scaled_remainder_lift BT011B nonzero_remainder_not_multiple BT0119 prime_of_no_small_prime_divisor_below_square BT000F le_trans BT011A prime_le_twenty_two_cases BT001I lt_not_le

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

215 script commands · 99 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 (11)
add eq zero rightle not ltadd assocadd commmul succ leftscaled remainder liftnonzero remainder not multipleprime of no small prime divisor below squarele transprime le twenty two caseslt not le
01Establish hn0L1–2

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

  1. L1
    have hn0 : ~(9 * (9) + 2 = 0)
  2. L2
    intro hzero
02Establish htail_zeroL3–9

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

  1. L3
    have htail_zero : 2 = 0
  2. L4
    specialize add_eq_zero_right (9 * (9))
  3. L5
    specialize add_eq_zero_right 2
  4. L6
    apply add_eq_zero_right
  5. L7
    exact hzero
  6. L8
    apply PA1
  7. L9
    exact htail_zero
03Establish hn1L10–11

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

  1. L10
    have hn1 : ~(9 * (9) + 2 = 1)
  2. L11
    intro hone
04Establish htail_le_oneL12–12

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

  1. L12
    have htail_le_one : Lt(1,1)Definitions: Lt(1,1)Original native command in the exact edition
05Construct an explicit witnessL13–13

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

  1. L13
    exists 9 * (9)
06Use earlier factsL14–14

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

  1. L14
    exact hone
07Establish hone_lt_tailL15–15

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

  1. L15
    have hone_lt_tail : Lt(1,2)Definitions: Lt(1,2)Original native command in the exact edition
08Construct an explicit witnessL16–16

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

  1. L16
    exists 0
09Calculate and transport equalitiesL17–17

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

  1. L17
    norm_num
10Use earlier factsL18–22

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

  1. L18
    specialize le_not_lt 2
  2. L19
    specialize le_not_lt 1
  3. L20
    apply le_not_lt
  4. L21
    exact htail_le_one
  5. L22
    exact hone_lt_tail
11Establish hsquareL23–23

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

  1. L23
    have hsquare : Lt(9 · 9 + 2,10 · 10)Definitions: Lt(9 · 9 + 2,10 · 10)Original native command in the exact edition
12Construct an explicit witnessL24–24

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

  1. L24
    exists 16
13Calculate and transport equalitiesL25–29

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

  1. L25
    trans (9 * 9 + 9) + 10
  2. L26
    rewrite <- PA4
  3. L27
    trans 9 * 9 + (16 + S 2)
  4. L28
    trans (16 + 9 * 9) + S 2
  5. L29
    symm
14Use earlier factsL30–30

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

  1. L30
    apply add_assoc
15Calculate and transport equalitiesL31–32

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

  1. L31
    trans (9 * 9 + 16) + S 2
  2. L32
    congr
16Use earlier factsL33–33

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

  1. L33
    apply add_comm
17Calculate and transport equalitiesL34–34

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

  1. L34
    refl
18Use earlier factsL35–35

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

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

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

  1. L36
    trans 9 * 9 + (9 + 10)
  2. L37
    congr
  3. L38
    refl
  4. L39
    norm_num
  5. L40
    symm
20Use earlier factsL41–41

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

  1. L41
    apply add_assoc
21Calculate and transport equalitiesL42–43

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

  1. L42
    symm
  2. L43
    trans 10 * 9 + 10
22Use earlier factsL44–44

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

  1. L44
    apply PA6
23Calculate and transport equalitiesL45–45

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

  1. L45
    congr
24Use earlier factsL46–46

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

  1. L46
    apply mul_succ_left
25Calculate and transport equalitiesL47–47

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

  1. L47
    refl
26Use earlier factsL48–53

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

  1. L48
    specialize prime_of_no_small_prime_divisor_below_square 9
  2. L49
    specialize prime_of_no_small_prime_divisor_below_square (9 * 9 + 2)
  3. L50
    apply prime_of_no_small_prime_divisor_below_square
  4. L51
    exact hn0
  5. L52
    exact hn1
  6. L53
    exact hsquare
27Fix variables and assumptionsL54–57

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

  1. L54
    intro p
  2. L55
    intro hp
  3. L56
    intro hp_bound
  4. L57
    intro hdivides
28Establish hbound_22L58–58

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

  1. L58
    have hbound_22 : Lt(8,22)Definitions: Lt(8,22)Original native command in the exact edition
29Construct an explicit witnessL59–59

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

  1. L59
    exists 13
30Calculate and transport equalitiesL60–60

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

  1. L60
    norm_num
31Establish hp_22L61–67

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

  1. L61
  2. L62
    specialize le_trans p
  3. L63
    specialize le_trans 9
  4. L64
    specialize le_trans 22
  5. L65
    apply le_trans
  6. L66
    exact hp_bound
  7. L67
    exact hbound_22
32Establish hcasesL68–72

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

  1. L68
    have hcases : p = 2 \/ (p = 3 \/ (p = 5 \/ (p = 7 \/ (p = 11 \/ (p = 13 \/ (p = 17 \/ (p = 19)))))))
  2. L69
    specialize prime_le_twenty_two_cases p
  3. L70
    apply prime_le_twenty_two_cases
  4. L71
    exact hp
  5. L72
    exact hp_22
33Separate the logical casesL73–73

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

  1. L73
    cases hcases
34Calculate and transport equalitiesL74–74

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

  1. L74
    rewrite hcases_left at hdivides
35Establish hdivision_2L75–84

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

  1. L75
    have hdivision_2 : (9 * 9 + 2) = 2 * (9 * 4 + 5) + 1
  2. L76
    specialize scaled_remainder_lift 2
  3. L77
    specialize scaled_remainder_lift 9
  4. L78
    specialize scaled_remainder_lift 4
  5. L79
    specialize scaled_remainder_lift 1
  6. L80
    specialize scaled_remainder_lift 9
  7. L81
    specialize scaled_remainder_lift 2
  8. L82
    specialize scaled_remainder_lift 5
  9. L83
    specialize scaled_remainder_lift 1
  10. L84
    apply scaled_remainder_lift
36Calculate and transport equalitiesL85–86

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

  1. L85
    norm_num
  2. L86
    norm_num
37Use earlier factsL87–92

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

  1. L87
    specialize nonzero_remainder_not_multiple 2
  2. L88
    specialize nonzero_remainder_not_multiple (9 * 9 + 2)
  3. L89
    specialize nonzero_remainder_not_multiple (9 * 4 + 5)
  4. L90
    specialize nonzero_remainder_not_multiple 1
  5. L91
    apply nonzero_remainder_not_multiple
  6. L92
    exact hdivision_2
38Fix variables and assumptionsL93–93

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

  1. L93
    intro hrem_2_zero
39Use earlier factsL94–95

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

  1. L94
    apply PA1
  2. L95
    exact hrem_2_zero
40Construct an explicit witnessL96–96

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

  1. L96
    exists 0
41Calculate and transport equalitiesL97–97

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

  1. L97
    norm_num
42Use earlier factsL98–98

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

  1. L98
    exact hdivides
43Separate the logical casesL99–99

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

  1. L99
    cases hcases_right
44Calculate and transport equalitiesL100–100

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

  1. L100
    rewrite hcases_right_left at hdivides
45Establish hdivision_3L101–110

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

  1. L101
    have hdivision_3 : (9 * 9 + 2) = 3 * (9 * 3 + 0) + 2
  2. L102
    specialize scaled_remainder_lift 3
  3. L103
    specialize scaled_remainder_lift 9
  4. L104
    specialize scaled_remainder_lift 3
  5. L105
    specialize scaled_remainder_lift 0
  6. L106
    specialize scaled_remainder_lift 9
  7. L107
    specialize scaled_remainder_lift 2
  8. L108
    specialize scaled_remainder_lift 0
  9. L109
    specialize scaled_remainder_lift 2
  10. L110
    apply scaled_remainder_lift
46Calculate and transport equalitiesL111–112

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

  1. L111
    norm_num
  2. L112
    norm_num
47Use earlier factsL113–118

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

  1. L113
    specialize nonzero_remainder_not_multiple 3
  2. L114
    specialize nonzero_remainder_not_multiple (9 * 9 + 2)
  3. L115
    specialize nonzero_remainder_not_multiple (9 * 3 + 0)
  4. L116
    specialize nonzero_remainder_not_multiple 2
  5. L117
    apply nonzero_remainder_not_multiple
  6. L118
    exact hdivision_3
48Fix variables and assumptionsL119–119

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

  1. L119
    intro hrem_3_zero
49Use earlier factsL120–121

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

  1. L120
    apply PA1
  2. L121
    exact hrem_3_zero
50Construct an explicit witnessL122–122

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

  1. L122
    exists 0
51Calculate and transport equalitiesL123–123

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

  1. L123
    norm_num
52Use earlier factsL124–124

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

  1. L124
    exact hdivides
53Separate the logical casesL125–125

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

  1. L125
    cases hcases_right_right
54Calculate and transport equalitiesL126–126

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

  1. L126
    rewrite hcases_right_right_left at hdivides
55Establish hdivision_5L127–136

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

  1. L127
    have hdivision_5 : (9 * 9 + 2) = 5 * (9 * 1 + 7) + 3
  2. L128
    specialize scaled_remainder_lift 5
  3. L129
    specialize scaled_remainder_lift 9
  4. L130
    specialize scaled_remainder_lift 1
  5. L131
    specialize scaled_remainder_lift 4
  6. L132
    specialize scaled_remainder_lift 9
  7. L133
    specialize scaled_remainder_lift 2
  8. L134
    specialize scaled_remainder_lift 7
  9. L135
    specialize scaled_remainder_lift 3
  10. L136
    apply scaled_remainder_lift
56Calculate and transport equalitiesL137–138

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

  1. L137
    norm_num
  2. L138
    norm_num
57Use earlier factsL139–144

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

  1. L139
    specialize nonzero_remainder_not_multiple 5
  2. L140
    specialize nonzero_remainder_not_multiple (9 * 9 + 2)
  3. L141
    specialize nonzero_remainder_not_multiple (9 * 1 + 7)
  4. L142
    specialize nonzero_remainder_not_multiple 3
  5. L143
    apply nonzero_remainder_not_multiple
  6. L144
    exact hdivision_5
58Fix variables and assumptionsL145–145

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

  1. L145
    intro hrem_5_zero
59Use earlier factsL146–147

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

  1. L146
    apply PA1
  2. L147
    exact hrem_5_zero
60Construct an explicit witnessL148–148

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

  1. L148
    exists 1
61Calculate and transport equalitiesL149–149

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

  1. L149
    norm_num
62Use earlier factsL150–150

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

  1. L150
    exact hdivides
63Separate the logical casesL151–151

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

  1. L151
    cases hcases_right_right_right
64Calculate and transport equalitiesL152–152

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

  1. L152
    rewrite hcases_right_right_right_left at hdivides
65Establish hdivision_7L153–162

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

  1. L153
    have hdivision_7 : (9 * 9 + 2) = 7 * (9 * 1 + 2) + 6
  2. L154
    specialize scaled_remainder_lift 7
  3. L155
    specialize scaled_remainder_lift 9
  4. L156
    specialize scaled_remainder_lift 1
  5. L157
    specialize scaled_remainder_lift 2
  6. L158
    specialize scaled_remainder_lift 9
  7. L159
    specialize scaled_remainder_lift 2
  8. L160
    specialize scaled_remainder_lift 2
  9. L161
    specialize scaled_remainder_lift 6
  10. L162
    apply scaled_remainder_lift
66Calculate and transport equalitiesL163–164

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

  1. L163
    norm_num
  2. L164
    norm_num
67Use earlier factsL165–170

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

  1. L165
    specialize nonzero_remainder_not_multiple 7
  2. L166
    specialize nonzero_remainder_not_multiple (9 * 9 + 2)
  3. L167
    specialize nonzero_remainder_not_multiple (9 * 1 + 2)
  4. L168
    specialize nonzero_remainder_not_multiple 6
  5. L169
    apply nonzero_remainder_not_multiple
  6. L170
    exact hdivision_7
68Fix variables and assumptionsL171–171

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

  1. L171
    intro hrem_7_zero
69Use earlier factsL172–173

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

  1. L172
    apply PA1
  2. L173
    exact hrem_7_zero
70Construct an explicit witnessL174–174

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

  1. L174
    exists 0
71Calculate and transport equalitiesL175–175

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

  1. L175
    norm_num
72Use earlier factsL176–176

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

  1. L176
    exact hdivides
73Separate the logical casesL177–177

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

  1. L177
    cases hcases_right_right_right_right
74Establish htoo_large_11L178–178

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

  1. L178
    have htoo_large_11 : Lt(9,11)Definitions: Lt(9,11)Original native command in the exact edition
75Construct an explicit witnessL179–179

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

  1. L179
    exists 1
76Calculate and transport equalitiesL180–180

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

  1. L180
    norm_num
77Use earlier factsL181–184

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

  1. L181
    specialize lt_not_le 9
  2. L182
    specialize lt_not_le 11
  3. L183
    apply lt_not_le
  4. L184
    exact htoo_large_11
78Calculate and transport equalitiesL185–185

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

  1. L185
    rewrite hcases_right_right_right_right_left at hp_bound
79Use earlier factsL186–186

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

  1. L186
    exact hp_bound
80Separate the logical casesL187–187

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

  1. L187
    cases hcases_right_right_right_right_right
81Establish htoo_large_13L188–188

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

  1. L188
    have htoo_large_13 : Lt(9,13)Definitions: Lt(9,13)Original native command in the exact edition
82Construct an explicit witnessL189–189

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

  1. L189
    exists 3
83Calculate and transport equalitiesL190–190

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

  1. L190
    norm_num
84Use earlier factsL191–194

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

  1. L191
    specialize lt_not_le 9
  2. L192
    specialize lt_not_le 13
  3. L193
    apply lt_not_le
  4. L194
    exact htoo_large_13
85Calculate and transport equalitiesL195–195

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

  1. L195
    rewrite hcases_right_right_right_right_right_left at hp_bound
86Use earlier factsL196–196

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

  1. L196
    exact hp_bound
87Separate the logical casesL197–197

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

  1. L197
    cases hcases_right_right_right_right_right_right
88Establish htoo_large_17L198–198

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

  1. L198
    have htoo_large_17 : Lt(9,17)Definitions: Lt(9,17)Original native command in the exact edition
89Construct an explicit witnessL199–199

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

  1. L199
    exists 7
90Calculate and transport equalitiesL200–200

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

  1. L200
    norm_num
91Use earlier factsL201–204

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

  1. L201
    specialize lt_not_le 9
  2. L202
    specialize lt_not_le 17
  3. L203
    apply lt_not_le
  4. L204
    exact htoo_large_17
92Calculate and transport equalitiesL205–205

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

  1. L205
    rewrite hcases_right_right_right_right_right_right_left at hp_bound
93Use earlier factsL206–206

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

  1. L206
    exact hp_bound
94Establish htoo_large_19L207–207

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

  1. L207
    have htoo_large_19 : Lt(9,19)Definitions: Lt(9,19)Original native command in the exact edition
95Construct an explicit witnessL208–208

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

  1. L208
    exists 9
96Calculate and transport equalitiesL209–209

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

  1. L209
    norm_num
97Use earlier factsL210–213

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

  1. L210
    specialize lt_not_le 9
  2. L211
    specialize lt_not_le 19
  3. L212
    apply lt_not_le
  4. L213
    exact htoo_large_19
98Calculate and transport equalitiesL214–214

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

  1. L214
    rewrite hcases_right_right_right_right_right_right_right at hp_bound
99Use earlier factsL215–215

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

  1. L215
    exact hp_bound

Library-wide reading audit

Original defined command ledger · 215 lines
  1. 0001have hn0 : ~(9 * (9) + 2 = 0)
  2. 0002intro hzero
  3. 0003have htail_zero : 2 = 0
  4. 0004specialize add_eq_zero_right (9 * (9))
  5. 0005specialize add_eq_zero_right 2
  6. 0006apply add_eq_zero_right
  7. 0007exact hzero
  8. 0008apply PA1
  9. 0009exact htail_zero
  10. 0010have hn1 : ~(9 * (9) + 2 = 1)
  11. 0011intro hone
  12. 0012have htail_le_one : Lt(1,1)
    Exact native replay linehave htail_le_one : exists k. k + 2 = 1
  13. 0013exists 9 * (9)
  14. 0014exact hone
  15. 0015have hone_lt_tail : Lt(1,2)
    Exact native replay linehave hone_lt_tail : exists k. k + S 1 = 2
  16. 0016exists 0
  17. 0017norm_num
  18. 0018specialize le_not_lt 2
  19. 0019specialize le_not_lt 1
  20. 0020apply le_not_lt
  21. 0021exact htail_le_one
  22. 0022exact hone_lt_tail
  23. 0023have hsquare : Lt(9 · 9 + 2,10 · 10)
    Exact native replay linehave hsquare : exists bpr_gap_bb8cert_prime_eighty_three_square. bpr_gap_bb8cert_prime_eighty_three_square + S (9 * (9) + 2) = S 9 * S 9
  24. 0024exists 16
  25. 0025trans (9 * 9 + 9) + 10
  26. 0026rewrite <- PA4
  27. 0027trans 9 * 9 + (16 + S 2)
  28. 0028trans (16 + 9 * 9) + S 2
  29. 0029symm
  30. 0030apply add_assoc
  31. 0031trans (9 * 9 + 16) + S 2
  32. 0032congr
  33. 0033apply add_comm
  34. 0034refl
  35. 0035apply add_assoc
  36. 0036trans 9 * 9 + (9 + 10)
  37. 0037congr
  38. 0038refl
  39. 0039norm_num
  40. 0040symm
  41. 0041apply add_assoc
  42. 0042symm
  43. 0043trans 10 * 9 + 10
  44. 0044apply PA6
  45. 0045congr
  46. 0046apply mul_succ_left
  47. 0047refl
  48. 0048specialize prime_of_no_small_prime_divisor_below_square 9
  49. 0049specialize prime_of_no_small_prime_divisor_below_square (9 * 9 + 2)
  50. 0050apply prime_of_no_small_prime_divisor_below_square
  51. 0051exact hn0
  52. 0052exact hn1
  53. 0053exact hsquare
  54. 0054intro p
  55. 0055intro hp
  56. 0056intro hp_bound
  57. 0057intro hdivides
  58. 0058have hbound_22 : Lt(8,22)
    Exact native replay linehave hbound_22 : exists k. k + 9 = 22
  59. 0059exists 13
  60. 0060norm_num
  61. 0061have hp_22 : Le(p,22)
    Exact native replay linehave hp_22 : exists k. k + p = 22
  62. 0062specialize le_trans p
  63. 0063specialize le_trans 9
  64. 0064specialize le_trans 22
  65. 0065apply le_trans
  66. 0066exact hp_bound
  67. 0067exact hbound_22
  68. 0068have hcases : p = 2 \/ (p = 3 \/ (p = 5 \/ (p = 7 \/ (p = 11 \/ (p = 13 \/ (p = 17 \/ (p = 19)))))))
  69. 0069specialize prime_le_twenty_two_cases p
  70. 0070apply prime_le_twenty_two_cases
  71. 0071exact hp
  72. 0072exact hp_22
  73. 0073cases hcases
  74. 0074rewrite hcases_left at hdivides
  75. 0075have hdivision_2 : (9 * 9 + 2) = 2 * (9 * 4 + 5) + 1
  76. 0076specialize scaled_remainder_lift 2
  77. 0077specialize scaled_remainder_lift 9
  78. 0078specialize scaled_remainder_lift 4
  79. 0079specialize scaled_remainder_lift 1
  80. 0080specialize scaled_remainder_lift 9
  81. 0081specialize scaled_remainder_lift 2
  82. 0082specialize scaled_remainder_lift 5
  83. 0083specialize scaled_remainder_lift 1
  84. 0084apply scaled_remainder_lift
  85. 0085norm_num
  86. 0086norm_num
  87. 0087specialize nonzero_remainder_not_multiple 2
  88. 0088specialize nonzero_remainder_not_multiple (9 * 9 + 2)
  89. 0089specialize nonzero_remainder_not_multiple (9 * 4 + 5)
  90. 0090specialize nonzero_remainder_not_multiple 1
  91. 0091apply nonzero_remainder_not_multiple
  92. 0092exact hdivision_2
  93. 0093intro hrem_2_zero
  94. 0094apply PA1
  95. 0095exact hrem_2_zero
  96. 0096exists 0
  97. 0097norm_num
  98. 0098exact hdivides
  99. 0099cases hcases_right
  100. 0100rewrite hcases_right_left at hdivides
  101. 0101have hdivision_3 : (9 * 9 + 2) = 3 * (9 * 3 + 0) + 2
  102. 0102specialize scaled_remainder_lift 3
  103. 0103specialize scaled_remainder_lift 9
  104. 0104specialize scaled_remainder_lift 3
  105. 0105specialize scaled_remainder_lift 0
  106. 0106specialize scaled_remainder_lift 9
  107. 0107specialize scaled_remainder_lift 2
  108. 0108specialize scaled_remainder_lift 0
  109. 0109specialize scaled_remainder_lift 2
  110. 0110apply scaled_remainder_lift
  111. 0111norm_num
  112. 0112norm_num
  113. 0113specialize nonzero_remainder_not_multiple 3
  114. 0114specialize nonzero_remainder_not_multiple (9 * 9 + 2)
  115. 0115specialize nonzero_remainder_not_multiple (9 * 3 + 0)
  116. 0116specialize nonzero_remainder_not_multiple 2
  117. 0117apply nonzero_remainder_not_multiple
  118. 0118exact hdivision_3
  119. 0119intro hrem_3_zero
  120. 0120apply PA1
  121. 0121exact hrem_3_zero
  122. 0122exists 0
  123. 0123norm_num
  124. 0124exact hdivides
  125. 0125cases hcases_right_right
  126. 0126rewrite hcases_right_right_left at hdivides
  127. 0127have hdivision_5 : (9 * 9 + 2) = 5 * (9 * 1 + 7) + 3
  128. 0128specialize scaled_remainder_lift 5
  129. 0129specialize scaled_remainder_lift 9
  130. 0130specialize scaled_remainder_lift 1
  131. 0131specialize scaled_remainder_lift 4
  132. 0132specialize scaled_remainder_lift 9
  133. 0133specialize scaled_remainder_lift 2
  134. 0134specialize scaled_remainder_lift 7
  135. 0135specialize scaled_remainder_lift 3
  136. 0136apply scaled_remainder_lift
  137. 0137norm_num
  138. 0138norm_num
  139. 0139specialize nonzero_remainder_not_multiple 5
  140. 0140specialize nonzero_remainder_not_multiple (9 * 9 + 2)
  141. 0141specialize nonzero_remainder_not_multiple (9 * 1 + 7)
  142. 0142specialize nonzero_remainder_not_multiple 3
  143. 0143apply nonzero_remainder_not_multiple
  144. 0144exact hdivision_5
  145. 0145intro hrem_5_zero
  146. 0146apply PA1
  147. 0147exact hrem_5_zero
  148. 0148exists 1
  149. 0149norm_num
  150. 0150exact hdivides
  151. 0151cases hcases_right_right_right
  152. 0152rewrite hcases_right_right_right_left at hdivides
  153. 0153have hdivision_7 : (9 * 9 + 2) = 7 * (9 * 1 + 2) + 6
  154. 0154specialize scaled_remainder_lift 7
  155. 0155specialize scaled_remainder_lift 9
  156. 0156specialize scaled_remainder_lift 1
  157. 0157specialize scaled_remainder_lift 2
  158. 0158specialize scaled_remainder_lift 9
  159. 0159specialize scaled_remainder_lift 2
  160. 0160specialize scaled_remainder_lift 2
  161. 0161specialize scaled_remainder_lift 6
  162. 0162apply scaled_remainder_lift
  163. 0163norm_num
  164. 0164norm_num
  165. 0165specialize nonzero_remainder_not_multiple 7
  166. 0166specialize nonzero_remainder_not_multiple (9 * 9 + 2)
  167. 0167specialize nonzero_remainder_not_multiple (9 * 1 + 2)
  168. 0168specialize nonzero_remainder_not_multiple 6
  169. 0169apply nonzero_remainder_not_multiple
  170. 0170exact hdivision_7
  171. 0171intro hrem_7_zero
  172. 0172apply PA1
  173. 0173exact hrem_7_zero
  174. 0174exists 0
  175. 0175norm_num
  176. 0176exact hdivides
  177. 0177cases hcases_right_right_right_right
  178. 0178have htoo_large_11 : Lt(9,11)
    Exact native replay linehave htoo_large_11 : exists k. k + S 9 = 11
  179. 0179exists 1
  180. 0180norm_num
  181. 0181specialize lt_not_le 9
  182. 0182specialize lt_not_le 11
  183. 0183apply lt_not_le
  184. 0184exact htoo_large_11
  185. 0185rewrite hcases_right_right_right_right_left at hp_bound
  186. 0186exact hp_bound
  187. 0187cases hcases_right_right_right_right_right
  188. 0188have htoo_large_13 : Lt(9,13)
    Exact native replay linehave htoo_large_13 : exists k. k + S 9 = 13
  189. 0189exists 3
  190. 0190norm_num
  191. 0191specialize lt_not_le 9
  192. 0192specialize lt_not_le 13
  193. 0193apply lt_not_le
  194. 0194exact htoo_large_13
  195. 0195rewrite hcases_right_right_right_right_right_left at hp_bound
  196. 0196exact hp_bound
  197. 0197cases hcases_right_right_right_right_right_right
  198. 0198have htoo_large_17 : Lt(9,17)
    Exact native replay linehave htoo_large_17 : exists k. k + S 9 = 17
  199. 0199exists 7
  200. 0200norm_num
  201. 0201specialize lt_not_le 9
  202. 0202specialize lt_not_le 17
  203. 0203apply lt_not_le
  204. 0204exact htoo_large_17
  205. 0205rewrite hcases_right_right_right_right_right_right_left at hp_bound
  206. 0206exact hp_bound
  207. 0207have htoo_large_19 : Lt(9,19)
    Exact native replay linehave htoo_large_19 : exists k. k + S 9 = 19
  208. 0208exists 9
  209. 0209norm_num
  210. 0210specialize lt_not_le 9
  211. 0211specialize lt_not_le 19
  212. 0212apply lt_not_le
  213. 0213exact htoo_large_19
  214. 0214rewrite hcases_right_right_right_right_right_right_right at hp_bound
  215. 0215exact hp_bound