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 𝑁 ∈ ℕ
Assertion nneoi ( ( 𝑁 / 2 ) ∈ ℕ ↔ ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ )

Proof

Step Hyp Ref Expression
1 nneoi.1 𝑁 ∈ ℕ
2 nneo ( 𝑁 ∈ ℕ → ( ( 𝑁 / 2 ) ∈ ℕ ↔ ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) )
3 1 2 ax-mp ( ( 𝑁 / 2 ) ∈ ℕ ↔ ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ )