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

Metamath Proof Explorer

Theorem divmul24

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

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

Proof

Step Hyp Ref Expression
1 mulcom 
 |-  ( ( C e. CC /\ D e. CC ) -> ( C x. D ) = ( D x. C ) )
2 1 ad2ant2r 
 |-  ( ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( C x. D ) = ( D x. C ) )
3 2 adantl 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( C x. D ) = ( D x. C ) )
4 3 oveq2d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A x. B ) / ( C x. D ) ) = ( ( A x. B ) / ( D x. C ) ) )
5 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 ) ) )
6 divmuldiv 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( D e. CC /\ D =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) ) -> ( ( A / D ) x. ( B / C ) ) = ( ( A x. B ) / ( D x. C ) ) )
7 6 ancom2s 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A / D ) x. ( B / C ) ) = ( ( A x. B ) / ( D x. C ) ) )
8 4 5 7 3eqtr4d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A / C ) x. ( B / D ) ) = ( ( A / D ) x. ( B / C ) ) )