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

Metamath Proof Explorer

Theorem prm23lt5

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

Ref Expression
Assertion prm23lt5 
|- ( ( P e. Prime /\ P < 5 ) -> ( P = 2 \/ P = 3 ) )

Proof

Step Hyp Ref Expression
1 prmnn 
 |-  ( P e. Prime -> P e. NN )
2 1 nnnn0d 
 |-  ( P e. Prime -> P e. NN0 )
3 2 adantr 
 |-  ( ( P e. Prime /\ P < 5 ) -> P e. NN0 )
4 4nn0 
 |-  4 e. NN0
5 4 a1i 
 |-  ( ( P e. Prime /\ P < 5 ) -> 4 e. NN0 )
6 df-5 
 |-  5 = ( 4 + 1 )
7 6 breq2i 
 |-  ( P < 5 <-> P < ( 4 + 1 ) )
8 prmz 
 |-  ( P e. Prime -> P e. ZZ )
9 4z 
 |-  4 e. ZZ
10 zleltp1 
 |-  ( ( P e. ZZ /\ 4 e. ZZ ) -> ( P <_ 4 <-> P < ( 4 + 1 ) ) )
11 8 9 10 sylancl 
 |-  ( P e. Prime -> ( P <_ 4 <-> P < ( 4 + 1 ) ) )
12 11 biimprd 
 |-  ( P e. Prime -> ( P < ( 4 + 1 ) -> P <_ 4 ) )
13 7 12 biimtrid 
 |-  ( P e. Prime -> ( P < 5 -> P <_ 4 ) )
14 13 imp 
 |-  ( ( P e. Prime /\ P < 5 ) -> P <_ 4 )
15 elfz2nn0 
 |-  ( P e. ( 0 ... 4 ) <-> ( P e. NN0 /\ 4 e. NN0 /\ P <_ 4 ) )
16 3 5 14 15 syl3anbrc 
 |-  ( ( P e. Prime /\ P < 5 ) -> P e. ( 0 ... 4 ) )
17 fz0to4untppr 
 |-  ( 0 ... 4 ) = ( { 0 , 1 , 2 } u. { 3 , 4 } )
18 17 eleq2i 
 |-  ( P e. ( 0 ... 4 ) <-> P e. ( { 0 , 1 , 2 } u. { 3 , 4 } ) )
19 elun 
 |-  ( P e. ( { 0 , 1 , 2 } u. { 3 , 4 } ) <-> ( P e. { 0 , 1 , 2 } \/ P e. { 3 , 4 } ) )
20 eltpi 
 |-  ( P e. { 0 , 1 , 2 } -> ( P = 0 \/ P = 1 \/ P = 2 ) )
21 nnne0 
 |-  ( P e. NN -> P =/= 0 )
22 eqneqall 
 |-  ( P = 0 -> ( P =/= 0 -> ( P = 2 \/ P = 3 ) ) )
23 22 com12 
 |-  ( P =/= 0 -> ( P = 0 -> ( P = 2 \/ P = 3 ) ) )
24 1 21 23 3syl 
 |-  ( P e. Prime -> ( P = 0 -> ( P = 2 \/ P = 3 ) ) )
25 24 com12 
 |-  ( P = 0 -> ( P e. Prime -> ( P = 2 \/ P = 3 ) ) )
26 eleq1 
 |-  ( P = 1 -> ( P e. Prime <-> 1 e. Prime ) )
27 1nprm 
 |-  -. 1 e. Prime
28 27 pm2.21i 
 |-  ( 1 e. Prime -> ( P = 2 \/ P = 3 ) )
29 26 28 biimtrdi 
 |-  ( P = 1 -> ( P e. Prime -> ( P = 2 \/ P = 3 ) ) )
30 orc 
 |-  ( P = 2 -> ( P = 2 \/ P = 3 ) )
31 30 a1d 
 |-  ( P = 2 -> ( P e. Prime -> ( P = 2 \/ P = 3 ) ) )
32 25 29 31 3jaoi 
 |-  ( ( P = 0 \/ P = 1 \/ P = 2 ) -> ( P e. Prime -> ( P = 2 \/ P = 3 ) ) )
33 20 32 syl 
 |-  ( P e. { 0 , 1 , 2 } -> ( P e. Prime -> ( P = 2 \/ P = 3 ) ) )
34 elpri 
 |-  ( P e. { 3 , 4 } -> ( P = 3 \/ P = 4 ) )
35 olc 
 |-  ( P = 3 -> ( P = 2 \/ P = 3 ) )
36 35 a1d 
 |-  ( P = 3 -> ( P e. Prime -> ( P = 2 \/ P = 3 ) ) )
37 eleq1 
 |-  ( P = 4 -> ( P e. Prime <-> 4 e. Prime ) )
38 4nprm 
 |-  -. 4 e. Prime
39 38 pm2.21i 
 |-  ( 4 e. Prime -> ( P = 2 \/ P = 3 ) )
40 37 39 biimtrdi 
 |-  ( P = 4 -> ( P e. Prime -> ( P = 2 \/ P = 3 ) ) )
41 36 40 jaoi 
 |-  ( ( P = 3 \/ P = 4 ) -> ( P e. Prime -> ( P = 2 \/ P = 3 ) ) )
42 34 41 syl 
 |-  ( P e. { 3 , 4 } -> ( P e. Prime -> ( P = 2 \/ P = 3 ) ) )
43 33 42 jaoi 
 |-  ( ( P e. { 0 , 1 , 2 } \/ P e. { 3 , 4 } ) -> ( P e. Prime -> ( P = 2 \/ P = 3 ) ) )
44 19 43 sylbi 
 |-  ( P e. ( { 0 , 1 , 2 } u. { 3 , 4 } ) -> ( P e. Prime -> ( P = 2 \/ P = 3 ) ) )
45 44 com12 
 |-  ( P e. Prime -> ( P e. ( { 0 , 1 , 2 } u. { 3 , 4 } ) -> ( P = 2 \/ P = 3 ) ) )
46 45 adantr 
 |-  ( ( P e. Prime /\ P < 5 ) -> ( P e. ( { 0 , 1 , 2 } u. { 3 , 4 } ) -> ( P = 2 \/ P = 3 ) ) )
47 18 46 biimtrid 
 |-  ( ( P e. Prime /\ P < 5 ) -> ( P e. ( 0 ... 4 ) -> ( P = 2 \/ P = 3 ) ) )
48 16 47 mpd 
 |-  ( ( P e. Prime /\ P < 5 ) -> ( P = 2 \/ P = 3 ) )