Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Statement with defined notation
Prime(43)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
1 occurrences
In local proof propositions
8 occurrences
Exact expanded native-PA statement
(~(43 = 1) /\ forall bpr_left_bb8cert_prime_forty_three bpr_right_bb8cert_prime_forty_three. 43 = bpr_left_bb8cert_prime_forty_three * bpr_right_bb8cert_prime_forty_three -> bpr_left_bb8cert_prime_forty_three = 1 \/ bpr_right_bb8cert_prime_forty_three = 1)Proof neighborhood
Direct theorem prerequisites
BT011B nonzero_remainder_not_multiple BT0119 prime_of_no_small_prime_divisor_below_square BT000F le_trans BT011A prime_le_twenty_two_cases BT001I lt_not_leDirect 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)
01Establish hn0L1–4
02Establish hn1L5–9
03Establish hsquareL10–10
Establish this local claim before using it. It is not an additional assumption.
04Construct an explicit witnessL11–11
Supply the displayed value, then prove that it has the required property.
- L11
exists 5
05Calculate and transport equalitiesL12–12
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L12
norm_num
06Use earlier factsL13–18
07Fix variables and assumptionsL19–22
08Establish hbound_22L23–23
Establish this local claim before using it. It is not an additional assumption.
09Construct an explicit witnessL24–24
Supply the displayed value, then prove that it has the required property.
- L24
exists 16
10Calculate and transport equalitiesL25–25
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L25
norm_num
11Establish hp_22L26–32
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le trans.
12Establish hcasesL33–37
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime le twenty two cases.
13Separate the logical casesL38–38
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L38
cases hcases
14Calculate and transport equalitiesL39–39
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L39
rewrite hcases_left at hdivides
15Use earlier factsL40–44
Instantiate or apply named facts and discharge the corresponding proof obligations.
16Calculate and transport equalitiesL45–45
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L45
norm_num
17Fix variables and assumptionsL46–46
Work with arbitrary variables or the premises of the current implication.
- L46
intro hrem_2_zero
18Use earlier factsL47–48
19Construct an explicit witnessL49–49
Supply the displayed value, then prove that it has the required property.
- L49
exists 0
20Calculate and transport equalitiesL50–50
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L50
norm_num
21Use earlier factsL51–51
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L51
exact hdivides
22Separate the logical casesL52–52
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L52
cases hcases_right
23Calculate and transport equalitiesL53–53
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L53
rewrite hcases_right_left at hdivides
24Use earlier factsL54–58
Instantiate or apply named facts and discharge the corresponding proof obligations.
25Calculate and transport equalitiesL59–59
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L59
norm_num
26Fix variables and assumptionsL60–60
Work with arbitrary variables or the premises of the current implication.
- L60
intro hrem_3_zero
27Use earlier factsL61–62
28Construct an explicit witnessL63–63
Supply the displayed value, then prove that it has the required property.
- L63
exists 1
29Calculate and transport equalitiesL64–64
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L64
norm_num
30Use earlier factsL65–65
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L65
exact hdivides
31Separate the logical casesL66–66
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L66
cases hcases_right_right
32Calculate and transport equalitiesL67–67
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L67
rewrite hcases_right_right_left at hdivides
33Use earlier factsL68–72
Instantiate or apply named facts and discharge the corresponding proof obligations.
34Calculate and transport equalitiesL73–73
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L73
norm_num
35Fix variables and assumptionsL74–74
Work with arbitrary variables or the premises of the current implication.
- L74
intro hrem_5_zero
36Use earlier factsL75–76
37Construct an explicit witnessL77–77
Supply the displayed value, then prove that it has the required property.
- L77
exists 1
38Calculate and transport equalitiesL78–78
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L78
norm_num
39Use earlier factsL79–79
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L79
exact hdivides
40Separate the logical casesL80–80
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L80
cases hcases_right_right_right
41Establish htoo_large_7L81–81
Establish this local claim before using it. It is not an additional assumption.
42Construct an explicit witnessL82–82
Supply the displayed value, then prove that it has the required property.
- L82
exists 0
43Calculate and transport equalitiesL83–83
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L83
norm_num
44Use earlier factsL84–87
45Calculate and transport equalitiesL88–88
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L88
rewrite hcases_right_right_right_left at hp_bound
46Use earlier factsL89–89
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L89
exact hp_bound
47Separate the logical casesL90–90
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L90
cases hcases_right_right_right_right
48Establish htoo_large_11L91–91
Establish this local claim before using it. It is not an additional assumption.
49Construct an explicit witnessL92–92
Supply the displayed value, then prove that it has the required property.
- L92
exists 4
50Calculate and transport equalitiesL93–93
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L93
norm_num
51Use earlier factsL94–97
52Calculate and transport equalitiesL98–98
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L98
rewrite hcases_right_right_right_right_left at hp_bound
53Use earlier factsL99–99
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L99
exact hp_bound
54Separate the logical casesL100–100
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L100
cases hcases_right_right_right_right_right
55Establish htoo_large_13L101–101
Establish this local claim before using it. It is not an additional assumption.
56Construct an explicit witnessL102–102
Supply the displayed value, then prove that it has the required property.
- L102
exists 6
57Calculate and transport equalitiesL103–103
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L103
norm_num
58Use earlier factsL104–107
59Calculate and transport equalitiesL108–108
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L108
rewrite hcases_right_right_right_right_right_left at hp_bound
60Use earlier factsL109–109
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L109
exact hp_bound
61Separate the logical casesL110–110
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L110
cases hcases_right_right_right_right_right_right
62Establish htoo_large_17L111–111
Establish this local claim before using it. It is not an additional assumption.
63Construct an explicit witnessL112–112
Supply the displayed value, then prove that it has the required property.
- L112
exists 10
64Calculate and transport equalitiesL113–113
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L113
norm_num
65Use earlier factsL114–117
66Calculate and transport equalitiesL118–118
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L118
rewrite hcases_right_right_right_right_right_right_left at hp_bound
67Use earlier factsL119–119
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L119
exact hp_bound
68Establish htoo_large_19L120–120
Establish this local claim before using it. It is not an additional assumption.
69Construct an explicit witnessL121–121
Supply the displayed value, then prove that it has the required property.
- L121
exists 12
70Calculate and transport equalitiesL122–122
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L122
norm_num
71Use earlier factsL123–126
72Calculate and transport equalitiesL127–127
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L127
rewrite hcases_right_right_right_right_right_right_right at hp_bound
73Use earlier factsL128–128
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L128
exact hp_bound
Original defined command ledger · 128 lines
- 0001
have hn0 : ~(43 = 0) - 0002
intro hzero - 0003
apply PA1 - 0004
exact hzero - 0005
have hn1 : ~(43 = 1) - 0006
intro hone - 0007
apply PA1 - 0008
apply PA2 - 0009
exact hone - 0010
have hsquare : Lt(43,7 · 7)Exact native replay line
have hsquare : exists bpr_gap_bb8cert_prime_forty_three_square. bpr_gap_bb8cert_prime_forty_three_square + S (43) = S 6 * S 6 - 0011
exists 5 - 0012
norm_num - 0013
specialize prime_of_no_small_prime_divisor_below_square 6 - 0014
specialize prime_of_no_small_prime_divisor_below_square (43) - 0015
apply prime_of_no_small_prime_divisor_below_square - 0016
exact hn0 - 0017
exact hn1 - 0018
exact hsquare - 0019
intro p - 0020
intro hp - 0021
intro hp_bound - 0022
intro hdivides - 0023
have hbound_22 : Lt(5,22)Exact native replay line
have hbound_22 : exists k. k + 6 = 22 - 0024
exists 16 - 0025
norm_num - 0026
have hp_22 : Le(p,22)Exact native replay line
have hp_22 : exists k. k + p = 22 - 0027
specialize le_trans p - 0028
specialize le_trans 6 - 0029
specialize le_trans 22 - 0030
apply le_trans - 0031
exact hp_bound - 0032
exact hbound_22 - 0033
have hcases : p = 2 \/ (p = 3 \/ (p = 5 \/ (p = 7 \/ (p = 11 \/ (p = 13 \/ (p = 17 \/ (p = 19))))))) - 0034
specialize prime_le_twenty_two_cases p - 0035
apply prime_le_twenty_two_cases - 0036
exact hp - 0037
exact hp_22 - 0038
cases hcases - 0039
rewrite hcases_left at hdivides - 0040
specialize nonzero_remainder_not_multiple 2 - 0041
specialize nonzero_remainder_not_multiple (43) - 0042
specialize nonzero_remainder_not_multiple 21 - 0043
specialize nonzero_remainder_not_multiple 1 - 0044
apply nonzero_remainder_not_multiple - 0045
norm_num - 0046
intro hrem_2_zero - 0047
apply PA1 - 0048
exact hrem_2_zero - 0049
exists 0 - 0050
norm_num - 0051
exact hdivides - 0052
cases hcases_right - 0053
rewrite hcases_right_left at hdivides - 0054
specialize nonzero_remainder_not_multiple 3 - 0055
specialize nonzero_remainder_not_multiple (43) - 0056
specialize nonzero_remainder_not_multiple 14 - 0057
specialize nonzero_remainder_not_multiple 1 - 0058
apply nonzero_remainder_not_multiple - 0059
norm_num - 0060
intro hrem_3_zero - 0061
apply PA1 - 0062
exact hrem_3_zero - 0063
exists 1 - 0064
norm_num - 0065
exact hdivides - 0066
cases hcases_right_right - 0067
rewrite hcases_right_right_left at hdivides - 0068
specialize nonzero_remainder_not_multiple 5 - 0069
specialize nonzero_remainder_not_multiple (43) - 0070
specialize nonzero_remainder_not_multiple 8 - 0071
specialize nonzero_remainder_not_multiple 3 - 0072
apply nonzero_remainder_not_multiple - 0073
norm_num - 0074
intro hrem_5_zero - 0075
apply PA1 - 0076
exact hrem_5_zero - 0077
exists 1 - 0078
norm_num - 0079
exact hdivides - 0080
cases hcases_right_right_right - 0081
have htoo_large_7 : Lt(6,7)Exact native replay line
have htoo_large_7 : exists k. k + S 6 = 7 - 0082
exists 0 - 0083
norm_num - 0084
specialize lt_not_le 6 - 0085
specialize lt_not_le 7 - 0086
apply lt_not_le - 0087
exact htoo_large_7 - 0088
rewrite hcases_right_right_right_left at hp_bound - 0089
exact hp_bound - 0090
cases hcases_right_right_right_right - 0091
have htoo_large_11 : Lt(6,11)Exact native replay line
have htoo_large_11 : exists k. k + S 6 = 11 - 0092
exists 4 - 0093
norm_num - 0094
specialize lt_not_le 6 - 0095
specialize lt_not_le 11 - 0096
apply lt_not_le - 0097
exact htoo_large_11 - 0098
rewrite hcases_right_right_right_right_left at hp_bound - 0099
exact hp_bound - 0100
cases hcases_right_right_right_right_right - 0101
have htoo_large_13 : Lt(6,13)Exact native replay line
have htoo_large_13 : exists k. k + S 6 = 13 - 0102
exists 6 - 0103
norm_num - 0104
specialize lt_not_le 6 - 0105
specialize lt_not_le 13 - 0106
apply lt_not_le - 0107
exact htoo_large_13 - 0108
rewrite hcases_right_right_right_right_right_left at hp_bound - 0109
exact hp_bound - 0110
cases hcases_right_right_right_right_right_right - 0111
have htoo_large_17 : Lt(6,17)Exact native replay line
have htoo_large_17 : exists k. k + S 6 = 17 - 0112
exists 10 - 0113
norm_num - 0114
specialize lt_not_le 6 - 0115
specialize lt_not_le 17 - 0116
apply lt_not_le - 0117
exact htoo_large_17 - 0118
rewrite hcases_right_right_right_right_right_right_left at hp_bound - 0119
exact hp_bound - 0120
have htoo_large_19 : Lt(6,19)Exact native replay line
have htoo_large_19 : exists k. k + S 6 = 19 - 0121
exists 12 - 0122
norm_num - 0123
specialize lt_not_le 6 - 0124
specialize lt_not_le 19 - 0125
apply lt_not_le - 0126
exact htoo_large_19 - 0127
rewrite hcases_right_right_right_right_right_right_right at hp_bound - 0128
exact hp_bound