Metamath Proof Explorer

Theorem nn0enn0ex

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

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

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( N e. NN0 /\ ( N / 2 ) e. NN0 ) -> ( N / 2 ) e. NN0 )
2 oveq2 
 |-  ( m = ( N / 2 ) -> ( 2 x. m ) = ( 2 x. ( N / 2 ) ) )
3 2 adantl 
 |-  ( ( ( N e. NN0 /\ ( N / 2 ) e. NN0 ) /\ m = ( N / 2 ) ) -> ( 2 x. m ) = ( 2 x. ( N / 2 ) ) )
4 3 eqeq2d 
 |-  ( ( ( N e. NN0 /\ ( N / 2 ) e. NN0 ) /\ m = ( N / 2 ) ) -> ( N = ( 2 x. m ) <-> N = ( 2 x. ( N / 2 ) ) ) )
5 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
6 2cnd 
 |-  ( N e. NN0 -> 2 e. CC )
7 2ne0 
 |-  2 =/= 0
8 7 a1i 
 |-  ( N e. NN0 -> 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. NN0 -> N = ( 2 x. ( N / 2 ) ) )
12 11 adantr 
 |-  ( ( N e. NN0 /\ ( N / 2 ) e. NN0 ) -> N = ( 2 x. ( N / 2 ) ) )
13 1 4 12 rspcedvd 
 |-  ( ( N e. NN0 /\ ( N / 2 ) e. NN0 ) -> E. m e. NN0 N = ( 2 x. m ) )