This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )