Metamath Proof Explorer

Theorem zob

Description: Alternate characterizations of an odd number. (Contributed by AV, 7-Jun-2020)

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

Proof

Step Hyp Ref Expression
1 peano2zm 
 |-  ( ( ( N + 1 ) / 2 ) e. ZZ -> ( ( ( N + 1 ) / 2 ) - 1 ) e. ZZ )
2 peano2z 
 |-  ( ( ( ( N + 1 ) / 2 ) - 1 ) e. ZZ -> ( ( ( ( N + 1 ) / 2 ) - 1 ) + 1 ) e. ZZ )
3 peano2z 
 |-  ( N e. ZZ -> ( N + 1 ) e. ZZ )
4 3 zcnd 
 |-  ( N e. ZZ -> ( N + 1 ) e. CC )
5 4 halfcld 
 |-  ( N e. ZZ -> ( ( N + 1 ) / 2 ) e. CC )
6 npcan1 
 |-  ( ( ( N + 1 ) / 2 ) e. CC -> ( ( ( ( N + 1 ) / 2 ) - 1 ) + 1 ) = ( ( N + 1 ) / 2 ) )
7 5 6 syl 
 |-  ( N e. ZZ -> ( ( ( ( N + 1 ) / 2 ) - 1 ) + 1 ) = ( ( N + 1 ) / 2 ) )
8 7 eqcomd 
 |-  ( N e. ZZ -> ( ( N + 1 ) / 2 ) = ( ( ( ( N + 1 ) / 2 ) - 1 ) + 1 ) )
9 8 eleq1d 
 |-  ( N e. ZZ -> ( ( ( N + 1 ) / 2 ) e. ZZ <-> ( ( ( ( N + 1 ) / 2 ) - 1 ) + 1 ) e. ZZ ) )
10 2 9 imbitrrid 
 |-  ( N e. ZZ -> ( ( ( ( N + 1 ) / 2 ) - 1 ) e. ZZ -> ( ( N + 1 ) / 2 ) e. ZZ ) )
11 1 10 impbid2 
 |-  ( N e. ZZ -> ( ( ( N + 1 ) / 2 ) e. ZZ <-> ( ( ( N + 1 ) / 2 ) - 1 ) e. ZZ ) )
12 zcn 
 |-  ( N e. ZZ -> N e. CC )
13 xp1d2m1eqxm1d2 
 |-  ( N e. CC -> ( ( ( N + 1 ) / 2 ) - 1 ) = ( ( N - 1 ) / 2 ) )
14 12 13 syl 
 |-  ( N e. ZZ -> ( ( ( N + 1 ) / 2 ) - 1 ) = ( ( N - 1 ) / 2 ) )
15 14 eleq1d 
 |-  ( N e. ZZ -> ( ( ( ( N + 1 ) / 2 ) - 1 ) e. ZZ <-> ( ( N - 1 ) / 2 ) e. ZZ ) )
16 11 15 bitrd 
 |-  ( N e. ZZ -> ( ( ( N + 1 ) / 2 ) e. ZZ <-> ( ( N - 1 ) / 2 ) e. ZZ ) )