# Metamath Proof Explorer

## Theorem dvdivf

Description: The quotient rule for everywhere-differentiable functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dvdivf.s ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
dvdivf.f ${⊢}{\phi }\to {F}:{X}⟶ℂ$
dvdivf.g ${⊢}{\phi }\to {G}:{X}⟶ℂ\setminus \left\{0\right\}$
dvdivf.fdv ${⊢}{\phi }\to \mathrm{dom}{{F}}_{{S}}^{\prime }={X}$
dvdivf.gdv ${⊢}{\phi }\to \mathrm{dom}{{G}}_{{S}}^{\prime }={X}$
Assertion dvdivf ${⊢}{\phi }\to {S}\mathrm{D}\left({F}{÷}_{f}{G}\right)=\left(\left({{F}}_{{S}}^{\prime }{×}_{f}{G}\right){-}_{f}\left({{G}}_{{S}}^{\prime }{×}_{f}{F}\right)\right){÷}_{f}\left({G}{×}_{f}{G}\right)$

### Proof

Step Hyp Ref Expression
1 dvdivf.s ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
2 dvdivf.f ${⊢}{\phi }\to {F}:{X}⟶ℂ$
3 dvdivf.g ${⊢}{\phi }\to {G}:{X}⟶ℂ\setminus \left\{0\right\}$
4 dvdivf.fdv ${⊢}{\phi }\to \mathrm{dom}{{F}}_{{S}}^{\prime }={X}$
5 dvdivf.gdv ${⊢}{\phi }\to \mathrm{dom}{{G}}_{{S}}^{\prime }={X}$
6 2 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {F}\left({x}\right)\in ℂ$
7 dvfg ${⊢}{S}\in \left\{ℝ,ℂ\right\}\to {{F}}_{{S}}^{\prime }:\mathrm{dom}{{F}}_{{S}}^{\prime }⟶ℂ$
8 1 7 syl ${⊢}{\phi }\to {{F}}_{{S}}^{\prime }:\mathrm{dom}{{F}}_{{S}}^{\prime }⟶ℂ$
9 4 feq2d ${⊢}{\phi }\to \left({{F}}_{{S}}^{\prime }:\mathrm{dom}{{F}}_{{S}}^{\prime }⟶ℂ↔{{F}}_{{S}}^{\prime }:{X}⟶ℂ\right)$
10 8 9 mpbid ${⊢}{\phi }\to {{F}}_{{S}}^{\prime }:{X}⟶ℂ$
11 10 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {{F}}_{{S}}^{\prime }\left({x}\right)\in ℂ$
12 2 feqmptd ${⊢}{\phi }\to {F}=\left({x}\in {X}⟼{F}\left({x}\right)\right)$
13 12 oveq2d ${⊢}{\phi }\to {S}\mathrm{D}{F}=\frac{d\left({x}\in {X}⟼{F}\left({x}\right)\right)}{{d}_{{S}}{x}}$
14 10 feqmptd ${⊢}{\phi }\to {S}\mathrm{D}{F}=\left({x}\in {X}⟼{{F}}_{{S}}^{\prime }\left({x}\right)\right)$
15 13 14 eqtr3d ${⊢}{\phi }\to \frac{d\left({x}\in {X}⟼{F}\left({x}\right)\right)}{{d}_{{S}}{x}}=\left({x}\in {X}⟼{{F}}_{{S}}^{\prime }\left({x}\right)\right)$
16 3 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {G}\left({x}\right)\in \left(ℂ\setminus \left\{0\right\}\right)$
17 dvfg ${⊢}{S}\in \left\{ℝ,ℂ\right\}\to {{G}}_{{S}}^{\prime }:\mathrm{dom}{{G}}_{{S}}^{\prime }⟶ℂ$
18 1 17 syl ${⊢}{\phi }\to {{G}}_{{S}}^{\prime }:\mathrm{dom}{{G}}_{{S}}^{\prime }⟶ℂ$
19 5 feq2d ${⊢}{\phi }\to \left({{G}}_{{S}}^{\prime }:\mathrm{dom}{{G}}_{{S}}^{\prime }⟶ℂ↔{{G}}_{{S}}^{\prime }:{X}⟶ℂ\right)$
20 18 19 mpbid ${⊢}{\phi }\to {{G}}_{{S}}^{\prime }:{X}⟶ℂ$
21 20 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {{G}}_{{S}}^{\prime }\left({x}\right)\in ℂ$
22 3 feqmptd ${⊢}{\phi }\to {G}=\left({x}\in {X}⟼{G}\left({x}\right)\right)$
23 22 oveq2d ${⊢}{\phi }\to {S}\mathrm{D}{G}=\frac{d\left({x}\in {X}⟼{G}\left({x}\right)\right)}{{d}_{{S}}{x}}$
24 20 feqmptd ${⊢}{\phi }\to {S}\mathrm{D}{G}=\left({x}\in {X}⟼{{G}}_{{S}}^{\prime }\left({x}\right)\right)$
25 23 24 eqtr3d ${⊢}{\phi }\to \frac{d\left({x}\in {X}⟼{G}\left({x}\right)\right)}{{d}_{{S}}{x}}=\left({x}\in {X}⟼{{G}}_{{S}}^{\prime }\left({x}\right)\right)$
26 1 6 11 15 16 21 25 dvmptdiv ${⊢}{\phi }\to \frac{d\left({x}\in {X}⟼\frac{{F}\left({x}\right)}{{G}\left({x}\right)}\right)}{{d}_{{S}}{x}}=\left({x}\in {X}⟼\frac{{{F}}_{{S}}^{\prime }\left({x}\right){G}\left({x}\right)-{{G}}_{{S}}^{\prime }\left({x}\right){F}\left({x}\right)}{{{G}\left({x}\right)}^{2}}\right)$
27 ovex ${⊢}{S}\mathrm{D}{F}\in \mathrm{V}$
28 27 dmex ${⊢}\mathrm{dom}{{F}}_{{S}}^{\prime }\in \mathrm{V}$
29 4 28 eqeltrrdi ${⊢}{\phi }\to {X}\in \mathrm{V}$
30 29 6 16 12 22 offval2 ${⊢}{\phi }\to {F}{÷}_{f}{G}=\left({x}\in {X}⟼\frac{{F}\left({x}\right)}{{G}\left({x}\right)}\right)$
31 30 oveq2d ${⊢}{\phi }\to {S}\mathrm{D}\left({F}{÷}_{f}{G}\right)=\frac{d\left({x}\in {X}⟼\frac{{F}\left({x}\right)}{{G}\left({x}\right)}\right)}{{d}_{{S}}{x}}$
32 ovexd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {{F}}_{{S}}^{\prime }\left({x}\right){G}\left({x}\right)-{{G}}_{{S}}^{\prime }\left({x}\right){F}\left({x}\right)\in \mathrm{V}$
33 16 eldifad ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {G}\left({x}\right)\in ℂ$
34 33 sqcld ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {{G}\left({x}\right)}^{2}\in ℂ$
35 11 33 mulcld ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {{F}}_{{S}}^{\prime }\left({x}\right){G}\left({x}\right)\in ℂ$
36 21 6 mulcld ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {{G}}_{{S}}^{\prime }\left({x}\right){F}\left({x}\right)\in ℂ$
37 29 11 33 14 22 offval2 ${⊢}{\phi }\to {{F}}_{{S}}^{\prime }{×}_{f}{G}=\left({x}\in {X}⟼{{F}}_{{S}}^{\prime }\left({x}\right){G}\left({x}\right)\right)$
38 29 21 6 24 12 offval2 ${⊢}{\phi }\to {{G}}_{{S}}^{\prime }{×}_{f}{F}=\left({x}\in {X}⟼{{G}}_{{S}}^{\prime }\left({x}\right){F}\left({x}\right)\right)$
39 29 35 36 37 38 offval2 ${⊢}{\phi }\to \left({{F}}_{{S}}^{\prime }{×}_{f}{G}\right){-}_{f}\left({{G}}_{{S}}^{\prime }{×}_{f}{F}\right)=\left({x}\in {X}⟼{{F}}_{{S}}^{\prime }\left({x}\right){G}\left({x}\right)-{{G}}_{{S}}^{\prime }\left({x}\right){F}\left({x}\right)\right)$
40 29 16 16 22 22 offval2 ${⊢}{\phi }\to {G}{×}_{f}{G}=\left({x}\in {X}⟼{G}\left({x}\right){G}\left({x}\right)\right)$
41 33 sqvald ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {{G}\left({x}\right)}^{2}={G}\left({x}\right){G}\left({x}\right)$
42 41 mpteq2dva ${⊢}{\phi }\to \left({x}\in {X}⟼{{G}\left({x}\right)}^{2}\right)=\left({x}\in {X}⟼{G}\left({x}\right){G}\left({x}\right)\right)$
43 40 42 eqtr4d ${⊢}{\phi }\to {G}{×}_{f}{G}=\left({x}\in {X}⟼{{G}\left({x}\right)}^{2}\right)$
44 29 32 34 39 43 offval2 ${⊢}{\phi }\to \left(\left({{F}}_{{S}}^{\prime }{×}_{f}{G}\right){-}_{f}\left({{G}}_{{S}}^{\prime }{×}_{f}{F}\right)\right){÷}_{f}\left({G}{×}_{f}{G}\right)=\left({x}\in {X}⟼\frac{{{F}}_{{S}}^{\prime }\left({x}\right){G}\left({x}\right)-{{G}}_{{S}}^{\prime }\left({x}\right){F}\left({x}\right)}{{{G}\left({x}\right)}^{2}}\right)$
45 26 31 44 3eqtr4d ${⊢}{\phi }\to {S}\mathrm{D}\left({F}{÷}_{f}{G}\right)=\left(\left({{F}}_{{S}}^{\prime }{×}_{f}{G}\right){-}_{f}\left({{G}}_{{S}}^{\prime }{×}_{f}{F}\right)\right){÷}_{f}\left({G}{×}_{f}{G}\right)$