BT011N · Bertrand theorem

prime_five_hundred_twenty_one

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

A native checked trial-division certificate for 521.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

Prime(2 · (11 · 22) + 37)

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

5 occurrences

Exact expanded native-PA statement
(~(2 * (11 * 22) + 37 = 1) /\ forall bpr_left_bb8cert_prime_five_hundred_twenty_one bpr_right_bb8cert_prime_five_hundred_twenty_one. 2 * (11 * 22) + 37 = bpr_left_bb8cert_prime_five_hundred_twenty_one * bpr_right_bb8cert_prime_five_hundred_twenty_one -> bpr_left_bb8cert_prime_five_hundred_twenty_one = 1 \/ bpr_right_bb8cert_prime_five_hundred_twenty_one = 1)

Proof neighborhood

Direct theorem prerequisites

BT000L add_eq_zero_right BT001J le_not_lt BT0003 add_assoc BT0002 add_comm BT011E double_scaled_remainder_lift BT000B add_mul BT0008 mul_assoc BT0009 one_mul BT011B nonzero_remainder_not_multiple BT0119 prime_of_no_small_prime_divisor_below_square BT000F le_trans BT011A prime_le_twenty_two_cases

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

287 script commands · 111 reading checkpoints · 11 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 (12)
add eq zero rightle not ltadd assocadd commdouble scaled remainder liftadd mulmul assocone mulnonzero remainder not multipleprime of no small prime divisor below squarele transprime le twenty two cases
01Establish hn0L1–2

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

  1. L1
    have hn0 : ~(2 * (11 * 22) + 37 = 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 : 37 = 0
  2. L4
    specialize add_eq_zero_right (2 * (11 * 22))
  3. L5
    specialize add_eq_zero_right 37
  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 : ~(2 * (11 * 22) + 37 = 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(36,1)Definitions: Lt(36,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 2 * (11 * 22)
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,37)Definitions: Lt(1,37)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 35
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 37
  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(2 · (11 · 22) + 37,23 · 23)Definitions: Lt(2 · (11 · 22) + 37,23 · 23)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 7
13Establish hvalueL25–26

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

  1. L25
    have hvalue : 2 * (11 * 22) + 37 = 23 * 22 + 15
  2. L26
    symm
14Establish hcoeffL27–36

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

  1. L27
    have hcoeff : 23 = 2 * 11 + 1
  2. L28
    norm_num
  3. L29
    rewrite hcoeff
  4. L30
    trans ((2 * 11) * 22 + 1 * 22) + 15
  5. L31
    congr
  6. L32
    apply add_mul
  7. L33
    refl
  8. L34
    trans (2 * (11 * 22) + 22) + 15
  9. L35
    congr
  10. L36
    congr
15Use earlier factsL37–38

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

  1. L37
    apply mul_assoc
  2. L38
    apply one_mul
16Calculate and transport equalitiesL39–40

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

  1. L39
    refl
  2. L40
    trans 2 * (11 * 22) + (22 + 15)
17Use earlier factsL41–41

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

  1. L41
    apply add_assoc
18Calculate and transport equalitiesL42–51

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

  1. L42
    trans 2 * (11 * 22) + 37
  2. L43
    congr
  3. L44
    refl
  4. L45
    norm_num
  5. L46
    refl
  6. L47
    rewrite hvalue
  7. L48
    trans 23 * 22 + 23
  8. L49
    rewrite <- PA4
  9. L50
    trans 23 * 22 + (7 + S 15)
  10. L51
    trans (7 + 23 * 22) + S 15
19Calculate and transport equalitiesL52–52

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

  1. L52
    symm
20Use earlier factsL53–53

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

  1. L53
    apply add_assoc
21Calculate and transport equalitiesL54–55

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

  1. L54
    trans (23 * 22 + 7) + S 15
  2. L55
    congr
22Use earlier factsL56–56

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

  1. L56
    apply add_comm
23Calculate and transport equalitiesL57–57

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

  1. L57
    refl
24Use earlier factsL58–58

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

  1. L58
    apply add_assoc
25Calculate and transport equalitiesL59–62

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

  1. L59
    congr
  2. L60
    refl
  3. L61
    norm_num
  4. L62
    symm
26Use earlier factsL63–69

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

  1. L63
    apply PA6
  2. L64
    specialize prime_of_no_small_prime_divisor_below_square 22
  3. L65
    specialize prime_of_no_small_prime_divisor_below_square (2 * (11 * 22) + 37)
  4. L66
    apply prime_of_no_small_prime_divisor_below_square
  5. L67
    exact hn0
  6. L68
    exact hn1
  7. L69
    exact hsquare
27Fix variables and assumptionsL70–73

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

  1. L70
    intro p
  2. L71
    intro hp
  3. L72
    intro hp_bound
  4. L73
    intro hdivides
28Establish hbound_22L74–74

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

  1. L74
    have hbound_22 : Lt(21,22)Definitions: Lt(21,22)Original native command in the exact edition
29Construct an explicit witnessL75–75

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

  1. L75
    exists 0
30Calculate and transport equalitiesL76–76

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

  1. L76
    norm_num
31Establish hp_22L77–83

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

  1. L77
  2. L78
    specialize le_trans p
  3. L79
    specialize le_trans 22
  4. L80
    specialize le_trans 22
  5. L81
    apply le_trans
  6. L82
    exact hp_bound
  7. L83
    exact hbound_22
32Establish hcasesL84–88

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

  1. L84
    have hcases : p = 2 \/ (p = 3 \/ (p = 5 \/ (p = 7 \/ (p = 11 \/ (p = 13 \/ (p = 17 \/ (p = 19)))))))
  2. L85
    specialize prime_le_twenty_two_cases p
  3. L86
    apply prime_le_twenty_two_cases
  4. L87
    exact hp
  5. L88
    exact hp_22
33Separate the logical casesL89–89

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

  1. L89
    cases hcases
34Calculate and transport equalitiesL90–90

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

  1. L90
    rewrite hcases_left at hdivides
35Use earlier factsL91–100

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

  1. L91
    specialize nonzero_remainder_not_multiple 2
  2. L92
    specialize nonzero_remainder_not_multiple (2 * (11 * 22) + 37)
  3. L93
    specialize nonzero_remainder_not_multiple (2 * (11 * 11 + 0) + 18)
  4. L94
    specialize nonzero_remainder_not_multiple 1
  5. L95
    apply nonzero_remainder_not_multiple
  6. L96
    specialize double_scaled_remainder_lift 2
  7. L97
    specialize double_scaled_remainder_lift 22
  8. L98
    specialize double_scaled_remainder_lift 11
  9. L99
    specialize double_scaled_remainder_lift 0
  10. L100
    specialize double_scaled_remainder_lift 0
36Use earlier factsL101–104

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

  1. L101
    specialize double_scaled_remainder_lift 0
  2. L102
    specialize double_scaled_remainder_lift 18
  3. L103
    specialize double_scaled_remainder_lift 1
  4. L104
    apply double_scaled_remainder_lift
37Calculate and transport equalitiesL105–107

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

  1. L105
    norm_num
  2. L106
    norm_num
  3. L107
    norm_num
38Fix variables and assumptionsL108–108

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

  1. L108
    intro hrem_2_zero
39Use earlier factsL109–110

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

  1. L109
    apply PA1
  2. L110
    exact hrem_2_zero
40Construct an explicit witnessL111–111

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

  1. L111
    exists 0
41Calculate and transport equalitiesL112–112

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

  1. L112
    norm_num
42Use earlier factsL113–113

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

  1. L113
    exact hdivides
43Separate the logical casesL114–114

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

  1. L114
    cases hcases_right
44Calculate and transport equalitiesL115–115

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

  1. L115
    rewrite hcases_right_left at hdivides
45Use earlier factsL116–125

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

  1. L116
    specialize nonzero_remainder_not_multiple 3
  2. L117
    specialize nonzero_remainder_not_multiple (2 * (11 * 22) + 37)
  3. L118
    specialize nonzero_remainder_not_multiple (2 * (11 * 7 + 3) + 13)
  4. L119
    specialize nonzero_remainder_not_multiple 2
  5. L120
    apply nonzero_remainder_not_multiple
  6. L121
    specialize double_scaled_remainder_lift 3
  7. L122
    specialize double_scaled_remainder_lift 22
  8. L123
    specialize double_scaled_remainder_lift 7
  9. L124
    specialize double_scaled_remainder_lift 1
  10. L125
    specialize double_scaled_remainder_lift 3
46Use earlier factsL126–129

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

  1. L126
    specialize double_scaled_remainder_lift 2
  2. L127
    specialize double_scaled_remainder_lift 13
  3. L128
    specialize double_scaled_remainder_lift 2
  4. L129
    apply double_scaled_remainder_lift
47Calculate and transport equalitiesL130–132

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
  3. L132
    norm_num
48Fix variables and assumptionsL133–133

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

  1. L133
    intro hrem_3_zero
49Use earlier factsL134–135

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

  1. L134
    apply PA1
  2. L135
    exact hrem_3_zero
50Construct an explicit witnessL136–136

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

  1. L136
    exists 0
51Calculate and transport equalitiesL137–137

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

  1. L137
    norm_num
52Use earlier factsL138–138

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

  1. L138
    exact hdivides
53Separate the logical casesL139–139

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

  1. L139
    cases hcases_right_right
54Calculate and transport equalitiesL140–140

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

  1. L140
    rewrite hcases_right_right_left at hdivides
55Use earlier factsL141–150

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

  1. L141
    specialize nonzero_remainder_not_multiple 5
  2. L142
    specialize nonzero_remainder_not_multiple (2 * (11 * 22) + 37)
  3. L143
    specialize nonzero_remainder_not_multiple (2 * (11 * 4 + 4) + 8)
  4. L144
    specialize nonzero_remainder_not_multiple 1
  5. L145
    apply nonzero_remainder_not_multiple
  6. L146
    specialize double_scaled_remainder_lift 5
  7. L147
    specialize double_scaled_remainder_lift 22
  8. L148
    specialize double_scaled_remainder_lift 4
  9. L149
    specialize double_scaled_remainder_lift 2
  10. L150
    specialize double_scaled_remainder_lift 4
56Use earlier factsL151–154

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

  1. L151
    specialize double_scaled_remainder_lift 2
  2. L152
    specialize double_scaled_remainder_lift 8
  3. L153
    specialize double_scaled_remainder_lift 1
  4. L154
    apply double_scaled_remainder_lift
57Calculate and transport equalitiesL155–157

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

  1. L155
    norm_num
  2. L156
    norm_num
  3. L157
    norm_num
58Fix variables and assumptionsL158–158

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

  1. L158
    intro hrem_5_zero
59Use earlier factsL159–160

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

  1. L159
    apply PA1
  2. L160
    exact hrem_5_zero
60Construct an explicit witnessL161–161

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

  1. L161
    exists 3
61Calculate and transport equalitiesL162–162

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

  1. L162
    norm_num
62Use earlier factsL163–163

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

  1. L163
    exact hdivides
63Separate the logical casesL164–164

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

  1. L164
    cases hcases_right_right_right
64Calculate and transport equalitiesL165–165

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

  1. L165
    rewrite hcases_right_right_right_left at hdivides
65Use earlier factsL166–175

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

  1. L166
    specialize nonzero_remainder_not_multiple 7
  2. L167
    specialize nonzero_remainder_not_multiple (2 * (11 * 22) + 37)
  3. L168
    specialize nonzero_remainder_not_multiple (2 * (11 * 3 + 1) + 6)
  4. L169
    specialize nonzero_remainder_not_multiple 3
  5. L170
    apply nonzero_remainder_not_multiple
  6. L171
    specialize double_scaled_remainder_lift 7
  7. L172
    specialize double_scaled_remainder_lift 22
  8. L173
    specialize double_scaled_remainder_lift 3
  9. L174
    specialize double_scaled_remainder_lift 1
  10. L175
    specialize double_scaled_remainder_lift 1
66Use earlier factsL176–179

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

  1. L176
    specialize double_scaled_remainder_lift 4
  2. L177
    specialize double_scaled_remainder_lift 6
  3. L178
    specialize double_scaled_remainder_lift 3
  4. L179
    apply double_scaled_remainder_lift
67Calculate and transport equalitiesL180–182

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

  1. L180
    norm_num
  2. L181
    norm_num
  3. L182
    norm_num
68Fix variables and assumptionsL183–183

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

  1. L183
    intro hrem_7_zero
69Use earlier factsL184–185

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

  1. L184
    apply PA1
  2. L185
    exact hrem_7_zero
70Construct an explicit witnessL186–186

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

  1. L186
    exists 3
71Calculate and transport equalitiesL187–187

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

  1. L187
    norm_num
72Use earlier factsL188–188

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

  1. L188
    exact hdivides
73Separate the logical casesL189–189

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

  1. L189
    cases hcases_right_right_right_right
74Calculate and transport equalitiesL190–190

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

  1. L190
    rewrite hcases_right_right_right_right_left at hdivides
75Use earlier factsL191–200

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

  1. L191
    specialize nonzero_remainder_not_multiple 11
  2. L192
    specialize nonzero_remainder_not_multiple (2 * (11 * 22) + 37)
  3. L193
    specialize nonzero_remainder_not_multiple (2 * (11 * 2 + 0) + 3)
  4. L194
    specialize nonzero_remainder_not_multiple 4
  5. L195
    apply nonzero_remainder_not_multiple
  6. L196
    specialize double_scaled_remainder_lift 11
  7. L197
    specialize double_scaled_remainder_lift 22
  8. L198
    specialize double_scaled_remainder_lift 2
  9. L199
    specialize double_scaled_remainder_lift 0
  10. L200
    specialize double_scaled_remainder_lift 0
76Use earlier factsL201–204

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

  1. L201
    specialize double_scaled_remainder_lift 0
  2. L202
    specialize double_scaled_remainder_lift 3
  3. L203
    specialize double_scaled_remainder_lift 4
  4. L204
    apply double_scaled_remainder_lift
77Calculate and transport equalitiesL205–207

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

  1. L205
    norm_num
  2. L206
    norm_num
  3. L207
    norm_num
78Fix variables and assumptionsL208–208

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

  1. L208
    intro hrem_11_zero
79Use earlier factsL209–210

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

  1. L209
    apply PA1
  2. L210
    exact hrem_11_zero
80Construct an explicit witnessL211–211

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

  1. L211
    exists 6
81Calculate and transport equalitiesL212–212

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

  1. L212
    norm_num
82Use earlier factsL213–213

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

  1. L213
    exact hdivides
83Separate the logical casesL214–214

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

  1. L214
    cases hcases_right_right_right_right_right
84Calculate and transport equalitiesL215–215

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

  1. L215
    rewrite hcases_right_right_right_right_right_left at hdivides
85Use earlier factsL216–225

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

  1. L216
    specialize nonzero_remainder_not_multiple 13
  2. L217
    specialize nonzero_remainder_not_multiple (2 * (11 * 22) + 37)
  3. L218
    specialize nonzero_remainder_not_multiple (2 * (11 * 1 + 7) + 4)
  4. L219
    specialize nonzero_remainder_not_multiple 1
  5. L220
    apply nonzero_remainder_not_multiple
  6. L221
    specialize double_scaled_remainder_lift 13
  7. L222
    specialize double_scaled_remainder_lift 22
  8. L223
    specialize double_scaled_remainder_lift 1
  9. L224
    specialize double_scaled_remainder_lift 9
  10. L225
    specialize double_scaled_remainder_lift 7
86Use earlier factsL226–229

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

  1. L226
    specialize double_scaled_remainder_lift 8
  2. L227
    specialize double_scaled_remainder_lift 4
  3. L228
    specialize double_scaled_remainder_lift 1
  4. L229
    apply double_scaled_remainder_lift
87Calculate and transport equalitiesL230–232

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

  1. L230
    norm_num
  2. L231
    norm_num
  3. L232
    norm_num
88Fix variables and assumptionsL233–233

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

  1. L233
    intro hrem_13_zero
89Use earlier factsL234–235

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

  1. L234
    apply PA1
  2. L235
    exact hrem_13_zero
90Construct an explicit witnessL236–236

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

  1. L236
    exists 11
91Calculate and transport equalitiesL237–237

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

  1. L237
    norm_num
92Use earlier factsL238–238

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

  1. L238
    exact hdivides
93Separate the logical casesL239–239

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

  1. L239
    cases hcases_right_right_right_right_right_right
94Calculate and transport equalitiesL240–240

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

  1. L240
    rewrite hcases_right_right_right_right_right_right_left at hdivides
95Use earlier factsL241–250

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

  1. L241
    specialize nonzero_remainder_not_multiple 17
  2. L242
    specialize nonzero_remainder_not_multiple (2 * (11 * 22) + 37)
  3. L243
    specialize nonzero_remainder_not_multiple (2 * (11 * 1 + 3) + 2)
  4. L244
    specialize nonzero_remainder_not_multiple 11
  5. L245
    apply nonzero_remainder_not_multiple
  6. L246
    specialize double_scaled_remainder_lift 17
  7. L247
    specialize double_scaled_remainder_lift 22
  8. L248
    specialize double_scaled_remainder_lift 1
  9. L249
    specialize double_scaled_remainder_lift 5
  10. L250
    specialize double_scaled_remainder_lift 3
96Use earlier factsL251–254

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

  1. L251
    specialize double_scaled_remainder_lift 4
  2. L252
    specialize double_scaled_remainder_lift 2
  3. L253
    specialize double_scaled_remainder_lift 11
  4. L254
    apply double_scaled_remainder_lift
97Calculate and transport equalitiesL255–257

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

  1. L255
    norm_num
  2. L256
    norm_num
  3. L257
    norm_num
98Fix variables and assumptionsL258–258

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

  1. L258
    intro hrem_17_zero
99Use earlier factsL259–260

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

  1. L259
    apply PA1
  2. L260
    exact hrem_17_zero
100Construct an explicit witnessL261–261

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

  1. L261
    exists 5
101Calculate and transport equalitiesL262–262

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

  1. L262
    norm_num
102Use earlier factsL263–263

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

  1. L263
    exact hdivides
103Calculate and transport equalitiesL264–264

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

  1. L264
    rewrite hcases_right_right_right_right_right_right_right at hdivides
104Use earlier factsL265–274

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

  1. L265
    specialize nonzero_remainder_not_multiple 19
  2. L266
    specialize nonzero_remainder_not_multiple (2 * (11 * 22) + 37)
  3. L267
    specialize nonzero_remainder_not_multiple (2 * (11 * 1 + 1) + 3)
  4. L268
    specialize nonzero_remainder_not_multiple 8
  5. L269
    apply nonzero_remainder_not_multiple
  6. L270
    specialize double_scaled_remainder_lift 19
  7. L271
    specialize double_scaled_remainder_lift 22
  8. L272
    specialize double_scaled_remainder_lift 1
  9. L273
    specialize double_scaled_remainder_lift 3
  10. L274
    specialize double_scaled_remainder_lift 1
105Use earlier factsL275–278

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

  1. L275
    specialize double_scaled_remainder_lift 14
  2. L276
    specialize double_scaled_remainder_lift 3
  3. L277
    specialize double_scaled_remainder_lift 8
  4. L278
    apply double_scaled_remainder_lift
106Calculate and transport equalitiesL279–281

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

  1. L279
    norm_num
  2. L280
    norm_num
  3. L281
    norm_num
107Fix variables and assumptionsL282–282

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

  1. L282
    intro hrem_19_zero
108Use earlier factsL283–284

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

  1. L283
    apply PA1
  2. L284
    exact hrem_19_zero
109Construct an explicit witnessL285–285

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

  1. L285
    exists 10
110Calculate and transport equalitiesL286–286

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

  1. L286
    norm_num
111Use earlier factsL287–287

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

  1. L287
    exact hdivides

Library-wide reading audit

Original defined command ledger · 287 lines
  1. 0001have hn0 : ~(2 * (11 * 22) + 37 = 0)
  2. 0002intro hzero
  3. 0003have htail_zero : 37 = 0
  4. 0004specialize add_eq_zero_right (2 * (11 * 22))
  5. 0005specialize add_eq_zero_right 37
  6. 0006apply add_eq_zero_right
  7. 0007exact hzero
  8. 0008apply PA1
  9. 0009exact htail_zero
  10. 0010have hn1 : ~(2 * (11 * 22) + 37 = 1)
  11. 0011intro hone
  12. 0012have htail_le_one : Lt(36,1)
    Exact native replay linehave htail_le_one : exists k. k + 37 = 1
  13. 0013exists 2 * (11 * 22)
  14. 0014exact hone
  15. 0015have hone_lt_tail : Lt(1,37)
    Exact native replay linehave hone_lt_tail : exists k. k + S 1 = 37
  16. 0016exists 35
  17. 0017norm_num
  18. 0018specialize le_not_lt 37
  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(2 · (11 · 22) + 37,23 · 23)
    Exact native replay linehave hsquare : exists bpr_gap_bb8cert_prime_five_hundred_twenty_one_square. bpr_gap_bb8cert_prime_five_hundred_twenty_one_square + S (2 * (11 * 22) + 37) = S 22 * S 22
  24. 0024exists 7
  25. 0025have hvalue : 2 * (11 * 22) + 37 = 23 * 22 + 15
  26. 0026symm
  27. 0027have hcoeff : 23 = 2 * 11 + 1
  28. 0028norm_num
  29. 0029rewrite hcoeff
  30. 0030trans ((2 * 11) * 22 + 1 * 22) + 15
  31. 0031congr
  32. 0032apply add_mul
  33. 0033refl
  34. 0034trans (2 * (11 * 22) + 22) + 15
  35. 0035congr
  36. 0036congr
  37. 0037apply mul_assoc
  38. 0038apply one_mul
  39. 0039refl
  40. 0040trans 2 * (11 * 22) + (22 + 15)
  41. 0041apply add_assoc
  42. 0042trans 2 * (11 * 22) + 37
  43. 0043congr
  44. 0044refl
  45. 0045norm_num
  46. 0046refl
  47. 0047rewrite hvalue
  48. 0048trans 23 * 22 + 23
  49. 0049rewrite <- PA4
  50. 0050trans 23 * 22 + (7 + S 15)
  51. 0051trans (7 + 23 * 22) + S 15
  52. 0052symm
  53. 0053apply add_assoc
  54. 0054trans (23 * 22 + 7) + S 15
  55. 0055congr
  56. 0056apply add_comm
  57. 0057refl
  58. 0058apply add_assoc
  59. 0059congr
  60. 0060refl
  61. 0061norm_num
  62. 0062symm
  63. 0063apply PA6
  64. 0064specialize prime_of_no_small_prime_divisor_below_square 22
  65. 0065specialize prime_of_no_small_prime_divisor_below_square (2 * (11 * 22) + 37)
  66. 0066apply prime_of_no_small_prime_divisor_below_square
  67. 0067exact hn0
  68. 0068exact hn1
  69. 0069exact hsquare
  70. 0070intro p
  71. 0071intro hp
  72. 0072intro hp_bound
  73. 0073intro hdivides
  74. 0074have hbound_22 : Lt(21,22)
    Exact native replay linehave hbound_22 : exists k. k + 22 = 22
  75. 0075exists 0
  76. 0076norm_num
  77. 0077have hp_22 : Le(p,22)
    Exact native replay linehave hp_22 : exists k. k + p = 22
  78. 0078specialize le_trans p
  79. 0079specialize le_trans 22
  80. 0080specialize le_trans 22
  81. 0081apply le_trans
  82. 0082exact hp_bound
  83. 0083exact hbound_22
  84. 0084have hcases : p = 2 \/ (p = 3 \/ (p = 5 \/ (p = 7 \/ (p = 11 \/ (p = 13 \/ (p = 17 \/ (p = 19)))))))
  85. 0085specialize prime_le_twenty_two_cases p
  86. 0086apply prime_le_twenty_two_cases
  87. 0087exact hp
  88. 0088exact hp_22
  89. 0089cases hcases
  90. 0090rewrite hcases_left at hdivides
  91. 0091specialize nonzero_remainder_not_multiple 2
  92. 0092specialize nonzero_remainder_not_multiple (2 * (11 * 22) + 37)
  93. 0093specialize nonzero_remainder_not_multiple (2 * (11 * 11 + 0) + 18)
  94. 0094specialize nonzero_remainder_not_multiple 1
  95. 0095apply nonzero_remainder_not_multiple
  96. 0096specialize double_scaled_remainder_lift 2
  97. 0097specialize double_scaled_remainder_lift 22
  98. 0098specialize double_scaled_remainder_lift 11
  99. 0099specialize double_scaled_remainder_lift 0
  100. 0100specialize double_scaled_remainder_lift 0
  101. 0101specialize double_scaled_remainder_lift 0
  102. 0102specialize double_scaled_remainder_lift 18
  103. 0103specialize double_scaled_remainder_lift 1
  104. 0104apply double_scaled_remainder_lift
  105. 0105norm_num
  106. 0106norm_num
  107. 0107norm_num
  108. 0108intro hrem_2_zero
  109. 0109apply PA1
  110. 0110exact hrem_2_zero
  111. 0111exists 0
  112. 0112norm_num
  113. 0113exact hdivides
  114. 0114cases hcases_right
  115. 0115rewrite hcases_right_left at hdivides
  116. 0116specialize nonzero_remainder_not_multiple 3
  117. 0117specialize nonzero_remainder_not_multiple (2 * (11 * 22) + 37)
  118. 0118specialize nonzero_remainder_not_multiple (2 * (11 * 7 + 3) + 13)
  119. 0119specialize nonzero_remainder_not_multiple 2
  120. 0120apply nonzero_remainder_not_multiple
  121. 0121specialize double_scaled_remainder_lift 3
  122. 0122specialize double_scaled_remainder_lift 22
  123. 0123specialize double_scaled_remainder_lift 7
  124. 0124specialize double_scaled_remainder_lift 1
  125. 0125specialize double_scaled_remainder_lift 3
  126. 0126specialize double_scaled_remainder_lift 2
  127. 0127specialize double_scaled_remainder_lift 13
  128. 0128specialize double_scaled_remainder_lift 2
  129. 0129apply double_scaled_remainder_lift
  130. 0130norm_num
  131. 0131norm_num
  132. 0132norm_num
  133. 0133intro hrem_3_zero
  134. 0134apply PA1
  135. 0135exact hrem_3_zero
  136. 0136exists 0
  137. 0137norm_num
  138. 0138exact hdivides
  139. 0139cases hcases_right_right
  140. 0140rewrite hcases_right_right_left at hdivides
  141. 0141specialize nonzero_remainder_not_multiple 5
  142. 0142specialize nonzero_remainder_not_multiple (2 * (11 * 22) + 37)
  143. 0143specialize nonzero_remainder_not_multiple (2 * (11 * 4 + 4) + 8)
  144. 0144specialize nonzero_remainder_not_multiple 1
  145. 0145apply nonzero_remainder_not_multiple
  146. 0146specialize double_scaled_remainder_lift 5
  147. 0147specialize double_scaled_remainder_lift 22
  148. 0148specialize double_scaled_remainder_lift 4
  149. 0149specialize double_scaled_remainder_lift 2
  150. 0150specialize double_scaled_remainder_lift 4
  151. 0151specialize double_scaled_remainder_lift 2
  152. 0152specialize double_scaled_remainder_lift 8
  153. 0153specialize double_scaled_remainder_lift 1
  154. 0154apply double_scaled_remainder_lift
  155. 0155norm_num
  156. 0156norm_num
  157. 0157norm_num
  158. 0158intro hrem_5_zero
  159. 0159apply PA1
  160. 0160exact hrem_5_zero
  161. 0161exists 3
  162. 0162norm_num
  163. 0163exact hdivides
  164. 0164cases hcases_right_right_right
  165. 0165rewrite hcases_right_right_right_left at hdivides
  166. 0166specialize nonzero_remainder_not_multiple 7
  167. 0167specialize nonzero_remainder_not_multiple (2 * (11 * 22) + 37)
  168. 0168specialize nonzero_remainder_not_multiple (2 * (11 * 3 + 1) + 6)
  169. 0169specialize nonzero_remainder_not_multiple 3
  170. 0170apply nonzero_remainder_not_multiple
  171. 0171specialize double_scaled_remainder_lift 7
  172. 0172specialize double_scaled_remainder_lift 22
  173. 0173specialize double_scaled_remainder_lift 3
  174. 0174specialize double_scaled_remainder_lift 1
  175. 0175specialize double_scaled_remainder_lift 1
  176. 0176specialize double_scaled_remainder_lift 4
  177. 0177specialize double_scaled_remainder_lift 6
  178. 0178specialize double_scaled_remainder_lift 3
  179. 0179apply double_scaled_remainder_lift
  180. 0180norm_num
  181. 0181norm_num
  182. 0182norm_num
  183. 0183intro hrem_7_zero
  184. 0184apply PA1
  185. 0185exact hrem_7_zero
  186. 0186exists 3
  187. 0187norm_num
  188. 0188exact hdivides
  189. 0189cases hcases_right_right_right_right
  190. 0190rewrite hcases_right_right_right_right_left at hdivides
  191. 0191specialize nonzero_remainder_not_multiple 11
  192. 0192specialize nonzero_remainder_not_multiple (2 * (11 * 22) + 37)
  193. 0193specialize nonzero_remainder_not_multiple (2 * (11 * 2 + 0) + 3)
  194. 0194specialize nonzero_remainder_not_multiple 4
  195. 0195apply nonzero_remainder_not_multiple
  196. 0196specialize double_scaled_remainder_lift 11
  197. 0197specialize double_scaled_remainder_lift 22
  198. 0198specialize double_scaled_remainder_lift 2
  199. 0199specialize double_scaled_remainder_lift 0
  200. 0200specialize double_scaled_remainder_lift 0
  201. 0201specialize double_scaled_remainder_lift 0
  202. 0202specialize double_scaled_remainder_lift 3
  203. 0203specialize double_scaled_remainder_lift 4
  204. 0204apply double_scaled_remainder_lift
  205. 0205norm_num
  206. 0206norm_num
  207. 0207norm_num
  208. 0208intro hrem_11_zero
  209. 0209apply PA1
  210. 0210exact hrem_11_zero
  211. 0211exists 6
  212. 0212norm_num
  213. 0213exact hdivides
  214. 0214cases hcases_right_right_right_right_right
  215. 0215rewrite hcases_right_right_right_right_right_left at hdivides
  216. 0216specialize nonzero_remainder_not_multiple 13
  217. 0217specialize nonzero_remainder_not_multiple (2 * (11 * 22) + 37)
  218. 0218specialize nonzero_remainder_not_multiple (2 * (11 * 1 + 7) + 4)
  219. 0219specialize nonzero_remainder_not_multiple 1
  220. 0220apply nonzero_remainder_not_multiple
  221. 0221specialize double_scaled_remainder_lift 13
  222. 0222specialize double_scaled_remainder_lift 22
  223. 0223specialize double_scaled_remainder_lift 1
  224. 0224specialize double_scaled_remainder_lift 9
  225. 0225specialize double_scaled_remainder_lift 7
  226. 0226specialize double_scaled_remainder_lift 8
  227. 0227specialize double_scaled_remainder_lift 4
  228. 0228specialize double_scaled_remainder_lift 1
  229. 0229apply double_scaled_remainder_lift
  230. 0230norm_num
  231. 0231norm_num
  232. 0232norm_num
  233. 0233intro hrem_13_zero
  234. 0234apply PA1
  235. 0235exact hrem_13_zero
  236. 0236exists 11
  237. 0237norm_num
  238. 0238exact hdivides
  239. 0239cases hcases_right_right_right_right_right_right
  240. 0240rewrite hcases_right_right_right_right_right_right_left at hdivides
  241. 0241specialize nonzero_remainder_not_multiple 17
  242. 0242specialize nonzero_remainder_not_multiple (2 * (11 * 22) + 37)
  243. 0243specialize nonzero_remainder_not_multiple (2 * (11 * 1 + 3) + 2)
  244. 0244specialize nonzero_remainder_not_multiple 11
  245. 0245apply nonzero_remainder_not_multiple
  246. 0246specialize double_scaled_remainder_lift 17
  247. 0247specialize double_scaled_remainder_lift 22
  248. 0248specialize double_scaled_remainder_lift 1
  249. 0249specialize double_scaled_remainder_lift 5
  250. 0250specialize double_scaled_remainder_lift 3
  251. 0251specialize double_scaled_remainder_lift 4
  252. 0252specialize double_scaled_remainder_lift 2
  253. 0253specialize double_scaled_remainder_lift 11
  254. 0254apply double_scaled_remainder_lift
  255. 0255norm_num
  256. 0256norm_num
  257. 0257norm_num
  258. 0258intro hrem_17_zero
  259. 0259apply PA1
  260. 0260exact hrem_17_zero
  261. 0261exists 5
  262. 0262norm_num
  263. 0263exact hdivides
  264. 0264rewrite hcases_right_right_right_right_right_right_right at hdivides
  265. 0265specialize nonzero_remainder_not_multiple 19
  266. 0266specialize nonzero_remainder_not_multiple (2 * (11 * 22) + 37)
  267. 0267specialize nonzero_remainder_not_multiple (2 * (11 * 1 + 1) + 3)
  268. 0268specialize nonzero_remainder_not_multiple 8
  269. 0269apply nonzero_remainder_not_multiple
  270. 0270specialize double_scaled_remainder_lift 19
  271. 0271specialize double_scaled_remainder_lift 22
  272. 0272specialize double_scaled_remainder_lift 1
  273. 0273specialize double_scaled_remainder_lift 3
  274. 0274specialize double_scaled_remainder_lift 1
  275. 0275specialize double_scaled_remainder_lift 14
  276. 0276specialize double_scaled_remainder_lift 3
  277. 0277specialize double_scaled_remainder_lift 8
  278. 0278apply double_scaled_remainder_lift
  279. 0279norm_num
  280. 0280norm_num
  281. 0281norm_num
  282. 0282intro hrem_19_zero
  283. 0283apply PA1
  284. 0284exact hrem_19_zero
  285. 0285exists 10
  286. 0286norm_num
  287. 0287exact hdivides