Theorem dfeven3

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

	Ref	Expression
Assertion	dfeven3	|- Even = { z e. ZZ | ( z mod 2 ) = 0 }

Proof

Step	Hyp	Ref	Expression
1		df-even	|- Even = { z e. ZZ | ( z / 2 ) e. ZZ }
2		zre	|- ( z e. ZZ -> z e. RR )
3		2rp	|- 2 e. RR+
4		mod0	|- ( ( z e. RR /\ 2 e. RR+ ) -> ( ( z mod 2 ) = 0 <-> ( z / 2 ) e. ZZ ) )
5	2 3 4	sylancl	|- ( z e. ZZ -> ( ( z mod 2 ) = 0 <-> ( z / 2 ) e. ZZ ) )
6	5	bicomd	|- ( z e. ZZ -> ( ( z / 2 ) e. ZZ <-> ( z mod 2 ) = 0 ) )
7	6	rabbiia	|- { z e. ZZ | ( z / 2 ) e. ZZ } = { z e. ZZ | ( z mod 2 ) = 0 }
8	1 7	eqtri	|- Even = { z e. ZZ | ( z mod 2 ) = 0 }