Theorem nn0n0n1ge2

Description: A nonnegative integer which is neither 0 nor 1 is greater than or equal to 2. (Contributed by Alexander van der Vekens, 6-Dec-2017)

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

Proof

Step	Hyp	Ref	Expression
1		nn0cn	$$⊢N\in {\mathbb{N}}_0\to N\in ℂ$$
2		1cnd	$$⊢N\in {\mathbb{N}}_0\to 1\in ℂ$$
3	1 2 2	subsub4d	$$⊢N\in {\mathbb{N}}_0\to N-1-1=N-\left(1+1\right)$$
4		1p1e2	$$⊢1+1=2$$
5	4	oveq2i	$$⊢N-\left(1+1\right)=N-2$$
6	3 5	eqtr2di	$$⊢N\in {\mathbb{N}}_0\to N-2=N-1-1$$
7	6	3ad2ant1	$$⊢\left(N\in {\mathbb{N}}_0\wedge N\ne 0\wedge N\ne 1\right)\to N-2=N-1-1$$
8		3simpa	$$⊢\left(N\in {\mathbb{N}}_0\wedge N\ne 0\wedge N\ne 1\right)\to \left(N\in {\mathbb{N}}_0\wedge N\ne 0\right)$$
9		elnnne0	$$⊢N\in \mathbb{N}\leftrightarrow \left(N\in {\mathbb{N}}_0\wedge N\ne 0\right)$$
10	8 9	sylibr	$$⊢\left(N\in {\mathbb{N}}_0\wedge N\ne 0\wedge N\ne 1\right)\to N\in \mathbb{N}$$
11		nnm1nn0	$$⊢N\in \mathbb{N}\to N-1\in {\mathbb{N}}_0$$
12	10 11	syl	$$⊢\left(N\in {\mathbb{N}}_0\wedge N\ne 0\wedge N\ne 1\right)\to N-1\in {\mathbb{N}}_0$$
13	1 2	subeq0ad	$$⊢N\in {\mathbb{N}}_0\to \left(N-1=0\leftrightarrow N=1\right)$$
14	13	biimpd	$$⊢N\in {\mathbb{N}}_0\to \left(N-1=0\to N=1\right)$$
15	14	necon3d	$$⊢N\in {\mathbb{N}}_0\to \left(N\ne 1\to N-1\ne 0\right)$$
16	15	imp	$$⊢\left(N\in {\mathbb{N}}_0\wedge N\ne 1\right)\to N-1\ne 0$$
17	16	3adant2	$$⊢\left(N\in {\mathbb{N}}_0\wedge N\ne 0\wedge N\ne 1\right)\to N-1\ne 0$$
18		elnnne0	$$⊢N-1\in \mathbb{N}\leftrightarrow \left(N-1\in {\mathbb{N}}_0\wedge N-1\ne 0\right)$$
19	12 17 18	sylanbrc	$$⊢\left(N\in {\mathbb{N}}_0\wedge N\ne 0\wedge N\ne 1\right)\to N-1\in \mathbb{N}$$
20		nnm1nn0	$$⊢N-1\in \mathbb{N}\to N-1-1\in {\mathbb{N}}_0$$
21	19 20	syl	$$⊢\left(N\in {\mathbb{N}}_0\wedge N\ne 0\wedge N\ne 1\right)\to N-1-1\in {\mathbb{N}}_0$$
22	7 21	eqeltrd	$$⊢\left(N\in {\mathbb{N}}_0\wedge N\ne 0\wedge N\ne 1\right)\to N-2\in {\mathbb{N}}_0$$
23		2nn0	$$⊢2\in {\mathbb{N}}_0$$
24	23	jctl	$$⊢N\in {\mathbb{N}}_0\to \left(2\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)$$
25	24	3ad2ant1	$$⊢\left(N\in {\mathbb{N}}_0\wedge N\ne 0\wedge N\ne 1\right)\to \left(2\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)$$
26		nn0sub	$$⊢\left(2\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to \left(2\le N\leftrightarrow N-2\in {\mathbb{N}}_0\right)$$
27	25 26	syl	$$⊢\left(N\in {\mathbb{N}}_0\wedge N\ne 0\wedge N\ne 1\right)\to \left(2\le N\leftrightarrow N-2\in {\mathbb{N}}_0\right)$$
28	22 27	mpbird	$$⊢\left(N\in {\mathbb{N}}_0\wedge N\ne 0\wedge N\ne 1\right)\to 2\le N$$