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(5)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
10 occurrences
Exact expanded native-PA statement
(~(5 = 1) /\ forall bpr_left_bb8cert_prime_five bpr_right_bb8cert_prime_five. 5 = bpr_left_bb8cert_prime_five * bpr_right_bb8cert_prime_five -> bpr_left_bb8cert_prime_five = 1 \/ bpr_right_bb8cert_prime_five = 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 3
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 20
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
23Establish htoo_large_3L53–53
Establish this local claim before using it. It is not an additional assumption.
24Construct an explicit witnessL54–54
Supply the displayed value, then prove that it has the required property.
- L54
exists 0
25Calculate and transport equalitiesL55–55
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L55
norm_num
26Use earlier factsL56–59
27Calculate and transport equalitiesL60–60
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L60
rewrite hcases_right_left at hp_bound
28Use earlier factsL61–61
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L61
exact hp_bound
29Separate the logical casesL62–62
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L62
cases hcases_right_right
30Establish htoo_large_5L63–63
Establish this local claim before using it. It is not an additional assumption.
31Construct an explicit witnessL64–64
Supply the displayed value, then prove that it has the required property.
- L64
exists 2
32Calculate and transport equalitiesL65–65
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L65
norm_num
33Use earlier factsL66–69
34Calculate and transport equalitiesL70–70
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L70
rewrite hcases_right_right_left at hp_bound
35Use earlier factsL71–71
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L71
exact hp_bound
36Separate the logical casesL72–72
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L72
cases hcases_right_right_right
37Establish htoo_large_7L73–73
Establish this local claim before using it. It is not an additional assumption.
38Construct an explicit witnessL74–74
Supply the displayed value, then prove that it has the required property.
- L74
exists 4
39Calculate and transport equalitiesL75–75
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L75
norm_num
40Use earlier factsL76–79
41Calculate and transport equalitiesL80–80
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L80
rewrite hcases_right_right_right_left at hp_bound
42Use earlier factsL81–81
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L81
exact hp_bound
43Separate the logical casesL82–82
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L82
cases hcases_right_right_right_right
44Establish htoo_large_11L83–83
Establish this local claim before using it. It is not an additional assumption.
45Construct an explicit witnessL84–84
Supply the displayed value, then prove that it has the required property.
- L84
exists 8
46Calculate and transport equalitiesL85–85
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L85
norm_num
47Use earlier factsL86–89
48Calculate and transport equalitiesL90–90
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L90
rewrite hcases_right_right_right_right_left at hp_bound
49Use earlier factsL91–91
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L91
exact hp_bound
50Separate the logical casesL92–92
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L92
cases hcases_right_right_right_right_right
51Establish htoo_large_13L93–93
Establish this local claim before using it. It is not an additional assumption.
52Construct an explicit witnessL94–94
Supply the displayed value, then prove that it has the required property.
- L94
exists 10
53Calculate and transport equalitiesL95–95
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L95
norm_num
54Use earlier factsL96–99
55Calculate and transport equalitiesL100–100
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L100
rewrite hcases_right_right_right_right_right_left at hp_bound
56Use earlier factsL101–101
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L101
exact hp_bound
57Separate the logical casesL102–102
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L102
cases hcases_right_right_right_right_right_right
58Establish htoo_large_17L103–103
Establish this local claim before using it. It is not an additional assumption.
59Construct an explicit witnessL104–104
Supply the displayed value, then prove that it has the required property.
- L104
exists 14
60Calculate and transport equalitiesL105–105
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L105
norm_num
61Use earlier factsL106–109
62Calculate and transport equalitiesL110–110
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L110
rewrite hcases_right_right_right_right_right_right_left at hp_bound
63Use earlier factsL111–111
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L111
exact hp_bound
64Establish htoo_large_19L112–112
Establish this local claim before using it. It is not an additional assumption.
65Construct an explicit witnessL113–113
Supply the displayed value, then prove that it has the required property.
- L113
exists 16
66Calculate and transport equalitiesL114–114
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L114
norm_num
67Use earlier factsL115–118
68Calculate and transport equalitiesL119–119
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L119
rewrite hcases_right_right_right_right_right_right_right at hp_bound
69Use earlier factsL120–120
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L120
exact hp_bound
Original defined command ledger · 120 lines
- 0001
have hn0 : ~(5 = 0) - 0002
intro hzero - 0003
apply PA1 - 0004
exact hzero - 0005
have hn1 : ~(5 = 1) - 0006
intro hone - 0007
apply PA1 - 0008
apply PA2 - 0009
exact hone - 0010
have hsquare : Lt(5,3 · 3)Exact native replay line
have hsquare : exists bpr_gap_bb8cert_prime_five_square. bpr_gap_bb8cert_prime_five_square + S (5) = S 2 * S 2 - 0011
exists 3 - 0012
norm_num - 0013
specialize prime_of_no_small_prime_divisor_below_square 2 - 0014
specialize prime_of_no_small_prime_divisor_below_square (5) - 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(1,22)Exact native replay line
have hbound_22 : exists k. k + 2 = 22 - 0024
exists 20 - 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 2 - 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 (5) - 0042
specialize nonzero_remainder_not_multiple 2 - 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
have htoo_large_3 : Lt(2,3)Exact native replay line
have htoo_large_3 : exists k. k + S 2 = 3 - 0054
exists 0 - 0055
norm_num - 0056
specialize lt_not_le 2 - 0057
specialize lt_not_le 3 - 0058
apply lt_not_le - 0059
exact htoo_large_3 - 0060
rewrite hcases_right_left at hp_bound - 0061
exact hp_bound - 0062
cases hcases_right_right - 0063
have htoo_large_5 : Lt(2,5)Exact native replay line
have htoo_large_5 : exists k. k + S 2 = 5 - 0064
exists 2 - 0065
norm_num - 0066
specialize lt_not_le 2 - 0067
specialize lt_not_le 5 - 0068
apply lt_not_le - 0069
exact htoo_large_5 - 0070
rewrite hcases_right_right_left at hp_bound - 0071
exact hp_bound - 0072
cases hcases_right_right_right - 0073
have htoo_large_7 : Lt(2,7)Exact native replay line
have htoo_large_7 : exists k. k + S 2 = 7 - 0074
exists 4 - 0075
norm_num - 0076
specialize lt_not_le 2 - 0077
specialize lt_not_le 7 - 0078
apply lt_not_le - 0079
exact htoo_large_7 - 0080
rewrite hcases_right_right_right_left at hp_bound - 0081
exact hp_bound - 0082
cases hcases_right_right_right_right - 0083
have htoo_large_11 : Lt(2,11)Exact native replay line
have htoo_large_11 : exists k. k + S 2 = 11 - 0084
exists 8 - 0085
norm_num - 0086
specialize lt_not_le 2 - 0087
specialize lt_not_le 11 - 0088
apply lt_not_le - 0089
exact htoo_large_11 - 0090
rewrite hcases_right_right_right_right_left at hp_bound - 0091
exact hp_bound - 0092
cases hcases_right_right_right_right_right - 0093
have htoo_large_13 : Lt(2,13)Exact native replay line
have htoo_large_13 : exists k. k + S 2 = 13 - 0094
exists 10 - 0095
norm_num - 0096
specialize lt_not_le 2 - 0097
specialize lt_not_le 13 - 0098
apply lt_not_le - 0099
exact htoo_large_13 - 0100
rewrite hcases_right_right_right_right_right_left at hp_bound - 0101
exact hp_bound - 0102
cases hcases_right_right_right_right_right_right - 0103
have htoo_large_17 : Lt(2,17)Exact native replay line
have htoo_large_17 : exists k. k + S 2 = 17 - 0104
exists 14 - 0105
norm_num - 0106
specialize lt_not_le 2 - 0107
specialize lt_not_le 17 - 0108
apply lt_not_le - 0109
exact htoo_large_17 - 0110
rewrite hcases_right_right_right_right_right_right_left at hp_bound - 0111
exact hp_bound - 0112
have htoo_large_19 : Lt(2,19)Exact native replay line
have htoo_large_19 : exists k. k + S 2 = 19 - 0113
exists 16 - 0114
norm_num - 0115
specialize lt_not_le 2 - 0116
specialize lt_not_le 19 - 0117
apply lt_not_le - 0118
exact htoo_large_19 - 0119
rewrite hcases_right_right_right_right_right_right_right at hp_bound - 0120
exact hp_bound