# Metamath Proof Explorer

## Theorem dvmptdiv

Description: Function-builder for derivative, quotient rule. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dvmptdiv.s ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
dvmptdiv.a ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {A}\in ℂ$
dvmptdiv.b ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {B}\in {V}$
dvmptdiv.da ${⊢}{\phi }\to \frac{d\left({x}\in {X}⟼{A}\right)}{{d}_{{S}}{x}}=\left({x}\in {X}⟼{B}\right)$
dvmptdiv.c ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {C}\in \left(ℂ\setminus \left\{0\right\}\right)$
dvmptdiv.d ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {D}\in ℂ$
dvmptdiv.dc ${⊢}{\phi }\to \frac{d\left({x}\in {X}⟼{C}\right)}{{d}_{{S}}{x}}=\left({x}\in {X}⟼{D}\right)$
Assertion dvmptdiv ${⊢}{\phi }\to \frac{d\left({x}\in {X}⟼\frac{{A}}{{C}}\right)}{{d}_{{S}}{x}}=\left({x}\in {X}⟼\frac{{B}{C}-{D}{A}}{{{C}}^{2}}\right)$

### Proof

Step Hyp Ref Expression
1 dvmptdiv.s ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
2 dvmptdiv.a ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {A}\in ℂ$
3 dvmptdiv.b ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {B}\in {V}$
4 dvmptdiv.da ${⊢}{\phi }\to \frac{d\left({x}\in {X}⟼{A}\right)}{{d}_{{S}}{x}}=\left({x}\in {X}⟼{B}\right)$
5 dvmptdiv.c ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {C}\in \left(ℂ\setminus \left\{0\right\}\right)$
6 dvmptdiv.d ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {D}\in ℂ$
7 dvmptdiv.dc ${⊢}{\phi }\to \frac{d\left({x}\in {X}⟼{C}\right)}{{d}_{{S}}{x}}=\left({x}\in {X}⟼{D}\right)$
8 5 eldifad ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {C}\in ℂ$
9 eldifsn ${⊢}{C}\in \left(ℂ\setminus \left\{0\right\}\right)↔\left({C}\in ℂ\wedge {C}\ne 0\right)$
10 5 9 sylib ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \left({C}\in ℂ\wedge {C}\ne 0\right)$
11 10 simprd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {C}\ne 0$
12 2 8 11 divrecd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \frac{{A}}{{C}}={A}\left(\frac{1}{{C}}\right)$
13 12 mpteq2dva ${⊢}{\phi }\to \left({x}\in {X}⟼\frac{{A}}{{C}}\right)=\left({x}\in {X}⟼{A}\left(\frac{1}{{C}}\right)\right)$
14 13 oveq2d ${⊢}{\phi }\to \frac{d\left({x}\in {X}⟼\frac{{A}}{{C}}\right)}{{d}_{{S}}{x}}=\frac{d\left({x}\in {X}⟼{A}\left(\frac{1}{{C}}\right)\right)}{{d}_{{S}}{x}}$
15 8 11 reccld ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \frac{1}{{C}}\in ℂ$
16 1cnd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to 1\in ℂ$
17 16 6 mulcld ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to 1{D}\in ℂ$
18 8 sqcld ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {{C}}^{2}\in ℂ$
19 11 neneqd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to ¬{C}=0$
20 sqeq0 ${⊢}{C}\in ℂ\to \left({{C}}^{2}=0↔{C}=0\right)$
21 8 20 syl ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \left({{C}}^{2}=0↔{C}=0\right)$
22 19 21 mtbird ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to ¬{{C}}^{2}=0$
23 22 neqned ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {{C}}^{2}\ne 0$
24 17 18 23 divcld ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \frac{1{D}}{{{C}}^{2}}\in ℂ$
25 24 negcld ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to -\frac{1{D}}{{{C}}^{2}}\in ℂ$
26 1cnd ${⊢}{\phi }\to 1\in ℂ$
27 1 26 5 6 7 dvrecg ${⊢}{\phi }\to \frac{d\left({x}\in {X}⟼\frac{1}{{C}}\right)}{{d}_{{S}}{x}}=\left({x}\in {X}⟼-\frac{1{D}}{{{C}}^{2}}\right)$
28 1 2 3 4 15 25 27 dvmptmul ${⊢}{\phi }\to \frac{d\left({x}\in {X}⟼{A}\left(\frac{1}{{C}}\right)\right)}{{d}_{{S}}{x}}=\left({x}\in {X}⟼{B}\left(\frac{1}{{C}}\right)+\left(-\frac{1{D}}{{{C}}^{2}}\right){A}\right)$
29 1 2 3 4 dvmptcl ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {B}\in ℂ$
30 29 8 mulcld ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {B}{C}\in ℂ$
31 30 18 23 divcld ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \frac{{B}{C}}{{{C}}^{2}}\in ℂ$
32 6 2 mulcld ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {D}{A}\in ℂ$
33 32 18 23 divcld ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \frac{{D}{A}}{{{C}}^{2}}\in ℂ$
34 31 33 negsubd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \left(\frac{{B}{C}}{{{C}}^{2}}\right)+\left(-\frac{{D}{A}}{{{C}}^{2}}\right)=\left(\frac{{B}{C}}{{{C}}^{2}}\right)-\left(\frac{{D}{A}}{{{C}}^{2}}\right)$
35 29 16 8 11 div12d ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {B}\left(\frac{1}{{C}}\right)=1\left(\frac{{B}}{{C}}\right)$
36 29 8 11 divcld ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \frac{{B}}{{C}}\in ℂ$
37 36 mulid2d ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to 1\left(\frac{{B}}{{C}}\right)=\frac{{B}}{{C}}$
38 8 sqvald ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {{C}}^{2}={C}{C}$
39 38 oveq2d ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \frac{{B}{C}}{{{C}}^{2}}=\frac{{B}{C}}{{C}{C}}$
40 29 8 8 11 11 divcan5rd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \frac{{B}{C}}{{C}{C}}=\frac{{B}}{{C}}$
41 39 40 eqtr2d ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \frac{{B}}{{C}}=\frac{{B}{C}}{{{C}}^{2}}$
42 35 37 41 3eqtrd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {B}\left(\frac{1}{{C}}\right)=\frac{{B}{C}}{{{C}}^{2}}$
43 6 mulid2d ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to 1{D}={D}$
44 43 oveq1d ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \frac{1{D}}{{{C}}^{2}}=\frac{{D}}{{{C}}^{2}}$
45 44 negeqd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to -\frac{1{D}}{{{C}}^{2}}=-\frac{{D}}{{{C}}^{2}}$
46 45 oveq1d ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \left(-\frac{1{D}}{{{C}}^{2}}\right){A}=\left(-\frac{{D}}{{{C}}^{2}}\right){A}$
47 6 18 23 divcld ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \frac{{D}}{{{C}}^{2}}\in ℂ$
48 47 2 mulneg1d ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \left(-\frac{{D}}{{{C}}^{2}}\right){A}=-\left(\frac{{D}}{{{C}}^{2}}\right){A}$
49 6 2 18 23 div23d ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \frac{{D}{A}}{{{C}}^{2}}=\left(\frac{{D}}{{{C}}^{2}}\right){A}$
50 49 eqcomd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \left(\frac{{D}}{{{C}}^{2}}\right){A}=\frac{{D}{A}}{{{C}}^{2}}$
51 50 negeqd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to -\left(\frac{{D}}{{{C}}^{2}}\right){A}=-\frac{{D}{A}}{{{C}}^{2}}$
52 46 48 51 3eqtrd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \left(-\frac{1{D}}{{{C}}^{2}}\right){A}=-\frac{{D}{A}}{{{C}}^{2}}$
53 42 52 oveq12d ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {B}\left(\frac{1}{{C}}\right)+\left(-\frac{1{D}}{{{C}}^{2}}\right){A}=\left(\frac{{B}{C}}{{{C}}^{2}}\right)+\left(-\frac{{D}{A}}{{{C}}^{2}}\right)$
54 30 32 18 23 divsubdird ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \frac{{B}{C}-{D}{A}}{{{C}}^{2}}=\left(\frac{{B}{C}}{{{C}}^{2}}\right)-\left(\frac{{D}{A}}{{{C}}^{2}}\right)$
55 34 53 54 3eqtr4d ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {B}\left(\frac{1}{{C}}\right)+\left(-\frac{1{D}}{{{C}}^{2}}\right){A}=\frac{{B}{C}-{D}{A}}{{{C}}^{2}}$
56 55 mpteq2dva ${⊢}{\phi }\to \left({x}\in {X}⟼{B}\left(\frac{1}{{C}}\right)+\left(-\frac{1{D}}{{{C}}^{2}}\right){A}\right)=\left({x}\in {X}⟼\frac{{B}{C}-{D}{A}}{{{C}}^{2}}\right)$
57 14 28 56 3eqtrd ${⊢}{\phi }\to \frac{d\left({x}\in {X}⟼\frac{{A}}{{C}}\right)}{{d}_{{S}}{x}}=\left({x}\in {X}⟼\frac{{B}{C}-{D}{A}}{{{C}}^{2}}\right)$