MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prmlem2 Structured version   Visualization version   GIF version

Theorem prmlem2 15808
Description: Our last proving session got as far as 25 because we started with the two "bootstrap" primes 2 and 3, and the next prime is 5, so knowing that 2 and 3 are prime and 4 is not allows us to cover the numbers less than 5↑2 = 25. Additionally, nonprimes are "easy", so we can extend this range of known prime/nonprimes all the way until 29, which is the first prime larger than 25. Thus, in this lemma we extend another blanket out to 29↑2 = 841, from which we can prove even more primes. If we wanted, we could keep doing this, but the goal is Bertrand's postulate, and for that we only need a few large primes - we don't need to find them all, as we have been doing thus far. So after this blanket runs out, we'll have to switch to another method (see 1259prm 15824).

As a side note, you can see the pattern of the primes in the indentation pattern of this lemma! (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)

Hypotheses
Ref Expression
prmlem2.n 𝑁 ∈ ℕ
prmlem2.lt 𝑁 < 841
prmlem2.gt 1 < 𝑁
prmlem2.2 ¬ 2 ∥ 𝑁
prmlem2.3 ¬ 3 ∥ 𝑁
prmlem2.5 ¬ 5 ∥ 𝑁
prmlem2.7 ¬ 7 ∥ 𝑁
prmlem2.11 ¬ 11 ∥ 𝑁
prmlem2.13 ¬ 13 ∥ 𝑁
prmlem2.17 ¬ 17 ∥ 𝑁
prmlem2.19 ¬ 19 ∥ 𝑁
prmlem2.23 ¬ 23 ∥ 𝑁
Assertion
Ref Expression
prmlem2 𝑁 ∈ ℙ

Proof of Theorem prmlem2
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 prmlem2.n . 2 𝑁 ∈ ℕ
2 prmlem2.gt . 2 1 < 𝑁
3 prmlem2.2 . 2 ¬ 2 ∥ 𝑁
4 prmlem2.3 . 2 ¬ 3 ∥ 𝑁
5 eluzelre 11683 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (ℤ29) → 𝑥 ∈ ℝ)
65resqcld 13018 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (ℤ29) → (𝑥↑2) ∈ ℝ)
7 eluzle 11685 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (ℤ29) → 29 ≤ 𝑥)
8 2nn0 11294 . . . . . . . . . . . . . . . . . . . . . . 23 2 ∈ ℕ0
9 9nn0 11301 . . . . . . . . . . . . . . . . . . . . . . 23 9 ∈ ℕ0
108, 9deccl 11497 . . . . . . . . . . . . . . . . . . . . . 22 29 ∈ ℕ0
1110nn0rei 11288 . . . . . . . . . . . . . . . . . . . . 21 29 ∈ ℝ
1210nn0ge0i 11305 . . . . . . . . . . . . . . . . . . . . 21 0 ≤ 29
13 le2sq2 12922 . . . . . . . . . . . . . . . . . . . . 21 (((29 ∈ ℝ ∧ 0 ≤ 29) ∧ (𝑥 ∈ ℝ ∧ 29 ≤ 𝑥)) → (29↑2) ≤ (𝑥↑2))
1411, 12, 13mpanl12 717 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ℝ ∧ 29 ≤ 𝑥) → (29↑2) ≤ (𝑥↑2))
155, 7, 14syl2anc 692 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (ℤ29) → (29↑2) ≤ (𝑥↑2))
161nnrei 11014 . . . . . . . . . . . . . . . . . . . 20 𝑁 ∈ ℝ
1711resqcli 12932 . . . . . . . . . . . . . . . . . . . 20 (29↑2) ∈ ℝ
18 prmlem2.lt . . . . . . . . . . . . . . . . . . . . . 22 𝑁 < 841
1910nn0cni 11289 . . . . . . . . . . . . . . . . . . . . . . . 24 29 ∈ ℂ
2019sqvali 12926 . . . . . . . . . . . . . . . . . . . . . . 23 (29↑2) = (29 · 29)
21 eqid 2620 . . . . . . . . . . . . . . . . . . . . . . . 24 29 = 29
22 1nn0 11293 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ∈ ℕ0
23 6nn0 11298 . . . . . . . . . . . . . . . . . . . . . . . . 25 6 ∈ ℕ0
248, 23deccl 11497 . . . . . . . . . . . . . . . . . . . . . . . 24 26 ∈ ℕ0
25 5nn0 11297 . . . . . . . . . . . . . . . . . . . . . . . . 25 5 ∈ ℕ0
26 8nn0 11300 . . . . . . . . . . . . . . . . . . . . . . . . 25 8 ∈ ℕ0
27192timesi 11132 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (2 · 29) = (29 + 29)
28 2p2e4 11129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (2 + 2) = 4
2928oveq1i 6645 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2 + 2) + 1) = (4 + 1)
30 4p1e5 11139 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (4 + 1) = 5
3129, 30eqtri 2642 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((2 + 2) + 1) = 5
32 9p9e18 11612 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (9 + 9) = 18
338, 9, 8, 9, 21, 21, 31, 26, 32decaddc 11557 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (29 + 29) = 58
3427, 33eqtri 2642 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2 · 29) = 58
35 eqid 2620 . . . . . . . . . . . . . . . . . . . . . . . . 25 26 = 26
36 5p2e7 11150 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (5 + 2) = 7
3736oveq1i 6645 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((5 + 2) + 1) = (7 + 1)
38 7p1e8 11142 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (7 + 1) = 8
3937, 38eqtri 2642 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((5 + 2) + 1) = 8
40 4nn0 11296 . . . . . . . . . . . . . . . . . . . . . . . . 25 4 ∈ ℕ0
41 8p6e14 11601 . . . . . . . . . . . . . . . . . . . . . . . . 25 (8 + 6) = 14
4225, 26, 8, 23, 34, 35, 39, 40, 41decaddc 11557 . . . . . . . . . . . . . . . . . . . . . . . 24 ((2 · 29) + 26) = 84
43 9t2e18 11648 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (9 · 2) = 18
44 1p1e2 11119 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1 + 1) = 2
45 8p8e16 11603 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (8 + 8) = 16
4622, 26, 26, 43, 44, 23, 45decaddci 11565 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((9 · 2) + 8) = 26
47 9t9e81 11655 . . . . . . . . . . . . . . . . . . . . . . . . 25 (9 · 9) = 81
489, 8, 9, 21, 22, 26, 46, 47decmul2c 11574 . . . . . . . . . . . . . . . . . . . . . . . 24 (9 · 29) = 261
4910, 8, 9, 21, 22, 24, 42, 48decmul1c 11572 . . . . . . . . . . . . . . . . . . . . . . 23 (29 · 29) = 841
5020, 49eqtri 2642 . . . . . . . . . . . . . . . . . . . . . 22 (29↑2) = 841
5118, 50breqtrri 4671 . . . . . . . . . . . . . . . . . . . . 21 𝑁 < (29↑2)
52 ltletr 10114 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℝ ∧ (29↑2) ∈ ℝ ∧ (𝑥↑2) ∈ ℝ) → ((𝑁 < (29↑2) ∧ (29↑2) ≤ (𝑥↑2)) → 𝑁 < (𝑥↑2)))
5351, 52mpani 711 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℝ ∧ (29↑2) ∈ ℝ ∧ (𝑥↑2) ∈ ℝ) → ((29↑2) ≤ (𝑥↑2) → 𝑁 < (𝑥↑2)))
5416, 17, 53mp3an12 1412 . . . . . . . . . . . . . . . . . . 19 ((𝑥↑2) ∈ ℝ → ((29↑2) ≤ (𝑥↑2) → 𝑁 < (𝑥↑2)))
556, 15, 54sylc 65 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (ℤ29) → 𝑁 < (𝑥↑2))
56 ltnle 10102 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℝ ∧ (𝑥↑2) ∈ ℝ) → (𝑁 < (𝑥↑2) ↔ ¬ (𝑥↑2) ≤ 𝑁))
5716, 6, 56sylancr 694 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (ℤ29) → (𝑁 < (𝑥↑2) ↔ ¬ (𝑥↑2) ≤ 𝑁))
5855, 57mpbid 222 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (ℤ29) → ¬ (𝑥↑2) ≤ 𝑁)
5958pm2.21d 118 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (ℤ29) → ((𝑥↑2) ≤ 𝑁 → ¬ 𝑥𝑁))
6059adantld 483 . . . . . . . . . . . . . . 15 (𝑥 ∈ (ℤ29) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥𝑁))
6160adantl 482 . . . . . . . . . . . . . 14 ((¬ 2 ∥ 29 ∧ 𝑥 ∈ (ℤ29)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥𝑁))
62 9nn 11177 . . . . . . . . . . . . . . . 16 9 ∈ ℕ
63 3nn 11171 . . . . . . . . . . . . . . . 16 3 ∈ ℕ
64 1lt9 11214 . . . . . . . . . . . . . . . 16 1 < 9
65 1lt3 11181 . . . . . . . . . . . . . . . 16 1 < 3
66 9t3e27 11649 . . . . . . . . . . . . . . . 16 (9 · 3) = 27
6762, 63, 64, 65, 66nprmi 15383 . . . . . . . . . . . . . . 15 ¬ 27 ∈ ℙ
6867pm2.21i 116 . . . . . . . . . . . . . 14 (27 ∈ ℙ → ¬ 27 ∥ 𝑁)
69 7nn0 11299 . . . . . . . . . . . . . . 15 7 ∈ ℕ0
70 eqid 2620 . . . . . . . . . . . . . . 15 27 = 27
71 7p2e9 11157 . . . . . . . . . . . . . . 15 (7 + 2) = 9
728, 69, 8, 70, 71decaddi 11564 . . . . . . . . . . . . . 14 (27 + 2) = 29
7361, 68, 72prmlem0 15793 . . . . . . . . . . . . 13 ((¬ 2 ∥ 27 ∧ 𝑥 ∈ (ℤ27)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥𝑁))
74 5nn 11173 . . . . . . . . . . . . . . 15 5 ∈ ℕ
75 1lt5 11188 . . . . . . . . . . . . . . 15 1 < 5
76 5t5e25 11624 . . . . . . . . . . . . . . 15 (5 · 5) = 25
7774, 74, 75, 75, 76nprmi 15383 . . . . . . . . . . . . . 14 ¬ 25 ∈ ℙ
7877pm2.21i 116 . . . . . . . . . . . . 13 (25 ∈ ℙ → ¬ 25 ∥ 𝑁)
79 eqid 2620 . . . . . . . . . . . . . 14 25 = 25
808, 25, 8, 79, 36decaddi 11564 . . . . . . . . . . . . 13 (25 + 2) = 27
8173, 78, 80prmlem0 15793 . . . . . . . . . . . 12 ((¬ 2 ∥ 25 ∧ 𝑥 ∈ (ℤ25)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥𝑁))
82 prmlem2.23 . . . . . . . . . . . . 13 ¬ 23 ∥ 𝑁
8382a1i 11 . . . . . . . . . . . 12 (23 ∈ ℙ → ¬ 23 ∥ 𝑁)
84 3nn0 11295 . . . . . . . . . . . . 13 3 ∈ ℕ0
85 eqid 2620 . . . . . . . . . . . . 13 23 = 23
86 3p2e5 11145 . . . . . . . . . . . . 13 (3 + 2) = 5
878, 84, 8, 85, 86decaddi 11564 . . . . . . . . . . . 12 (23 + 2) = 25
8881, 83, 87prmlem0 15793 . . . . . . . . . . 11 ((¬ 2 ∥ 23 ∧ 𝑥 ∈ (ℤ23)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥𝑁))
89 7nn 11175 . . . . . . . . . . . . 13 7 ∈ ℕ
90 1lt7 11199 . . . . . . . . . . . . 13 1 < 7
91 7t3e21 11634 . . . . . . . . . . . . 13 (7 · 3) = 21
9289, 63, 90, 65, 91nprmi 15383 . . . . . . . . . . . 12 ¬ 21 ∈ ℙ
9392pm2.21i 116 . . . . . . . . . . 11 (21 ∈ ℙ → ¬ 21 ∥ 𝑁)
94 eqid 2620 . . . . . . . . . . . 12 21 = 21
95 1p2e3 11137 . . . . . . . . . . . 12 (1 + 2) = 3
968, 22, 8, 94, 95decaddi 11564 . . . . . . . . . . 11 (21 + 2) = 23
9788, 93, 96prmlem0 15793 . . . . . . . . . 10 ((¬ 2 ∥ 21 ∧ 𝑥 ∈ (ℤ21)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥𝑁))
98 prmlem2.19 . . . . . . . . . . 11 ¬ 19 ∥ 𝑁
9998a1i 11 . . . . . . . . . 10 (19 ∈ ℙ → ¬ 19 ∥ 𝑁)
100 eqid 2620 . . . . . . . . . . 11 19 = 19
101 9p2e11 11604 . . . . . . . . . . 11 (9 + 2) = 11
10222, 9, 8, 100, 44, 22, 101decaddci 11565 . . . . . . . . . 10 (19 + 2) = 21
10397, 99, 102prmlem0 15793 . . . . . . . . 9 ((¬ 2 ∥ 19 ∧ 𝑥 ∈ (ℤ19)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥𝑁))
104 prmlem2.17 . . . . . . . . . 10 ¬ 17 ∥ 𝑁
105104a1i 11 . . . . . . . . 9 (17 ∈ ℙ → ¬ 17 ∥ 𝑁)
106 eqid 2620 . . . . . . . . . 10 17 = 17
10722, 69, 8, 106, 71decaddi 11564 . . . . . . . . 9 (17 + 2) = 19
108103, 105, 107prmlem0 15793 . . . . . . . 8 ((¬ 2 ∥ 17 ∧ 𝑥 ∈ (ℤ17)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥𝑁))
109 5t3e15 11620 . . . . . . . . . 10 (5 · 3) = 15
11074, 63, 75, 65, 109nprmi 15383 . . . . . . . . 9 ¬ 15 ∈ ℙ
111110pm2.21i 116 . . . . . . . 8 (15 ∈ ℙ → ¬ 15 ∥ 𝑁)
112 eqid 2620 . . . . . . . . 9 15 = 15
11322, 25, 8, 112, 36decaddi 11564 . . . . . . . 8 (15 + 2) = 17
114108, 111, 113prmlem0 15793 . . . . . . 7 ((¬ 2 ∥ 15 ∧ 𝑥 ∈ (ℤ15)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥𝑁))
115 prmlem2.13 . . . . . . . 8 ¬ 13 ∥ 𝑁
116115a1i 11 . . . . . . 7 (13 ∈ ℙ → ¬ 13 ∥ 𝑁)
117 eqid 2620 . . . . . . . 8 13 = 13
11822, 84, 8, 117, 86decaddi 11564 . . . . . . 7 (13 + 2) = 15
119114, 116, 118prmlem0 15793 . . . . . 6 ((¬ 2 ∥ 13 ∧ 𝑥 ∈ (ℤ13)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥𝑁))
120 prmlem2.11 . . . . . . 7 ¬ 11 ∥ 𝑁
121120a1i 11 . . . . . 6 (11 ∈ ℙ → ¬ 11 ∥ 𝑁)
122 eqid 2620 . . . . . . 7 11 = 11
12322, 22, 8, 122, 95decaddi 11564 . . . . . 6 (11 + 2) = 13
124119, 121, 123prmlem0 15793 . . . . 5 ((¬ 2 ∥ 11 ∧ 𝑥 ∈ (ℤ11)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥𝑁))
125 9nprm 15800 . . . . . 6 ¬ 9 ∈ ℙ
126125pm2.21i 116 . . . . 5 (9 ∈ ℙ → ¬ 9 ∥ 𝑁)
127124, 126, 101prmlem0 15793 . . . 4 ((¬ 2 ∥ 9 ∧ 𝑥 ∈ (ℤ‘9)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥𝑁))
128 prmlem2.7 . . . . 5 ¬ 7 ∥ 𝑁
129128a1i 11 . . . 4 (7 ∈ ℙ → ¬ 7 ∥ 𝑁)
130127, 129, 71prmlem0 15793 . . 3 ((¬ 2 ∥ 7 ∧ 𝑥 ∈ (ℤ‘7)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥𝑁))
131 prmlem2.5 . . . 4 ¬ 5 ∥ 𝑁
132131a1i 11 . . 3 (5 ∈ ℙ → ¬ 5 ∥ 𝑁)
133130, 132, 36prmlem0 15793 . 2 ((¬ 2 ∥ 5 ∧ 𝑥 ∈ (ℤ‘5)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥𝑁))
1341, 2, 3, 4, 133prmlem1a 15794 1 𝑁 ∈ ℙ
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036  wcel 1988  cdif 3564  {csn 4168   class class class wbr 4644  cfv 5876  (class class class)co 6635  cr 9920  0cc0 9921  1c1 9922   + caddc 9924   · cmul 9926   < clt 10059  cle 10060  cn 11005  2c2 11055  3c3 11056  4c4 11057  5c5 11058  6c6 11059  7c7 11060  8c8 11061  9c9 11062  cdc 11478  cuz 11672  cexp 12843  cdvds 14964  cprime 15366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998  ax-pre-sup 9999
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-2o 7546  df-oadd 7549  df-er 7727  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-sup 8333  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-div 10670  df-nn 11006  df-2 11064  df-3 11065  df-4 11066  df-5 11067  df-6 11068  df-7 11069  df-8 11070  df-9 11071  df-n0 11278  df-z 11363  df-dec 11479  df-uz 11673  df-rp 11818  df-fz 12312  df-seq 12785  df-exp 12844  df-cj 13820  df-re 13821  df-im 13822  df-sqrt 13956  df-abs 13957  df-dvds 14965  df-prm 15367
This theorem is referenced by:  37prm  15809  43prm  15810  83prm  15811  139prm  15812  163prm  15813  317prm  15814  631prm  15815  257prm  41238  139prmALT  41276  127prm  41280
  Copyright terms: Public domain W3C validator