Description: Function-builder for derivative, subtraction rule. (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 11-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dvmptadd.s | |
|
dvmptadd.a | |
||
dvmptadd.b | |
||
dvmptadd.da | |
||
dvmptsub.c | |
||
dvmptsub.d | |
||
dvmptsub.dc | |
||
Assertion | dvmptsub | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dvmptadd.s | |
|
2 | dvmptadd.a | |
|
3 | dvmptadd.b | |
|
4 | dvmptadd.da | |
|
5 | dvmptsub.c | |
|
6 | dvmptsub.d | |
|
7 | dvmptsub.dc | |
|
8 | 5 | negcld | |
9 | negex | |
|
10 | 9 | a1i | |
11 | 1 5 6 7 | dvmptneg | |
12 | 1 2 3 4 8 10 11 | dvmptadd | |
13 | 2 5 | negsubd | |
14 | 13 | mpteq2dva | |
15 | 14 | oveq2d | |
16 | 1 2 3 4 | dvmptcl | |
17 | 1 5 6 7 | dvmptcl | |
18 | 16 17 | negsubd | |
19 | 18 | mpteq2dva | |
20 | 12 15 19 | 3eqtr3d | |