This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nnennexALTV

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 nnennexALTV 
|- ( ( N e. NN /\ N e. Even ) -> E. m e. NN N = ( 2 x. m ) )

Proof

Step Hyp Ref Expression
1 nneven 
 |-  ( ( N e. NN /\ N e. Even ) -> ( 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 e. Even ) /\ 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 e. Even ) -> N = ( 2 x. ( N / 2 ) ) )
13 1 4 12 rspcedvd 
 |-  ( ( N e. NN /\ N e. Even ) -> E. m e. NN N = ( 2 x. m ) )