Description: Function-builder for derivative, quotient rule. (Contributed by Glauco Siliprandi, 11-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dvmptdiv.s | |
|
dvmptdiv.a | |
||
dvmptdiv.b | |
||
dvmptdiv.da | |
||
dvmptdiv.c | |
||
dvmptdiv.d | |
||
dvmptdiv.dc | |
||
Assertion | dvmptdiv | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dvmptdiv.s | |
|
2 | dvmptdiv.a | |
|
3 | dvmptdiv.b | |
|
4 | dvmptdiv.da | |
|
5 | dvmptdiv.c | |
|
6 | dvmptdiv.d | |
|
7 | dvmptdiv.dc | |
|
8 | 5 | eldifad | |
9 | eldifsn | |
|
10 | 5 9 | sylib | |
11 | 10 | simprd | |
12 | 2 8 11 | divrecd | |
13 | 12 | mpteq2dva | |
14 | 13 | oveq2d | |
15 | 8 11 | reccld | |
16 | 1cnd | |
|
17 | 16 6 | mulcld | |
18 | 8 | sqcld | |
19 | 11 | neneqd | |
20 | sqeq0 | |
|
21 | 8 20 | syl | |
22 | 19 21 | mtbird | |
23 | 22 | neqned | |
24 | 17 18 23 | divcld | |
25 | 24 | negcld | |
26 | 1cnd | |
|
27 | 1 26 5 6 7 | dvrecg | |
28 | 1 2 3 4 15 25 27 | dvmptmul | |
29 | 1 2 3 4 | dvmptcl | |
30 | 29 8 | mulcld | |
31 | 30 18 23 | divcld | |
32 | 6 2 | mulcld | |
33 | 32 18 23 | divcld | |
34 | 31 33 | negsubd | |
35 | 29 16 8 11 | div12d | |
36 | 29 8 11 | divcld | |
37 | 36 | mulid2d | |
38 | 8 | sqvald | |
39 | 38 | oveq2d | |
40 | 29 8 8 11 11 | divcan5rd | |
41 | 39 40 | eqtr2d | |
42 | 35 37 41 | 3eqtrd | |
43 | 6 | mulid2d | |
44 | 43 | oveq1d | |
45 | 44 | negeqd | |
46 | 45 | oveq1d | |
47 | 6 18 23 | divcld | |
48 | 47 2 | mulneg1d | |
49 | 6 2 18 23 | div23d | |
50 | 49 | eqcomd | |
51 | 50 | negeqd | |
52 | 46 48 51 | 3eqtrd | |
53 | 42 52 | oveq12d | |
54 | 30 32 18 23 | divsubdird | |
55 | 34 53 54 | 3eqtr4d | |
56 | 55 | mpteq2dva | |
57 | 14 28 56 | 3eqtrd | |