Metamath Proof Explorer

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 ⊢ N ∈ ℕ → N ∈ Even ↔ ¬ N ∈ Odd

Proof

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