Metamath Proof Explorer


Theorem nnennex

Description: For each even positive integer there is a positive integer which, multiplied by 2, results in the even positive integer. (Contributed by AV, 5-Jun-2023)

Ref Expression
Assertion nnennex
|- ( ( N e. NN /\ ( N / 2 ) e. NN ) -> E. m e. NN N = ( 2 x. m ) )

Proof

Step Hyp Ref Expression
1 simpr
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN ) -> ( N / 2 ) e. NN )
2 oveq2
 |-  ( m = ( N / 2 ) -> ( 2 x. m ) = ( 2 x. ( N / 2 ) ) )
3 2 eqeq2d
 |-  ( m = ( N / 2 ) -> ( N = ( 2 x. m ) <-> N = ( 2 x. ( N / 2 ) ) ) )
4 3 adantl
 |-  ( ( ( N e. NN /\ ( N / 2 ) e. NN ) /\ m = ( N / 2 ) ) -> ( N = ( 2 x. m ) <-> N = ( 2 x. ( N / 2 ) ) ) )
5 nncn
 |-  ( N e. NN -> N e. CC )
6 2cnd
 |-  ( N e. NN -> 2 e. CC )
7 2ne0
 |-  2 =/= 0
8 7 a1i
 |-  ( N e. NN -> 2 =/= 0 )
9 divcan2
 |-  ( ( N e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( 2 x. ( N / 2 ) ) = N )
10 9 eqcomd
 |-  ( ( N e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> N = ( 2 x. ( N / 2 ) ) )
11 5 6 8 10 syl3anc
 |-  ( N e. NN -> N = ( 2 x. ( N / 2 ) ) )
12 11 adantr
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN ) -> N = ( 2 x. ( N / 2 ) ) )
13 1 4 12 rspcedvd
 |-  ( ( N e. NN /\ ( N / 2 ) e. NN ) -> E. m e. NN N = ( 2 x. m ) )