Theorem xnn0n0n1ge2b

Description: An extended nonnegative integer is neither 0 nor 1 if and only if it is greater than or equal to 2. (Contributed by AV, 5-Apr-2021)

	Ref	Expression
Assertion	xnn0n0n1ge2b	$$⊢N\in {\mathbb{N}}_0^{*}\to \left(\left(N\ne 0\wedge N\ne 1\right)\leftrightarrow 2\le N\right)$$

Proof

Step	Hyp	Ref	Expression
1		elxnn0	$$⊢N\in {\mathbb{N}}_0^{*}\leftrightarrow \left(N\in {\mathbb{N}}_0\vee N=\mathrm{+\infty }\right)$$
2		nn0n0n1ge2b	$$⊢N\in {\mathbb{N}}_0\to \left(\left(N\ne 0\wedge N\ne 1\right)\leftrightarrow 2\le N\right)$$
3		0nn0	$$⊢0\in {\mathbb{N}}_0$$
4		nn0nepnf	$$⊢0\in {\mathbb{N}}_0\to 0\ne \mathrm{+\infty }$$
5	3 4	ax-mp	$$⊢0\ne \mathrm{+\infty }$$
6	5	necomi	$$⊢\mathrm{+\infty }\ne 0$$
7		neeq1	$$⊢N=\mathrm{+\infty }\to \left(N\ne 0\leftrightarrow \mathrm{+\infty }\ne 0\right)$$
8	6 7	mpbiri	$$⊢N=\mathrm{+\infty }\to N\ne 0$$
9		1nn0	$$⊢1\in {\mathbb{N}}_0$$
10		nn0nepnf	$$⊢1\in {\mathbb{N}}_0\to 1\ne \mathrm{+\infty }$$
11	9 10	ax-mp	$$⊢1\ne \mathrm{+\infty }$$
12	11	necomi	$$⊢\mathrm{+\infty }\ne 1$$
13		neeq1	$$⊢N=\mathrm{+\infty }\to \left(N\ne 1\leftrightarrow \mathrm{+\infty }\ne 1\right)$$
14	12 13	mpbiri	$$⊢N=\mathrm{+\infty }\to N\ne 1$$
15	8 14	jca	$$⊢N=\mathrm{+\infty }\to \left(N\ne 0\wedge N\ne 1\right)$$
16		2re	$$⊢2\in ℝ$$
17	16	rexri	$$⊢2\in {ℝ}^{*}$$
18		pnfge	$$⊢2\in {ℝ}^{*}\to 2\le \mathrm{+\infty }$$
19	17 18	ax-mp	$$⊢2\le \mathrm{+\infty }$$
20		breq2	$$⊢N=\mathrm{+\infty }\to \left(2\le N\leftrightarrow 2\le \mathrm{+\infty }\right)$$
21	19 20	mpbiri	$$⊢N=\mathrm{+\infty }\to 2\le N$$
22	15 21	2thd	$$⊢N=\mathrm{+\infty }\to \left(\left(N\ne 0\wedge N\ne 1\right)\leftrightarrow 2\le N\right)$$
23	2 22	jaoi	$$⊢\left(N\in {\mathbb{N}}_0\vee N=\mathrm{+\infty }\right)\to \left(\left(N\ne 0\wedge N\ne 1\right)\leftrightarrow 2\le N\right)$$
24	1 23	sylbi	$$⊢N\in {\mathbb{N}}_0^{*}\to \left(\left(N\ne 0\wedge N\ne 1\right)\leftrightarrow 2\le N\right)$$