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 )