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