Theorem 0evenALTV

Description: 0 is an even number. (Contributed by AV, 11-Feb-2020) (Revised by AV, 17-Jun-2020)

	Ref	Expression
Assertion	0evenALTV	$$⊢0\in \mathrm{Even}$$

Proof

Step	Hyp	Ref	Expression
1		0z	$$⊢0\in \mathbb{Z}$$
2		2cn	$$⊢2\in ℂ$$
3		2ne0	$$⊢2\ne 0$$
4	2 3	div0i	$$⊢\frac{0}{2}=0$$
5	4 1	eqeltri	$$⊢\frac{0}{2}\in \mathbb{Z}$$
6		iseven	$$⊢0\in \mathrm{Even}\leftrightarrow \left(0\in \mathbb{Z}\wedge \frac{0}{2}\in \mathbb{Z}\right)$$
7	1 5 6	mpbir2an	$$⊢0\in \mathrm{Even}$$