Metamath Proof Explorer

Theorem divmuldiv

Description: Multiplication of two ratios. Theorem I.14 of Apostol p. 18. (Contributed by NM, 1-Aug-2004)

Ref Expression
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 3anass 
 |-  ( ( A e. CC /\ C e. CC /\ C =/= 0 ) <-> ( A e. CC /\ ( C e. CC /\ C =/= 0 ) ) )
2 3anass 
 |-  ( ( B e. CC /\ D e. CC /\ D =/= 0 ) <-> ( B e. CC /\ ( D e. CC /\ D =/= 0 ) ) )
3 divcl 
 |-  ( ( A e. CC /\ C e. CC /\ C =/= 0 ) -> ( A / C ) e. CC )
4 divcl 
 |-  ( ( B e. CC /\ D e. CC /\ D =/= 0 ) -> ( B / D ) e. CC )
5 mulcl 
 |-  ( ( ( A / C ) e. CC /\ ( B / D ) e. CC ) -> ( ( A / C ) x. ( B / D ) ) e. CC )
6 3 4 5 syl2an 
 |-  ( ( ( A e. CC /\ C e. CC /\ C =/= 0 ) /\ ( B e. CC /\ D e. CC /\ D =/= 0 ) ) -> ( ( A / C ) x. ( 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 8 3adantr1 
 |-  ( ( ( C e. CC /\ C =/= 0 ) /\ ( B e. CC /\ D e. CC /\ D =/= 0 ) ) -> ( C x. D ) e. CC )
10 9 3adantl1 
 |-  ( ( ( A e. CC /\ C e. CC /\ C =/= 0 ) /\ ( B e. CC /\ D e. CC /\ D =/= 0 ) ) -> ( C x. D ) e. CC )
11 mulne0 
 |-  ( ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( C x. D ) =/= 0 )
12 11 3adantr1 
 |-  ( ( ( C e. CC /\ C =/= 0 ) /\ ( B e. CC /\ D e. CC /\ D =/= 0 ) ) -> ( C x. D ) =/= 0 )
13 12 3adantl1 
 |-  ( ( ( A e. CC /\ C e. CC /\ C =/= 0 ) /\ ( B e. CC /\ D e. CC /\ D =/= 0 ) ) -> ( C x. D ) =/= 0 )
14 divcan3 
 |-  ( ( ( ( A / C ) x. ( B / D ) ) e. CC /\ ( C x. D ) e. CC /\ ( C x. D ) =/= 0 ) -> ( ( ( C x. D ) x. ( ( A / C ) x. ( B / D ) ) ) / ( C x. D ) ) = ( ( A / C ) x. ( B / D ) ) )
15 6 10 13 14 syl3anc 
 |-  ( ( ( A e. CC /\ C e. CC /\ C =/= 0 ) /\ ( B e. CC /\ D e. CC /\ D =/= 0 ) ) -> ( ( ( C x. D ) x. ( ( A / C ) x. ( B / D ) ) ) / ( C x. D ) ) = ( ( A / C ) x. ( B / D ) ) )
16 simp2 
 |-  ( ( A e. CC /\ C e. CC /\ C =/= 0 ) -> C e. CC )
17 16 3 jca 
 |-  ( ( A e. CC /\ C e. CC /\ C =/= 0 ) -> ( C e. CC /\ ( A / C ) e. CC ) )
18 simp2 
 |-  ( ( B e. CC /\ D e. CC /\ D =/= 0 ) -> D e. CC )
19 18 4 jca 
 |-  ( ( B e. CC /\ D e. CC /\ D =/= 0 ) -> ( D e. CC /\ ( B / D ) e. CC ) )
20 mul4 
 |-  ( ( ( C e. CC /\ ( A / C ) e. CC ) /\ ( D e. CC /\ ( B / D ) e. CC ) ) -> ( ( C x. ( A / C ) ) x. ( D x. ( B / D ) ) ) = ( ( C x. D ) x. ( ( A / C ) x. ( B / D ) ) ) )
21 17 19 20 syl2an 
 |-  ( ( ( A e. CC /\ C e. CC /\ C =/= 0 ) /\ ( B e. CC /\ D e. CC /\ D =/= 0 ) ) -> ( ( C x. ( A / C ) ) x. ( D x. ( B / D ) ) ) = ( ( C x. D ) x. ( ( A / C ) x. ( B / D ) ) ) )
22 divcan2 
 |-  ( ( A e. CC /\ C e. CC /\ C =/= 0 ) -> ( C x. ( A / C ) ) = A )
23 divcan2 
 |-  ( ( B e. CC /\ D e. CC /\ D =/= 0 ) -> ( D x. ( B / D ) ) = B )
24 22 23 oveqan12d 
 |-  ( ( ( A e. CC /\ C e. CC /\ C =/= 0 ) /\ ( B e. CC /\ D e. CC /\ D =/= 0 ) ) -> ( ( C x. ( A / C ) ) x. ( D x. ( B / D ) ) ) = ( A x. B ) )
25 21 24 eqtr3d 
 |-  ( ( ( A e. CC /\ C e. CC /\ C =/= 0 ) /\ ( B e. CC /\ D e. CC /\ D =/= 0 ) ) -> ( ( C x. D ) x. ( ( A / C ) x. ( B / D ) ) ) = ( A x. B ) )
26 25 oveq1d 
 |-  ( ( ( A e. CC /\ C e. CC /\ C =/= 0 ) /\ ( B e. CC /\ D e. CC /\ D =/= 0 ) ) -> ( ( ( C x. D ) x. ( ( A / C ) x. ( B / D ) ) ) / ( C x. D ) ) = ( ( A x. B ) / ( C x. D ) ) )
27 15 26 eqtr3d 
 |-  ( ( ( A e. CC /\ C e. CC /\ C =/= 0 ) /\ ( B e. CC /\ D e. CC /\ D =/= 0 ) ) -> ( ( A / C ) x. ( B / D ) ) = ( ( A x. B ) / ( C x. D ) ) )
28 1 2 27 syl2anbr 
 |-  ( ( ( A e. CC /\ ( C e. CC /\ C =/= 0 ) ) /\ ( B e. CC /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A / C ) x. ( B / D ) ) = ( ( A x. B ) / ( C x. D ) ) )
29 28 an4s 
 |-  ( ( ( 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 ) ) )