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

Metamath Proof Explorer

Theorem 4div2e2

Description: One half of four is two. (Contributed by NM, 3-Sep-1999)

		Ref	Expression
	Assertion	4div2e2	$⊢ \frac{4}{2} = 2$

Step	Hyp	Ref	Expression
1		2t2e4	$⊢ 2 \cdot 2 = 4$
2		4cn	$⊢ 4 \in ℂ$
3		2cn	$⊢ 2 \in ℂ$
4		2ne0	$⊢ 2 \neq 0$
5	2 3 3 4	divmuli	$⊢ \frac{4}{2} = 2 \leftrightarrow 2 \cdot 2 = 4$
6	1 5	mpbir	$⊢ \frac{4}{2} = 2$