Metamath Proof Explorer

Theorem nneop

Description: A positive integer is even or odd. (Contributed by AV, 30-May-2020)

Ref Expression
Assertion nneop 
|- ( N e. NN -> ( ( N / 2 ) e. NN \/ ( ( N + 1 ) / 2 ) e. NN ) )

Proof

Step Hyp Ref Expression
1 nneo 
 |-  ( N e. NN -> ( ( N / 2 ) e. NN <-> -. ( ( N + 1 ) / 2 ) e. NN ) )
2 1 biimprd 
 |-  ( N e. NN -> ( -. ( ( N + 1 ) / 2 ) e. NN -> ( N / 2 ) e. NN ) )
3 2 orrd 
 |-  ( N e. NN -> ( ( ( N + 1 ) / 2 ) e. NN \/ ( N / 2 ) e. NN ) )
4 3 orcomd 
 |-  ( N e. NN -> ( ( N / 2 ) e. NN \/ ( ( N + 1 ) / 2 ) e. NN ) )