Theorem 6even

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

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

Proof

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