MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lhop Unicode version

Theorem lhop 19357
Description: L'Hôpital's Rule. If  I is an open set of the reals,  F and  G are real functions on  A containing all of  I except possibly  B, which are differentiable everywhere on  I  \  { B },  F and  G both approach 0, and the limit of  F'  ( x )  /  G'  ( x ) at  B is  C, then the limit  F ( x )  /  G ( x ) at  B also exists and equals  C. (Contributed by Mario Carneiro, 30-Dec-2016.)
Hypotheses
Ref Expression
lhop.a  |-  ( ph  ->  A  C_  RR )
lhop.f  |-  ( ph  ->  F : A --> RR )
lhop.g  |-  ( ph  ->  G : A --> RR )
lhop.i  |-  ( ph  ->  I  e.  ( topGen ` 
ran  (,) ) )
lhop.b  |-  ( ph  ->  B  e.  I )
lhop.d  |-  D  =  ( I  \  { B } )
lhop.if  |-  ( ph  ->  D  C_  dom  ( RR 
_D  F ) )
lhop.ig  |-  ( ph  ->  D  C_  dom  ( RR 
_D  G ) )
lhop.f0  |-  ( ph  ->  0  e.  ( F lim
CC  B ) )
lhop.g0  |-  ( ph  ->  0  e.  ( G lim
CC  B ) )
lhop.gn0  |-  ( ph  ->  -.  0  e.  ( G " D ) )
lhop.gd0  |-  ( ph  ->  -.  0  e.  ( ( RR  _D  G
) " D ) )
lhop.c  |-  ( ph  ->  C  e.  ( ( z  e.  D  |->  ( ( ( RR  _D  F ) `  z
)  /  ( ( RR  _D  G ) `
 z ) ) ) lim CC  B ) )
Assertion
Ref Expression
lhop  |-  ( ph  ->  C  e.  ( ( z  e.  D  |->  ( ( F `  z
)  /  ( G `
 z ) ) ) lim CC  B ) )
Distinct variable groups:    z, B    z, C    z, D    z, F    ph, z    z, G   
z, I
Allowed substitution hint:    A( z)

Proof of Theorem lhop
StepHypRef Expression
1 eqid 2284 . . . . 5  |-  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )  =  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )
21rexmet 18291 . . . 4  |-  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )  e.  ( * Met `  RR )
32a1i 12 . . 3  |-  ( ph  ->  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) )  e.  ( * Met `  RR ) )
4 lhop.i . . 3  |-  ( ph  ->  I  e.  ( topGen ` 
ran  (,) ) )
5 lhop.b . . 3  |-  ( ph  ->  B  e.  I )
6 eqid 2284 . . . . 5  |-  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )  =  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )
71, 6tgioo 18296 . . . 4  |-  ( topGen ` 
ran  (,) )  =  (
MetOpen `  ( ( abs 
o.  -  )  |`  ( RR  X.  RR ) ) )
87mopni2 18033 . . 3  |-  ( ( ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) )  e.  ( * Met `  RR )  /\  I  e.  ( topGen `  ran  (,) )  /\  B  e.  I
)  ->  E. r  e.  RR+  ( B (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  I )
93, 4, 5, 8syl3anc 1187 . 2  |-  ( ph  ->  E. r  e.  RR+  ( B ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  I )
10 elssuni 3856 . . . . . . . . 9  |-  ( I  e.  ( topGen `  ran  (,) )  ->  I  C_  U. ( topGen `
 ran  (,) )
)
11 uniretop 18265 . . . . . . . . 9  |-  RR  =  U. ( topGen `  ran  (,) )
1210, 11syl6sseqr 3226 . . . . . . . 8  |-  ( I  e.  ( topGen `  ran  (,) )  ->  I  C_  RR )
134, 12syl 17 . . . . . . 7  |-  ( ph  ->  I  C_  RR )
1413, 5sseldd 3182 . . . . . 6  |-  ( ph  ->  B  e.  RR )
15 rpre 10355 . . . . . 6  |-  ( r  e.  RR+  ->  r  e.  RR )
161bl2ioo 18292 . . . . . 6  |-  ( ( B  e.  RR  /\  r  e.  RR )  ->  ( B ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) r )  =  ( ( B  -  r ) (,) ( B  +  r )
) )
1714, 15, 16syl2an 465 . . . . 5  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( B
( ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  =  ( ( B  -  r ) (,) ( B  +  r ) ) )
1817sseq1d 3206 . . . 4  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( ( B ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  I  <->  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I
) )
1914adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  B  e.  RR )
20 simprl 735 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
r  e.  RR+ )
2120rpred 10385 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
r  e.  RR )
2219, 21resubcld 9206 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B  -  r
)  e.  RR )
2322rexrd 8876 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B  -  r
)  e.  RR* )
2419, 20ltsubrpd 10413 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B  -  r
)  <  B )
25 lhop.f . . . . . . . . . . 11  |-  ( ph  ->  F : A --> RR )
2625adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  F : A --> RR )
27 ssun1 3339 . . . . . . . . . . . 12  |-  ( ( B  -  r ) (,) B )  C_  ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r ) ) )
28 unass 3333 . . . . . . . . . . . . . . 15  |-  ( ( { B }  u.  ( ( B  -  r ) (,) B
) )  u.  ( B (,) ( B  +  r ) ) )  =  ( { B }  u.  ( (
( B  -  r
) (,) B )  u.  ( B (,) ( B  +  r
) ) ) )
29 uncom 3320 . . . . . . . . . . . . . . . 16  |-  ( { B }  u.  (
( B  -  r
) (,) B ) )  =  ( ( ( B  -  r
) (,) B )  u.  { B }
)
3029uneq1i 3326 . . . . . . . . . . . . . . 15  |-  ( ( { B }  u.  ( ( B  -  r ) (,) B
) )  u.  ( B (,) ( B  +  r ) ) )  =  ( ( ( ( B  -  r
) (,) B )  u.  { B }
)  u.  ( B (,) ( B  +  r ) ) )
3128, 30eqtr3i 2306 . . . . . . . . . . . . . 14  |-  ( { B }  u.  (
( ( B  -  r ) (,) B
)  u.  ( B (,) ( B  +  r ) ) ) )  =  ( ( ( ( B  -  r ) (,) B
)  u.  { B } )  u.  ( B (,) ( B  +  r ) ) )
3219rexrd 8876 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  B  e.  RR* )
3319, 21readdcld 8857 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B  +  r )  e.  RR )
3433rexrd 8876 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B  +  r )  e.  RR* )
3519, 20ltaddrpd 10414 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  B  <  ( B  +  r ) )
36 ioojoin 10760 . . . . . . . . . . . . . . 15  |-  ( ( ( ( B  -  r )  e.  RR*  /\  B  e.  RR*  /\  ( B  +  r )  e.  RR* )  /\  (
( B  -  r
)  <  B  /\  B  <  ( B  +  r ) ) )  ->  ( ( ( ( B  -  r
) (,) B )  u.  { B }
)  u.  ( B (,) ( B  +  r ) ) )  =  ( ( B  -  r ) (,) ( B  +  r ) ) )
3723, 32, 34, 24, 35, 36syl32anc 1195 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( ( ( B  -  r ) (,) B )  u. 
{ B } )  u.  ( B (,) ( B  +  r
) ) )  =  ( ( B  -  r ) (,) ( B  +  r )
) )
3831, 37syl5eq 2328 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( { B }  u.  ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r ) ) ) )  =  ( ( B  -  r ) (,) ( B  +  r ) ) )
39 elioo2 10691 . . . . . . . . . . . . . . . . 17  |-  ( ( ( B  -  r
)  e.  RR*  /\  ( B  +  r )  e.  RR* )  ->  ( B  e.  ( ( B  -  r ) (,) ( B  +  r ) )  <->  ( B  e.  RR  /\  ( B  -  r )  < 
B  /\  B  <  ( B  +  r ) ) ) )
4023, 34, 39syl2anc 645 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B  e.  ( ( B  -  r
) (,) ( B  +  r ) )  <-> 
( B  e.  RR  /\  ( B  -  r
)  <  B  /\  B  <  ( B  +  r ) ) ) )
4119, 24, 35, 40mpbir3and 1140 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  B  e.  ( ( B  -  r ) (,) ( B  +  r ) ) )
4241snssd 3761 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  { B }  C_  (
( B  -  r
) (,) ( B  +  r ) ) )
43 incom 3362 . . . . . . . . . . . . . . 15  |-  ( { B }  i^i  (
( ( B  -  r ) (,) B
)  u.  ( B (,) ( B  +  r ) ) ) )  =  ( ( ( ( B  -  r ) (,) B
)  u.  ( B (,) ( B  +  r ) ) )  i^i  { B }
)
44 ubioo 10682 . . . . . . . . . . . . . . . . . 18  |-  -.  B  e.  ( ( B  -  r ) (,) B
)
45 lbioo 10681 . . . . . . . . . . . . . . . . . 18  |-  -.  B  e.  ( B (,) ( B  +  r )
)
4644, 45pm3.2ni 830 . . . . . . . . . . . . . . . . 17  |-  -.  ( B  e.  ( ( B  -  r ) (,) B )  \/  B  e.  ( B (,) ( B  +  r )
) )
47 elun 3317 . . . . . . . . . . . . . . . . 17  |-  ( B  e.  ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r )
) )  <->  ( B  e.  ( ( B  -  r ) (,) B
)  \/  B  e.  ( B (,) ( B  +  r )
) ) )
4846, 47mtbir 292 . . . . . . . . . . . . . . . 16  |-  -.  B  e.  ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r ) ) )
49 disjsn 3694 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r ) ) )  i^i  { B }
)  =  (/)  <->  -.  B  e.  ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r ) ) ) )
5048, 49mpbir 202 . . . . . . . . . . . . . . 15  |-  ( ( ( ( B  -  r ) (,) B
)  u.  ( B (,) ( B  +  r ) ) )  i^i  { B }
)  =  (/)
5143, 50eqtri 2304 . . . . . . . . . . . . . 14  |-  ( { B }  i^i  (
( ( B  -  r ) (,) B
)  u.  ( B (,) ( B  +  r ) ) ) )  =  (/)
52 uneqdifeq 3543 . . . . . . . . . . . . . 14  |-  ( ( { B }  C_  ( ( B  -  r ) (,) ( B  +  r )
)  /\  ( { B }  i^i  (
( ( B  -  r ) (,) B
)  u.  ( B (,) ( B  +  r ) ) ) )  =  (/) )  -> 
( ( { B }  u.  ( (
( B  -  r
) (,) B )  u.  ( B (,) ( B  +  r
) ) ) )  =  ( ( B  -  r ) (,) ( B  +  r ) )  <->  ( (
( B  -  r
) (,) ( B  +  r ) ) 
\  { B }
)  =  ( ( ( B  -  r
) (,) B )  u.  ( B (,) ( B  +  r
) ) ) ) )
5342, 51, 52sylancl 646 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( { B }  u.  ( (
( B  -  r
) (,) B )  u.  ( B (,) ( B  +  r
) ) ) )  =  ( ( B  -  r ) (,) ( B  +  r ) )  <->  ( (
( B  -  r
) (,) ( B  +  r ) ) 
\  { B }
)  =  ( ( ( B  -  r
) (,) B )  u.  ( B (,) ( B  +  r
) ) ) ) )
5438, 53mpbid 203 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  =  ( ( ( B  -  r ) (,) B
)  u.  ( B (,) ( B  +  r ) ) ) )
5527, 54syl5sseqr 3228 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  ( (
( B  -  r
) (,) ( B  +  r ) ) 
\  { B }
) )
56 ssdif 3312 . . . . . . . . . . . . . 14  |-  ( ( ( B  -  r
) (,) ( B  +  r ) ) 
C_  I  ->  (
( ( B  -  r ) (,) ( B  +  r )
)  \  { B } )  C_  (
I  \  { B } ) )
5756ad2antll 712 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  C_  (
I  \  { B } ) )
58 lhop.d . . . . . . . . . . . . 13  |-  D  =  ( I  \  { B } )
5957, 58syl6sseqr 3226 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  C_  D
)
60 lhop.if . . . . . . . . . . . . . 14  |-  ( ph  ->  D  C_  dom  ( RR 
_D  F ) )
61 ax-resscn 8789 . . . . . . . . . . . . . . . 16  |-  RR  C_  CC
6261a1i 12 . . . . . . . . . . . . . . 15  |-  ( ph  ->  RR  C_  CC )
63 fss 5362 . . . . . . . . . . . . . . . 16  |-  ( ( F : A --> RR  /\  RR  C_  CC )  ->  F : A --> CC )
6425, 61, 63sylancl 646 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F : A --> CC )
65 lhop.a . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  C_  RR )
6662, 64, 65dvbss 19245 . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  ( RR  _D  F )  C_  A
)
6760, 66sstrd 3190 . . . . . . . . . . . . 13  |-  ( ph  ->  D  C_  A )
6867adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  D  C_  A )
6959, 68sstrd 3190 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  C_  A
)
7055, 69sstrd 3190 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  A )
71 fssres 5373 . . . . . . . . . 10  |-  ( ( F : A --> RR  /\  ( ( B  -  r ) (,) B
)  C_  A )  ->  ( F  |`  (
( B  -  r
) (,) B ) ) : ( ( B  -  r ) (,) B ) --> RR )
7226, 70, 71syl2anc 645 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( F  |`  (
( B  -  r
) (,) B ) ) : ( ( B  -  r ) (,) B ) --> RR )
73 lhop.g . . . . . . . . . . 11  |-  ( ph  ->  G : A --> RR )
7473adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  G : A --> RR )
75 fssres 5373 . . . . . . . . . 10  |-  ( ( G : A --> RR  /\  ( ( B  -  r ) (,) B
)  C_  A )  ->  ( G  |`  (
( B  -  r
) (,) B ) ) : ( ( B  -  r ) (,) B ) --> RR )
7674, 70, 75syl2anc 645 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( G  |`  (
( B  -  r
) (,) B ) ) : ( ( B  -  r ) (,) B ) --> RR )
7761a1i 12 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  RR  C_  CC )
7864adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  F : A --> CC )
7965adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  A  C_  RR )
80 ioossre 10706 . . . . . . . . . . . . . 14  |-  ( ( B  -  r ) (,) B )  C_  RR
8180a1i 12 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  RR )
82 eqid 2284 . . . . . . . . . . . . . 14  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
8382tgioo2 18303 . . . . . . . . . . . . . 14  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
8482, 83dvres 19255 . . . . . . . . . . . . 13  |-  ( ( ( RR  C_  CC  /\  F : A --> CC )  /\  ( A  C_  RR  /\  ( ( B  -  r ) (,) B )  C_  RR ) )  ->  ( RR  _D  ( F  |`  ( ( B  -  r ) (,) B
) ) )  =  ( ( RR  _D  F )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( ( B  -  r ) (,) B ) ) ) )
8577, 78, 79, 81, 84syl22anc 1188 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( RR  _D  ( F  |`  ( ( B  -  r ) (,) B ) ) )  =  ( ( RR 
_D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( B  -  r ) (,) B ) ) ) )
86 retop 18264 . . . . . . . . . . . . . 14  |-  ( topGen ` 
ran  (,) )  e.  Top
87 iooretop 18269 . . . . . . . . . . . . . 14  |-  ( ( B  -  r ) (,) B )  e.  ( topGen `  ran  (,) )
88 isopn3i 16813 . . . . . . . . . . . . . 14  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( ( B  -  r ) (,) B )  e.  ( topGen `  ran  (,) )
)  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  (
( B  -  r
) (,) B ) )  =  ( ( B  -  r ) (,) B ) )
8986, 87, 88mp2an 656 . . . . . . . . . . . . 13  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( ( B  -  r ) (,) B
) )  =  ( ( B  -  r
) (,) B )
9089reseq2i 4951 . . . . . . . . . . . 12  |-  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( B  -  r ) (,) B ) ) )  =  ( ( RR 
_D  F )  |`  ( ( B  -  r ) (,) B
) )
9185, 90syl6eq 2332 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( RR  _D  ( F  |`  ( ( B  -  r ) (,) B ) ) )  =  ( ( RR 
_D  F )  |`  ( ( B  -  r ) (,) B
) ) )
9291dmeqd 4880 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( RR  _D  ( F  |`  ( ( B  -  r ) (,) B ) ) )  =  dom  ( ( RR  _D  F )  |`  ( ( B  -  r ) (,) B
) ) )
9355, 59sstrd 3190 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  D )
9460adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  D  C_  dom  ( RR 
_D  F ) )
9593, 94sstrd 3190 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  dom  ( RR 
_D  F ) )
96 ssdmres 4976 . . . . . . . . . . 11  |-  ( ( ( B  -  r
) (,) B ) 
C_  dom  ( RR  _D  F )  <->  dom  ( ( RR  _D  F )  |`  ( ( B  -  r ) (,) B
) )  =  ( ( B  -  r
) (,) B ) )
9795, 96sylib 190 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( ( RR  _D  F )  |`  (
( B  -  r
) (,) B ) )  =  ( ( B  -  r ) (,) B ) )
9892, 97eqtrd 2316 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( RR  _D  ( F  |`  ( ( B  -  r ) (,) B ) ) )  =  ( ( B  -  r ) (,) B ) )
99 fss 5362 . . . . . . . . . . . . . . 15  |-  ( ( G : A --> RR  /\  RR  C_  CC )  ->  G : A --> CC )
10073, 61, 99sylancl 646 . . . . . . . . . . . . . 14  |-  ( ph  ->  G : A --> CC )
101100adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  G : A --> CC )
10282, 83dvres 19255 . . . . . . . . . . . . 13  |-  ( ( ( RR  C_  CC  /\  G : A --> CC )  /\  ( A  C_  RR  /\  ( ( B  -  r ) (,) B )  C_  RR ) )  ->  ( RR  _D  ( G  |`  ( ( B  -  r ) (,) B
) ) )  =  ( ( RR  _D  G )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( ( B  -  r ) (,) B ) ) ) )
10377, 101, 79, 81, 102syl22anc 1188 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) )  =  ( ( RR 
_D  G )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( B  -  r ) (,) B ) ) ) )
10489reseq2i 4951 . . . . . . . . . . . 12  |-  ( ( RR  _D  G )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( B  -  r ) (,) B ) ) )  =  ( ( RR 
_D  G )  |`  ( ( B  -  r ) (,) B
) )
105103, 104syl6eq 2332 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) )  =  ( ( RR 
_D  G )  |`  ( ( B  -  r ) (,) B
) ) )
106105dmeqd 4880 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) )  =  dom  ( ( RR  _D  G )  |`  ( ( B  -  r ) (,) B
) ) )
107 lhop.ig . . . . . . . . . . . . 13  |-  ( ph  ->  D  C_  dom  ( RR 
_D  G ) )
108107adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  D  C_  dom  ( RR 
_D  G ) )
10993, 108sstrd 3190 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  dom  ( RR 
_D  G ) )
110 ssdmres 4976 . . . . . . . . . . 11  |-  ( ( ( B  -  r
) (,) B ) 
C_  dom  ( RR  _D  G )  <->  dom  ( ( RR  _D  G )  |`  ( ( B  -  r ) (,) B
) )  =  ( ( B  -  r
) (,) B ) )
111109, 110sylib 190 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( ( RR  _D  G )  |`  (
( B  -  r
) (,) B ) )  =  ( ( B  -  r ) (,) B ) )
112106, 111eqtrd 2316 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) )  =  ( ( B  -  r ) (,) B ) )
113 limcresi 19229 . . . . . . . . . 10  |-  ( F lim
CC  B )  C_  ( ( F  |`  ( ( B  -  r ) (,) B
) ) lim CC  B
)
114 lhop.f0 . . . . . . . . . . 11  |-  ( ph  ->  0  e.  ( F lim
CC  B ) )
115114adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( F lim
CC  B ) )
116113, 115sseldi 3179 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( ( F  |`  ( ( B  -  r ) (,) B ) ) lim CC  B ) )
117 limcresi 19229 . . . . . . . . . 10  |-  ( G lim
CC  B )  C_  ( ( G  |`  ( ( B  -  r ) (,) B
) ) lim CC  B
)
118 lhop.g0 . . . . . . . . . . 11  |-  ( ph  ->  0  e.  ( G lim
CC  B ) )
119118adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( G lim
CC  B ) )
120117, 119sseldi 3179 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( ( G  |`  ( ( B  -  r ) (,) B ) ) lim CC  B ) )
121 lhop.gn0 . . . . . . . . . . 11  |-  ( ph  ->  -.  0  e.  ( G " D ) )
122121adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  ( G " D ) )
123 df-ima 4701 . . . . . . . . . . . 12  |-  ( G
" ( ( B  -  r ) (,) B ) )  =  ran  (  G  |`  ( ( B  -  r ) (,) B
) )
124 imass2 5048 . . . . . . . . . . . . 13  |-  ( ( ( B  -  r
) (,) B ) 
C_  D  ->  ( G " ( ( B  -  r ) (,) B ) )  C_  ( G " D ) )
12593, 124syl 17 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( G " (
( B  -  r
) (,) B ) )  C_  ( G " D ) )
126123, 125syl5eqssr 3224 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  ran  (  G  |`  (
( B  -  r
) (,) B ) )  C_  ( G " D ) )
127126sseld 3180 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( 0  e.  ran  (  G  |`  ( ( B  -  r ) (,) B ) )  ->  0  e.  ( G " D ) ) )
128122, 127mtod 170 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  ran  (  G  |`  ( ( B  -  r ) (,) B ) ) )
129 lhop.gd0 . . . . . . . . . . 11  |-  ( ph  ->  -.  0  e.  ( ( RR  _D  G
) " D ) )
130129adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  (
( RR  _D  G
) " D ) )
131105rneqd 4905 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  ran  ( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) )  =  ran  ( ( RR  _D  G )  |`  ( ( B  -  r ) (,) B
) ) )
132 df-ima 4701 . . . . . . . . . . . . 13  |-  ( ( RR  _D  G )
" ( ( B  -  r ) (,) B ) )  =  ran  ( ( RR 
_D  G )  |`  ( ( B  -  r ) (,) B
) )
133131, 132syl6eqr 2334 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  ran  ( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) )  =  ( ( RR 
_D  G ) "
( ( B  -  r ) (,) B
) ) )
134 imass2 5048 . . . . . . . . . . . . 13  |-  ( ( ( B  -  r
) (,) B ) 
C_  D  ->  (
( RR  _D  G
) " ( ( B  -  r ) (,) B ) ) 
C_  ( ( RR 
_D  G ) " D ) )
13593, 134syl 17 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( RR  _D  G ) " (
( B  -  r
) (,) B ) )  C_  ( ( RR  _D  G ) " D ) )
136133, 135eqsstrd 3213 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  ran  ( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) ) 
C_  ( ( RR 
_D  G ) " D ) )
137136sseld 3180 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( 0  e.  ran  ( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) )  ->  0  e.  ( ( RR  _D  G
) " D ) ) )
138130, 137mtod 170 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  ran  ( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) ) )
139 limcresi 19229 . . . . . . . . . . 11  |-  ( ( z  e.  D  |->  ( ( ( RR  _D  F ) `  z
)  /  ( ( RR  _D  G ) `
 z ) ) ) lim CC  B ) 
C_  ( ( ( z  e.  D  |->  ( ( ( RR  _D  F ) `  z
)  /  ( ( RR  _D  G ) `
 z ) ) )  |`  ( ( B  -  r ) (,) B ) ) lim CC  B )
140 resmpt 4999 . . . . . . . . . . . . . 14  |-  ( ( ( B  -  r
) (,) B ) 
C_  D  ->  (
( z  e.  D  |->  ( ( ( RR 
_D  F ) `  z )  /  (
( RR  _D  G
) `  z )
) )  |`  (
( B  -  r
) (,) B ) )  =  ( z  e.  ( ( B  -  r ) (,) B )  |->  ( ( ( RR  _D  F
) `  z )  /  ( ( RR 
_D  G ) `  z ) ) ) )
14193, 140syl 17 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( z  e.  D  |->  ( ( ( RR  _D  F ) `
 z )  / 
( ( RR  _D  G ) `  z
) ) )  |`  ( ( B  -  r ) (,) B
) )  =  ( z  e.  ( ( B  -  r ) (,) B )  |->  ( ( ( RR  _D  F ) `  z
)  /  ( ( RR  _D  G ) `
 z ) ) ) )
14291fveq1d 5487 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( RR  _D  ( F  |`  ( ( B  -  r ) (,) B ) ) ) `  z )  =  ( ( ( RR  _D  F )  |`  ( ( B  -  r ) (,) B
) ) `  z
) )
143 fvres 5502 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( ( B  -  r ) (,) B )  ->  (
( ( RR  _D  F )  |`  (
( B  -  r
) (,) B ) ) `  z )  =  ( ( RR 
_D  F ) `  z ) )
144142, 143sylan9eq 2336 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  (
( B  -  r
) (,) ( B  +  r ) ) 
C_  I ) )  /\  z  e.  ( ( B  -  r
) (,) B ) )  ->  ( ( RR  _D  ( F  |`  ( ( B  -  r ) (,) B
) ) ) `  z )  =  ( ( RR  _D  F
) `  z )
)
145105fveq1d 5487 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) ) `  z )  =  ( ( ( RR  _D  G )  |`  ( ( B  -  r ) (,) B
) ) `  z
) )
146 fvres 5502 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( ( B  -  r ) (,) B )  ->  (
( ( RR  _D  G )  |`  (
( B  -  r
) (,) B ) ) `  z )  =  ( ( RR 
_D  G ) `  z ) )
147145, 146sylan9eq 2336 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  (
( B  -  r
) (,) ( B  +  r ) ) 
C_  I ) )  /\  z  e.  ( ( B  -  r
) (,) B ) )  ->  ( ( RR  _D  ( G  |`  ( ( B  -  r ) (,) B
) ) ) `  z )  =  ( ( RR  _D  G
) `  z )
)
148144, 147oveq12d 5837 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  (
( B  -  r
) (,) ( B  +  r ) ) 
C_  I ) )  /\  z  e.  ( ( B  -  r
) (,) B ) )  ->  ( (
( RR  _D  ( F  |`  ( ( B  -  r ) (,) B ) ) ) `
 z )  / 
( ( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) ) `  z ) )  =  ( ( ( RR  _D  F
) `  z )  /  ( ( RR 
_D  G ) `  z ) ) )
149148mpteq2dva 4107 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( z  e.  ( ( B  -  r
) (,) B ) 
|->  ( ( ( RR 
_D  ( F  |`  ( ( B  -  r ) (,) B
) ) ) `  z )  /  (
( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) ) `
 z ) ) )  =  ( z  e.  ( ( B  -  r ) (,) B )  |->  ( ( ( RR  _D  F
) `  z )  /  ( ( RR 
_D  G ) `  z ) ) ) )
150141, 149eqtr4d 2319 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( z  e.  D  |->  ( ( ( RR  _D  F ) `
 z )  / 
( ( RR  _D  G ) `  z
) ) )  |`  ( ( B  -  r ) (,) B
) )  =  ( z  e.  ( ( B  -  r ) (,) B )  |->  ( ( ( RR  _D  ( F  |`  ( ( B  -  r ) (,) B ) ) ) `  z )  /  ( ( RR 
_D  ( G  |`  ( ( B  -  r ) (,) B
) ) ) `  z ) ) ) )
151150oveq1d 5834 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( ( z  e.  D  |->  ( ( ( RR  _D  F
) `  z )  /  ( ( RR 
_D  G ) `  z ) ) )  |`  ( ( B  -  r ) (,) B
) ) lim CC  B
)  =  ( ( z  e.  ( ( B  -  r ) (,) B )  |->  ( ( ( RR  _D  ( F  |`  ( ( B  -  r ) (,) B ) ) ) `  z )  /  ( ( RR 
_D  ( G  |`  ( ( B  -  r ) (,) B
) ) ) `  z ) ) ) lim
CC  B ) )
152139, 151syl5sseq 3227 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( z  e.  D  |->  ( ( ( RR  _D  F ) `
 z )  / 
( ( RR  _D  G ) `  z
) ) ) lim CC  B )  C_  (
( z  e.  ( ( B  -  r
) (,) B ) 
|->  ( ( ( RR 
_D  ( F  |`  ( ( B  -  r ) (,) B
) ) ) `  z )  /  (
( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) ) `
 z ) ) ) lim CC  B ) )
153 lhop.c . . . . . . . . . . 11  |-  ( ph  ->  C  e.  ( ( z  e.  D  |->  ( ( ( RR  _D  F ) `  z
)  /  ( ( RR  _D  G ) `
 z ) ) ) lim CC  B ) )
154153adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  C  e.  ( (
z  e.  D  |->  ( ( ( RR  _D  F ) `  z
)  /  ( ( RR  _D  G ) `
 z ) ) ) lim CC  B ) )
155152, 154sseldd 3182 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  C  e.  ( (
z  e.  ( ( B  -  r ) (,) B )  |->  ( ( ( RR  _D  ( F  |`  ( ( B  -  r ) (,) B ) ) ) `  z )  /  ( ( RR 
_D  ( G  |`  ( ( B  -  r ) (,) B
) ) ) `  z ) ) ) lim
CC  B ) )
15623, 19, 24, 72, 76, 98, 112, 116, 120, 128, 138, 155lhop2 19356 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  C  e.  ( (
z  e.  ( ( B  -  r ) (,) B )  |->  ( ( ( F  |`  ( ( B  -  r ) (,) B
) ) `  z
)  /  ( ( G  |`  ( ( B  -  r ) (,) B ) ) `  z ) ) ) lim
CC  B ) )
157 resmpt 4999 . . . . . . . . . . 11  |-  ( ( ( B  -  r
) (,) B ) 
C_  ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  -> 
( ( z  e.  ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  |->  ( ( F `  z )  /  ( G `  z ) ) )  |`  ( ( B  -  r ) (,) B
) )  =  ( z  e.  ( ( B  -  r ) (,) B )  |->  ( ( F `  z
)  /  ( G `
 z ) ) ) )
15855, 157syl 17 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( z  e.  ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  |->  ( ( F `  z )  /  ( G `  z ) ) )  |`  ( ( B  -  r ) (,) B
) )  =  ( z  e.  ( ( B  -  r ) (,) B )  |->  ( ( F `  z
)  /  ( G `
 z ) ) ) )
159 fvres 5502 . . . . . . . . . . . 12  |-  ( z  e.  ( ( B  -  r ) (,) B )  ->  (
( F  |`  (
( B  -  r
) (,) B ) ) `  z )  =  ( F `  z ) )
160 fvres 5502 . . . . . . . . . . . 12  |-  ( z  e.  ( ( B  -  r ) (,) B )  ->  (
( G  |`  (
( B  -  r
) (,) B ) ) `  z )  =  ( G `  z ) )
161159, 160oveq12d 5837 . . . . . . . . . . 11  |-  ( z  e.  ( ( B  -  r ) (,) B )  ->  (
( ( F  |`  ( ( B  -  r ) (,) B
) ) `  z
)  /  ( ( G  |`  ( ( B  -  r ) (,) B ) ) `  z ) )  =  ( ( F `  z )  /  ( G `  z )
) )
162161mpteq2ia 4103 . . . . . . . . . 10  |-  ( z  e.  ( ( B  -  r ) (,) B )  |->  ( ( ( F  |`  (
( B  -  r
) (,) B ) ) `  z )  /  ( ( G  |`  ( ( B  -  r ) (,) B
) ) `  z
) ) )  =  ( z  e.  ( ( B  -  r
) (,) B ) 
|->  ( ( F `  z )  /  ( G `  z )
) )
163158, 162syl6eqr 2334 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( z  e.  ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  |->  ( ( F `  z )  /  ( G `  z ) ) )  |`  ( ( B  -  r ) (,) B
) )  =  ( z  e.  ( ( B  -  r ) (,) B )  |->  ( ( ( F  |`  ( ( B  -  r ) (,) B
) ) `  z
)  /  ( ( G  |`  ( ( B  -  r ) (,) B ) ) `  z ) ) ) )
164163oveq1d 5834 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( ( z  e.  ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  |->  ( ( F `  z
)  /  ( G `
 z ) ) )  |`  ( ( B  -  r ) (,) B ) ) lim CC  B )  =  ( ( z  e.  ( ( B  -  r
) (,) B ) 
|->  ( ( ( F  |`  ( ( B  -  r ) (,) B
) ) `  z
)  /  ( ( G  |`  ( ( B  -  r ) (,) B ) ) `  z ) ) ) lim
CC  B ) )
165156, 164eleqtrrd 2361 . . . . . . 7  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  C  e.  ( (
( z  e.  ( ( ( B  -  r ) (,) ( B  +  r )
)  \  { B } )  |->  ( ( F `  z )  /  ( G `  z ) ) )  |`  ( ( B  -  r ) (,) B
) ) lim CC  B
) )
166 ssun2 3340 . . . . . . . . . . . 12  |-  ( B (,) ( B  +  r ) )  C_  ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r ) ) )
167166, 54syl5sseqr 3228 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  ( (
( B  -  r
) (,) ( B  +  r ) ) 
\  { B }
) )
168167, 69sstrd 3190 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  A )
169 fssres 5373 . . . . . . . . . 10  |-  ( ( F : A --> RR  /\  ( B (,) ( B  +  r ) ) 
C_  A )  -> 
( F  |`  ( B (,) ( B  +  r ) ) ) : ( B (,) ( B  +  r
) ) --> RR )
17026, 168, 169syl2anc 645 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( F  |`  ( B (,) ( B  +  r ) ) ) : ( B (,) ( B  +  r
) ) --> RR )
171 fssres 5373 . . . . . . . . . 10  |-  ( ( G : A --> RR  /\  ( B (,) ( B  +  r ) ) 
C_  A )  -> 
( G  |`  ( B (,) ( B  +  r ) ) ) : ( B (,) ( B  +  r
) ) --> RR )
17274, 168, 171syl2anc 645 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( G  |`  ( B (,) ( B  +  r ) ) ) : ( B (,) ( B  +  r
) ) --> RR )
173 ioossre 10706 . . . . . . . . . . . . . 14  |-  ( B (,) ( B  +  r ) )  C_  RR
174173a1i 12 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  RR )
17582, 83dvres 19255 . . . . . . . . . . . . 13  |-  ( ( ( RR  C_  CC  /\  F : A --> CC )  /\  ( A  C_  RR  /\  ( B (,) ( B  +  r
) )  C_  RR ) )  ->  ( RR  _D  ( F  |`  ( B (,) ( B  +  r ) ) ) )  =  ( ( RR  _D  F
)  |`  ( ( int `  ( topGen `  ran  (,) )
) `  ( B (,) ( B  +  r ) ) ) ) )
17677, 78, 79, 174, 175syl22anc 1188 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( RR  _D  ( F  |`  ( B (,) ( B  +  r
) ) ) )  =  ( ( RR 
_D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( B (,) ( B  +  r ) ) ) ) )
177 iooretop 18269 . . . . . . . . . . . . . 14  |-  ( B (,) ( B  +  r ) )  e.  ( topGen `  ran  (,) )
178 isopn3i 16813 . . . . . . . . . . . . . 14  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( B (,) ( B  +  r ) )  e.  ( topGen `  ran  (,) )
)  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  ( B (,) ( B  +  r ) ) )  =  ( B (,) ( B  +  r
) ) )
17986, 177, 178mp2an 656 . . . . . . . . . . . . 13  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( B (,) ( B  +  r ) ) )  =  ( B (,) ( B  +  r ) )
180179reseq2i 4951 . . . . . . . . . . . 12  |-  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( B (,) ( B  +  r ) ) ) )  =  ( ( RR 
_D  F )  |`  ( B (,) ( B  +  r ) ) )
181176, 180syl6eq 2332 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( RR  _D  ( F  |`  ( B (,) ( B  +  r
) ) ) )  =  ( ( RR 
_D  F )  |`  ( B (,) ( B  +  r ) ) ) )
182181dmeqd 4880 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( RR  _D  ( F  |`  ( B (,) ( B  +  r
) ) ) )  =  dom  ( ( RR  _D  F )  |`  ( B (,) ( B  +  r )
) ) )
183167, 59sstrd 3190 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  D )
184183, 94sstrd 3190 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  dom  ( RR 
_D  F ) )
185 ssdmres 4976 . . . . . . . . . . 11  |-  ( ( B (,) ( B  +  r ) ) 
C_  dom  ( RR  _D  F )  <->  dom  ( ( RR  _D  F )  |`  ( B (,) ( B  +  r )
) )  =  ( B (,) ( B  +  r ) ) )
186184, 185sylib 190 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( ( RR  _D  F )  |`  ( B (,) ( B  +  r ) ) )  =  ( B (,) ( B  +  r
) ) )
187182, 186eqtrd 2316 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( RR  _D  ( F  |`  ( B (,) ( B  +  r
) ) ) )  =  ( B (,) ( B  +  r
) ) )
18882, 83dvres 19255 . . . . . . . . . . . . 13  |-  ( ( ( RR  C_  CC  /\  G : A --> CC )  /\  ( A  C_  RR  /\  ( B (,) ( B  +  r
) )  C_  RR ) )  ->  ( RR  _D  ( G  |`  ( B (,) ( B  +  r ) ) ) )  =  ( ( RR  _D  G
)  |`  ( ( int `  ( topGen `  ran  (,) )
) `  ( B (,) ( B  +  r ) ) ) ) )
18977, 101, 79, 174, 188syl22anc 1188 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( RR  _D  ( G  |`  ( B (,) ( B  +  r
) ) ) )  =  ( ( RR 
_D  G )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( B (,) ( B  +  r ) ) ) ) )
190179reseq2i 4951 . . . . . . . . . . . 12  |-  ( ( RR  _D  G )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( B (,) ( B  +  r ) ) ) )  =  ( ( RR 
_D  G )  |`  ( B (,) ( B  +  r ) ) )
191189, 190syl6eq 2332 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( RR  _D  ( G  |`  ( B (,) ( B  +  r
) ) ) )  =  ( ( RR 
_D  G )  |`  ( B (,) ( B  +  r ) ) ) )
192191dmeqd 4880 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( RR  _D  ( G  |`  ( B (,) ( B  +  r
) ) ) )  =  dom  ( ( RR  _D  G )  |`  ( B (,) ( B  +  r )
) ) )
193183, 108sstrd 3190 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  dom  ( RR 
_D  G ) )
194 ssdmres 4976 . . . . . . . . . . 11  |-  ( ( B (,) ( B  +  r ) ) 
C_  dom  ( RR  _D  G )  <->  dom  ( ( RR  _D  G )  |`  ( B (,) ( B  +  r )
) )  =  ( B (,) ( B  +  r ) ) )
195193, 194sylib 190 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( ( RR  _D  G )  |`  ( B (,) ( B  +  r ) ) )  =  ( B (,) ( B  +  r
) ) )
196192, 195eqtrd 2316 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( RR  _D  ( G  |`  ( B (,) ( B  +  r
) ) ) )  =  ( B (,) ( B  +  r
) ) )
197 limcresi 19229 . . . . . . . . . 10  |-  ( F lim
CC  B )  C_  ( ( F  |`  ( B (,) ( B  +  r ) ) ) lim CC  B )
198197, 115sseldi 3179 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( ( F  |`  ( B (,) ( B  +  r ) ) ) lim CC  B ) )
199 limcresi 19229 . . . . . . . . . 10  |-  ( G lim
CC  B )  C_  ( ( G  |`  ( B (,) ( B  +  r ) ) ) lim CC  B )
200199, 119sseldi 3179 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( ( G  |`  ( B (,) ( B  +  r ) ) ) lim CC  B ) )
201 df-ima 4701 . . . . . . . . . . . 12  |-  ( G
" ( B (,) ( B  +  r
) ) )  =  ran  (  G  |`  ( B (,) ( B  +  r ) ) )
202 imass2 5048 . . . . . . . . . . . . 13  |-  ( ( B (,) ( B  +  r ) ) 
C_  D  ->  ( G " ( B (,) ( B  +  r
) ) )  C_  ( G " D ) )
203183, 202syl 17 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( G " ( B (,) ( B  +  r ) ) ) 
C_  ( G " D ) )
204201, 203syl5eqssr 3224 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  ran  (  G  |`  ( B (,) ( B  +  r ) ) ) 
C_  ( G " D ) )
205204sseld 3180 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( 0  e.  ran  (  G  |`  ( B (,) ( B  +  r ) ) )  ->  0  e.  ( G " D ) ) )
206122, 205mtod 170 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  ran  (  G  |`  ( B (,) ( B  +  r ) ) ) )
207191rneqd 4905 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  ran  ( RR  _D  ( G  |`  ( B (,) ( B  +  r
) ) ) )  =  ran  ( ( RR  _D  G )  |`  ( B (,) ( B  +  r )
) ) )
208 df-ima 4701 . . . . . . . . . . . . 13  |-  ( ( RR  _D  G )
" ( B (,) ( B  +  r
) ) )  =  ran  ( ( RR 
_D  G )  |`  ( B (,) ( B  +  r ) ) )
209207, 208syl6eqr 2334 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  ran  ( RR  _D  ( G  |`  ( B (,) ( B  +  r
) ) ) )  =  ( ( RR 
_D  G ) "
( B (,) ( B  +  r )
) ) )
210 imass2 5048 . . . . . . . . . . . . 13  |-  ( ( B (,) ( B  +  r ) ) 
C_  D  ->  (
( RR  _D  G
) " ( B (,) ( B  +  r ) ) ) 
C_  ( ( RR 
_D  G ) " D ) )
211183, 210syl 17 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( RR  _D  G ) " ( B (,) ( B  +  r ) ) ) 
C_  ( ( RR 
_D  G ) " D ) )
212209, 211eqsstrd 3213 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  ran  ( RR  _D  ( G  |`  ( B (,) ( B  +  r
) ) ) ) 
C_  ( ( RR 
_D  G ) " D ) )
213212sseld 3180 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( 0  e.  ran  ( RR  _D  ( G  |`  ( B (,) ( B  +  r
) ) ) )  ->  0  e.  ( ( RR  _D  G
) " D ) ) )
214130, 213mtod 170 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  ran  ( RR  _D  ( G  |`  ( B (,) ( B  +  r
) ) ) ) )
215 limcresi 19229 . . . . . . . . . . 11  |-  ( ( z  e.  D  |->  ( ( ( RR  _D  F ) `  z
)  /  ( ( RR  _D  G ) `
 z ) ) ) lim CC  B ) 
C_  ( ( ( z  e.  D  |->  ( ( ( RR  _D  F ) `  z
)  /  ( ( RR  _D  G ) `
 z ) ) )  |`  ( B (,) ( B  +  r ) ) ) lim CC  B )
216 resmpt 4999 . . . . . . . . . . . . . 14  |-  ( ( B (,) ( B  +  r ) ) 
C_  D  ->  (
( z  e.  D  |->  ( ( ( RR 
_D  F ) `  z )  /  (
( RR  _D  G
) `  z )
) )  |`  ( B (,) ( B  +  r ) ) )  =  ( z  e.  ( B (,) ( B  +  r )
)  |->  ( ( ( RR  _D  F ) `
 z )  / 
( ( RR  _D  G ) `  z
) ) ) )
217183, 216syl 17 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( z  e.  D  |->  ( ( ( RR  _D  F ) `
 z )  / 
( ( RR  _D  G ) `  z
) ) )  |`  ( B (,) ( B  +  r ) ) )  =  ( z  e.  ( B (,) ( B  +  r
) )  |->  ( ( ( RR  _D  F
) `  z )  /  ( ( RR 
_D  G ) `  z ) ) ) )
218181fveq1d 5487 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( RR  _D  ( F  |`  ( B (,) ( B  +  r ) ) ) ) `  z )  =  ( ( ( RR  _D  F )  |`  ( B (,) ( B  +  r )
) ) `  z
) )
219 fvres 5502 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( B (,) ( B  +  r
) )  ->  (
( ( RR  _D  F )  |`  ( B (,) ( B  +  r ) ) ) `
 z )  =  ( ( RR  _D  F ) `  z
) )
220218, 219sylan9eq 2336 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  (
( B  -  r
) (,) ( B  +  r ) ) 
C_  I ) )  /\  z  e.  ( B (,) ( B  +  r ) ) )  ->  ( ( RR  _D  ( F  |`  ( B (,) ( B  +  r ) ) ) ) `  z
)  =  ( ( RR  _D  F ) `
 z ) )
221191fveq1d 5487 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( RR  _D  ( G  |`  ( B (,) ( B  +  r ) ) ) ) `  z )  =  ( ( ( RR  _D  G )  |`  ( B (,) ( B  +  r )
) ) `  z
) )
222 fvres 5502 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( B (,) ( B  +  r
) )  ->  (
( ( RR  _D  G )  |`  ( B (,) ( B  +  r ) ) ) `
 z )  =  ( ( RR  _D  G ) `  z
) )
223221, 222sylan9eq 2336 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  (
( B  -  r
) (,) ( B  +  r ) ) 
C_  I ) )  /\  z  e.  ( B (,) ( B  +  r ) ) )  ->  ( ( RR  _D  ( G  |`  ( B (,) ( B  +  r ) ) ) ) `  z
)  =  ( ( RR  _D  G ) `
 z ) )
224220, 223oveq12d 5837 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  (
( B  -  r
) (,) ( B  +  r ) ) 
C_  I ) )  /\  z  e.  ( B (,) ( B  +  r ) ) )  ->  ( (
( RR  _D  ( F  |`  ( B (,) ( B  +  r
) ) ) ) `
 z )  / 
( ( RR  _D  ( G  |`  ( B (,) ( B  +  r ) ) ) ) `  z ) )  =  ( ( ( RR  _D  F
) `  z )  /  ( ( RR 
_D  G ) `  z ) ) )
225224mpteq2dva 4107 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( z  e.  ( B (,) ( B  +  r ) ) 
|->  ( ( ( RR 
_D  ( F  |`  ( B (,) ( B  +  r ) ) ) ) `  z
)  /  ( ( RR  _D  ( G  |`  ( B (,) ( B  +  r )
) ) ) `  z ) ) )  =  ( z  e.  ( B (,) ( B  +  r )
)  |->  ( ( ( RR  _D  F ) `
 z )  / 
( ( RR  _D  G ) `  z
) ) ) )
226217, 225eqtr4d 2319 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( z  e.  D  |->  ( ( ( RR  _D  F ) `
 z )  / 
( ( RR  _D  G ) `  z
) ) )  |`  ( B (,) ( B  +  r ) ) )  =  ( z  e.  ( B (,) ( B  +  r
) )  |->  ( ( ( RR  _D  ( F  |`  ( B (,) ( B  +  r
) ) ) ) `
 z )  / 
( ( RR  _D  ( G  |`  ( B (,) ( B  +  r ) ) ) ) `  z ) ) ) )
227226oveq1d 5834 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( ( z  e.  D  |->  ( ( ( RR  _D  F
) `  z )  /  ( ( RR 
_D  G ) `  z ) ) )  |`  ( B (,) ( B  +  r )
) ) lim CC  B
)  =  ( ( z  e.  ( B (,) ( B  +  r ) )  |->  ( ( ( RR  _D  ( F  |`  ( B (,) ( B  +  r ) ) ) ) `  z )  /  ( ( RR 
_D  ( G  |`  ( B (,) ( B  +  r ) ) ) ) `  z
) ) ) lim CC  B ) )
228215, 227syl5sseq 3227 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( z  e.  D  |->  ( ( ( RR  _D  F ) `
 z )  / 
( ( RR  _D  G ) `  z
) ) ) lim CC  B )  C_  (
( z  e.  ( B (,) ( B  +  r ) ) 
|->  ( ( ( RR 
_D  ( F  |`  ( B (,) ( B  +  r ) ) ) ) `  z
)  /  ( ( RR  _D  ( G  |`  ( B (,) ( B  +  r )
) ) ) `  z ) ) ) lim
CC  B ) )
229228, 154sseldd 3182 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  C  e.  ( (
z  e.  ( B (,) ( B  +  r ) )  |->  ( ( ( RR  _D  ( F  |`  ( B (,) ( B  +  r ) ) ) ) `  z )  /  ( ( RR 
_D  ( G  |`  ( B (,) ( B  +  r ) ) ) ) `  z
) ) ) lim CC  B ) )
23019, 34, 35, 170, 172, 187, 196, 198, 200, 206, 214, 229lhop1 19355 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  C  e.  ( (
z  e.  ( B (,) ( B  +  r ) )  |->  ( ( ( F  |`  ( B (,) ( B  +  r ) ) ) `  z )  /  ( ( G  |`  ( B (,) ( B  +  r )
) ) `  z
) ) ) lim CC  B ) )
231 resmpt 4999 . . . . . . . . . . 11  |-  ( ( B (,) ( B  +  r ) ) 
C_  ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  -> 
( ( z  e.  ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  |->  ( ( F `  z )  /  ( G `  z ) ) )  |`  ( B (,) ( B  +  r )
) )  =  ( z  e.  ( B (,) ( B  +  r ) )  |->  ( ( F `  z
)  /  ( G `
 z ) ) ) )
232167, 231syl 17 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( z  e.  ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  |->  ( ( F `  z )  /  ( G `  z ) ) )  |`  ( B (,) ( B  +  r )
) )  =  ( z  e.  ( B (,) ( B  +  r ) )  |->  ( ( F `  z
)  /  ( G `
 z ) ) ) )
233 fvres 5502 . . . . . . . . . . . 12  |-  ( z  e.  ( B (,) ( B  +  r
) )  ->  (
( F  |`  ( B (,) ( B  +  r ) ) ) `
 z )  =  ( F `  z
) )
234 fvres 5502 . . . . . . . . . . . 12  |-  ( z  e.  ( B (,) ( B  +  r
) )  ->  (
( G  |`  ( B (,) ( B  +  r ) ) ) `
 z )  =  ( G `  z
) )
235233, 234oveq12d 5837 . . . . . . . . . . 11  |-  ( z  e.  ( B (,) ( B  +  r
) )  ->  (
( ( F  |`  ( B (,) ( B  +  r ) ) ) `  z )  /  ( ( G  |`  ( B (,) ( B  +  r )
) ) `  z
) )  =  ( ( F `  z
)  /  ( G `
 z ) ) )
236235mpteq2ia 4103 . . . . . . . . . 10  |-  ( z  e.  ( B (,) ( B  +  r
) )  |->  ( ( ( F  |`  ( B (,) ( B  +  r ) ) ) `
 z )  / 
( ( G  |`  ( B (,) ( B  +  r ) ) ) `  z ) ) )  =  ( z  e.  ( B (,) ( B  +  r ) )  |->  ( ( F `  z
)  /  ( G `
 z ) ) )
237232, 236syl6eqr 2334 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( z  e.  ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  |->  ( ( F `  z )  /  ( G `  z ) ) )  |`  ( B (,) ( B  +  r )
) )  =  ( z  e.  ( B (,) ( B  +  r ) )  |->  ( ( ( F  |`  ( B (,) ( B  +  r ) ) ) `  z )  /  ( ( G  |`  ( B (,) ( B  +  r )
) ) `  z
) ) ) )
238237oveq1d 5834 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( ( z  e.  ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  |->  ( ( F `  z
)  /  ( G `
 z ) ) )  |`  ( B (,) ( B  +  r ) ) ) lim CC  B )  =  ( ( z  e.  ( B (,) ( B  +  r ) ) 
|->  ( ( ( F  |`  ( B (,) ( B  +  r )
) ) `  z
)  /  ( ( G  |`  ( B (,) ( B  +  r ) ) ) `  z ) ) ) lim
CC  B ) )
239230, 238eleqtrrd 2361 . . . . . . 7  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  C  e.  ( (
( z  e.  ( ( ( B  -  r ) (,) ( B  +  r )
)  \  { B } )  |->  ( ( F `  z )  /  ( G `  z ) ) )  |`  ( B (,) ( B  +  r )
) ) lim CC  B
) )
240 elin 3359 . . . . . . 7  |-  ( C  e.  ( ( ( ( z  e.  ( ( ( B  -  r ) (,) ( B  +  r )
)  \  { B } )  |->  ( ( F `  z )  /  ( G `  z ) ) )  |`  ( ( B  -  r ) (,) B
) ) lim CC  B
)  i^i  ( (
( z  e.  ( ( ( B  -  r ) (,) ( B  +  r )
)  \  { B } )  |->  ( ( F `  z )  /  ( G `  z ) ) )  |`  ( B (,) ( B  +  r )
) ) lim CC  B
) )  <->  ( C  e.  ( ( ( z  e.  ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  |->  ( ( F `  z
)  /  ( G `
 z ) ) )  |`  ( ( B  -  r ) (,) B ) ) lim CC  B )  /\  C  e.  ( ( ( z  e.  ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  |->  ( ( F `  z
)  /  ( G `
 z ) ) )  |`  ( B (,) ( B  +  r ) ) ) lim CC  B ) ) )
241165, 239, 240sylanbrc 648 . . . . . 6  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  C  e.  ( (
( ( z  e.  ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  |->  ( ( F `  z )  /  ( G `  z ) ) )  |`  ( ( B  -  r ) (,) B
) ) lim CC  B
)  i^i  ( (
( z  e.  ( ( ( B  -  r ) (,) ( B  +  r )
)  \  { B } )  |->  ( ( F `  z )  /  ( G `  z ) ) )  |`  ( B (,) ( B  +  r )
) ) lim CC  B
) ) )
242 resmpt 4999 . . . . . . . . 9  |-  ( ( ( ( B  -  r ) (,) ( B  +  r )
)  \  { B } )  C_  D  ->  ( ( z  e.  D  |->  ( ( F `
 z )  / 
( G `  z
) ) )  |`  ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } ) )  =  ( z  e.  ( ( ( B  -  r ) (,) ( B  +  r )
)  \  { B } )  |->  ( ( F `  z )  /  ( G `  z ) ) ) )
24359, 242syl 17 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( z  e.  D  |->  ( ( F `
 z )  / 
( G `  z
) ) )  |`  ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } ) )  =  ( z  e.  ( ( ( B  -  r ) (,) ( B  +  r )
)  \  { B } )  |->  ( ( F `  z )  /  ( G `  z ) ) ) )
244243oveq1d 5834 . . . . . . 7  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( ( z  e.  D  |->  ( ( F `  z )  /  ( G `  z ) ) )  |`  ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } ) ) lim CC  B )  =  ( ( z  e.  ( ( ( B  -  r ) (,) ( B  +  r )
)  \  { B } )  |->  ( ( F `  z )  /  ( G `  z ) ) ) lim
CC  B ) )
24567sselda 3181 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  D )  ->  z  e.  A )
24625ffvelrnda 5626 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  A )  ->  ( F `  z )  e.  RR )
247245, 246syldan 458 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  D )  ->  ( F `  z )  e.  RR )
248247recnd 8856 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  D )  ->  ( F `  z )  e.  CC )
24973ffvelrnda 5626 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  A )  ->  ( G `  z )  e.  RR )
250245, 249syldan 458 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  D )  ->  ( G `  z )  e.  RR )
251250recnd 8856 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  D )  ->  ( G `  z )  e.  CC )
252121adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  D )  ->  -.  0  e.  ( G " D ) )
253 ffn 5354 . . . . . . . . . . . . . . . . 17  |-  ( G : A --> RR  ->  G  Fn  A )
25473, 253syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  G  Fn  A )
255254adantr 453 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  D )  ->  G  Fn  A )
25667adantr 453 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  D )  ->  D  C_  A )
257 simpr 449 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  D )  ->  z  e.  D )
258 fnfvima 5717 . . . . . . . . . . . . . . 15  |-  ( ( G  Fn  A  /\  D  C_  A  /\  z  e.  D )  ->  ( G `  z )  e.  ( G " D
) )
259255, 256, 257, 258syl3anc 1187 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  z  e.  D )  ->  ( G `  z )  e.  ( G " D
) )
260 eleq1 2344 . . . . . . . . . . . . . 14  |-  ( ( G `  z )  =  0  ->  (
( G `  z
)  e.  ( G
" D )  <->  0  e.  ( G " D ) ) )
261259, 260syl5ibcom 213 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  D )  ->  (
( G `  z
)  =  0  -> 
0  e.  ( G
" D ) ) )
262261necon3bd 2484 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  D )  ->  ( -.  0  e.  ( G " D )  -> 
( G `  z
)  =/=  0 ) )
263252, 262mpd 16 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  D )  ->  ( G `  z )  =/=  0 )
264248, 251, 263divcld 9531 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  D )  ->  (
( F `  z
)  /  ( G `
 z ) )  e.  CC )
265264adantlr 698 . . . . . . . . 9  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  (
( B  -  r
) (,) ( B  +  r ) ) 
C_  I ) )  /\  z  e.  D
)  ->  ( ( F `  z )  /  ( G `  z ) )  e.  CC )
266 eqid 2284 . . . . . . . . 9  |-  ( z  e.  D  |->  ( ( F `  z )  /  ( G `  z ) ) )  =  ( z  e.  D  |->  ( ( F `
 z )  / 
( G `  z
) ) )
267265, 266fmptd 5645 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( z  e.  D  |->  ( ( F `  z )  /  ( G `  z )
) ) : D --> CC )
268 difss 3304 . . . . . . . . . . 11  |-  ( I 
\  { B }
)  C_  I
26958, 268eqsstri 3209 . . . . . . . . . 10  |-  D  C_  I
27013, 61syl6ss 3192 . . . . . . . . . 10  |-  ( ph  ->  I  C_  CC )
271269, 270syl5ss 3191 . . . . . . . . 9  |-  ( ph  ->  D  C_  CC )
272271adantr 453 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  D  C_  CC )
273 eqid 2284 . . . . . . . 8  |-  ( (
TopOpen ` fld )t  ( D  u.  { B } ) )  =  ( ( TopOpen ` fld )t  ( D  u.  { B } ) )
27458uneq1i 3326 . . . . . . . . . . . . . . . . 17  |-  ( D  u.  { B }
)  =  ( ( I  \  { B } )  u.  { B } )
275 undif1 3530 . . . . . . . . . . . . . . . . 17  |-  ( ( I  \  { B } )  u.  { B } )  =  ( I  u.  { B } )
276274, 275eqtri 2304 . . . . . . . . . . . . . . . 16  |-  ( D  u.  { B }
)  =  ( I  u.  { B }
)
277 simprr 736 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) ( B  +  r )
)  C_  I )
27842, 277sstrd 3190 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  { B }  C_  I
)
279 ssequn2 3349 . . . . . . . . . . . . . . . . 17  |-  ( { B }  C_  I  <->  ( I  u.  { B } )  =  I )
280278, 279sylib 190 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( I  u.  { B } )  =  I )
281276, 280syl5eq 2328 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( D  u.  { B } )  =  I )
282281oveq2d 5835 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( TopOpen ` fld )t  ( D  u.  { B } ) )  =  ( ( TopOpen ` fld )t  I
) )
28313adantr 453 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  I  C_  RR )
284 eqid 2284 . . . . . . . . . . . . . . . 16  |-  ( topGen ` 
ran  (,) )  =  (
topGen `  ran  (,) )
28582, 284rerest 18304 . . . . . . . . . . . . . . 15  |-  ( I 
C_  RR  ->  ( (
TopOpen ` fld )t  I )  =  ( ( topGen `  ran  (,) )t  I
) )
286283, 285syl 17 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( TopOpen ` fld )t  I )  =  ( ( topGen `  ran  (,) )t  I
) )
287282, 286eqtrd 2316 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( TopOpen ` fld )t  ( D  u.  { B } ) )  =  ( ( topGen ` 
ran  (,) )t  I ) )
288287fveq2d 5489 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( int `  (
( TopOpen ` fld )t  ( D  u.  { B } ) ) )  =  ( int `  ( ( topGen `  ran  (,) )t  I ) ) )
289288fveq1d 5487 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( int `  (
( TopOpen ` fld )t  ( D  u.  { B } ) ) ) `  ( ( B  -  r ) (,) ( B  +  r ) ) )  =  ( ( int `  ( ( topGen `  ran  (,) )t  I ) ) `  ( ( B  -  r ) (,) ( B  +  r )
) ) )
29082cnfldtopon 18286 . . . . . . . . . . . . . . 15  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
291270adantr 453 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  I  C_  CC )
292 resttopon 16886 . . . . . . . . . . . . . . 15  |-  ( ( ( TopOpen ` fld )  e.  (TopOn `  CC )  /\  I  C_  CC )  ->  (
( TopOpen ` fld )t  I )  e.  (TopOn `  I ) )
293290, 291, 292sylancr 647 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( TopOpen ` fld )t  I )  e.  (TopOn `  I ) )
294 topontop 16658 . . . . . . . . . . . . . 14  |-  ( ( ( TopOpen ` fld )t  I )  e.  (TopOn `  I )  ->  (
( TopOpen ` fld )t  I )  e.  Top )
295293, 294syl 17 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( TopOpen ` fld )t  I )  e.  Top )
296286, 295eqeltrrd 2359 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( topGen `  ran  (,) )t  I )  e.  Top )
297 iooretop 18269 . . . . . . . . . . . . . 14  |-  ( ( B  -  r ) (,) ( B  +  r ) )  e.  ( topGen `  ran  (,) )
298297a1i 12 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) ( B  +  r )
)  e.  ( topGen ` 
ran  (,) ) )
2994adantr 453 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  I  e.  ( topGen ` 
ran  (,) ) )
300 restopn2 16902 . . . . . . . . . . . . . 14  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  I  e.  ( topGen `  ran  (,) )
)  ->  ( (
( B  -  r
) (,) ( B  +  r ) )  e.  ( ( topGen ` 
ran  (,) )t  I )  <->  ( (
( B  -  r
) (,) ( B  +  r ) )  e.  ( topGen `  ran  (,) )  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) ) )
30186, 299, 300sylancr 647 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( ( B  -  r ) (,) ( B  +  r ) )  e.  ( ( topGen `  ran  (,) )t  I
)  <->  ( ( ( B  -  r ) (,) ( B  +  r ) )  e.  ( topGen `  ran  (,) )  /\  ( ( B  -  r ) (,) ( B  +  r )
)  C_  I )
) )
302298, 277, 301mpbir2and 893 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) ( B  +  r )
)  e.  ( (
topGen `  ran  (,) )t  I
) )
303 isopn3i 16813 . . . . . . . . . . . 12  |-  ( ( ( ( topGen `  ran  (,) )t  I )  e.  Top  /\  ( ( B  -  r ) (,) ( B  +  r )
)  e.  ( (
topGen `  ran  (,) )t  I
) )  ->  (
( int `  (
( topGen `  ran  (,) )t  I
) ) `  (
( B  -  r
) (,) ( B  +  r ) ) )  =  ( ( B  -  r ) (,) ( B  +  r ) ) )
304296, 302, 303syl2anc 645 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( int `  (
( topGen `  ran  (,) )t  I
) ) `  (
( B  -  r
) (,) ( B  +  r ) ) )  =  ( ( B  -  r ) (,) ( B  +  r ) ) )
305289, 304eqtrd 2316 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( int `  (
( TopOpen ` fld )t  ( D  u.  { B } ) ) ) `  ( ( B  -  r ) (,) ( B  +  r ) ) )  =  ( ( B  -  r ) (,) ( B  +  r ) ) )
30641, 305eleqtrrd 2361 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  B  e.  ( ( int `  ( ( TopOpen ` fld )t  ( D  u.  { B } ) ) ) `
 ( ( B  -  r ) (,) ( B  +  r ) ) ) )
307 undif1 3530 . . . . . . . . . . 11  |-  ( ( ( ( B  -  r ) (,) ( B  +  r )
)  \  { B } )  u.  { B } )  =  ( ( ( B  -  r ) (,) ( B  +  r )
)  u.  { B } )
308 ssequn2 3349 . . . . . . . . . . . 12  |-  ( { B }  C_  (
( B  -  r
) (,) ( B  +  r ) )  <-> 
( ( ( B  -  r ) (,) ( B  +  r ) )  u.  { B } )  =  ( ( B  -  r
) (,) ( B  +  r ) ) )
30942, 308sylib 190 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( ( B  -  r ) (,) ( B  +  r ) )  u.  { B } )  =  ( ( B  -  r
) (,) ( B  +  r ) ) )
310307, 309syl5eq 2328 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  u. 
{ B } )  =  ( ( B  -  r ) (,) ( B  +  r ) ) )
311310fveq2d 5489 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( int `  (
( TopOpen ` fld )t  ( D  u.  { B } ) ) ) `  ( ( ( ( B  -  r ) (,) ( B  +  r )
)  \  { B } )  u.  { B } ) )  =  ( ( int `  (
( TopOpen ` fld )t  ( D  u.  { B } ) ) ) `  ( ( B  -  r ) (,) ( B  +  r ) ) ) )
312306, 311eleqtrrd 2361 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  B  e.  ( ( int `  ( ( TopOpen ` fld )t  ( D  u.  { B } ) ) ) `
 ( ( ( ( B  -  r
) (,) ( B  +  r ) ) 
\  { B }
)  u.  { B } ) ) )
313267, 59, 272, 82, 273, 312limcres 19230 . . . . . . 7  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( ( z  e.  D  |->  ( ( F `  z )  /  ( G `  z ) ) )  |`  ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } ) ) lim CC  B )  =  ( ( z  e.  D  |->  ( ( F `  z )  /  ( G `  z )
) ) lim CC  B
) )
31480, 61sstri 3189 . . . . . . . . 9  |-  ( ( B  -  r ) (,) B )  C_  CC
315314a1i 12 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  CC )
316173, 61sstri 3189 . . . . . . . . 9  |-  ( B (,) ( B  +  r ) )  C_  CC
317316a1i 12 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +