Theorem nn0n0n1ge2b

Description: A nonnegative integer is neither 0 nor 1 if and only if it is greater than or equal to 2. (Contributed by Alexander van der Vekens, 17-Jan-2018)

	Ref	Expression
Assertion	nn0n0n1ge2b	$$⊢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		nn0n0n1ge2	$$⊢\left(N\in {\mathbb{N}}_0\wedge N\ne 0\wedge N\ne 1\right)\to 2\le N$$
2	1	3expib	$$⊢N\in {\mathbb{N}}_0\to \left(\left(N\ne 0\wedge N\ne 1\right)\to 2\le N\right)$$
3		ianor	$$⊢\neg \left(N\ne 0\wedge N\ne 1\right)\leftrightarrow \left(\neg N\ne 0\vee \neg N\ne 1\right)$$
4		nne	$$⊢\neg N\ne 0\leftrightarrow N=0$$
5		nne	$$⊢\neg N\ne 1\leftrightarrow N=1$$
6	4 5	orbi12i	$$⊢\left(\neg N\ne 0\vee \neg N\ne 1\right)\leftrightarrow \left(N=0\vee N=1\right)$$
7	3 6	bitri	$$⊢\neg \left(N\ne 0\wedge N\ne 1\right)\leftrightarrow \left(N=0\vee N=1\right)$$
8		2pos	$$⊢0<2$$
9		breq1	$$⊢N=0\to \left(N<2\leftrightarrow 0<2\right)$$
10	8 9	mpbiri	$$⊢N=0\to N<2$$
11	10	a1d	$$⊢N=0\to \left(N\in {\mathbb{N}}_0\to N<2\right)$$
12		1lt2	$$⊢1<2$$
13		breq1	$$⊢N=1\to \left(N<2\leftrightarrow 1<2\right)$$
14	12 13	mpbiri	$$⊢N=1\to N<2$$
15	14	a1d	$$⊢N=1\to \left(N\in {\mathbb{N}}_0\to N<2\right)$$
16	11 15	jaoi	$$⊢\left(N=0\vee N=1\right)\to \left(N\in {\mathbb{N}}_0\to N<2\right)$$
17	16	impcom	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(N=0\vee N=1\right)\right)\to N<2$$
18		nn0re	$$⊢N\in {\mathbb{N}}_0\to N\in ℝ$$
19		2re	$$⊢2\in ℝ$$
20	18 19	jctir	$$⊢N\in {\mathbb{N}}_0\to \left(N\in ℝ\wedge 2\in ℝ\right)$$
21	20	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(N=0\vee N=1\right)\right)\to \left(N\in ℝ\wedge 2\in ℝ\right)$$
22		ltnle	$$⊢\left(N\in ℝ\wedge 2\in ℝ\right)\to \left(N<2\leftrightarrow \neg 2\le N\right)$$
23	21 22	syl	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(N=0\vee N=1\right)\right)\to \left(N<2\leftrightarrow \neg 2\le N\right)$$
24	17 23	mpbid	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(N=0\vee N=1\right)\right)\to \neg 2\le N$$
25	24	ex	$$⊢N\in {\mathbb{N}}_0\to \left(\left(N=0\vee N=1\right)\to \neg 2\le N\right)$$
26	7 25	biimtrid	$$⊢N\in {\mathbb{N}}_0\to \left(\neg \left(N\ne 0\wedge N\ne 1\right)\to \neg 2\le N\right)$$
27	2 26	impcon4bid	$$⊢N\in {\mathbb{N}}_0\to \left(\left(N\ne 0\wedge N\ne 1\right)\leftrightarrow 2\le N\right)$$