This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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