Theorem 4d2e2

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

	Ref	Expression
Assertion	4d2e2	⊢ ( 4 / 2 ) = 2

Proof

Step	Hyp	Ref	Expression
1		2t2e4	⊢ ( 2 · 2 ) = 4
2		4cn	⊢ 4 ∈ ℂ
3		2cn	⊢ 2 ∈ ℂ
4		2ne0	⊢ 2 ≠ 0
5	2 3 3 4	divmuli	⊢ ( ( 4 / 2 ) = 2 ↔ ( 2 · 2 ) = 4 )
6	1 5	mpbir	⊢ ( 4 / 2 ) = 2