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 = TopOpen fld
eldv.g G = z A B F z F B z B
eldv.s φ S
eldv.f φ F : A
eldv.a φ A S
Assertion eldv φ B F S C B int T A C G lim B

Proof

Step Hyp Ref Expression
1 dvval.t T = K 𝑡 S
2 dvval.k K = TopOpen fld
3 eldv.g G = z A B F z F B z B
4 eldv.s φ S
5 eldv.f φ F : A
6 eldv.a φ A S
7 1 2 dvfval S F : A A S S D F = x int T A x × z A x F z F x z x lim x S D F int T A ×
8 4 5 6 7 syl3anc φ S D F = x int T A x × z A x F z F x z x lim x S D F int T A ×
9 8 simpld φ S D F = x int T A x × z A x F z F x z x lim x
10 9 eleq2d φ B C F S B C x int T A x × z A x F z F x z x lim x
11 df-br B F S C B C F S
12 11 bicomi B C F S B F S C
13 sneq x = B x = B
14 13 difeq2d x = B A x = A B
15 fveq2 x = B F x = F B
16 15 oveq2d x = B F z F x = F z F B
17 oveq2 x = B z x = z B
18 16 17 oveq12d x = B F z F x z x = F z F B z B
19 14 18 mpteq12dv x = B z A x F z F x z x = z A B F z F B z B
20 19 3 syl6eqr x = B z A x F z F x z x = G
21 id x = B x = B
22 20 21 oveq12d x = B z A x F z F x z x lim x = G lim B
23 22 opeliunxp2 B C x int T A x × z A x F z F x z x lim x B int T A C G lim B
24 10 12 23 3bitr3g φ B F S C B int T A C G lim B