Theorem nneoi

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

	Ref	Expression
Hypothesis	nneoi.1	⊢ 𝑁 ∈ ℕ
Assertion	nneoi	⊢ ( ( 𝑁 / 2 ) ∈ ℕ ↔ ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		nneoi.1	⊢ 𝑁 ∈ ℕ
2		nneo	⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 / 2 ) ∈ ℕ ↔ ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) )
3	1 2	ax-mp	⊢ ( ( 𝑁 / 2 ) ∈ ℕ ↔ ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ )