# Metamath Proof Explorer

## Theorem eldv

Description: The differentiable predicate. A function F is differentiable at B with derivative C iff F is defined in a neighborhood of B and the difference quotient has limit C at B . (Contributed by Mario Carneiro, 7-Aug-2014) (Revised by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypotheses dvval.t ${⊢}{T}={K}{↾}_{𝑡}{S}$
dvval.k ${⊢}{K}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
eldv.g ${⊢}{G}=\left({z}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({B}\right)}{{z}-{B}}\right)$
eldv.s ${⊢}{\phi }\to {S}\subseteq ℂ$
eldv.f ${⊢}{\phi }\to {F}:{A}⟶ℂ$
eldv.a ${⊢}{\phi }\to {A}\subseteq {S}$
Assertion eldv ${⊢}{\phi }\to \left({B}{{F}}_{{S}}^{\prime }{C}↔\left({B}\in \mathrm{int}\left({T}\right)\left({A}\right)\wedge {C}\in \left({G}{lim}_{ℂ}{B}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 dvval.t ${⊢}{T}={K}{↾}_{𝑡}{S}$
2 dvval.k ${⊢}{K}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
3 eldv.g ${⊢}{G}=\left({z}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({B}\right)}{{z}-{B}}\right)$
4 eldv.s ${⊢}{\phi }\to {S}\subseteq ℂ$
5 eldv.f ${⊢}{\phi }\to {F}:{A}⟶ℂ$
6 eldv.a ${⊢}{\phi }\to {A}\subseteq {S}$
7 1 2 dvfval ${⊢}\left({S}\subseteq ℂ\wedge {F}:{A}⟶ℂ\wedge {A}\subseteq {S}\right)\to \left({S}\mathrm{D}{F}=\bigcup _{{x}\in \mathrm{int}\left({T}\right)\left({A}\right)}\left(\left\{{x}\right\}×\left(\left({z}\in \left({A}\setminus \left\{{x}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({x}\right)}{{z}-{x}}\right){lim}_{ℂ}{x}\right)\right)\wedge {S}\mathrm{D}{F}\subseteq \mathrm{int}\left({T}\right)\left({A}\right)×ℂ\right)$
8 4 5 6 7 syl3anc ${⊢}{\phi }\to \left({S}\mathrm{D}{F}=\bigcup _{{x}\in \mathrm{int}\left({T}\right)\left({A}\right)}\left(\left\{{x}\right\}×\left(\left({z}\in \left({A}\setminus \left\{{x}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({x}\right)}{{z}-{x}}\right){lim}_{ℂ}{x}\right)\right)\wedge {S}\mathrm{D}{F}\subseteq \mathrm{int}\left({T}\right)\left({A}\right)×ℂ\right)$
9 8 simpld ${⊢}{\phi }\to {S}\mathrm{D}{F}=\bigcup _{{x}\in \mathrm{int}\left({T}\right)\left({A}\right)}\left(\left\{{x}\right\}×\left(\left({z}\in \left({A}\setminus \left\{{x}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({x}\right)}{{z}-{x}}\right){lim}_{ℂ}{x}\right)\right)$
10 9 eleq2d ${⊢}{\phi }\to \left(⟨{B},{C}⟩\in {{F}}_{{S}}^{\prime }↔⟨{B},{C}⟩\in \bigcup _{{x}\in \mathrm{int}\left({T}\right)\left({A}\right)}\left(\left\{{x}\right\}×\left(\left({z}\in \left({A}\setminus \left\{{x}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({x}\right)}{{z}-{x}}\right){lim}_{ℂ}{x}\right)\right)\right)$
11 df-br ${⊢}{B}{{F}}_{{S}}^{\prime }{C}↔⟨{B},{C}⟩\in {{F}}_{{S}}^{\prime }$
12 11 bicomi ${⊢}⟨{B},{C}⟩\in {{F}}_{{S}}^{\prime }↔{B}{{F}}_{{S}}^{\prime }{C}$
13 sneq ${⊢}{x}={B}\to \left\{{x}\right\}=\left\{{B}\right\}$
14 13 difeq2d ${⊢}{x}={B}\to {A}\setminus \left\{{x}\right\}={A}\setminus \left\{{B}\right\}$
15 fveq2 ${⊢}{x}={B}\to {F}\left({x}\right)={F}\left({B}\right)$
16 15 oveq2d ${⊢}{x}={B}\to {F}\left({z}\right)-{F}\left({x}\right)={F}\left({z}\right)-{F}\left({B}\right)$
17 oveq2 ${⊢}{x}={B}\to {z}-{x}={z}-{B}$
18 16 17 oveq12d ${⊢}{x}={B}\to \frac{{F}\left({z}\right)-{F}\left({x}\right)}{{z}-{x}}=\frac{{F}\left({z}\right)-{F}\left({B}\right)}{{z}-{B}}$
19 14 18 mpteq12dv ${⊢}{x}={B}\to \left({z}\in \left({A}\setminus \left\{{x}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({x}\right)}{{z}-{x}}\right)=\left({z}\in \left({A}\setminus \left\{{B}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({B}\right)}{{z}-{B}}\right)$
20 19 3 syl6eqr ${⊢}{x}={B}\to \left({z}\in \left({A}\setminus \left\{{x}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({x}\right)}{{z}-{x}}\right)={G}$
21 id ${⊢}{x}={B}\to {x}={B}$
22 20 21 oveq12d ${⊢}{x}={B}\to \left({z}\in \left({A}\setminus \left\{{x}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({x}\right)}{{z}-{x}}\right){lim}_{ℂ}{x}={G}{lim}_{ℂ}{B}$
23 22 opeliunxp2 ${⊢}⟨{B},{C}⟩\in \bigcup _{{x}\in \mathrm{int}\left({T}\right)\left({A}\right)}\left(\left\{{x}\right\}×\left(\left({z}\in \left({A}\setminus \left\{{x}\right\}\right)⟼\frac{{F}\left({z}\right)-{F}\left({x}\right)}{{z}-{x}}\right){lim}_{ℂ}{x}\right)\right)↔\left({B}\in \mathrm{int}\left({T}\right)\left({A}\right)\wedge {C}\in \left({G}{lim}_{ℂ}{B}\right)\right)$
24 10 12 23 3bitr3g ${⊢}{\phi }\to \left({B}{{F}}_{{S}}^{\prime }{C}↔\left({B}\in \mathrm{int}\left({T}\right)\left({A}\right)\wedge {C}\in \left({G}{lim}_{ℂ}{B}\right)\right)\right)$