Description: A prime less than 5 is either 2 or 3. (Contributed by AV, 5-Jul-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | prm23lt5 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prmnn | |
|
2 | 1 | nnnn0d | |
3 | 2 | adantr | |
4 | 4nn0 | |
|
5 | 4 | a1i | |
6 | df-5 | |
|
7 | 6 | breq2i | |
8 | prmz | |
|
9 | 4z | |
|
10 | zleltp1 | |
|
11 | 8 9 10 | sylancl | |
12 | 11 | biimprd | |
13 | 7 12 | syl5bi | |
14 | 13 | imp | |
15 | elfz2nn0 | |
|
16 | 3 5 14 15 | syl3anbrc | |
17 | fz0to4untppr | |
|
18 | 17 | eleq2i | |
19 | elun | |
|
20 | eltpi | |
|
21 | nnne0 | |
|
22 | eqneqall | |
|
23 | 22 | com12 | |
24 | 1 21 23 | 3syl | |
25 | 24 | com12 | |
26 | eleq1 | |
|
27 | 1nprm | |
|
28 | 27 | pm2.21i | |
29 | 26 28 | syl6bi | |
30 | orc | |
|
31 | 30 | a1d | |
32 | 25 29 31 | 3jaoi | |
33 | 20 32 | syl | |
34 | elpri | |
|
35 | olc | |
|
36 | 35 | a1d | |
37 | eleq1 | |
|
38 | 4nprm | |
|
39 | 38 | pm2.21i | |
40 | 37 39 | syl6bi | |
41 | 36 40 | jaoi | |
42 | 34 41 | syl | |
43 | 33 42 | jaoi | |
44 | 19 43 | sylbi | |
45 | 44 | com12 | |
46 | 45 | adantr | |
47 | 18 46 | syl5bi | |
48 | 16 47 | mpd | |