Theorem nn0o

Description: An alternate characterization of an odd nonnegative integer. (Contributed by AV, 28-May-2020) (Proof shortened by AV, 2-Jun-2020)

	Ref	Expression
Assertion	nn0o	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N+1}{2}\in {\mathbb{N}}_0\right)\to \frac{N-1}{2}\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		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)$$
2		1m1e0	$$⊢1-1=0$$
3	2	oveq1i	$$⊢\frac{1-1}{2}=\frac{0}{2}$$
4		2cn	$$⊢2\in ℂ$$
5		2ne0	$$⊢2\ne 0$$
6	4 5	div0i	$$⊢\frac{0}{2}=0$$
7	3 6	eqtri	$$⊢\frac{1-1}{2}=0$$
8		0nn0	$$⊢0\in {\mathbb{N}}_0$$
9	7 8	eqeltri	$$⊢\frac{1-1}{2}\in {\mathbb{N}}_0$$
10		oveq1	$$⊢N=1\to N-1=1-1$$
11	10	oveq1d	$$⊢N=1\to \frac{N-1}{2}=\frac{1-1}{2}$$
12	11	eleq1d	$$⊢N=1\to \left(\frac{N-1}{2}\in {\mathbb{N}}_0\leftrightarrow \frac{1-1}{2}\in {\mathbb{N}}_0\right)$$
13	12	adantr	$$⊢\left(N=1\wedge \left(N\in {\mathbb{N}}_0\wedge \frac{N+1}{2}\in {\mathbb{N}}_0\right)\right)\to \left(\frac{N-1}{2}\in {\mathbb{N}}_0\leftrightarrow \frac{1-1}{2}\in {\mathbb{N}}_0\right)$$
14	9 13	mpbiri	$$⊢\left(N=1\wedge \left(N\in {\mathbb{N}}_0\wedge \frac{N+1}{2}\in {\mathbb{N}}_0\right)\right)\to \frac{N-1}{2}\in {\mathbb{N}}_0$$
15	14	ex	$$⊢N=1\to \left(\left(N\in {\mathbb{N}}_0\wedge \frac{N+1}{2}\in {\mathbb{N}}_0\right)\to \frac{N-1}{2}\in {\mathbb{N}}_0\right)$$
16		2z	$$⊢2\in \mathbb{Z}$$
17	16	a1i	$$⊢\left(2<N\wedge \left(N\in {\mathbb{N}}_0\wedge \frac{N+1}{2}\in {\mathbb{N}}_0\right)\right)\to 2\in \mathbb{Z}$$
18		nn0z	$$⊢N\in {\mathbb{N}}_0\to N\in \mathbb{Z}$$
19	18	ad2antrl	$$⊢\left(2<N\wedge \left(N\in {\mathbb{N}}_0\wedge \frac{N+1}{2}\in {\mathbb{N}}_0\right)\right)\to N\in \mathbb{Z}$$
20		2re	$$⊢2\in ℝ$$
21		nn0re	$$⊢N\in {\mathbb{N}}_0\to N\in ℝ$$
22		ltle	$$⊢\left(2\in ℝ\wedge N\in ℝ\right)\to \left(2<N\to 2\le N\right)$$
23	20 21 22	sylancr	$$⊢N\in {\mathbb{N}}_0\to \left(2<N\to 2\le N\right)$$
24	23	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N+1}{2}\in {\mathbb{N}}_0\right)\to \left(2<N\to 2\le N\right)$$
25	24	impcom	$$⊢\left(2<N\wedge \left(N\in {\mathbb{N}}_0\wedge \frac{N+1}{2}\in {\mathbb{N}}_0\right)\right)\to 2\le N$$
26		eluz2	$$⊢N\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(2\in \mathbb{Z}\wedge N\in \mathbb{Z}\wedge 2\le N\right)$$
27	17 19 25 26	syl3anbrc	$$⊢\left(2<N\wedge \left(N\in {\mathbb{N}}_0\wedge \frac{N+1}{2}\in {\mathbb{N}}_0\right)\right)\to N\in {\mathbb{Z}}_{\ge 2}$$
28		simprr	$$⊢\left(2<N\wedge \left(N\in {\mathbb{N}}_0\wedge \frac{N+1}{2}\in {\mathbb{N}}_0\right)\right)\to \frac{N+1}{2}\in {\mathbb{N}}_0$$
29	27 28	jca	$$⊢\left(2<N\wedge \left(N\in {\mathbb{N}}_0\wedge \frac{N+1}{2}\in {\mathbb{N}}_0\right)\right)\to \left(N\in {\mathbb{Z}}_{\ge 2}\wedge \frac{N+1}{2}\in {\mathbb{N}}_0\right)$$
30		nno	$$⊢\left(N\in {\mathbb{Z}}_{\ge 2}\wedge \frac{N+1}{2}\in {\mathbb{N}}_0\right)\to \frac{N-1}{2}\in \mathbb{N}$$
31		nnnn0	$$⊢\frac{N-1}{2}\in \mathbb{N}\to \frac{N-1}{2}\in {\mathbb{N}}_0$$
32	29 30 31	3syl	$$⊢\left(2<N\wedge \left(N\in {\mathbb{N}}_0\wedge \frac{N+1}{2}\in {\mathbb{N}}_0\right)\right)\to \frac{N-1}{2}\in {\mathbb{N}}_0$$
33	32	ex	$$⊢2<N\to \left(\left(N\in {\mathbb{N}}_0\wedge \frac{N+1}{2}\in {\mathbb{N}}_0\right)\to \frac{N-1}{2}\in {\mathbb{N}}_0\right)$$
34	15 33	jaoi	$$⊢\left(N=1\vee 2<N\right)\to \left(\left(N\in {\mathbb{N}}_0\wedge \frac{N+1}{2}\in {\mathbb{N}}_0\right)\to \frac{N-1}{2}\in {\mathbb{N}}_0\right)$$
35	1 34	mpcom	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N+1}{2}\in {\mathbb{N}}_0\right)\to \frac{N-1}{2}\in {\mathbb{N}}_0$$