This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. Prime -> ( P = 2 \/ P = 3 \/ P e. ( ZZ>= ` 5 ) ) )

Proof

Step Hyp Ref Expression
1 ax-1 
 |-  ( ( P = 2 \/ P = 3 \/ P e. ( ZZ>= ` 5 ) ) -> ( P e. Prime -> ( P = 2 \/ P = 3 \/ P e. ( ZZ>= ` 5 ) ) ) )
2 3ioran 
 |-  ( -. ( P = 2 \/ P = 3 \/ P e. ( ZZ>= ` 5 ) ) <-> ( -. P = 2 /\ -. P = 3 /\ -. P e. ( ZZ>= ` 5 ) ) )
3 3ianor 
 |-  ( -. ( 5 e. ZZ /\ P e. ZZ /\ 5 <_ P ) <-> ( -. 5 e. ZZ \/ -. P e. ZZ \/ -. 5 <_ P ) )
4 eluz2 
 |-  ( P e. ( ZZ>= ` 5 ) <-> ( 5 e. ZZ /\ P e. ZZ /\ 5 <_ P ) )
5 3 4 xchnxbir 
 |-  ( -. P e. ( ZZ>= ` 5 ) <-> ( -. 5 e. ZZ \/ -. P e. ZZ \/ -. 5 <_ P ) )
6 5nn 
 |-  5 e. NN
7 6 nnzi 
 |-  5 e. ZZ
8 7 pm2.24i 
 |-  ( -. 5 e. ZZ -> ( ( -. P = 2 /\ -. P = 3 ) -> ( P e. Prime -> ( P = 2 \/ P = 3 \/ P e. ( ZZ>= ` 5 ) ) ) ) )
9 pm2.24 
 |-  ( P e. ZZ -> ( -. P e. ZZ -> ( P = 2 \/ P = 3 \/ P e. ( ZZ>= ` 5 ) ) ) )
10 prmz 
 |-  ( P e. Prime -> P e. ZZ )
11 9 10 syl11 
 |-  ( -. P e. ZZ -> ( P e. Prime -> ( P = 2 \/ P = 3 \/ P e. ( ZZ>= ` 5 ) ) ) )
12 11 a1d 
 |-  ( -. P e. ZZ -> ( ( -. P = 2 /\ -. P = 3 ) -> ( P e. Prime -> ( P = 2 \/ P = 3 \/ P e. ( ZZ>= ` 5 ) ) ) ) )
13 10 zred 
 |-  ( P e. Prime -> P e. RR )
14 5re 
 |-  5 e. RR
15 14 a1i 
 |-  ( P e. Prime -> 5 e. RR )
16 13 15 ltnled 
 |-  ( P e. Prime -> ( P < 5 <-> -. 5 <_ P ) )
17 prm23lt5 
 |-  ( ( P e. Prime /\ 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 e. ( ZZ>= ` 5 ) ) ) )
20 18 19 biimtrrid 
 |-  ( ( P = 2 \/ P = 3 ) -> ( ( -. P = 2 /\ -. P = 3 ) -> ( P = 2 \/ P = 3 \/ P e. ( ZZ>= ` 5 ) ) ) )
21 17 20 syl 
 |-  ( ( P e. Prime /\ P < 5 ) -> ( ( -. P = 2 /\ -. P = 3 ) -> ( P = 2 \/ P = 3 \/ P e. ( ZZ>= ` 5 ) ) ) )
22 21 ex 
 |-  ( P e. Prime -> ( P < 5 -> ( ( -. P = 2 /\ -. P = 3 ) -> ( P = 2 \/ P = 3 \/ P e. ( ZZ>= ` 5 ) ) ) ) )
23 16 22 sylbird 
 |-  ( P e. Prime -> ( -. 5 <_ P -> ( ( -. P = 2 /\ -. P = 3 ) -> ( P = 2 \/ P = 3 \/ P e. ( ZZ>= ` 5 ) ) ) ) )
24 23 com3l 
 |-  ( -. 5 <_ P -> ( ( -. P = 2 /\ -. P = 3 ) -> ( P e. Prime -> ( P = 2 \/ P = 3 \/ P e. ( ZZ>= ` 5 ) ) ) ) )
25 8 12 24 3jaoi 
 |-  ( ( -. 5 e. ZZ \/ -. P e. ZZ \/ -. 5 <_ P ) -> ( ( -. P = 2 /\ -. P = 3 ) -> ( P e. Prime -> ( P = 2 \/ P = 3 \/ P e. ( ZZ>= ` 5 ) ) ) ) )
26 5 25 sylbi 
 |-  ( -. P e. ( ZZ>= ` 5 ) -> ( ( -. P = 2 /\ -. P = 3 ) -> ( P e. Prime -> ( P = 2 \/ P = 3 \/ P e. ( ZZ>= ` 5 ) ) ) ) )
27 26 com12 
 |-  ( ( -. P = 2 /\ -. P = 3 ) -> ( -. P e. ( ZZ>= ` 5 ) -> ( P e. Prime -> ( P = 2 \/ P = 3 \/ P e. ( ZZ>= ` 5 ) ) ) ) )
28 27 3impia 
 |-  ( ( -. P = 2 /\ -. P = 3 /\ -. P e. ( ZZ>= ` 5 ) ) -> ( P e. Prime -> ( P = 2 \/ P = 3 \/ P e. ( ZZ>= ` 5 ) ) ) )
29 2 28 sylbi 
 |-  ( -. ( P = 2 \/ P = 3 \/ P e. ( ZZ>= ` 5 ) ) -> ( P e. Prime -> ( P = 2 \/ P = 3 \/ P e. ( ZZ>= ` 5 ) ) ) )
30 1 29 pm2.61i 
 |-  ( P e. Prime -> ( P = 2 \/ P = 3 \/ P e. ( ZZ>= ` 5 ) ) )