Metamath Proof Explorer

Theorem oddp1even

Description: An integer is odd iff its successor is even. (Contributed by Mario Carneiro, 5-Sep-2016)

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

Proof

Step Hyp Ref Expression
1 oddm1even 
 |-  ( N e. ZZ -> ( -. 2 || N <-> 2 || ( N - 1 ) ) )
2 2z 
 |-  2 e. ZZ
3 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
4 dvdsadd 
 |-  ( ( 2 e. ZZ /\ ( N - 1 ) e. ZZ ) -> ( 2 || ( N - 1 ) <-> 2 || ( 2 + ( N - 1 ) ) ) )
5 2 3 4 sylancr 
 |-  ( N e. ZZ -> ( 2 || ( N - 1 ) <-> 2 || ( 2 + ( N - 1 ) ) ) )
6 2cnd 
 |-  ( N e. ZZ -> 2 e. CC )
7 zcn 
 |-  ( N e. ZZ -> N e. CC )
8 1cnd 
 |-  ( N e. ZZ -> 1 e. CC )
9 6 7 8 addsub12d 
 |-  ( N e. ZZ -> ( 2 + ( N - 1 ) ) = ( N + ( 2 - 1 ) ) )
10 2m1e1 
 |-  ( 2 - 1 ) = 1
11 10 oveq2i 
 |-  ( N + ( 2 - 1 ) ) = ( N + 1 )
12 9 11 eqtrdi 
 |-  ( N e. ZZ -> ( 2 + ( N - 1 ) ) = ( N + 1 ) )
13 12 breq2d 
 |-  ( N e. ZZ -> ( 2 || ( 2 + ( N - 1 ) ) <-> 2 || ( N + 1 ) ) )
14 1 5 13 3bitrd 
 |-  ( N e. ZZ -> ( -. 2 || N <-> 2 || ( N + 1 ) ) )