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

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

Proof

Step Hyp Ref Expression
1 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
2 2re ⊢ 2 ∈ ℝ
3 2 a1i ⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℝ )
4 1 3 leloed ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ≤ 2 ↔ ( 𝑁 < 2 ∨ 𝑁 = 2 ) ) )
5 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
6 2z ⊢ 2 ∈ ℤ
7 zltlem1 ⊢ ( ( 𝑁 ∈ ℤ ∧ 2 ∈ ℤ ) → ( 𝑁 < 2 ↔ 𝑁 ≤ ( 2 − 1 ) ) )
8 5 6 7 sylancl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 < 2 ↔ 𝑁 ≤ ( 2 − 1 ) ) )
9 2m1e1 ⊢ ( 2 − 1 ) = 1
10 9 a1i ⊢ ( 𝑁 ∈ ℕ0 → ( 2 − 1 ) = 1 )
11 10 breq2d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ≤ ( 2 − 1 ) ↔ 𝑁 ≤ 1 ) )
12 8 11 bitrd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 < 2 ↔ 𝑁 ≤ 1 ) )
13 1red ⊢ ( 𝑁 ∈ ℕ0 → 1 ∈ ℝ )
14 1 13 leloed ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ≤ 1 ↔ ( 𝑁 < 1 ∨ 𝑁 = 1 ) ) )
15 nn0lt10b ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 < 1 ↔ 𝑁 = 0 ) )
16 3mix1 ⊢ ( 𝑁 = 0 → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) )
17 15 16 biimtrdi ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 < 1 → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) )
18 17 com12 ⊢ ( 𝑁 < 1 → ( 𝑁 ∈ ℕ0 → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) )
19 3mix2 ⊢ ( 𝑁 = 1 → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) )
20 19 a1d ⊢ ( 𝑁 = 1 → ( 𝑁 ∈ ℕ0 → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) )
21 18 20 jaoi ⊢ ( ( 𝑁 < 1 ∨ 𝑁 = 1 ) → ( 𝑁 ∈ ℕ0 → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) )
22 21 com12 ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 < 1 ∨ 𝑁 = 1 ) → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) )
23 14 22 sylbid ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ≤ 1 → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) )
24 12 23 sylbid ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 < 2 → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) )
25 24 com12 ⊢ ( 𝑁 < 2 → ( 𝑁 ∈ ℕ0 → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) )
26 3mix3 ⊢ ( 𝑁 = 2 → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) )
27 26 a1d ⊢ ( 𝑁 = 2 → ( 𝑁 ∈ ℕ0 → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) )
28 25 27 jaoi ⊢ ( ( 𝑁 < 2 ∨ 𝑁 = 2 ) → ( 𝑁 ∈ ℕ0 → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) )
29 28 com12 ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 < 2 ∨ 𝑁 = 2 ) → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) )
30 4 29 sylbid ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ≤ 2 → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) ) )
31 30 imp ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 2 ) → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) )