Theorem divcan4

Description: A cancellation law for division. (Contributed by NM, 8-Feb-2005)

	Ref	Expression
Assertion	divcan4	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A x. B ) / B ) = A )

Proof

Step	Hyp	Ref	Expression
1		mulcom	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
2	1	3adant3	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A x. B ) = ( B x. A ) )
3	2	oveq1d	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A x. B ) / B ) = ( ( B x. A ) / B ) )
4		divcan3	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( B x. A ) / B ) = A )
5	3 4	eqtrd	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A x. B ) / B ) = A )