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

Theorem lhop 22583
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 2454 . . . . 5  |-  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )  =  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )
21rexmet 21462 . . . 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 2454 . . . . 5  |-  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )  =  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )
71, 6tgioo 21467 . . . 4  |-  ( topGen ` 
ran  (,) )  =  (
MetOpen `  ( ( abs 
o.  -  )  |`  ( RR  X.  RR ) ) )
87mopni2 21162 . . 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 1226 . 2  |-  ( ph  ->  E. r  e.  RR+  ( B ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  I )
10 elssuni 4264 . . . . . . . . 9  |-  ( I  e.  ( topGen `  ran  (,) )  ->  I  C_  U. ( topGen `
 ran  (,) )
)
11 uniretop 21435 . . . . . . . . 9  |-  RR  =  U. ( topGen `  ran  (,) )
1210, 11syl6sseqr 3536 . . . . . . . 8  |-  ( I  e.  ( topGen `  ran  (,) )  ->  I  C_  RR )
134, 12syl 16 . . . . . . 7  |-  ( ph  ->  I  C_  RR )
1413, 5sseldd 3490 . . . . . 6  |-  ( ph  ->  B  e.  RR )
15 rpre 11227 . . . . . 6  |-  ( r  e.  RR+  ->  r  e.  RR )
161bl2ioo 21463 . . . . . 6  |-  ( ( B  e.  RR  /\  r  e.  RR )  ->  ( B ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) r )  =  ( ( B  -  r ) (,) ( B  +  r )
) )
1714, 15, 16syl2an 475 . . . . 5  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( B
( ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  =  ( ( B  -  r ) (,) ( B  +  r ) ) )
1817sseq1d 3516 . . . 4  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( ( B ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  I  <->  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I
) )
1914adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  B  e.  RR )
20 simprl 754 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
r  e.  RR+ )
2120rpred 11259 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
r  e.  RR )
2219, 21resubcld 9983 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B  -  r
)  e.  RR )
2322rexrd 9632 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B  -  r
)  e.  RR* )
2419, 20ltsubrpd 11287 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B  -  r
)  <  B )
25 lhop.f . . . . . . . . . . 11  |-  ( ph  ->  F : A --> RR )
2625adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  F : A --> RR )
27 ssun1 3653 . . . . . . . . . . . 12  |-  ( ( B  -  r ) (,) B )  C_  ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r ) ) )
28 unass 3647 . . . . . . . . . . . . . . 15  |-  ( ( { B }  u.  ( ( B  -  r ) (,) B
) )  u.  ( B (,) ( B  +  r ) ) )  =  ( { B }  u.  ( (
( B  -  r
) (,) B )  u.  ( B (,) ( B  +  r
) ) ) )
29 uncom 3634 . . . . . . . . . . . . . . . 16  |-  ( { B }  u.  (
( B  -  r
) (,) B ) )  =  ( ( ( B  -  r
) (,) B )  u.  { B }
)
3029uneq1i 3640 . . . . . . . . . . . . . . 15  |-  ( ( { B }  u.  ( ( B  -  r ) (,) B
) )  u.  ( B (,) ( B  +  r ) ) )  =  ( ( ( ( B  -  r
) (,) B )  u.  { B }
)  u.  ( B (,) ( B  +  r ) ) )
3128, 30eqtr3i 2485 . . . . . . . . . . . . . 14  |-  ( { B }  u.  (
( ( B  -  r ) (,) B
)  u.  ( B (,) ( B  +  r ) ) ) )  =  ( ( ( ( B  -  r ) (,) B
)  u.  { B } )  u.  ( B (,) ( B  +  r ) ) )
3219rexrd 9632 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  B  e.  RR* )
3319, 21readdcld 9612 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B  +  r )  e.  RR )
3433rexrd 9632 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B  +  r )  e.  RR* )
3519, 20ltaddrpd 11288 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  B  <  ( B  +  r ) )
36 ioojoin 11654 . . . . . . . . . . . . . . 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 1234 . . . . . . . . . . . . . 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 2507 . . . . . . . . . . . . 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 11573 . . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . . 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 1177 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  B  e.  ( ( B  -  r ) (,) ( B  +  r ) ) )
4241snssd 4161 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  { B }  C_  (
( B  -  r
) (,) ( B  +  r ) ) )
43 incom 3677 . . . . . . . . . . . . . . 15  |-  ( { B }  i^i  (
( ( B  -  r ) (,) B
)  u.  ( B (,) ( B  +  r ) ) ) )  =  ( ( ( ( B  -  r ) (,) B
)  u.  ( B (,) ( B  +  r ) ) )  i^i  { B }
)
44 ubioo 11564 . . . . . . . . . . . . . . . . . 18  |-  -.  B  e.  ( ( B  -  r ) (,) B
)
45 lbioo 11563 . . . . . . . . . . . . . . . . . 18  |-  -.  B  e.  ( B (,) ( B  +  r )
)
4644, 45pm3.2ni 852 . . . . . . . . . . . . . . . . 17  |-  -.  ( B  e.  ( ( B  -  r ) (,) B )  \/  B  e.  ( B (,) ( B  +  r )
) )
47 elun 3631 . . . . . . . . . . . . . . . . 17  |-  ( B  e.  ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r )
) )  <->  ( B  e.  ( ( B  -  r ) (,) B
)  \/  B  e.  ( B (,) ( B  +  r )
) ) )
4846, 47mtbir 297 . . . . . . . . . . . . . . . 16  |-  -.  B  e.  ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r ) ) )
49 disjsn 4076 . . . . . . . . . . . . . . . 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 2483 . . . . . . . . . . . . . 14  |-  ( { B }  i^i  (
( ( B  -  r ) (,) B
)  u.  ( B (,) ( B  +  r ) ) ) )  =  (/)
52 uneqdifeq 3904 . . . . . . . . . . . . . 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 660 . . . . . . . . . . . . 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 3538 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  ( (
( B  -  r
) (,) ( B  +  r ) ) 
\  { B }
) )
56 ssdif 3625 . . . . . . . . . . . . . 14  |-  ( ( ( B  -  r
) (,) ( B  +  r ) ) 
C_  I  ->  (
( ( B  -  r ) (,) ( B  +  r )
)  \  { B } )  C_  (
I  \  { B } ) )
5756ad2antll 726 . . . . . . . . . . . . 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 3536 . . . . . . . . . . . 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 9538 . . . . . . . . . . . . . . . 16  |-  RR  C_  CC
6261a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  RR  C_  CC )
63 fss 5721 . . . . . . . . . . . . . . . 16  |-  ( ( F : A --> RR  /\  RR  C_  CC )  ->  F : A --> CC )
6425, 61, 63sylancl 660 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F : A --> CC )
65 lhop.a . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  C_  RR )
6662, 64, 65dvbss 22471 . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  ( RR  _D  F )  C_  A
)
6760, 66sstrd 3499 . . . . . . . . . . . . 13  |-  ( ph  ->  D  C_  A )
6867adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  D  C_  A )
6959, 68sstrd 3499 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  C_  A
)
7055, 69sstrd 3499 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  A )
7126, 70fssresd 5734 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( F  |`  (
( B  -  r
) (,) B ) ) : ( ( B  -  r ) (,) B ) --> RR )
72 lhop.g . . . . . . . . . . 11  |-  ( ph  ->  G : A --> RR )
7372adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  G : A --> RR )
7473, 70fssresd 5734 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( G  |`  (
( B  -  r
) (,) B ) ) : ( ( B  -  r ) (,) B ) --> RR )
7561a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  RR  C_  CC )
7664adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  F : A --> CC )
7765adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  A  C_  RR )
78 ioossre 11589 . . . . . . . . . . . . . 14  |-  ( ( B  -  r ) (,) B )  C_  RR
7978a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  RR )
80 eqid 2454 . . . . . . . . . . . . . 14  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
8180tgioo2 21474 . . . . . . . . . . . . . 14  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
8280, 81dvres 22481 . . . . . . . . . . . . 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 ) ) ) )
8375, 76, 77, 79, 82syl22anc 1227 . . . . . . . . . . . 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 ) ) ) )
84 retop 21434 . . . . . . . . . . . . . 14  |-  ( topGen ` 
ran  (,) )  e.  Top
85 iooretop 21439 . . . . . . . . . . . . . 14  |-  ( ( B  -  r ) (,) B )  e.  ( topGen `  ran  (,) )
86 isopn3i 19750 . . . . . . . . . . . . . 14  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( ( B  -  r ) (,) B )  e.  ( topGen `  ran  (,) )
)  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  (
( B  -  r
) (,) B ) )  =  ( ( B  -  r ) (,) B ) )
8784, 85, 86mp2an 670 . . . . . . . . . . . . 13  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( ( B  -  r ) (,) B
) )  =  ( ( B  -  r
) (,) B )
8887reseq2i 5259 . . . . . . . . . . . 12  |-  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( B  -  r ) (,) B ) ) )  =  ( ( RR 
_D  F )  |`  ( ( B  -  r ) (,) B
) )
8983, 88syl6eq 2511 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( RR  _D  ( F  |`  ( ( B  -  r ) (,) B ) ) )  =  ( ( RR 
_D  F )  |`  ( ( B  -  r ) (,) B
) ) )
9089dmeqd 5194 . . . . . . . . . 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
) ) )
9155, 59sstrd 3499 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  D )
9260adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  D  C_  dom  ( RR 
_D  F ) )
9391, 92sstrd 3499 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  dom  ( RR 
_D  F ) )
94 ssdmres 5283 . . . . . . . . . . 11  |-  ( ( ( B  -  r
) (,) B ) 
C_  dom  ( RR  _D  F )  <->  dom  ( ( RR  _D  F )  |`  ( ( B  -  r ) (,) B
) )  =  ( ( B  -  r
) (,) B ) )
9593, 94sylib 196 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( ( RR  _D  F )  |`  (
( B  -  r
) (,) B ) )  =  ( ( B  -  r ) (,) B ) )
9690, 95eqtrd 2495 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( RR  _D  ( F  |`  ( ( B  -  r ) (,) B ) ) )  =  ( ( B  -  r ) (,) B ) )
97 fss 5721 . . . . . . . . . . . . . . 15  |-  ( ( G : A --> RR  /\  RR  C_  CC )  ->  G : A --> CC )
9872, 61, 97sylancl 660 . . . . . . . . . . . . . 14  |-  ( ph  ->  G : A --> CC )
9998adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  G : A --> CC )
10080, 81dvres 22481 . . . . . . . . . . . . 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 ) ) ) )
10175, 99, 77, 79, 100syl22anc 1227 . . . . . . . . . . . 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 ) ) ) )
10287reseq2i 5259 . . . . . . . . . . . 12  |-  ( ( RR  _D  G )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( B  -  r ) (,) B ) ) )  =  ( ( RR 
_D  G )  |`  ( ( B  -  r ) (,) B
) )
103101, 102syl6eq 2511 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) )  =  ( ( RR 
_D  G )  |`  ( ( B  -  r ) (,) B
) ) )
104103dmeqd 5194 . . . . . . . . . 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
) ) )
105 lhop.ig . . . . . . . . . . . . 13  |-  ( ph  ->  D  C_  dom  ( RR 
_D  G ) )
106105adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  D  C_  dom  ( RR 
_D  G ) )
10791, 106sstrd 3499 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  dom  ( RR 
_D  G ) )
108 ssdmres 5283 . . . . . . . . . . 11  |-  ( ( ( B  -  r
) (,) B ) 
C_  dom  ( RR  _D  G )  <->  dom  ( ( RR  _D  G )  |`  ( ( B  -  r ) (,) B
) )  =  ( ( B  -  r
) (,) B ) )
109107, 108sylib 196 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( ( RR  _D  G )  |`  (
( B  -  r
) (,) B ) )  =  ( ( B  -  r ) (,) B ) )
110104, 109eqtrd 2495 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) )  =  ( ( B  -  r ) (,) B ) )
111 limcresi 22455 . . . . . . . . . 10  |-  ( F lim
CC  B )  C_  ( ( F  |`  ( ( B  -  r ) (,) B
) ) lim CC  B
)
112 lhop.f0 . . . . . . . . . . 11  |-  ( ph  ->  0  e.  ( F lim
CC  B ) )
113112adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( F lim
CC  B ) )
114111, 113sseldi 3487 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( ( F  |`  ( ( B  -  r ) (,) B ) ) lim CC  B ) )
115 limcresi 22455 . . . . . . . . . 10  |-  ( G lim
CC  B )  C_  ( ( G  |`  ( ( B  -  r ) (,) B
) ) lim CC  B
)
116 lhop.g0 . . . . . . . . . . 11  |-  ( ph  ->  0  e.  ( G lim
CC  B ) )
117116adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( G lim
CC  B ) )
118115, 117sseldi 3487 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( ( G  |`  ( ( B  -  r ) (,) B ) ) lim CC  B ) )
119 df-ima 5001 . . . . . . . . . . 11  |-  ( G
" ( ( B  -  r ) (,) B ) )  =  ran  ( G  |`  ( ( B  -  r ) (,) B
) )
120 imass2 5360 . . . . . . . . . . . 12  |-  ( ( ( B  -  r
) (,) B ) 
C_  D  ->  ( G " ( ( B  -  r ) (,) B ) )  C_  ( G " D ) )
12191, 120syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( G " (
( B  -  r
) (,) B ) )  C_  ( G " D ) )
122119, 121syl5eqssr 3534 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  ran  ( G  |`  (
( B  -  r
) (,) B ) )  C_  ( G " D ) )
123 lhop.gn0 . . . . . . . . . . 11  |-  ( ph  ->  -.  0  e.  ( G " D ) )
124123adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  ( G " D ) )
125122, 124ssneldd 3492 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  ran  ( G  |`  ( ( B  -  r ) (,) B ) ) )
126103rneqd 5219 . . . . . . . . . . . 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
) ) )
127 df-ima 5001 . . . . . . . . . . . 12  |-  ( ( RR  _D  G )
" ( ( B  -  r ) (,) B ) )  =  ran  ( ( RR 
_D  G )  |`  ( ( B  -  r ) (,) B
) )
128126, 127syl6eqr 2513 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  ran  ( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) )  =  ( ( RR 
_D  G ) "
( ( B  -  r ) (,) B
) ) )
129 imass2 5360 . . . . . . . . . . . 12  |-  ( ( ( B  -  r
) (,) B ) 
C_  D  ->  (
( RR  _D  G
) " ( ( B  -  r ) (,) B ) ) 
C_  ( ( RR 
_D  G ) " D ) )
13091, 129syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( RR  _D  G ) " (
( B  -  r
) (,) B ) )  C_  ( ( RR  _D  G ) " D ) )
131128, 130eqsstrd 3523 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  ran  ( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) ) 
C_  ( ( RR 
_D  G ) " D ) )
132 lhop.gd0 . . . . . . . . . . 11  |-  ( ph  ->  -.  0  e.  ( ( RR  _D  G
) " D ) )
133132adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  (
( RR  _D  G
) " D ) )
134131, 133ssneldd 3492 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  ran  ( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) ) )
135 limcresi 22455 . . . . . . . . . . 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 )
13691resmptd 5313 . . . . . . . . . . . . 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 ) ) ) )
13789fveq1d 5850 . . . . . . . . . . . . . . . 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
) )
138 fvres 5862 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( ( B  -  r ) (,) B )  ->  (
( ( RR  _D  F )  |`  (
( B  -  r
) (,) B ) ) `  z )  =  ( ( RR 
_D  F ) `  z ) )
139137, 138sylan9eq 2515 . . . . . . . . . . . . . . 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 )
)
140103fveq1d 5850 . . . . . . . . . . . . . . . 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
) )
141 fvres 5862 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( ( B  -  r ) (,) B )  ->  (
( ( RR  _D  G )  |`  (
( B  -  r
) (,) B ) ) `  z )  =  ( ( RR 
_D  G ) `  z ) )
142140, 141sylan9eq 2515 . . . . . . . . . . . . . . 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 )
)
143139, 142oveq12d 6288 . . . . . . . . . . . . . 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 ) ) )
144143mpteq2dva 4525 . . . . . . . . . . . . 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 ) ) ) )
145136, 144eqtr4d 2498 . . . . . . . . . . . 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 ) ) ) )
146145oveq1d 6285 . . . . . . . . . . 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 ) )
147135, 146syl5sseq 3537 . . . . . . . . . 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 ) )
148 lhop.c . . . . . . . . . . 11  |-  ( ph  ->  C  e.  ( ( z  e.  D  |->  ( ( ( RR  _D  F ) `  z
)  /  ( ( RR  _D  G ) `
 z ) ) ) lim CC  B ) )
149148adantr 463 . . . . . . . . . 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 ) )
150147, 149sseldd 3490 . . . . . . . . 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 ) )
15123, 19, 24, 71, 74, 96, 110, 114, 118, 125, 134, 150lhop2 22582 . . . . . . . 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 ) )
15255resmptd 5313 . . . . . . . . . 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 ) ) ) )
153 fvres 5862 . . . . . . . . . . . 12  |-  ( z  e.  ( ( B  -  r ) (,) B )  ->  (
( F  |`  (
( B  -  r
) (,) B ) ) `  z )  =  ( F `  z ) )
154 fvres 5862 . . . . . . . . . . . 12  |-  ( z  e.  ( ( B  -  r ) (,) B )  ->  (
( G  |`  (
( B  -  r
) (,) B ) ) `  z )  =  ( G `  z ) )
155153, 154oveq12d 6288 . . . . . . . . . . 11  |-  ( z  e.  ( ( B  -  r ) (,) B )  ->  (
( ( F  |`  ( ( B  -  r ) (,) B
) ) `  z
)  /  ( ( G  |`  ( ( B  -  r ) (,) B ) ) `  z ) )  =  ( ( F `  z )  /  ( G `  z )
) )
156155mpteq2ia 4521 . . . . . . . . . 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 )
) )
157152, 156syl6eqr 2513 . . . . . . . . 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 ) ) ) )
158157oveq1d 6285 . . . . . . . 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 ) )
159151, 158eleqtrrd 2545 . . . . . . 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
) )
160 ssun2 3654 . . . . . . . . . . . 12  |-  ( B (,) ( B  +  r ) )  C_  ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r ) ) )
161160, 54syl5sseqr 3538 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  ( (
( B  -  r
) (,) ( B  +  r ) ) 
\  { B }
) )
162161, 69sstrd 3499 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  A )
16326, 162fssresd 5734 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( F  |`  ( B (,) ( B  +  r ) ) ) : ( B (,) ( B  +  r
) ) --> RR )
16473, 162fssresd 5734 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( G  |`  ( B (,) ( B  +  r ) ) ) : ( B (,) ( B  +  r
) ) --> RR )
165 ioossre 11589 . . . . . . . . . . . . . 14  |-  ( B (,) ( B  +  r ) )  C_  RR
166165a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  RR )
16780, 81dvres 22481 . . . . . . . . . . . . 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 ) ) ) ) )
16875, 76, 77, 166, 167syl22anc 1227 . . . . . . . . . . . 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 ) ) ) ) )
169 iooretop 21439 . . . . . . . . . . . . . 14  |-  ( B (,) ( B  +  r ) )  e.  ( topGen `  ran  (,) )
170 isopn3i 19750 . . . . . . . . . . . . . 14  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( B (,) ( B  +  r ) )  e.  ( topGen `  ran  (,) )
)  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  ( B (,) ( B  +  r ) ) )  =  ( B (,) ( B  +  r
) ) )
17184, 169, 170mp2an 670 . . . . . . . . . . . . 13  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( B (,) ( B  +  r ) ) )  =  ( B (,) ( B  +  r ) )
172171reseq2i 5259 . . . . . . . . . . . 12  |-  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( B (,) ( B  +  r ) ) ) )  =  ( ( RR 
_D  F )  |`  ( B (,) ( B  +  r ) ) )
173168, 172syl6eq 2511 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( RR  _D  ( F  |`  ( B (,) ( B  +  r
) ) ) )  =  ( ( RR 
_D  F )  |`  ( B (,) ( B  +  r ) ) ) )
174173dmeqd 5194 . . . . . . . . . 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 )
) ) )
175161, 59sstrd 3499 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  D )
176175, 92sstrd 3499 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  dom  ( RR 
_D  F ) )
177 ssdmres 5283 . . . . . . . . . . 11  |-  ( ( B (,) ( B  +  r ) ) 
C_  dom  ( RR  _D  F )  <->  dom  ( ( RR  _D  F )  |`  ( B (,) ( B  +  r )
) )  =  ( B (,) ( B  +  r ) ) )
178176, 177sylib 196 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( ( RR  _D  F )  |`  ( B (,) ( B  +  r ) ) )  =  ( B (,) ( B  +  r
) ) )
179174, 178eqtrd 2495 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( RR  _D  ( F  |`  ( B (,) ( B  +  r
) ) ) )  =  ( B (,) ( B  +  r
) ) )
18080, 81dvres 22481 . . . . . . . . . . . . 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 ) ) ) ) )
18175, 99, 77, 166, 180syl22anc 1227 . . . . . . . . . . . 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 ) ) ) ) )
182171reseq2i 5259 . . . . . . . . . . . 12  |-  ( ( RR  _D  G )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( B (,) ( B  +  r ) ) ) )  =  ( ( RR 
_D  G )  |`  ( B (,) ( B  +  r ) ) )
183181, 182syl6eq 2511 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( RR  _D  ( G  |`  ( B (,) ( B  +  r
) ) ) )  =  ( ( RR 
_D  G )  |`  ( B (,) ( B  +  r ) ) ) )
184183dmeqd 5194 . . . . . . . . . 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 )
) ) )
185175, 106sstrd 3499 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  dom  ( RR 
_D  G ) )
186 ssdmres 5283 . . . . . . . . . . 11  |-  ( ( B (,) ( B  +  r ) ) 
C_  dom  ( RR  _D  G )  <->  dom  ( ( RR  _D  G )  |`  ( B (,) ( B  +  r )
) )  =  ( B (,) ( B  +  r ) ) )
187185, 186sylib 196 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( ( RR  _D  G )  |`  ( B (,) ( B  +  r ) ) )  =  ( B (,) ( B  +  r
) ) )
188184, 187eqtrd 2495 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( RR  _D  ( G  |`  ( B (,) ( B  +  r
) ) ) )  =  ( B (,) ( B  +  r
) ) )
189 limcresi 22455 . . . . . . . . . 10  |-  ( F lim
CC  B )  C_  ( ( F  |`  ( B (,) ( B  +  r ) ) ) lim CC  B )
190189, 113sseldi 3487 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( ( F  |`  ( B (,) ( B  +  r ) ) ) lim CC  B ) )
191 limcresi 22455 . . . . . . . . . 10  |-  ( G lim
CC  B )  C_  ( ( G  |`  ( B (,) ( B  +  r ) ) ) lim CC  B )
192191, 117sseldi 3487 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( ( G  |`  ( B (,) ( B  +  r ) ) ) lim CC  B ) )
193 df-ima 5001 . . . . . . . . . . 11  |-  ( G
" ( B (,) ( B  +  r
) ) )  =  ran  ( G  |`  ( B (,) ( B  +  r ) ) )
194 imass2 5360 . . . . . . . . . . . 12  |-  ( ( B (,) ( B  +  r ) ) 
C_  D  ->  ( G " ( B (,) ( B  +  r
) ) )  C_  ( G " D ) )
195175, 194syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( G " ( B (,) ( B  +  r ) ) ) 
C_  ( G " D ) )
196193, 195syl5eqssr 3534 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  ran  ( G  |`  ( B (,) ( B  +  r ) ) ) 
C_  ( G " D ) )
197196, 124ssneldd 3492 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  ran  ( G  |`  ( B (,) ( B  +  r ) ) ) )
198183rneqd 5219 . . . . . . . . . . . 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 )
) ) )
199 df-ima 5001 . . . . . . . . . . . 12  |-  ( ( RR  _D  G )
" ( B (,) ( B  +  r
) ) )  =  ran  ( ( RR 
_D  G )  |`  ( B (,) ( B  +  r ) ) )
200198, 199syl6eqr 2513 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  ran  ( RR  _D  ( G  |`  ( B (,) ( B  +  r
) ) ) )  =  ( ( RR 
_D  G ) "
( B (,) ( B  +  r )
) ) )
201 imass2 5360 . . . . . . . . . . . 12  |-  ( ( B (,) ( B  +  r ) ) 
C_  D  ->  (
( RR  _D  G
) " ( B (,) ( B  +  r ) ) ) 
C_  ( ( RR 
_D  G ) " D ) )
202175, 201syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( RR  _D  G ) " ( B (,) ( B  +  r ) ) ) 
C_  ( ( RR 
_D  G ) " D ) )
203200, 202eqsstrd 3523 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  ran  ( RR  _D  ( G  |`  ( B (,) ( B  +  r
) ) ) ) 
C_  ( ( RR 
_D  G ) " D ) )
204203, 133ssneldd 3492 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  ran  ( RR  _D  ( G  |`  ( B (,) ( B  +  r
) ) ) ) )
205 limcresi 22455 . . . . . . . . . . 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 )
206175resmptd 5313 . . . . . . . . . . . . 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 ) ) ) )
207173fveq1d 5850 . . . . . . . . . . . . . . . 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
) )
208 fvres 5862 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( B (,) ( B  +  r
) )  ->  (
( ( RR  _D  F )  |`  ( B (,) ( B  +  r ) ) ) `
 z )  =  ( ( RR  _D  F ) `  z
) )
209207, 208sylan9eq 2515 . . . . . . . . . . . . . . 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 ) )
210183fveq1d 5850 . . . . . . . . . . . . . . . 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
) )
211 fvres 5862 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( B (,) ( B  +  r
) )  ->  (
( ( RR  _D  G )  |`  ( B (,) ( B  +  r ) ) ) `
 z )  =  ( ( RR  _D  G ) `  z
) )
212210, 211sylan9eq 2515 . . . . . . . . . . . . . . 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 ) )
213209, 212oveq12d 6288 . . . . . . . . . . . . . 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 ) ) )
214213mpteq2dva 4525 . . . . . . . . . . . . 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
) ) ) )
215206, 214eqtr4d 2498 . . . . . . . . . . . 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 ) ) ) )
216215oveq1d 6285 . . . . . . . . . . 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 ) )
217205, 216syl5sseq 3537 . . . . . . . . . 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 ) )
218217, 149sseldd 3490 . . . . . . . . 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 ) )
21919, 34, 35, 163, 164, 179, 188, 190, 192, 197, 204, 218lhop1 22581 . . . . . . . 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 ) )
220161resmptd 5313 . . . . . . . . . 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 ) ) ) )
221 fvres 5862 . . . . . . . . . . . 12  |-  ( z  e.  ( B (,) ( B  +  r
) )  ->  (
( F  |`  ( B (,) ( B  +  r ) ) ) `
 z )  =  ( F `  z
) )
222 fvres 5862 . . . . . . . . . . . 12  |-  ( z  e.  ( B (,) ( B  +  r
) )  ->  (
( G  |`  ( B (,) ( B  +  r ) ) ) `
 z )  =  ( G `  z
) )
223221, 222oveq12d 6288 . . . . . . . . . . 11  |-  ( z  e.  ( B (,) ( B  +  r
) )  ->  (
( ( F  |`  ( B (,) ( B  +  r ) ) ) `  z )  /  ( ( G  |`  ( B (,) ( B  +  r )
) ) `  z
) )  =  ( ( F `  z
)  /  ( G `
 z ) ) )
224223mpteq2ia 4521 . . . . . . . . . 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 ) ) )
225220, 224syl6eqr 2513 . . . . . . . . 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
) ) ) )
226225oveq1d 6285 . . . . . . . 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 ) )
227219, 226eleqtrrd 2545 . . . . . . 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
) )
228159, 227elind 3674 . . . . . 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
) ) )
22959resmptd 5313 . . . . . . . 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 ) ) ) )
230229oveq1d 6285 . . . . . . 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 ) )
23167sselda 3489 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  D )  ->  z  e.  A )
23225ffvelrnda 6007 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  A )  ->  ( F `  z )  e.  RR )
233231, 232syldan 468 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  D )  ->  ( F `  z )  e.  RR )
234233recnd 9611 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  D )  ->  ( F `  z )  e.  CC )
23572ffvelrnda 6007 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  A )  ->  ( G `  z )  e.  RR )
236231, 235syldan 468 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  D )  ->  ( G `  z )  e.  RR )
237236recnd 9611 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  D )  ->  ( G `  z )  e.  CC )
238123adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  D )  ->  -.  0  e.  ( G " D ) )
239 ffn 5713 . . . . . . . . . . . . . . . . 17  |-  ( G : A --> RR  ->  G  Fn  A )
24072, 239syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  G  Fn  A )
241240adantr 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  D )  ->  G  Fn  A )
24267adantr 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  D )  ->  D  C_  A )
243 simpr 459 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  D )  ->  z  e.  D )
244 fnfvima 6125 . . . . . . . . . . . . . . 15  |-  ( ( G  Fn  A  /\  D  C_  A  /\  z  e.  D )  ->  ( G `  z )  e.  ( G " D
) )
245241, 242, 243, 244syl3anc 1226 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  z  e.  D )  ->  ( G `  z )  e.  ( G " D
) )
246 eleq1 2526 . . . . . . . . . . . . . 14  |-  ( ( G `  z )  =  0  ->  (
( G `  z
)  e.  ( G
" D )  <->  0  e.  ( G " D ) ) )
247245, 246syl5ibcom 220 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  D )  ->  (
( G `  z
)  =  0  -> 
0  e.  ( G
" D ) ) )
248247necon3bd 2666 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  D )  ->  ( -.  0  e.  ( G " D )  -> 
( G `  z
)  =/=  0 ) )
249238, 248mpd 15 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  D )  ->  ( G `  z )  =/=  0 )
250234, 237, 249divcld 10316 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  D )  ->  (
( F `  z
)  /  ( G `
 z ) )  e.  CC )
251250adantlr 712 . . . . . . . . 9  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  (
( B  -  r
) (,) ( B  +  r ) ) 
C_  I ) )  /\  z  e.  D
)  ->  ( ( F `  z )  /  ( G `  z ) )  e.  CC )
252 eqid 2454 . . . . . . . . 9  |-  ( z  e.  D  |->  ( ( F `  z )  /  ( G `  z ) ) )  =  ( z  e.  D  |->  ( ( F `
 z )  / 
( G `  z
) ) )
253251, 252fmptd 6031 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( z  e.  D  |->  ( ( F `  z )  /  ( G `  z )
) ) : D --> CC )
254 difss 3617 . . . . . . . . . . 11  |-  ( I 
\  { B }
)  C_  I
25558, 254eqsstri 3519 . . . . . . . . . 10  |-  D  C_  I
25613, 61syl6ss 3501 . . . . . . . . . 10  |-  ( ph  ->  I  C_  CC )
257255, 256syl5ss 3500 . . . . . . . . 9  |-  ( ph  ->  D  C_  CC )
258257adantr 463 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  D  C_  CC )
259 eqid 2454 . . . . . . . 8  |-  ( (
TopOpen ` fld )t  ( D  u.  { B } ) )  =  ( ( TopOpen ` fld )t  ( D  u.  { B } ) )
26058uneq1i 3640 . . . . . . . . . . . . . . . . 17  |-  ( D  u.  { B }
)  =  ( ( I  \  { B } )  u.  { B } )
261 undif1 3891 . . . . . . . . . . . . . . . . 17  |-  ( ( I  \  { B } )  u.  { B } )  =  ( I  u.  { B } )
262260, 261eqtri 2483 . . . . . . . . . . . . . . . 16  |-  ( D  u.  { B }
)  =  ( I  u.  { B }
)
263 simprr 755 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) ( B  +  r )
)  C_  I )
26442, 263sstrd 3499 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  { B }  C_  I
)
265 ssequn2 3663 . . . . . . . . . . . . . . . . 17  |-  ( { B }  C_  I  <->  ( I  u.  { B } )  =  I )
266264, 265sylib 196 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( I  u.  { B } )  =  I )
267262, 266syl5eq 2507 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( D  u.  { B } )  =  I )
268267oveq2d 6286 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( TopOpen ` fld )t  ( D  u.  { B } ) )  =  ( ( TopOpen ` fld )t  I
) )
26913adantr 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  I  C_  RR )
270 eqid 2454 . . . . . . . . . . . . . . . 16  |-  ( topGen ` 
ran  (,) )  =  (
topGen `  ran  (,) )
27180, 270rerest 21475 . . . . . . . . . . . . . . 15  |-  ( I 
C_  RR  ->  ( (
TopOpen ` fld )t  I )  =  ( ( topGen `  ran  (,) )t  I
) )
272269, 271syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( TopOpen ` fld )t  I )  =  ( ( topGen `  ran  (,) )t  I
) )
273268, 272eqtrd 2495 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( TopOpen ` fld )t  ( D  u.  { B } ) )  =  ( ( topGen ` 
ran  (,) )t  I ) )
274273fveq2d 5852 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( int `  (
( TopOpen ` fld )t  ( D  u.  { B } ) ) )  =  ( int `  ( ( topGen `  ran  (,) )t  I ) ) )
275274fveq1d 5850 . . . . . . . . . . 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 )
) ) )
27680cnfldtopon 21456 . . . . . . . . . . . . . . 15  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
277256adantr 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  I  C_  CC )
278 resttopon 19829 . . . . . . . . . . . . . . 15  |-  ( ( ( TopOpen ` fld )  e.  (TopOn `  CC )  /\  I  C_  CC )  ->  (
( TopOpen ` fld )t  I )  e.  (TopOn `  I ) )
279276, 277, 278sylancr 661 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( TopOpen ` fld )t  I )  e.  (TopOn `  I ) )
280 topontop 19594 . . . . . . . . . . . . . 14  |-  ( ( ( TopOpen ` fld )t  I )  e.  (TopOn `  I )  ->  (
( TopOpen ` fld )t  I )  e.  Top )
281279, 280syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( TopOpen ` fld )t  I )  e.  Top )
282272, 281eqeltrrd 2543 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( topGen `  ran  (,) )t  I )  e.  Top )
283 iooretop 21439 . . . . . . . . . . . . . 14  |-  ( ( B  -  r ) (,) ( B  +  r ) )  e.  ( topGen `  ran  (,) )
284283a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) ( B  +  r )
)  e.  ( topGen ` 
ran  (,) ) )
2854adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  I  e.  ( topGen ` 
ran  (,) ) )
286 restopn2 19845 . . . . . . . . . . . . . 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 ) ) )
28784, 285, 286sylancr 661 . . . . . . . . . . . . 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 )
) )
288284, 263, 287mpbir2and 920 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) ( B  +  r )
)  e.  ( (
topGen `  ran  (,) )t  I
) )
289 isopn3i 19750 . . . . . . . . . . . 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 ) ) )
290282, 288, 289syl2anc 659 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( int `  (
( topGen `  ran  (,) )t  I
) ) `  (
( B  -  r
) (,) ( B  +  r ) ) )  =  ( ( B  -  r ) (,) ( B  +  r ) ) )
291275, 290eqtrd 2495 . . . . . . . . . 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 ) ) )
29241, 291eleqtrrd 2545 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  B  e.  ( ( int `  ( ( TopOpen ` fld )t  ( D  u.  { B } ) ) ) `
 ( ( B  -  r ) (,) ( B  +  r ) ) ) )
293 undif1 3891 . . . . . . . . . . 11  |-  ( ( ( ( B  -  r ) (,) ( B  +  r )
)  \  { B } )  u.  { B } )  =  ( ( ( B  -  r ) (,) ( B  +  r )
)  u.  { B } )
294 ssequn2 3663 . . . . . . . . . . . 12  |-  ( { B }  C_  (
( B  -  r
) (,) ( B  +  r ) )  <-> 
( ( ( B  -  r ) (,) ( B  +  r ) )  u.  { B } )  =  ( ( B  -  r
) (,) ( B  +  r ) ) )
29542, 294sylib 196 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( ( B  -  r ) (,) ( B  +  r ) )  u.  { B } )  =  ( ( B  -  r
) (,) ( B  +  r ) ) )
296293, 295syl5eq 2507 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  u. 
{ B } )  =  ( ( B  -  r ) (,) ( B  +  r ) ) )
297296fveq2d 5852 . . . . . . . . 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 ) ) ) )
298292, 297eleqtrrd 2545 . . . . . . . 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 } ) ) )
299253, 59, 258, 80, 259, 298limcres 22456 . . . . . . 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
) )
30078, 61sstri 3498 . . . . . . . . 9  |-  ( ( B  -  r ) (,) B )  C_  CC
301300a1i 11 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  CC )
302165, 61sstri 3498 . . . . . . . . 9  |-  ( B (,) ( B  +  r ) )  C_  CC
303302a1i 11 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  CC )
30459sselda 3489 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  (
( B  -  r
) (,) ( B  +  r ) ) 
C_  I ) )  /\  z  e.  ( ( ( B  -  r ) (,) ( B  +  r )
)  \  { B } ) )  -> 
z  e.  D )
305304, 251syldan 468 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  (
( B  -  r
) (,) ( B  +  r ) ) 
C_  I ) )  /\  z  e.  ( ( ( B  -  r ) (,) ( B  +  r )
)  \  { B } ) )  -> 
( ( F `  z )  /  ( G `  z )
)  e.  CC )
306 eqid 2454 . . . . . . . . . 10  |-  ( z  e.  ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  |->  ( ( F `  z
)  /  ( G `
 z ) ) )  =  ( z  e.  ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  |->  ( ( F `  z
)  /  ( G `
 z ) ) )
307305, 306fmptd 6031 . . . . . . . . 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 )
30854feq2d 5700 . . . . . . . . 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 ) )
309307, 308mpbid 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 (,) ( B  +  r )
) ) --> CC )
310301, 303, 309limcun 22465 . . . . . . 7  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( z  e.  ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  |->  ( ( F `  z )  /  ( G `  z ) ) ) lim
CC  B )  =  ( ( ( ( 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
) ) )
311230, 299, 3103eqtr3rd 2504 . . . . . 6  |-  ( (
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
)  i^i  ( (
( z  e.  ( ( ( B  -  r ) (,) ( B  +  r )
)  \  { B } )  |->  ( ( F `  z )  /  ( G `  z ) ) )  |`  ( B (,) ( B  +  r )
) ) lim CC  B
) )  =  ( ( z  e.  D  |->  ( ( F `  z )  /  ( G `  z )
) ) lim CC  B
) )
312228, 311eleqtrd 2544 . . . . 5  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  C  e.  ( (
z  e.  D  |->  ( ( F `  z
)  /  ( G `
 z ) ) ) lim CC  B ) )
313312expr 613 . . . 4  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( (
( B  -  r
) (,) ( B  +  r ) ) 
C_  I  ->  C  e.  ( ( z  e.  D  |->  ( ( F `
 z )  / 
( G `  z
) ) ) lim CC  B ) ) )
31418, 313sylbid 215 . . 3  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( ( B ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  I  ->  C  e.  ( ( z  e.  D  |->  ( ( F `  z )  /  ( G `  z ) ) ) lim
CC  B ) ) )
315314rexlimdva 2946 . 2  |-  ( ph  ->  ( E. r  e.  RR+  ( B ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) r )  C_  I  ->  C  e.  ( ( z  e.  D  |->  ( ( F `  z )  /  ( G `  z )
) ) lim CC  B
) ) )
3169, 315mpd 15 1  |-  ( ph  ->  C  e.  ( ( z  e.  D  |->  ( ( F `  z
)  /  ( G `
 z ) ) ) lim CC  B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 366    /\ wa 367    /\ w3a 971    = wceq 1398    e. wcel 1823    =/= wne 2649   E.wrex 2805    \ cdif 3458    u. cun 3459    i^i cin 3460    C_ wss 3461   (/)c0 3783   {csn 4016   U.cuni 4235   class class class wbr 4439    |-> cmpt 4497    X. cxp 4986   dom cdm 4988   ran crn 4989    |` cres 4990   "cima 4991    o. ccom 4992    Fn wfn 5565   -->wf 5566   ` cfv 5570  (class class class)co 6270   CCcc 9479   RRcr 9480   0cc0 9481    + caddc 9484   RR*cxr 9616