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

Metamath Proof Explorer

Theorem dfeven4

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

Ref Expression
Assertion dfeven4 
|- Even = { z e. ZZ | E. i e. ZZ z = ( 2 x. i ) }

Proof

Step Hyp Ref Expression
1 df-even 
 |-  Even = { z e. ZZ | ( z / 2 ) e. ZZ }
2 simpr 
 |-  ( ( z e. ZZ /\ ( z / 2 ) e. ZZ ) -> ( z / 2 ) e. ZZ )
3 oveq2 
 |-  ( i = ( z / 2 ) -> ( 2 x. i ) = ( 2 x. ( z / 2 ) ) )
4 3 eqeq2d 
 |-  ( i = ( z / 2 ) -> ( z = ( 2 x. i ) <-> z = ( 2 x. ( z / 2 ) ) ) )
5 4 adantl 
 |-  ( ( ( z e. ZZ /\ ( z / 2 ) e. ZZ ) /\ i = ( z / 2 ) ) -> ( z = ( 2 x. i ) <-> z = ( 2 x. ( z / 2 ) ) ) )
6 zcn 
 |-  ( z e. ZZ -> z e. CC )
7 6 adantr 
 |-  ( ( z e. ZZ /\ ( z / 2 ) e. ZZ ) -> z e. CC )
8 2cnd 
 |-  ( ( z e. ZZ /\ ( z / 2 ) e. ZZ ) -> 2 e. CC )
9 2ne0 
 |-  2 =/= 0
10 9 a1i 
 |-  ( ( z e. ZZ /\ ( z / 2 ) e. ZZ ) -> 2 =/= 0 )
11 7 8 10 divcan2d 
 |-  ( ( z e. ZZ /\ ( z / 2 ) e. ZZ ) -> ( 2 x. ( z / 2 ) ) = z )
12 11 eqcomd 
 |-  ( ( z e. ZZ /\ ( z / 2 ) e. ZZ ) -> z = ( 2 x. ( z / 2 ) ) )
13 2 5 12 rspcedvd 
 |-  ( ( z e. ZZ /\ ( z / 2 ) e. ZZ ) -> E. i e. ZZ z = ( 2 x. i ) )
14 13 ex 
 |-  ( z e. ZZ -> ( ( z / 2 ) e. ZZ -> E. i e. ZZ z = ( 2 x. i ) ) )
15 oveq1 
 |-  ( z = ( 2 x. i ) -> ( z / 2 ) = ( ( 2 x. i ) / 2 ) )
16 zcn 
 |-  ( i e. ZZ -> i e. CC )
17 16 adantl 
 |-  ( ( z e. ZZ /\ i e. ZZ ) -> i e. CC )
18 2cnd 
 |-  ( ( z e. ZZ /\ i e. ZZ ) -> 2 e. CC )
19 9 a1i 
 |-  ( ( z e. ZZ /\ i e. ZZ ) -> 2 =/= 0 )
20 17 18 19 divcan3d 
 |-  ( ( z e. ZZ /\ i e. ZZ ) -> ( ( 2 x. i ) / 2 ) = i )
21 15 20 sylan9eqr 
 |-  ( ( ( z e. ZZ /\ i e. ZZ ) /\ z = ( 2 x. i ) ) -> ( z / 2 ) = i )
22 simpr 
 |-  ( ( z e. ZZ /\ i e. ZZ ) -> i e. ZZ )
23 22 adantr 
 |-  ( ( ( z e. ZZ /\ i e. ZZ ) /\ z = ( 2 x. i ) ) -> i e. ZZ )
24 21 23 eqeltrd 
 |-  ( ( ( z e. ZZ /\ i e. ZZ ) /\ z = ( 2 x. i ) ) -> ( z / 2 ) e. ZZ )
25 24 rexlimdva2 
 |-  ( z e. ZZ -> ( E. i e. ZZ z = ( 2 x. i ) -> ( z / 2 ) e. ZZ ) )
26 14 25 impbid 
 |-  ( z e. ZZ -> ( ( z / 2 ) e. ZZ <-> E. i e. ZZ z = ( 2 x. i ) ) )
27 26 rabbiia 
 |-  { z e. ZZ | ( z / 2 ) e. ZZ } = { z e. ZZ | E. i e. ZZ z = ( 2 x. i ) }
28 1 27 eqtri 
 |-  Even = { z e. ZZ | E. i e. ZZ z = ( 2 x. i ) }