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 }