Metamath Proof Explorer

Theorem divsubdiv

Description: Subtraction of two ratios. (Contributed by Scott Fenton, 22-Apr-2014) (Revised by Mario Carneiro, 2-May-2016)

Ref Expression
Assertion divsubdiv 
|- ( ( ( 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 negcl 
 |-  ( B e. CC -> -u B e. CC )
2 divadddiv 
 |-  ( ( ( A e. CC /\ -u B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A / C ) + ( -u B / D ) ) = ( ( ( A x. D ) + ( -u B x. C ) ) / ( C x. D ) ) )
3 1 2 sylanl2 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A / C ) + ( -u B / D ) ) = ( ( ( A x. D ) + ( -u B x. C ) ) / ( C x. D ) ) )
4 simplr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> B e. CC )
5 simprrl 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> D e. CC )
6 simprrr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> D =/= 0 )
7 divneg 
 |-  ( ( B e. CC /\ D e. CC /\ D =/= 0 ) -> -u ( B / D ) = ( -u B / D ) )
8 4 5 6 7 syl3anc 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> -u ( B / D ) = ( -u B / D ) )
9 8 oveq2d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A / C ) + -u ( B / D ) ) = ( ( A / C ) + ( -u B / D ) ) )
10 simpll 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> A e. CC )
11 simprll 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> C e. CC )
12 simprlr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> C =/= 0 )
13 divcl 
 |-  ( ( A e. CC /\ C e. CC /\ C =/= 0 ) -> ( A / C ) e. CC )
14 10 11 12 13 syl3anc 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( A / C ) e. CC )
15 divcl 
 |-  ( ( B e. CC /\ D e. CC /\ D =/= 0 ) -> ( B / D ) e. CC )
16 4 5 6 15 syl3anc 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( B / D ) e. CC )
17 14 16 negsubd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A / C ) + -u ( B / D ) ) = ( ( A / C ) - ( B / D ) ) )
18 9 17 eqtr3d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A / C ) + ( -u B / D ) ) = ( ( A / C ) - ( B / D ) ) )
19 3 18 eqtr3d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( ( A x. D ) + ( -u B x. C ) ) / ( C x. D ) ) = ( ( A / C ) - ( B / D ) ) )
20 4 11 mulneg1d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( -u B x. C ) = -u ( B x. C ) )
21 20 oveq2d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A x. D ) + ( -u B x. C ) ) = ( ( A x. D ) + -u ( B x. C ) ) )
22 10 5 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( A x. D ) e. CC )
23 4 11 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( B x. C ) e. CC )
24 22 23 negsubd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A x. D ) + -u ( B x. C ) ) = ( ( A x. D ) - ( B x. C ) ) )
25 21 24 eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A x. D ) + ( -u B x. C ) ) = ( ( A x. D ) - ( B x. C ) ) )
26 25 oveq1d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( ( A x. D ) + ( -u B x. C ) ) / ( C x. D ) ) = ( ( ( A x. D ) - ( B x. C ) ) / ( C x. D ) ) )
27 19 26 eqtr3d 
 |-  ( ( ( 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 ) ) )