Metamath Proof Explorer

Theorem divmuleq

Description: Cross-multiply in an equality of ratios. (Contributed by Mario Carneiro, 23-Feb-2014)

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

Proof

Step Hyp Ref Expression
1 divcl 
 |-  ( ( A e. CC /\ C e. CC /\ C =/= 0 ) -> ( A / C ) e. CC )
2 1 3expb 
 |-  ( ( A e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( A / C ) e. CC )
3 2 ad2ant2r 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( A / C ) e. CC )
4 divcl 
 |-  ( ( B e. CC /\ D e. CC /\ D =/= 0 ) -> ( B / D ) e. CC )
5 4 3expb 
 |-  ( ( B e. CC /\ ( D e. CC /\ D =/= 0 ) ) -> ( B / D ) e. CC )
6 5 ad2ant2l 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( B / D ) e. CC )
7 mulcl 
 |-  ( ( C e. CC /\ D e. CC ) -> ( C x. D ) e. CC )
8 7 ad2ant2r 
 |-  ( ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( C x. D ) e. CC )
9 mulne0 
 |-  ( ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( C x. D ) =/= 0 )
10 8 9 jca 
 |-  ( ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( ( C x. D ) e. CC /\ ( C x. D ) =/= 0 ) )
11 10 adantl 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( C x. D ) e. CC /\ ( C x. D ) =/= 0 ) )
12 mulcan2 
 |-  ( ( ( A / C ) e. CC /\ ( B / D ) e. CC /\ ( ( C x. D ) e. CC /\ ( C x. D ) =/= 0 ) ) -> ( ( ( A / C ) x. ( C x. D ) ) = ( ( B / D ) x. ( C x. D ) ) <-> ( A / C ) = ( B / D ) ) )
13 3 6 11 12 syl3anc 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( ( A / C ) x. ( C x. D ) ) = ( ( B / D ) x. ( C x. D ) ) <-> ( A / C ) = ( B / D ) ) )
14 simprll 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> C e. CC )
15 simprrl 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> D e. CC )
16 3 14 15 mulassd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( ( A / C ) x. C ) x. D ) = ( ( A / C ) x. ( C x. D ) ) )
17 divcan1 
 |-  ( ( A e. CC /\ C e. CC /\ C =/= 0 ) -> ( ( A / C ) x. C ) = A )
18 17 3expb 
 |-  ( ( A e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / C ) x. C ) = A )
19 18 ad2ant2r 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A / C ) x. C ) = A )
20 19 oveq1d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( ( A / C ) x. C ) x. D ) = ( A x. D ) )
21 16 20 eqtr3d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A / C ) x. ( C x. D ) ) = ( A x. D ) )
22 14 15 mulcomd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( C x. D ) = ( D x. C ) )
23 22 oveq2d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( B / D ) x. ( C x. D ) ) = ( ( B / D ) x. ( D x. C ) ) )
24 6 15 14 mulassd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( ( B / D ) x. D ) x. C ) = ( ( B / D ) x. ( D x. C ) ) )
25 divcan1 
 |-  ( ( B e. CC /\ D e. CC /\ D =/= 0 ) -> ( ( B / D ) x. D ) = B )
26 25 3expb 
 |-  ( ( B e. CC /\ ( D e. CC /\ D =/= 0 ) ) -> ( ( B / D ) x. D ) = B )
27 26 ad2ant2l 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( B / D ) x. D ) = B )
28 27 oveq1d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( ( B / D ) x. D ) x. C ) = ( B x. C ) )
29 23 24 28 3eqtr2d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( B / D ) x. ( C x. D ) ) = ( B x. C ) )
30 21 29 eqeq12d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( ( A / C ) x. ( C x. D ) ) = ( ( B / D ) x. ( C x. D ) ) <-> ( A x. D ) = ( B x. C ) ) )
31 13 30 bitr3d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A / C ) = ( B / D ) <-> ( A x. D ) = ( B x. C ) ) )