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 ) ) ) )