Theorem nn0eo

Description: A nonnegative integer is even or odd. (Contributed by AV, 27-May-2020)

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

Proof

Step	Hyp	Ref	Expression
1		nn0z	$$⊢N\in {\mathbb{N}}_0\to N\in \mathbb{Z}$$
2		zeo	$$⊢N\in \mathbb{Z}\to \left(\frac{N}{2}\in \mathbb{Z}\vee \frac{N+1}{2}\in \mathbb{Z}\right)$$
3	1 2	syl	$$⊢N\in {\mathbb{N}}_0\to \left(\frac{N}{2}\in \mathbb{Z}\vee \frac{N+1}{2}\in \mathbb{Z}\right)$$
4		simpr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N}{2}\in \mathbb{Z}\right)\to \frac{N}{2}\in \mathbb{Z}$$
5		nn0re	$$⊢N\in {\mathbb{N}}_0\to N\in ℝ$$
6		nn0ge0	$$⊢N\in {\mathbb{N}}_0\to 0\le N$$
7		2re	$$⊢2\in ℝ$$
8	7	a1i	$$⊢N\in {\mathbb{N}}_0\to 2\in ℝ$$
9		2pos	$$⊢0<2$$
10	9	a1i	$$⊢N\in {\mathbb{N}}_0\to 0<2$$
11		divge0	$$⊢\left(\left(N\in ℝ\wedge 0\le N\right)\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to 0\le \frac{N}{2}$$
12	5 6 8 10 11	syl22anc	$$⊢N\in {\mathbb{N}}_0\to 0\le \frac{N}{2}$$
13	12	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N}{2}\in \mathbb{Z}\right)\to 0\le \frac{N}{2}$$
14		elnn0z	$$⊢\frac{N}{2}\in {\mathbb{N}}_0\leftrightarrow \left(\frac{N}{2}\in \mathbb{Z}\wedge 0\le \frac{N}{2}\right)$$
15	4 13 14	sylanbrc	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N}{2}\in \mathbb{Z}\right)\to \frac{N}{2}\in {\mathbb{N}}_0$$
16	15	ex	$$⊢N\in {\mathbb{N}}_0\to \left(\frac{N}{2}\in \mathbb{Z}\to \frac{N}{2}\in {\mathbb{N}}_0\right)$$
17		simpr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N+1}{2}\in \mathbb{Z}\right)\to \frac{N+1}{2}\in \mathbb{Z}$$
18		peano2nn0	$$⊢N\in {\mathbb{N}}_0\to N+1\in {\mathbb{N}}_0$$
19	18	nn0red	$$⊢N\in {\mathbb{N}}_0\to N+1\in ℝ$$
20		1red	$$⊢N\in {\mathbb{N}}_0\to 1\in ℝ$$
21		0le1	$$⊢0\le 1$$
22	21	a1i	$$⊢N\in {\mathbb{N}}_0\to 0\le 1$$
23	5 20 6 22	addge0d	$$⊢N\in {\mathbb{N}}_0\to 0\le N+1$$
24		divge0	$$⊢\left(\left(N+1\in ℝ\wedge 0\le N+1\right)\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to 0\le \frac{N+1}{2}$$
25	19 23 8 10 24	syl22anc	$$⊢N\in {\mathbb{N}}_0\to 0\le \frac{N+1}{2}$$
26	25	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N+1}{2}\in \mathbb{Z}\right)\to 0\le \frac{N+1}{2}$$
27		elnn0z	$$⊢\frac{N+1}{2}\in {\mathbb{N}}_0\leftrightarrow \left(\frac{N+1}{2}\in \mathbb{Z}\wedge 0\le \frac{N+1}{2}\right)$$
28	17 26 27	sylanbrc	$$⊢\left(N\in {\mathbb{N}}_0\wedge \frac{N+1}{2}\in \mathbb{Z}\right)\to \frac{N+1}{2}\in {\mathbb{N}}_0$$
29	28	ex	$$⊢N\in {\mathbb{N}}_0\to \left(\frac{N+1}{2}\in \mathbb{Z}\to \frac{N+1}{2}\in {\mathbb{N}}_0\right)$$
30	16 29	orim12d	$$⊢N\in {\mathbb{N}}_0\to \left(\left(\frac{N}{2}\in \mathbb{Z}\vee \frac{N+1}{2}\in \mathbb{Z}\right)\to \left(\frac{N}{2}\in {\mathbb{N}}_0\vee \frac{N+1}{2}\in {\mathbb{N}}_0\right)\right)$$
31	3 30	mpd	$$⊢N\in {\mathbb{N}}_0\to \left(\frac{N}{2}\in {\mathbb{N}}_0\vee \frac{N+1}{2}\in {\mathbb{N}}_0\right)$$