Metamath Proof Explorer

Theorem nn0le2is012

Description: A nonnegative integer which is less than or equal to 2 is either 0 or 1 or 2. (Contributed by AV, 16-Mar-2019)

Ref Expression
Assertion nn0le2is012 ⊢ N ∈ ℕ 0 ∧ N ≤ 2 → N = 0 ∨ N = 1 ∨ N = 2

Proof

Step Hyp Ref Expression
1 nn0re ⊢ N ∈ ℕ 0 → N ∈ ℝ
2 2re ⊢ 2 ∈ ℝ
3 2 a1i ⊢ N ∈ ℕ 0 → 2 ∈ ℝ
4 1 3 leloed ⊢ N ∈ ℕ 0 → N ≤ 2 ↔ N < 2 ∨ N = 2
5 nn0z ⊢ N ∈ ℕ 0 → N ∈ ℤ
6 2z ⊢ 2 ∈ ℤ
7 zltlem1 ⊢ N ∈ ℤ ∧ 2 ∈ ℤ → N < 2 ↔ N ≤ 2 − 1
8 5 6 7 sylancl ⊢ N ∈ ℕ 0 → N < 2 ↔ N ≤ 2 − 1
9 2m1e1 ⊢ 2 − 1 = 1
10 9 a1i ⊢ N ∈ ℕ 0 → 2 − 1 = 1
11 10 breq2d ⊢ N ∈ ℕ 0 → N ≤ 2 − 1 ↔ N ≤ 1
12 8 11 bitrd ⊢ N ∈ ℕ 0 → N < 2 ↔ N ≤ 1
13 1red ⊢ N ∈ ℕ 0 → 1 ∈ ℝ
14 1 13 leloed ⊢ N ∈ ℕ 0 → N ≤ 1 ↔ N < 1 ∨ N = 1
15 nn0lt10b ⊢ N ∈ ℕ 0 → N < 1 ↔ N = 0
16 3mix1 ⊢ N = 0 → N = 0 ∨ N = 1 ∨ N = 2
17 15 16 biimtrdi ⊢ N ∈ ℕ 0 → N < 1 → N = 0 ∨ N = 1 ∨ N = 2
18 17 com12 ⊢ N < 1 → N ∈ ℕ 0 → N = 0 ∨ N = 1 ∨ N = 2
19 3mix2 ⊢ N = 1 → N = 0 ∨ N = 1 ∨ N = 2
20 19 a1d ⊢ N = 1 → N ∈ ℕ 0 → N = 0 ∨ N = 1 ∨ N = 2
21 18 20 jaoi ⊢ N < 1 ∨ N = 1 → N ∈ ℕ 0 → N = 0 ∨ N = 1 ∨ N = 2
22 21 com12 ⊢ N ∈ ℕ 0 → N < 1 ∨ N = 1 → N = 0 ∨ N = 1 ∨ N = 2
23 14 22 sylbid ⊢ N ∈ ℕ 0 → N ≤ 1 → N = 0 ∨ N = 1 ∨ N = 2
24 12 23 sylbid ⊢ N ∈ ℕ 0 → N < 2 → N = 0 ∨ N = 1 ∨ N = 2
25 24 com12 ⊢ N < 2 → N ∈ ℕ 0 → N = 0 ∨ N = 1 ∨ N = 2
26 3mix3 ⊢ N = 2 → N = 0 ∨ N = 1 ∨ N = 2
27 26 a1d ⊢ N = 2 → N ∈ ℕ 0 → N = 0 ∨ N = 1 ∨ N = 2
28 25 27 jaoi ⊢ N < 2 ∨ N = 2 → N ∈ ℕ 0 → N = 0 ∨ N = 1 ∨ N = 2
29 28 com12 ⊢ N ∈ ℕ 0 → N < 2 ∨ N = 2 → N = 0 ∨ N = 1 ∨ N = 2
30 4 29 sylbid ⊢ N ∈ ℕ 0 → N ≤ 2 → N = 0 ∨ N = 1 ∨ N = 2
31 30 imp ⊢ N ∈ ℕ 0 ∧ N ≤ 2 → N = 0 ∨ N = 1 ∨ N = 2