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