Description: Subtraction of two ratios. (Contributed by Scott Fenton, 22-Apr-2014) (Revised by Mario Carneiro, 2-May-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | divsubdiv | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | negcl | |
|
2 | divadddiv | |
|
3 | 1 2 | sylanl2 | |
4 | simplr | |
|
5 | simprrl | |
|
6 | simprrr | |
|
7 | divneg | |
|
8 | 4 5 6 7 | syl3anc | |
9 | 8 | oveq2d | |
10 | simpll | |
|
11 | simprll | |
|
12 | simprlr | |
|
13 | divcl | |
|
14 | 10 11 12 13 | syl3anc | |
15 | divcl | |
|
16 | 4 5 6 15 | syl3anc | |
17 | 14 16 | negsubd | |
18 | 9 17 | eqtr3d | |
19 | 3 18 | eqtr3d | |
20 | 4 11 | mulneg1d | |
21 | 20 | oveq2d | |
22 | 10 5 | mulcld | |
23 | 4 11 | mulcld | |
24 | 22 23 | negsubd | |
25 | 21 24 | eqtrd | |
26 | 25 | oveq1d | |
27 | 19 26 | eqtr3d | |