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 ) ) )