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 ) )