This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑁 ∈ ℕ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 ) )