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

Theorem lhop 21491
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. This is Metamath 100 proof #64. (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 2443 . . . . 5  |-  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )  =  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )
21rexmet 20371 . . . 4  |-  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )  e.  ( *Met `  RR )
32a1i 11 . . 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 2443 . . . . 5  |-  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )  =  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )
71, 6tgioo 20376 . . . 4  |-  ( topGen ` 
ran  (,) )  =  (
MetOpen `  ( ( abs 
o.  -  )  |`  ( RR  X.  RR ) ) )
87mopni2 20071 . . 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 1218 . 2  |-  ( ph  ->  E. r  e.  RR+  ( B ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  I )
10 elssuni 4124 . . . . . . . . 9  |-  ( I  e.  ( topGen `  ran  (,) )  ->  I  C_  U. ( topGen `
 ran  (,) )
)
11 uniretop 20344 . . . . . . . . 9  |-  RR  =  U. ( topGen `  ran  (,) )
1210, 11syl6sseqr 3406 . . . . . . . 8  |-  ( I  e.  ( topGen `  ran  (,) )  ->  I  C_  RR )
134, 12syl 16 . . . . . . 7  |-  ( ph  ->  I  C_  RR )
1413, 5sseldd 3360 . . . . . 6  |-  ( ph  ->  B  e.  RR )
15 rpre 11000 . . . . . 6  |-  ( r  e.  RR+  ->  r  e.  RR )
161bl2ioo 20372 . . . . . 6  |-  ( ( B  e.  RR  /\  r  e.  RR )  ->  ( B ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) r )  =  ( ( B  -  r ) (,) ( B  +  r )
) )
1714, 15, 16syl2an 477 . . . . 5  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( B
( ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  =  ( ( B  -  r ) (,) ( B  +  r ) ) )
1817sseq1d 3386 . . . 4  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( ( B ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  I  <->  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I
) )
1914adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  B  e.  RR )
20 simprl 755 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
r  e.  RR+ )
2120rpred 11030 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
r  e.  RR )
2219, 21resubcld 9779 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B  -  r
)  e.  RR )
2322rexrd 9436 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B  -  r
)  e.  RR* )
2419, 20ltsubrpd 11058 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B  -  r
)  <  B )
25 lhop.f . . . . . . . . . . 11  |-  ( ph  ->  F : A --> RR )
2625adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  F : A --> RR )
27 ssun1 3522 . . . . . . . . . . . 12  |-  ( ( B  -  r ) (,) B )  C_  ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r ) ) )
28 unass 3516 . . . . . . . . . . . . . . 15  |-  ( ( { B }  u.  ( ( B  -  r ) (,) B
) )  u.  ( B (,) ( B  +  r ) ) )  =  ( { B }  u.  ( (
( B  -  r
) (,) B )  u.  ( B (,) ( B  +  r
) ) ) )
29 uncom 3503 . . . . . . . . . . . . . . . 16  |-  ( { B }  u.  (
( B  -  r
) (,) B ) )  =  ( ( ( B  -  r
) (,) B )  u.  { B }
)
3029uneq1i 3509 . . . . . . . . . . . . . . 15  |-  ( ( { B }  u.  ( ( B  -  r ) (,) B
) )  u.  ( B (,) ( B  +  r ) ) )  =  ( ( ( ( B  -  r
) (,) B )  u.  { B }
)  u.  ( B (,) ( B  +  r ) ) )
3128, 30eqtr3i 2465 . . . . . . . . . . . . . 14  |-  ( { B }  u.  (
( ( B  -  r ) (,) B
)  u.  ( B (,) ( B  +  r ) ) ) )  =  ( ( ( ( B  -  r ) (,) B
)  u.  { B } )  u.  ( B (,) ( B  +  r ) ) )
3219rexrd 9436 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  B  e.  RR* )
3319, 21readdcld 9416 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B  +  r )  e.  RR )
3433rexrd 9436 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B  +  r )  e.  RR* )
3519, 20ltaddrpd 11059 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  B  <  ( B  +  r ) )
36 ioojoin 11419 . . . . . . . . . . . . . . 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 1226 . . . . . . . . . . . . . 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 2487 . . . . . . . . . . . . 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 11344 . . . . . . . . . . . . . . . . 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 661 . . . . . . . . . . . . . . . 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 1171 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  B  e.  ( ( B  -  r ) (,) ( B  +  r ) ) )
4241snssd 4021 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  { B }  C_  (
( B  -  r
) (,) ( B  +  r ) ) )
43 incom 3546 . . . . . . . . . . . . . . 15  |-  ( { B }  i^i  (
( ( B  -  r ) (,) B
)  u.  ( B (,) ( B  +  r ) ) ) )  =  ( ( ( ( B  -  r ) (,) B
)  u.  ( B (,) ( B  +  r ) ) )  i^i  { B }
)
44 ubioo 11335 . . . . . . . . . . . . . . . . . 18  |-  -.  B  e.  ( ( B  -  r ) (,) B
)
45 lbioo 11334 . . . . . . . . . . . . . . . . . 18  |-  -.  B  e.  ( B (,) ( B  +  r )
)
4644, 45pm3.2ni 850 . . . . . . . . . . . . . . . . 17  |-  -.  ( B  e.  ( ( B  -  r ) (,) B )  \/  B  e.  ( B (,) ( B  +  r )
) )
47 elun 3500 . . . . . . . . . . . . . . . . 17  |-  ( B  e.  ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r )
) )  <->  ( B  e.  ( ( B  -  r ) (,) B
)  \/  B  e.  ( B (,) ( B  +  r )
) ) )
4846, 47mtbir 299 . . . . . . . . . . . . . . . 16  |-  -.  B  e.  ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r ) ) )
49 disjsn 3939 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r ) ) )  i^i  { B }
)  =  (/)  <->  -.  B  e.  ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r ) ) ) )
5048, 49mpbir 209 . . . . . . . . . . . . . . 15  |-  ( ( ( ( B  -  r ) (,) B
)  u.  ( B (,) ( B  +  r ) ) )  i^i  { B }
)  =  (/)
5143, 50eqtri 2463 . . . . . . . . . . . . . 14  |-  ( { B }  i^i  (
( ( B  -  r ) (,) B
)  u.  ( B (,) ( B  +  r ) ) ) )  =  (/)
52 uneqdifeq 3770 . . . . . . . . . . . . . 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 662 . . . . . . . . . . . . 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 210 . . . . . . . . . . . 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 3408 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  ( (
( B  -  r
) (,) ( B  +  r ) ) 
\  { B }
) )
56 ssdif 3494 . . . . . . . . . . . . . 14  |-  ( ( ( B  -  r
) (,) ( B  +  r ) ) 
C_  I  ->  (
( ( B  -  r ) (,) ( B  +  r )
)  \  { B } )  C_  (
I  \  { B } ) )
5756ad2antll 728 . . . . . . . . . . . . 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 3406 . . . . . . . . . . . 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 9342 . . . . . . . . . . . . . . . 16  |-  RR  C_  CC
6261a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  RR  C_  CC )
63 fss 5570 . . . . . . . . . . . . . . . 16  |-  ( ( F : A --> RR  /\  RR  C_  CC )  ->  F : A --> CC )
6425, 61, 63sylancl 662 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F : A --> CC )
65 lhop.a . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  C_  RR )
6662, 64, 65dvbss 21379 . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  ( RR  _D  F )  C_  A
)
6760, 66sstrd 3369 . . . . . . . . . . . . 13  |-  ( ph  ->  D  C_  A )
6867adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  D  C_  A )
6959, 68sstrd 3369 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  C_  A
)
7055, 69sstrd 3369 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  A )
71 fssres 5581 . . . . . . . . . 10  |-  ( ( F : A --> RR  /\  ( ( B  -  r ) (,) B
)  C_  A )  ->  ( F  |`  (
( B  -  r
) (,) B ) ) : ( ( B  -  r ) (,) B ) --> RR )
7226, 70, 71syl2anc 661 . . . . . . . . 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 465 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  G : A --> RR )
75 fssres 5581 . . . . . . . . . 10  |-  ( ( G : A --> RR  /\  ( ( B  -  r ) (,) B
)  C_  A )  ->  ( G  |`  (
( B  -  r
) (,) B ) ) : ( ( B  -  r ) (,) B ) --> RR )
7674, 70, 75syl2anc 661 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( G  |`  (
( B  -  r
) (,) B ) ) : ( ( B  -  r ) (,) B ) --> RR )
7761a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  RR  C_  CC )
7864adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  F : A --> CC )
7965adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  A  C_  RR )
80 ioossre 11360 . . . . . . . . . . . . . 14  |-  ( ( B  -  r ) (,) B )  C_  RR
8180a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  RR )
82 eqid 2443 . . . . . . . . . . . . . 14  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
8382tgioo2 20383 . . . . . . . . . . . . . 14  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
8482, 83dvres 21389 . . . . . . . . . . . . 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 1219 . . . . . . . . . . . 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 20343 . . . . . . . . . . . . . 14  |-  ( topGen ` 
ran  (,) )  e.  Top
87 iooretop 20348 . . . . . . . . . . . . . 14  |-  ( ( B  -  r ) (,) B )  e.  ( topGen `  ran  (,) )
88 isopn3i 18689 . . . . . . . . . . . . . 14  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( ( B  -  r ) (,) B )  e.  ( topGen `  ran  (,) )
)  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  (
( B  -  r
) (,) B ) )  =  ( ( B  -  r ) (,) B ) )
8986, 87, 88mp2an 672 . . . . . . . . . . . . 13  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( ( B  -  r ) (,) B
) )  =  ( ( B  -  r
) (,) B )
9089reseq2i 5110 . . . . . . . . . . . 12  |-  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( B  -  r ) (,) B ) ) )  =  ( ( RR 
_D  F )  |`  ( ( B  -  r ) (,) B
) )
9185, 90syl6eq 2491 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( RR  _D  ( F  |`  ( ( B  -  r ) (,) B ) ) )  =  ( ( RR 
_D  F )  |`  ( ( B  -  r ) (,) B
) ) )
9291dmeqd 5045 . . . . . . . . . 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 3369 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  D )
9460adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  D  C_  dom  ( RR 
_D  F ) )
9593, 94sstrd 3369 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  dom  ( RR 
_D  F ) )
96 ssdmres 5135 . . . . . . . . . . 11  |-  ( ( ( B  -  r
) (,) B ) 
C_  dom  ( RR  _D  F )  <->  dom  ( ( RR  _D  F )  |`  ( ( B  -  r ) (,) B
) )  =  ( ( B  -  r
) (,) B ) )
9795, 96sylib 196 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( ( RR  _D  F )  |`  (
( B  -  r
) (,) B ) )  =  ( ( B  -  r ) (,) B ) )
9892, 97eqtrd 2475 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( RR  _D  ( F  |`  ( ( B  -  r ) (,) B ) ) )  =  ( ( B  -  r ) (,) B ) )
99 fss 5570 . . . . . . . . . . . . . . 15  |-  ( ( G : A --> RR  /\  RR  C_  CC )  ->  G : A --> CC )
10073, 61, 99sylancl 662 . . . . . . . . . . . . . 14  |-  ( ph  ->  G : A --> CC )
101100adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  G : A --> CC )
10282, 83dvres 21389 . . . . . . . . . . . . 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 1219 . . . . . . . . . . . 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 5110 . . . . . . . . . . . 12  |-  ( ( RR  _D  G )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( B  -  r ) (,) B ) ) )  =  ( ( RR 
_D  G )  |`  ( ( B  -  r ) (,) B
) )
105103, 104syl6eq 2491 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) )  =  ( ( RR 
_D  G )  |`  ( ( B  -  r ) (,) B
) ) )
106105dmeqd 5045 . . . . . . . . . 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 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  D  C_  dom  ( RR 
_D  G ) )
10993, 108sstrd 3369 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  dom  ( RR 
_D  G ) )
110 ssdmres 5135 . . . . . . . . . . 11  |-  ( ( ( B  -  r
) (,) B ) 
C_  dom  ( RR  _D  G )  <->  dom  ( ( RR  _D  G )  |`  ( ( B  -  r ) (,) B
) )  =  ( ( B  -  r
) (,) B ) )
111109, 110sylib 196 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( ( RR  _D  G )  |`  (
( B  -  r
) (,) B ) )  =  ( ( B  -  r ) (,) B ) )
112106, 111eqtrd 2475 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) )  =  ( ( B  -  r ) (,) B ) )
113 limcresi 21363 . . . . . . . . . 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 465 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( F lim
CC  B ) )
116113, 115sseldi 3357 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( ( F  |`  ( ( B  -  r ) (,) B ) ) lim CC  B ) )
117 limcresi 21363 . . . . . . . . . 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 465 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( G lim
CC  B ) )
120117, 119sseldi 3357 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( ( G  |`  ( ( B  -  r ) (,) B ) ) lim CC  B ) )
121 df-ima 4856 . . . . . . . . . . 11  |-  ( G
" ( ( B  -  r ) (,) B ) )  =  ran  ( G  |`  ( ( B  -  r ) (,) B
) )
122 imass2 5207 . . . . . . . . . . . 12  |-  ( ( ( B  -  r
) (,) B ) 
C_  D  ->  ( G " ( ( B  -  r ) (,) B ) )  C_  ( G " D ) )
12393, 122syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( G " (
( B  -  r
) (,) B ) )  C_  ( G " D ) )
124121, 123syl5eqssr 3404 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  ran  ( G  |`  (
( B  -  r
) (,) B ) )  C_  ( G " D ) )
125 lhop.gn0 . . . . . . . . . . 11  |-  ( ph  ->  -.  0  e.  ( G " D ) )
126125adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  ( G " D ) )
127124, 126ssneldd 3362 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  ran  ( G  |`  ( ( B  -  r ) (,) B ) ) )
128105rneqd 5070 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  ran  ( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) )  =  ran  ( ( RR  _D  G )  |`  ( ( B  -  r ) (,) B
) ) )
129 df-ima 4856 . . . . . . . . . . . 12  |-  ( ( RR  _D  G )
" ( ( B  -  r ) (,) B ) )  =  ran  ( ( RR 
_D  G )  |`  ( ( B  -  r ) (,) B
) )
130128, 129syl6eqr 2493 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  ran  ( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) )  =  ( ( RR 
_D  G ) "
( ( B  -  r ) (,) B
) ) )
131 imass2 5207 . . . . . . . . . . . 12  |-  ( ( ( B  -  r
) (,) B ) 
C_  D  ->  (
( RR  _D  G
) " ( ( B  -  r ) (,) B ) ) 
C_  ( ( RR 
_D  G ) " D ) )
13293, 131syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( RR  _D  G ) " (
( B  -  r
) (,) B ) )  C_  ( ( RR  _D  G ) " D ) )
133130, 132eqsstrd 3393 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  ran  ( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) ) 
C_  ( ( RR 
_D  G ) " D ) )
134 lhop.gd0 . . . . . . . . . . 11  |-  ( ph  ->  -.  0  e.  ( ( RR  _D  G
) " D ) )
135134adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  (
( RR  _D  G
) " D ) )
136133, 135ssneldd 3362 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  ran  ( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) ) )
137 limcresi 21363 . . . . . . . . . . 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 )
138 resmpt 5159 . . . . . . . . . . . . . 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 ) ) ) )
13993, 138syl 16 . . . . . . . . . . . . 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 ) ) ) )
14091fveq1d 5696 . . . . . . . . . . . . . . . 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
) )
141 fvres 5707 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( ( B  -  r ) (,) B )  ->  (
( ( RR  _D  F )  |`  (
( B  -  r
) (,) B ) ) `  z )  =  ( ( RR 
_D  F ) `  z ) )
142140, 141sylan9eq 2495 . . . . . . . . . . . . . . 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 )
)
143105fveq1d 5696 . . . . . . . . . . . . . . . 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
) )
144 fvres 5707 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( ( B  -  r ) (,) B )  ->  (
( ( RR  _D  G )  |`  (
( B  -  r
) (,) B ) ) `  z )  =  ( ( RR 
_D  G ) `  z ) )
145143, 144sylan9eq 2495 . . . . . . . . . . . . . . 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 )
)
146142, 145oveq12d 6112 . . . . . . . . . . . . . 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 ) ) )
147146mpteq2dva 4381 . . . . . . . . . . . . 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 ) ) ) )
148139, 147eqtr4d 2478 . . . . . . . . . . . 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 ) ) ) )
149148oveq1d 6109 . . . . . . . . . . 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 ) )
150137, 149syl5sseq 3407 . . . . . . . . . 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 ) )
151 lhop.c . . . . . . . . . . 11  |-  ( ph  ->  C  e.  ( ( z  e.  D  |->  ( ( ( RR  _D  F ) `  z
)  /  ( ( RR  _D  G ) `
 z ) ) ) lim CC  B ) )
152151adantr 465 . . . . . . . . . 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 ) )
153150, 152sseldd 3360 . . . . . . . . 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 ) )
15423, 19, 24, 72, 76, 98, 112, 116, 120, 127, 136, 153lhop2 21490 . . . . . . . 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 ) )
155 resmpt 5159 . . . . . . . . . . 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 ) ) ) )
15655, 155syl 16 . . . . . . . . . 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 ) ) ) )
157 fvres 5707 . . . . . . . . . . . 12  |-  ( z  e.  ( ( B  -  r ) (,) B )  ->  (
( F  |`  (
( B  -  r
) (,) B ) ) `  z )  =  ( F `  z ) )
158 fvres 5707 . . . . . . . . . . . 12  |-  ( z  e.  ( ( B  -  r ) (,) B )  ->  (
( G  |`  (
( B  -  r
) (,) B ) ) `  z )  =  ( G `  z ) )
159157, 158oveq12d 6112 . . . . . . . . . . 11  |-  ( z  e.  ( ( B  -  r ) (,) B )  ->  (
( ( F  |`  ( ( B  -  r ) (,) B
) ) `  z
)  /  ( ( G  |`  ( ( B  -  r ) (,) B ) ) `  z ) )  =  ( ( F `  z )  /  ( G `  z )
) )
160159mpteq2ia 4377 . . . . . . . . . 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 )
) )
161156, 160syl6eqr 2493 . . . . . . . . 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 ) ) ) )
162161oveq1d 6109 . . . . . . . 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 ) )
163154, 162eleqtrrd 2520 . . . . . . 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
) )
164 ssun2 3523 . . . . . . . . . . . 12  |-  ( B (,) ( B  +  r ) )  C_  ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r ) ) )
165164, 54syl5sseqr 3408 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  ( (
( B  -  r
) (,) ( B  +  r ) ) 
\  { B }
) )
166165, 69sstrd 3369 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  A )
167 fssres 5581 . . . . . . . . . 10  |-  ( ( F : A --> RR  /\  ( B (,) ( B  +  r ) ) 
C_  A )  -> 
( F  |`  ( B (,) ( B  +  r ) ) ) : ( B (,) ( B  +  r
) ) --> RR )
16826, 166, 167syl2anc 661 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( F  |`  ( B (,) ( B  +  r ) ) ) : ( B (,) ( B  +  r
) ) --> RR )
169 fssres 5581 . . . . . . . . . 10  |-  ( ( G : A --> RR  /\  ( B (,) ( B  +  r ) ) 
C_  A )  -> 
( G  |`  ( B (,) ( B  +  r ) ) ) : ( B (,) ( B  +  r
) ) --> RR )
17074, 166, 169syl2anc 661 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( G  |`  ( B (,) ( B  +  r ) ) ) : ( B (,) ( B  +  r
) ) --> RR )
171 ioossre 11360 . . . . . . . . . . . . . 14  |-  ( B (,) ( B  +  r ) )  C_  RR
172171a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  RR )
17382, 83dvres 21389 . . . . . . . . . . . . 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 ) ) ) ) )
17477, 78, 79, 172, 173syl22anc 1219 . . . . . . . . . . . 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 ) ) ) ) )
175 iooretop 20348 . . . . . . . . . . . . . 14  |-  ( B (,) ( B  +  r ) )  e.  ( topGen `  ran  (,) )
176 isopn3i 18689 . . . . . . . . . . . . . 14  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( B (,) ( B  +  r ) )  e.  ( topGen `  ran  (,) )
)  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  ( B (,) ( B  +  r ) ) )  =  ( B (,) ( B  +  r
) ) )
17786, 175, 176mp2an 672 . . . . . . . . . . . . 13  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( B (,) ( B  +  r ) ) )  =  ( B (,) ( B  +  r ) )
178177reseq2i 5110 . . . . . . . . . . . 12  |-  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( B (,) ( B  +  r ) ) ) )  =  ( ( RR 
_D  F )  |`  ( B (,) ( B  +  r ) ) )
179174, 178syl6eq 2491 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( RR  _D  ( F  |`  ( B (,) ( B  +  r
) ) ) )  =  ( ( RR 
_D  F )  |`  ( B (,) ( B  +  r ) ) ) )
180179dmeqd 5045 . . . . . . . . . 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 )
) ) )
181165, 59sstrd 3369 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  D )
182181, 94sstrd 3369 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  dom  ( RR 
_D  F ) )
183 ssdmres 5135 . . . . . . . . . . 11  |-  ( ( B (,) ( B  +  r ) ) 
C_  dom  ( RR  _D  F )  <->  dom  ( ( RR  _D  F )  |`  ( B (,) ( B  +  r )
) )  =  ( B (,) ( B  +  r ) ) )
184182, 183sylib 196 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( ( RR  _D  F )  |`  ( B (,) ( B  +  r ) ) )  =  ( B (,) ( B  +  r
) ) )
185180, 184eqtrd 2475 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( RR  _D  ( F  |`  ( B (,) ( B  +  r
) ) ) )  =  ( B (,) ( B  +  r
) ) )
18682, 83dvres 21389 . . . . . . . . . . . . 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 ) ) ) ) )
18777, 101, 79, 172, 186syl22anc 1219 . . . . . . . . . . . 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 ) ) ) ) )
188177reseq2i 5110 . . . . . . . . . . . 12  |-  ( ( RR  _D  G )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( B (,) ( B  +  r ) ) ) )  =  ( ( RR 
_D  G )  |`  ( B (,) ( B  +  r ) ) )
189187, 188syl6eq 2491 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( RR  _D  ( G  |`  ( B (,) ( B  +  r
) ) ) )  =  ( ( RR 
_D  G )  |`  ( B (,) ( B  +  r ) ) ) )
190189dmeqd 5045 . . . . . . . . . 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 )
) ) )
191181, 108sstrd 3369 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  dom  ( RR 
_D  G ) )
192 ssdmres 5135 . . . . . . . . . . 11  |-  ( ( B (,) ( B  +  r ) ) 
C_  dom  ( RR  _D  G )  <->  dom  ( ( RR  _D  G )  |`  ( B (,) ( B  +  r )
) )  =  ( B (,) ( B  +  r ) ) )
193191, 192sylib 196 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( ( RR  _D  G )  |`  ( B (,) ( B  +  r ) ) )  =  ( B (,) ( B  +  r
) ) )
194190, 193eqtrd 2475 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( RR  _D  ( G  |`  ( B (,) ( B  +  r
) ) ) )  =  ( B (,) ( B  +  r
) ) )
195 limcresi 21363 . . . . . . . . . 10  |-  ( F lim
CC  B )  C_  ( ( F  |`  ( B (,) ( B  +  r ) ) ) lim CC  B )
196195, 115sseldi 3357 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( ( F  |`  ( B (,) ( B  +  r ) ) ) lim CC  B ) )
197 limcresi 21363 . . . . . . . . . 10  |-  ( G lim
CC  B )  C_  ( ( G  |`  ( B (,) ( B  +  r ) ) ) lim CC  B )
198197, 119sseldi 3357 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( ( G  |`  ( B (,) ( B  +  r ) ) ) lim CC  B ) )
199 df-ima 4856 . . . . . . . . . . 11  |-  ( G
" ( B (,) ( B  +  r
) ) )  =  ran  ( G  |`  ( B (,) ( B  +  r ) ) )
200 imass2 5207 . . . . . . . . . . . 12  |-  ( ( B (,) ( B  +  r ) ) 
C_  D  ->  ( G " ( B (,) ( B  +  r
) ) )  C_  ( G " D ) )
201181, 200syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( G " ( B (,) ( B  +  r ) ) ) 
C_  ( G " D ) )
202199, 201syl5eqssr 3404 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  ran  ( G  |`  ( B (,) ( B  +  r ) ) ) 
C_  ( G " D ) )
203202, 126ssneldd 3362 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  ran  ( G  |`  ( B (,) ( B  +  r ) ) ) )
204189rneqd 5070 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  ran  ( RR  _D  ( G  |`  ( B (,) ( B  +  r
) ) ) )  =  ran  ( ( RR  _D  G )  |`  ( B (,) ( B  +  r )
) ) )
205 df-ima 4856 . . . . . . . . . . . 12  |-  ( ( RR  _D  G )
" ( B (,) ( B  +  r
) ) )  =  ran  ( ( RR 
_D  G )  |`  ( B (,) ( B  +  r ) ) )
206204, 205syl6eqr 2493 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  ran  ( RR  _D  ( G  |`  ( B (,) ( B  +  r
) ) ) )  =  ( ( RR 
_D  G ) "
( B (,) ( B  +  r )
) ) )
207 imass2 5207 . . . . . . . . . . . 12  |-  ( ( B (,) ( B  +  r ) ) 
C_  D  ->  (
( RR  _D  G
) " ( B (,) ( B  +  r ) ) ) 
C_  ( ( RR 
_D  G ) " D ) )
208181, 207syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( RR  _D  G ) " ( B (,) ( B  +  r ) ) ) 
C_  ( ( RR 
_D  G ) " D ) )
209206, 208eqsstrd 3393 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  ran  ( RR  _D  ( G  |`  ( B (,) ( B  +  r
) ) ) ) 
C_  ( ( RR 
_D  G ) " D ) )
210209, 135ssneldd 3362 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  ran  ( RR  _D  ( G  |`  ( B (,) ( B  +  r
) ) ) ) )
211 limcresi 21363 . . . . . . . . . . 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 )
212 resmpt 5159 . . . . . . . . . . . . . 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
) ) ) )
213181, 212syl 16 . . . . . . . . . . . . 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 ) ) ) )
214179fveq1d 5696 . . . . . . . . . . . . . . . 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
) )
215 fvres 5707 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( B (,) ( B  +  r
) )  ->  (
( ( RR  _D  F )  |`  ( B (,) ( B  +  r ) ) ) `
 z )  =  ( ( RR  _D  F ) `  z
) )
216214, 215sylan9eq 2495 . . . . . . . . . . . . . . 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 ) )
217189fveq1d 5696 . . . . . . . . . . . . . . . 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
) )
218 fvres 5707 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( B (,) ( B  +  r
) )  ->  (
( ( RR  _D  G )  |`  ( B (,) ( B  +  r ) ) ) `
 z )  =  ( ( RR  _D  G ) `  z
) )
219217, 218sylan9eq 2495 . . . . . . . . . . . . . . 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 ) )
220216, 219oveq12d 6112 . . . . . . . . . . . . . 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 ) ) )
221220mpteq2dva 4381 . . . . . . . . . . . . 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
) ) ) )
222213, 221eqtr4d 2478 . . . . . . . . . . . 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 ) ) ) )
223222oveq1d 6109 . . . . . . . . . . 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 ) )
224211, 223syl5sseq 3407 . . . . . . . . . 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 ) )
225224, 152sseldd 3360 . . . . . . . . 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 ) )
22619, 34, 35, 168, 170, 185, 194, 196, 198, 203, 210, 225lhop1 21489 . . . . . . . 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 ) )
227 resmpt 5159 . . . . . . . . . . 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 ) ) ) )
228165, 227syl 16 . . . . . . . . . 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 ) ) ) )
229 fvres 5707 . . . . . . . . . . . 12  |-  ( z  e.  ( B (,) ( B  +  r
) )  ->  (
( F  |`  ( B (,) ( B  +  r ) ) ) `
 z )  =  ( F `  z
) )
230 fvres 5707 . . . . . . . . . . . 12  |-  ( z  e.  ( B (,) ( B  +  r
) )  ->  (
( G  |`  ( B (,) ( B  +  r ) ) ) `
 z )  =  ( G `  z
) )
231229, 230oveq12d 6112 . . . . . . . . . . 11  |-  ( z  e.  ( B (,) ( B  +  r
) )  ->  (
( ( F  |`  ( B (,) ( B  +  r ) ) ) `  z )  /  ( ( G  |`  ( B (,) ( B  +  r )
) ) `  z
) )  =  ( ( F `  z
)  /  ( G `
 z ) ) )
232231mpteq2ia 4377 . . . . . . . . . 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 ) ) )
233228, 232syl6eqr 2493 . . . . . . . . 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
) ) ) )
234233oveq1d 6109 . . . . . . . 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 ) )
235226, 234eleqtrrd 2520 . . . . . . 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
) )
236163, 235elind 3543 . . . . . 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
) ) )
237 resmpt 5159 . . . . . . . . 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 ) ) ) )
23859, 237syl 16 . . . . . . . 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 ) ) ) )
239238oveq1d 6109 . . . . . . 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 ) )
24067sselda 3359 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  D )  ->  z  e.  A )
24125ffvelrnda 5846 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  A )  ->  ( F `  z )  e.  RR )
242240, 241syldan 470 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  D )  ->  ( F `  z )  e.  RR )
243242recnd 9415 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  D )  ->  ( F `  z )  e.  CC )
24473ffvelrnda 5846 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  A )  ->  ( G `  z )  e.  RR )
245240, 244syldan 470 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  D )  ->  ( G `  z )  e.  RR )
246245recnd 9415 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  D )  ->  ( G `  z )  e.  CC )
247125adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  D )  ->  -.  0  e.  ( G " D ) )
248 ffn 5562 . . . . . . . . . . . . . . . . 17  |-  ( G : A --> RR  ->  G  Fn  A )
24973, 248syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  G  Fn  A )
250249adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  D )  ->  G  Fn  A )
25167adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  D )  ->  D  C_  A )
252 simpr 461 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  D )  ->  z  e.  D )
253 fnfvima 5958 . . . . . . . . . . . . . . 15  |-  ( ( G  Fn  A  /\  D  C_  A  /\  z  e.  D )  ->  ( G `  z )  e.  ( G " D
) )
254250, 251, 252, 253syl3anc 1218 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  z  e.  D )  ->  ( G `  z )  e.  ( G " D
) )
255 eleq1 2503 . . . . . . . . . . . . . 14  |-  ( ( G `  z )  =  0  ->  (
( G `  z
)  e.  ( G
" D )  <->  0  e.  ( G " D ) ) )
256254, 255syl5ibcom 220 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  D )  ->  (
( G `  z
)  =  0  -> 
0  e.  ( G
" D ) ) )
257256necon3bd 2648 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  D )  ->  ( -.  0  e.  ( G " D )  -> 
( G `  z
)  =/=  0 ) )
258247, 257mpd 15 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  D )  ->  ( G `  z )  =/=  0 )
259243, 246, 258divcld 10110 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  D )  ->  (
( F `  z
)  /  ( G `
 z ) )  e.  CC )
260259adantlr 714 . . . . . . . . 9  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  (
( B  -  r
) (,) ( B  +  r ) ) 
C_  I ) )  /\  z  e.  D
)  ->  ( ( F `  z )  /  ( G `  z ) )  e.  CC )
261 eqid 2443 . . . . . . . . 9  |-  ( z  e.  D  |->  ( ( F `  z )  /  ( G `  z ) ) )  =  ( z  e.  D  |->  ( ( F `
 z )  / 
( G `  z
) ) )
262260, 261fmptd 5870 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( z  e.  D  |->  ( ( F `  z )  /  ( G `  z )
) ) : D --> CC )
263 difss 3486 . . . . . . . . . . 11  |-  ( I 
\  { B }
)  C_  I
26458, 263eqsstri 3389 . . . . . . . . . 10  |-  D  C_  I
26513, 61syl6ss 3371 . . . . . . . . . 10  |-  ( ph  ->  I  C_  CC )
266264, 265syl5ss 3370 . . . . . . . . 9  |-  ( ph  ->  D  C_  CC )
267266adantr 465 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  D  C_  CC )
268 eqid 2443 . . . . . . . 8  |-  ( (
TopOpen ` fld )t  ( D  u.  { B } ) )  =  ( ( TopOpen ` fld )t  ( D  u.  { B } ) )
26958uneq1i 3509 . . . . . . . . . . . . . . . . 17  |-  ( D  u.  { B }
)  =  ( ( I  \  { B } )  u.  { B } )
270 undif1 3757 . . . . . . . . . . . . . . . . 17  |-  ( ( I  \  { B } )  u.  { B } )  =  ( I  u.  { B } )
271269, 270eqtri 2463 . . . . . . . . . . . . . . . 16  |-  ( D  u.  { B }
)  =  ( I  u.  { B }
)
272 simprr 756 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) ( B  +  r )
)  C_  I )
27342, 272sstrd 3369 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  { B }  C_  I
)
274 ssequn2 3532 . . . . . . . . . . . . . . . . 17  |-  ( { B }  C_  I  <->  ( I  u.  { B } )  =  I )
275273, 274sylib 196 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( I  u.  { B } )  =  I )
276271, 275syl5eq 2487 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( D  u.  { B } )  =  I )
277276oveq2d 6110 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( TopOpen ` fld )t  ( D  u.  { B } ) )  =  ( ( TopOpen ` fld )t  I
) )
27813adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  I  C_  RR )
279 eqid 2443 . . . . . . . . . . . . . . . 16  |-  ( topGen ` 
ran  (,) )  =  (
topGen `  ran  (,) )
28082, 279rerest 20384 . . . . . . . . . . . . . . 15  |-  ( I 
C_  RR  ->  ( (
TopOpen ` fld )t  I )  =  ( ( topGen `  ran  (,) )t  I
) )
281278, 280syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( TopOpen ` fld )t  I )  =  ( ( topGen `  ran  (,) )t  I
) )
282277, 281eqtrd 2475 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( TopOpen ` fld )t  ( D  u.  { B } ) )  =  ( ( topGen ` 
ran  (,) )t  I ) )
283282fveq2d 5698 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( int `  (
( TopOpen ` fld )t  ( D  u.  { B } ) ) )  =  ( int `  ( ( topGen `  ran  (,) )t  I ) ) )
284283fveq1d 5696 . . . . . . . . . . 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 )
) ) )
28582cnfldtopon 20365 . . . . . . . . . . . . . . 15  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
286265adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  I  C_  CC )
287 resttopon 18768 . . . . . . . . . . . . . . 15  |-  ( ( ( TopOpen ` fld )  e.  (TopOn `  CC )  /\  I  C_  CC )  ->  (
( TopOpen ` fld )t  I )  e.  (TopOn `  I ) )
288285, 286, 287sylancr 663 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( TopOpen ` fld )t  I )  e.  (TopOn `  I ) )
289 topontop 18534 . . . . . . . . . . . . . 14  |-  ( ( ( TopOpen ` fld )t  I )  e.  (TopOn `  I )  ->  (
( TopOpen ` fld )t  I )  e.  Top )
290288, 289syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( TopOpen ` fld )t  I )  e.  Top )
291281, 290eqeltrrd 2518 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( topGen `  ran  (,) )t  I )  e.  Top )
292 iooretop 20348 . . . . . . . . . . . . . 14  |-  ( ( B  -  r ) (,) ( B  +  r ) )  e.  ( topGen `  ran  (,) )
293292a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) ( B  +  r )
)  e.  ( topGen ` 
ran  (,) ) )
2944adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  I  e.  ( topGen ` 
ran  (,) ) )
295 restopn2 18784 . . . . . . . . . . . . . 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 ) ) )
29686, 294, 295sylancr 663 . . . . . . . . . . . . 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 )
) )
297293, 272, 296mpbir2and 913 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) ( B  +  r )
)  e.  ( (
topGen `  ran  (,) )t  I
) )
298 isopn3i 18689 . . . . . . . . . . . 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 ) ) )
299291, 297, 298syl2anc 661 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( int `  (
( topGen `  ran  (,) )t  I
) ) `  (
( B  -  r
) (,) ( B  +  r ) ) )  =  ( ( B  -  r ) (,) ( B  +  r ) ) )
300284, 299eqtrd 2475 . . . . . . . . . 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 ) ) )
30141, 300eleqtrrd 2520 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  B  e.  ( ( int `  ( ( TopOpen ` fld )t  ( D  u.  { B } ) ) ) `
 ( ( B  -  r ) (,) ( B  +  r ) ) ) )
302 undif1 3757 . . . . . . . . . . 11  |-  ( ( ( ( B  -  r ) (,) ( B  +  r )
)  \  { B } )  u.  { B } )  =  ( ( ( B  -  r ) (,) ( B  +  r )
)  u.  { B } )
303 ssequn2 3532 . . . . . . . . . . . 12  |-  ( { B }  C_  (
( B  -  r
) (,) ( B  +  r ) )  <-> 
( ( ( B  -  r ) (,) ( B  +  r ) )  u.  { B } )  =  ( ( B  -  r
) (,) ( B  +  r ) ) )
30442, 303sylib 196 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( ( B  -  r ) (,) ( B  +  r ) )  u.  { B } )  =  ( ( B  -  r
) (,) ( B  +  r ) ) )
305302, 304syl5eq 2487 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  u. 
{ B } )  =  ( ( B  -  r ) (,) ( B  +  r ) ) )
306305fveq2d 5698 . . . . . . . . 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 ) ) ) )
307301, 306eleqtrrd 2520 . . . . . . . 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 } ) ) )
308262, 59, 267, 82, 268, 307limcres 21364 . . . . . . 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
) )
30980, 61sstri 3368 . . . . . . . . 9  |-  ( ( B  -  r ) (,) B )  C_  CC
310309a1i 11 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  CC )
311171, 61sstri 3368 . . . . . . . . 9  |-  ( B (,) ( B  +  r ) )  C_  CC
312311a1i 11 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  CC )
31359sselda 3359 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  (
( B  -  r
) (,) ( B  +  r ) ) 
C_  I ) )  /\  z  e.  ( ( ( B  -  r ) (,) ( B  +  r )
)  \  { B } ) )  -> 
z  e.  D )
314313, 260syldan 470 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  (
( B  -  r
) (,) ( B  +  r ) ) 
C_  I ) )  /\  z  e.  ( ( ( B  -  r ) (,) ( B  +  r )
)  \  { B } ) )  -> 
( ( F `  z )  /  ( G `  z )
)  e.  CC )
315 eqid 2443 . . . . . . . . . 10  |-  ( z  e.  ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  |->  ( ( F `  z
)  /  ( G `
 z ) ) )  =  ( z  e.  ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  |->  ( ( F `  z
)  /  ( G `
 z ) ) )
316314, 315fmptd 5870 . . . . . . . . 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  +  r ) )  \  { B } ) --> CC )
31754feq2d 5550 . . . . . . . . 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  +  r ) )  \  { B } ) --> CC  <->  ( z  e.  ( ( ( B  -  r
) (,) ( B  +  r ) ) 
\  { B }
)  |->  ( ( F `
 z )  / 
( G `  z
) ) ) : ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r ) ) ) --> CC ) )
318316, 317mpbid 210 . . . . . . . 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 )  u.  ( B