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