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 ⊢ N ∈ ℕ 0 ∧ 1 ≤ N ∧ N ≤ 3 → N = 1 ∨ N = 2 ∨ N = 3

Proof

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