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 ) }