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
∀ p. Prime(p) → Le(p,22) → p = 2 ∨ (p = 3 ∨ (p = 5 ∨ (p = 7 ∨ (p = 11 ∨ (p = 13 ∨ (p = 17 ∨ p = 19))))))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
2 occurrences
In local proof propositions
42 occurrences
Exact expanded native-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))))))))Proof neighborhood
Direct theorem prerequisites
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_primeDirect theorem dependents
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
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)
01Fix variables and assumptionsL1–3
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.
03Separate the logical casesL9–10
04Use earlier factsL11–14
05Calculate and transport equalitiesL15–15
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L15
trans 22
06Use earlier factsL16–16
Instantiate or apply named facts and discharge the corresponding proof obligations.
- 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.
- L17
norm_num
08Fix variables and assumptionsL18–18
Work with arbitrary variables or the premises of the current implication.
- L18
intro hleft_one
09Use earlier factsL19–21
10Fix variables and assumptionsL22–22
Work with arbitrary variables or the premises of the current implication.
- L22
intro hright_one
11Use earlier factsL23–26
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.
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.
14Separate the logical casesL35–36
15Use earlier factsL37–40
16Calculate and transport equalitiesL41–41
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L41
trans 21
17Use earlier factsL42–42
Instantiate or apply named facts and discharge the corresponding proof obligations.
- 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.
- L43
norm_num
19Fix variables and assumptionsL44–44
Work with arbitrary variables or the premises of the current implication.
- L44
intro hleft_one
20Use earlier factsL45–47
21Fix variables and assumptionsL48–48
Work with arbitrary variables or the premises of the current implication.
- L48
intro hright_one
22Use earlier factsL49–52
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.
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.
25Separate the logical casesL61–62
26Use earlier factsL63–66
27Calculate and transport equalitiesL67–67
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L67
trans 20
28Use earlier factsL68–68
Instantiate or apply named facts and discharge the corresponding proof obligations.
- 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.
- L69
norm_num
30Fix variables and assumptionsL70–70
Work with arbitrary variables or the premises of the current implication.
- L70
intro hleft_one
31Use earlier factsL71–73
32Fix variables and assumptionsL74–74
Work with arbitrary variables or the premises of the current implication.
- L74
intro hright_one
33Use earlier factsL75–78
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.
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.
36Separate the logical casesL87–94
37Use earlier factsL95–95
Instantiate or apply named facts and discharge the corresponding proof obligations.
- 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.
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.
40Separate the logical casesL104–105
41Use earlier factsL106–109
42Calculate and transport equalitiesL110–110
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L110
trans 18
43Use earlier factsL111–111
Instantiate or apply named facts and discharge the corresponding proof obligations.
- 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.
- L112
norm_num
45Fix variables and assumptionsL113–113
Work with arbitrary variables or the premises of the current implication.
- L113
intro hleft_one
46Use earlier factsL114–116
47Fix variables and assumptionsL117–117
Work with arbitrary variables or the premises of the current implication.
- L117
intro hright_one
48Use earlier factsL118–121
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.
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.
51Separate the logical casesL130–137
52Use earlier factsL138–138
Instantiate or apply named facts and discharge the corresponding proof obligations.
- 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.
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.
55Separate the logical casesL147–148
56Use earlier factsL149–152
57Calculate and transport equalitiesL153–153
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L153
trans 16
58Use earlier factsL154–154
Instantiate or apply named facts and discharge the corresponding proof obligations.
- 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.
- L155
norm_num
60Fix variables and assumptionsL156–156
Work with arbitrary variables or the premises of the current implication.
- L156
intro hleft_one
61Use earlier factsL157–159
62Fix variables and assumptionsL160–160
Work with arbitrary variables or the premises of the current implication.
- L160
intro hright_one
63Use earlier factsL161–164
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.
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.
66Separate the logical casesL173–174
67Use earlier factsL175–178
68Calculate and transport equalitiesL179–179
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L179
trans 15
69Use earlier factsL180–180
Instantiate or apply named facts and discharge the corresponding proof obligations.
- 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.
- L181
norm_num
71Fix variables and assumptionsL182–182
Work with arbitrary variables or the premises of the current implication.
- L182
intro hleft_one
72Use earlier factsL183–185
73Fix variables and assumptionsL186–186
Work with arbitrary variables or the premises of the current implication.
- L186
intro hright_one
74Use earlier factsL187–190
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.
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.
77Separate the logical casesL199–200
78Use earlier factsL201–204
79Calculate and transport equalitiesL205–205
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L205
trans 14
80Use earlier factsL206–206
Instantiate or apply named facts and discharge the corresponding proof obligations.
- 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.
- L207
norm_num
82Fix variables and assumptionsL208–208
Work with arbitrary variables or the premises of the current implication.
- L208
intro hleft_one
83Use earlier factsL209–211
84Fix variables and assumptionsL212–212
Work with arbitrary variables or the premises of the current implication.
- L212
intro hright_one
85Use earlier factsL213–216
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.
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.
88Separate the logical casesL225–231
89Use earlier factsL232–232
Instantiate or apply named facts and discharge the corresponding proof obligations.
- 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.
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.
92Separate the logical casesL241–242
93Use earlier factsL243–246
94Calculate and transport equalitiesL247–247
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L247
trans 12
95Use earlier factsL248–248
Instantiate or apply named facts and discharge the corresponding proof obligations.
- 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.
- L249
norm_num
97Fix variables and assumptionsL250–250
Work with arbitrary variables or the premises of the current implication.
- L250
intro hleft_one
98Use earlier factsL251–253
99Fix variables and assumptionsL254–254
Work with arbitrary variables or the premises of the current implication.
- L254
intro hright_one
100Use earlier factsL255–258
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.
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.
103Separate the logical casesL267–272
104Use earlier factsL273–273
Instantiate or apply named facts and discharge the corresponding proof obligations.
- 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.
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.
107Separate the logical casesL282–283
108Use earlier factsL284–287
109Calculate and transport equalitiesL288–288
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L288
trans 10
110Use earlier factsL289–289
Instantiate or apply named facts and discharge the corresponding proof obligations.
- 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.
- L290
norm_num
112Fix variables and assumptionsL291–291
Work with arbitrary variables or the premises of the current implication.
- L291
intro hleft_one
113Use earlier factsL292–294
114Fix variables and assumptionsL295–295
Work with arbitrary variables or the premises of the current implication.
- L295
intro hright_one
115Use earlier factsL296–299
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.
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.
118Separate the logical casesL308–309
119Use earlier factsL310–313
120Calculate and transport equalitiesL314–314
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L314
trans 9
121Use earlier factsL315–315
Instantiate or apply named facts and discharge the corresponding proof obligations.
- 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.
- L316
norm_num
123Fix variables and assumptionsL317–317
Work with arbitrary variables or the premises of the current implication.
- L317
intro hleft_one
124Use earlier factsL318–320
125Fix variables and assumptionsL321–321
Work with arbitrary variables or the premises of the current implication.
- L321
intro hright_one
126Use earlier factsL322–325
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.
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.
129Separate the logical casesL334–335
130Use earlier factsL336–339
131Calculate and transport equalitiesL340–340
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L340
trans 8
132Use earlier factsL341–341
Instantiate or apply named facts and discharge the corresponding proof obligations.
- 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.
- L342
norm_num
134Fix variables and assumptionsL343–343
Work with arbitrary variables or the premises of the current implication.
- L343
intro hleft_one
135Use earlier factsL344–346
136Fix variables and assumptionsL347–347
Work with arbitrary variables or the premises of the current implication.
- L347
intro hright_one
137Use earlier factsL348–351
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.
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.
140Separate the logical casesL360–364
141Use earlier factsL365–365
Instantiate or apply named facts and discharge the corresponding proof obligations.
- 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.
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.
144Separate the logical casesL374–375
145Use earlier factsL376–379
146Calculate and transport equalitiesL380–380
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L380
trans 6
147Use earlier factsL381–381
Instantiate or apply named facts and discharge the corresponding proof obligations.
- 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.
- L382
norm_num
149Fix variables and assumptionsL383–383
Work with arbitrary variables or the premises of the current implication.
- L383
intro hleft_one
150Use earlier factsL384–386
151Fix variables and assumptionsL387–387
Work with arbitrary variables or the premises of the current implication.
- L387
intro hright_one
152Use earlier factsL388–391
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.
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.
155Separate the logical casesL400–403
156Use earlier factsL404–404
Instantiate or apply named facts and discharge the corresponding proof obligations.
- 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.
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.
159Separate the logical casesL413–414
160Use earlier factsL415–418
161Calculate and transport equalitiesL419–419
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L419
trans 4
162Use earlier factsL420–420
Instantiate or apply named facts and discharge the corresponding proof obligations.
- 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.
- L421
norm_num
164Fix variables and assumptionsL422–422
Work with arbitrary variables or the premises of the current implication.
- L422
intro hleft_one
165Use earlier factsL423–425
166Fix variables and assumptionsL426–426
Work with arbitrary variables or the premises of the current implication.
- L426
intro hright_one
167Use earlier factsL427–430
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.
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.
170Separate the logical casesL439–441
171Use earlier factsL442–442
Instantiate or apply named facts and discharge the corresponding proof obligations.
- 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.
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.
174Separate the logical casesL451–452
175Use earlier factsL453–453
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L453
exact hsplit_2_left
176Establish hshapeL454–457
177Separate the logical casesL458–458
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L458
cases hshape
178Establish htwoL459–459
Establish this local claim before using it. It is not an additional assumption.
179Construct an explicit witnessL460–460
Supply the displayed value, then prove that it has the required property.
- L460
exists x
180Calculate and transport equalitiesL461–466
181Use earlier factsL467–467
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L467
exact hshape_witness
182Separate the logical casesL468–468
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L468
exfalso
Original defined command ledger · 473 lines
- 0001
intro p - 0002
intro hp - 0003
intro hbound - 0004
have hsplit_22 : p = 22 ∨ Lt(p,22)Exact native replay line
have hsplit_22 : p = 22 \/ (exists k. k + S p = 22) - 0005
specialize le_eq_or_lt p - 0006
specialize le_eq_or_lt 22 - 0007
apply le_eq_or_lt - 0008
exact hbound - 0009
cases hsplit_22 - 0010
exfalso - 0011
specialize fixed_nontrivial_factor_not_prime p - 0012
specialize fixed_nontrivial_factor_not_prime 2 - 0013
specialize fixed_nontrivial_factor_not_prime 11 - 0014
apply fixed_nontrivial_factor_not_prime - 0015
trans 22 - 0016
exact hsplit_22_left - 0017
norm_num - 0018
intro hleft_one - 0019
apply PA1 - 0020
apply PA2 - 0021
exact hleft_one - 0022
intro hright_one - 0023
apply PA1 - 0024
apply PA2 - 0025
exact hright_one - 0026
exact hp - 0027
have hbound_21 : Le(p,21)Exact native replay line
have hbound_21 : exists k. k + p = 21 - 0028
apply le_of_succ_le_succ - 0029
exact hsplit_22_right - 0030
have hsplit_21 : p = 21 ∨ Lt(p,21)Exact native replay line
have hsplit_21 : p = 21 \/ (exists k. k + S p = 21) - 0031
specialize le_eq_or_lt p - 0032
specialize le_eq_or_lt 21 - 0033
apply le_eq_or_lt - 0034
exact hbound_21 - 0035
cases hsplit_21 - 0036
exfalso - 0037
specialize fixed_nontrivial_factor_not_prime p - 0038
specialize fixed_nontrivial_factor_not_prime 3 - 0039
specialize fixed_nontrivial_factor_not_prime 7 - 0040
apply fixed_nontrivial_factor_not_prime - 0041
trans 21 - 0042
exact hsplit_21_left - 0043
norm_num - 0044
intro hleft_one - 0045
apply PA1 - 0046
apply PA2 - 0047
exact hleft_one - 0048
intro hright_one - 0049
apply PA1 - 0050
apply PA2 - 0051
exact hright_one - 0052
exact hp - 0053
have hbound_20 : Le(p,20)Exact native replay line
have hbound_20 : exists k. k + p = 20 - 0054
apply le_of_succ_le_succ - 0055
exact hsplit_21_right - 0056
have hsplit_20 : p = 20 ∨ Lt(p,20)Exact native replay line
have hsplit_20 : p = 20 \/ (exists k. k + S p = 20) - 0057
specialize le_eq_or_lt p - 0058
specialize le_eq_or_lt 20 - 0059
apply le_eq_or_lt - 0060
exact hbound_20 - 0061
cases hsplit_20 - 0062
exfalso - 0063
specialize fixed_nontrivial_factor_not_prime p - 0064
specialize fixed_nontrivial_factor_not_prime 4 - 0065
specialize fixed_nontrivial_factor_not_prime 5 - 0066
apply fixed_nontrivial_factor_not_prime - 0067
trans 20 - 0068
exact hsplit_20_left - 0069
norm_num - 0070
intro hleft_one - 0071
apply PA1 - 0072
apply PA2 - 0073
exact hleft_one - 0074
intro hright_one - 0075
apply PA1 - 0076
apply PA2 - 0077
exact hright_one - 0078
exact hp - 0079
have hbound_19 : Le(p,19)Exact native replay line
have hbound_19 : exists k. k + p = 19 - 0080
apply le_of_succ_le_succ - 0081
exact hsplit_20_right - 0082
have hsplit_19 : p = 19 ∨ Lt(p,19)Exact native replay line
have hsplit_19 : p = 19 \/ (exists k. k + S p = 19) - 0083
specialize le_eq_or_lt p - 0084
specialize le_eq_or_lt 19 - 0085
apply le_eq_or_lt - 0086
exact hbound_19 - 0087
cases hsplit_19 - 0088
right - 0089
right - 0090
right - 0091
right - 0092
right - 0093
right - 0094
right - 0095
exact hsplit_19_left - 0096
have hbound_18 : Le(p,18)Exact native replay line
have hbound_18 : exists k. k + p = 18 - 0097
apply le_of_succ_le_succ - 0098
exact hsplit_19_right - 0099
have hsplit_18 : p = 18 ∨ Lt(p,18)Exact native replay line
have hsplit_18 : p = 18 \/ (exists k. k + S p = 18) - 0100
specialize le_eq_or_lt p - 0101
specialize le_eq_or_lt 18 - 0102
apply le_eq_or_lt - 0103
exact hbound_18 - 0104
cases hsplit_18 - 0105
exfalso - 0106
specialize fixed_nontrivial_factor_not_prime p - 0107
specialize fixed_nontrivial_factor_not_prime 3 - 0108
specialize fixed_nontrivial_factor_not_prime 6 - 0109
apply fixed_nontrivial_factor_not_prime - 0110
trans 18 - 0111
exact hsplit_18_left - 0112
norm_num - 0113
intro hleft_one - 0114
apply PA1 - 0115
apply PA2 - 0116
exact hleft_one - 0117
intro hright_one - 0118
apply PA1 - 0119
apply PA2 - 0120
exact hright_one - 0121
exact hp - 0122
have hbound_17 : Le(p,17)Exact native replay line
have hbound_17 : exists k. k + p = 17 - 0123
apply le_of_succ_le_succ - 0124
exact hsplit_18_right - 0125
have hsplit_17 : p = 17 ∨ Lt(p,17)Exact native replay line
have hsplit_17 : p = 17 \/ (exists k. k + S p = 17) - 0126
specialize le_eq_or_lt p - 0127
specialize le_eq_or_lt 17 - 0128
apply le_eq_or_lt - 0129
exact hbound_17 - 0130
cases hsplit_17 - 0131
right - 0132
right - 0133
right - 0134
right - 0135
right - 0136
right - 0137
left - 0138
exact hsplit_17_left - 0139
have hbound_16 : Le(p,16)Exact native replay line
have hbound_16 : exists k. k + p = 16 - 0140
apply le_of_succ_le_succ - 0141
exact hsplit_17_right - 0142
have hsplit_16 : p = 16 ∨ Lt(p,16)Exact native replay line
have hsplit_16 : p = 16 \/ (exists k. k + S p = 16) - 0143
specialize le_eq_or_lt p - 0144
specialize le_eq_or_lt 16 - 0145
apply le_eq_or_lt - 0146
exact hbound_16 - 0147
cases hsplit_16 - 0148
exfalso - 0149
specialize fixed_nontrivial_factor_not_prime p - 0150
specialize fixed_nontrivial_factor_not_prime 4 - 0151
specialize fixed_nontrivial_factor_not_prime 4 - 0152
apply fixed_nontrivial_factor_not_prime - 0153
trans 16 - 0154
exact hsplit_16_left - 0155
norm_num - 0156
intro hleft_one - 0157
apply PA1 - 0158
apply PA2 - 0159
exact hleft_one - 0160
intro hright_one - 0161
apply PA1 - 0162
apply PA2 - 0163
exact hright_one - 0164
exact hp - 0165
have hbound_15 : Le(p,15)Exact native replay line
have hbound_15 : exists k. k + p = 15 - 0166
apply le_of_succ_le_succ - 0167
exact hsplit_16_right - 0168
have hsplit_15 : p = 15 ∨ Lt(p,15)Exact native replay line
have hsplit_15 : p = 15 \/ (exists k. k + S p = 15) - 0169
specialize le_eq_or_lt p - 0170
specialize le_eq_or_lt 15 - 0171
apply le_eq_or_lt - 0172
exact hbound_15 - 0173
cases hsplit_15 - 0174
exfalso - 0175
specialize fixed_nontrivial_factor_not_prime p - 0176
specialize fixed_nontrivial_factor_not_prime 3 - 0177
specialize fixed_nontrivial_factor_not_prime 5 - 0178
apply fixed_nontrivial_factor_not_prime - 0179
trans 15 - 0180
exact hsplit_15_left - 0181
norm_num - 0182
intro hleft_one - 0183
apply PA1 - 0184
apply PA2 - 0185
exact hleft_one - 0186
intro hright_one - 0187
apply PA1 - 0188
apply PA2 - 0189
exact hright_one - 0190
exact hp - 0191
have hbound_14 : Le(p,14)Exact native replay line
have hbound_14 : exists k. k + p = 14 - 0192
apply le_of_succ_le_succ - 0193
exact hsplit_15_right - 0194
have hsplit_14 : p = 14 ∨ Lt(p,14)Exact native replay line
have hsplit_14 : p = 14 \/ (exists k. k + S p = 14) - 0195
specialize le_eq_or_lt p - 0196
specialize le_eq_or_lt 14 - 0197
apply le_eq_or_lt - 0198
exact hbound_14 - 0199
cases hsplit_14 - 0200
exfalso - 0201
specialize fixed_nontrivial_factor_not_prime p - 0202
specialize fixed_nontrivial_factor_not_prime 2 - 0203
specialize fixed_nontrivial_factor_not_prime 7 - 0204
apply fixed_nontrivial_factor_not_prime - 0205
trans 14 - 0206
exact hsplit_14_left - 0207
norm_num - 0208
intro hleft_one - 0209
apply PA1 - 0210
apply PA2 - 0211
exact hleft_one - 0212
intro hright_one - 0213
apply PA1 - 0214
apply PA2 - 0215
exact hright_one - 0216
exact hp - 0217
have hbound_13 : Le(p,13)Exact native replay line
have hbound_13 : exists k. k + p = 13 - 0218
apply le_of_succ_le_succ - 0219
exact hsplit_14_right - 0220
have hsplit_13 : p = 13 ∨ Lt(p,13)Exact native replay line
have hsplit_13 : p = 13 \/ (exists k. k + S p = 13) - 0221
specialize le_eq_or_lt p - 0222
specialize le_eq_or_lt 13 - 0223
apply le_eq_or_lt - 0224
exact hbound_13 - 0225
cases hsplit_13 - 0226
right - 0227
right - 0228
right - 0229
right - 0230
right - 0231
left - 0232
exact hsplit_13_left - 0233
have hbound_12 : Le(p,12)Exact native replay line
have hbound_12 : exists k. k + p = 12 - 0234
apply le_of_succ_le_succ - 0235
exact hsplit_13_right - 0236
have hsplit_12 : p = 12 ∨ Lt(p,12)Exact native replay line
have hsplit_12 : p = 12 \/ (exists k. k + S p = 12) - 0237
specialize le_eq_or_lt p - 0238
specialize le_eq_or_lt 12 - 0239
apply le_eq_or_lt - 0240
exact hbound_12 - 0241
cases hsplit_12 - 0242
exfalso - 0243
specialize fixed_nontrivial_factor_not_prime p - 0244
specialize fixed_nontrivial_factor_not_prime 3 - 0245
specialize fixed_nontrivial_factor_not_prime 4 - 0246
apply fixed_nontrivial_factor_not_prime - 0247
trans 12 - 0248
exact hsplit_12_left - 0249
norm_num - 0250
intro hleft_one - 0251
apply PA1 - 0252
apply PA2 - 0253
exact hleft_one - 0254
intro hright_one - 0255
apply PA1 - 0256
apply PA2 - 0257
exact hright_one - 0258
exact hp - 0259
have hbound_11 : Le(p,11)Exact native replay line
have hbound_11 : exists k. k + p = 11 - 0260
apply le_of_succ_le_succ - 0261
exact hsplit_12_right - 0262
have hsplit_11 : p = 11 ∨ Lt(p,11)Exact native replay line
have hsplit_11 : p = 11 \/ (exists k. k + S p = 11) - 0263
specialize le_eq_or_lt p - 0264
specialize le_eq_or_lt 11 - 0265
apply le_eq_or_lt - 0266
exact hbound_11 - 0267
cases hsplit_11 - 0268
right - 0269
right - 0270
right - 0271
right - 0272
left - 0273
exact hsplit_11_left - 0274
have hbound_10 : Le(p,10)Exact native replay line
have hbound_10 : exists k. k + p = 10 - 0275
apply le_of_succ_le_succ - 0276
exact hsplit_11_right - 0277
have hsplit_10 : p = 10 ∨ Lt(p,10)Exact native replay line
have hsplit_10 : p = 10 \/ (exists k. k + S p = 10) - 0278
specialize le_eq_or_lt p - 0279
specialize le_eq_or_lt 10 - 0280
apply le_eq_or_lt - 0281
exact hbound_10 - 0282
cases hsplit_10 - 0283
exfalso - 0284
specialize fixed_nontrivial_factor_not_prime p - 0285
specialize fixed_nontrivial_factor_not_prime 2 - 0286
specialize fixed_nontrivial_factor_not_prime 5 - 0287
apply fixed_nontrivial_factor_not_prime - 0288
trans 10 - 0289
exact hsplit_10_left - 0290
norm_num - 0291
intro hleft_one - 0292
apply PA1 - 0293
apply PA2 - 0294
exact hleft_one - 0295
intro hright_one - 0296
apply PA1 - 0297
apply PA2 - 0298
exact hright_one - 0299
exact hp - 0300
have hbound_9 : Le(p,9)Exact native replay line
have hbound_9 : exists k. k + p = 9 - 0301
apply le_of_succ_le_succ - 0302
exact hsplit_10_right - 0303
have hsplit_9 : p = 9 ∨ Lt(p,9)Exact native replay line
have hsplit_9 : p = 9 \/ (exists k. k + S p = 9) - 0304
specialize le_eq_or_lt p - 0305
specialize le_eq_or_lt 9 - 0306
apply le_eq_or_lt - 0307
exact hbound_9 - 0308
cases hsplit_9 - 0309
exfalso - 0310
specialize fixed_nontrivial_factor_not_prime p - 0311
specialize fixed_nontrivial_factor_not_prime 3 - 0312
specialize fixed_nontrivial_factor_not_prime 3 - 0313
apply fixed_nontrivial_factor_not_prime - 0314
trans 9 - 0315
exact hsplit_9_left - 0316
norm_num - 0317
intro hleft_one - 0318
apply PA1 - 0319
apply PA2 - 0320
exact hleft_one - 0321
intro hright_one - 0322
apply PA1 - 0323
apply PA2 - 0324
exact hright_one - 0325
exact hp - 0326
have hbound_8 : Le(p,8)Exact native replay line
have hbound_8 : exists k. k + p = 8 - 0327
apply le_of_succ_le_succ - 0328
exact hsplit_9_right - 0329
have hsplit_8 : p = 8 ∨ Lt(p,8)Exact native replay line
have hsplit_8 : p = 8 \/ (exists k. k + S p = 8) - 0330
specialize le_eq_or_lt p - 0331
specialize le_eq_or_lt 8 - 0332
apply le_eq_or_lt - 0333
exact hbound_8 - 0334
cases hsplit_8 - 0335
exfalso - 0336
specialize fixed_nontrivial_factor_not_prime p - 0337
specialize fixed_nontrivial_factor_not_prime 2 - 0338
specialize fixed_nontrivial_factor_not_prime 4 - 0339
apply fixed_nontrivial_factor_not_prime - 0340
trans 8 - 0341
exact hsplit_8_left - 0342
norm_num - 0343
intro hleft_one - 0344
apply PA1 - 0345
apply PA2 - 0346
exact hleft_one - 0347
intro hright_one - 0348
apply PA1 - 0349
apply PA2 - 0350
exact hright_one - 0351
exact hp - 0352
have hbound_7 : Le(p,7)Exact native replay line
have hbound_7 : exists k. k + p = 7 - 0353
apply le_of_succ_le_succ - 0354
exact hsplit_8_right - 0355
have hsplit_7 : p = 7 ∨ Lt(p,7)Exact native replay line
have hsplit_7 : p = 7 \/ (exists k. k + S p = 7) - 0356
specialize le_eq_or_lt p - 0357
specialize le_eq_or_lt 7 - 0358
apply le_eq_or_lt - 0359
exact hbound_7 - 0360
cases hsplit_7 - 0361
right - 0362
right - 0363
right - 0364
left - 0365
exact hsplit_7_left - 0366
have hbound_6 : Le(p,6)Exact native replay line
have hbound_6 : exists k. k + p = 6 - 0367
apply le_of_succ_le_succ - 0368
exact hsplit_7_right - 0369
have hsplit_6 : p = 6 ∨ Lt(p,6)Exact native replay line
have hsplit_6 : p = 6 \/ (exists k. k + S p = 6) - 0370
specialize le_eq_or_lt p - 0371
specialize le_eq_or_lt 6 - 0372
apply le_eq_or_lt - 0373
exact hbound_6 - 0374
cases hsplit_6 - 0375
exfalso - 0376
specialize fixed_nontrivial_factor_not_prime p - 0377
specialize fixed_nontrivial_factor_not_prime 2 - 0378
specialize fixed_nontrivial_factor_not_prime 3 - 0379
apply fixed_nontrivial_factor_not_prime - 0380
trans 6 - 0381
exact hsplit_6_left - 0382
norm_num - 0383
intro hleft_one - 0384
apply PA1 - 0385
apply PA2 - 0386
exact hleft_one - 0387
intro hright_one - 0388
apply PA1 - 0389
apply PA2 - 0390
exact hright_one - 0391
exact hp - 0392
have hbound_5 : Le(p,5)Exact native replay line
have hbound_5 : exists k. k + p = 5 - 0393
apply le_of_succ_le_succ - 0394
exact hsplit_6_right - 0395
have hsplit_5 : p = 5 ∨ Lt(p,5)Exact native replay line
have hsplit_5 : p = 5 \/ (exists k. k + S p = 5) - 0396
specialize le_eq_or_lt p - 0397
specialize le_eq_or_lt 5 - 0398
apply le_eq_or_lt - 0399
exact hbound_5 - 0400
cases hsplit_5 - 0401
right - 0402
right - 0403
left - 0404
exact hsplit_5_left - 0405
have hbound_4 : Le(p,4)Exact native replay line
have hbound_4 : exists k. k + p = 4 - 0406
apply le_of_succ_le_succ - 0407
exact hsplit_5_right - 0408
have hsplit_4 : p = 4 ∨ Lt(p,4)Exact native replay line
have hsplit_4 : p = 4 \/ (exists k. k + S p = 4) - 0409
specialize le_eq_or_lt p - 0410
specialize le_eq_or_lt 4 - 0411
apply le_eq_or_lt - 0412
exact hbound_4 - 0413
cases hsplit_4 - 0414
exfalso - 0415
specialize fixed_nontrivial_factor_not_prime p - 0416
specialize fixed_nontrivial_factor_not_prime 2 - 0417
specialize fixed_nontrivial_factor_not_prime 2 - 0418
apply fixed_nontrivial_factor_not_prime - 0419
trans 4 - 0420
exact hsplit_4_left - 0421
norm_num - 0422
intro hleft_one - 0423
apply PA1 - 0424
apply PA2 - 0425
exact hleft_one - 0426
intro hright_one - 0427
apply PA1 - 0428
apply PA2 - 0429
exact hright_one - 0430
exact hp - 0431
have hbound_3 : Le(p,3)Exact native replay line
have hbound_3 : exists k. k + p = 3 - 0432
apply le_of_succ_le_succ - 0433
exact hsplit_4_right - 0434
have hsplit_3 : p = 3 ∨ Lt(p,3)Exact native replay line
have hsplit_3 : p = 3 \/ (exists k. k + S p = 3) - 0435
specialize le_eq_or_lt p - 0436
specialize le_eq_or_lt 3 - 0437
apply le_eq_or_lt - 0438
exact hbound_3 - 0439
cases hsplit_3 - 0440
right - 0441
left - 0442
exact hsplit_3_left - 0443
have hbound_2 : Le(p,2)Exact native replay line
have hbound_2 : exists k. k + p = 2 - 0444
apply le_of_succ_le_succ - 0445
exact hsplit_3_right - 0446
have hsplit_2 : p = 2 ∨ Lt(p,2)Exact native replay line
have hsplit_2 : p = 2 \/ (exists k. k + S p = 2) - 0447
specialize le_eq_or_lt p - 0448
specialize le_eq_or_lt 2 - 0449
apply le_eq_or_lt - 0450
exact hbound_2 - 0451
cases hsplit_2 - 0452
left - 0453
exact hsplit_2_left - 0454
have hshape : exists k. p = S (S k) - 0455
specialize prime_is_succ_succ p - 0456
apply prime_is_succ_succ - 0457
exact hp - 0458
cases hshape - 0459
have htwo : Lt(1,p)Exact native replay line
have htwo : exists k. k + 2 = p - 0460
exists x - 0461
trans S (S x) - 0462
rewrite PA4 - 0463
rewrite PA4 - 0464
rewrite PA3 - 0465
refl - 0466
symm - 0467
exact hshape_witness - 0468
exfalso - 0469
specialize lt_not_le p - 0470
specialize lt_not_le 2 - 0471
apply lt_not_le - 0472
exact hsplit_2_right - 0473
exact htwo