Metamath Proof Explorer


Theorem dfeven3

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

Ref Expression
Assertion dfeven3 Even = z | z mod 2 = 0

Proof

Step Hyp Ref Expression
1 df-even Even = z | z 2
2 zre z z
3 2rp 2 +
4 mod0 z 2 + z mod 2 = 0 z 2
5 2 3 4 sylancl z z mod 2 = 0 z 2
6 5 bicomd z z 2 z mod 2 = 0
7 6 rabbiia z | z 2 = z | z mod 2 = 0
8 1 7 eqtri Even = z | z mod 2 = 0