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

Metamath Proof Explorer

Theorem divadddiv

Description: Addition of two ratios. Theorem I.13 of Apostol p. 18. (Contributed by NM, 1-Aug-2004) (Revised by Mario Carneiro, 2-May-2016)

Ref Expression
Assertion divadddiv 
|- ( ( ( 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 ) ) / ( C x. D ) ) )

Proof

Step Hyp Ref Expression
1 mulcl 
 |-  ( ( A e. CC /\ D e. CC ) -> ( A x. D ) e. CC )
2 1 ad2ant2r 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( A x. D ) e. CC )
3 2 adantrl 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( A x. D ) e. CC )
4 mulcl 
 |-  ( ( B e. CC /\ C e. CC ) -> ( B x. C ) e. CC )
5 4 adantrr 
 |-  ( ( B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( B x. C ) e. CC )
6 5 ad2ant2lr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( B x. C ) 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 divdir 
 |-  ( ( ( A x. D ) e. CC /\ ( B x. C ) e. CC /\ ( ( C x. D ) e. CC /\ ( C x. D ) =/= 0 ) ) -> ( ( ( A x. D ) + ( B x. C ) ) / ( C x. D ) ) = ( ( ( A x. D ) / ( C x. D ) ) + ( ( B x. C ) / ( C x. D ) ) ) )
13 3 6 11 12 syl3anc 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( ( A x. D ) + ( B x. C ) ) / ( C x. D ) ) = ( ( ( A x. D ) / ( C x. D ) ) + ( ( B x. C ) / ( C x. D ) ) ) )
14 simpll 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> A e. CC )
15 simprr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( D e. CC /\ D =/= 0 ) )
16 15 simpld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> D e. CC )
17 14 16 mulcomd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( A x. D ) = ( D x. A ) )
18 simprll 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> C e. CC )
19 18 16 mulcomd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( C x. D ) = ( D x. C ) )
20 17 19 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A x. D ) / ( C x. D ) ) = ( ( D x. A ) / ( D x. C ) ) )
21 simprl 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( C e. CC /\ C =/= 0 ) )
22 divcan5 
 |-  ( ( A e. CC /\ ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( ( D x. A ) / ( D x. C ) ) = ( A / C ) )
23 14 21 15 22 syl3anc 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( D x. A ) / ( D x. C ) ) = ( A / C ) )
24 20 23 eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A x. D ) / ( C x. D ) ) = ( A / C ) )
25 simplr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> B e. CC )
26 25 18 mulcomd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( B x. C ) = ( C x. B ) )
27 26 oveq1d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( B x. C ) / ( C x. D ) ) = ( ( C x. B ) / ( C x. D ) ) )
28 divcan5 
 |-  ( ( B e. CC /\ ( D e. CC /\ D =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. B ) / ( C x. D ) ) = ( B / D ) )
29 25 15 21 28 syl3anc 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( C x. B ) / ( C x. D ) ) = ( B / D ) )
30 27 29 eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( B x. C ) / ( C x. D ) ) = ( B / D ) )
31 24 30 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( ( A x. D ) / ( C x. D ) ) + ( ( B x. C ) / ( C x. D ) ) ) = ( ( A / C ) + ( B / D ) ) )
32 13 31 eqtr2d 
 |-  ( ( ( 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 ) ) / ( C x. D ) ) )