Proof of Theorem prm23lt5
| Step | Hyp | Ref
| Expression |
| 1 | | prmnn 16711 |
. . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
| 2 | 1 | nnnn0d 12587 |
. . . 4
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ0) |
| 3 | 2 | adantr 480 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 < 5) → 𝑃 ∈
ℕ0) |
| 4 | | 4nn0 12545 |
. . . 4
⊢ 4 ∈
ℕ0 |
| 5 | 4 | a1i 11 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 < 5) → 4 ∈
ℕ0) |
| 6 | | df-5 12332 |
. . . . . 6
⊢ 5 = (4 +
1) |
| 7 | 6 | breq2i 5151 |
. . . . 5
⊢ (𝑃 < 5 ↔ 𝑃 < (4 + 1)) |
| 8 | | prmz 16712 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
| 9 | | 4z 12651 |
. . . . . . 7
⊢ 4 ∈
ℤ |
| 10 | | zleltp1 12668 |
. . . . . . 7
⊢ ((𝑃 ∈ ℤ ∧ 4 ∈
ℤ) → (𝑃 ≤ 4
↔ 𝑃 < (4 +
1))) |
| 11 | 8, 9, 10 | sylancl 586 |
. . . . . 6
⊢ (𝑃 ∈ ℙ → (𝑃 ≤ 4 ↔ 𝑃 < (4 + 1))) |
| 12 | 11 | biimprd 248 |
. . . . 5
⊢ (𝑃 ∈ ℙ → (𝑃 < (4 + 1) → 𝑃 ≤ 4)) |
| 13 | 7, 12 | biimtrid 242 |
. . . 4
⊢ (𝑃 ∈ ℙ → (𝑃 < 5 → 𝑃 ≤ 4)) |
| 14 | 13 | imp 406 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 < 5) → 𝑃 ≤ 4) |
| 15 | | elfz2nn0 13658 |
. . 3
⊢ (𝑃 ∈ (0...4) ↔ (𝑃 ∈ ℕ0
∧ 4 ∈ ℕ0 ∧ 𝑃 ≤ 4)) |
| 16 | 3, 5, 14, 15 | syl3anbrc 1344 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 < 5) → 𝑃 ∈
(0...4)) |
| 17 | | fz0to4untppr 13670 |
. . . 4
⊢ (0...4) =
({0, 1, 2} ∪ {3, 4}) |
| 18 | 17 | eleq2i 2833 |
. . 3
⊢ (𝑃 ∈ (0...4) ↔ 𝑃 ∈ ({0, 1, 2} ∪ {3,
4})) |
| 19 | | elun 4153 |
. . . . . 6
⊢ (𝑃 ∈ ({0, 1, 2} ∪ {3, 4})
↔ (𝑃 ∈ {0, 1, 2}
∨ 𝑃 ∈ {3,
4})) |
| 20 | | eltpi 4688 |
. . . . . . . 8
⊢ (𝑃 ∈ {0, 1, 2} → (𝑃 = 0 ∨ 𝑃 = 1 ∨ 𝑃 = 2)) |
| 21 | | nnne0 12300 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ ℕ → 𝑃 ≠ 0) |
| 22 | | eqneqall 2951 |
. . . . . . . . . . . 12
⊢ (𝑃 = 0 → (𝑃 ≠ 0 → (𝑃 = 2 ∨ 𝑃 = 3))) |
| 23 | 22 | com12 32 |
. . . . . . . . . . 11
⊢ (𝑃 ≠ 0 → (𝑃 = 0 → (𝑃 = 2 ∨ 𝑃 = 3))) |
| 24 | 1, 21, 23 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → (𝑃 = 0 → (𝑃 = 2 ∨ 𝑃 = 3))) |
| 25 | 24 | com12 32 |
. . . . . . . . 9
⊢ (𝑃 = 0 → (𝑃 ∈ ℙ → (𝑃 = 2 ∨ 𝑃 = 3))) |
| 26 | | eleq1 2829 |
. . . . . . . . . 10
⊢ (𝑃 = 1 → (𝑃 ∈ ℙ ↔ 1 ∈
ℙ)) |
| 27 | | 1nprm 16716 |
. . . . . . . . . . 11
⊢ ¬ 1
∈ ℙ |
| 28 | 27 | pm2.21i 119 |
. . . . . . . . . 10
⊢ (1 ∈
ℙ → (𝑃 = 2 ∨
𝑃 = 3)) |
| 29 | 26, 28 | biimtrdi 253 |
. . . . . . . . 9
⊢ (𝑃 = 1 → (𝑃 ∈ ℙ → (𝑃 = 2 ∨ 𝑃 = 3))) |
| 30 | | orc 868 |
. . . . . . . . . 10
⊢ (𝑃 = 2 → (𝑃 = 2 ∨ 𝑃 = 3)) |
| 31 | 30 | a1d 25 |
. . . . . . . . 9
⊢ (𝑃 = 2 → (𝑃 ∈ ℙ → (𝑃 = 2 ∨ 𝑃 = 3))) |
| 32 | 25, 29, 31 | 3jaoi 1430 |
. . . . . . . 8
⊢ ((𝑃 = 0 ∨ 𝑃 = 1 ∨ 𝑃 = 2) → (𝑃 ∈ ℙ → (𝑃 = 2 ∨ 𝑃 = 3))) |
| 33 | 20, 32 | syl 17 |
. . . . . . 7
⊢ (𝑃 ∈ {0, 1, 2} → (𝑃 ∈ ℙ → (𝑃 = 2 ∨ 𝑃 = 3))) |
| 34 | | elpri 4649 |
. . . . . . . 8
⊢ (𝑃 ∈ {3, 4} → (𝑃 = 3 ∨ 𝑃 = 4)) |
| 35 | | olc 869 |
. . . . . . . . . 10
⊢ (𝑃 = 3 → (𝑃 = 2 ∨ 𝑃 = 3)) |
| 36 | 35 | a1d 25 |
. . . . . . . . 9
⊢ (𝑃 = 3 → (𝑃 ∈ ℙ → (𝑃 = 2 ∨ 𝑃 = 3))) |
| 37 | | eleq1 2829 |
. . . . . . . . . 10
⊢ (𝑃 = 4 → (𝑃 ∈ ℙ ↔ 4 ∈
ℙ)) |
| 38 | | 4nprm 16732 |
. . . . . . . . . . 11
⊢ ¬ 4
∈ ℙ |
| 39 | 38 | pm2.21i 119 |
. . . . . . . . . 10
⊢ (4 ∈
ℙ → (𝑃 = 2 ∨
𝑃 = 3)) |
| 40 | 37, 39 | biimtrdi 253 |
. . . . . . . . 9
⊢ (𝑃 = 4 → (𝑃 ∈ ℙ → (𝑃 = 2 ∨ 𝑃 = 3))) |
| 41 | 36, 40 | jaoi 858 |
. . . . . . . 8
⊢ ((𝑃 = 3 ∨ 𝑃 = 4) → (𝑃 ∈ ℙ → (𝑃 = 2 ∨ 𝑃 = 3))) |
| 42 | 34, 41 | syl 17 |
. . . . . . 7
⊢ (𝑃 ∈ {3, 4} → (𝑃 ∈ ℙ → (𝑃 = 2 ∨ 𝑃 = 3))) |
| 43 | 33, 42 | jaoi 858 |
. . . . . 6
⊢ ((𝑃 ∈ {0, 1, 2} ∨ 𝑃 ∈ {3, 4}) → (𝑃 ∈ ℙ → (𝑃 = 2 ∨ 𝑃 = 3))) |
| 44 | 19, 43 | sylbi 217 |
. . . . 5
⊢ (𝑃 ∈ ({0, 1, 2} ∪ {3, 4})
→ (𝑃 ∈ ℙ
→ (𝑃 = 2 ∨ 𝑃 = 3))) |
| 45 | 44 | com12 32 |
. . . 4
⊢ (𝑃 ∈ ℙ → (𝑃 ∈ ({0, 1, 2} ∪ {3, 4})
→ (𝑃 = 2 ∨ 𝑃 = 3))) |
| 46 | 45 | adantr 480 |
. . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 < 5) → (𝑃 ∈ ({0, 1, 2} ∪ {3, 4})
→ (𝑃 = 2 ∨ 𝑃 = 3))) |
| 47 | 18, 46 | biimtrid 242 |
. 2
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 < 5) → (𝑃 ∈ (0...4) → (𝑃 = 2 ∨ 𝑃 = 3))) |
| 48 | 16, 47 | mpd 15 |
1
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 < 5) → (𝑃 = 2 ∨ 𝑃 = 3)) |