Metamath Proof Explorer

Theorem nneoALTV

Description: A positive integer is even or odd but not both. (Contributed by NM, 1-Jan-2006) (Revised by AV, 19-Jun-2020)

Ref Expression
Assertion nneoALTV 
|- ( N e. NN -> ( N e. Even <-> -. N e. Odd ) )

Proof

Step Hyp Ref Expression
1 nnz 
 |-  ( N e. NN -> N e. ZZ )
2 zeo2ALTV 
 |-  ( N e. ZZ -> ( N e. Even <-> -. N e. Odd ) )
3 1 2 syl 
 |-  ( N e. NN -> ( N e. Even <-> -. N e. Odd ) )