Theorem dfeven3

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

	Ref	Expression
Assertion	dfeven3	$$⊢\mathrm{Even}=\left\{z\in \mathbb{Z}|z\mathrm{mod}2=0\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-even	$$⊢\mathrm{Even}=\left\{z\in \mathbb{Z}|\frac{z}{2}\in \mathbb{Z}\right\}$$
2		zre	$$⊢z\in \mathbb{Z}\to z\in ℝ$$
3		2rp	$$⊢2\in {ℝ}^{+}$$
4		mod0	$$⊢\left(z\in ℝ\wedge 2\in {ℝ}^{+}\right)\to \left(z\mathrm{mod}2=0\leftrightarrow \frac{z}{2}\in \mathbb{Z}\right)$$
5	2 3 4	sylancl	$$⊢z\in \mathbb{Z}\to \left(z\mathrm{mod}2=0\leftrightarrow \frac{z}{2}\in \mathbb{Z}\right)$$
6	5	bicomd	$$⊢z\in \mathbb{Z}\to \left(\frac{z}{2}\in \mathbb{Z}\leftrightarrow z\mathrm{mod}2=0\right)$$
7	6	rabbiia	$$⊢\left\{z\in \mathbb{Z}|\frac{z}{2}\in \mathbb{Z}\right\}=\left\{z\in \mathbb{Z}|z\mathrm{mod}2=0\right\}$$
8	1 7	eqtri	$$⊢\mathrm{Even}=\left\{z\in \mathbb{Z}|z\mathrm{mod}2=0\right\}$$