Metamath Proof Explorer

Theorem dvcnp2

Description: A function is continuous at each point for which it is differentiable. (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 28-Dec-2016) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

Ref Expression
Hypotheses dvcnp.j 
|- J = ( K |`t A )
dvcnp.k 
|- K = ( TopOpen ` CCfld )
Assertion dvcnp2 
|- ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B e. dom ( S _D F ) ) -> F e. ( ( J CnP K ) ` B ) )

Proof

Step Hyp Ref Expression
1 dvcnp.j 
 |-  J = ( K |`t A )
2 dvcnp.k 
 |-  K = ( TopOpen ` CCfld )
3 simpl2 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> F : A --> CC )
4 3 ffvelcdmda 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. A ) -> ( F ` z ) e. CC )
5 2 cnfldtop 
 |-  K e. Top
6 simpl1 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> S C_ CC )
7 cnex 
 |-  CC e. _V
8 ssexg 
 |-  ( ( S C_ CC /\ CC e. _V ) -> S e. _V )
9 6 7 8 sylancl 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> S e. _V )
10 resttop 
 |-  ( ( K e. Top /\ S e. _V ) -> ( K |`t S ) e. Top )
11 5 9 10 sylancr 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( K |`t S ) e. Top )
12 simpl3 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> A C_ S )
13 2 cnfldtopon 
 |-  K e. ( TopOn ` CC )
14 resttopon 
 |-  ( ( K e. ( TopOn ` CC ) /\ S C_ CC ) -> ( K |`t S ) e. ( TopOn ` S ) )
15 13 6 14 sylancr 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( K |`t S ) e. ( TopOn ` S ) )
16 toponuni 
 |-  ( ( K |`t S ) e. ( TopOn ` S ) -> S = U. ( K |`t S ) )
17 15 16 syl 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> S = U. ( K |`t S ) )
18 12 17 sseqtrd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> A C_ U. ( K |`t S ) )
19 eqid 
 |-  U. ( K |`t S ) = U. ( K |`t S )
20 19 ntrss2 
 |-  ( ( ( K |`t S ) e. Top /\ A C_ U. ( K |`t S ) ) -> ( ( int ` ( K |`t S ) ) ` A ) C_ A )
21 11 18 20 syl2anc 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( ( int ` ( K |`t S ) ) ` A ) C_ A )
22 eqid 
 |-  ( K |`t S ) = ( K |`t S )
23 eqid 
 |-  ( z e. ( A \ { B } ) |-> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ) = ( z e. ( A \ { B } ) |-> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) )
24 simp1 
 |-  ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> S C_ CC )
25 simp2 
 |-  ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> F : A --> CC )
26 simp3 
 |-  ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> A C_ S )
27 22 2 23 24 25 26 eldv 
 |-  ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> ( B ( S _D F ) y <-> ( B e. ( ( int ` ( K |`t S ) ) ` A ) /\ y e. ( ( z e. ( A \ { B } ) |-> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ) limCC B ) ) ) )
28 27 simprbda 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> B e. ( ( int ` ( K |`t S ) ) ` A ) )
29 21 28 sseldd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> B e. A )
30 3 29 ffvelcdmd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( F ` B ) e. CC )
31 30 adantr 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. A ) -> ( F ` B ) e. CC )
32 4 31 subcld 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. A ) -> ( ( F ` z ) - ( F ` B ) ) e. CC )
33 ssidd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> CC C_ CC )
34 txtopon 
 |-  ( ( K e. ( TopOn ` CC ) /\ K e. ( TopOn ` CC ) ) -> ( K tX K ) e. ( TopOn ` ( CC X. CC ) ) )
35 13 13 34 mp2an 
 |-  ( K tX K ) e. ( TopOn ` ( CC X. CC ) )
36 35 toponrestid 
 |-  ( K tX K ) = ( ( K tX K ) |`t ( CC X. CC ) )
37 12 6 sstrd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> A C_ CC )
38 eqid 
 |-  ( x e. ( A \ { B } ) |-> ( ( ( F ` x ) - ( F ` B ) ) / ( x - B ) ) ) = ( x e. ( A \ { B } ) |-> ( ( ( F ` x ) - ( F ` B ) ) / ( x - B ) ) )
39 22 2 38 24 25 26 eldv 
 |-  ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> ( B ( S _D F ) y <-> ( B e. ( ( int ` ( K |`t S ) ) ` A ) /\ y e. ( ( x e. ( A \ { B } ) |-> ( ( ( F ` x ) - ( F ` B ) ) / ( x - B ) ) ) limCC B ) ) ) )
40 39 simprbda 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> B e. ( ( int ` ( K |`t S ) ) ` A ) )
41 21 40 sseldd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> B e. A )
42 3 37 41 dvlem 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) e. CC )
43 37 ssdifssd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( A \ { B } ) C_ CC )
44 43 sselda 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> z e. CC )
45 37 41 sseldd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> B e. CC )
46 45 adantr 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> B e. CC )
47 44 46 subcld 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> ( z - B ) e. CC )
48 27 simplbda 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> y e. ( ( z e. ( A \ { B } ) |-> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ) limCC B ) )
49 limcresi 
 |-  ( ( z e. A |-> ( z - B ) ) limCC B ) C_ ( ( ( z e. A |-> ( z - B ) ) |` ( A \ { B } ) ) limCC B )
50 difss 
 |-  ( A \ { B } ) C_ A
51 resmpt 
 |-  ( ( A \ { B } ) C_ A -> ( ( z e. A |-> ( z - B ) ) |` ( A \ { B } ) ) = ( z e. ( A \ { B } ) |-> ( z - B ) ) )
52 50 51 ax-mp 
 |-  ( ( z e. A |-> ( z - B ) ) |` ( A \ { B } ) ) = ( z e. ( A \ { B } ) |-> ( z - B ) )
53 52 oveq1i 
 |-  ( ( ( z e. A |-> ( z - B ) ) |` ( A \ { B } ) ) limCC B ) = ( ( z e. ( A \ { B } ) |-> ( z - B ) ) limCC B )
54 49 53 sseqtri 
 |-  ( ( z e. A |-> ( z - B ) ) limCC B ) C_ ( ( z e. ( A \ { B } ) |-> ( z - B ) ) limCC B )
55 45 subidd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( B - B ) = 0 )
56 ssid 
 |-  CC C_ CC
57 cncfmptid 
 |-  ( ( A C_ CC /\ CC C_ CC ) -> ( z e. A |-> z ) e. ( A -cn-> CC ) )
58 37 56 57 sylancl 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( z e. A |-> z ) e. ( A -cn-> CC ) )
59 cncfmptc 
 |-  ( ( B e. CC /\ A C_ CC /\ CC C_ CC ) -> ( z e. A |-> B ) e. ( A -cn-> CC ) )
60 45 37 33 59 syl3anc 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( z e. A |-> B ) e. ( A -cn-> CC ) )
61 58 60 subcncf 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( z e. A |-> ( z - B ) ) e. ( A -cn-> CC ) )
62 oveq1 
 |-  ( z = B -> ( z - B ) = ( B - B ) )
63 61 41 62 cnmptlimc 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( B - B ) e. ( ( z e. A |-> ( z - B ) ) limCC B ) )
64 55 63 eqeltrrd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> 0 e. ( ( z e. A |-> ( z - B ) ) limCC B ) )
65 54 64 sselid 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> 0 e. ( ( z e. ( A \ { B } ) |-> ( z - B ) ) limCC B ) )
66 2 mpomulcn 
 |-  ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( K tX K ) Cn K )
67 24 25 26 dvcl 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> y e. CC )
68 0cn 
 |-  0 e. CC
69 opelxpi 
 |-  ( ( y e. CC /\ 0 e. CC ) -> <. y , 0 >. e. ( CC X. CC ) )
70 67 68 69 sylancl 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> <. y , 0 >. e. ( CC X. CC ) )
71 35 toponunii 
 |-  ( CC X. CC ) = U. ( K tX K )
72 71 cncnpi 
 |-  ( ( ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( K tX K ) Cn K ) /\ <. y , 0 >. e. ( CC X. CC ) ) -> ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( ( K tX K ) CnP K ) ` <. y , 0 >. ) )
73 66 70 72 sylancr 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( ( K tX K ) CnP K ) ` <. y , 0 >. ) )
74 42 47 33 33 2 36 48 65 73 limccnp2 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( y ( u e. CC , v e. CC |-> ( u x. v ) ) 0 ) e. ( ( z e. ( A \ { B } ) |-> ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( z - B ) ) ) limCC B ) )
75 df-mpt 
 |-  ( z e. ( A \ { B } ) |-> ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( z - B ) ) ) = { <. z , w >. | ( z e. ( A \ { B } ) /\ w = ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( z - B ) ) ) }
76 75 oveq1i 
 |-  ( ( z e. ( A \ { B } ) |-> ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( z - B ) ) ) limCC B ) = ( { <. z , w >. | ( z e. ( A \ { B } ) /\ w = ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( z - B ) ) ) } limCC B )
77 74 76 eleqtrdi 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( y ( u e. CC , v e. CC |-> ( u x. v ) ) 0 ) e. ( { <. z , w >. | ( z e. ( A \ { B } ) /\ w = ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( z - B ) ) ) } limCC B ) )
78 0cnd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> 0 e. CC )
79 ovmpot 
 |-  ( ( y e. CC /\ 0 e. CC ) -> ( y ( u e. CC , v e. CC |-> ( u x. v ) ) 0 ) = ( y x. 0 ) )
80 67 78 79 syl2anc 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( y ( u e. CC , v e. CC |-> ( u x. v ) ) 0 ) = ( y x. 0 ) )
81 3 37 29 dvlem 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) e. CC )
82 37 29 sseldd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> B e. CC )
83 82 adantr 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> B e. CC )
84 44 83 subcld 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> ( z - B ) e. CC )
85 ovmpot 
 |-  ( ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) e. CC /\ ( z - B ) e. CC ) -> ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( z - B ) ) = ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) x. ( z - B ) ) )
86 81 84 85 syl2anc 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( z - B ) ) = ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) x. ( z - B ) ) )
87 86 eqeq2d 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> ( w = ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( z - B ) ) <-> w = ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) x. ( z - B ) ) ) )
88 87 pm5.32da 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( ( z e. ( A \ { B } ) /\ w = ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( z - B ) ) ) <-> ( z e. ( A \ { B } ) /\ w = ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) x. ( z - B ) ) ) ) )
89 88 opabbidv 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> { <. z , w >. | ( z e. ( A \ { B } ) /\ w = ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( z - B ) ) ) } = { <. z , w >. | ( z e. ( A \ { B } ) /\ w = ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) x. ( z - B ) ) ) } )
90 df-mpt 
 |-  ( z e. ( A \ { B } ) |-> ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) x. ( z - B ) ) ) = { <. z , w >. | ( z e. ( A \ { B } ) /\ w = ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) x. ( z - B ) ) ) }
91 89 90 eqtr4di 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> { <. z , w >. | ( z e. ( A \ { B } ) /\ w = ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( z - B ) ) ) } = ( z e. ( A \ { B } ) |-> ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) x. ( z - B ) ) ) )
92 91 oveq1d 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( { <. z , w >. | ( z e. ( A \ { B } ) /\ w = ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( z - B ) ) ) } limCC B ) = ( ( z e. ( A \ { B } ) |-> ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) x. ( z - B ) ) ) limCC B ) )
93 77 80 92 3eltr3d 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( y x. 0 ) e. ( ( z e. ( A \ { B } ) |-> ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) x. ( z - B ) ) ) limCC B ) )
94 67 mul01d 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( y x. 0 ) = 0 )
95 3 adantr 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> F : A --> CC )
96 simpr 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> z e. ( A \ { B } ) )
97 50 96 sselid 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> z e. A )
98 95 97 ffvelcdmd 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> ( F ` z ) e. CC )
99 30 adantr 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> ( F ` B ) e. CC )
100 98 99 subcld 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> ( ( F ` z ) - ( F ` B ) ) e. CC )
101 eldifsni 
 |-  ( z e. ( A \ { B } ) -> z =/= B )
102 101 adantl 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> z =/= B )
103 44 83 102 subne0d 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> ( z - B ) =/= 0 )
104 100 84 103 divcan1d 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. ( A \ { B } ) ) -> ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) x. ( z - B ) ) = ( ( F ` z ) - ( F ` B ) ) )
105 104 mpteq2dva 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( z e. ( A \ { B } ) |-> ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) x. ( z - B ) ) ) = ( z e. ( A \ { B } ) |-> ( ( F ` z ) - ( F ` B ) ) ) )
106 105 oveq1d 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( ( z e. ( A \ { B } ) |-> ( ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) x. ( z - B ) ) ) limCC B ) = ( ( z e. ( A \ { B } ) |-> ( ( F ` z ) - ( F ` B ) ) ) limCC B ) )
107 93 94 106 3eltr3d 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> 0 e. ( ( z e. ( A \ { B } ) |-> ( ( F ` z ) - ( F ` B ) ) ) limCC B ) )
108 32 fmpttd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( z e. A |-> ( ( F ` z ) - ( F ` B ) ) ) : A --> CC )
109 108 limcdif 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( ( z e. A |-> ( ( F ` z ) - ( F ` B ) ) ) limCC B ) = ( ( ( z e. A |-> ( ( F ` z ) - ( F ` B ) ) ) |` ( A \ { B } ) ) limCC B ) )
110 resmpt 
 |-  ( ( A \ { B } ) C_ A -> ( ( z e. A |-> ( ( F ` z ) - ( F ` B ) ) ) |` ( A \ { B } ) ) = ( z e. ( A \ { B } ) |-> ( ( F ` z ) - ( F ` B ) ) ) )
111 50 110 ax-mp 
 |-  ( ( z e. A |-> ( ( F ` z ) - ( F ` B ) ) ) |` ( A \ { B } ) ) = ( z e. ( A \ { B } ) |-> ( ( F ` z ) - ( F ` B ) ) )
112 111 oveq1i 
 |-  ( ( ( z e. A |-> ( ( F ` z ) - ( F ` B ) ) ) |` ( A \ { B } ) ) limCC B ) = ( ( z e. ( A \ { B } ) |-> ( ( F ` z ) - ( F ` B ) ) ) limCC B )
113 109 112 eqtrdi 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( ( z e. A |-> ( ( F ` z ) - ( F ` B ) ) ) limCC B ) = ( ( z e. ( A \ { B } ) |-> ( ( F ` z ) - ( F ` B ) ) ) limCC B ) )
114 107 113 eleqtrrd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> 0 e. ( ( z e. A |-> ( ( F ` z ) - ( F ` B ) ) ) limCC B ) )
115 cncfmptc 
 |-  ( ( ( F ` B ) e. CC /\ A C_ CC /\ CC C_ CC ) -> ( z e. A |-> ( F ` B ) ) e. ( A -cn-> CC ) )
116 30 37 33 115 syl3anc 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( z e. A |-> ( F ` B ) ) e. ( A -cn-> CC ) )
117 eqidd 
 |-  ( z = B -> ( F ` B ) = ( F ` B ) )
118 116 29 117 cnmptlimc 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( F ` B ) e. ( ( z e. A |-> ( F ` B ) ) limCC B ) )
119 2 addcn 
 |-  + e. ( ( K tX K ) Cn K )
120 opelxpi 
 |-  ( ( 0 e. CC /\ ( F ` B ) e. CC ) -> <. 0 , ( F ` B ) >. e. ( CC X. CC ) )
121 68 30 120 sylancr 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> <. 0 , ( F ` B ) >. e. ( CC X. CC ) )
122 71 cncnpi 
 |-  ( ( + e. ( ( K tX K ) Cn K ) /\ <. 0 , ( F ` B ) >. e. ( CC X. CC ) ) -> + e. ( ( ( K tX K ) CnP K ) ` <. 0 , ( F ` B ) >. ) )
123 119 121 122 sylancr 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> + e. ( ( ( K tX K ) CnP K ) ` <. 0 , ( F ` B ) >. ) )
124 32 31 33 33 2 36 114 118 123 limccnp2 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( 0 + ( F ` B ) ) e. ( ( z e. A |-> ( ( ( F ` z ) - ( F ` B ) ) + ( F ` B ) ) ) limCC B ) )
125 30 addlidd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( 0 + ( F ` B ) ) = ( F ` B ) )
126 4 31 npcand 
 |-  ( ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) /\ z e. A ) -> ( ( ( F ` z ) - ( F ` B ) ) + ( F ` B ) ) = ( F ` z ) )
127 126 mpteq2dva 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( z e. A |-> ( ( ( F ` z ) - ( F ` B ) ) + ( F ` B ) ) ) = ( z e. A |-> ( F ` z ) ) )
128 3 feqmptd 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> F = ( z e. A |-> ( F ` z ) ) )
129 127 128 eqtr4d 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( z e. A |-> ( ( ( F ` z ) - ( F ` B ) ) + ( F ` B ) ) ) = F )
130 129 oveq1d 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( ( z e. A |-> ( ( ( F ` z ) - ( F ` B ) ) + ( F ` B ) ) ) limCC B ) = ( F limCC B ) )
131 124 125 130 3eltr3d 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( F ` B ) e. ( F limCC B ) )
132 2 1 cnplimc 
 |-  ( ( A C_ CC /\ B e. A ) -> ( F e. ( ( J CnP K ) ` B ) <-> ( F : A --> CC /\ ( F ` B ) e. ( F limCC B ) ) ) )
133 37 29 132 syl2anc 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> ( F e. ( ( J CnP K ) ` B ) <-> ( F : A --> CC /\ ( F ` B ) e. ( F limCC B ) ) ) )
134 3 131 133 mpbir2and 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B ( S _D F ) y ) -> F e. ( ( J CnP K ) ` B ) )
135 134 ex 
 |-  ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> ( B ( S _D F ) y -> F e. ( ( J CnP K ) ` B ) ) )
136 135 exlimdv 
 |-  ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> ( E. y B ( S _D F ) y -> F e. ( ( J CnP K ) ` B ) ) )
137 eldmg 
 |-  ( B e. dom ( S _D F ) -> ( B e. dom ( S _D F ) <-> E. y B ( S _D F ) y ) )
138 137 ibi 
 |-  ( B e. dom ( S _D F ) -> E. y B ( S _D F ) y )
139 136 138 impel 
 |-  ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B e. dom ( S _D F ) ) -> F e. ( ( J CnP K ) ` B ) )