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

Metamath Proof Explorer

Theorem dfeven2

Description: Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020)

Ref Expression
Assertion dfeven2 
|- Even = { z e. ZZ | 2 || z }

Proof

Step Hyp Ref Expression
1 dfeven4 
 |-  Even = { z e. ZZ | E. i e. ZZ z = ( 2 x. i ) }
2 eqcom 
 |-  ( z = ( 2 x. i ) <-> ( 2 x. i ) = z )
3 2cnd 
 |-  ( ( z e. ZZ /\ i e. ZZ ) -> 2 e. CC )
4 zcn 
 |-  ( i e. ZZ -> i e. CC )
5 4 adantl 
 |-  ( ( z e. ZZ /\ i e. ZZ ) -> i e. CC )
6 3 5 mulcomd 
 |-  ( ( z e. ZZ /\ i e. ZZ ) -> ( 2 x. i ) = ( i x. 2 ) )
7 6 eqeq1d 
 |-  ( ( z e. ZZ /\ i e. ZZ ) -> ( ( 2 x. i ) = z <-> ( i x. 2 ) = z ) )
8 2 7 bitrid 
 |-  ( ( z e. ZZ /\ i e. ZZ ) -> ( z = ( 2 x. i ) <-> ( i x. 2 ) = z ) )
9 8 rexbidva 
 |-  ( z e. ZZ -> ( E. i e. ZZ z = ( 2 x. i ) <-> E. i e. ZZ ( i x. 2 ) = z ) )
10 2z 
 |-  2 e. ZZ
11 divides 
 |-  ( ( 2 e. ZZ /\ z e. ZZ ) -> ( 2 || z <-> E. i e. ZZ ( i x. 2 ) = z ) )
12 10 11 mpan 
 |-  ( z e. ZZ -> ( 2 || z <-> E. i e. ZZ ( i x. 2 ) = z ) )
13 9 12 bitr4d 
 |-  ( z e. ZZ -> ( E. i e. ZZ z = ( 2 x. i ) <-> 2 || z ) )
14 13 rabbiia 
 |-  { z e. ZZ | E. i e. ZZ z = ( 2 x. i ) } = { z e. ZZ | 2 || z }
15 1 14 eqtri 
 |-  Even = { z e. ZZ | 2 || z }