Metamath Proof Explorer

Theorem nn0onn0ex

Description: For each odd nonnegative integer there is a nonnegative integer which, multiplied by 2 and increased by 1, results in the odd nonnegative integer. (Contributed by AV, 30-May-2020)

Ref Expression
Assertion nn0onn0ex 
|- ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> E. m e. NN0 N = ( ( 2 x. m ) + 1 ) )

Proof

Step Hyp Ref Expression
1 nn0o 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( N - 1 ) / 2 ) e. NN0 )
2 simpr 
 |-  ( ( N e. NN0 /\ ( ( N - 1 ) / 2 ) e. NN0 ) -> ( ( N - 1 ) / 2 ) e. NN0 )
3 oveq2 
 |-  ( m = ( ( N - 1 ) / 2 ) -> ( 2 x. m ) = ( 2 x. ( ( N - 1 ) / 2 ) ) )
4 3 oveq1d 
 |-  ( m = ( ( N - 1 ) / 2 ) -> ( ( 2 x. m ) + 1 ) = ( ( 2 x. ( ( N - 1 ) / 2 ) ) + 1 ) )
5 4 eqeq2d 
 |-  ( m = ( ( N - 1 ) / 2 ) -> ( N = ( ( 2 x. m ) + 1 ) <-> N = ( ( 2 x. ( ( N - 1 ) / 2 ) ) + 1 ) ) )
6 5 adantl 
 |-  ( ( ( N e. NN0 /\ ( ( N - 1 ) / 2 ) e. NN0 ) /\ m = ( ( N - 1 ) / 2 ) ) -> ( N = ( ( 2 x. m ) + 1 ) <-> N = ( ( 2 x. ( ( N - 1 ) / 2 ) ) + 1 ) ) )
7 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
8 peano2cnm 
 |-  ( N e. CC -> ( N - 1 ) e. CC )
9 7 8 syl 
 |-  ( N e. NN0 -> ( N - 1 ) e. CC )
10 2cnd 
 |-  ( N e. NN0 -> 2 e. CC )
11 2ne0 
 |-  2 =/= 0
12 11 a1i 
 |-  ( N e. NN0 -> 2 =/= 0 )
13 9 10 12 divcan2d 
 |-  ( N e. NN0 -> ( 2 x. ( ( N - 1 ) / 2 ) ) = ( N - 1 ) )
14 13 oveq1d 
 |-  ( N e. NN0 -> ( ( 2 x. ( ( N - 1 ) / 2 ) ) + 1 ) = ( ( N - 1 ) + 1 ) )
15 npcan1 
 |-  ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
16 7 15 syl 
 |-  ( N e. NN0 -> ( ( N - 1 ) + 1 ) = N )
17 14 16 eqtr2d 
 |-  ( N e. NN0 -> N = ( ( 2 x. ( ( N - 1 ) / 2 ) ) + 1 ) )
18 17 adantr 
 |-  ( ( N e. NN0 /\ ( ( N - 1 ) / 2 ) e. NN0 ) -> N = ( ( 2 x. ( ( N - 1 ) / 2 ) ) + 1 ) )
19 2 6 18 rspcedvd 
 |-  ( ( N e. NN0 /\ ( ( N - 1 ) / 2 ) e. NN0 ) -> E. m e. NN0 N = ( ( 2 x. m ) + 1 ) )
20 1 19 syldan 
 |-  ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> E. m e. NN0 N = ( ( 2 x. m ) + 1 ) )