Theorem 4div2e2

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

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

Proof

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