Metamath Proof Explorer

Theorem nn0lt2

Description: A nonnegative integer less than 2 must be 0 or 1. (Contributed by Alexander van der Vekens, 16-Sep-2018)

Ref Expression
Assertion nn0lt2 ⊢N∈ℕ0∧N<2→N=0∨N=1

Proof

Step Hyp Ref Expression
1 olc ⊢N=1→N=0∨N=1
2 1 a1d ⊢N=1→N∈ℕ0∧N<2→N=0∨N=1
3 nn0z ⊢N∈ℕ0→N∈ℤ
4 2z ⊢2∈ℤ
5 zltlem1 ⊢N∈ℤ∧2∈ℤ→N<2↔N≤2−1
6 3 4 5 sylancl ⊢N∈ℕ0→N<2↔N≤2−1
7 2m1e1 ⊢2−1=1
8 7 breq2i ⊢N≤2−1↔N≤1
9 6 8 bitrdi ⊢N∈ℕ0→N<2↔N≤1
10 necom ⊢N≠1↔1≠N
11 nn0re ⊢N∈ℕ0→N∈ℝ
12 1re ⊢1∈ℝ
13 ltlen ⊢N∈ℝ∧1∈ℝ→N<1↔N≤1∧1≠N
14 11 12 13 sylancl ⊢N∈ℕ0→N<1↔N≤1∧1≠N
15 nn0lt10b ⊢N∈ℕ0→N<1↔N=0
16 15 biimpa ⊢N∈ℕ0∧N<1→N=0
17 16 orcd ⊢N∈ℕ0∧N<1→N=0∨N=1
18 17 ex ⊢N∈ℕ0→N<1→N=0∨N=1
19 14 18 sylbird ⊢N∈ℕ0→N≤1∧1≠N→N=0∨N=1
20 19 expd ⊢N∈ℕ0→N≤1→1≠N→N=0∨N=1
21 10 20 syl7bi ⊢N∈ℕ0→N≤1→N≠1→N=0∨N=1
22 9 21 sylbid ⊢N∈ℕ0→N<2→N≠1→N=0∨N=1
23 22 imp ⊢N∈ℕ0∧N<2→N≠1→N=0∨N=1
24 23 com12 ⊢N≠1→N∈ℕ0∧N<2→N=0∨N=1
25 2 24 pm2.61ine ⊢N∈ℕ0∧N<2→N=0∨N=1