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 e. NN
Assertion nneoi
|- ( ( N / 2 ) e. NN <-> -. ( ( N + 1 ) / 2 ) e. NN )

Proof

Step Hyp Ref Expression
1 nneoi.1
 |-  N e. NN
2 nneo
 |-  ( N e. NN -> ( ( N / 2 ) e. NN <-> -. ( ( N + 1 ) / 2 ) e. NN ) )
3 1 2 ax-mp
 |-  ( ( N / 2 ) e. NN <-> -. ( ( N + 1 ) / 2 ) e. NN )