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 ∈ ℙ ∧ P < 5 → P = 2 ∨ P = 3

Proof

Step Hyp Ref Expression
1 prmnn ⊢ P ∈ ℙ → P ∈ ℕ
2 1 nnnn0d ⊢ P ∈ ℙ → P ∈ ℕ 0
3 2 adantr ⊢ P ∈ ℙ ∧ P < 5 → P ∈ ℕ 0
4 4nn0 ⊢ 4 ∈ ℕ 0
5 4 a1i ⊢ P ∈ ℙ ∧ P < 5 → 4 ∈ ℕ 0
6 df-5 ⊢ 5 = 4 + 1
7 6 breq2i ⊢ P < 5 ↔ P < 4 + 1
8 prmz ⊢ P ∈ ℙ → P ∈ ℤ
9 4z ⊢ 4 ∈ ℤ
10 zleltp1 ⊢ P ∈ ℤ ∧ 4 ∈ ℤ → P ≤ 4 ↔ P < 4 + 1
11 8 9 10 sylancl ⊢ P ∈ ℙ → P ≤ 4 ↔ P < 4 + 1
12 11 biimprd ⊢ P ∈ ℙ → P < 4 + 1 → P ≤ 4
13 7 12 syl5bi ⊢ P ∈ ℙ → P < 5 → P ≤ 4
14 13 imp ⊢ P ∈ ℙ ∧ P < 5 → P ≤ 4
15 elfz2nn0 ⊢ P ∈ 0 … 4 ↔ P ∈ ℕ 0 ∧ 4 ∈ ℕ 0 ∧ P ≤ 4
16 3 5 14 15 syl3anbrc ⊢ P ∈ ℙ ∧ P < 5 → P ∈ 0 … 4
17 fz0to4untppr ⊢ 0 … 4 = 0 1 2 ∪ 3 4
18 17 eleq2i ⊢ P ∈ 0 … 4 ↔ P ∈ 0 1 2 ∪ 3 4
19 elun ⊢ P ∈ 0 1 2 ∪ 3 4 ↔ P ∈ 0 1 2 ∨ P ∈ 3 4
20 eltpi ⊢ P ∈ 0 1 2 → P = 0 ∨ P = 1 ∨ P = 2
21 nnne0 ⊢ P ∈ ℕ → 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 ∈ ℙ → P = 0 → P = 2 ∨ P = 3
25 24 com12 ⊢ P = 0 → P ∈ ℙ → P = 2 ∨ P = 3
26 eleq1 ⊢ P = 1 → P ∈ ℙ ↔ 1 ∈ ℙ
27 1nprm ⊢ ¬ 1 ∈ ℙ
28 27 pm2.21i ⊢ 1 ∈ ℙ → P = 2 ∨ P = 3
29 26 28 syl6bi ⊢ P = 1 → P ∈ ℙ → P = 2 ∨ P = 3
30 orc ⊢ P = 2 → P = 2 ∨ P = 3
31 30 a1d ⊢ P = 2 → P ∈ ℙ → P = 2 ∨ P = 3
32 25 29 31 3jaoi ⊢ P = 0 ∨ P = 1 ∨ P = 2 → P ∈ ℙ → P = 2 ∨ P = 3
33 20 32 syl ⊢ P ∈ 0 1 2 → P ∈ ℙ → P = 2 ∨ P = 3
34 elpri ⊢ P ∈ 3 4 → P = 3 ∨ P = 4
35 olc ⊢ P = 3 → P = 2 ∨ P = 3
36 35 a1d ⊢ P = 3 → P ∈ ℙ → P = 2 ∨ P = 3
37 eleq1 ⊢ P = 4 → P ∈ ℙ ↔ 4 ∈ ℙ
38 4nprm ⊢ ¬ 4 ∈ ℙ
39 38 pm2.21i ⊢ 4 ∈ ℙ → P = 2 ∨ P = 3
40 37 39 syl6bi ⊢ P = 4 → P ∈ ℙ → P = 2 ∨ P = 3
41 36 40 jaoi ⊢ P = 3 ∨ P = 4 → P ∈ ℙ → P = 2 ∨ P = 3
42 34 41 syl ⊢ P ∈ 3 4 → P ∈ ℙ → P = 2 ∨ P = 3
43 33 42 jaoi ⊢ P ∈ 0 1 2 ∨ P ∈ 3 4 → P ∈ ℙ → P = 2 ∨ P = 3
44 19 43 sylbi ⊢ P ∈ 0 1 2 ∪ 3 4 → P ∈ ℙ → P = 2 ∨ P = 3
45 44 com12 ⊢ P ∈ ℙ → P ∈ 0 1 2 ∪ 3 4 → P = 2 ∨ P = 3
46 45 adantr ⊢ P ∈ ℙ ∧ P < 5 → P ∈ 0 1 2 ∪ 3 4 → P = 2 ∨ P = 3
47 18 46 syl5bi ⊢ P ∈ ℙ ∧ P < 5 → P ∈ 0 … 4 → P = 2 ∨ P = 3
48 16 47 mpd ⊢ P ∈ ℙ ∧ P < 5 → P = 2 ∨ P = 3