Proof of Theorem ppiublem1
| Step | Hyp | Ref
| Expression |
| 1 | | ppiublem1.1 |
. . . . . 6
⊢ (𝑁 ≤ 6 ∧ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → ((𝑃 mod 6) ∈ (𝑁...5) → (𝑃 mod 6) ∈ {1, 5}))) |
| 2 | 1 | simpli 483 |
. . . . 5
⊢ 𝑁 ≤ 6 |
| 3 | | ppiublem1.3 |
. . . . 5
⊢ 𝑁 = (𝑀 + 1) |
| 4 | | df-6 12333 |
. . . . 5
⊢ 6 = (5 +
1) |
| 5 | 2, 3, 4 | 3brtr3i 5172 |
. . . 4
⊢ (𝑀 + 1) ≤ (5 +
1) |
| 6 | | ppiublem1.2 |
. . . . . 6
⊢ 𝑀 ∈
ℕ0 |
| 7 | 6 | nn0rei 12537 |
. . . . 5
⊢ 𝑀 ∈ ℝ |
| 8 | | 5re 12353 |
. . . . 5
⊢ 5 ∈
ℝ |
| 9 | | 1re 11261 |
. . . . 5
⊢ 1 ∈
ℝ |
| 10 | 7, 8, 9 | leadd1i 11818 |
. . . 4
⊢ (𝑀 ≤ 5 ↔ (𝑀 + 1) ≤ (5 +
1)) |
| 11 | 5, 10 | mpbir 231 |
. . 3
⊢ 𝑀 ≤ 5 |
| 12 | | 6re 12356 |
. . . 4
⊢ 6 ∈
ℝ |
| 13 | | 5lt6 12447 |
. . . 4
⊢ 5 <
6 |
| 14 | 8, 12, 13 | ltleii 11384 |
. . 3
⊢ 5 ≤
6 |
| 15 | 7, 8, 12 | letri 11390 |
. . 3
⊢ ((𝑀 ≤ 5 ∧ 5 ≤ 6) →
𝑀 ≤ 6) |
| 16 | 11, 14, 15 | mp2an 692 |
. 2
⊢ 𝑀 ≤ 6 |
| 17 | 6 | nn0zi 12642 |
. . . . 5
⊢ 𝑀 ∈ ℤ |
| 18 | | 5nn 12352 |
. . . . . 6
⊢ 5 ∈
ℕ |
| 19 | 18 | nnzi 12641 |
. . . . 5
⊢ 5 ∈
ℤ |
| 20 | | eluz2 12884 |
. . . . 5
⊢ (5 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 5 ∈ ℤ ∧
𝑀 ≤ 5)) |
| 21 | 17, 19, 11, 20 | mpbir3an 1342 |
. . . 4
⊢ 5 ∈
(ℤ≥‘𝑀) |
| 22 | | elfzp12 13643 |
. . . 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 | | 2nn 12339 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ |
| 26 | | 6nn 12355 |
. . . . . . . . . . 11
⊢ 6 ∈
ℕ |
| 27 | | prmz 16712 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
| 28 | 27 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → 𝑃 ∈ ℤ) |
| 29 | | 3z 12650 |
. . . . . . . . . . . . . 14
⊢ 3 ∈
ℤ |
| 30 | | 2z 12649 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℤ |
| 31 | | dvdsmul2 16316 |
. . . . . . . . . . . . . 14
⊢ ((3
∈ ℤ ∧ 2 ∈ ℤ) → 2 ∥ (3 ·
2)) |
| 32 | 29, 30, 31 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ 2 ∥
(3 · 2) |
| 33 | | 3t2e6 12432 |
. . . . . . . . . . . . 13
⊢ (3
· 2) = 6 |
| 34 | 32, 33 | breqtri 5168 |
. . . . . . . . . . . 12
⊢ 2 ∥
6 |
| 35 | | dvdsmod 16366 |
. . . . . . . . . . . 12
⊢ (((2
∈ ℕ ∧ 6 ∈ ℕ ∧ 𝑃 ∈ ℤ) ∧ 2 ∥ 6) →
(2 ∥ (𝑃 mod 6) ↔
2 ∥ 𝑃)) |
| 36 | 34, 35 | mpan2 691 |
. . . . . . . . . . 11
⊢ ((2
∈ ℕ ∧ 6 ∈ ℕ ∧ 𝑃 ∈ ℤ) → (2 ∥ (𝑃 mod 6) ↔ 2 ∥ 𝑃)) |
| 37 | 25, 26, 28, 36 | mp3an12i 1467 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (2 ∥ (𝑃 mod 6) ↔ 2 ∥ 𝑃)) |
| 38 | | uzid 12893 |
. . . . . . . . . . . 12
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) |
| 39 | 30, 38 | ax-mp 5 |
. . . . . . . . . . 11
⊢ 2 ∈
(ℤ≥‘2) |
| 40 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → 𝑃 ∈ ℙ) |
| 41 | | dvdsprm 16740 |
. . . . . . . . . . 11
⊢ ((2
∈ (ℤ≥‘2) ∧ 𝑃 ∈ ℙ) → (2 ∥ 𝑃 ↔ 2 = 𝑃)) |
| 42 | 39, 40, 41 | sylancr 587 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (2 ∥ 𝑃 ↔ 2 = 𝑃)) |
| 43 | 37, 42 | bitrd 279 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (2 ∥ (𝑃 mod 6) ↔ 2 = 𝑃)) |
| 44 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → 4 ≤ 𝑃) |
| 45 | | breq2 5147 |
. . . . . . . . . . 11
⊢ (2 =
𝑃 → (4 ≤ 2 ↔ 4
≤ 𝑃)) |
| 46 | 44, 45 | syl5ibrcom 247 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (2 = 𝑃 → 4 ≤
2)) |
| 47 | | 2lt4 12441 |
. . . . . . . . . . . 12
⊢ 2 <
4 |
| 48 | | 2re 12340 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ |
| 49 | | 4re 12350 |
. . . . . . . . . . . . 13
⊢ 4 ∈
ℝ |
| 50 | 48, 49 | ltnlei 11382 |
. . . . . . . . . . . 12
⊢ (2 < 4
↔ ¬ 4 ≤ 2) |
| 51 | 47, 50 | mpbi 230 |
. . . . . . . . . . 11
⊢ ¬ 4
≤ 2 |
| 52 | 51 | pm2.21i 119 |
. . . . . . . . . 10
⊢ (4 ≤ 2
→ (𝑃 mod 6) ∈ {1,
5}) |
| 53 | 46, 52 | syl6 35 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (2 = 𝑃 → (𝑃 mod 6) ∈ {1, 5})) |
| 54 | 43, 53 | sylbid 240 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (2 ∥ (𝑃 mod 6) → (𝑃 mod 6) ∈ {1,
5})) |
| 55 | | breq2 5147 |
. . . . . . . . 9
⊢ ((𝑃 mod 6) = 𝑀 → (2 ∥ (𝑃 mod 6) ↔ 2 ∥ 𝑀)) |
| 56 | 55 | imbi1d 341 |
. . . . . . . 8
⊢ ((𝑃 mod 6) = 𝑀 → ((2 ∥ (𝑃 mod 6) → (𝑃 mod 6) ∈ {1, 5}) ↔ (2 ∥
𝑀 → (𝑃 mod 6) ∈ {1, 5}))) |
| 57 | 54, 56 | syl5ibcom 245 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → ((𝑃 mod 6) = 𝑀 → (2 ∥ 𝑀 → (𝑃 mod 6) ∈ {1, 5}))) |
| 58 | 57 | com3r 87 |
. . . . . 6
⊢ (2
∥ 𝑀 → ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → ((𝑃 mod 6) = 𝑀 → (𝑃 mod 6) ∈ {1, 5}))) |
| 59 | | 3nn 12345 |
. . . . . . . . . . 11
⊢ 3 ∈
ℕ |
| 60 | | dvdsmul1 16315 |
. . . . . . . . . . . . . 14
⊢ ((3
∈ ℤ ∧ 2 ∈ ℤ) → 3 ∥ (3 ·
2)) |
| 61 | 29, 30, 60 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ 3 ∥
(3 · 2) |
| 62 | 61, 33 | breqtri 5168 |
. . . . . . . . . . . 12
⊢ 3 ∥
6 |
| 63 | | dvdsmod 16366 |
. . . . . . . . . . . 12
⊢ (((3
∈ ℕ ∧ 6 ∈ ℕ ∧ 𝑃 ∈ ℤ) ∧ 3 ∥ 6) →
(3 ∥ (𝑃 mod 6) ↔
3 ∥ 𝑃)) |
| 64 | 62, 63 | mpan2 691 |
. . . . . . . . . . 11
⊢ ((3
∈ ℕ ∧ 6 ∈ ℕ ∧ 𝑃 ∈ ℤ) → (3 ∥ (𝑃 mod 6) ↔ 3 ∥ 𝑃)) |
| 65 | 59, 26, 28, 64 | mp3an12i 1467 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (3 ∥ (𝑃 mod 6) ↔ 3 ∥ 𝑃)) |
| 66 | | df-3 12330 |
. . . . . . . . . . . 12
⊢ 3 = (2 +
1) |
| 67 | | peano2uz 12943 |
. . . . . . . . . . . . 13
⊢ (2 ∈
(ℤ≥‘2) → (2 + 1) ∈
(ℤ≥‘2)) |
| 68 | 39, 67 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (2 + 1)
∈ (ℤ≥‘2) |
| 69 | 66, 68 | eqeltri 2837 |
. . . . . . . . . . 11
⊢ 3 ∈
(ℤ≥‘2) |
| 70 | | dvdsprm 16740 |
. . . . . . . . . . 11
⊢ ((3
∈ (ℤ≥‘2) ∧ 𝑃 ∈ ℙ) → (3 ∥ 𝑃 ↔ 3 = 𝑃)) |
| 71 | 69, 40, 70 | sylancr 587 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (3 ∥ 𝑃 ↔ 3 = 𝑃)) |
| 72 | 65, 71 | bitrd 279 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (3 ∥ (𝑃 mod 6) ↔ 3 = 𝑃)) |
| 73 | | breq2 5147 |
. . . . . . . . . . 11
⊢ (3 =
𝑃 → (4 ≤ 3 ↔ 4
≤ 𝑃)) |
| 74 | 44, 73 | syl5ibrcom 247 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (3 = 𝑃 → 4 ≤
3)) |
| 75 | | 3lt4 12440 |
. . . . . . . . . . . 12
⊢ 3 <
4 |
| 76 | | 3re 12346 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℝ |
| 77 | 76, 49 | ltnlei 11382 |
. . . . . . . . . . . 12
⊢ (3 < 4
↔ ¬ 4 ≤ 3) |
| 78 | 75, 77 | mpbi 230 |
. . . . . . . . . . 11
⊢ ¬ 4
≤ 3 |
| 79 | 78 | pm2.21i 119 |
. . . . . . . . . 10
⊢ (4 ≤ 3
→ (𝑃 mod 6) ∈ {1,
5}) |
| 80 | 74, 79 | syl6 35 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (3 = 𝑃 → (𝑃 mod 6) ∈ {1, 5})) |
| 81 | 72, 80 | sylbid 240 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (3 ∥ (𝑃 mod 6) → (𝑃 mod 6) ∈ {1,
5})) |
| 82 | | breq2 5147 |
. . . . . . . . 9
⊢ ((𝑃 mod 6) = 𝑀 → (3 ∥ (𝑃 mod 6) ↔ 3 ∥ 𝑀)) |
| 83 | 82 | imbi1d 341 |
. . . . . . . 8
⊢ ((𝑃 mod 6) = 𝑀 → ((3 ∥ (𝑃 mod 6) → (𝑃 mod 6) ∈ {1, 5}) ↔ (3 ∥
𝑀 → (𝑃 mod 6) ∈ {1, 5}))) |
| 84 | 81, 83 | syl5ibcom 245 |
. . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → ((𝑃 mod 6) = 𝑀 → (3 ∥ 𝑀 → (𝑃 mod 6) ∈ {1, 5}))) |
| 85 | 84 | com3r 87 |
. . . . . 6
⊢ (3
∥ 𝑀 → ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → ((𝑃 mod 6) = 𝑀 → (𝑃 mod 6) ∈ {1, 5}))) |
| 86 | | eleq1a 2836 |
. . . . . . 7
⊢ (𝑀 ∈ {1, 5} → ((𝑃 mod 6) = 𝑀 → (𝑃 mod 6) ∈ {1, 5})) |
| 87 | 86 | a1d 25 |
. . . . . 6
⊢ (𝑀 ∈ {1, 5} → ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → ((𝑃 mod 6) = 𝑀 → (𝑃 mod 6) ∈ {1, 5}))) |
| 88 | 58, 85, 87 | 3jaoi 1430 |
. . . . 5
⊢ ((2
∥ 𝑀 ∨ 3 ∥
𝑀 ∨ 𝑀 ∈ {1, 5}) → ((𝑃 ∈ ℙ ∧ 4 ≤ 𝑃) → ((𝑃 mod 6) = 𝑀 → (𝑃 mod 6) ∈ {1, 5}))) |
| 89 | 24, 88 | ax-mp 5 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → ((𝑃 mod 6) = 𝑀 → (𝑃 mod 6) ∈ {1, 5})) |
| 90 | 3 | oveq1i 7441 |
. . . . . 6
⊢ (𝑁...5) = ((𝑀 + 1)...5) |
| 91 | 90 | eleq2i 2833 |
. . . . 5
⊢ ((𝑃 mod 6) ∈ (𝑁...5) ↔ (𝑃 mod 6) ∈ ((𝑀 + 1)...5)) |
| 92 | 1 | simpri 485 |
. . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → ((𝑃 mod 6) ∈ (𝑁...5) → (𝑃 mod 6) ∈ {1, 5})) |
| 93 | 91, 92 | biimtrrid 243 |
. . . 4
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → ((𝑃 mod 6) ∈ ((𝑀 + 1)...5) → (𝑃 mod 6) ∈ {1,
5})) |
| 94 | 89, 93 | jaod 860 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → (((𝑃 mod 6) = 𝑀 ∨ (𝑃 mod 6) ∈ ((𝑀 + 1)...5)) → (𝑃 mod 6) ∈ {1, 5})) |
| 95 | 23, 94 | biimtrid 242 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → ((𝑃 mod 6) ∈ (𝑀...5) → (𝑃 mod 6) ∈ {1, 5})) |
| 96 | 16, 95 | pm3.2i 470 |
1
⊢ (𝑀 ≤ 6 ∧ ((𝑃 ∈ ℙ ∧ 4 ≤
𝑃) → ((𝑃 mod 6) ∈ (𝑀...5) → (𝑃 mod 6) ∈ {1, 5}))) |