Theorem nneoALTV

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

	Ref	Expression
Assertion	nneoALTV	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ Even ↔ ¬ 𝑁 ∈ Odd ) )

Proof

Step	Hyp	Ref	Expression
1		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
2		zeo2ALTV	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ∈ Even ↔ ¬ 𝑁 ∈ Odd ) )
3	1 2	syl	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ Even ↔ ¬ 𝑁 ∈ Odd ) )