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