Theorem nneom

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

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

Proof

Step	Hyp	Ref	Expression
1		nneop	$$⊢N\in \mathbb{N}\to \left(\frac{N}{2}\in \mathbb{N}\vee \frac{N+1}{2}\in \mathbb{N}\right)$$
2		nnnn0	$$⊢N\in \mathbb{N}\to N\in {\mathbb{N}}_0$$
3		nnnn0	$$⊢\frac{N+1}{2}\in \mathbb{N}\to \frac{N+1}{2}\in {\mathbb{N}}_0$$
4		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$$
5	2 3 4	syl2an	$$⊢\left(N\in \mathbb{N}\wedge \frac{N+1}{2}\in \mathbb{N}\right)\to \frac{N-1}{2}\in {\mathbb{N}}_0$$
6	5	ex	$$⊢N\in \mathbb{N}\to \left(\frac{N+1}{2}\in \mathbb{N}\to \frac{N-1}{2}\in {\mathbb{N}}_0\right)$$
7	6	orim2d	$$⊢N\in \mathbb{N}\to \left(\left(\frac{N}{2}\in \mathbb{N}\vee \frac{N+1}{2}\in \mathbb{N}\right)\to \left(\frac{N}{2}\in \mathbb{N}\vee \frac{N-1}{2}\in {\mathbb{N}}_0\right)\right)$$
8	1 7	mpd	$$⊢N\in \mathbb{N}\to \left(\frac{N}{2}\in \mathbb{N}\vee \frac{N-1}{2}\in {\mathbb{N}}_0\right)$$