Metamath Proof Explorer


Theorem dfeven2

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

Ref Expression
Assertion dfeven2 Even=z|2z

Proof

Step Hyp Ref Expression
1 dfeven4 Even=z|iz=2i
2 eqcom z=2i2i=z
3 2cnd zi2
4 zcn ii
5 4 adantl zii
6 3 5 mulcomd zi2i=i2
7 6 eqeq1d zi2i=zi2=z
8 2 7 syl5bb ziz=2ii2=z
9 8 rexbidva ziz=2iii2=z
10 2z 2
11 divides 2z2zii2=z
12 10 11 mpan z2zii2=z
13 9 12 bitr4d ziz=2i2z
14 13 rabbiia z|iz=2i=z|2z
15 1 14 eqtri Even=z|2z