Theorem xnn01gt

Description: An extended nonnegative integer is neither 0 nor 1 if and only if it is greater than 1. (Contributed by Thierry Arnoux, 21-Nov-2023)

	Ref	Expression
Assertion	xnn01gt	$$⊢N\in {\mathbb{N}}_0^{*}\to \left(\neg N\in \left\{0,1\right\}\leftrightarrow 1<N\right)$$

Proof

Step	Hyp	Ref	Expression
1		nelpr	$$⊢N\in {\mathbb{N}}_0^{*}\to \left(\neg N\in \left\{0,1\right\}\leftrightarrow \left(N\ne 0\wedge N\ne 1\right)\right)$$
2		xnn0n0n1ge2b	$$⊢N\in {\mathbb{N}}_0^{*}\to \left(\left(N\ne 0\wedge N\ne 1\right)\leftrightarrow 2\le N\right)$$
3		2nn0	$$⊢2\in {\mathbb{N}}_0$$
4		xnn0lem1lt	$$⊢\left(2\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0^{*}\right)\to \left(2\le N\leftrightarrow 2-1<N\right)$$
5	3 4	mpan	$$⊢N\in {\mathbb{N}}_0^{*}\to \left(2\le N\leftrightarrow 2-1<N\right)$$
6		2m1e1	$$⊢2-1=1$$
7	6	breq1i	$$⊢2-1<N\leftrightarrow 1<N$$
8	5 7	bitrdi	$$⊢N\in {\mathbb{N}}_0^{*}\to \left(2\le N\leftrightarrow 1<N\right)$$
9	1 2 8	3bitrd	$$⊢N\in {\mathbb{N}}_0^{*}\to \left(\neg N\in \left\{0,1\right\}\leftrightarrow 1<N\right)$$