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 x. 2 ) = 4
2		4cn	|- 4 e. CC
3		2cn	|- 2 e. CC
4		2ne0	|- 2 =/= 0
5	2 3 3 4	divmuli	|- ( ( 4 / 2 ) = 2 <-> ( 2 x. 2 ) = 4 )
6	1 5	mpbir	|- ( 4 / 2 ) = 2