Theorem nn0o1gt2

Description: An odd nonnegative integer is either 1 or greater than 2. (Contributed by AV, 2-Jun-2020)

	Ref	Expression
Assertion	nn0o1gt2	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N+1}{2}\in {\mathbb{N}}_0\right)\to \left(N=1\vee 2<N\right)$$

Proof

Step	Hyp	Ref	Expression
1		elnn0	$$⊢N\in {\mathbb{N}}_0\leftrightarrow \left(N\in \mathbb{N}\vee N=0\right)$$
2		elnnnn0c	$$⊢N\in \mathbb{N}\leftrightarrow \left(N\in {\mathbb{N}}_0\wedge 1\le N\right)$$
3		1red	$$⊢N\in {\mathbb{N}}_0\to 1\in ℝ$$
4		nn0re	$$⊢N\in {\mathbb{N}}_0\to N\in ℝ$$
5	3 4	leloed	$$⊢N\in {\mathbb{N}}_0\to \left(1\le N\leftrightarrow \left(1<N\vee 1=N\right)\right)$$
6		1zzd	$$⊢N\in {\mathbb{N}}_0\to 1\in \mathbb{Z}$$
7		nn0z	$$⊢N\in {\mathbb{N}}_0\to N\in \mathbb{Z}$$
8		zltp1le	$$⊢\left(1\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(1<N\leftrightarrow 1+1\le N\right)$$
9	6 7 8	syl2anc	$$⊢N\in {\mathbb{N}}_0\to \left(1<N\leftrightarrow 1+1\le N\right)$$
10		1p1e2	$$⊢1+1=2$$
11	10	breq1i	$$⊢1+1\le N\leftrightarrow 2\le N$$
12	11	a1i	$$⊢N\in {\mathbb{N}}_0\to \left(1+1\le N\leftrightarrow 2\le N\right)$$
13		2re	$$⊢2\in ℝ$$
14	13	a1i	$$⊢N\in {\mathbb{N}}_0\to 2\in ℝ$$
15	14 4	leloed	$$⊢N\in {\mathbb{N}}_0\to \left(2\le N\leftrightarrow \left(2<N\vee 2=N\right)\right)$$
16	9 12 15	3bitrd	$$⊢N\in {\mathbb{N}}_0\to \left(1<N\leftrightarrow \left(2<N\vee 2=N\right)\right)$$
17		olc	$$⊢2<N\to \left(N=1\vee 2<N\right)$$
18	17	2a1d	$$⊢2<N\to \left(N\in {\mathbb{N}}_0\to \left(\frac{N+1}{2}\in {\mathbb{N}}_0\to \left(N=1\vee 2<N\right)\right)\right)$$
19		oveq1	$$⊢N=2\to N+1=2+1$$
20	19	oveq1d	$$⊢N=2\to \frac{N+1}{2}=\frac{2+1}{2}$$
21	20	eqcoms	$$⊢2=N\to \frac{N+1}{2}=\frac{2+1}{2}$$
22	21	adantl	$$⊢\left(N\in {\mathbb{N}}_0\wedge 2=N\right)\to \frac{N+1}{2}=\frac{2+1}{2}$$
23		2p1e3	$$⊢2+1=3$$
24	23	oveq1i	$$⊢\frac{2+1}{2}=\frac{3}{2}$$
25	22 24	eqtrdi	$$⊢\left(N\in {\mathbb{N}}_0\wedge 2=N\right)\to \frac{N+1}{2}=\frac{3}{2}$$
26	25	eleq1d	$$⊢\left(N\in {\mathbb{N}}_0\wedge 2=N\right)\to \left(\frac{N+1}{2}\in {\mathbb{N}}_0\leftrightarrow \frac{3}{2}\in {\mathbb{N}}_0\right)$$
27		3halfnz	$$⊢\neg \frac{3}{2}\in \mathbb{Z}$$
28		nn0z	$$⊢\frac{3}{2}\in {\mathbb{N}}_0\to \frac{3}{2}\in \mathbb{Z}$$
29	28	pm2.24d	$$⊢\frac{3}{2}\in {\mathbb{N}}_0\to \left(\neg \frac{3}{2}\in \mathbb{Z}\to \left(N=1\vee 2<N\right)\right)$$
30	27 29	mpi	$$⊢\frac{3}{2}\in {\mathbb{N}}_0\to \left(N=1\vee 2<N\right)$$
31	26 30	biimtrdi	$$⊢\left(N\in {\mathbb{N}}_0\wedge 2=N\right)\to \left(\frac{N+1}{2}\in {\mathbb{N}}_0\to \left(N=1\vee 2<N\right)\right)$$
32	31	expcom	$$⊢2=N\to \left(N\in {\mathbb{N}}_0\to \left(\frac{N+1}{2}\in {\mathbb{N}}_0\to \left(N=1\vee 2<N\right)\right)\right)$$
33	18 32	jaoi	$$⊢\left(2<N\vee 2=N\right)\to \left(N\in {\mathbb{N}}_0\to \left(\frac{N+1}{2}\in {\mathbb{N}}_0\to \left(N=1\vee 2<N\right)\right)\right)$$
34	33	com12	$$⊢N\in {\mathbb{N}}_0\to \left(\left(2<N\vee 2=N\right)\to \left(\frac{N+1}{2}\in {\mathbb{N}}_0\to \left(N=1\vee 2<N\right)\right)\right)$$
35	16 34	sylbid	$$⊢N\in {\mathbb{N}}_0\to \left(1<N\to \left(\frac{N+1}{2}\in {\mathbb{N}}_0\to \left(N=1\vee 2<N\right)\right)\right)$$
36	35	com12	$$⊢1<N\to \left(N\in {\mathbb{N}}_0\to \left(\frac{N+1}{2}\in {\mathbb{N}}_0\to \left(N=1\vee 2<N\right)\right)\right)$$
37		orc	$$⊢N=1\to \left(N=1\vee 2<N\right)$$
38	37	eqcoms	$$⊢1=N\to \left(N=1\vee 2<N\right)$$
39	38	2a1d	$$⊢1=N\to \left(N\in {\mathbb{N}}_0\to \left(\frac{N+1}{2}\in {\mathbb{N}}_0\to \left(N=1\vee 2<N\right)\right)\right)$$
40	36 39	jaoi	$$⊢\left(1<N\vee 1=N\right)\to \left(N\in {\mathbb{N}}_0\to \left(\frac{N+1}{2}\in {\mathbb{N}}_0\to \left(N=1\vee 2<N\right)\right)\right)$$
41	40	com12	$$⊢N\in {\mathbb{N}}_0\to \left(\left(1<N\vee 1=N\right)\to \left(\frac{N+1}{2}\in {\mathbb{N}}_0\to \left(N=1\vee 2<N\right)\right)\right)$$
42	5 41	sylbid	$$⊢N\in {\mathbb{N}}_0\to \left(1\le N\to \left(\frac{N+1}{2}\in {\mathbb{N}}_0\to \left(N=1\vee 2<N\right)\right)\right)$$
43	42	imp	$$⊢\left(N\in {\mathbb{N}}_0\wedge 1\le N\right)\to \left(\frac{N+1}{2}\in {\mathbb{N}}_0\to \left(N=1\vee 2<N\right)\right)$$
44	2 43	sylbi	$$⊢N\in \mathbb{N}\to \left(\frac{N+1}{2}\in {\mathbb{N}}_0\to \left(N=1\vee 2<N\right)\right)$$
45		oveq1	$$⊢N=0\to N+1=0+1$$
46		0p1e1	$$⊢0+1=1$$
47	45 46	eqtrdi	$$⊢N=0\to N+1=1$$
48	47	oveq1d	$$⊢N=0\to \frac{N+1}{2}=\frac{1}{2}$$
49	48	eleq1d	$$⊢N=0\to \left(\frac{N+1}{2}\in {\mathbb{N}}_0\leftrightarrow \frac{1}{2}\in {\mathbb{N}}_0\right)$$
50		halfnz	$$⊢\neg \frac{1}{2}\in \mathbb{Z}$$
51		nn0z	$$⊢\frac{1}{2}\in {\mathbb{N}}_0\to \frac{1}{2}\in \mathbb{Z}$$
52	51	pm2.24d	$$⊢\frac{1}{2}\in {\mathbb{N}}_0\to \left(\neg \frac{1}{2}\in \mathbb{Z}\to \left(N=1\vee 2<N\right)\right)$$
53	50 52	mpi	$$⊢\frac{1}{2}\in {\mathbb{N}}_0\to \left(N=1\vee 2<N\right)$$
54	49 53	biimtrdi	$$⊢N=0\to \left(\frac{N+1}{2}\in {\mathbb{N}}_0\to \left(N=1\vee 2<N\right)\right)$$
55	44 54	jaoi	$$⊢\left(N\in \mathbb{N}\vee N=0\right)\to \left(\frac{N+1}{2}\in {\mathbb{N}}_0\to \left(N=1\vee 2<N\right)\right)$$
56	1 55	sylbi	$$⊢N\in {\mathbb{N}}_0\to \left(\frac{N+1}{2}\in {\mathbb{N}}_0\to \left(N=1\vee 2<N\right)\right)$$
57	56	imp	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N+1}{2}\in {\mathbb{N}}_0\right)\to \left(N=1\vee 2<N\right)$$