Metamath Proof Explorer

Theorem divmulass

Description: An associative law for division and multiplication. (Contributed by AV, 10-Jul-2021)

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

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ D =/= 0 ) ) -> A e. CC )
2 simpl2 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ D =/= 0 ) ) -> B e. CC )
3 simpr 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( D e. CC /\ D =/= 0 ) )
4 divass 
 |-  ( ( A e. CC /\ B e. CC /\ ( D e. CC /\ D =/= 0 ) ) -> ( ( A x. B ) / D ) = ( A x. ( B / D ) ) )
5 1 2 3 4 syl3anc 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( ( A x. B ) / D ) = ( A x. ( B / D ) ) )
6 5 eqcomd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( A x. ( B / D ) ) = ( ( A x. B ) / D ) )
7 6 oveq1d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( ( A x. ( B / D ) ) x. C ) = ( ( ( A x. B ) / D ) x. C ) )
8 mulcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
9 8 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. B ) e. CC )
10 9 adantr 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( A x. B ) e. CC )
11 simpl3 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ D =/= 0 ) ) -> C e. CC )
12 div32 
 |-  ( ( ( A x. B ) e. CC /\ ( D e. CC /\ D =/= 0 ) /\ C e. CC ) -> ( ( ( A x. B ) / D ) x. C ) = ( ( A x. B ) x. ( C / D ) ) )
13 10 3 11 12 syl3anc 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( ( ( A x. B ) / D ) x. C ) = ( ( A x. B ) x. ( C / D ) ) )
14 7 13 eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( ( A x. ( B / D ) ) x. C ) = ( ( A x. B ) x. ( C / D ) ) )