Theorem dmmcand

Description: Cancellation law for division and multiplication. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	dmmcand.a	|- ( ph -> A e. CC )
	dmmcand.b	|- ( ph -> B e. CC )
	dmmcand.c	|- ( ph -> C e. CC )
	dmmcand.bn0	|- ( ph -> B =/= 0 )
Assertion	dmmcand	|- ( ph -> ( ( A / B ) x. ( B x. C ) ) = ( A x. C ) )

Proof

Step	Hyp	Ref	Expression
1		dmmcand.a	|- ( ph -> A e. CC )
2		dmmcand.b	|- ( ph -> B e. CC )
3		dmmcand.c	|- ( ph -> C e. CC )
4		dmmcand.bn0	|- ( ph -> B =/= 0 )
5	2 3	mulcld	|- ( ph -> ( B x. C ) e. CC )
6	1 2 5 4	div32d	|- ( ph -> ( ( A / B ) x. ( B x. C ) ) = ( A x. ( ( B x. C ) / B ) ) )
7	3 2 4	divcan3d	|- ( ph -> ( ( B x. C ) / B ) = C )
8	7	oveq2d	|- ( ph -> ( A x. ( ( B x. C ) / B ) ) = ( A x. C ) )
9		eqidd	|- ( ph -> ( A x. C ) = ( A x. C ) )
10	6 8 9	3eqtrd	|- ( ph -> ( ( A / B ) x. ( B x. C ) ) = ( A x. C ) )