Proof of Theorem ppiublem2
Step | Hyp | Ref
| Expression |
1 | | prmz 15227 |
. . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
2 | 1 | adantr 480 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → 𝑃 ∈ ℤ) |
3 | | 6nn 11066 |
. . . 4
⊢ 6 ∈
ℕ |
4 | | zmodfz 12554 |
. . . 4
⊢ ((𝑃 ∈ ℤ ∧ 6 ∈
ℕ) → (𝑃 mod 6)
∈ (0...(6 − 1))) |
5 | 2, 3, 4 | sylancl 693 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (𝑃 mod 6) ∈ (0...(6 −
1))) |
6 | | df-6 10960 |
. . . . . 6
⊢ 6 = (5 +
1) |
7 | 6 | oveq1i 6559 |
. . . . 5
⊢ (6
− 1) = ((5 + 1) − 1) |
8 | | 5cn 10977 |
. . . . . 6
⊢ 5 ∈
ℂ |
9 | | ax-1cn 9873 |
. . . . . 6
⊢ 1 ∈
ℂ |
10 | 8, 9 | pncan3oi 10176 |
. . . . 5
⊢ ((5 + 1)
− 1) = 5 |
11 | 7, 10 | eqtri 2632 |
. . . 4
⊢ (6
− 1) = 5 |
12 | 11 | oveq2i 6560 |
. . 3
⊢ (0...(6
− 1)) = (0...5) |
13 | 5, 12 | syl6eleq 2698 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (𝑃 mod 6) ∈
(0...5)) |
14 | | 6re 10978 |
. . . . . . . . . . 11
⊢ 6 ∈
ℝ |
15 | 14 | leidi 10441 |
. . . . . . . . . 10
⊢ 6 ≤
6 |
16 | | noel 3878 |
. . . . . . . . . . . . 13
⊢ ¬
(𝑃 mod 6) ∈
∅ |
17 | 16 | pm2.21i 115 |
. . . . . . . . . . . 12
⊢ ((𝑃 mod 6) ∈ ∅ →
(𝑃 mod 6) ∈ {1,
5}) |
18 | | 5lt6 11081 |
. . . . . . . . . . . . 13
⊢ 5 <
6 |
19 | 3 | nnzi 11278 |
. . . . . . . . . . . . . 14
⊢ 6 ∈
ℤ |
20 | | 5nn 11065 |
. . . . . . . . . . . . . . 15
⊢ 5 ∈
ℕ |
21 | 20 | nnzi 11278 |
. . . . . . . . . . . . . 14
⊢ 5 ∈
ℤ |
22 | | fzn 12228 |
. . . . . . . . . . . . . 14
⊢ ((6
∈ ℤ ∧ 5 ∈ ℤ) → (5 < 6 ↔ (6...5) =
∅)) |
23 | 19, 21, 22 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ (5 < 6
↔ (6...5) = ∅) |
24 | 18, 23 | mpbi 219 |
. . . . . . . . . . . 12
⊢ (6...5) =
∅ |
25 | 17, 24 | eleq2s 2706 |
. . . . . . . . . . 11
⊢ ((𝑃 mod 6) ∈ (6...5) →
(𝑃 mod 6) ∈ {1,
5}) |
26 | 25 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → ((𝑃 mod 6) ∈ (6...5) →
(𝑃 mod 6) ∈ {1,
5})) |
27 | 15, 26 | pm3.2i 470 |
. . . . . . . . 9
⊢ (6 ≤ 6
∧ ((𝑃 ∈ ℙ
∧ 4 ≤ 𝑃) →
((𝑃 mod 6) ∈ (6...5)
→ (𝑃 mod 6) ∈ {1,
5}))) |
28 | | 5nn0 11189 |
. . . . . . . . 9
⊢ 5 ∈
ℕ0 |
29 | 20 | elexi 3186 |
. . . . . . . . . . 11
⊢ 5 ∈
V |
30 | 29 | prid2 4242 |
. . . . . . . . . 10
⊢ 5 ∈
{1, 5} |
31 | 30 | 3mix3i 1228 |
. . . . . . . . 9
⊢ (2
∥ 5 ∨ 3 ∥ 5 ∨ 5 ∈ {1, 5}) |
32 | 27, 28, 6, 31 | ppiublem1 24727 |
. . . . . . . 8
⊢ (5 ≤ 6
∧ ((𝑃 ∈ ℙ
∧ 4 ≤ 𝑃) →
((𝑃 mod 6) ∈ (5...5)
→ (𝑃 mod 6) ∈ {1,
5}))) |
33 | | 4nn0 11188 |
. . . . . . . 8
⊢ 4 ∈
ℕ0 |
34 | | df-5 10959 |
. . . . . . . 8
⊢ 5 = (4 +
1) |
35 | | 2z 11286 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
36 | | dvdsmul1 14841 |
. . . . . . . . . . 11
⊢ ((2
∈ ℤ ∧ 2 ∈ ℤ) → 2 ∥ (2 ·
2)) |
37 | 35, 35, 36 | mp2an 704 |
. . . . . . . . . 10
⊢ 2 ∥
(2 · 2) |
38 | | 2t2e4 11054 |
. . . . . . . . . 10
⊢ (2
· 2) = 4 |
39 | 37, 38 | breqtri 4608 |
. . . . . . . . 9
⊢ 2 ∥
4 |
40 | 39 | 3mix1i 1226 |
. . . . . . . 8
⊢ (2
∥ 4 ∨ 3 ∥ 4 ∨ 4 ∈ {1, 5}) |
41 | 32, 33, 34, 40 | ppiublem1 24727 |
. . . . . . 7
⊢ (4 ≤ 6
∧ ((𝑃 ∈ ℙ
∧ 4 ≤ 𝑃) →
((𝑃 mod 6) ∈ (4...5)
→ (𝑃 mod 6) ∈ {1,
5}))) |
42 | | 3nn0 11187 |
. . . . . . 7
⊢ 3 ∈
ℕ0 |
43 | | df-4 10958 |
. . . . . . 7
⊢ 4 = (3 +
1) |
44 | | 3z 11287 |
. . . . . . . . 9
⊢ 3 ∈
ℤ |
45 | | iddvds 14833 |
. . . . . . . . 9
⊢ (3 ∈
ℤ → 3 ∥ 3) |
46 | 44, 45 | ax-mp 5 |
. . . . . . . 8
⊢ 3 ∥
3 |
47 | 46 | 3mix2i 1227 |
. . . . . . 7
⊢ (2
∥ 3 ∨ 3 ∥ 3 ∨ 3 ∈ {1, 5}) |
48 | 41, 42, 43, 47 | ppiublem1 24727 |
. . . . . 6
⊢ (3 ≤ 6
∧ ((𝑃 ∈ ℙ
∧ 4 ≤ 𝑃) →
((𝑃 mod 6) ∈ (3...5)
→ (𝑃 mod 6) ∈ {1,
5}))) |
49 | | 2nn0 11186 |
. . . . . 6
⊢ 2 ∈
ℕ0 |
50 | | df-3 10957 |
. . . . . 6
⊢ 3 = (2 +
1) |
51 | | iddvds 14833 |
. . . . . . . 8
⊢ (2 ∈
ℤ → 2 ∥ 2) |
52 | 35, 51 | ax-mp 5 |
. . . . . . 7
⊢ 2 ∥
2 |
53 | 52 | 3mix1i 1226 |
. . . . . 6
⊢ (2
∥ 2 ∨ 3 ∥ 2 ∨ 2 ∈ {1, 5}) |
54 | 48, 49, 50, 53 | ppiublem1 24727 |
. . . . 5
⊢ (2 ≤ 6
∧ ((𝑃 ∈ ℙ
∧ 4 ≤ 𝑃) →
((𝑃 mod 6) ∈ (2...5)
→ (𝑃 mod 6) ∈ {1,
5}))) |
55 | | 1nn0 11185 |
. . . . 5
⊢ 1 ∈
ℕ0 |
56 | | df-2 10956 |
. . . . 5
⊢ 2 = (1 +
1) |
57 | | 1ex 9914 |
. . . . . . 7
⊢ 1 ∈
V |
58 | 57 | prid1 4241 |
. . . . . 6
⊢ 1 ∈
{1, 5} |
59 | 58 | 3mix3i 1228 |
. . . . 5
⊢ (2
∥ 1 ∨ 3 ∥ 1 ∨ 1 ∈ {1, 5}) |
60 | 54, 55, 56, 59 | ppiublem1 24727 |
. . . 4
⊢ (1 ≤ 6
∧ ((𝑃 ∈ ℙ
∧ 4 ≤ 𝑃) →
((𝑃 mod 6) ∈ (1...5)
→ (𝑃 mod 6) ∈ {1,
5}))) |
61 | | 0nn0 11184 |
. . . 4
⊢ 0 ∈
ℕ0 |
62 | | 1e0p1 11428 |
. . . 4
⊢ 1 = (0 +
1) |
63 | | dvds0 14835 |
. . . . . 6
⊢ (2 ∈
ℤ → 2 ∥ 0) |
64 | 35, 63 | ax-mp 5 |
. . . . 5
⊢ 2 ∥
0 |
65 | 64 | 3mix1i 1226 |
. . . 4
⊢ (2
∥ 0 ∨ 3 ∥ 0 ∨ 0 ∈ {1, 5}) |
66 | 60, 61, 62, 65 | ppiublem1 24727 |
. . 3
⊢ (0 ≤ 6
∧ ((𝑃 ∈ ℙ
∧ 4 ≤ 𝑃) →
((𝑃 mod 6) ∈ (0...5)
→ (𝑃 mod 6) ∈ {1,
5}))) |
67 | 66 | simpri 477 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → ((𝑃 mod 6) ∈ (0...5) →
(𝑃 mod 6) ∈ {1,
5})) |
68 | 13, 67 | mpd 15 |
1
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (𝑃 mod 6) ∈ {1,
5}) |