Metamath Proof Explorer

Theorem nn0ob

Description: Alternate characterizations of an odd nonnegative integer. (Contributed by AV, 4-Jun-2020)

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

Proof

Step Hyp Ref Expression
1 nn0o 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( N - 1 ) / 2 ) e. NN0 )
2 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
3 xp1d2m1eqxm1d2 
 |-  ( N e. CC -> ( ( ( N + 1 ) / 2 ) - 1 ) = ( ( N - 1 ) / 2 ) )
4 3 eqcomd 
 |-  ( N e. CC -> ( ( N - 1 ) / 2 ) = ( ( ( N + 1 ) / 2 ) - 1 ) )
5 2 4 syl 
 |-  ( N e. NN0 -> ( ( N - 1 ) / 2 ) = ( ( ( N + 1 ) / 2 ) - 1 ) )
6 peano2cnm 
 |-  ( N e. CC -> ( N - 1 ) e. CC )
7 2 6 syl 
 |-  ( N e. NN0 -> ( N - 1 ) e. CC )
8 7 halfcld 
 |-  ( N e. NN0 -> ( ( N - 1 ) / 2 ) e. CC )
9 1cnd 
 |-  ( N e. NN0 -> 1 e. CC )
10 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
11 10 nn0cnd 
 |-  ( N e. NN0 -> ( N + 1 ) e. CC )
12 11 halfcld 
 |-  ( N e. NN0 -> ( ( N + 1 ) / 2 ) e. CC )
13 8 9 12 addlsub 
 |-  ( N e. NN0 -> ( ( ( ( N - 1 ) / 2 ) + 1 ) = ( ( N + 1 ) / 2 ) <-> ( ( N - 1 ) / 2 ) = ( ( ( N + 1 ) / 2 ) - 1 ) ) )
14 5 13 mpbird 
 |-  ( N e. NN0 -> ( ( ( N - 1 ) / 2 ) + 1 ) = ( ( N + 1 ) / 2 ) )
15 14 adantr 
 |-  ( ( N e. NN0 /\ ( ( N - 1 ) / 2 ) e. NN0 ) -> ( ( ( N - 1 ) / 2 ) + 1 ) = ( ( N + 1 ) / 2 ) )
16 peano2nn0 
 |-  ( ( ( N - 1 ) / 2 ) e. NN0 -> ( ( ( N - 1 ) / 2 ) + 1 ) e. NN0 )
17 16 adantl 
 |-  ( ( N e. NN0 /\ ( ( N - 1 ) / 2 ) e. NN0 ) -> ( ( ( N - 1 ) / 2 ) + 1 ) e. NN0 )
18 15 17 eqeltrrd 
 |-  ( ( N e. NN0 /\ ( ( N - 1 ) / 2 ) e. NN0 ) -> ( ( N + 1 ) / 2 ) e. NN0 )
19 1 18 impbida 
 |-  ( N e. NN0 -> ( ( ( N + 1 ) / 2 ) e. NN0 <-> ( ( N - 1 ) / 2 ) e. NN0 ) )