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

Theorem lhop 19363
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
Dummy variable  r is distinct from all other variables.
StepHypRef Expression
1 eqid 2283 . . . . 5  |-  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )  =  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )
21rexmet 18297 . . . 4  |-  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )  e.  ( * Met `  RR )
32a1i 10 . . 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 2283 . . . . 5  |-  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )  =  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )
71, 6tgioo 18302 . . . 4  |-  ( topGen ` 
ran  (,) )  =  (
MetOpen `  ( ( abs 
o.  -  )  |`  ( RR  X.  RR ) ) )
87mopni2 18039 . . 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 1182 . 2  |-  ( ph  ->  E. r  e.  RR+  ( B ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  I )
10 elssuni 3855 . . . . . . . . 9  |-  ( I  e.  ( topGen `  ran  (,) )  ->  I  C_  U. ( topGen `
 ran  (,) )
)
11 uniretop 18271 . . . . . . . . 9  |-  RR  =  U. ( topGen `  ran  (,) )
1210, 11syl6sseqr 3225 . . . . . . . 8  |-  ( I  e.  ( topGen `  ran  (,) )  ->  I  C_  RR )
134, 12syl 15 . . . . . . 7  |-  ( ph  ->  I  C_  RR )
1413, 5sseldd 3181 . . . . . 6  |-  ( ph  ->  B  e.  RR )
15 rpre 10360 . . . . . 6  |-  ( r  e.  RR+  ->  r  e.  RR )
161bl2ioo 18298 . . . . . 6  |-  ( ( B  e.  RR  /\  r  e.  RR )  ->  ( B ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) r )  =  ( ( B  -  r ) (,) ( B  +  r )
) )
1714, 15, 16syl2an 463 . . . . 5  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( B
( ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  =  ( ( B  -  r ) (,) ( B  +  r ) ) )
1817sseq1d 3205 . . . 4  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( ( B ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  I  <->  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I
) )
1914adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  B  e.  RR )
20 simprl 732 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
r  e.  RR+ )
2120rpred 10390 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
r  e.  RR )
2219, 21resubcld 9211 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B  -  r
)  e.  RR )
2322rexrd 8881 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B  -  r
)  e.  RR* )
2419, 20ltsubrpd 10418 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B  -  r
)  <  B )
25 lhop.f . . . . . . . . . . 11  |-  ( ph  ->  F : A --> RR )
2625adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  F : A --> RR )
27 ssun1 3338 . . . . . . . . . . . 12  |-  ( ( B  -  r ) (,) B )  C_  ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r ) ) )
28 unass 3332 . . . . . . . . . . . . . . 15  |-  ( ( { B }  u.  ( ( B  -  r ) (,) B
) )  u.  ( B (,) ( B  +  r ) ) )  =  ( { B }  u.  ( (
( B  -  r
) (,) B )  u.  ( B (,) ( B  +  r
) ) ) )
29 uncom 3319 . . . . . . . . . . . . . . . 16  |-  ( { B }  u.  (
( B  -  r
) (,) B ) )  =  ( ( ( B  -  r
) (,) B )  u.  { B }
)
3029uneq1i 3325 . . . . . . . . . . . . . . 15  |-  ( ( { B }  u.  ( ( B  -  r ) (,) B
) )  u.  ( B (,) ( B  +  r ) ) )  =  ( ( ( ( B  -  r
) (,) B )  u.  { B }
)  u.  ( B (,) ( B  +  r ) ) )
3128, 30eqtr3i 2305 . . . . . . . . . . . . . 14  |-  ( { B }  u.  (
( ( B  -  r ) (,) B
)  u.  ( B (,) ( B  +  r ) ) ) )  =  ( ( ( ( B  -  r ) (,) B
)  u.  { B } )  u.  ( B (,) ( B  +  r ) ) )
3219rexrd 8881 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  B  e.  RR* )
3319, 21readdcld 8862 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B  +  r )  e.  RR )
3433rexrd 8881 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B  +  r )  e.  RR* )
3519, 20ltaddrpd 10419 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  B  <  ( B  +  r ) )
36 ioojoin 10766 . . . . . . . . . . . . . . 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 1190 . . . . . . . . . . . . . 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 2327 . . . . . . . . . . . . 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 10697 . . . . . . . . . . . . . . . . 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 642 . . . . . . . . . . . . . . . 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 1135 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  B  e.  ( ( B  -  r ) (,) ( B  +  r ) ) )
4241snssd 3760 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  { B }  C_  (
( B  -  r
) (,) ( B  +  r ) ) )
43 incom 3361 . . . . . . . . . . . . . . 15  |-  ( { B }  i^i  (
( ( B  -  r ) (,) B
)  u.  ( B (,) ( B  +  r ) ) ) )  =  ( ( ( ( B  -  r ) (,) B
)  u.  ( B (,) ( B  +  r ) ) )  i^i  { B }
)
44 ubioo 10688 . . . . . . . . . . . . . . . . . 18  |-  -.  B  e.  ( ( B  -  r ) (,) B
)
45 lbioo 10687 . . . . . . . . . . . . . . . . . 18  |-  -.  B  e.  ( B (,) ( B  +  r )
)
4644, 45pm3.2ni 827 . . . . . . . . . . . . . . . . 17  |-  -.  ( B  e.  ( ( B  -  r ) (,) B )  \/  B  e.  ( B (,) ( B  +  r )
) )
47 elun 3316 . . . . . . . . . . . . . . . . 17  |-  ( B  e.  ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r )
) )  <->  ( B  e.  ( ( B  -  r ) (,) B
)  \/  B  e.  ( B (,) ( B  +  r )
) ) )
4846, 47mtbir 290 . . . . . . . . . . . . . . . 16  |-  -.  B  e.  ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r ) ) )
49 disjsn 3693 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r ) ) )  i^i  { B }
)  =  (/)  <->  -.  B  e.  ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r ) ) ) )
5048, 49mpbir 200 . . . . . . . . . . . . . . 15  |-  ( ( ( ( B  -  r ) (,) B
)  u.  ( B (,) ( B  +  r ) ) )  i^i  { B }
)  =  (/)
5143, 50eqtri 2303 . . . . . . . . . . . . . 14  |-  ( { B }  i^i  (
( ( B  -  r ) (,) B
)  u.  ( B (,) ( B  +  r ) ) ) )  =  (/)
52 uneqdifeq 3542 . . . . . . . . . . . . . 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 643 . . . . . . . . . . . . 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 201 . . . . . . . . . . . 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 3227 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  ( (
( B  -  r
) (,) ( B  +  r ) ) 
\  { B }
) )
56 ssdif 3311 . . . . . . . . . . . . . 14  |-  ( ( ( B  -  r
) (,) ( B  +  r ) ) 
C_  I  ->  (
( ( B  -  r ) (,) ( B  +  r )
)  \  { B } )  C_  (
I  \  { B } ) )
5756ad2antll 709 . . . . . . . . . . . . 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 3225 . . . . . . . . . . . 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 8794 . . . . . . . . . . . . . . . 16  |-  RR  C_  CC
6261a1i 10 . . . . . . . . . . . . . . 15  |-  ( ph  ->  RR  C_  CC )
63 fss 5397 . . . . . . . . . . . . . . . 16  |-  ( ( F : A --> RR  /\  RR  C_  CC )  ->  F : A --> CC )
6425, 61, 63sylancl 643 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F : A --> CC )
65 lhop.a . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  C_  RR )
6662, 64, 65dvbss 19251 . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  ( RR  _D  F )  C_  A
)
6760, 66sstrd 3189 . . . . . . . . . . . . 13  |-  ( ph  ->  D  C_  A )
6867adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  D  C_  A )
6959, 68sstrd 3189 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  C_  A
)
7055, 69sstrd 3189 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  A )
71 fssres 5408 . . . . . . . . . 10  |-  ( ( F : A --> RR  /\  ( ( B  -  r ) (,) B
)  C_  A )  ->  ( F  |`  (
( B  -  r
) (,) B ) ) : ( ( B  -  r ) (,) B ) --> RR )
7226, 70, 71syl2anc 642 . . . . . . . . 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 451 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  G : A --> RR )
75 fssres 5408 . . . . . . . . . 10  |-  ( ( G : A --> RR  /\  ( ( B  -  r ) (,) B
)  C_  A )  ->  ( G  |`  (
( B  -  r
) (,) B ) ) : ( ( B  -  r ) (,) B ) --> RR )
7674, 70, 75syl2anc 642 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( G  |`  (
( B  -  r
) (,) B ) ) : ( ( B  -  r ) (,) B ) --> RR )
7761a1i 10 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  RR  C_  CC )
7864adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  F : A --> CC )
7965adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  A  C_  RR )
80 ioossre 10712 . . . . . . . . . . . . . 14  |-  ( ( B  -  r ) (,) B )  C_  RR
8180a1i 10 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  RR )
82 eqid 2283 . . . . . . . . . . . . . 14  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
8382tgioo2 18309 . . . . . . . . . . . . . 14  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
8482, 83dvres 19261 . . . . . . . . . . . . 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 1183 . . . . . . . . . . . 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 18270 . . . . . . . . . . . . . 14  |-  ( topGen ` 
ran  (,) )  e.  Top
87 iooretop 18275 . . . . . . . . . . . . . 14  |-  ( ( B  -  r ) (,) B )  e.  ( topGen `  ran  (,) )
88 isopn3i 16819 . . . . . . . . . . . . . 14  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( ( B  -  r ) (,) B )  e.  ( topGen `  ran  (,) )
)  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  (
( B  -  r
) (,) B ) )  =  ( ( B  -  r ) (,) B ) )
8986, 87, 88mp2an 653 . . . . . . . . . . . . 13  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( ( B  -  r ) (,) B
) )  =  ( ( B  -  r
) (,) B )
9089reseq2i 4952 . . . . . . . . . . . 12  |-  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( B  -  r ) (,) B ) ) )  =  ( ( RR 
_D  F )  |`  ( ( B  -  r ) (,) B
) )
9185, 90syl6eq 2331 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( RR  _D  ( F  |`  ( ( B  -  r ) (,) B ) ) )  =  ( ( RR 
_D  F )  |`  ( ( B  -  r ) (,) B
) ) )
9291dmeqd 4881 . . . . . . . . . 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 3189 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  D )
9460adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  D  C_  dom  ( RR 
_D  F ) )
9593, 94sstrd 3189 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  dom  ( RR 
_D  F ) )
96 ssdmres 4977 . . . . . . . . . . 11  |-  ( ( ( B  -  r
) (,) B ) 
C_  dom  ( RR  _D  F )  <->  dom  ( ( RR  _D  F )  |`  ( ( B  -  r ) (,) B
) )  =  ( ( B  -  r
) (,) B ) )
9795, 96sylib 188 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( ( RR  _D  F )  |`  (
( B  -  r
) (,) B ) )  =  ( ( B  -  r ) (,) B ) )
9892, 97eqtrd 2315 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( RR  _D  ( F  |`  ( ( B  -  r ) (,) B ) ) )  =  ( ( B  -  r ) (,) B ) )
99 fss 5397 . . . . . . . . . . . . . . 15  |-  ( ( G : A --> RR  /\  RR  C_  CC )  ->  G : A --> CC )
10073, 61, 99sylancl 643 . . . . . . . . . . . . . 14  |-  ( ph  ->  G : A --> CC )
101100adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  G : A --> CC )
10282, 83dvres 19261 . . . . . . . . . . . . 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 1183 . . . . . . . . . . . 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 4952 . . . . . . . . . . . 12  |-  ( ( RR  _D  G )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( B  -  r ) (,) B ) ) )  =  ( ( RR 
_D  G )  |`  ( ( B  -  r ) (,) B
) )
105103, 104syl6eq 2331 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) )  =  ( ( RR 
_D  G )  |`  ( ( B  -  r ) (,) B
) ) )
106105dmeqd 4881 . . . . . . . . . 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 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  D  C_  dom  ( RR 
_D  G ) )
10993, 108sstrd 3189 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  dom  ( RR 
_D  G ) )
110 ssdmres 4977 . . . . . . . . . . 11  |-  ( ( ( B  -  r
) (,) B ) 
C_  dom  ( RR  _D  G )  <->  dom  ( ( RR  _D  G )  |`  ( ( B  -  r ) (,) B
) )  =  ( ( B  -  r
) (,) B ) )
111109, 110sylib 188 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( ( RR  _D  G )  |`  (
( B  -  r
) (,) B ) )  =  ( ( B  -  r ) (,) B ) )
112106, 111eqtrd 2315 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) )  =  ( ( B  -  r ) (,) B ) )
113 limcresi 19235 . . . . . . . . . 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 451 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( F lim
CC  B ) )
116113, 115sseldi 3178 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( ( F  |`  ( ( B  -  r ) (,) B ) ) lim CC  B ) )
117 limcresi 19235 . . . . . . . . . 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 451 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( G lim
CC  B ) )
120117, 119sseldi 3178 . . . . . . . . 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 451 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  ( G " D ) )
123 df-ima 4702 . . . . . . . . . . . 12  |-  ( G
" ( ( B  -  r ) (,) B ) )  =  ran  ( G  |`  ( ( B  -  r ) (,) B
) )
124 imass2 5049 . . . . . . . . . . . . 13  |-  ( ( ( B  -  r
) (,) B ) 
C_  D  ->  ( G " ( ( B  -  r ) (,) B ) )  C_  ( G " D ) )
12593, 124syl 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( G " (
( B  -  r
) (,) B ) )  C_  ( G " D ) )
126123, 125syl5eqssr 3223 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  ran  ( G  |`  (
( B  -  r
) (,) B ) )  C_  ( G " D ) )
127126sseld 3179 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( 0  e.  ran  ( G  |`  ( ( B  -  r ) (,) B ) )  ->  0  e.  ( G " D ) ) )
128122, 127mtod 168 . . . . . . . . 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 451 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  (
( RR  _D  G
) " D ) )
131105rneqd 4906 . . . . . . . . . . . . 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 4702 . . . . . . . . . . . . 13  |-  ( ( RR  _D  G )
" ( ( B  -  r ) (,) B ) )  =  ran  ( ( RR 
_D  G )  |`  ( ( B  -  r ) (,) B
) )
133131, 132syl6eqr 2333 . . . . . . . . . . . 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 5049 . . . . . . . . . . . . 13  |-  ( ( ( B  -  r
) (,) B ) 
C_  D  ->  (
( RR  _D  G
) " ( ( B  -  r ) (,) B ) ) 
C_  ( ( RR 
_D  G ) " D ) )
13593, 134syl 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( RR  _D  G ) " (
( B  -  r
) (,) B ) )  C_  ( ( RR  _D  G ) " D ) )
136133, 135eqsstrd 3212 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  ran  ( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) ) 
C_  ( ( RR 
_D  G ) " D ) )
137136sseld 3179 . . . . . . . . . 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 168 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  ran  ( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) ) )
139 limcresi 19235 . . . . . . . . . . 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 5000 . . . . . . . . . . . . . 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 15 . . . . . . . . . . . . 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 5527 . . . . . . . . . . . . . . . 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 5542 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( ( B  -  r ) (,) B )  ->  (
( ( RR  _D  F )  |`  (
( B  -  r
) (,) B ) ) `  z )  =  ( ( RR 
_D  F ) `  z ) )
144142, 143sylan9eq 2335 . . . . . . . . . . . . . . 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 5527 . . . . . . . . . . . . . . . 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 5542 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( ( B  -  r ) (,) B )  ->  (
( ( RR  _D  G )  |`  (
( B  -  r
) (,) B ) ) `  z )  =  ( ( RR 
_D  G ) `  z ) )
147145, 146sylan9eq 2335 . . . . . . . . . . . . . . 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 5876 . . . . . . . . . . . . . 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 4106 . . . . . . . . . . . . 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 2318 . . . . . . . . . . . 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 5873 . . . . . . . . . . 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 3226 . . . . . . . . . 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 451 . . . . . . . . . 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 3181 . . . . . . . . 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 19362 . . . . . . . 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 5000 . . . . . . . . . . 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 15 . . . . . . . . . 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 5542 . . . . . . . . . . . 12  |-  ( z  e.  ( ( B  -  r ) (,) B )  ->  (
( F  |`  (
( B  -  r
) (,) B ) ) `  z )  =  ( F `  z ) )
160 fvres 5542 . . . . . . . . . . . 12  |-  ( z  e.  ( ( B  -  r ) (,) B )  ->  (
( G  |`  (
( B  -  r
) (,) B ) ) `  z )  =  ( G `  z ) )
161159, 160oveq12d 5876 . . . . . . . . . . 11  |-  ( z  e.  ( ( B  -  r ) (,) B )  ->  (
( ( F  |`  ( ( B  -  r ) (,) B
) ) `  z
)  /  ( ( G  |`  ( ( B  -  r ) (,) B ) ) `  z ) )  =  ( ( F `  z )  /  ( G `  z )
) )
162161mpteq2ia 4102 . . . . . . . . . 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 2333 . . . . . . . . 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 5873 . . . . . . . 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 2360 . . . . . . 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 3339 . . . . . . . . . . . 12  |-  ( B (,) ( B  +  r ) )  C_  ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r ) ) )
167166, 54syl5sseqr 3227 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  ( (
( B  -  r
) (,) ( B  +  r ) ) 
\  { B }
) )
168167, 69sstrd 3189 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  A )
169 fssres 5408 . . . . . . . . . 10  |-  ( ( F : A --> RR  /\  ( B (,) ( B  +  r ) ) 
C_  A )  -> 
( F  |`  ( B (,) ( B  +  r ) ) ) : ( B (,) ( B  +  r
) ) --> RR )
17026, 168, 169syl2anc 642 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( F  |`  ( B (,) ( B  +  r ) ) ) : ( B (,) ( B  +  r
) ) --> RR )
171 fssres 5408 . . . . . . . . . 10  |-  ( ( G : A --> RR  /\  ( B (,) ( B  +  r ) ) 
C_  A )  -> 
( G  |`  ( B (,) ( B  +  r ) ) ) : ( B (,) ( B  +  r
) ) --> RR )
17274, 168, 171syl2anc 642 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( G  |`  ( B (,) ( B  +  r ) ) ) : ( B (,) ( B  +  r
) ) --> RR )
173 ioossre 10712 . . . . . . . . . . . . . 14  |-  ( B (,) ( B  +  r ) )  C_  RR
174173a1i 10 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  RR )
17582, 83dvres 19261 . . . . . . . . . . . . 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 1183 . . . . . . . . . . . 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 18275 . . . . . . . . . . . . . 14  |-  ( B (,) ( B  +  r ) )  e.  ( topGen `  ran  (,) )
178 isopn3i 16819 . . . . . . . . . . . . . 14  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( B (,) ( B  +  r ) )  e.  ( topGen `  ran  (,) )
)  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  ( B (,) ( B  +  r ) ) )  =  ( B (,) ( B  +  r
) ) )
17986, 177, 178mp2an 653 . . . . . . . . . . . . 13  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( B (,) ( B  +  r ) ) )  =  ( B (,) ( B  +  r ) )
180179reseq2i 4952 . . . . . . . . . . . 12  |-  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( B (,) ( B  +  r ) ) ) )  =  ( ( RR 
_D  F )  |`  ( B (,) ( B  +  r ) ) )
181176, 180syl6eq 2331 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( RR  _D  ( F  |`  ( B (,) ( B  +  r
) ) ) )  =  ( ( RR 
_D  F )  |`  ( B (,) ( B  +  r ) ) ) )
182181dmeqd 4881 . . . . . . . . . 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 3189 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  D )
184183, 94sstrd 3189 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  dom  ( RR 
_D  F ) )
185 ssdmres 4977 . . . . . . . . . . 11  |-  ( ( B (,) ( B  +  r ) ) 
C_  dom  ( RR  _D  F )  <->  dom  ( ( RR  _D  F )  |`  ( B (,) ( B  +  r )
) )  =  ( B (,) ( B  +  r ) ) )
186184, 185sylib 188 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( ( RR  _D  F )  |`  ( B (,) ( B  +  r ) ) )  =  ( B (,) ( B  +  r
) ) )
187182, 186eqtrd 2315 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( RR  _D  ( F  |`  ( B (,) ( B  +  r
) ) ) )  =  ( B (,) ( B  +  r
) ) )
18882, 83dvres 19261 . . . . . . . . . . . . 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 1183 . . . . . . . . . . . 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 4952 . . . . . . . . . . . 12  |-  ( ( RR  _D  G )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( B (,) ( B  +  r ) ) ) )  =  ( ( RR 
_D  G )  |`  ( B (,) ( B  +  r ) ) )
191189, 190syl6eq 2331 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( RR  _D  ( G  |`  ( B (,) ( B  +  r
) ) ) )  =  ( ( RR 
_D  G )  |`  ( B (,) ( B  +  r ) ) ) )
192191dmeqd 4881 . . . . . . . . . 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 3189 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  dom  ( RR 
_D  G ) )
194 ssdmres 4977 . . . . . . . . . . 11  |-  ( ( B (,) ( B  +  r ) ) 
C_  dom  ( RR  _D  G )  <->  dom  ( ( RR  _D  G )  |`  ( B (,) ( B  +  r )
) )  =  ( B (,) ( B  +  r ) ) )
195193, 194sylib 188 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( ( RR  _D  G )  |`  ( B (,) ( B  +  r ) ) )  =  ( B (,) ( B  +  r
) ) )
196192, 195eqtrd 2315 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( RR  _D  ( G  |`  ( B (,) ( B  +  r
) ) ) )  =  ( B (,) ( B  +  r
) ) )
197 limcresi 19235 . . . . . . . . . 10  |-  ( F lim
CC  B )  C_  ( ( F  |`  ( B (,) ( B  +  r ) ) ) lim CC  B )
198197, 115sseldi 3178 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( ( F  |`  ( B (,) ( B  +  r ) ) ) lim CC  B ) )
199 limcresi 19235 . . . . . . . . . 10  |-  ( G lim
CC  B )  C_  ( ( G  |`  ( B (,) ( B  +  r ) ) ) lim CC  B )
200199, 119sseldi 3178 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( ( G  |`  ( B (,) ( B  +  r ) ) ) lim CC  B ) )
201 df-ima 4702 . . . . . . . . . . . 12  |-  ( G
" ( B (,) ( B  +  r
) ) )  =  ran  ( G  |`  ( B (,) ( B  +  r ) ) )
202 imass2 5049 . . . . . . . . . . . . 13  |-  ( ( B (,) ( B  +  r ) ) 
C_  D  ->  ( G " ( B (,) ( B  +  r
) ) )  C_  ( G " D ) )
203183, 202syl 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( G " ( B (,) ( B  +  r ) ) ) 
C_  ( G " D ) )
204201, 203syl5eqssr 3223 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  ran  ( G  |`  ( B (,) ( B  +  r ) ) ) 
C_  ( G " D ) )
205204sseld 3179 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( 0  e.  ran  ( G  |`  ( B (,) ( B  +  r ) ) )  ->  0  e.  ( G " D ) ) )
206122, 205mtod 168 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  ran  ( G  |`  ( B (,) ( B  +  r ) ) ) )
207191rneqd 4906 . . . . . . . . . . . . 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 4702 . . . . . . . . . . . . 13  |-  ( ( RR  _D  G )
" ( B (,) ( B  +  r
) ) )  =  ran  ( ( RR 
_D  G )  |`  ( B (,) ( B  +  r ) ) )
209207, 208syl6eqr 2333 . . . . . . . . . . . 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 5049 . . . . . . . . . . . . 13  |-  ( ( B (,) ( B  +  r ) ) 
C_  D  ->  (
( RR  _D  G
) " ( B (,) ( B  +  r ) ) ) 
C_  ( ( RR 
_D  G ) " D ) )
211183, 210syl 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( RR  _D  G ) " ( B (,) ( B  +  r ) ) ) 
C_  ( ( RR 
_D  G ) " D ) )
212209, 211eqsstrd 3212 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  ran  ( RR  _D  ( G  |`  ( B (,) ( B  +  r
) ) ) ) 
C_  ( ( RR 
_D  G ) " D ) )
213212sseld 3179 . . . . . . . . . 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 168 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  ran  ( RR  _D  ( G  |`  ( B (,) ( B  +  r
) ) ) ) )
215 limcresi 19235 . . . . . . . . . . 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 5000 . . . . . . . . . . . . . 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 15 . . . . . . . . . . . . 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 5527 . . . . . . . . . . . . . . . 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 5542 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( B (,) ( B  +  r
) )  ->  (
( ( RR  _D  F )  |`  ( B (,) ( B  +  r ) ) ) `
 z )  =  ( ( RR  _D  F ) `  z
) )
220218, 219sylan9eq 2335 . . . . . . . . . . . . . . 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 5527 . . . . . . . . . . . . . . . 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 5542 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( B (,) ( B  +  r
) )  ->  (
( ( RR  _D  G )  |`  ( B (,) ( B  +  r ) ) ) `
 z )  =  ( ( RR  _D  G ) `  z
) )
223221, 222sylan9eq 2335 . . . . . . . . . . . . . . 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 5876 . . . . . . . . . . . . . 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 4106 . . . . . . . . . . . . 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 2318 . . . . . . . . . . . 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 5873 . . . . . . . . . . 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 3226 . . . . . . . . . 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 3181 . . . . . . . . 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 19361 . . . . . . . 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 5000 . . . . . . . . . . 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 15 . . . . . . . . . 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 5542 . . . . . . . . . . . 12  |-  ( z  e.  ( B (,) ( B  +  r
) )  ->  (
( F  |`  ( B (,) ( B  +  r ) ) ) `
 z )  =  ( F `  z
) )
234 fvres 5542 . . . . . . . . . . . 12  |-  ( z  e.  ( B (,) ( B  +  r
) )  ->  (
( G  |`  ( B (,) ( B  +  r ) ) ) `
 z )  =  ( G `  z
) )
235233, 234oveq12d 5876 . . . . . . . . . . 11  |-  ( z  e.  ( B (,) ( B  +  r
) )  ->  (
( ( F  |`  ( B (,) ( B  +  r ) ) ) `  z )  /  ( ( G  |`  ( B (,) ( B  +  r )
) ) `  z
) )  =  ( ( F `  z
)  /  ( G `
 z ) ) )
236235mpteq2ia 4102 . . . . . . . . . 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 2333 . . . . . . . . 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 5873 . . . . . . . 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 2360 . . . . . . 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 3358 . . . . . . 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 645 . . . . . 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 5000 . . . . . . . . 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 15 . . . . . . . 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 5873 . . . . . . 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 3180 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  D )  ->  z  e.  A )
24625ffvelrnda 5665 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  A )  ->  ( F `  z )  e.  RR )
247245, 246syldan 456 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  D )  ->  ( F `  z )  e.  RR )
248247recnd 8861 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  D )  ->  ( F `  z )  e.  CC )
24973ffvelrnda 5665 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  A )  ->  ( G `  z )  e.  RR )
250245, 249syldan 456 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  D )  ->  ( G `  z )  e.  RR )
251250recnd 8861 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  D )  ->  ( G `  z )  e.  CC )
252121adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  D )  ->  -.  0  e.  ( G " D ) )
253 ffn 5389 . . . . . . . . . . . . . . . . 17  |-  ( G : A --> RR  ->  G  Fn  A )
25473, 253syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  G  Fn  A )
255254adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  D )  ->  G  Fn  A )
25667adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  D )  ->  D  C_  A )
257 simpr 447 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  D )  ->  z  e.  D )
258 fnfvima 5756 . . . . . . . . . . . . . . 15  |-  ( ( G  Fn  A  /\  D  C_  A  /\  z  e.  D )  ->  ( G `  z )  e.  ( G " D
) )
259255, 256, 257, 258syl3anc 1182 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  z  e.  D )  ->  ( G `  z )  e.  ( G " D
) )
260 eleq1 2343 . . . . . . . . . . . . . 14  |-  ( ( G `  z )  =  0  ->  (
( G `  z
)  e.  ( G
" D )  <->  0  e.  ( G " D ) ) )
261259, 260syl5ibcom 211 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  D )  ->  (
( G `  z
)  =  0  -> 
0  e.  ( G
" D ) ) )
262261necon3bd 2483 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  D )  ->  ( -.  0  e.  ( G " D )  -> 
( G `  z
)  =/=  0 ) )
263252, 262mpd 14 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  D )  ->  ( G `  z )  =/=  0 )
264248, 251, 263divcld 9536 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  D )  ->  (
( F `  z
)  /  ( G `
 z ) )  e.  CC )
265264adantlr 695 . . . . . . . . 9  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  (
( B  -  r
) (,) ( B  +  r ) ) 
C_  I ) )  /\  z  e.  D
)  ->  ( ( F `  z )  /  ( G `  z ) )  e.  CC )
266 eqid 2283 . . . . . . . . 9  |-  ( z  e.  D  |->  ( ( F `  z )  /  ( G `  z ) ) )  =  ( z  e.  D  |->  ( ( F `
 z )  / 
( G `  z
) ) )
267265, 266fmptd 5684 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( z  e.  D  |->  ( ( F `  z )  /  ( G `  z )
) ) : D --> CC )
268 difss 3303 . . . . . . . . . . 11  |-  ( I 
\  { B }
)  C_  I
26958, 268eqsstri 3208 . . . . . . . . . 10  |-  D  C_  I
27013, 61syl6ss 3191 . . . . . . . . . 10  |-  ( ph  ->  I  C_  CC )
271269, 270syl5ss 3190 . . . . . . . . 9  |-  ( ph  ->  D  C_  CC )
272271adantr 451 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  D  C_  CC )
273 eqid 2283 . . . . . . . 8  |-  ( (
TopOpen ` fld )t  ( D  u.  { B } ) )  =  ( ( TopOpen ` fld )t  ( D  u.  { B } ) )
27458uneq1i 3325 . . . . . . . . . . . . . . . . 17  |-  ( D  u.  { B }
)  =  ( ( I  \  { B } )  u.  { B } )
275 undif1 3529 . . . . . . . . . . . . . . . . 17  |-  ( ( I  \  { B } )  u.  { B } )  =  ( I  u.  { B } )
276274, 275eqtri 2303 . . . . . . . . . . . . . . . 16  |-  ( D  u.  { B }
)  =  ( I  u.  { B }
)
277 simprr 733 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) ( B  +  r )
)  C_  I )
27842, 277sstrd 3189 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  { B }  C_  I
)
279 ssequn2 3348 . . . . . . . . . . . . . . . . 17  |-  ( { B }  C_  I  <->  ( I  u.  { B } )  =  I )
280278, 279sylib 188 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( I  u.  { B } )  =  I )
281276, 280syl5eq 2327 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( D  u.  { B } )  =  I )
282281oveq2d 5874 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( TopOpen ` fld )t  ( D  u.  { B } ) )  =  ( ( TopOpen ` fld )t  I
) )
28313adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  I  C_  RR )
284 eqid 2283 . . . . . . . . . . . . . . . 16  |-  ( topGen ` 
ran  (,) )  =  (
topGen `  ran  (,) )
28582, 284rerest 18310 . . . . . . . . . . . . . . 15  |-  ( I 
C_  RR  ->  ( (
TopOpen ` fld )t  I )  =  ( ( topGen `  ran  (,) )t  I
) )
286283, 285syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( TopOpen ` fld )t  I )  =  ( ( topGen `  ran  (,) )t  I
) )
287282, 286eqtrd 2315 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( TopOpen ` fld )t  ( D  u.  { B } ) )  =  ( ( topGen ` 
ran  (,) )t  I ) )
288287fveq2d 5529 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( int `  (
( TopOpen ` fld )t  ( D  u.  { B } ) ) )  =  ( int `  ( ( topGen `  ran  (,) )t  I ) ) )
289288fveq1d 5527 . . . . . . . . . . 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 18292 . . . . . . . . . . . . . . 15  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
291270adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  I  C_  CC )
292 resttopon 16892 . . . . . . . . . . . . . . 15  |-  ( ( ( TopOpen ` fld )  e.  (TopOn `  CC )  /\  I  C_  CC )  ->  (
( TopOpen ` fld )t  I )  e.  (TopOn `  I ) )
293290, 291, 292sylancr 644 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( TopOpen ` fld )t  I )  e.  (TopOn `  I ) )
294 topontop 16664 . . . . . . . . . . . . . 14  |-  ( ( ( TopOpen ` fld )t  I )  e.  (TopOn `  I )  ->  (
( TopOpen ` fld )t  I )  e.  Top )
295293, 294syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( TopOpen ` fld )t  I )  e.  Top )
296286, 295eqeltrrd 2358 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( topGen `  ran  (,) )t  I )  e.  Top )
297 iooretop 18275 . . . . . . . . . . . . . 14  |-  ( ( B  -  r ) (,) ( B  +  r ) )  e.  ( topGen `  ran  (,) )
298297a1i 10 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) ( B  +  r )
)  e.  ( topGen ` 
ran  (,) ) )
2994adantr 451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  I  e.  ( topGen ` 
ran  (,) ) )
300 restopn2 16908 . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . 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 888 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) ( B  +  r )
)  e.  ( (
topGen `  ran  (,) )t  I
) )
303 isopn3i 16819 . . . . . . . . . . . 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 642 . . . . . . . . . . 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 2315 . . . . . . . . . 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 2360 . . . . . . . . 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 3529 . . . . . . . . . . 11  |-  ( ( ( ( B  -  r ) (,) ( B  +  r )
)  \  { B } )  u.  { B } )  =  ( ( ( B  -  r ) (,) ( B  +  r )
)  u.  { B } )
308 ssequn2 3348 . . . . . . . . . . . 12  |-  ( { B }  C_  (
( B  -  r
) (,) ( B  +  r ) )  <-> 
( ( ( B  -  r ) (,) ( B  +  r ) )  u.  { B } )  =  ( ( B  -  r
) (,) ( B  +  r ) ) )
30942, 308sylib 188 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( ( B  -  r ) (,) ( B  +  r ) )  u.  { B } )  =  ( ( B  -  r
) (,) ( B  +  r ) ) )
310307, 309syl5eq 2327 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  u. 
{ B } )  =  ( ( B  -  r ) (,) ( B  +  r ) ) )
311310fveq2d 5529 . . . . . . . . 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 2360 . . . . . . . 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 19236 . . . . . . 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 3188 . . . . . . . . 9  |-  ( ( B  -  r ) (,) B )  C_  CC
315314a1i 10 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  CC )
316173, 61sstri 3188 . . . . . . . . 9  |-  ( B (,) ( B  +  r ) )  C_  CC
317316a1i 10 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r )