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 ABCC0DD0ACBD=ADBCCD

Proof

Step Hyp Ref Expression
1 negcl BB
2 divadddiv ABCC0DD0AC+BD=AD+BCCD
3 1 2 sylanl2 ABCC0DD0AC+BD=AD+BCCD
4 simplr ABCC0DD0B
5 simprrl ABCC0DD0D
6 simprrr ABCC0DD0D0
7 divneg BDD0BD=BD
8 4 5 6 7 syl3anc ABCC0DD0BD=BD
9 8 oveq2d ABCC0DD0AC+BD=AC+BD
10 simpll ABCC0DD0A
11 simprll ABCC0DD0C
12 simprlr ABCC0DD0C0
13 divcl ACC0AC
14 10 11 12 13 syl3anc ABCC0DD0AC
15 divcl BDD0BD
16 4 5 6 15 syl3anc ABCC0DD0BD
17 14 16 negsubd ABCC0DD0AC+BD=ACBD
18 9 17 eqtr3d ABCC0DD0AC+BD=ACBD
19 3 18 eqtr3d ABCC0DD0AD+BCCD=ACBD
20 4 11 mulneg1d ABCC0DD0BC=BC
21 20 oveq2d ABCC0DD0AD+BC=AD+BC
22 10 5 mulcld ABCC0DD0AD
23 4 11 mulcld ABCC0DD0BC
24 22 23 negsubd ABCC0DD0AD+BC=ADBC
25 21 24 eqtrd ABCC0DD0AD+BC=ADBC
26 25 oveq1d ABCC0DD0AD+BCCD=ADBCCD
27 19 26 eqtr3d ABCC0DD0ACBD=ADBCCD