Metamath Proof Explorer

Theorem even2n

Description: An integer is even iff it is twice another integer. (Contributed by AV, 25-Jun-2020)

Ref Expression
Assertion even2n 
|- ( 2 || N <-> E. n e. ZZ ( 2 x. n ) = N )

Proof

Step Hyp Ref Expression
1 evenelz 
 |-  ( 2 || N -> N e. ZZ )
2 2z 
 |-  2 e. ZZ
3 2 a1i 
 |-  ( n e. ZZ -> 2 e. ZZ )
4 id 
 |-  ( n e. ZZ -> n e. ZZ )
5 3 4 zmulcld 
 |-  ( n e. ZZ -> ( 2 x. n ) e. ZZ )
6 5 adantr 
 |-  ( ( n e. ZZ /\ ( 2 x. n ) = N ) -> ( 2 x. n ) e. ZZ )
7 eleq1 
 |-  ( ( 2 x. n ) = N -> ( ( 2 x. n ) e. ZZ <-> N e. ZZ ) )
8 7 adantl 
 |-  ( ( n e. ZZ /\ ( 2 x. n ) = N ) -> ( ( 2 x. n ) e. ZZ <-> N e. ZZ ) )
9 6 8 mpbid 
 |-  ( ( n e. ZZ /\ ( 2 x. n ) = N ) -> N e. ZZ )
10 9 rexlimiva 
 |-  ( E. n e. ZZ ( 2 x. n ) = N -> N e. ZZ )
11 divides 
 |-  ( ( 2 e. ZZ /\ N e. ZZ ) -> ( 2 || N <-> E. n e. ZZ ( n x. 2 ) = N ) )
12 zcn 
 |-  ( n e. ZZ -> n e. CC )
13 2cnd 
 |-  ( n e. ZZ -> 2 e. CC )
14 12 13 mulcomd 
 |-  ( n e. ZZ -> ( n x. 2 ) = ( 2 x. n ) )
15 14 eqeq1d 
 |-  ( n e. ZZ -> ( ( n x. 2 ) = N <-> ( 2 x. n ) = N ) )
16 15 rexbiia 
 |-  ( E. n e. ZZ ( n x. 2 ) = N <-> E. n e. ZZ ( 2 x. n ) = N )
17 11 16 bitrdi 
 |-  ( ( 2 e. ZZ /\ N e. ZZ ) -> ( 2 || N <-> E. n e. ZZ ( 2 x. n ) = N ) )
18 2 17 mpan 
 |-  ( N e. ZZ -> ( 2 || N <-> E. n e. ZZ ( 2 x. n ) = N ) )
19 1 10 18 pm5.21nii 
 |-  ( 2 || N <-> E. n e. ZZ ( 2 x. n ) = N )