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 ) )