Metamath Proof Explorer


Theorem nn01to3

Description: A (nonnegative) integer between 1 and 3 must be 1, 2 or 3. (Contributed by Alexander van der Vekens, 13-Sep-2018)

Ref Expression
Assertion nn01to3 ( ( 𝑁 ∈ ℕ0 ∧ 1 ≤ 𝑁𝑁 ≤ 3 ) → ( 𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3 ) )

Proof

Step Hyp Ref Expression
1 3mix3 ( 𝑁 = 3 → ( 𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3 ) )
2 1 a1d ( 𝑁 = 3 → ( ( 𝑁 ∈ ℕ0 ∧ 1 ≤ 𝑁𝑁 ≤ 3 ) → ( 𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3 ) ) )
3 nn0re ( 𝑁 ∈ ℕ0𝑁 ∈ ℝ )
4 3 3ad2ant1 ( ( 𝑁 ∈ ℕ0 ∧ 1 ≤ 𝑁𝑁 ≤ 3 ) → 𝑁 ∈ ℝ )
5 3re 3 ∈ ℝ
6 5 a1i ( ( 𝑁 ∈ ℕ0 ∧ 1 ≤ 𝑁𝑁 ≤ 3 ) → 3 ∈ ℝ )
7 simp3 ( ( 𝑁 ∈ ℕ0 ∧ 1 ≤ 𝑁𝑁 ≤ 3 ) → 𝑁 ≤ 3 )
8 4 6 7 leltned ( ( 𝑁 ∈ ℕ0 ∧ 1 ≤ 𝑁𝑁 ≤ 3 ) → ( 𝑁 < 3 ↔ 3 ≠ 𝑁 ) )
9 nesym ( 3 ≠ 𝑁 ↔ ¬ 𝑁 = 3 )
10 8 9 bitr2di ( ( 𝑁 ∈ ℕ0 ∧ 1 ≤ 𝑁𝑁 ≤ 3 ) → ( ¬ 𝑁 = 3 ↔ 𝑁 < 3 ) )
11 elnnnn0c ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℕ0 ∧ 1 ≤ 𝑁 ) )
12 orc ( 𝑁 = 1 → ( 𝑁 = 1 ∨ 𝑁 = 2 ) )
13 12 2a1d ( 𝑁 = 1 → ( 𝑁 ∈ ℕ → ( 𝑁 < 3 → ( 𝑁 = 1 ∨ 𝑁 = 2 ) ) ) )
14 eluz2b3 ( 𝑁 ∈ ( ℤ ‘ 2 ) ↔ ( 𝑁 ∈ ℕ ∧ 𝑁 ≠ 1 ) )
15 eluz2 ( 𝑁 ∈ ( ℤ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁 ) )
16 2a1 ( 𝑁 = 2 → ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁 ) → ( 𝑁 < 3 → 𝑁 = 2 ) ) )
17 zre ( 2 ∈ ℤ → 2 ∈ ℝ )
18 zre ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
19 id ( 2 ≤ 𝑁 → 2 ≤ 𝑁 )
20 leltne ( ( 2 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) → ( 2 < 𝑁𝑁 ≠ 2 ) )
21 17 18 19 20 syl3an ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁 ) → ( 2 < 𝑁𝑁 ≠ 2 ) )
22 2z 2 ∈ ℤ
23 simpr ( ( ( 𝑁 ∈ ℤ ∧ 𝑁 < 3 ) ∧ 2 < 𝑁 ) → 2 < 𝑁 )
24 df-3 3 = ( 2 + 1 )
25 24 a1i ( 𝑁 ∈ ℤ → 3 = ( 2 + 1 ) )
26 25 breq2d ( 𝑁 ∈ ℤ → ( 𝑁 < 3 ↔ 𝑁 < ( 2 + 1 ) ) )
27 26 biimpa ( ( 𝑁 ∈ ℤ ∧ 𝑁 < 3 ) → 𝑁 < ( 2 + 1 ) )
28 27 adantr ( ( ( 𝑁 ∈ ℤ ∧ 𝑁 < 3 ) ∧ 2 < 𝑁 ) → 𝑁 < ( 2 + 1 ) )
29 btwnnz ( ( 2 ∈ ℤ ∧ 2 < 𝑁𝑁 < ( 2 + 1 ) ) → ¬ 𝑁 ∈ ℤ )
30 22 23 28 29 mp3an2i ( ( ( 𝑁 ∈ ℤ ∧ 𝑁 < 3 ) ∧ 2 < 𝑁 ) → ¬ 𝑁 ∈ ℤ )
31 30 pm2.21d ( ( ( 𝑁 ∈ ℤ ∧ 𝑁 < 3 ) ∧ 2 < 𝑁 ) → ( 𝑁 ∈ ℤ → 𝑁 = 2 ) )
32 31 exp31 ( 𝑁 ∈ ℤ → ( 𝑁 < 3 → ( 2 < 𝑁 → ( 𝑁 ∈ ℤ → 𝑁 = 2 ) ) ) )
33 32 com24 ( 𝑁 ∈ ℤ → ( 𝑁 ∈ ℤ → ( 2 < 𝑁 → ( 𝑁 < 3 → 𝑁 = 2 ) ) ) )
34 33 pm2.43i ( 𝑁 ∈ ℤ → ( 2 < 𝑁 → ( 𝑁 < 3 → 𝑁 = 2 ) ) )
35 34 3ad2ant2 ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁 ) → ( 2 < 𝑁 → ( 𝑁 < 3 → 𝑁 = 2 ) ) )
36 21 35 sylbird ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁 ) → ( 𝑁 ≠ 2 → ( 𝑁 < 3 → 𝑁 = 2 ) ) )
37 36 com12 ( 𝑁 ≠ 2 → ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁 ) → ( 𝑁 < 3 → 𝑁 = 2 ) ) )
38 16 37 pm2.61ine ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁 ) → ( 𝑁 < 3 → 𝑁 = 2 ) )
39 15 38 sylbi ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 𝑁 < 3 → 𝑁 = 2 ) )
40 39 imp ( ( 𝑁 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 < 3 ) → 𝑁 = 2 )
41 40 olcd ( ( 𝑁 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 < 3 ) → ( 𝑁 = 1 ∨ 𝑁 = 2 ) )
42 41 ex ( 𝑁 ∈ ( ℤ ‘ 2 ) → ( 𝑁 < 3 → ( 𝑁 = 1 ∨ 𝑁 = 2 ) ) )
43 14 42 sylbir ( ( 𝑁 ∈ ℕ ∧ 𝑁 ≠ 1 ) → ( 𝑁 < 3 → ( 𝑁 = 1 ∨ 𝑁 = 2 ) ) )
44 43 expcom ( 𝑁 ≠ 1 → ( 𝑁 ∈ ℕ → ( 𝑁 < 3 → ( 𝑁 = 1 ∨ 𝑁 = 2 ) ) ) )
45 13 44 pm2.61ine ( 𝑁 ∈ ℕ → ( 𝑁 < 3 → ( 𝑁 = 1 ∨ 𝑁 = 2 ) ) )
46 11 45 sylbir ( ( 𝑁 ∈ ℕ0 ∧ 1 ≤ 𝑁 ) → ( 𝑁 < 3 → ( 𝑁 = 1 ∨ 𝑁 = 2 ) ) )
47 46 3adant3 ( ( 𝑁 ∈ ℕ0 ∧ 1 ≤ 𝑁𝑁 ≤ 3 ) → ( 𝑁 < 3 → ( 𝑁 = 1 ∨ 𝑁 = 2 ) ) )
48 10 47 sylbid ( ( 𝑁 ∈ ℕ0 ∧ 1 ≤ 𝑁𝑁 ≤ 3 ) → ( ¬ 𝑁 = 3 → ( 𝑁 = 1 ∨ 𝑁 = 2 ) ) )
49 48 impcom ( ( ¬ 𝑁 = 3 ∧ ( 𝑁 ∈ ℕ0 ∧ 1 ≤ 𝑁𝑁 ≤ 3 ) ) → ( 𝑁 = 1 ∨ 𝑁 = 2 ) )
50 49 orcd ( ( ¬ 𝑁 = 3 ∧ ( 𝑁 ∈ ℕ0 ∧ 1 ≤ 𝑁𝑁 ≤ 3 ) ) → ( ( 𝑁 = 1 ∨ 𝑁 = 2 ) ∨ 𝑁 = 3 ) )
51 df-3or ( ( 𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3 ) ↔ ( ( 𝑁 = 1 ∨ 𝑁 = 2 ) ∨ 𝑁 = 3 ) )
52 50 51 sylibr ( ( ¬ 𝑁 = 3 ∧ ( 𝑁 ∈ ℕ0 ∧ 1 ≤ 𝑁𝑁 ≤ 3 ) ) → ( 𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3 ) )
53 52 ex ( ¬ 𝑁 = 3 → ( ( 𝑁 ∈ ℕ0 ∧ 1 ≤ 𝑁𝑁 ≤ 3 ) → ( 𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3 ) ) )
54 2 53 pm2.61i ( ( 𝑁 ∈ ℕ0 ∧ 1 ≤ 𝑁𝑁 ≤ 3 ) → ( 𝑁 = 1 ∨ 𝑁 = 2 ∨ 𝑁 = 3 ) )