Theorem nneoiALTV

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

	Ref	Expression
Hypothesis	nneoiALTV.1	$$⊢N\in \mathbb{N}$$
Assertion	nneoiALTV	$$⊢N\in \mathrm{Even}\leftrightarrow \neg N\in \mathrm{Odd}$$

Proof

Step	Hyp	Ref	Expression
1		nneoiALTV.1	$$⊢N\in \mathbb{N}$$
2		nneoALTV	$$⊢N\in \mathbb{N}\to \left(N\in \mathrm{Even}\leftrightarrow \neg N\in \mathrm{Odd}\right)$$
3	1 2	ax-mp	$$⊢N\in \mathrm{Even}\leftrightarrow \neg N\in \mathrm{Odd}$$