Theorem xnn0le2is012

Description: An extended nonnegative integer which is less than or equal to 2 is either 0 or 1 or 2. (Contributed by AV, 24-Nov-2021)

	Ref	Expression
Assertion	xnn0le2is012	⊢ ( ( 𝑁 ∈ ℕ0* ∧ 𝑁 ≤ 2 ) → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) )

Proof

Step	Hyp	Ref	Expression
1		2nn0	⊢ 2 ∈ ℕ0
2		xnn0lenn0nn0	⊢ ( ( 𝑁 ∈ ℕ0* ∧ 2 ∈ ℕ0 ∧ 𝑁 ≤ 2 ) → 𝑁 ∈ ℕ0 )
3	1 2	mp3an2	⊢ ( ( 𝑁 ∈ ℕ0* ∧ 𝑁 ≤ 2 ) → 𝑁 ∈ ℕ0 )
4		nn0le2is012	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 2 ) → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) )
5	3 4	sylancom	⊢ ( ( 𝑁 ∈ ℕ0* ∧ 𝑁 ≤ 2 ) → ( 𝑁 = 0 ∨ 𝑁 = 1 ∨ 𝑁 = 2 ) )