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	$$⊢\left(N\in {\mathbb{N}}_0^{*}\wedge N\le 2\right)\to \left(N=0\vee N=1\vee N=2\right)$$

Proof

Step	Hyp	Ref	Expression
1		2nn0	$$⊢2\in {\mathbb{N}}_0$$
2		xnn0lenn0nn0	$$⊢\left(N\in {\mathbb{N}}_0^{*}\wedge 2\in {\mathbb{N}}_0\wedge N\le 2\right)\to N\in {\mathbb{N}}_0$$
3	1 2	mp3an2	$$⊢\left(N\in {\mathbb{N}}_0^{*}\wedge N\le 2\right)\to N\in {\mathbb{N}}_0$$
4		nn0le2is012	$$⊢\left(N\in {\mathbb{N}}_0\wedge N\le 2\right)\to \left(N=0\vee N=1\vee N=2\right)$$
5	3 4	sylancom	$$⊢\left(N\in {\mathbb{N}}_0^{*}\wedge N\le 2\right)\to \left(N=0\vee N=1\vee N=2\right)$$