Theorem nneoi

Description: A positive integer is even or odd but not both. (Contributed by NM, 20-Aug-2001)

	Ref	Expression
Hypothesis	nneoi.1	$$⊢N\in \mathbb{N}$$
Assertion	nneoi	$$⊢\frac{N}{2}\in \mathbb{N}\leftrightarrow \neg \frac{N+1}{2}\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		nneoi.1	$$⊢N\in \mathbb{N}$$
2		nneo	$$⊢N\in \mathbb{N}\to \left(\frac{N}{2}\in \mathbb{N}\leftrightarrow \neg \frac{N+1}{2}\in \mathbb{N}\right)$$
3	1 2	ax-mp	$$⊢\frac{N}{2}\in \mathbb{N}\leftrightarrow \neg \frac{N+1}{2}\in \mathbb{N}$$