Metamath Proof Explorer


Theorem dfeven4

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

Ref Expression
Assertion dfeven4 Even=z|iz=2i

Proof

Step Hyp Ref Expression
1 df-even Even=z|z2
2 simpr zz2z2
3 oveq2 i=z22i=2z2
4 3 eqeq2d i=z2z=2iz=2z2
5 4 adantl zz2i=z2z=2iz=2z2
6 zcn zz
7 6 adantr zz2z
8 2cnd zz22
9 2ne0 20
10 9 a1i zz220
11 7 8 10 divcan2d zz22z2=z
12 11 eqcomd zz2z=2z2
13 2 5 12 rspcedvd zz2iz=2i
14 13 ex zz2iz=2i
15 oveq1 z=2iz2=2i2
16 zcn ii
17 16 adantl zii
18 2cnd zi2
19 9 a1i zi20
20 17 18 19 divcan3d zi2i2=i
21 15 20 sylan9eqr ziz=2iz2=i
22 simpr zii
23 22 adantr ziz=2ii
24 21 23 eqeltrd ziz=2iz2
25 24 rexlimdva2 ziz=2iz2
26 14 25 impbid zz2iz=2i
27 26 rabbiia z|z2=z|iz=2i
28 1 27 eqtri Even=z|iz=2i