BT011A

prime_le_twenty_two_cases

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

The only primes at most twenty-two are the eight displayed values.

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.

Exact expanded PA statement

forall p. ((~(p = 1) /\ forall bpr_left_bb8p22_prime bpr_right_bb8p22_prime. p = bpr_left_bb8p22_prime * bpr_right_bb8p22_prime -> bpr_left_bb8p22_prime = 1 \/ bpr_right_bb8p22_prime = 1)) -> (exists bpr_le_gap_bb8p22_bound. bpr_le_gap_bb8p22_bound + (p) = (22)) -> (p = 2 \/ (p = 3 \/ (p = 5 \/ (p = 7 \/ (p = 11 \/ (p = 13 \/ (p = 17 \/ (p = 19))))))))

Structural proof guide

The only primes at most twenty-two are the eight displayed values.

Direct prerequisites: le_eq_or_lt, le_of_succ_le_succ, prime_is_succ_succ, lt_not_le, fixed_nontrivial_factor_not_prime. The authored body proceeds by case analysis (22), intermediate claims (43), equality transport (3), closed numeral normalization (13).

Proof neighborhood

Direct dependencies

BT001C le_eq_or_lt BT0017 le_of_succ_le_succ BT00AW prime_is_succ_succ BT001I lt_not_le BT0116 fixed_nontrivial_factor_not_prime

Direct dependents

BT011F prime_five BT011G prime_seven BT011H prime_thirteen BT011I prime_twenty_three BT011J prime_forty_three BT011K prime_eighty_three BT011L prime_one_hundred_sixty_three BT011M prime_three_hundred_seventeen BT011N prime_five_hundred_twenty_one

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

473 script commands · 183 reading checkpoints · 43 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.

Named ingredients (5)
le eq or ltle of succ le succprime is succ succlt not lefixed nontrivial factor not prime
01Fix variables and assumptionsL1–3

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

  1. L1
    intro p
  2. L2
    intro hp
  3. L3
    intro hbound
02Establish hsplit_22L4–8

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

  1. L4
    have hsplit_22 : p = 22 \/ (exists k. k + S p = 22)
  2. L5
    specialize le_eq_or_lt p
  3. L6
    specialize le_eq_or_lt 22
  4. L7
    apply le_eq_or_lt
  5. L8
    exact hbound
03Separate the logical casesL9–10

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

  1. L9
    cases hsplit_22
  2. L10
    exfalso
04Use earlier factsL11–14

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

  1. L11
    specialize fixed_nontrivial_factor_not_prime p
  2. L12
    specialize fixed_nontrivial_factor_not_prime 2
  3. L13
    specialize fixed_nontrivial_factor_not_prime 11
  4. L14
    apply fixed_nontrivial_factor_not_prime
05Calculate and transport equalitiesL15–15

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

  1. L15
    trans 22
06Use earlier factsL16–16

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

  1. L16
    exact hsplit_22_left
07Calculate 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
08Fix variables and assumptionsL18–18

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

  1. L18
    intro hleft_one
09Use earlier factsL19–21

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

  1. L19
    apply PA1
  2. L20
    apply PA2
  3. L21
    exact hleft_one
10Fix variables and assumptionsL22–22

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

  1. L22
    intro hright_one
11Use earlier factsL23–26

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

  1. L23
    apply PA1
  2. L24
    apply PA2
  3. L25
    exact hright_one
  4. L26
    exact hp
12Establish hbound_21L27–29

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

  1. L27
    have hbound_21 : exists k. k + p = 21
  2. L28
    apply le_of_succ_le_succ
  3. L29
    exact hsplit_22_right
13Establish hsplit_21L30–34

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

  1. L30
    have hsplit_21 : p = 21 \/ (exists k. k + S p = 21)
  2. L31
    specialize le_eq_or_lt p
  3. L32
    specialize le_eq_or_lt 21
  4. L33
    apply le_eq_or_lt
  5. L34
    exact hbound_21
14Separate the logical casesL35–36

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

  1. L35
    cases hsplit_21
  2. L36
    exfalso
15Use earlier factsL37–40

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

  1. L37
    specialize fixed_nontrivial_factor_not_prime p
  2. L38
    specialize fixed_nontrivial_factor_not_prime 3
  3. L39
    specialize fixed_nontrivial_factor_not_prime 7
  4. L40
    apply fixed_nontrivial_factor_not_prime
16Calculate and transport equalitiesL41–41

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

  1. L41
    trans 21
17Use earlier factsL42–42

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

  1. L42
    exact hsplit_21_left
18Calculate and transport equalitiesL43–43

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

  1. L43
    norm_num
19Fix variables and assumptionsL44–44

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

  1. L44
    intro hleft_one
20Use earlier factsL45–47

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

  1. L45
    apply PA1
  2. L46
    apply PA2
  3. L47
    exact hleft_one
21Fix variables and assumptionsL48–48

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

  1. L48
    intro hright_one
22Use earlier factsL49–52

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

  1. L49
    apply PA1
  2. L50
    apply PA2
  3. L51
    exact hright_one
  4. L52
    exact hp
23Establish hbound_20L53–55

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

  1. L53
    have hbound_20 : exists k. k + p = 20
  2. L54
    apply le_of_succ_le_succ
  3. L55
    exact hsplit_21_right
24Establish hsplit_20L56–60

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

  1. L56
    have hsplit_20 : p = 20 \/ (exists k. k + S p = 20)
  2. L57
    specialize le_eq_or_lt p
  3. L58
    specialize le_eq_or_lt 20
  4. L59
    apply le_eq_or_lt
  5. L60
    exact hbound_20
25Separate the logical casesL61–62

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

  1. L61
    cases hsplit_20
  2. L62
    exfalso
26Use earlier factsL63–66

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

  1. L63
    specialize fixed_nontrivial_factor_not_prime p
  2. L64
    specialize fixed_nontrivial_factor_not_prime 4
  3. L65
    specialize fixed_nontrivial_factor_not_prime 5
  4. L66
    apply fixed_nontrivial_factor_not_prime
27Calculate and transport equalitiesL67–67

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

  1. L67
    trans 20
28Use earlier factsL68–68

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

  1. L68
    exact hsplit_20_left
29Calculate and transport equalitiesL69–69

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

  1. L69
    norm_num
30Fix variables and assumptionsL70–70

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

  1. L70
    intro hleft_one
31Use earlier factsL71–73

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

  1. L71
    apply PA1
  2. L72
    apply PA2
  3. L73
    exact hleft_one
32Fix variables and assumptionsL74–74

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

  1. L74
    intro hright_one
33Use earlier factsL75–78

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

  1. L75
    apply PA1
  2. L76
    apply PA2
  3. L77
    exact hright_one
  4. L78
    exact hp
34Establish hbound_19L79–81

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

  1. L79
    have hbound_19 : exists k. k + p = 19
  2. L80
    apply le_of_succ_le_succ
  3. L81
    exact hsplit_20_right
35Establish hsplit_19L82–86

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

  1. L82
    have hsplit_19 : p = 19 \/ (exists k. k + S p = 19)
  2. L83
    specialize le_eq_or_lt p
  3. L84
    specialize le_eq_or_lt 19
  4. L85
    apply le_eq_or_lt
  5. L86
    exact hbound_19
36Separate the logical casesL87–94

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

  1. L87
    cases hsplit_19
  2. L88
    right
  3. L89
    right
  4. L90
    right
  5. L91
    right
  6. L92
    right
  7. L93
    right
  8. L94
    right
37Use earlier factsL95–95

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

  1. L95
    exact hsplit_19_left
38Establish hbound_18L96–98

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

  1. L96
    have hbound_18 : exists k. k + p = 18
  2. L97
    apply le_of_succ_le_succ
  3. L98
    exact hsplit_19_right
39Establish hsplit_18L99–103

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

  1. L99
    have hsplit_18 : p = 18 \/ (exists k. k + S p = 18)
  2. L100
    specialize le_eq_or_lt p
  3. L101
    specialize le_eq_or_lt 18
  4. L102
    apply le_eq_or_lt
  5. L103
    exact hbound_18
40Separate the logical casesL104–105

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

  1. L104
    cases hsplit_18
  2. L105
    exfalso
41Use earlier factsL106–109

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

  1. L106
    specialize fixed_nontrivial_factor_not_prime p
  2. L107
    specialize fixed_nontrivial_factor_not_prime 3
  3. L108
    specialize fixed_nontrivial_factor_not_prime 6
  4. L109
    apply fixed_nontrivial_factor_not_prime
42Calculate and transport equalitiesL110–110

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

  1. L110
    trans 18
43Use earlier factsL111–111

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

  1. L111
    exact hsplit_18_left
44Calculate 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
45Fix variables and assumptionsL113–113

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

  1. L113
    intro hleft_one
46Use earlier factsL114–116

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

  1. L114
    apply PA1
  2. L115
    apply PA2
  3. L116
    exact hleft_one
47Fix variables and assumptionsL117–117

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

  1. L117
    intro hright_one
48Use earlier factsL118–121

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

  1. L118
    apply PA1
  2. L119
    apply PA2
  3. L120
    exact hright_one
  4. L121
    exact hp
49Establish hbound_17L122–124

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

  1. L122
    have hbound_17 : exists k. k + p = 17
  2. L123
    apply le_of_succ_le_succ
  3. L124
    exact hsplit_18_right
50Establish hsplit_17L125–129

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

  1. L125
    have hsplit_17 : p = 17 \/ (exists k. k + S p = 17)
  2. L126
    specialize le_eq_or_lt p
  3. L127
    specialize le_eq_or_lt 17
  4. L128
    apply le_eq_or_lt
  5. L129
    exact hbound_17
51Separate the logical casesL130–137

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

  1. L130
    cases hsplit_17
  2. L131
    right
  3. L132
    right
  4. L133
    right
  5. L134
    right
  6. L135
    right
  7. L136
    right
  8. L137
    left
52Use earlier factsL138–138

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

  1. L138
    exact hsplit_17_left
53Establish hbound_16L139–141

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

  1. L139
    have hbound_16 : exists k. k + p = 16
  2. L140
    apply le_of_succ_le_succ
  3. L141
    exact hsplit_17_right
54Establish hsplit_16L142–146

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

  1. L142
    have hsplit_16 : p = 16 \/ (exists k. k + S p = 16)
  2. L143
    specialize le_eq_or_lt p
  3. L144
    specialize le_eq_or_lt 16
  4. L145
    apply le_eq_or_lt
  5. L146
    exact hbound_16
55Separate the logical casesL147–148

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

  1. L147
    cases hsplit_16
  2. L148
    exfalso
56Use earlier factsL149–152

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

  1. L149
    specialize fixed_nontrivial_factor_not_prime p
  2. L150
    specialize fixed_nontrivial_factor_not_prime 4
  3. L151
    specialize fixed_nontrivial_factor_not_prime 4
  4. L152
    apply fixed_nontrivial_factor_not_prime
57Calculate and transport equalitiesL153–153

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

  1. L153
    trans 16
58Use earlier factsL154–154

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

  1. L154
    exact hsplit_16_left
59Calculate and transport equalitiesL155–155

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

  1. L155
    norm_num
60Fix variables and assumptionsL156–156

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

  1. L156
    intro hleft_one
61Use earlier factsL157–159

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

  1. L157
    apply PA1
  2. L158
    apply PA2
  3. L159
    exact hleft_one
62Fix variables and assumptionsL160–160

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

  1. L160
    intro hright_one
63Use earlier factsL161–164

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

  1. L161
    apply PA1
  2. L162
    apply PA2
  3. L163
    exact hright_one
  4. L164
    exact hp
64Establish hbound_15L165–167

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

  1. L165
    have hbound_15 : exists k. k + p = 15
  2. L166
    apply le_of_succ_le_succ
  3. L167
    exact hsplit_16_right
65Establish hsplit_15L168–172

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

  1. L168
    have hsplit_15 : p = 15 \/ (exists k. k + S p = 15)
  2. L169
    specialize le_eq_or_lt p
  3. L170
    specialize le_eq_or_lt 15
  4. L171
    apply le_eq_or_lt
  5. L172
    exact hbound_15
66Separate the logical casesL173–174

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

  1. L173
    cases hsplit_15
  2. L174
    exfalso
67Use earlier factsL175–178

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

  1. L175
    specialize fixed_nontrivial_factor_not_prime p
  2. L176
    specialize fixed_nontrivial_factor_not_prime 3
  3. L177
    specialize fixed_nontrivial_factor_not_prime 5
  4. L178
    apply fixed_nontrivial_factor_not_prime
68Calculate and transport equalitiesL179–179

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

  1. L179
    trans 15
69Use earlier factsL180–180

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

  1. L180
    exact hsplit_15_left
70Calculate and transport equalitiesL181–181

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

  1. L181
    norm_num
71Fix variables and assumptionsL182–182

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

  1. L182
    intro hleft_one
72Use earlier factsL183–185

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

  1. L183
    apply PA1
  2. L184
    apply PA2
  3. L185
    exact hleft_one
73Fix variables and assumptionsL186–186

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

  1. L186
    intro hright_one
74Use earlier factsL187–190

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

  1. L187
    apply PA1
  2. L188
    apply PA2
  3. L189
    exact hright_one
  4. L190
    exact hp
75Establish hbound_14L191–193

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

  1. L191
    have hbound_14 : exists k. k + p = 14
  2. L192
    apply le_of_succ_le_succ
  3. L193
    exact hsplit_15_right
76Establish hsplit_14L194–198

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

  1. L194
    have hsplit_14 : p = 14 \/ (exists k. k + S p = 14)
  2. L195
    specialize le_eq_or_lt p
  3. L196
    specialize le_eq_or_lt 14
  4. L197
    apply le_eq_or_lt
  5. L198
    exact hbound_14
77Separate the logical casesL199–200

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

  1. L199
    cases hsplit_14
  2. L200
    exfalso
78Use earlier factsL201–204

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

  1. L201
    specialize fixed_nontrivial_factor_not_prime p
  2. L202
    specialize fixed_nontrivial_factor_not_prime 2
  3. L203
    specialize fixed_nontrivial_factor_not_prime 7
  4. L204
    apply fixed_nontrivial_factor_not_prime
79Calculate and transport equalitiesL205–205

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

  1. L205
    trans 14
80Use earlier factsL206–206

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

  1. L206
    exact hsplit_14_left
81Calculate and transport equalitiesL207–207

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

  1. L207
    norm_num
82Fix variables and assumptionsL208–208

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

  1. L208
    intro hleft_one
83Use earlier factsL209–211

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

  1. L209
    apply PA1
  2. L210
    apply PA2
  3. L211
    exact hleft_one
84Fix variables and assumptionsL212–212

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

  1. L212
    intro hright_one
85Use earlier factsL213–216

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

  1. L213
    apply PA1
  2. L214
    apply PA2
  3. L215
    exact hright_one
  4. L216
    exact hp
86Establish hbound_13L217–219

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

  1. L217
    have hbound_13 : exists k. k + p = 13
  2. L218
    apply le_of_succ_le_succ
  3. L219
    exact hsplit_14_right
87Establish hsplit_13L220–224

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

  1. L220
    have hsplit_13 : p = 13 \/ (exists k. k + S p = 13)
  2. L221
    specialize le_eq_or_lt p
  3. L222
    specialize le_eq_or_lt 13
  4. L223
    apply le_eq_or_lt
  5. L224
    exact hbound_13
88Separate the logical casesL225–231

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

  1. L225
    cases hsplit_13
  2. L226
    right
  3. L227
    right
  4. L228
    right
  5. L229
    right
  6. L230
    right
  7. L231
    left
89Use earlier factsL232–232

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

  1. L232
    exact hsplit_13_left
90Establish hbound_12L233–235

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

  1. L233
    have hbound_12 : exists k. k + p = 12
  2. L234
    apply le_of_succ_le_succ
  3. L235
    exact hsplit_13_right
91Establish hsplit_12L236–240

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

  1. L236
    have hsplit_12 : p = 12 \/ (exists k. k + S p = 12)
  2. L237
    specialize le_eq_or_lt p
  3. L238
    specialize le_eq_or_lt 12
  4. L239
    apply le_eq_or_lt
  5. L240
    exact hbound_12
92Separate the logical casesL241–242

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

  1. L241
    cases hsplit_12
  2. L242
    exfalso
93Use earlier factsL243–246

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

  1. L243
    specialize fixed_nontrivial_factor_not_prime p
  2. L244
    specialize fixed_nontrivial_factor_not_prime 3
  3. L245
    specialize fixed_nontrivial_factor_not_prime 4
  4. L246
    apply fixed_nontrivial_factor_not_prime
94Calculate and transport equalitiesL247–247

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

  1. L247
    trans 12
95Use earlier factsL248–248

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

  1. L248
    exact hsplit_12_left
96Calculate and transport equalitiesL249–249

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

  1. L249
    norm_num
97Fix variables and assumptionsL250–250

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

  1. L250
    intro hleft_one
98Use earlier factsL251–253

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

  1. L251
    apply PA1
  2. L252
    apply PA2
  3. L253
    exact hleft_one
99Fix variables and assumptionsL254–254

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

  1. L254
    intro hright_one
100Use earlier factsL255–258

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

  1. L255
    apply PA1
  2. L256
    apply PA2
  3. L257
    exact hright_one
  4. L258
    exact hp
101Establish hbound_11L259–261

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

  1. L259
    have hbound_11 : exists k. k + p = 11
  2. L260
    apply le_of_succ_le_succ
  3. L261
    exact hsplit_12_right
102Establish hsplit_11L262–266

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

  1. L262
    have hsplit_11 : p = 11 \/ (exists k. k + S p = 11)
  2. L263
    specialize le_eq_or_lt p
  3. L264
    specialize le_eq_or_lt 11
  4. L265
    apply le_eq_or_lt
  5. L266
    exact hbound_11
103Separate the logical casesL267–272

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

  1. L267
    cases hsplit_11
  2. L268
    right
  3. L269
    right
  4. L270
    right
  5. L271
    right
  6. L272
    left
104Use earlier factsL273–273

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

  1. L273
    exact hsplit_11_left
105Establish hbound_10L274–276

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

  1. L274
    have hbound_10 : exists k. k + p = 10
  2. L275
    apply le_of_succ_le_succ
  3. L276
    exact hsplit_11_right
106Establish hsplit_10L277–281

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

  1. L277
    have hsplit_10 : p = 10 \/ (exists k. k + S p = 10)
  2. L278
    specialize le_eq_or_lt p
  3. L279
    specialize le_eq_or_lt 10
  4. L280
    apply le_eq_or_lt
  5. L281
    exact hbound_10
107Separate the logical casesL282–283

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

  1. L282
    cases hsplit_10
  2. L283
    exfalso
108Use earlier factsL284–287

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

  1. L284
    specialize fixed_nontrivial_factor_not_prime p
  2. L285
    specialize fixed_nontrivial_factor_not_prime 2
  3. L286
    specialize fixed_nontrivial_factor_not_prime 5
  4. L287
    apply fixed_nontrivial_factor_not_prime
109Calculate and transport equalitiesL288–288

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

  1. L288
    trans 10
110Use earlier factsL289–289

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

  1. L289
    exact hsplit_10_left
111Calculate and transport equalitiesL290–290

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

  1. L290
    norm_num
112Fix variables and assumptionsL291–291

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

  1. L291
    intro hleft_one
113Use earlier factsL292–294

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

  1. L292
    apply PA1
  2. L293
    apply PA2
  3. L294
    exact hleft_one
114Fix variables and assumptionsL295–295

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

  1. L295
    intro hright_one
115Use earlier factsL296–299

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

  1. L296
    apply PA1
  2. L297
    apply PA2
  3. L298
    exact hright_one
  4. L299
    exact hp
116Establish hbound_9L300–302

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

  1. L300
    have hbound_9 : exists k. k + p = 9
  2. L301
    apply le_of_succ_le_succ
  3. L302
    exact hsplit_10_right
117Establish hsplit_9L303–307

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

  1. L303
    have hsplit_9 : p = 9 \/ (exists k. k + S p = 9)
  2. L304
    specialize le_eq_or_lt p
  3. L305
    specialize le_eq_or_lt 9
  4. L306
    apply le_eq_or_lt
  5. L307
    exact hbound_9
118Separate the logical casesL308–309

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

  1. L308
    cases hsplit_9
  2. L309
    exfalso
119Use earlier factsL310–313

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

  1. L310
    specialize fixed_nontrivial_factor_not_prime p
  2. L311
    specialize fixed_nontrivial_factor_not_prime 3
  3. L312
    specialize fixed_nontrivial_factor_not_prime 3
  4. L313
    apply fixed_nontrivial_factor_not_prime
120Calculate and transport equalitiesL314–314

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

  1. L314
    trans 9
121Use earlier factsL315–315

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

  1. L315
    exact hsplit_9_left
122Calculate and transport equalitiesL316–316

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

  1. L316
    norm_num
123Fix variables and assumptionsL317–317

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

  1. L317
    intro hleft_one
124Use earlier factsL318–320

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

  1. L318
    apply PA1
  2. L319
    apply PA2
  3. L320
    exact hleft_one
125Fix variables and assumptionsL321–321

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

  1. L321
    intro hright_one
126Use earlier factsL322–325

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

  1. L322
    apply PA1
  2. L323
    apply PA2
  3. L324
    exact hright_one
  4. L325
    exact hp
127Establish hbound_8L326–328

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

  1. L326
    have hbound_8 : exists k. k + p = 8
  2. L327
    apply le_of_succ_le_succ
  3. L328
    exact hsplit_9_right
128Establish hsplit_8L329–333

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

  1. L329
    have hsplit_8 : p = 8 \/ (exists k. k + S p = 8)
  2. L330
    specialize le_eq_or_lt p
  3. L331
    specialize le_eq_or_lt 8
  4. L332
    apply le_eq_or_lt
  5. L333
    exact hbound_8
129Separate the logical casesL334–335

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

  1. L334
    cases hsplit_8
  2. L335
    exfalso
130Use earlier factsL336–339

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

  1. L336
    specialize fixed_nontrivial_factor_not_prime p
  2. L337
    specialize fixed_nontrivial_factor_not_prime 2
  3. L338
    specialize fixed_nontrivial_factor_not_prime 4
  4. L339
    apply fixed_nontrivial_factor_not_prime
131Calculate and transport equalitiesL340–340

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

  1. L340
    trans 8
132Use earlier factsL341–341

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

  1. L341
    exact hsplit_8_left
133Calculate and transport equalitiesL342–342

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

  1. L342
    norm_num
134Fix variables and assumptionsL343–343

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

  1. L343
    intro hleft_one
135Use earlier factsL344–346

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

  1. L344
    apply PA1
  2. L345
    apply PA2
  3. L346
    exact hleft_one
136Fix variables and assumptionsL347–347

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

  1. L347
    intro hright_one
137Use earlier factsL348–351

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

  1. L348
    apply PA1
  2. L349
    apply PA2
  3. L350
    exact hright_one
  4. L351
    exact hp
138Establish hbound_7L352–354

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

  1. L352
    have hbound_7 : exists k. k + p = 7
  2. L353
    apply le_of_succ_le_succ
  3. L354
    exact hsplit_8_right
139Establish hsplit_7L355–359

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

  1. L355
    have hsplit_7 : p = 7 \/ (exists k. k + S p = 7)
  2. L356
    specialize le_eq_or_lt p
  3. L357
    specialize le_eq_or_lt 7
  4. L358
    apply le_eq_or_lt
  5. L359
    exact hbound_7
140Separate the logical casesL360–364

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

  1. L360
    cases hsplit_7
  2. L361
    right
  3. L362
    right
  4. L363
    right
  5. L364
    left
141Use earlier factsL365–365

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

  1. L365
    exact hsplit_7_left
142Establish hbound_6L366–368

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

  1. L366
    have hbound_6 : exists k. k + p = 6
  2. L367
    apply le_of_succ_le_succ
  3. L368
    exact hsplit_7_right
143Establish hsplit_6L369–373

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

  1. L369
    have hsplit_6 : p = 6 \/ (exists k. k + S p = 6)
  2. L370
    specialize le_eq_or_lt p
  3. L371
    specialize le_eq_or_lt 6
  4. L372
    apply le_eq_or_lt
  5. L373
    exact hbound_6
144Separate the logical casesL374–375

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

  1. L374
    cases hsplit_6
  2. L375
    exfalso
145Use earlier factsL376–379

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

  1. L376
    specialize fixed_nontrivial_factor_not_prime p
  2. L377
    specialize fixed_nontrivial_factor_not_prime 2
  3. L378
    specialize fixed_nontrivial_factor_not_prime 3
  4. L379
    apply fixed_nontrivial_factor_not_prime
146Calculate and transport equalitiesL380–380

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

  1. L380
    trans 6
147Use earlier factsL381–381

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

  1. L381
    exact hsplit_6_left
148Calculate and transport equalitiesL382–382

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

  1. L382
    norm_num
149Fix variables and assumptionsL383–383

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

  1. L383
    intro hleft_one
150Use earlier factsL384–386

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

  1. L384
    apply PA1
  2. L385
    apply PA2
  3. L386
    exact hleft_one
151Fix variables and assumptionsL387–387

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

  1. L387
    intro hright_one
152Use earlier factsL388–391

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

  1. L388
    apply PA1
  2. L389
    apply PA2
  3. L390
    exact hright_one
  4. L391
    exact hp
153Establish hbound_5L392–394

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

  1. L392
    have hbound_5 : exists k. k + p = 5
  2. L393
    apply le_of_succ_le_succ
  3. L394
    exact hsplit_6_right
154Establish hsplit_5L395–399

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

  1. L395
    have hsplit_5 : p = 5 \/ (exists k. k + S p = 5)
  2. L396
    specialize le_eq_or_lt p
  3. L397
    specialize le_eq_or_lt 5
  4. L398
    apply le_eq_or_lt
  5. L399
    exact hbound_5
155Separate the logical casesL400–403

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

  1. L400
    cases hsplit_5
  2. L401
    right
  3. L402
    right
  4. L403
    left
156Use earlier factsL404–404

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

  1. L404
    exact hsplit_5_left
157Establish hbound_4L405–407

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

  1. L405
    have hbound_4 : exists k. k + p = 4
  2. L406
    apply le_of_succ_le_succ
  3. L407
    exact hsplit_5_right
158Establish hsplit_4L408–412

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

  1. L408
    have hsplit_4 : p = 4 \/ (exists k. k + S p = 4)
  2. L409
    specialize le_eq_or_lt p
  3. L410
    specialize le_eq_or_lt 4
  4. L411
    apply le_eq_or_lt
  5. L412
    exact hbound_4
159Separate the logical casesL413–414

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

  1. L413
    cases hsplit_4
  2. L414
    exfalso
160Use earlier factsL415–418

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

  1. L415
    specialize fixed_nontrivial_factor_not_prime p
  2. L416
    specialize fixed_nontrivial_factor_not_prime 2
  3. L417
    specialize fixed_nontrivial_factor_not_prime 2
  4. L418
    apply fixed_nontrivial_factor_not_prime
161Calculate and transport equalitiesL419–419

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

  1. L419
    trans 4
162Use earlier factsL420–420

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

  1. L420
    exact hsplit_4_left
163Calculate and transport equalitiesL421–421

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

  1. L421
    norm_num
164Fix variables and assumptionsL422–422

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

  1. L422
    intro hleft_one
165Use earlier factsL423–425

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

  1. L423
    apply PA1
  2. L424
    apply PA2
  3. L425
    exact hleft_one
166Fix variables and assumptionsL426–426

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

  1. L426
    intro hright_one
167Use earlier factsL427–430

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

  1. L427
    apply PA1
  2. L428
    apply PA2
  3. L429
    exact hright_one
  4. L430
    exact hp
168Establish hbound_3L431–433

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

  1. L431
    have hbound_3 : exists k. k + p = 3
  2. L432
    apply le_of_succ_le_succ
  3. L433
    exact hsplit_4_right
169Establish hsplit_3L434–438

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

  1. L434
    have hsplit_3 : p = 3 \/ (exists k. k + S p = 3)
  2. L435
    specialize le_eq_or_lt p
  3. L436
    specialize le_eq_or_lt 3
  4. L437
    apply le_eq_or_lt
  5. L438
    exact hbound_3
170Separate the logical casesL439–441

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

  1. L439
    cases hsplit_3
  2. L440
    right
  3. L441
    left
171Use earlier factsL442–442

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

  1. L442
    exact hsplit_3_left
172Establish hbound_2L443–445

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

  1. L443
    have hbound_2 : exists k. k + p = 2
  2. L444
    apply le_of_succ_le_succ
  3. L445
    exact hsplit_3_right
173Establish hsplit_2L446–450

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

  1. L446
    have hsplit_2 : p = 2 \/ (exists k. k + S p = 2)
  2. L447
    specialize le_eq_or_lt p
  3. L448
    specialize le_eq_or_lt 2
  4. L449
    apply le_eq_or_lt
  5. L450
    exact hbound_2
174Separate the logical casesL451–452

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

  1. L451
    cases hsplit_2
  2. L452
    left
175Use earlier factsL453–453

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

  1. L453
    exact hsplit_2_left
176Establish hshapeL454–457

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

  1. L454
    have hshape : exists k. p = S (S k)
  2. L455
    specialize prime_is_succ_succ p
  3. L456
    apply prime_is_succ_succ
  4. L457
    exact hp
177Separate the logical casesL458–458

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

  1. L458
    cases hshape
178Establish htwoL459–459

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

  1. L459
    have htwo : exists k. k + 2 = p
179Construct an explicit witnessL460–460

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

  1. L460
    exists x
180Calculate and transport equalitiesL461–466

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

  1. L461
    trans S (S x)
  2. L462
    rewrite PA4
  3. L463
    rewrite PA4
  4. L464
    rewrite PA3
  5. L465
    refl
  6. L466
    symm
181Use earlier factsL467–467

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

  1. L467
    exact hshape_witness
182Separate the logical casesL468–468

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

  1. L468
    exfalso
183Use earlier factsL469–473

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

  1. L469
    specialize lt_not_le p
  2. L470
    specialize lt_not_le 2
  3. L471
    apply lt_not_le
  4. L472
    exact hsplit_2_right
  5. L473
    exact htwo

Library-wide reading audit

Original exact command ledger · 473 lines
  1. 0001intro p
  2. 0002intro hp
  3. 0003intro hbound
  4. 0004have hsplit_22 : p = 22 \/ (exists k. k + S p = 22)
  5. 0005specialize le_eq_or_lt p
  6. 0006specialize le_eq_or_lt 22
  7. 0007apply le_eq_or_lt
  8. 0008exact hbound
  9. 0009cases hsplit_22
  10. 0010exfalso
  11. 0011specialize fixed_nontrivial_factor_not_prime p
  12. 0012specialize fixed_nontrivial_factor_not_prime 2
  13. 0013specialize fixed_nontrivial_factor_not_prime 11
  14. 0014apply fixed_nontrivial_factor_not_prime
  15. 0015trans 22
  16. 0016exact hsplit_22_left
  17. 0017norm_num
  18. 0018intro hleft_one
  19. 0019apply PA1
  20. 0020apply PA2
  21. 0021exact hleft_one
  22. 0022intro hright_one
  23. 0023apply PA1
  24. 0024apply PA2
  25. 0025exact hright_one
  26. 0026exact hp
  27. 0027have hbound_21 : exists k. k + p = 21
  28. 0028apply le_of_succ_le_succ
  29. 0029exact hsplit_22_right
  30. 0030have hsplit_21 : p = 21 \/ (exists k. k + S p = 21)
  31. 0031specialize le_eq_or_lt p
  32. 0032specialize le_eq_or_lt 21
  33. 0033apply le_eq_or_lt
  34. 0034exact hbound_21
  35. 0035cases hsplit_21
  36. 0036exfalso
  37. 0037specialize fixed_nontrivial_factor_not_prime p
  38. 0038specialize fixed_nontrivial_factor_not_prime 3
  39. 0039specialize fixed_nontrivial_factor_not_prime 7
  40. 0040apply fixed_nontrivial_factor_not_prime
  41. 0041trans 21
  42. 0042exact hsplit_21_left
  43. 0043norm_num
  44. 0044intro hleft_one
  45. 0045apply PA1
  46. 0046apply PA2
  47. 0047exact hleft_one
  48. 0048intro hright_one
  49. 0049apply PA1
  50. 0050apply PA2
  51. 0051exact hright_one
  52. 0052exact hp
  53. 0053have hbound_20 : exists k. k + p = 20
  54. 0054apply le_of_succ_le_succ
  55. 0055exact hsplit_21_right
  56. 0056have hsplit_20 : p = 20 \/ (exists k. k + S p = 20)
  57. 0057specialize le_eq_or_lt p
  58. 0058specialize le_eq_or_lt 20
  59. 0059apply le_eq_or_lt
  60. 0060exact hbound_20
  61. 0061cases hsplit_20
  62. 0062exfalso
  63. 0063specialize fixed_nontrivial_factor_not_prime p
  64. 0064specialize fixed_nontrivial_factor_not_prime 4
  65. 0065specialize fixed_nontrivial_factor_not_prime 5
  66. 0066apply fixed_nontrivial_factor_not_prime
  67. 0067trans 20
  68. 0068exact hsplit_20_left
  69. 0069norm_num
  70. 0070intro hleft_one
  71. 0071apply PA1
  72. 0072apply PA2
  73. 0073exact hleft_one
  74. 0074intro hright_one
  75. 0075apply PA1
  76. 0076apply PA2
  77. 0077exact hright_one
  78. 0078exact hp
  79. 0079have hbound_19 : exists k. k + p = 19
  80. 0080apply le_of_succ_le_succ
  81. 0081exact hsplit_20_right
  82. 0082have hsplit_19 : p = 19 \/ (exists k. k + S p = 19)
  83. 0083specialize le_eq_or_lt p
  84. 0084specialize le_eq_or_lt 19
  85. 0085apply le_eq_or_lt
  86. 0086exact hbound_19
  87. 0087cases hsplit_19
  88. 0088right
  89. 0089right
  90. 0090right
  91. 0091right
  92. 0092right
  93. 0093right
  94. 0094right
  95. 0095exact hsplit_19_left
  96. 0096have hbound_18 : exists k. k + p = 18
  97. 0097apply le_of_succ_le_succ
  98. 0098exact hsplit_19_right
  99. 0099have hsplit_18 : p = 18 \/ (exists k. k + S p = 18)
  100. 0100specialize le_eq_or_lt p
  101. 0101specialize le_eq_or_lt 18
  102. 0102apply le_eq_or_lt
  103. 0103exact hbound_18
  104. 0104cases hsplit_18
  105. 0105exfalso
  106. 0106specialize fixed_nontrivial_factor_not_prime p
  107. 0107specialize fixed_nontrivial_factor_not_prime 3
  108. 0108specialize fixed_nontrivial_factor_not_prime 6
  109. 0109apply fixed_nontrivial_factor_not_prime
  110. 0110trans 18
  111. 0111exact hsplit_18_left
  112. 0112norm_num
  113. 0113intro hleft_one
  114. 0114apply PA1
  115. 0115apply PA2
  116. 0116exact hleft_one
  117. 0117intro hright_one
  118. 0118apply PA1
  119. 0119apply PA2
  120. 0120exact hright_one
  121. 0121exact hp
  122. 0122have hbound_17 : exists k. k + p = 17
  123. 0123apply le_of_succ_le_succ
  124. 0124exact hsplit_18_right
  125. 0125have hsplit_17 : p = 17 \/ (exists k. k + S p = 17)
  126. 0126specialize le_eq_or_lt p
  127. 0127specialize le_eq_or_lt 17
  128. 0128apply le_eq_or_lt
  129. 0129exact hbound_17
  130. 0130cases hsplit_17
  131. 0131right
  132. 0132right
  133. 0133right
  134. 0134right
  135. 0135right
  136. 0136right
  137. 0137left
  138. 0138exact hsplit_17_left
  139. 0139have hbound_16 : exists k. k + p = 16
  140. 0140apply le_of_succ_le_succ
  141. 0141exact hsplit_17_right
  142. 0142have hsplit_16 : p = 16 \/ (exists k. k + S p = 16)
  143. 0143specialize le_eq_or_lt p
  144. 0144specialize le_eq_or_lt 16
  145. 0145apply le_eq_or_lt
  146. 0146exact hbound_16
  147. 0147cases hsplit_16
  148. 0148exfalso
  149. 0149specialize fixed_nontrivial_factor_not_prime p
  150. 0150specialize fixed_nontrivial_factor_not_prime 4
  151. 0151specialize fixed_nontrivial_factor_not_prime 4
  152. 0152apply fixed_nontrivial_factor_not_prime
  153. 0153trans 16
  154. 0154exact hsplit_16_left
  155. 0155norm_num
  156. 0156intro hleft_one
  157. 0157apply PA1
  158. 0158apply PA2
  159. 0159exact hleft_one
  160. 0160intro hright_one
  161. 0161apply PA1
  162. 0162apply PA2
  163. 0163exact hright_one
  164. 0164exact hp
  165. 0165have hbound_15 : exists k. k + p = 15
  166. 0166apply le_of_succ_le_succ
  167. 0167exact hsplit_16_right
  168. 0168have hsplit_15 : p = 15 \/ (exists k. k + S p = 15)
  169. 0169specialize le_eq_or_lt p
  170. 0170specialize le_eq_or_lt 15
  171. 0171apply le_eq_or_lt
  172. 0172exact hbound_15
  173. 0173cases hsplit_15
  174. 0174exfalso
  175. 0175specialize fixed_nontrivial_factor_not_prime p
  176. 0176specialize fixed_nontrivial_factor_not_prime 3
  177. 0177specialize fixed_nontrivial_factor_not_prime 5
  178. 0178apply fixed_nontrivial_factor_not_prime
  179. 0179trans 15
  180. 0180exact hsplit_15_left
  181. 0181norm_num
  182. 0182intro hleft_one
  183. 0183apply PA1
  184. 0184apply PA2
  185. 0185exact hleft_one
  186. 0186intro hright_one
  187. 0187apply PA1
  188. 0188apply PA2
  189. 0189exact hright_one
  190. 0190exact hp
  191. 0191have hbound_14 : exists k. k + p = 14
  192. 0192apply le_of_succ_le_succ
  193. 0193exact hsplit_15_right
  194. 0194have hsplit_14 : p = 14 \/ (exists k. k + S p = 14)
  195. 0195specialize le_eq_or_lt p
  196. 0196specialize le_eq_or_lt 14
  197. 0197apply le_eq_or_lt
  198. 0198exact hbound_14
  199. 0199cases hsplit_14
  200. 0200exfalso
  201. 0201specialize fixed_nontrivial_factor_not_prime p
  202. 0202specialize fixed_nontrivial_factor_not_prime 2
  203. 0203specialize fixed_nontrivial_factor_not_prime 7
  204. 0204apply fixed_nontrivial_factor_not_prime
  205. 0205trans 14
  206. 0206exact hsplit_14_left
  207. 0207norm_num
  208. 0208intro hleft_one
  209. 0209apply PA1
  210. 0210apply PA2
  211. 0211exact hleft_one
  212. 0212intro hright_one
  213. 0213apply PA1
  214. 0214apply PA2
  215. 0215exact hright_one
  216. 0216exact hp
  217. 0217have hbound_13 : exists k. k + p = 13
  218. 0218apply le_of_succ_le_succ
  219. 0219exact hsplit_14_right
  220. 0220have hsplit_13 : p = 13 \/ (exists k. k + S p = 13)
  221. 0221specialize le_eq_or_lt p
  222. 0222specialize le_eq_or_lt 13
  223. 0223apply le_eq_or_lt
  224. 0224exact hbound_13
  225. 0225cases hsplit_13
  226. 0226right
  227. 0227right
  228. 0228right
  229. 0229right
  230. 0230right
  231. 0231left
  232. 0232exact hsplit_13_left
  233. 0233have hbound_12 : exists k. k + p = 12
  234. 0234apply le_of_succ_le_succ
  235. 0235exact hsplit_13_right
  236. 0236have hsplit_12 : p = 12 \/ (exists k. k + S p = 12)
  237. 0237specialize le_eq_or_lt p
  238. 0238specialize le_eq_or_lt 12
  239. 0239apply le_eq_or_lt
  240. 0240exact hbound_12
  241. 0241cases hsplit_12
  242. 0242exfalso
  243. 0243specialize fixed_nontrivial_factor_not_prime p
  244. 0244specialize fixed_nontrivial_factor_not_prime 3
  245. 0245specialize fixed_nontrivial_factor_not_prime 4
  246. 0246apply fixed_nontrivial_factor_not_prime
  247. 0247trans 12
  248. 0248exact hsplit_12_left
  249. 0249norm_num
  250. 0250intro hleft_one
  251. 0251apply PA1
  252. 0252apply PA2
  253. 0253exact hleft_one
  254. 0254intro hright_one
  255. 0255apply PA1
  256. 0256apply PA2
  257. 0257exact hright_one
  258. 0258exact hp
  259. 0259have hbound_11 : exists k. k + p = 11
  260. 0260apply le_of_succ_le_succ
  261. 0261exact hsplit_12_right
  262. 0262have hsplit_11 : p = 11 \/ (exists k. k + S p = 11)
  263. 0263specialize le_eq_or_lt p
  264. 0264specialize le_eq_or_lt 11
  265. 0265apply le_eq_or_lt
  266. 0266exact hbound_11
  267. 0267cases hsplit_11
  268. 0268right
  269. 0269right
  270. 0270right
  271. 0271right
  272. 0272left
  273. 0273exact hsplit_11_left
  274. 0274have hbound_10 : exists k. k + p = 10
  275. 0275apply le_of_succ_le_succ
  276. 0276exact hsplit_11_right
  277. 0277have hsplit_10 : p = 10 \/ (exists k. k + S p = 10)
  278. 0278specialize le_eq_or_lt p
  279. 0279specialize le_eq_or_lt 10
  280. 0280apply le_eq_or_lt
  281. 0281exact hbound_10
  282. 0282cases hsplit_10
  283. 0283exfalso
  284. 0284specialize fixed_nontrivial_factor_not_prime p
  285. 0285specialize fixed_nontrivial_factor_not_prime 2
  286. 0286specialize fixed_nontrivial_factor_not_prime 5
  287. 0287apply fixed_nontrivial_factor_not_prime
  288. 0288trans 10
  289. 0289exact hsplit_10_left
  290. 0290norm_num
  291. 0291intro hleft_one
  292. 0292apply PA1
  293. 0293apply PA2
  294. 0294exact hleft_one
  295. 0295intro hright_one
  296. 0296apply PA1
  297. 0297apply PA2
  298. 0298exact hright_one
  299. 0299exact hp
  300. 0300have hbound_9 : exists k. k + p = 9
  301. 0301apply le_of_succ_le_succ
  302. 0302exact hsplit_10_right
  303. 0303have hsplit_9 : p = 9 \/ (exists k. k + S p = 9)
  304. 0304specialize le_eq_or_lt p
  305. 0305specialize le_eq_or_lt 9
  306. 0306apply le_eq_or_lt
  307. 0307exact hbound_9
  308. 0308cases hsplit_9
  309. 0309exfalso
  310. 0310specialize fixed_nontrivial_factor_not_prime p
  311. 0311specialize fixed_nontrivial_factor_not_prime 3
  312. 0312specialize fixed_nontrivial_factor_not_prime 3
  313. 0313apply fixed_nontrivial_factor_not_prime
  314. 0314trans 9
  315. 0315exact hsplit_9_left
  316. 0316norm_num
  317. 0317intro hleft_one
  318. 0318apply PA1
  319. 0319apply PA2
  320. 0320exact hleft_one
  321. 0321intro hright_one
  322. 0322apply PA1
  323. 0323apply PA2
  324. 0324exact hright_one
  325. 0325exact hp
  326. 0326have hbound_8 : exists k. k + p = 8
  327. 0327apply le_of_succ_le_succ
  328. 0328exact hsplit_9_right
  329. 0329have hsplit_8 : p = 8 \/ (exists k. k + S p = 8)
  330. 0330specialize le_eq_or_lt p
  331. 0331specialize le_eq_or_lt 8
  332. 0332apply le_eq_or_lt
  333. 0333exact hbound_8
  334. 0334cases hsplit_8
  335. 0335exfalso
  336. 0336specialize fixed_nontrivial_factor_not_prime p
  337. 0337specialize fixed_nontrivial_factor_not_prime 2
  338. 0338specialize fixed_nontrivial_factor_not_prime 4
  339. 0339apply fixed_nontrivial_factor_not_prime
  340. 0340trans 8
  341. 0341exact hsplit_8_left
  342. 0342norm_num
  343. 0343intro hleft_one
  344. 0344apply PA1
  345. 0345apply PA2
  346. 0346exact hleft_one
  347. 0347intro hright_one
  348. 0348apply PA1
  349. 0349apply PA2
  350. 0350exact hright_one
  351. 0351exact hp
  352. 0352have hbound_7 : exists k. k + p = 7
  353. 0353apply le_of_succ_le_succ
  354. 0354exact hsplit_8_right
  355. 0355have hsplit_7 : p = 7 \/ (exists k. k + S p = 7)
  356. 0356specialize le_eq_or_lt p
  357. 0357specialize le_eq_or_lt 7
  358. 0358apply le_eq_or_lt
  359. 0359exact hbound_7
  360. 0360cases hsplit_7
  361. 0361right
  362. 0362right
  363. 0363right
  364. 0364left
  365. 0365exact hsplit_7_left
  366. 0366have hbound_6 : exists k. k + p = 6
  367. 0367apply le_of_succ_le_succ
  368. 0368exact hsplit_7_right
  369. 0369have hsplit_6 : p = 6 \/ (exists k. k + S p = 6)
  370. 0370specialize le_eq_or_lt p
  371. 0371specialize le_eq_or_lt 6
  372. 0372apply le_eq_or_lt
  373. 0373exact hbound_6
  374. 0374cases hsplit_6
  375. 0375exfalso
  376. 0376specialize fixed_nontrivial_factor_not_prime p
  377. 0377specialize fixed_nontrivial_factor_not_prime 2
  378. 0378specialize fixed_nontrivial_factor_not_prime 3
  379. 0379apply fixed_nontrivial_factor_not_prime
  380. 0380trans 6
  381. 0381exact hsplit_6_left
  382. 0382norm_num
  383. 0383intro hleft_one
  384. 0384apply PA1
  385. 0385apply PA2
  386. 0386exact hleft_one
  387. 0387intro hright_one
  388. 0388apply PA1
  389. 0389apply PA2
  390. 0390exact hright_one
  391. 0391exact hp
  392. 0392have hbound_5 : exists k. k + p = 5
  393. 0393apply le_of_succ_le_succ
  394. 0394exact hsplit_6_right
  395. 0395have hsplit_5 : p = 5 \/ (exists k. k + S p = 5)
  396. 0396specialize le_eq_or_lt p
  397. 0397specialize le_eq_or_lt 5
  398. 0398apply le_eq_or_lt
  399. 0399exact hbound_5
  400. 0400cases hsplit_5
  401. 0401right
  402. 0402right
  403. 0403left
  404. 0404exact hsplit_5_left
  405. 0405have hbound_4 : exists k. k + p = 4
  406. 0406apply le_of_succ_le_succ
  407. 0407exact hsplit_5_right
  408. 0408have hsplit_4 : p = 4 \/ (exists k. k + S p = 4)
  409. 0409specialize le_eq_or_lt p
  410. 0410specialize le_eq_or_lt 4
  411. 0411apply le_eq_or_lt
  412. 0412exact hbound_4
  413. 0413cases hsplit_4
  414. 0414exfalso
  415. 0415specialize fixed_nontrivial_factor_not_prime p
  416. 0416specialize fixed_nontrivial_factor_not_prime 2
  417. 0417specialize fixed_nontrivial_factor_not_prime 2
  418. 0418apply fixed_nontrivial_factor_not_prime
  419. 0419trans 4
  420. 0420exact hsplit_4_left
  421. 0421norm_num
  422. 0422intro hleft_one
  423. 0423apply PA1
  424. 0424apply PA2
  425. 0425exact hleft_one
  426. 0426intro hright_one
  427. 0427apply PA1
  428. 0428apply PA2
  429. 0429exact hright_one
  430. 0430exact hp
  431. 0431have hbound_3 : exists k. k + p = 3
  432. 0432apply le_of_succ_le_succ
  433. 0433exact hsplit_4_right
  434. 0434have hsplit_3 : p = 3 \/ (exists k. k + S p = 3)
  435. 0435specialize le_eq_or_lt p
  436. 0436specialize le_eq_or_lt 3
  437. 0437apply le_eq_or_lt
  438. 0438exact hbound_3
  439. 0439cases hsplit_3
  440. 0440right
  441. 0441left
  442. 0442exact hsplit_3_left
  443. 0443have hbound_2 : exists k. k + p = 2
  444. 0444apply le_of_succ_le_succ
  445. 0445exact hsplit_3_right
  446. 0446have hsplit_2 : p = 2 \/ (exists k. k + S p = 2)
  447. 0447specialize le_eq_or_lt p
  448. 0448specialize le_eq_or_lt 2
  449. 0449apply le_eq_or_lt
  450. 0450exact hbound_2
  451. 0451cases hsplit_2
  452. 0452left
  453. 0453exact hsplit_2_left
  454. 0454have hshape : exists k. p = S (S k)
  455. 0455specialize prime_is_succ_succ p
  456. 0456apply prime_is_succ_succ
  457. 0457exact hp
  458. 0458cases hshape
  459. 0459have htwo : exists k. k + 2 = p
  460. 0460exists x
  461. 0461trans S (S x)
  462. 0462rewrite PA4
  463. 0463rewrite PA4
  464. 0464rewrite PA3
  465. 0465refl
  466. 0466symm
  467. 0467exact hshape_witness
  468. 0468exfalso
  469. 0469specialize lt_not_le p
  470. 0470specialize lt_not_le 2
  471. 0471apply lt_not_le
  472. 0472exact hsplit_2_right
  473. 0473exact htwo