Metamath Proof Explorer

Theorem prm23ge5

Description: A prime is either 2 or 3 or greater than or equal to 5. (Contributed by AV, 5-Jul-2021)

Ref Expression
Assertion prm23ge5 ⊢ P ∈ ℙ → P = 2 ∨ P = 3 ∨ P ∈ ℤ ≥ 5

Proof

Step Hyp Ref Expression
1 ax-1 ⊢ P = 2 ∨ P = 3 ∨ P ∈ ℤ ≥ 5 → P ∈ ℙ → P = 2 ∨ P = 3 ∨ P ∈ ℤ ≥ 5
2 3ioran ⊢ ¬ P = 2 ∨ P = 3 ∨ P ∈ ℤ ≥ 5 ↔ ¬ P = 2 ∧ ¬ P = 3 ∧ ¬ P ∈ ℤ ≥ 5
3 3ianor ⊢ ¬ 5 ∈ ℤ ∧ P ∈ ℤ ∧ 5 ≤ P ↔ ¬ 5 ∈ ℤ ∨ ¬ P ∈ ℤ ∨ ¬ 5 ≤ P
4 eluz2 ⊢ P ∈ ℤ ≥ 5 ↔ 5 ∈ ℤ ∧ P ∈ ℤ ∧ 5 ≤ P
5 3 4 xchnxbir ⊢ ¬ P ∈ ℤ ≥ 5 ↔ ¬ 5 ∈ ℤ ∨ ¬ P ∈ ℤ ∨ ¬ 5 ≤ P
6 5nn ⊢ 5 ∈ ℕ
7 6 nnzi ⊢ 5 ∈ ℤ
8 7 pm2.24i ⊢ ¬ 5 ∈ ℤ → ¬ P = 2 ∧ ¬ P = 3 → P ∈ ℙ → P = 2 ∨ P = 3 ∨ P ∈ ℤ ≥ 5
9 pm2.24 ⊢ P ∈ ℤ → ¬ P ∈ ℤ → P = 2 ∨ P = 3 ∨ P ∈ ℤ ≥ 5
10 prmz ⊢ P ∈ ℙ → P ∈ ℤ
11 9 10 syl11 ⊢ ¬ P ∈ ℤ → P ∈ ℙ → P = 2 ∨ P = 3 ∨ P ∈ ℤ ≥ 5
12 11 a1d ⊢ ¬ P ∈ ℤ → ¬ P = 2 ∧ ¬ P = 3 → P ∈ ℙ → P = 2 ∨ P = 3 ∨ P ∈ ℤ ≥ 5
13 10 zred ⊢ P ∈ ℙ → P ∈ ℝ
14 5re ⊢ 5 ∈ ℝ
15 14 a1i ⊢ P ∈ ℙ → 5 ∈ ℝ
16 13 15 ltnled ⊢ P ∈ ℙ → P < 5 ↔ ¬ 5 ≤ P
17 prm23lt5 ⊢ P ∈ ℙ ∧ P < 5 → P = 2 ∨ P = 3
18 ioran ⊢ ¬ P = 2 ∨ P = 3 ↔ ¬ P = 2 ∧ ¬ P = 3
19 pm2.24 ⊢ P = 2 ∨ P = 3 → ¬ P = 2 ∨ P = 3 → P = 2 ∨ P = 3 ∨ P ∈ ℤ ≥ 5
20 18 19 biimtrrid ⊢ P = 2 ∨ P = 3 → ¬ P = 2 ∧ ¬ P = 3 → P = 2 ∨ P = 3 ∨ P ∈ ℤ ≥ 5
21 17 20 syl ⊢ P ∈ ℙ ∧ P < 5 → ¬ P = 2 ∧ ¬ P = 3 → P = 2 ∨ P = 3 ∨ P ∈ ℤ ≥ 5
22 21 ex ⊢ P ∈ ℙ → P < 5 → ¬ P = 2 ∧ ¬ P = 3 → P = 2 ∨ P = 3 ∨ P ∈ ℤ ≥ 5
23 16 22 sylbird ⊢ P ∈ ℙ → ¬ 5 ≤ P → ¬ P = 2 ∧ ¬ P = 3 → P = 2 ∨ P = 3 ∨ P ∈ ℤ ≥ 5
24 23 com3l ⊢ ¬ 5 ≤ P → ¬ P = 2 ∧ ¬ P = 3 → P ∈ ℙ → P = 2 ∨ P = 3 ∨ P ∈ ℤ ≥ 5
25 8 12 24 3jaoi ⊢ ¬ 5 ∈ ℤ ∨ ¬ P ∈ ℤ ∨ ¬ 5 ≤ P → ¬ P = 2 ∧ ¬ P = 3 → P ∈ ℙ → P = 2 ∨ P = 3 ∨ P ∈ ℤ ≥ 5
26 5 25 sylbi ⊢ ¬ P ∈ ℤ ≥ 5 → ¬ P = 2 ∧ ¬ P = 3 → P ∈ ℙ → P = 2 ∨ P = 3 ∨ P ∈ ℤ ≥ 5
27 26 com12 ⊢ ¬ P = 2 ∧ ¬ P = 3 → ¬ P ∈ ℤ ≥ 5 → P ∈ ℙ → P = 2 ∨ P = 3 ∨ P ∈ ℤ ≥ 5
28 27 3impia ⊢ ¬ P = 2 ∧ ¬ P = 3 ∧ ¬ P ∈ ℤ ≥ 5 → P ∈ ℙ → P = 2 ∨ P = 3 ∨ P ∈ ℤ ≥ 5
29 2 28 sylbi ⊢ ¬ P = 2 ∨ P = 3 ∨ P ∈ ℤ ≥ 5 → P ∈ ℙ → P = 2 ∨ P = 3 ∨ P ∈ ℤ ≥ 5
30 1 29 pm2.61i ⊢ P ∈ ℙ → P = 2 ∨ P = 3 ∨ P ∈ ℤ ≥ 5