Metamath Proof Explorer

Theorem divdivdiv

Description: Division of two ratios. Theorem I.15 of Apostol p. 18. (Contributed by NM, 2-Aug-2004)

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

Proof

Step Hyp Ref Expression
1 simprrl 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> D e. CC )
2 simprll 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> C e. CC )
3 simprlr 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> C =/= 0 )
4 divcl 
 |-  ( ( D e. CC /\ C e. CC /\ C =/= 0 ) -> ( D / C ) e. CC )
5 1 2 3 4 syl3anc 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( D / C ) e. CC )
6 simpll 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> A e. CC )
7 simplrl 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> B e. CC )
8 simplrr 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> B =/= 0 )
9 divcl 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) e. CC )
10 6 7 8 9 syl3anc 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( A / B ) e. CC )
11 5 10 mulcomd 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( D / C ) x. ( A / B ) ) = ( ( A / B ) x. ( D / C ) ) )
12 simplr 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( B e. CC /\ B =/= 0 ) )
13 simprl 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( C e. CC /\ C =/= 0 ) )
14 divmuldiv 
 |-  ( ( ( A e. CC /\ D e. CC ) /\ ( ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) ) -> ( ( A / B ) x. ( D / C ) ) = ( ( A x. D ) / ( B x. C ) ) )
15 6 1 12 13 14 syl22anc 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A / B ) x. ( D / C ) ) = ( ( A x. D ) / ( B x. C ) ) )
16 11 15 eqtrd 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( D / C ) x. ( A / B ) ) = ( ( A x. D ) / ( B x. C ) ) )
17 16 oveq2d 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( C / D ) x. ( ( D / C ) x. ( A / B ) ) ) = ( ( C / D ) x. ( ( A x. D ) / ( B x. C ) ) ) )
18 simprr 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( D e. CC /\ D =/= 0 ) )
19 divmuldiv 
 |-  ( ( ( C e. CC /\ D e. CC ) /\ ( ( D e. CC /\ D =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) ) -> ( ( C / D ) x. ( D / C ) ) = ( ( C x. D ) / ( D x. C ) ) )
20 2 1 18 13 19 syl22anc 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( C / D ) x. ( D / C ) ) = ( ( C x. D ) / ( D x. C ) ) )
21 2 1 mulcomd 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( C x. D ) = ( D x. C ) )
22 21 oveq1d 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( C x. D ) / ( D x. C ) ) = ( ( D x. C ) / ( D x. C ) ) )
23 1 2 mulcld 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( D x. C ) e. CC )
24 simprrr 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> D =/= 0 )
25 1 2 24 3 mulne0d 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( D x. C ) =/= 0 )
26 divid 
 |-  ( ( ( D x. C ) e. CC /\ ( D x. C ) =/= 0 ) -> ( ( D x. C ) / ( D x. C ) ) = 1 )
27 23 25 26 syl2anc 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( D x. C ) / ( D x. C ) ) = 1 )
28 22 27 eqtrd 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( C x. D ) / ( D x. C ) ) = 1 )
29 20 28 eqtrd 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( C / D ) x. ( D / C ) ) = 1 )
30 29 oveq1d 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( ( C / D ) x. ( D / C ) ) x. ( A / B ) ) = ( 1 x. ( A / B ) ) )
31 divcl 
 |-  ( ( C e. CC /\ D e. CC /\ D =/= 0 ) -> ( C / D ) e. CC )
32 2 1 24 31 syl3anc 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( C / D ) e. CC )
33 32 5 10 mulassd 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( ( C / D ) x. ( D / C ) ) x. ( A / B ) ) = ( ( C / D ) x. ( ( D / C ) x. ( A / B ) ) ) )
34 10 mulid2d 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( 1 x. ( A / B ) ) = ( A / B ) )
35 30 33 34 3eqtr3d 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( C / D ) x. ( ( D / C ) x. ( A / B ) ) ) = ( A / B ) )
36 17 35 eqtr3d 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( C / D ) x. ( ( A x. D ) / ( B x. C ) ) ) = ( A / B ) )
37 6 1 mulcld 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( A x. D ) e. CC )
38 7 2 mulcld 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( B x. C ) e. CC )
39 mulne0 
 |-  ( ( ( B e. CC /\ B =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( B x. C ) =/= 0 )
40 39 ad2ant2lr 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( B x. C ) =/= 0 )
41 divcl 
 |-  ( ( ( A x. D ) e. CC /\ ( B x. C ) e. CC /\ ( B x. C ) =/= 0 ) -> ( ( A x. D ) / ( B x. C ) ) e. CC )
42 37 38 40 41 syl3anc 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A x. D ) / ( B x. C ) ) e. CC )
43 divne0 
 |-  ( ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( C / D ) =/= 0 )
44 43 adantl 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( C / D ) =/= 0 )
45 divmul 
 |-  ( ( ( A / B ) e. CC /\ ( ( A x. D ) / ( B x. C ) ) e. CC /\ ( ( C / D ) e. CC /\ ( C / D ) =/= 0 ) ) -> ( ( ( A / B ) / ( C / D ) ) = ( ( A x. D ) / ( B x. C ) ) <-> ( ( C / D ) x. ( ( A x. D ) / ( B x. C ) ) ) = ( A / B ) ) )
46 10 42 32 44 45 syl112anc 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( ( A / B ) / ( C / D ) ) = ( ( A x. D ) / ( B x. C ) ) <-> ( ( C / D ) x. ( ( A x. D ) / ( B x. C ) ) ) = ( A / B ) ) )
47 36 46 mpbird 
 |-  ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A / B ) / ( C / D ) ) = ( ( A x. D ) / ( B x. C ) ) )