This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∥ 4$

Step	Hyp	Ref	Expression
1		2z	$⊢ 2 \in ℤ$
2		dvdsmul1	$⊢ (2 \in ℤ \land 2 \in ℤ) \to 2 ∥ 2 \cdot 2$
3	1 1 2	mp2an	$⊢ 2 ∥ 2 \cdot 2$
4		2t2e4	$⊢ 2 \cdot 2 = 4$
5	3 4	breqtri	$⊢ 2 ∥ 4$