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 ) )