Metamath Proof Explorer

Theorem divmulasscom

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

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

Proof

Step Hyp Ref Expression
1 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 ) ) )
2 mulcom 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
3 2 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. B ) = ( B x. A ) )
4 3 adantr 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( A x. B ) = ( B x. A ) )
5 4 oveq1d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( ( A x. B ) x. ( C / D ) ) = ( ( B x. A ) x. ( C / D ) ) )
6 simpl2 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ D =/= 0 ) ) -> B e. CC )
7 simpl1 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ D =/= 0 ) ) -> A e. CC )
8 simp3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> C e. CC )
9 8 anim1i 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( C e. CC /\ ( D e. CC /\ D =/= 0 ) ) )
10 3anass 
 |-  ( ( C e. CC /\ D e. CC /\ D =/= 0 ) <-> ( C e. CC /\ ( D e. CC /\ D =/= 0 ) ) )
11 9 10 sylibr 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( C e. CC /\ D e. CC /\ D =/= 0 ) )
12 divcl 
 |-  ( ( C e. CC /\ D e. CC /\ D =/= 0 ) -> ( C / D ) e. CC )
13 11 12 syl 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( C / D ) e. CC )
14 6 7 13 mulassd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( ( B x. A ) x. ( C / D ) ) = ( B x. ( A x. ( C / D ) ) ) )
15 8 adantr 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ D =/= 0 ) ) -> C e. CC )
16 simpr 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( D e. CC /\ D =/= 0 ) )
17 divass 
 |-  ( ( A e. CC /\ C e. CC /\ ( D e. CC /\ D =/= 0 ) ) -> ( ( A x. C ) / D ) = ( A x. ( C / D ) ) )
18 7 15 16 17 syl3anc 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( ( A x. C ) / D ) = ( A x. ( C / D ) ) )
19 18 eqcomd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( A x. ( C / D ) ) = ( ( A x. C ) / D ) )
20 19 oveq2d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( B x. ( A x. ( C / D ) ) ) = ( B x. ( ( A x. C ) / D ) ) )
21 14 20 eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( ( B x. A ) x. ( C / D ) ) = ( B x. ( ( A x. C ) / D ) ) )
22 1 5 21 3eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( ( A x. ( B / D ) ) x. C ) = ( B x. ( ( A x. C ) / D ) ) )