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(13)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
9 occurrences
Exact expanded native-PA statement
(~(13 = 1) /\ forall bpr_left_bb8cert_prime_thirteen bpr_right_bb8cert_prime_thirteen. 13 = bpr_left_bb8cert_prime_thirteen * bpr_right_bb8cert_prime_thirteen -> bpr_left_bb8cert_prime_thirteen = 1 \/ bpr_right_bb8cert_prime_thirteen = 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 2
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 19
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
32Establish htoo_large_5L67–67
Establish this local claim before using it. It is not an additional assumption.
33Construct an explicit witnessL68–68
Supply the displayed value, then prove that it has the required property.
- L68
exists 1
34Calculate and transport equalitiesL69–69
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L69
norm_num
35Use earlier factsL70–73
36Calculate and transport equalitiesL74–74
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L74
rewrite hcases_right_right_left at hp_bound
37Use earlier factsL75–75
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L75
exact hp_bound
38Separate the logical casesL76–76
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L76
cases hcases_right_right_right
39Establish htoo_large_7L77–77
Establish this local claim before using it. It is not an additional assumption.
40Construct an explicit witnessL78–78
Supply the displayed value, then prove that it has the required property.
- L78
exists 3
41Calculate and transport equalitiesL79–79
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L79
norm_num
42Use earlier factsL80–83
43Calculate and transport equalitiesL84–84
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L84
rewrite hcases_right_right_right_left at hp_bound
44Use earlier factsL85–85
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L85
exact hp_bound
45Separate the logical casesL86–86
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L86
cases hcases_right_right_right_right
46Establish htoo_large_11L87–87
Establish this local claim before using it. It is not an additional assumption.
47Construct an explicit witnessL88–88
Supply the displayed value, then prove that it has the required property.
- L88
exists 7
48Calculate and transport equalitiesL89–89
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L89
norm_num
49Use earlier factsL90–93
50Calculate and transport equalitiesL94–94
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L94
rewrite hcases_right_right_right_right_left at hp_bound
51Use earlier factsL95–95
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L95
exact hp_bound
52Separate the logical casesL96–96
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L96
cases hcases_right_right_right_right_right
53Establish htoo_large_13L97–97
Establish this local claim before using it. It is not an additional assumption.
54Construct an explicit witnessL98–98
Supply the displayed value, then prove that it has the required property.
- L98
exists 9
55Calculate and transport equalitiesL99–99
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L99
norm_num
56Use earlier factsL100–103
57Calculate and transport equalitiesL104–104
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L104
rewrite hcases_right_right_right_right_right_left at hp_bound
58Use earlier factsL105–105
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L105
exact hp_bound
59Separate the logical casesL106–106
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L106
cases hcases_right_right_right_right_right_right
60Establish htoo_large_17L107–107
Establish this local claim before using it. It is not an additional assumption.
61Construct an explicit witnessL108–108
Supply the displayed value, then prove that it has the required property.
- L108
exists 13
62Calculate and transport equalitiesL109–109
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L109
norm_num
63Use earlier factsL110–113
64Calculate and transport equalitiesL114–114
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L114
rewrite hcases_right_right_right_right_right_right_left at hp_bound
65Use earlier factsL115–115
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L115
exact hp_bound
66Establish htoo_large_19L116–116
Establish this local claim before using it. It is not an additional assumption.
67Construct an explicit witnessL117–117
Supply the displayed value, then prove that it has the required property.
- L117
exists 15
68Calculate and transport equalitiesL118–118
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L118
norm_num
69Use earlier factsL119–122
70Calculate and transport equalitiesL123–123
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L123
rewrite hcases_right_right_right_right_right_right_right at hp_bound
71Use earlier factsL124–124
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L124
exact hp_bound
Original defined command ledger · 124 lines
- 0001
have hn0 : ~(13 = 0) - 0002
intro hzero - 0003
apply PA1 - 0004
exact hzero - 0005
have hn1 : ~(13 = 1) - 0006
intro hone - 0007
apply PA1 - 0008
apply PA2 - 0009
exact hone - 0010
have hsquare : Lt(13,4 · 4)Exact native replay line
have hsquare : exists bpr_gap_bb8cert_prime_thirteen_square. bpr_gap_bb8cert_prime_thirteen_square + S (13) = S 3 * S 3 - 0011
exists 2 - 0012
norm_num - 0013
specialize prime_of_no_small_prime_divisor_below_square 3 - 0014
specialize prime_of_no_small_prime_divisor_below_square (13) - 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(2,22)Exact native replay line
have hbound_22 : exists k. k + 3 = 22 - 0024
exists 19 - 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 3 - 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 (13) - 0042
specialize nonzero_remainder_not_multiple 6 - 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 (13) - 0056
specialize nonzero_remainder_not_multiple 4 - 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
have htoo_large_5 : Lt(3,5)Exact native replay line
have htoo_large_5 : exists k. k + S 3 = 5 - 0068
exists 1 - 0069
norm_num - 0070
specialize lt_not_le 3 - 0071
specialize lt_not_le 5 - 0072
apply lt_not_le - 0073
exact htoo_large_5 - 0074
rewrite hcases_right_right_left at hp_bound - 0075
exact hp_bound - 0076
cases hcases_right_right_right - 0077
have htoo_large_7 : Lt(3,7)Exact native replay line
have htoo_large_7 : exists k. k + S 3 = 7 - 0078
exists 3 - 0079
norm_num - 0080
specialize lt_not_le 3 - 0081
specialize lt_not_le 7 - 0082
apply lt_not_le - 0083
exact htoo_large_7 - 0084
rewrite hcases_right_right_right_left at hp_bound - 0085
exact hp_bound - 0086
cases hcases_right_right_right_right - 0087
have htoo_large_11 : Lt(3,11)Exact native replay line
have htoo_large_11 : exists k. k + S 3 = 11 - 0088
exists 7 - 0089
norm_num - 0090
specialize lt_not_le 3 - 0091
specialize lt_not_le 11 - 0092
apply lt_not_le - 0093
exact htoo_large_11 - 0094
rewrite hcases_right_right_right_right_left at hp_bound - 0095
exact hp_bound - 0096
cases hcases_right_right_right_right_right - 0097
have htoo_large_13 : Lt(3,13)Exact native replay line
have htoo_large_13 : exists k. k + S 3 = 13 - 0098
exists 9 - 0099
norm_num - 0100
specialize lt_not_le 3 - 0101
specialize lt_not_le 13 - 0102
apply lt_not_le - 0103
exact htoo_large_13 - 0104
rewrite hcases_right_right_right_right_right_left at hp_bound - 0105
exact hp_bound - 0106
cases hcases_right_right_right_right_right_right - 0107
have htoo_large_17 : Lt(3,17)Exact native replay line
have htoo_large_17 : exists k. k + S 3 = 17 - 0108
exists 13 - 0109
norm_num - 0110
specialize lt_not_le 3 - 0111
specialize lt_not_le 17 - 0112
apply lt_not_le - 0113
exact htoo_large_17 - 0114
rewrite hcases_right_right_right_right_right_right_left at hp_bound - 0115
exact hp_bound - 0116
have htoo_large_19 : Lt(3,19)Exact native replay line
have htoo_large_19 : exists k. k + S 3 = 19 - 0117
exists 15 - 0118
norm_num - 0119
specialize lt_not_le 3 - 0120
specialize lt_not_le 19 - 0121
apply lt_not_le - 0122
exact htoo_large_19 - 0123
rewrite hcases_right_right_right_right_right_right_right at hp_bound - 0124
exact hp_bound