BT011L · Bertrand theorem

prime_one_hundred_sixty_three

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

A native checked trial-division certificate for 163.

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(13 · 12 + 7)

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

8 occurrences

Exact expanded native-PA statement
(~(13 * 12 + 7 = 1) /\ forall bpr_left_bb8cert_prime_one_hundred_sixty_three bpr_right_bb8cert_prime_one_hundred_sixty_three. 13 * 12 + 7 = bpr_left_bb8cert_prime_one_hundred_sixty_three * bpr_right_bb8cert_prime_one_hundred_sixty_three -> bpr_left_bb8cert_prime_one_hundred_sixty_three = 1 \/ bpr_right_bb8cert_prime_one_hundred_sixty_three = 1)

Proof neighborhood

Direct theorem prerequisites

BT000L add_eq_zero_right BT001J le_not_lt BT0003 add_assoc BT0002 add_comm 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

224 script commands · 96 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 (10)
add eq zero rightle not ltadd assocadd commscaled 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 : ~(13 * (12) + 7 = 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 : 7 = 0
  2. L4
    specialize add_eq_zero_right (13 * (12))
  3. L5
    specialize add_eq_zero_right 7
  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 : ~(13 * (12) + 7 = 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(6,1)Definitions: Lt(6,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 13 * (12)
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,7)Definitions: Lt(1,7)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 5
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 7
  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(13 · 12 + 7,13 · 13)Definitions: Lt(13 · 12 + 7,13 · 13)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 5
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 13 * 12 + 13
  2. L26
    rewrite <- PA4
  3. L27
    trans 13 * 12 + (5 + S 7)
  4. L28
    trans (5 + 13 * 12) + S 7
  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 (13 * 12 + 5) + S 7
  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–39

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

  1. L36
    congr
  2. L37
    refl
  3. L38
    norm_num
  4. L39
    symm
20Use earlier factsL40–46

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

  1. L40
    apply PA6
  2. L41
    specialize prime_of_no_small_prime_divisor_below_square 12
  3. L42
    specialize prime_of_no_small_prime_divisor_below_square (13 * 12 + 7)
  4. L43
    apply prime_of_no_small_prime_divisor_below_square
  5. L44
    exact hn0
  6. L45
    exact hn1
  7. L46
    exact hsquare
21Fix variables and assumptionsL47–50

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

  1. L47
    intro p
  2. L48
    intro hp
  3. L49
    intro hp_bound
  4. L50
    intro hdivides
22Establish hbound_22L51–51

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

  1. L51
    have hbound_22 : Lt(11,22)Definitions: Lt(11,22)Original native command in the exact edition
23Construct an explicit witnessL52–52

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

  1. L52
    exists 10
24Calculate and transport equalitiesL53–53

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

  1. L53
    norm_num
25Establish hp_22L54–60

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

  1. L54
  2. L55
    specialize le_trans p
  3. L56
    specialize le_trans 12
  4. L57
    specialize le_trans 22
  5. L58
    apply le_trans
  6. L59
    exact hp_bound
  7. L60
    exact hbound_22
26Establish hcasesL61–65

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

  1. L61
    have hcases : p = 2 \/ (p = 3 \/ (p = 5 \/ (p = 7 \/ (p = 11 \/ (p = 13 \/ (p = 17 \/ (p = 19)))))))
  2. L62
    specialize prime_le_twenty_two_cases p
  3. L63
    apply prime_le_twenty_two_cases
  4. L64
    exact hp
  5. L65
    exact hp_22
27Separate the logical casesL66–66

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

  1. L66
    cases hcases
28Calculate and transport equalitiesL67–67

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

  1. L67
    rewrite hcases_left at hdivides
29Establish hdivision_2L68–77

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

  1. L68
    have hdivision_2 : (13 * 12 + 7) = 2 * (13 * 6 + 3) + 1
  2. L69
    specialize scaled_remainder_lift 2
  3. L70
    specialize scaled_remainder_lift 12
  4. L71
    specialize scaled_remainder_lift 6
  5. L72
    specialize scaled_remainder_lift 0
  6. L73
    specialize scaled_remainder_lift 13
  7. L74
    specialize scaled_remainder_lift 7
  8. L75
    specialize scaled_remainder_lift 3
  9. L76
    specialize scaled_remainder_lift 1
  10. L77
    apply scaled_remainder_lift
30Calculate and transport equalitiesL78–79

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

  1. L78
    norm_num
  2. L79
    norm_num
31Use earlier factsL80–85

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

  1. L80
    specialize nonzero_remainder_not_multiple 2
  2. L81
    specialize nonzero_remainder_not_multiple (13 * 12 + 7)
  3. L82
    specialize nonzero_remainder_not_multiple (13 * 6 + 3)
  4. L83
    specialize nonzero_remainder_not_multiple 1
  5. L84
    apply nonzero_remainder_not_multiple
  6. L85
    exact hdivision_2
32Fix variables and assumptionsL86–86

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

  1. L86
    intro hrem_2_zero
33Use earlier factsL87–88

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

  1. L87
    apply PA1
  2. L88
    exact hrem_2_zero
34Construct an explicit witnessL89–89

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

  1. L89
    exists 0
35Calculate and transport equalitiesL90–90

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

  1. L90
    norm_num
36Use earlier factsL91–91

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

  1. L91
    exact hdivides
37Separate the logical casesL92–92

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

  1. L92
    cases hcases_right
38Calculate and transport equalitiesL93–93

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

  1. L93
    rewrite hcases_right_left at hdivides
39Establish hdivision_3L94–103

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

  1. L94
    have hdivision_3 : (13 * 12 + 7) = 3 * (13 * 4 + 2) + 1
  2. L95
    specialize scaled_remainder_lift 3
  3. L96
    specialize scaled_remainder_lift 12
  4. L97
    specialize scaled_remainder_lift 4
  5. L98
    specialize scaled_remainder_lift 0
  6. L99
    specialize scaled_remainder_lift 13
  7. L100
    specialize scaled_remainder_lift 7
  8. L101
    specialize scaled_remainder_lift 2
  9. L102
    specialize scaled_remainder_lift 1
  10. L103
    apply scaled_remainder_lift
40Calculate and transport equalitiesL104–105

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

  1. L104
    norm_num
  2. L105
    norm_num
41Use earlier factsL106–111

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

  1. L106
    specialize nonzero_remainder_not_multiple 3
  2. L107
    specialize nonzero_remainder_not_multiple (13 * 12 + 7)
  3. L108
    specialize nonzero_remainder_not_multiple (13 * 4 + 2)
  4. L109
    specialize nonzero_remainder_not_multiple 1
  5. L110
    apply nonzero_remainder_not_multiple
  6. L111
    exact hdivision_3
42Fix variables and assumptionsL112–112

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

  1. L112
    intro hrem_3_zero
43Use earlier factsL113–114

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

  1. L113
    apply PA1
  2. L114
    exact hrem_3_zero
44Construct an explicit witnessL115–115

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

  1. L115
    exists 1
45Calculate and transport equalitiesL116–116

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

  1. L116
    norm_num
46Use earlier factsL117–117

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

  1. L117
    exact hdivides
47Separate the logical casesL118–118

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

  1. L118
    cases hcases_right_right
48Calculate and transport equalitiesL119–119

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

  1. L119
    rewrite hcases_right_right_left at hdivides
49Establish hdivision_5L120–129

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

  1. L120
    have hdivision_5 : (13 * 12 + 7) = 5 * (13 * 2 + 6) + 3
  2. L121
    specialize scaled_remainder_lift 5
  3. L122
    specialize scaled_remainder_lift 12
  4. L123
    specialize scaled_remainder_lift 2
  5. L124
    specialize scaled_remainder_lift 2
  6. L125
    specialize scaled_remainder_lift 13
  7. L126
    specialize scaled_remainder_lift 7
  8. L127
    specialize scaled_remainder_lift 6
  9. L128
    specialize scaled_remainder_lift 3
  10. L129
    apply scaled_remainder_lift
50Calculate and transport equalitiesL130–131

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

  1. L130
    norm_num
  2. L131
    norm_num
51Use earlier factsL132–137

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

  1. L132
    specialize nonzero_remainder_not_multiple 5
  2. L133
    specialize nonzero_remainder_not_multiple (13 * 12 + 7)
  3. L134
    specialize nonzero_remainder_not_multiple (13 * 2 + 6)
  4. L135
    specialize nonzero_remainder_not_multiple 3
  5. L136
    apply nonzero_remainder_not_multiple
  6. L137
    exact hdivision_5
52Fix variables and assumptionsL138–138

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

  1. L138
    intro hrem_5_zero
53Use earlier factsL139–140

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

  1. L139
    apply PA1
  2. L140
    exact hrem_5_zero
54Construct an explicit witnessL141–141

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

  1. L141
    exists 1
55Calculate and transport equalitiesL142–142

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

  1. L142
    norm_num
56Use earlier factsL143–143

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

  1. L143
    exact hdivides
57Separate the logical casesL144–144

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

  1. L144
    cases hcases_right_right_right
58Calculate and transport equalitiesL145–145

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

  1. L145
    rewrite hcases_right_right_right_left at hdivides
59Establish hdivision_7L146–155

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

  1. L146
    have hdivision_7 : (13 * 12 + 7) = 7 * (13 * 1 + 10) + 2
  2. L147
    specialize scaled_remainder_lift 7
  3. L148
    specialize scaled_remainder_lift 12
  4. L149
    specialize scaled_remainder_lift 1
  5. L150
    specialize scaled_remainder_lift 5
  6. L151
    specialize scaled_remainder_lift 13
  7. L152
    specialize scaled_remainder_lift 7
  8. L153
    specialize scaled_remainder_lift 10
  9. L154
    specialize scaled_remainder_lift 2
  10. L155
    apply scaled_remainder_lift
60Calculate and transport equalitiesL156–157

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

  1. L156
    norm_num
  2. L157
    norm_num
61Use earlier factsL158–163

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

  1. L158
    specialize nonzero_remainder_not_multiple 7
  2. L159
    specialize nonzero_remainder_not_multiple (13 * 12 + 7)
  3. L160
    specialize nonzero_remainder_not_multiple (13 * 1 + 10)
  4. L161
    specialize nonzero_remainder_not_multiple 2
  5. L162
    apply nonzero_remainder_not_multiple
  6. L163
    exact hdivision_7
62Fix variables and assumptionsL164–164

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

  1. L164
    intro hrem_7_zero
63Use earlier factsL165–166

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

  1. L165
    apply PA1
  2. L166
    exact hrem_7_zero
64Construct an explicit witnessL167–167

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

  1. L167
    exists 4
65Calculate and transport equalitiesL168–168

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

  1. L168
    norm_num
66Use earlier factsL169–169

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

  1. L169
    exact hdivides
67Separate the logical casesL170–170

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

  1. L170
    cases hcases_right_right_right_right
68Calculate and transport equalitiesL171–171

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

  1. L171
    rewrite hcases_right_right_right_right_left at hdivides
69Establish hdivision_11L172–181

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

  1. L172
    have hdivision_11 : (13 * 12 + 7) = 11 * (13 * 1 + 1) + 9
  2. L173
    specialize scaled_remainder_lift 11
  3. L174
    specialize scaled_remainder_lift 12
  4. L175
    specialize scaled_remainder_lift 1
  5. L176
    specialize scaled_remainder_lift 1
  6. L177
    specialize scaled_remainder_lift 13
  7. L178
    specialize scaled_remainder_lift 7
  8. L179
    specialize scaled_remainder_lift 1
  9. L180
    specialize scaled_remainder_lift 9
  10. L181
    apply scaled_remainder_lift
70Calculate and transport equalitiesL182–183

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

  1. L182
    norm_num
  2. L183
    norm_num
71Use earlier factsL184–189

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

  1. L184
    specialize nonzero_remainder_not_multiple 11
  2. L185
    specialize nonzero_remainder_not_multiple (13 * 12 + 7)
  3. L186
    specialize nonzero_remainder_not_multiple (13 * 1 + 1)
  4. L187
    specialize nonzero_remainder_not_multiple 9
  5. L188
    apply nonzero_remainder_not_multiple
  6. L189
    exact hdivision_11
72Fix variables and assumptionsL190–190

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

  1. L190
    intro hrem_11_zero
73Use earlier factsL191–192

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

  1. L191
    apply PA1
  2. L192
    exact hrem_11_zero
74Construct an explicit witnessL193–193

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

  1. L193
    exists 1
75Calculate and transport equalitiesL194–194

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

  1. L194
    norm_num
76Use earlier factsL195–195

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

  1. L195
    exact hdivides
77Separate the logical casesL196–196

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

  1. L196
    cases hcases_right_right_right_right_right
78Establish htoo_large_13L197–197

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

  1. L197
    have htoo_large_13 : Lt(12,13)Definitions: Lt(12,13)Original native command in the exact edition
79Construct an explicit witnessL198–198

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

  1. L198
    exists 0
80Calculate and transport equalitiesL199–199

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

  1. L199
    norm_num
81Use earlier factsL200–203

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

  1. L200
    specialize lt_not_le 12
  2. L201
    specialize lt_not_le 13
  3. L202
    apply lt_not_le
  4. L203
    exact htoo_large_13
82Calculate and transport equalitiesL204–204

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

  1. L204
    rewrite hcases_right_right_right_right_right_left at hp_bound
83Use earlier factsL205–205

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

  1. L205
    exact hp_bound
84Separate the logical casesL206–206

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

  1. L206
    cases hcases_right_right_right_right_right_right
85Establish htoo_large_17L207–207

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

  1. L207
    have htoo_large_17 : Lt(12,17)Definitions: Lt(12,17)Original native command in the exact edition
86Construct an explicit witnessL208–208

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

  1. L208
    exists 4
87Calculate 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
88Use earlier factsL210–213

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

  1. L210
    specialize lt_not_le 12
  2. L211
    specialize lt_not_le 17
  3. L212
    apply lt_not_le
  4. L213
    exact htoo_large_17
89Calculate 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_left at hp_bound
90Use earlier factsL215–215

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

  1. L215
    exact hp_bound
91Establish htoo_large_19L216–216

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

  1. L216
    have htoo_large_19 : Lt(12,19)Definitions: Lt(12,19)Original native command in the exact edition
92Construct an explicit witnessL217–217

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

  1. L217
    exists 6
93Calculate and transport equalitiesL218–218

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

  1. L218
    norm_num
94Use earlier factsL219–222

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

  1. L219
    specialize lt_not_le 12
  2. L220
    specialize lt_not_le 19
  3. L221
    apply lt_not_le
  4. L222
    exact htoo_large_19
95Calculate and transport equalitiesL223–223

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

  1. L223
    rewrite hcases_right_right_right_right_right_right_right at hp_bound
96Use earlier factsL224–224

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

  1. L224
    exact hp_bound

Library-wide reading audit

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