Theorem z4even

Description: 2 divides 4. That means 4 is even. (Contributed by AV, 23-Jul-2020) (Revised by AV, 4-Jul-2021)

	Ref	Expression
Assertion	z4even	$$⊢2\parallel 4$$

Proof

Step	Hyp	Ref	Expression
1		2z	$$⊢2\in \mathbb{Z}$$
2		dvdsmul1	$$⊢\left(2\in \mathbb{Z}\wedge 2\in \mathbb{Z}\right)\to 2\parallel 2\cdot 2$$
3	1 1 2	mp2an	$$⊢2\parallel 2\cdot 2$$
4		2t2e4	$$⊢2\cdot 2=4$$
5	3 4	breqtri	$$⊢2\parallel 4$$