This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 |`t S )
dvval.k 
|- K = ( TopOpen ` CCfld )
eldv.g 
|- G = ( z e. ( A \ { B } ) |-> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) )
eldv.s 
|- ( ph -> S C_ CC )
eldv.f 
|- ( ph -> F : A --> CC )
eldv.a 
|- ( ph -> A C_ S )
Assertion eldv 
|- ( ph -> ( B ( S _D F ) C <-> ( B e. ( ( int ` T ) ` A ) /\ C e. ( G limCC B ) ) ) )

Proof

Step Hyp Ref Expression
1 dvval.t 
 |-  T = ( K |`t S )
2 dvval.k 
 |-  K = ( TopOpen ` CCfld )
3 eldv.g 
 |-  G = ( z e. ( A \ { B } ) |-> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) )
4 eldv.s 
 |-  ( ph -> S C_ CC )
5 eldv.f 
 |-  ( ph -> F : A --> CC )
6 eldv.a 
 |-  ( ph -> A C_ S )
7 1 2 dvfval 
 |-  ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> ( ( S _D F ) = U_ x e. ( ( int ` T ) ` A ) ( { x } X. ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) /\ ( S _D F ) C_ ( ( ( int ` T ) ` A ) X. CC ) ) )
8 4 5 6 7 syl3anc 
 |-  ( ph -> ( ( S _D F ) = U_ x e. ( ( int ` T ) ` A ) ( { x } X. ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) /\ ( S _D F ) C_ ( ( ( int ` T ) ` A ) X. CC ) ) )
9 8 simpld 
 |-  ( ph -> ( S _D F ) = U_ x e. ( ( int ` T ) ` A ) ( { x } X. ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) )
10 9 eleq2d 
 |-  ( ph -> ( <. B , C >. e. ( S _D F ) <-> <. B , C >. e. U_ x e. ( ( int ` T ) ` A ) ( { x } X. ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) ) )
11 df-br 
 |-  ( B ( S _D F ) C <-> <. B , C >. e. ( S _D F ) )
12 11 bicomi 
 |-  ( <. B , C >. e. ( S _D F ) <-> B ( S _D F ) 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 e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) = ( z e. ( A \ { B } ) |-> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ) )
20 19 3 eqtr4di 
 |-  ( x = B -> ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) = G )
21 id 
 |-  ( x = B -> x = B )
22 20 21 oveq12d 
 |-  ( x = B -> ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) = ( G limCC B ) )
23 22 opeliunxp2 
 |-  ( <. B , C >. e. U_ x e. ( ( int ` T ) ` A ) ( { x } X. ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) limCC x ) ) <-> ( B e. ( ( int ` T ) ` A ) /\ C e. ( G limCC B ) ) )
24 10 12 23 3bitr3g 
 |-  ( ph -> ( B ( S _D F ) C <-> ( B e. ( ( int ` T ) ` A ) /\ C e. ( G limCC B ) ) ) )