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	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 < 2 ) → ( 𝑁 = 0 ∨ 𝑁 = 1 ) )

Proof

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