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 ( 𝑃 ∈ ℙ → ( 𝑃 = 2 ∨ 𝑃 = 3 ∨ 𝑃 ∈ ( ℤ≥ ‘ 5 ) ) )

Proof

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