BT011M · Bertrand theorem

prime_three_hundred_seventeen

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

A native checked trial-division certificate for 317.

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(18 · 17 + 11)

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0004 Prime

1 occurrences

In local proof propositions

PD0001 Le PD0002 Lt

6 occurrences

Exact expanded native-PA statement
(~(18 * 17 + 11 = 1) /\ forall bpr_left_bb8cert_prime_three_hundred_seventeen bpr_right_bb8cert_prime_three_hundred_seventeen. 18 * 17 + 11 = bpr_left_bb8cert_prime_three_hundred_seventeen * bpr_right_bb8cert_prime_three_hundred_seventeen -> bpr_left_bb8cert_prime_three_hundred_seventeen = 1 \/ bpr_right_bb8cert_prime_three_hundred_seventeen = 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

256 script commands · 102 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 : ~(18 * (17) + 11 = 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 : 11 = 0
  2. L4
    specialize add_eq_zero_right (18 * (17))
  3. L5
    specialize add_eq_zero_right 11
  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 : ~(18 * (17) + 11 = 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(10,1)Definitions: Lt(10,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 18 * (17)
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,11)Definitions: Lt(1,11)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 9
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 11
  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(18 · 17 + 11,18 · 18)Definitions: Lt(18 · 17 + 11,18 · 18)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 6
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 18 * 17 + 18
  2. L26
    rewrite <- PA4
  3. L27
    trans 18 * 17 + (6 + S 11)
  4. L28
    trans (6 + 18 * 17) + S 11
  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 (18 * 17 + 6) + S 11
  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 17
  3. L42
    specialize prime_of_no_small_prime_divisor_below_square (18 * 17 + 11)
  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(16,22)Definitions: Lt(16,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 5
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 17
  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 : (18 * 17 + 11) = 2 * (18 * 8 + 14) + 1
  2. L69
    specialize scaled_remainder_lift 2
  3. L70
    specialize scaled_remainder_lift 17
  4. L71
    specialize scaled_remainder_lift 8
  5. L72
    specialize scaled_remainder_lift 1
  6. L73
    specialize scaled_remainder_lift 18
  7. L74
    specialize scaled_remainder_lift 11
  8. L75
    specialize scaled_remainder_lift 14
  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 (18 * 17 + 11)
  3. L82
    specialize nonzero_remainder_not_multiple (18 * 8 + 14)
  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 : (18 * 17 + 11) = 3 * (18 * 5 + 15) + 2
  2. L95
    specialize scaled_remainder_lift 3
  3. L96
    specialize scaled_remainder_lift 17
  4. L97
    specialize scaled_remainder_lift 5
  5. L98
    specialize scaled_remainder_lift 2
  6. L99
    specialize scaled_remainder_lift 18
  7. L100
    specialize scaled_remainder_lift 11
  8. L101
    specialize scaled_remainder_lift 15
  9. L102
    specialize scaled_remainder_lift 2
  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 (18 * 17 + 11)
  3. L108
    specialize nonzero_remainder_not_multiple (18 * 5 + 15)
  4. L109
    specialize nonzero_remainder_not_multiple 2
  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 0
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 : (18 * 17 + 11) = 5 * (18 * 3 + 9) + 2
  2. L121
    specialize scaled_remainder_lift 5
  3. L122
    specialize scaled_remainder_lift 17
  4. L123
    specialize scaled_remainder_lift 3
  5. L124
    specialize scaled_remainder_lift 2
  6. L125
    specialize scaled_remainder_lift 18
  7. L126
    specialize scaled_remainder_lift 11
  8. L127
    specialize scaled_remainder_lift 9
  9. L128
    specialize scaled_remainder_lift 2
  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 (18 * 17 + 11)
  3. L134
    specialize nonzero_remainder_not_multiple (18 * 3 + 9)
  4. L135
    specialize nonzero_remainder_not_multiple 2
  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 2
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 : (18 * 17 + 11) = 7 * (18 * 2 + 9) + 2
  2. L147
    specialize scaled_remainder_lift 7
  3. L148
    specialize scaled_remainder_lift 17
  4. L149
    specialize scaled_remainder_lift 2
  5. L150
    specialize scaled_remainder_lift 3
  6. L151
    specialize scaled_remainder_lift 18
  7. L152
    specialize scaled_remainder_lift 11
  8. L153
    specialize scaled_remainder_lift 9
  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 (18 * 17 + 11)
  3. L160
    specialize nonzero_remainder_not_multiple (18 * 2 + 9)
  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 : (18 * 17 + 11) = 11 * (18 * 1 + 10) + 9
  2. L173
    specialize scaled_remainder_lift 11
  3. L174
    specialize scaled_remainder_lift 17
  4. L175
    specialize scaled_remainder_lift 1
  5. L176
    specialize scaled_remainder_lift 6
  6. L177
    specialize scaled_remainder_lift 18
  7. L178
    specialize scaled_remainder_lift 11
  8. L179
    specialize scaled_remainder_lift 10
  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 (18 * 17 + 11)
  3. L186
    specialize nonzero_remainder_not_multiple (18 * 1 + 10)
  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
78Calculate and transport equalitiesL197–197

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

  1. L197
    rewrite hcases_right_right_right_right_right_left at hdivides
79Establish hdivision_13L198–207

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

  1. L198
    have hdivision_13 : (18 * 17 + 11) = 13 * (18 * 1 + 6) + 5
  2. L199
    specialize scaled_remainder_lift 13
  3. L200
    specialize scaled_remainder_lift 17
  4. L201
    specialize scaled_remainder_lift 1
  5. L202
    specialize scaled_remainder_lift 4
  6. L203
    specialize scaled_remainder_lift 18
  7. L204
    specialize scaled_remainder_lift 11
  8. L205
    specialize scaled_remainder_lift 6
  9. L206
    specialize scaled_remainder_lift 5
  10. L207
    apply scaled_remainder_lift
80Calculate and transport equalitiesL208–209

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

  1. L208
    norm_num
  2. L209
    norm_num
81Use earlier factsL210–215

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

  1. L210
    specialize nonzero_remainder_not_multiple 13
  2. L211
    specialize nonzero_remainder_not_multiple (18 * 17 + 11)
  3. L212
    specialize nonzero_remainder_not_multiple (18 * 1 + 6)
  4. L213
    specialize nonzero_remainder_not_multiple 5
  5. L214
    apply nonzero_remainder_not_multiple
  6. L215
    exact hdivision_13
82Fix variables and assumptionsL216–216

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

  1. L216
    intro hrem_13_zero
83Use earlier factsL217–218

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

  1. L217
    apply PA1
  2. L218
    exact hrem_13_zero
84Construct an explicit witnessL219–219

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

  1. L219
    exists 7
85Calculate and transport equalitiesL220–220

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

  1. L220
    norm_num
86Use earlier factsL221–221

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

  1. L221
    exact hdivides
87Separate the logical casesL222–222

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

  1. L222
    cases hcases_right_right_right_right_right_right
88Calculate 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_left at hdivides
89Establish hdivision_17L224–233

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

  1. L224
    have hdivision_17 : (18 * 17 + 11) = 17 * (18 * 1 + 0) + 11
  2. L225
    specialize scaled_remainder_lift 17
  3. L226
    specialize scaled_remainder_lift 17
  4. L227
    specialize scaled_remainder_lift 1
  5. L228
    specialize scaled_remainder_lift 0
  6. L229
    specialize scaled_remainder_lift 18
  7. L230
    specialize scaled_remainder_lift 11
  8. L231
    specialize scaled_remainder_lift 0
  9. L232
    specialize scaled_remainder_lift 11
  10. L233
    apply scaled_remainder_lift
90Calculate and transport equalitiesL234–235

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

  1. L234
    norm_num
  2. L235
    norm_num
91Use earlier factsL236–241

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

  1. L236
    specialize nonzero_remainder_not_multiple 17
  2. L237
    specialize nonzero_remainder_not_multiple (18 * 17 + 11)
  3. L238
    specialize nonzero_remainder_not_multiple (18 * 1 + 0)
  4. L239
    specialize nonzero_remainder_not_multiple 11
  5. L240
    apply nonzero_remainder_not_multiple
  6. L241
    exact hdivision_17
92Fix variables and assumptionsL242–242

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

  1. L242
    intro hrem_17_zero
93Use earlier factsL243–244

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

  1. L243
    apply PA1
  2. L244
    exact hrem_17_zero
94Construct an explicit witnessL245–245

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

  1. L245
    exists 5
95Calculate and transport equalitiesL246–246

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

  1. L246
    norm_num
96Use earlier factsL247–247

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

  1. L247
    exact hdivides
97Establish htoo_large_19L248–248

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

  1. L248
    have htoo_large_19 : Lt(17,19)Definitions: Lt(17,19)Original native command in the exact edition
98Construct an explicit witnessL249–249

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

  1. L249
    exists 1
99Calculate and transport equalitiesL250–250

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

  1. L250
    norm_num
100Use earlier factsL251–254

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

  1. L251
    specialize lt_not_le 17
  2. L252
    specialize lt_not_le 19
  3. L253
    apply lt_not_le
  4. L254
    exact htoo_large_19
101Calculate and transport equalitiesL255–255

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

  1. L255
    rewrite hcases_right_right_right_right_right_right_right at hp_bound
102Use earlier factsL256–256

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

  1. L256
    exact hp_bound

Library-wide reading audit

Original defined command ledger · 256 lines
  1. 0001have hn0 : ~(18 * (17) + 11 = 0)
  2. 0002intro hzero
  3. 0003have htail_zero : 11 = 0
  4. 0004specialize add_eq_zero_right (18 * (17))
  5. 0005specialize add_eq_zero_right 11
  6. 0006apply add_eq_zero_right
  7. 0007exact hzero
  8. 0008apply PA1
  9. 0009exact htail_zero
  10. 0010have hn1 : ~(18 * (17) + 11 = 1)
  11. 0011intro hone
  12. 0012have htail_le_one : Lt(10,1)
    Exact native replay linehave htail_le_one : exists k. k + 11 = 1
  13. 0013exists 18 * (17)
  14. 0014exact hone
  15. 0015have hone_lt_tail : Lt(1,11)
    Exact native replay linehave hone_lt_tail : exists k. k + S 1 = 11
  16. 0016exists 9
  17. 0017norm_num
  18. 0018specialize le_not_lt 11
  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(18 · 17 + 11,18 · 18)
    Exact native replay linehave hsquare : exists bpr_gap_bb8cert_prime_three_hundred_seventeen_square. bpr_gap_bb8cert_prime_three_hundred_seventeen_square + S (18 * (17) + 11) = S 17 * S 17
  24. 0024exists 6
  25. 0025trans 18 * 17 + 18
  26. 0026rewrite <- PA4
  27. 0027trans 18 * 17 + (6 + S 11)
  28. 0028trans (6 + 18 * 17) + S 11
  29. 0029symm
  30. 0030apply add_assoc
  31. 0031trans (18 * 17 + 6) + S 11
  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 17
  42. 0042specialize prime_of_no_small_prime_divisor_below_square (18 * 17 + 11)
  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(16,22)
    Exact native replay linehave hbound_22 : exists k. k + 17 = 22
  52. 0052exists 5
  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 17
  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 : (18 * 17 + 11) = 2 * (18 * 8 + 14) + 1
  69. 0069specialize scaled_remainder_lift 2
  70. 0070specialize scaled_remainder_lift 17
  71. 0071specialize scaled_remainder_lift 8
  72. 0072specialize scaled_remainder_lift 1
  73. 0073specialize scaled_remainder_lift 18
  74. 0074specialize scaled_remainder_lift 11
  75. 0075specialize scaled_remainder_lift 14
  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 (18 * 17 + 11)
  82. 0082specialize nonzero_remainder_not_multiple (18 * 8 + 14)
  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 : (18 * 17 + 11) = 3 * (18 * 5 + 15) + 2
  95. 0095specialize scaled_remainder_lift 3
  96. 0096specialize scaled_remainder_lift 17
  97. 0097specialize scaled_remainder_lift 5
  98. 0098specialize scaled_remainder_lift 2
  99. 0099specialize scaled_remainder_lift 18
  100. 0100specialize scaled_remainder_lift 11
  101. 0101specialize scaled_remainder_lift 15
  102. 0102specialize scaled_remainder_lift 2
  103. 0103apply scaled_remainder_lift
  104. 0104norm_num
  105. 0105norm_num
  106. 0106specialize nonzero_remainder_not_multiple 3
  107. 0107specialize nonzero_remainder_not_multiple (18 * 17 + 11)
  108. 0108specialize nonzero_remainder_not_multiple (18 * 5 + 15)
  109. 0109specialize nonzero_remainder_not_multiple 2
  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 0
  116. 0116norm_num
  117. 0117exact hdivides
  118. 0118cases hcases_right_right
  119. 0119rewrite hcases_right_right_left at hdivides
  120. 0120have hdivision_5 : (18 * 17 + 11) = 5 * (18 * 3 + 9) + 2
  121. 0121specialize scaled_remainder_lift 5
  122. 0122specialize scaled_remainder_lift 17
  123. 0123specialize scaled_remainder_lift 3
  124. 0124specialize scaled_remainder_lift 2
  125. 0125specialize scaled_remainder_lift 18
  126. 0126specialize scaled_remainder_lift 11
  127. 0127specialize scaled_remainder_lift 9
  128. 0128specialize scaled_remainder_lift 2
  129. 0129apply scaled_remainder_lift
  130. 0130norm_num
  131. 0131norm_num
  132. 0132specialize nonzero_remainder_not_multiple 5
  133. 0133specialize nonzero_remainder_not_multiple (18 * 17 + 11)
  134. 0134specialize nonzero_remainder_not_multiple (18 * 3 + 9)
  135. 0135specialize nonzero_remainder_not_multiple 2
  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 2
  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 : (18 * 17 + 11) = 7 * (18 * 2 + 9) + 2
  147. 0147specialize scaled_remainder_lift 7
  148. 0148specialize scaled_remainder_lift 17
  149. 0149specialize scaled_remainder_lift 2
  150. 0150specialize scaled_remainder_lift 3
  151. 0151specialize scaled_remainder_lift 18
  152. 0152specialize scaled_remainder_lift 11
  153. 0153specialize scaled_remainder_lift 9
  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 (18 * 17 + 11)
  160. 0160specialize nonzero_remainder_not_multiple (18 * 2 + 9)
  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 : (18 * 17 + 11) = 11 * (18 * 1 + 10) + 9
  173. 0173specialize scaled_remainder_lift 11
  174. 0174specialize scaled_remainder_lift 17
  175. 0175specialize scaled_remainder_lift 1
  176. 0176specialize scaled_remainder_lift 6
  177. 0177specialize scaled_remainder_lift 18
  178. 0178specialize scaled_remainder_lift 11
  179. 0179specialize scaled_remainder_lift 10
  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 (18 * 17 + 11)
  186. 0186specialize nonzero_remainder_not_multiple (18 * 1 + 10)
  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. 0197rewrite hcases_right_right_right_right_right_left at hdivides
  198. 0198have hdivision_13 : (18 * 17 + 11) = 13 * (18 * 1 + 6) + 5
  199. 0199specialize scaled_remainder_lift 13
  200. 0200specialize scaled_remainder_lift 17
  201. 0201specialize scaled_remainder_lift 1
  202. 0202specialize scaled_remainder_lift 4
  203. 0203specialize scaled_remainder_lift 18
  204. 0204specialize scaled_remainder_lift 11
  205. 0205specialize scaled_remainder_lift 6
  206. 0206specialize scaled_remainder_lift 5
  207. 0207apply scaled_remainder_lift
  208. 0208norm_num
  209. 0209norm_num
  210. 0210specialize nonzero_remainder_not_multiple 13
  211. 0211specialize nonzero_remainder_not_multiple (18 * 17 + 11)
  212. 0212specialize nonzero_remainder_not_multiple (18 * 1 + 6)
  213. 0213specialize nonzero_remainder_not_multiple 5
  214. 0214apply nonzero_remainder_not_multiple
  215. 0215exact hdivision_13
  216. 0216intro hrem_13_zero
  217. 0217apply PA1
  218. 0218exact hrem_13_zero
  219. 0219exists 7
  220. 0220norm_num
  221. 0221exact hdivides
  222. 0222cases hcases_right_right_right_right_right_right
  223. 0223rewrite hcases_right_right_right_right_right_right_left at hdivides
  224. 0224have hdivision_17 : (18 * 17 + 11) = 17 * (18 * 1 + 0) + 11
  225. 0225specialize scaled_remainder_lift 17
  226. 0226specialize scaled_remainder_lift 17
  227. 0227specialize scaled_remainder_lift 1
  228. 0228specialize scaled_remainder_lift 0
  229. 0229specialize scaled_remainder_lift 18
  230. 0230specialize scaled_remainder_lift 11
  231. 0231specialize scaled_remainder_lift 0
  232. 0232specialize scaled_remainder_lift 11
  233. 0233apply scaled_remainder_lift
  234. 0234norm_num
  235. 0235norm_num
  236. 0236specialize nonzero_remainder_not_multiple 17
  237. 0237specialize nonzero_remainder_not_multiple (18 * 17 + 11)
  238. 0238specialize nonzero_remainder_not_multiple (18 * 1 + 0)
  239. 0239specialize nonzero_remainder_not_multiple 11
  240. 0240apply nonzero_remainder_not_multiple
  241. 0241exact hdivision_17
  242. 0242intro hrem_17_zero
  243. 0243apply PA1
  244. 0244exact hrem_17_zero
  245. 0245exists 5
  246. 0246norm_num
  247. 0247exact hdivides
  248. 0248have htoo_large_19 : Lt(17,19)
    Exact native replay linehave htoo_large_19 : exists k. k + S 17 = 19
  249. 0249exists 1
  250. 0250norm_num
  251. 0251specialize lt_not_le 17
  252. 0252specialize lt_not_le 19
  253. 0253apply lt_not_le
  254. 0254exact htoo_large_19
  255. 0255rewrite hcases_right_right_right_right_right_right_right at hp_bound
  256. 0256exact hp_bound