Metamath Proof Explorer

Theorem oddm1even

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

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

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( N e. ZZ /\ n e. ZZ ) -> N e. ZZ )
2 1 zcnd 
 |-  ( ( N e. ZZ /\ n e. ZZ ) -> N e. CC )
3 1cnd 
 |-  ( ( N e. ZZ /\ n e. ZZ ) -> 1 e. CC )
4 2cnd 
 |-  ( ( N e. ZZ /\ n e. ZZ ) -> 2 e. CC )
5 simpr 
 |-  ( ( N e. ZZ /\ n e. ZZ ) -> n e. ZZ )
6 5 zcnd 
 |-  ( ( N e. ZZ /\ n e. ZZ ) -> n e. CC )
7 4 6 mulcld 
 |-  ( ( N e. ZZ /\ n e. ZZ ) -> ( 2 x. n ) e. CC )
8 2 3 7 subadd2d 
 |-  ( ( N e. ZZ /\ n e. ZZ ) -> ( ( N - 1 ) = ( 2 x. n ) <-> ( ( 2 x. n ) + 1 ) = N ) )
9 eqcom 
 |-  ( ( N - 1 ) = ( 2 x. n ) <-> ( 2 x. n ) = ( N - 1 ) )
10 4 6 mulcomd 
 |-  ( ( N e. ZZ /\ n e. ZZ ) -> ( 2 x. n ) = ( n x. 2 ) )
11 10 eqeq1d 
 |-  ( ( N e. ZZ /\ n e. ZZ ) -> ( ( 2 x. n ) = ( N - 1 ) <-> ( n x. 2 ) = ( N - 1 ) ) )
12 9 11 bitrid 
 |-  ( ( N e. ZZ /\ n e. ZZ ) -> ( ( N - 1 ) = ( 2 x. n ) <-> ( n x. 2 ) = ( N - 1 ) ) )
13 8 12 bitr3d 
 |-  ( ( N e. ZZ /\ n e. ZZ ) -> ( ( ( 2 x. n ) + 1 ) = N <-> ( n x. 2 ) = ( N - 1 ) ) )
14 13 rexbidva 
 |-  ( N e. ZZ -> ( E. n e. ZZ ( ( 2 x. n ) + 1 ) = N <-> E. n e. ZZ ( n x. 2 ) = ( N - 1 ) ) )
15 odd2np1 
 |-  ( N e. ZZ -> ( -. 2 || N <-> E. n e. ZZ ( ( 2 x. n ) + 1 ) = N ) )
16 2z 
 |-  2 e. ZZ
17 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
18 divides 
 |-  ( ( 2 e. ZZ /\ ( N - 1 ) e. ZZ ) -> ( 2 || ( N - 1 ) <-> E. n e. ZZ ( n x. 2 ) = ( N - 1 ) ) )
19 16 17 18 sylancr 
 |-  ( N e. ZZ -> ( 2 || ( N - 1 ) <-> E. n e. ZZ ( n x. 2 ) = ( N - 1 ) ) )
20 14 15 19 3bitr4d 
 |-  ( N e. ZZ -> ( -. 2 || N <-> 2 || ( N - 1 ) ) )