Theorem 8even

Description: 8 is an even number. (Contributed by AV, 23-Jul-2020)

	Ref	Expression
Assertion	8even	$$⊢8\in \mathrm{Even}$$

Proof

Step	Hyp	Ref	Expression
1		8nn	$$⊢8\in \mathbb{N}$$
2	1	nnzi	$$⊢8\in \mathbb{Z}$$
3		4t2e8	$$⊢4\cdot 2=8$$
4	3	eqcomi	$$⊢8=4\cdot 2$$
5	4	oveq1i	$$⊢\frac{8}{2}=\frac{4\cdot 2}{2}$$
6		4cn	$$⊢4\in ℂ$$
7		2cn	$$⊢2\in ℂ$$
8		2ne0	$$⊢2\ne 0$$
9	6 7 8	divcan4i	$$⊢\frac{4\cdot 2}{2}=4$$
10	5 9	eqtri	$$⊢\frac{8}{2}=4$$
11		4z	$$⊢4\in \mathbb{Z}$$
12	10 11	eqeltri	$$⊢\frac{8}{2}\in \mathbb{Z}$$
13		iseven	$$⊢8\in \mathrm{Even}\leftrightarrow \left(8\in \mathbb{Z}\wedge \frac{8}{2}\in \mathbb{Z}\right)$$
14	2 12 13	mpbir2an	$$⊢8\in \mathrm{Even}$$