Metamath Proof Explorer

Theorem divmul13

Description: Swap the denominators in the product of two ratios. (Contributed by NM, 3-May-2005)

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

Proof

Step Hyp Ref Expression
1 mulcom 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
2 1 adantr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( A x. B ) = ( B x. A ) )
3 2 oveq1d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A x. B ) / ( C x. D ) ) = ( ( B x. A ) / ( C x. D ) ) )
4 divmuldiv 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A / C ) x. ( B / D ) ) = ( ( A x. B ) / ( C x. D ) ) )
5 divmuldiv 
 |-  ( ( ( B e. CC /\ A e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( B / C ) x. ( A / D ) ) = ( ( B x. A ) / ( C x. D ) ) )
6 5 ancom1s 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( B / C ) x. ( A / D ) ) = ( ( B x. A ) / ( C x. D ) ) )
7 3 4 6 3eqtr4d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A / C ) x. ( B / D ) ) = ( ( B / C ) x. ( A / D ) ) )