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

Proof

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