Theorem nneop

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

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

Proof

Step	Hyp	Ref	Expression
1		nneo	$$⊢N\in \mathbb{N}\to \left(\frac{N}{2}\in \mathbb{N}\leftrightarrow \neg \frac{N+1}{2}\in \mathbb{N}\right)$$
2	1	biimprd	$$⊢N\in \mathbb{N}\to \left(\neg \frac{N+1}{2}\in \mathbb{N}\to \frac{N}{2}\in \mathbb{N}\right)$$
3	2	orrd	$$⊢N\in \mathbb{N}\to \left(\frac{N+1}{2}\in \mathbb{N}\vee \frac{N}{2}\in \mathbb{N}\right)$$
4	3	orcomd	$$⊢N\in \mathbb{N}\to \left(\frac{N}{2}\in \mathbb{N}\vee \frac{N+1}{2}\in \mathbb{N}\right)$$