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 PP<5P=2P=3

Proof

Step Hyp Ref Expression
1 prmnn PP
2 1 nnnn0d PP0
3 2 adantr PP<5P0
4 4nn0 40
5 4 a1i PP<540
6 df-5 5=4+1
7 6 breq2i P<5P<4+1
8 prmz PP
9 4z 4
10 zleltp1 P4P4P<4+1
11 8 9 10 sylancl PP4P<4+1
12 11 biimprd PP<4+1P4
13 7 12 syl5bi PP<5P4
14 13 imp PP<5P4
15 elfz2nn0 P04P040P4
16 3 5 14 15 syl3anbrc PP<5P04
17 fz0to4untppr 04=01234
18 17 eleq2i P04P01234
19 elun P01234P012P34
20 eltpi P012P=0P=1P=2
21 nnne0 PP0
22 eqneqall P=0P0P=2P=3
23 22 com12 P0P=0P=2P=3
24 1 21 23 3syl PP=0P=2P=3
25 24 com12 P=0PP=2P=3
26 eleq1 P=1P1
27 1nprm ¬1
28 27 pm2.21i 1P=2P=3
29 26 28 syl6bi P=1PP=2P=3
30 orc P=2P=2P=3
31 30 a1d P=2PP=2P=3
32 25 29 31 3jaoi P=0P=1P=2PP=2P=3
33 20 32 syl P012PP=2P=3
34 elpri P34P=3P=4
35 olc P=3P=2P=3
36 35 a1d P=3PP=2P=3
37 eleq1 P=4P4
38 4nprm ¬4
39 38 pm2.21i 4P=2P=3
40 37 39 syl6bi P=4PP=2P=3
41 36 40 jaoi P=3P=4PP=2P=3
42 34 41 syl P34PP=2P=3
43 33 42 jaoi P012P34PP=2P=3
44 19 43 sylbi P01234PP=2P=3
45 44 com12 PP01234P=2P=3
46 45 adantr PP<5P01234P=2P=3
47 18 46 syl5bi PP<5P04P=2P=3
48 16 47 mpd PP<5P=2P=3