Metamath Proof Explorer

Theorem zeo2

Description: An integer is even or odd but not both. (Contributed by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion zeo2 
|- ( N e. ZZ -> ( ( N / 2 ) e. ZZ <-> -. ( ( N + 1 ) / 2 ) e. ZZ ) )

Proof

Step Hyp Ref Expression
1 zcn 
 |-  ( N e. ZZ -> N e. CC )
2 peano2cn 
 |-  ( N e. CC -> ( N + 1 ) e. CC )
3 1 2 syl 
 |-  ( N e. ZZ -> ( N + 1 ) e. CC )
4 2cnd 
 |-  ( N e. ZZ -> 2 e. CC )
5 2ne0 
 |-  2 =/= 0
6 5 a1i 
 |-  ( N e. ZZ -> 2 =/= 0 )
7 3 4 6 divcan2d 
 |-  ( N e. ZZ -> ( 2 x. ( ( N + 1 ) / 2 ) ) = ( N + 1 ) )
8 1 4 6 divcan2d 
 |-  ( N e. ZZ -> ( 2 x. ( N / 2 ) ) = N )
9 8 oveq1d 
 |-  ( N e. ZZ -> ( ( 2 x. ( N / 2 ) ) + 1 ) = ( N + 1 ) )
10 7 9 eqtr4d 
 |-  ( N e. ZZ -> ( 2 x. ( ( N + 1 ) / 2 ) ) = ( ( 2 x. ( N / 2 ) ) + 1 ) )
11 zneo 
 |-  ( ( ( ( N + 1 ) / 2 ) e. ZZ /\ ( N / 2 ) e. ZZ ) -> ( 2 x. ( ( N + 1 ) / 2 ) ) =/= ( ( 2 x. ( N / 2 ) ) + 1 ) )
12 11 expcom 
 |-  ( ( N / 2 ) e. ZZ -> ( ( ( N + 1 ) / 2 ) e. ZZ -> ( 2 x. ( ( N + 1 ) / 2 ) ) =/= ( ( 2 x. ( N / 2 ) ) + 1 ) ) )
13 12 necon2bd 
 |-  ( ( N / 2 ) e. ZZ -> ( ( 2 x. ( ( N + 1 ) / 2 ) ) = ( ( 2 x. ( N / 2 ) ) + 1 ) -> -. ( ( N + 1 ) / 2 ) e. ZZ ) )
14 10 13 syl5com 
 |-  ( N e. ZZ -> ( ( N / 2 ) e. ZZ -> -. ( ( N + 1 ) / 2 ) e. ZZ ) )
15 zeo 
 |-  ( N e. ZZ -> ( ( N / 2 ) e. ZZ \/ ( ( N + 1 ) / 2 ) e. ZZ ) )
16 15 ord 
 |-  ( N e. ZZ -> ( -. ( N / 2 ) e. ZZ -> ( ( N + 1 ) / 2 ) e. ZZ ) )
17 16 con1d 
 |-  ( N e. ZZ -> ( -. ( ( N + 1 ) / 2 ) e. ZZ -> ( N / 2 ) e. ZZ ) )
18 14 17 impbid 
 |-  ( N e. ZZ -> ( ( N / 2 ) e. ZZ <-> -. ( ( N + 1 ) / 2 ) e. ZZ ) )