Metamath Proof Explorer


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 𝑁 ∈ ℕ
Assertion nneoiALTV ( 𝑁 ∈ Even ↔ ¬ 𝑁 ∈ Odd )

Proof

Step Hyp Ref Expression
1 nneoiALTV.1 𝑁 ∈ ℕ
2 nneoALTV ( 𝑁 ∈ ℕ → ( 𝑁 ∈ Even ↔ ¬ 𝑁 ∈ Odd ) )
3 1 2 ax-mp ( 𝑁 ∈ Even ↔ ¬ 𝑁 ∈ Odd )