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

Metamath Proof Explorer

Theorem nneoi

Description: A positive integer is even or odd but not both. (Contributed by NM, 20-Aug-2001)

Ref Expression
Hypothesis nneoi.1 ⊢ N ∈ ℕ
Assertion nneoi ⊢ N 2 ∈ ℕ ↔ ¬ N + 1 2 ∈ ℕ

Proof

Step Hyp Ref Expression
1 nneoi.1 ⊢ N ∈ ℕ
2 nneo ⊢ N ∈ ℕ → N 2 ∈ ℕ ↔ ¬ N + 1 2 ∈ ℕ
3 1 2 ax-mp ⊢ N 2 ∈ ℕ ↔ ¬ N + 1 2 ∈ ℕ