Proof of Theorem ppiublem1
Step | Hyp | Ref
| Expression |
1 | | ppiublem1.1 |
. . . . . 6
⊢ (𝑁 ≤ 6 ∧ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → ((𝑃 mod 6) ∈ (𝑁...5) → (𝑃 mod 6) ∈ {1, 5}))) |
2 | 1 | simpli 473 |
. . . . 5
⊢ 𝑁 ≤ 6 |
3 | | ppiublem1.3 |
. . . . 5
⊢ 𝑁 = (𝑀 + 1) |
4 | | df-6 10960 |
. . . . 5
⊢ 6 = (5 +
1) |
5 | 2, 3, 4 | 3brtr3i 4612 |
. . . 4
⊢ (𝑀 + 1) ≤ (5 +
1) |
6 | | ppiublem1.2 |
. . . . . 6
⊢ 𝑀 ∈
ℕ0 |
7 | 6 | nn0rei 11180 |
. . . . 5
⊢ 𝑀 ∈ ℝ |
8 | | 5re 10976 |
. . . . 5
⊢ 5 ∈
ℝ |
9 | | 1re 9918 |
. . . . 5
⊢ 1 ∈
ℝ |
10 | 7, 8, 9 | leadd1i 10462 |
. . . 4
⊢ (𝑀 ≤ 5 ↔ (𝑀 + 1) ≤ (5 +
1)) |
11 | 5, 10 | mpbir 220 |
. . 3
⊢ 𝑀 ≤ 5 |
12 | | 6re 10978 |
. . . 4
⊢ 6 ∈
ℝ |
13 | | 5lt6 11081 |
. . . 4
⊢ 5 <
6 |
14 | 8, 12, 13 | ltleii 10039 |
. . 3
⊢ 5 ≤
6 |
15 | 7, 8, 12 | letri 10045 |
. . 3
⊢ ((𝑀 ≤ 5 ∧ 5 ≤ 6) →
𝑀 ≤ 6) |
16 | 11, 14, 15 | mp2an 704 |
. 2
⊢ 𝑀 ≤ 6 |
17 | 6 | nn0zi 11279 |
. . . . 5
⊢ 𝑀 ∈ ℤ |
18 | | 5nn 11065 |
. . . . . 6
⊢ 5 ∈
ℕ |
19 | 18 | nnzi 11278 |
. . . . 5
⊢ 5 ∈
ℤ |
20 | | eluz2 11569 |
. . . . 5
⊢ (5 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 5 ∈ ℤ ∧
𝑀 ≤ 5)) |
21 | 17, 19, 11, 20 | mpbir3an 1237 |
. . . 4
⊢ 5 ∈
(ℤ≥‘𝑀) |
22 | | elfzp12 12288 |
. . . 4
⊢ (5 ∈
(ℤ≥‘𝑀) → ((𝑃 mod 6) ∈ (𝑀...5) ↔ ((𝑃 mod 6) = 𝑀 ∨ (𝑃 mod 6) ∈ ((𝑀 + 1)...5)))) |
23 | 21, 22 | ax-mp 5 |
. . 3
⊢ ((𝑃 mod 6) ∈ (𝑀...5) ↔ ((𝑃 mod 6) = 𝑀 ∨ (𝑃 mod 6) ∈ ((𝑀 + 1)...5))) |
24 | | ppiublem1.4 |
. . . . 5
⊢ (2
∥ 𝑀 ∨ 3 ∥
𝑀 ∨ 𝑀 ∈ {1, 5}) |
25 | | prmz 15227 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
26 | 25 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → 𝑃 ∈ ℤ) |
27 | | 2nn 11062 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ |
28 | | 6nn 11066 |
. . . . . . . . . . . 12
⊢ 6 ∈
ℕ |
29 | | 3z 11287 |
. . . . . . . . . . . . . . 15
⊢ 3 ∈
ℤ |
30 | | 2z 11286 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℤ |
31 | | dvdsmul2 14842 |
. . . . . . . . . . . . . . 15
⊢ ((3
∈ ℤ ∧ 2 ∈ ℤ) → 2 ∥ (3 ·
2)) |
32 | 29, 30, 31 | mp2an 704 |
. . . . . . . . . . . . . 14
⊢ 2 ∥
(3 · 2) |
33 | | 3t2e6 11056 |
. . . . . . . . . . . . . 14
⊢ (3
· 2) = 6 |
34 | 32, 33 | breqtri 4608 |
. . . . . . . . . . . . 13
⊢ 2 ∥
6 |
35 | | dvdsmod 14888 |
. . . . . . . . . . . . 13
⊢ (((2
∈ ℕ ∧ 6 ∈ ℕ ∧ 𝑃 ∈ ℤ) ∧ 2 ∥ 6) →
(2 ∥ (𝑃 mod 6) ↔
2 ∥ 𝑃)) |
36 | 34, 35 | mpan2 703 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℕ ∧ 6 ∈ ℕ ∧ 𝑃 ∈ ℤ) → (2 ∥ (𝑃 mod 6) ↔ 2 ∥ 𝑃)) |
37 | 27, 28, 36 | mp3an12 1406 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ ℤ → (2
∥ (𝑃 mod 6) ↔ 2
∥ 𝑃)) |
38 | 26, 37 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (2 ∥ (𝑃 mod 6) ↔ 2 ∥ 𝑃)) |
39 | | uzid 11578 |
. . . . . . . . . . . 12
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) |
40 | 30, 39 | ax-mp 5 |
. . . . . . . . . . 11
⊢ 2 ∈
(ℤ≥‘2) |
41 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → 𝑃 ∈ ℙ) |
42 | | dvdsprm 15253 |
. . . . . . . . . . 11
⊢ ((2
∈ (ℤ≥‘2) ∧ 𝑃 ∈ ℙ) → (2 ∥ 𝑃 ↔ 2 = 𝑃)) |
43 | 40, 41, 42 | sylancr 694 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (2 ∥ 𝑃 ↔ 2 = 𝑃)) |
44 | 38, 43 | bitrd 267 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (2 ∥ (𝑃 mod 6) ↔ 2 = 𝑃)) |
45 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → 4 ≤ 𝑃) |
46 | | breq2 4587 |
. . . . . . . . . . 11
⊢ (2 =
𝑃 → (4 ≤ 2 ↔ 4
≤ 𝑃)) |
47 | 45, 46 | syl5ibrcom 236 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (2 = 𝑃 → 4 ≤
2)) |
48 | | 2lt4 11075 |
. . . . . . . . . . . 12
⊢ 2 <
4 |
49 | | 2re 10967 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ |
50 | | 4re 10974 |
. . . . . . . . . . . . 13
⊢ 4 ∈
ℝ |
51 | 49, 50 | ltnlei 10037 |
. . . . . . . . . . . 12
⊢ (2 < 4
↔ ¬ 4 ≤ 2) |
52 | 48, 51 | mpbi 219 |
. . . . . . . . . . 11
⊢ ¬ 4
≤ 2 |
53 | 52 | pm2.21i 115 |
. . . . . . . . . 10
⊢ (4 ≤ 2
→ (𝑃 mod 6) ∈ {1,
5}) |
54 | 47, 53 | syl6 34 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (2 = 𝑃 → (𝑃 mod 6) ∈ {1, 5})) |
55 | 44, 54 | sylbid 229 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (2 ∥ (𝑃 mod 6) → (𝑃 mod 6) ∈ {1,
5})) |
56 | | breq2 4587 |
. . . . . . . . 9
⊢ ((𝑃 mod 6) = 𝑀 → (2 ∥ (𝑃 mod 6) ↔ 2 ∥ 𝑀)) |
57 | 56 | imbi1d 330 |
. . . . . . . 8
⊢ ((𝑃 mod 6) = 𝑀 → ((2 ∥ (𝑃 mod 6) → (𝑃 mod 6) ∈ {1, 5}) ↔ (2 ∥
𝑀 → (𝑃 mod 6) ∈ {1, 5}))) |
58 | 55, 57 | syl5ibcom 234 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → ((𝑃 mod 6) = 𝑀 → (2 ∥ 𝑀 → (𝑃 mod 6) ∈ {1, 5}))) |
59 | 58 | com3r 85 |
. . . . . 6
⊢ (2
∥ 𝑀 → ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → ((𝑃 mod 6) = 𝑀 → (𝑃 mod 6) ∈ {1, 5}))) |
60 | | 3nn 11063 |
. . . . . . . . . . . 12
⊢ 3 ∈
ℕ |
61 | | dvdsmul1 14841 |
. . . . . . . . . . . . . . 15
⊢ ((3
∈ ℤ ∧ 2 ∈ ℤ) → 3 ∥ (3 ·
2)) |
62 | 29, 30, 61 | mp2an 704 |
. . . . . . . . . . . . . 14
⊢ 3 ∥
(3 · 2) |
63 | 62, 33 | breqtri 4608 |
. . . . . . . . . . . . 13
⊢ 3 ∥
6 |
64 | | dvdsmod 14888 |
. . . . . . . . . . . . 13
⊢ (((3
∈ ℕ ∧ 6 ∈ ℕ ∧ 𝑃 ∈ ℤ) ∧ 3 ∥ 6) →
(3 ∥ (𝑃 mod 6) ↔
3 ∥ 𝑃)) |
65 | 63, 64 | mpan2 703 |
. . . . . . . . . . . 12
⊢ ((3
∈ ℕ ∧ 6 ∈ ℕ ∧ 𝑃 ∈ ℤ) → (3 ∥ (𝑃 mod 6) ↔ 3 ∥ 𝑃)) |
66 | 60, 28, 65 | mp3an12 1406 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ ℤ → (3
∥ (𝑃 mod 6) ↔ 3
∥ 𝑃)) |
67 | 26, 66 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (3 ∥ (𝑃 mod 6) ↔ 3 ∥ 𝑃)) |
68 | | df-3 10957 |
. . . . . . . . . . . 12
⊢ 3 = (2 +
1) |
69 | | peano2uz 11617 |
. . . . . . . . . . . . 13
⊢ (2 ∈
(ℤ≥‘2) → (2 + 1) ∈
(ℤ≥‘2)) |
70 | 40, 69 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (2 + 1)
∈ (ℤ≥‘2) |
71 | 68, 70 | eqeltri 2684 |
. . . . . . . . . . 11
⊢ 3 ∈
(ℤ≥‘2) |
72 | | dvdsprm 15253 |
. . . . . . . . . . 11
⊢ ((3
∈ (ℤ≥‘2) ∧ 𝑃 ∈ ℙ) → (3 ∥ 𝑃 ↔ 3 = 𝑃)) |
73 | 71, 41, 72 | sylancr 694 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (3 ∥ 𝑃 ↔ 3 = 𝑃)) |
74 | 67, 73 | bitrd 267 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (3 ∥ (𝑃 mod 6) ↔ 3 = 𝑃)) |
75 | | breq2 4587 |
. . . . . . . . . . 11
⊢ (3 =
𝑃 → (4 ≤ 3 ↔ 4
≤ 𝑃)) |
76 | 45, 75 | syl5ibrcom 236 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (3 = 𝑃 → 4 ≤
3)) |
77 | | 3lt4 11074 |
. . . . . . . . . . . 12
⊢ 3 <
4 |
78 | | 3re 10971 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℝ |
79 | 78, 50 | ltnlei 10037 |
. . . . . . . . . . . 12
⊢ (3 < 4
↔ ¬ 4 ≤ 3) |
80 | 77, 79 | mpbi 219 |
. . . . . . . . . . 11
⊢ ¬ 4
≤ 3 |
81 | 80 | pm2.21i 115 |
. . . . . . . . . 10
⊢ (4 ≤ 3
→ (𝑃 mod 6) ∈ {1,
5}) |
82 | 76, 81 | syl6 34 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (3 = 𝑃 → (𝑃 mod 6) ∈ {1, 5})) |
83 | 74, 82 | sylbid 229 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (3 ∥ (𝑃 mod 6) → (𝑃 mod 6) ∈ {1,
5})) |
84 | | breq2 4587 |
. . . . . . . . 9
⊢ ((𝑃 mod 6) = 𝑀 → (3 ∥ (𝑃 mod 6) ↔ 3 ∥ 𝑀)) |
85 | 84 | imbi1d 330 |
. . . . . . . 8
⊢ ((𝑃 mod 6) = 𝑀 → ((3 ∥ (𝑃 mod 6) → (𝑃 mod 6) ∈ {1, 5}) ↔ (3 ∥
𝑀 → (𝑃 mod 6) ∈ {1, 5}))) |
86 | 83, 85 | syl5ibcom 234 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → ((𝑃 mod 6) = 𝑀 → (3 ∥ 𝑀 → (𝑃 mod 6) ∈ {1, 5}))) |
87 | 86 | com3r 85 |
. . . . . 6
⊢ (3
∥ 𝑀 → ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → ((𝑃 mod 6) = 𝑀 → (𝑃 mod 6) ∈ {1, 5}))) |
88 | | eleq1a 2683 |
. . . . . . 7
⊢ (𝑀 ∈ {1, 5} → ((𝑃 mod 6) = 𝑀 → (𝑃 mod 6) ∈ {1, 5})) |
89 | 88 | a1d 25 |
. . . . . 6
⊢ (𝑀 ∈ {1, 5} → ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → ((𝑃 mod 6) = 𝑀 → (𝑃 mod 6) ∈ {1, 5}))) |
90 | 59, 87, 89 | 3jaoi 1383 |
. . . . 5
⊢ ((2
∥ 𝑀 ∨ 3 ∥
𝑀 ∨ 𝑀 ∈ {1, 5}) → ((𝑃 ∈ ℙ ∧ 4 ≤ 𝑃) → ((𝑃 mod 6) = 𝑀 → (𝑃 mod 6) ∈ {1, 5}))) |
91 | 24, 90 | ax-mp 5 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → ((𝑃 mod 6) = 𝑀 → (𝑃 mod 6) ∈ {1, 5})) |
92 | 3 | oveq1i 6559 |
. . . . . 6
⊢ (𝑁...5) = ((𝑀 + 1)...5) |
93 | 92 | eleq2i 2680 |
. . . . 5
⊢ ((𝑃 mod 6) ∈ (𝑁...5) ↔ (𝑃 mod 6) ∈ ((𝑀 + 1)...5)) |
94 | 1 | simpri 477 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → ((𝑃 mod 6) ∈ (𝑁...5) → (𝑃 mod 6) ∈ {1, 5})) |
95 | 93, 94 | syl5bir 232 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → ((𝑃 mod 6) ∈ ((𝑀 + 1)...5) → (𝑃 mod 6) ∈ {1,
5})) |
96 | 91, 95 | jaod 394 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (((𝑃 mod 6) = 𝑀 ∨ (𝑃 mod 6) ∈ ((𝑀 + 1)...5)) → (𝑃 mod 6) ∈ {1, 5})) |
97 | 23, 96 | syl5bi 231 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → ((𝑃 mod 6) ∈ (𝑀...5) → (𝑃 mod 6) ∈ {1, 5})) |
98 | 16, 97 | pm3.2i 470 |
1
⊢ (𝑀 ≤ 6 ∧ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → ((𝑃 mod 6) ∈ (𝑀...5) → (𝑃 mod 6) ∈ {1, 5}))) |