Metamath Proof Explorer

Theorem dvcnp

Description: The difference quotient is continuous at B when the original function is differentiable at B . (Contributed by Mario Carneiro, 8-Aug-2014) (Revised by Mario Carneiro, 28-Dec-2016)

Ref Expression
Hypotheses dvcnp.j 
|- J = ( K |`t A )
dvcnp.k 
|- K = ( TopOpen ` CCfld )
dvcnp.g 
|- G = ( z e. A |-> if ( z = B , ( ( S _D F ) ` B ) , ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ) )
Assertion dvcnp 
|- ( ( ( S e. { RR , CC } /\ F : A --> CC /\ A C_ S ) /\ B e. dom ( S _D F ) ) -> G e. ( ( J CnP K ) ` B ) )

Proof

Step Hyp Ref Expression
1 dvcnp.j 
 |-  J = ( K |`t A )
2 dvcnp.k 
 |-  K = ( TopOpen ` CCfld )
3 dvcnp.g 
 |-  G = ( z e. A |-> if ( z = B , ( ( S _D F ) ` B ) , ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ) )
4 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D F ) : dom ( S _D F ) --> CC )
5 4 3ad2ant1 
 |-  ( ( S e. { RR , CC } /\ F : A --> CC /\ A C_ S ) -> ( S _D F ) : dom ( S _D F ) --> CC )
6 ffun 
 |-  ( ( S _D F ) : dom ( S _D F ) --> CC -> Fun ( S _D F ) )
7 funfvbrb 
 |-  ( Fun ( S _D F ) -> ( B e. dom ( S _D F ) <-> B ( S _D F ) ( ( S _D F ) ` B ) ) )
8 5 6 7 3syl 
 |-  ( ( S e. { RR , CC } /\ F : A --> CC /\ A C_ S ) -> ( B e. dom ( S _D F ) <-> B ( S _D F ) ( ( S _D F ) ` B ) ) )
9 eqid 
 |-  ( K |`t S ) = ( K |`t S )
10 eqid 
 |-  ( z e. ( A \ { B } ) |-> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ) = ( z e. ( A \ { B } ) |-> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) )
11 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
12 11 3ad2ant1 
 |-  ( ( S e. { RR , CC } /\ F : A --> CC /\ A C_ S ) -> S C_ CC )
13 simp2 
 |-  ( ( S e. { RR , CC } /\ F : A --> CC /\ A C_ S ) -> F : A --> CC )
14 simp3 
 |-  ( ( S e. { RR , CC } /\ F : A --> CC /\ A C_ S ) -> A C_ S )
15 9 2 10 12 13 14 eldv 
 |-  ( ( S e. { RR , CC } /\ F : A --> CC /\ A C_ S ) -> ( B ( S _D F ) ( ( S _D F ) ` B ) <-> ( B e. ( ( int ` ( K |`t S ) ) ` A ) /\ ( ( S _D F ) ` B ) e. ( ( z e. ( A \ { B } ) |-> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ) limCC B ) ) ) )
16 8 15 bitrd 
 |-  ( ( S e. { RR , CC } /\ F : A --> CC /\ A C_ S ) -> ( B e. dom ( S _D F ) <-> ( B e. ( ( int ` ( K |`t S ) ) ` A ) /\ ( ( S _D F ) ` B ) e. ( ( z e. ( A \ { B } ) |-> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ) limCC B ) ) ) )
17 16 simplbda 
 |-  ( ( ( S e. { RR , CC } /\ F : A --> CC /\ A C_ S ) /\ B e. dom ( S _D F ) ) -> ( ( S _D F ) ` B ) e. ( ( z e. ( A \ { B } ) |-> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ) limCC B ) )
18 14 12 sstrd 
 |-  ( ( S e. { RR , CC } /\ F : A --> CC /\ A C_ S ) -> A C_ CC )
19 18 adantr 
 |-  ( ( ( S e. { RR , CC } /\ F : A --> CC /\ A C_ S ) /\ B e. dom ( S _D F ) ) -> A C_ CC )
20 12 13 14 dvbss 
 |-  ( ( S e. { RR , CC } /\ F : A --> CC /\ A C_ S ) -> dom ( S _D F ) C_ A )
21 20 sselda 
 |-  ( ( ( S e. { RR , CC } /\ F : A --> CC /\ A C_ S ) /\ B e. dom ( S _D F ) ) -> B e. A )
22 eldifsn 
 |-  ( z e. ( A \ { B } ) <-> ( z e. A /\ z =/= B ) )
23 13 adantr 
 |-  ( ( ( S e. { RR , CC } /\ F : A --> CC /\ A C_ S ) /\ B e. dom ( S _D F ) ) -> F : A --> CC )
24 23 19 21 dvlem 
 |-  ( ( ( ( S e. { RR , CC } /\ F : A --> CC /\ A C_ S ) /\ B e. dom ( S _D F ) ) /\ z e. ( A \ { B } ) ) -> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) e. CC )
25 22 24 sylan2br 
 |-  ( ( ( ( S e. { RR , CC } /\ F : A --> CC /\ A C_ S ) /\ B e. dom ( S _D F ) ) /\ ( z e. A /\ z =/= B ) ) -> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) e. CC )
26 19 21 25 1 2 limcmpt2 
 |-  ( ( ( S e. { RR , CC } /\ F : A --> CC /\ A C_ S ) /\ B e. dom ( S _D F ) ) -> ( ( ( S _D F ) ` B ) e. ( ( z e. ( A \ { B } ) |-> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ) limCC B ) <-> ( z e. A |-> if ( z = B , ( ( S _D F ) ` B ) , ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ) ) e. ( ( J CnP K ) ` B ) ) )
27 17 26 mpbid 
 |-  ( ( ( S e. { RR , CC } /\ F : A --> CC /\ A C_ S ) /\ B e. dom ( S _D F ) ) -> ( z e. A |-> if ( z = B , ( ( S _D F ) ` B ) , ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ) ) e. ( ( J CnP K ) ` B ) )
28 3 27 eqeltrid 
 |-  ( ( ( S e. { RR , CC } /\ F : A --> CC /\ A C_ S ) /\ B e. dom ( S _D F ) ) -> G e. ( ( J CnP K ) ` B ) )