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