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

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

Proof of Theorem lhop
Dummy variable  r is distinct from all other variables.
StepHypRef Expression
1 eqid 2435 . . . . 5  |-  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )  =  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )
21rexmet 18810 . . . 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 2435 . . . . 5  |-  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )  =  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )
71, 6tgioo 18815 . . . 4  |-  ( topGen ` 
ran  (,) )  =  (
MetOpen `  ( ( abs 
o.  -  )  |`  ( RR  X.  RR ) ) )
87mopni2 18511 . . 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 1184 . 2  |-  ( ph  ->  E. r  e.  RR+  ( B ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  I )
10 elssuni 4035 . . . . . . . . 9  |-  ( I  e.  ( topGen `  ran  (,) )  ->  I  C_  U. ( topGen `
 ran  (,) )
)
11 uniretop 18784 . . . . . . . . 9  |-  RR  =  U. ( topGen `  ran  (,) )
1210, 11syl6sseqr 3387 . . . . . . . 8  |-  ( I  e.  ( topGen `  ran  (,) )  ->  I  C_  RR )
134, 12syl 16 . . . . . . 7  |-  ( ph  ->  I  C_  RR )
1413, 5sseldd 3341 . . . . . 6  |-  ( ph  ->  B  e.  RR )
15 rpre 10607 . . . . . 6  |-  ( r  e.  RR+  ->  r  e.  RR )
161bl2ioo 18811 . . . . . 6  |-  ( ( B  e.  RR  /\  r  e.  RR )  ->  ( B ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) r )  =  ( ( B  -  r ) (,) ( B  +  r )
) )
1714, 15, 16syl2an 464 . . . . 5  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( B
( ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  =  ( ( B  -  r ) (,) ( B  +  r ) ) )
1817sseq1d 3367 . . . 4  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( ( B ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  I  <->  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I
) )
1914adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  B  e.  RR )
20 simprl 733 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
r  e.  RR+ )
2120rpred 10637 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
r  e.  RR )
2219, 21resubcld 9454 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B  -  r
)  e.  RR )
2322rexrd 9123 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B  -  r
)  e.  RR* )
2419, 20ltsubrpd 10665 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B  -  r
)  <  B )
25 lhop.f . . . . . . . . . . 11  |-  ( ph  ->  F : A --> RR )
2625adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  F : A --> RR )
27 ssun1 3502 . . . . . . . . . . . 12  |-  ( ( B  -  r ) (,) B )  C_  ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r ) ) )
28 unass 3496 . . . . . . . . . . . . . . 15  |-  ( ( { B }  u.  ( ( B  -  r ) (,) B
) )  u.  ( B (,) ( B  +  r ) ) )  =  ( { B }  u.  ( (
( B  -  r
) (,) B )  u.  ( B (,) ( B  +  r
) ) ) )
29 uncom 3483 . . . . . . . . . . . . . . . 16  |-  ( { B }  u.  (
( B  -  r
) (,) B ) )  =  ( ( ( B  -  r
) (,) B )  u.  { B }
)
3029uneq1i 3489 . . . . . . . . . . . . . . 15  |-  ( ( { B }  u.  ( ( B  -  r ) (,) B
) )  u.  ( B (,) ( B  +  r ) ) )  =  ( ( ( ( B  -  r
) (,) B )  u.  { B }
)  u.  ( B (,) ( B  +  r ) ) )
3128, 30eqtr3i 2457 . . . . . . . . . . . . . 14  |-  ( { B }  u.  (
( ( B  -  r ) (,) B
)  u.  ( B (,) ( B  +  r ) ) ) )  =  ( ( ( ( B  -  r ) (,) B
)  u.  { B } )  u.  ( B (,) ( B  +  r ) ) )
3219rexrd 9123 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  B  e.  RR* )
3319, 21readdcld 9104 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B  +  r )  e.  RR )
3433rexrd 9123 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B  +  r )  e.  RR* )
3519, 20ltaddrpd 10666 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  B  <  ( B  +  r ) )
36 ioojoin 11016 . . . . . . . . . . . . . . 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 1192 . . . . . . . . . . . . . 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 2479 . . . . . . . . . . . . 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 10946 . . . . . . . . . . . . . . . . 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 643 . . . . . . . . . . . . . . . 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 1137 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  B  e.  ( ( B  -  r ) (,) ( B  +  r ) ) )
4241snssd 3935 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  { B }  C_  (
( B  -  r
) (,) ( B  +  r ) ) )
43 incom 3525 . . . . . . . . . . . . . . 15  |-  ( { B }  i^i  (
( ( B  -  r ) (,) B
)  u.  ( B (,) ( B  +  r ) ) ) )  =  ( ( ( ( B  -  r ) (,) B
)  u.  ( B (,) ( B  +  r ) ) )  i^i  { B }
)
44 ubioo 10937 . . . . . . . . . . . . . . . . . 18  |-  -.  B  e.  ( ( B  -  r ) (,) B
)
45 lbioo 10936 . . . . . . . . . . . . . . . . . 18  |-  -.  B  e.  ( B (,) ( B  +  r )
)
4644, 45pm3.2ni 828 . . . . . . . . . . . . . . . . 17  |-  -.  ( B  e.  ( ( B  -  r ) (,) B )  \/  B  e.  ( B (,) ( B  +  r )
) )
47 elun 3480 . . . . . . . . . . . . . . . . 17  |-  ( B  e.  ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r )
) )  <->  ( B  e.  ( ( B  -  r ) (,) B
)  \/  B  e.  ( B (,) ( B  +  r )
) ) )
4846, 47mtbir 291 . . . . . . . . . . . . . . . 16  |-  -.  B  e.  ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r ) ) )
49 disjsn 3860 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r ) ) )  i^i  { B }
)  =  (/)  <->  -.  B  e.  ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r ) ) ) )
5048, 49mpbir 201 . . . . . . . . . . . . . . 15  |-  ( ( ( ( B  -  r ) (,) B
)  u.  ( B (,) ( B  +  r ) ) )  i^i  { B }
)  =  (/)
5143, 50eqtri 2455 . . . . . . . . . . . . . 14  |-  ( { B }  i^i  (
( ( B  -  r ) (,) B
)  u.  ( B (,) ( B  +  r ) ) ) )  =  (/)
52 uneqdifeq 3708 . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . 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 202 . . . . . . . . . . . 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 3389 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  ( (
( B  -  r
) (,) ( B  +  r ) ) 
\  { B }
) )
56 ssdif 3474 . . . . . . . . . . . . . 14  |-  ( ( ( B  -  r
) (,) ( B  +  r ) ) 
C_  I  ->  (
( ( B  -  r ) (,) ( B  +  r )
)  \  { B } )  C_  (
I  \  { B } ) )
5756ad2antll 710 . . . . . . . . . . . . 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 3387 . . . . . . . . . . . 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 9036 . . . . . . . . . . . . . . . 16  |-  RR  C_  CC
6261a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  RR  C_  CC )
63 fss 5590 . . . . . . . . . . . . . . . 16  |-  ( ( F : A --> RR  /\  RR  C_  CC )  ->  F : A --> CC )
6425, 61, 63sylancl 644 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F : A --> CC )
65 lhop.a . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  C_  RR )
6662, 64, 65dvbss 19776 . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  ( RR  _D  F )  C_  A
)
6760, 66sstrd 3350 . . . . . . . . . . . . 13  |-  ( ph  ->  D  C_  A )
6867adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  D  C_  A )
6959, 68sstrd 3350 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  C_  A
)
7055, 69sstrd 3350 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  A )
71 fssres 5601 . . . . . . . . . 10  |-  ( ( F : A --> RR  /\  ( ( B  -  r ) (,) B
)  C_  A )  ->  ( F  |`  (
( B  -  r
) (,) B ) ) : ( ( B  -  r ) (,) B ) --> RR )
7226, 70, 71syl2anc 643 . . . . . . . . 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 452 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  G : A --> RR )
75 fssres 5601 . . . . . . . . . 10  |-  ( ( G : A --> RR  /\  ( ( B  -  r ) (,) B
)  C_  A )  ->  ( G  |`  (
( B  -  r
) (,) B ) ) : ( ( B  -  r ) (,) B ) --> RR )
7674, 70, 75syl2anc 643 . . . . . . . . 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 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  F : A --> CC )
7965adantr 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  A  C_  RR )
80 ioossre 10961 . . . . . . . . . . . . . 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 2435 . . . . . . . . . . . . . 14  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
8382tgioo2 18822 . . . . . . . . . . . . . 14  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
8482, 83dvres 19786 . . . . . . . . . . . . 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 1185 . . . . . . . . . . . 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 18783 . . . . . . . . . . . . . 14  |-  ( topGen ` 
ran  (,) )  e.  Top
87 iooretop 18788 . . . . . . . . . . . . . 14  |-  ( ( B  -  r ) (,) B )  e.  ( topGen `  ran  (,) )
88 isopn3i 17134 . . . . . . . . . . . . . 14  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( ( B  -  r ) (,) B )  e.  ( topGen `  ran  (,) )
)  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  (
( B  -  r
) (,) B ) )  =  ( ( B  -  r ) (,) B ) )
8986, 87, 88mp2an 654 . . . . . . . . . . . . 13  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( ( B  -  r ) (,) B
) )  =  ( ( B  -  r
) (,) B )
9089reseq2i 5134 . . . . . . . . . . . 12  |-  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( B  -  r ) (,) B ) ) )  =  ( ( RR 
_D  F )  |`  ( ( B  -  r ) (,) B
) )
9185, 90syl6eq 2483 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( RR  _D  ( F  |`  ( ( B  -  r ) (,) B ) ) )  =  ( ( RR 
_D  F )  |`  ( ( B  -  r ) (,) B
) ) )
9291dmeqd 5063 . . . . . . . . . 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 3350 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  D )
9460adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  D  C_  dom  ( RR 
_D  F ) )
9593, 94sstrd 3350 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  dom  ( RR 
_D  F ) )
96 ssdmres 5159 . . . . . . . . . . 11  |-  ( ( ( B  -  r
) (,) B ) 
C_  dom  ( RR  _D  F )  <->  dom  ( ( RR  _D  F )  |`  ( ( B  -  r ) (,) B
) )  =  ( ( B  -  r
) (,) B ) )
9795, 96sylib 189 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( ( RR  _D  F )  |`  (
( B  -  r
) (,) B ) )  =  ( ( B  -  r ) (,) B ) )
9892, 97eqtrd 2467 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( RR  _D  ( F  |`  ( ( B  -  r ) (,) B ) ) )  =  ( ( B  -  r ) (,) B ) )
99 fss 5590 . . . . . . . . . . . . . . 15  |-  ( ( G : A --> RR  /\  RR  C_  CC )  ->  G : A --> CC )
10073, 61, 99sylancl 644 . . . . . . . . . . . . . 14  |-  ( ph  ->  G : A --> CC )
101100adantr 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  G : A --> CC )
10282, 83dvres 19786 . . . . . . . . . . . . 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 1185 . . . . . . . . . . . 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 5134 . . . . . . . . . . . 12  |-  ( ( RR  _D  G )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( ( B  -  r ) (,) B ) ) )  =  ( ( RR 
_D  G )  |`  ( ( B  -  r ) (,) B
) )
105103, 104syl6eq 2483 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) )  =  ( ( RR 
_D  G )  |`  ( ( B  -  r ) (,) B
) ) )
106105dmeqd 5063 . . . . . . . . . 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 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  D  C_  dom  ( RR 
_D  G ) )
10993, 108sstrd 3350 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  dom  ( RR 
_D  G ) )
110 ssdmres 5159 . . . . . . . . . . 11  |-  ( ( ( B  -  r
) (,) B ) 
C_  dom  ( RR  _D  G )  <->  dom  ( ( RR  _D  G )  |`  ( ( B  -  r ) (,) B
) )  =  ( ( B  -  r
) (,) B ) )
111109, 110sylib 189 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( ( RR  _D  G )  |`  (
( B  -  r
) (,) B ) )  =  ( ( B  -  r ) (,) B ) )
112106, 111eqtrd 2467 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) )  =  ( ( B  -  r ) (,) B ) )
113 limcresi 19760 . . . . . . . . . 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 452 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( F lim
CC  B ) )
116113, 115sseldi 3338 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( ( F  |`  ( ( B  -  r ) (,) B ) ) lim CC  B ) )
117 limcresi 19760 . . . . . . . . . 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 452 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( G lim
CC  B ) )
120117, 119sseldi 3338 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( ( G  |`  ( ( B  -  r ) (,) B ) ) lim CC  B ) )
121 df-ima 4882 . . . . . . . . . . 11  |-  ( G
" ( ( B  -  r ) (,) B ) )  =  ran  ( G  |`  ( ( B  -  r ) (,) B
) )
122 imass2 5231 . . . . . . . . . . . 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 3385 . . . . . . . . . 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 452 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  ( G " D ) )
127124, 126ssneldd 3343 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  ran  ( G  |`  ( ( B  -  r ) (,) B ) ) )
128105rneqd 5088 . . . . . . . . . . . 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 4882 . . . . . . . . . . . 12  |-  ( ( RR  _D  G )
" ( ( B  -  r ) (,) B ) )  =  ran  ( ( RR 
_D  G )  |`  ( ( B  -  r ) (,) B
) )
130128, 129syl6eqr 2485 . . . . . . . . . . 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 5231 . . . . . . . . . . . 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 3374 . . . . . . . . . 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 452 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  (
( RR  _D  G
) " D ) )
136133, 135ssneldd 3343 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  ran  ( RR  _D  ( G  |`  ( ( B  -  r ) (,) B ) ) ) )
137 limcresi 19760 . . . . . . . . . . 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 5182 . . . . . . . . . . . . . 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 5721 . . . . . . . . . . . . . . . 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 5736 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( ( B  -  r ) (,) B )  ->  (
( ( RR  _D  F )  |`  (
( B  -  r
) (,) B ) ) `  z )  =  ( ( RR 
_D  F ) `  z ) )
142140, 141sylan9eq 2487 . . . . . . . . . . . . . . 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 5721 . . . . . . . . . . . . . . . 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 5736 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( ( B  -  r ) (,) B )  ->  (
( ( RR  _D  G )  |`  (
( B  -  r
) (,) B ) ) `  z )  =  ( ( RR 
_D  G ) `  z ) )
145143, 144sylan9eq 2487 . . . . . . . . . . . . . . 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 6090 . . . . . . . . . . . . . 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 4287 . . . . . . . . . . . . 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 2470 . . . . . . . . . . . 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 6087 . . . . . . . . . . 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 3388 . . . . . . . . . 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 452 . . . . . . . . . 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 3341 . . . . . . . . 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 19887 . . . . . . . 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 5182 . . . . . . . . . . 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 5736 . . . . . . . . . . . 12  |-  ( z  e.  ( ( B  -  r ) (,) B )  ->  (
( F  |`  (
( B  -  r
) (,) B ) ) `  z )  =  ( F `  z ) )
158 fvres 5736 . . . . . . . . . . . 12  |-  ( z  e.  ( ( B  -  r ) (,) B )  ->  (
( G  |`  (
( B  -  r
) (,) B ) ) `  z )  =  ( G `  z ) )
159157, 158oveq12d 6090 . . . . . . . . . . 11  |-  ( z  e.  ( ( B  -  r ) (,) B )  ->  (
( ( F  |`  ( ( B  -  r ) (,) B
) ) `  z
)  /  ( ( G  |`  ( ( B  -  r ) (,) B ) ) `  z ) )  =  ( ( F `  z )  /  ( G `  z )
) )
160159mpteq2ia 4283 . . . . . . . . . 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 2485 . . . . . . . . 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 6087 . . . . . . . 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 2512 . . . . . . 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 3503 . . . . . . . . . . . 12  |-  ( B (,) ( B  +  r ) )  C_  ( ( ( B  -  r ) (,) B )  u.  ( B (,) ( B  +  r ) ) )
165164, 54syl5sseqr 3389 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  ( (
( B  -  r
) (,) ( B  +  r ) ) 
\  { B }
) )
166165, 69sstrd 3350 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  A )
167 fssres 5601 . . . . . . . . . 10  |-  ( ( F : A --> RR  /\  ( B (,) ( B  +  r ) ) 
C_  A )  -> 
( F  |`  ( B (,) ( B  +  r ) ) ) : ( B (,) ( B  +  r
) ) --> RR )
16826, 166, 167syl2anc 643 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( F  |`  ( B (,) ( B  +  r ) ) ) : ( B (,) ( B  +  r
) ) --> RR )
169 fssres 5601 . . . . . . . . . 10  |-  ( ( G : A --> RR  /\  ( B (,) ( B  +  r ) ) 
C_  A )  -> 
( G  |`  ( B (,) ( B  +  r ) ) ) : ( B (,) ( B  +  r
) ) --> RR )
17074, 166, 169syl2anc 643 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( G  |`  ( B (,) ( B  +  r ) ) ) : ( B (,) ( B  +  r
) ) --> RR )
171 ioossre 10961 . . . . . . . . . . . . . 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 19786 . . . . . . . . . . . . 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 1185 . . . . . . . . . . . 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 18788 . . . . . . . . . . . . . 14  |-  ( B (,) ( B  +  r ) )  e.  ( topGen `  ran  (,) )
176 isopn3i 17134 . . . . . . . . . . . . . 14  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( B (,) ( B  +  r ) )  e.  ( topGen `  ran  (,) )
)  ->  ( ( int `  ( topGen `  ran  (,) ) ) `  ( B (,) ( B  +  r ) ) )  =  ( B (,) ( B  +  r
) ) )
17786, 175, 176mp2an 654 . . . . . . . . . . . . 13  |-  ( ( int `  ( topGen ` 
ran  (,) ) ) `  ( B (,) ( B  +  r ) ) )  =  ( B (,) ( B  +  r ) )
178177reseq2i 5134 . . . . . . . . . . . 12  |-  ( ( RR  _D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( B (,) ( B  +  r ) ) ) )  =  ( ( RR 
_D  F )  |`  ( B (,) ( B  +  r ) ) )
179174, 178syl6eq 2483 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( RR  _D  ( F  |`  ( B (,) ( B  +  r
) ) ) )  =  ( ( RR 
_D  F )  |`  ( B (,) ( B  +  r ) ) ) )
180179dmeqd 5063 . . . . . . . . . 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 3350 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  D )
182181, 94sstrd 3350 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  dom  ( RR 
_D  F ) )
183 ssdmres 5159 . . . . . . . . . . 11  |-  ( ( B (,) ( B  +  r ) ) 
C_  dom  ( RR  _D  F )  <->  dom  ( ( RR  _D  F )  |`  ( B (,) ( B  +  r )
) )  =  ( B (,) ( B  +  r ) ) )
184182, 183sylib 189 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( ( RR  _D  F )  |`  ( B (,) ( B  +  r ) ) )  =  ( B (,) ( B  +  r
) ) )
185180, 184eqtrd 2467 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( RR  _D  ( F  |`  ( B (,) ( B  +  r
) ) ) )  =  ( B (,) ( B  +  r
) ) )
18682, 83dvres 19786 . . . . . . . . . . . . 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 1185 . . . . . . . . . . . 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 5134 . . . . . . . . . . . 12  |-  ( ( RR  _D  G )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( B (,) ( B  +  r ) ) ) )  =  ( ( RR 
_D  G )  |`  ( B (,) ( B  +  r ) ) )
189187, 188syl6eq 2483 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( RR  _D  ( G  |`  ( B (,) ( B  +  r
) ) ) )  =  ( ( RR 
_D  G )  |`  ( B (,) ( B  +  r ) ) ) )
190189dmeqd 5063 . . . . . . . . . 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 3350 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  dom  ( RR 
_D  G ) )
192 ssdmres 5159 . . . . . . . . . . 11  |-  ( ( B (,) ( B  +  r ) ) 
C_  dom  ( RR  _D  G )  <->  dom  ( ( RR  _D  G )  |`  ( B (,) ( B  +  r )
) )  =  ( B (,) ( B  +  r ) ) )
193191, 192sylib 189 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( ( RR  _D  G )  |`  ( B (,) ( B  +  r ) ) )  =  ( B (,) ( B  +  r
) ) )
194190, 193eqtrd 2467 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  dom  ( RR  _D  ( G  |`  ( B (,) ( B  +  r
) ) ) )  =  ( B (,) ( B  +  r
) ) )
195 limcresi 19760 . . . . . . . . . 10  |-  ( F lim
CC  B )  C_  ( ( F  |`  ( B (,) ( B  +  r ) ) ) lim CC  B )
196195, 115sseldi 3338 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( ( F  |`  ( B (,) ( B  +  r ) ) ) lim CC  B ) )
197 limcresi 19760 . . . . . . . . . 10  |-  ( G lim
CC  B )  C_  ( ( G  |`  ( B (,) ( B  +  r ) ) ) lim CC  B )
198197, 119sseldi 3338 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
0  e.  ( ( G  |`  ( B (,) ( B  +  r ) ) ) lim CC  B ) )
199 df-ima 4882 . . . . . . . . . . 11  |-  ( G
" ( B (,) ( B  +  r
) ) )  =  ran  ( G  |`  ( B (,) ( B  +  r ) ) )
200 imass2 5231 . . . . . . . . . . . 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 3385 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  ran  ( G  |`  ( B (,) ( B  +  r ) ) ) 
C_  ( G " D ) )
203202, 126ssneldd 3343 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  ran  ( G  |`  ( B (,) ( B  +  r ) ) ) )
204189rneqd 5088 . . . . . . . . . . . 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 4882 . . . . . . . . . . . 12  |-  ( ( RR  _D  G )
" ( B (,) ( B  +  r
) ) )  =  ran  ( ( RR 
_D  G )  |`  ( B (,) ( B  +  r ) ) )
206204, 205syl6eqr 2485 . . . . . . . . . . 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 5231 . . . . . . . . . . . 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 3374 . . . . . . . . . 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 3343 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  -.  0  e.  ran  ( RR  _D  ( G  |`  ( B (,) ( B  +  r
) ) ) ) )
211 limcresi 19760 . . . . . . . . . . 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 5182 . . . . . . . . . . . . . 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 5721 . . . . . . . . . . . . . . . 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 5736 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( B (,) ( B  +  r
) )  ->  (
( ( RR  _D  F )  |`  ( B (,) ( B  +  r ) ) ) `
 z )  =  ( ( RR  _D  F ) `  z
) )
216214, 215sylan9eq 2487 . . . . . . . . . . . . . . 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 5721 . . . . . . . . . . . . . . . 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 5736 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( B (,) ( B  +  r
) )  ->  (
( ( RR  _D  G )  |`  ( B (,) ( B  +  r ) ) ) `
 z )  =  ( ( RR  _D  G ) `  z
) )
219217, 218sylan9eq 2487 . . . . . . . . . . . . . . 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 6090 . . . . . . . . . . . . . 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 4287 . . . . . . . . . . . . 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 2470 . . . . . . . . . . . 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 6087 . . . . . . . . . . 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 3388 . . . . . . . . . 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 3341 . . . . . . . . 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 19886 . . . . . . . 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 5182 . . . . . . . . . . 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 5736 . . . . . . . . . . . 12  |-  ( z  e.  ( B (,) ( B  +  r
) )  ->  (
( F  |`  ( B (,) ( B  +  r ) ) ) `
 z )  =  ( F `  z
) )
230 fvres 5736 . . . . . . . . . . . 12  |-  ( z  e.  ( B (,) ( B  +  r
) )  ->  (
( G  |`  ( B (,) ( B  +  r ) ) ) `
 z )  =  ( G `  z
) )
231229, 230oveq12d 6090 . . . . . . . . . . 11  |-  ( z  e.  ( B (,) ( B  +  r
) )  ->  (
( ( F  |`  ( B (,) ( B  +  r ) ) ) `  z )  /  ( ( G  |`  ( B (,) ( B  +  r )
) ) `  z
) )  =  ( ( F `  z
)  /  ( G `
 z ) ) )
232231mpteq2ia 4283 . . . . . . . . . 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 2485 . . . . . . . . 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 6087 . . . . . . . 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 2512 . . . . . . 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
) )
236 elin 3522 . . . . . . 7  |-  ( C  e.  ( ( ( ( z  e.  ( ( ( B  -  r ) (,) ( B  +  r )
)  \  { B } )  |->  ( ( F `  z )  /  ( G `  z ) ) )  |`  ( ( B  -  r ) (,) B
) ) lim CC  B
)  i^i  ( (
( z  e.  ( ( ( B  -  r ) (,) ( B  +  r )
)  \  { B } )  |->  ( ( F `  z )  /  ( G `  z ) ) )  |`  ( B (,) ( B  +  r )
) ) lim CC  B
) )  <->  ( C  e.  ( ( ( z  e.  ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  |->  ( ( F `  z
)  /  ( G `
 z ) ) )  |`  ( ( B  -  r ) (,) B ) ) lim CC  B )  /\  C  e.  ( ( ( z  e.  ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  |->  ( ( F `  z
)  /  ( G `
 z ) ) )  |`  ( B (,) ( B  +  r ) ) ) lim CC  B ) ) )
237163, 235, 236sylanbrc 646 . . . . . 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
) ) )
238 resmpt 5182 . . . . . . . . 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 ) ) ) )
23959, 238syl 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 ) ) ) )
240239oveq1d 6087 . . . . . . 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 ) )
24167sselda 3340 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  D )  ->  z  e.  A )
24225ffvelrnda 5861 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  A )  ->  ( F `  z )  e.  RR )
243241, 242syldan 457 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  D )  ->  ( F `  z )  e.  RR )
244243recnd 9103 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  D )  ->  ( F `  z )  e.  CC )
24573ffvelrnda 5861 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  A )  ->  ( G `  z )  e.  RR )
246241, 245syldan 457 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  D )  ->  ( G `  z )  e.  RR )
247246recnd 9103 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  D )  ->  ( G `  z )  e.  CC )
248125adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  D )  ->  -.  0  e.  ( G " D ) )
249 ffn 5582 . . . . . . . . . . . . . . . . 17  |-  ( G : A --> RR  ->  G  Fn  A )
25073, 249syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  G  Fn  A )
251250adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  D )  ->  G  Fn  A )
25267adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  D )  ->  D  C_  A )
253 simpr 448 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  D )  ->  z  e.  D )
254 fnfvima 5967 . . . . . . . . . . . . . . 15  |-  ( ( G  Fn  A  /\  D  C_  A  /\  z  e.  D )  ->  ( G `  z )  e.  ( G " D
) )
255251, 252, 253, 254syl3anc 1184 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  z  e.  D )  ->  ( G `  z )  e.  ( G " D
) )
256 eleq1 2495 . . . . . . . . . . . . . 14  |-  ( ( G `  z )  =  0  ->  (
( G `  z
)  e.  ( G
" D )  <->  0  e.  ( G " D ) ) )
257255, 256syl5ibcom 212 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  D )  ->  (
( G `  z
)  =  0  -> 
0  e.  ( G
" D ) ) )
258257necon3bd 2635 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  D )  ->  ( -.  0  e.  ( G " D )  -> 
( G `  z
)  =/=  0 ) )
259248, 258mpd 15 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  D )  ->  ( G `  z )  =/=  0 )
260244, 247, 259divcld 9779 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  D )  ->  (
( F `  z
)  /  ( G `
 z ) )  e.  CC )
261260adantlr 696 . . . . . . . . 9  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  (
( B  -  r
) (,) ( B  +  r ) ) 
C_  I ) )  /\  z  e.  D
)  ->  ( ( F `  z )  /  ( G `  z ) )  e.  CC )
262 eqid 2435 . . . . . . . . 9  |-  ( z  e.  D  |->  ( ( F `  z )  /  ( G `  z ) ) )  =  ( z  e.  D  |->  ( ( F `
 z )  / 
( G `  z
) ) )
263261, 262fmptd 5884 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( z  e.  D  |->  ( ( F `  z )  /  ( G `  z )
) ) : D --> CC )
264 difss 3466 . . . . . . . . . . 11  |-  ( I 
\  { B }
)  C_  I
26558, 264eqsstri 3370 . . . . . . . . . 10  |-  D  C_  I
26613, 61syl6ss 3352 . . . . . . . . . 10  |-  ( ph  ->  I  C_  CC )
267265, 266syl5ss 3351 . . . . . . . . 9  |-  ( ph  ->  D  C_  CC )
268267adantr 452 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  D  C_  CC )
269 eqid 2435 . . . . . . . 8  |-  ( (
TopOpen ` fld )t  ( D  u.  { B } ) )  =  ( ( TopOpen ` fld )t  ( D  u.  { B } ) )
27058uneq1i 3489 . . . . . . . . . . . . . . . . 17  |-  ( D  u.  { B }
)  =  ( ( I  \  { B } )  u.  { B } )
271 undif1 3695 . . . . . . . . . . . . . . . . 17  |-  ( ( I  \  { B } )  u.  { B } )  =  ( I  u.  { B } )
272270, 271eqtri 2455 . . . . . . . . . . . . . . . 16  |-  ( D  u.  { B }
)  =  ( I  u.  { B }
)
273 simprr 734 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) ( B  +  r )
)  C_  I )
27442, 273sstrd 3350 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  { B }  C_  I
)
275 ssequn2 3512 . . . . . . . . . . . . . . . . 17  |-  ( { B }  C_  I  <->  ( I  u.  { B } )  =  I )
276274, 275sylib 189 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( I  u.  { B } )  =  I )
277272, 276syl5eq 2479 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( D  u.  { B } )  =  I )
278277oveq2d 6088 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( TopOpen ` fld )t  ( D  u.  { B } ) )  =  ( ( TopOpen ` fld )t  I
) )
27913adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  I  C_  RR )
280 eqid 2435 . . . . . . . . . . . . . . . 16  |-  ( topGen ` 
ran  (,) )  =  (
topGen `  ran  (,) )
28182, 280rerest 18823 . . . . . . . . . . . . . . 15  |-  ( I 
C_  RR  ->  ( (
TopOpen ` fld )t  I )  =  ( ( topGen `  ran  (,) )t  I
) )
282279, 281syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( TopOpen ` fld )t  I )  =  ( ( topGen `  ran  (,) )t  I
) )
283278, 282eqtrd 2467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( TopOpen ` fld )t  ( D  u.  { B } ) )  =  ( ( topGen ` 
ran  (,) )t  I ) )
284283fveq2d 5723 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( int `  (
( TopOpen ` fld )t  ( D  u.  { B } ) ) )  =  ( int `  ( ( topGen `  ran  (,) )t  I ) ) )
285284fveq1d 5721 . . . . . . . . . . 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 )
) ) )
28682cnfldtopon 18805 . . . . . . . . . . . . . . 15  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
287266adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  I  C_  CC )
288 resttopon 17213 . . . . . . . . . . . . . . 15  |-  ( ( ( TopOpen ` fld )  e.  (TopOn `  CC )  /\  I  C_  CC )  ->  (
( TopOpen ` fld )t  I )  e.  (TopOn `  I ) )
289286, 287, 288sylancr 645 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( TopOpen ` fld )t  I )  e.  (TopOn `  I ) )
290 topontop 16979 . . . . . . . . . . . . . 14  |-  ( ( ( TopOpen ` fld )t  I )  e.  (TopOn `  I )  ->  (
( TopOpen ` fld )t  I )  e.  Top )
291289, 290syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( TopOpen ` fld )t  I )  e.  Top )
292282, 291eqeltrrd 2510 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( topGen `  ran  (,) )t  I )  e.  Top )
293 iooretop 18788 . . . . . . . . . . . . . 14  |-  ( ( B  -  r ) (,) ( B  +  r ) )  e.  ( topGen `  ran  (,) )
294293a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) ( B  +  r )
)  e.  ( topGen ` 
ran  (,) ) )
2954adantr 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  I  e.  ( topGen ` 
ran  (,) ) )
296 restopn2 17229 . . . . . . . . . . . . . 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 ) ) )
29786, 295, 296sylancr 645 . . . . . . . . . . . . 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 )
) )
298294, 273, 297mpbir2and 889 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) ( B  +  r )
)  e.  ( (
topGen `  ran  (,) )t  I
) )
299 isopn3i 17134 . . . . . . . . . . . 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 ) ) )
300292, 298, 299syl2anc 643 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( int `  (
( topGen `  ran  (,) )t  I
) ) `  (
( B  -  r
) (,) ( B  +  r ) ) )  =  ( ( B  -  r ) (,) ( B  +  r ) ) )
301285, 300eqtrd 2467 . . . . . . . . . 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 ) ) )
30241, 301eleqtrrd 2512 . . . . . . . . 9  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  ->  B  e.  ( ( int `  ( ( TopOpen ` fld )t  ( D  u.  { B } ) ) ) `
 ( ( B  -  r ) (,) ( B  +  r ) ) ) )
303 undif1 3695 . . . . . . . . . . 11  |-  ( ( ( ( B  -  r ) (,) ( B  +  r )
)  \  { B } )  u.  { B } )  =  ( ( ( B  -  r ) (,) ( B  +  r )
)  u.  { B } )
304 ssequn2 3512 . . . . . . . . . . . 12  |-  ( { B }  C_  (
( B  -  r
) (,) ( B  +  r ) )  <-> 
( ( ( B  -  r ) (,) ( B  +  r ) )  u.  { B } )  =  ( ( B  -  r
) (,) ( B  +  r ) ) )
30542, 304sylib 189 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( ( B  -  r ) (,) ( B  +  r ) )  u.  { B } )  =  ( ( B  -  r
) (,) ( B  +  r ) ) )
306303, 305syl5eq 2479 . . . . . . . . . 10  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  u. 
{ B } )  =  ( ( B  -  r ) (,) ( B  +  r ) ) )
307306fveq2d 5723 . . . . . . . . 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 ) ) ) )
308302, 307eleqtrrd 2512 . . . . . . . 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 } ) ) )
309263, 59, 268, 82, 269, 308limcres 19761 . . . . . . 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
) )
31080, 61sstri 3349 . . . . . . . . 9  |-  ( ( B  -  r ) (,) B )  C_  CC
311310a1i 11 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( ( B  -  r ) (,) B
)  C_  CC )
312171, 61sstri 3349 . . . . . . . . 9  |-  ( B (,) ( B  +  r ) )  C_  CC
313312a1i 11 . . . . . . . 8  |-  ( (
ph  /\  ( r  e.  RR+  /\  ( ( B  -  r ) (,) ( B  +  r ) )  C_  I ) )  -> 
( B (,) ( B  +  r )
)  C_  CC )
31459sselda 3340 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  (
( B  -  r
) (,) ( B  +  r ) ) 
C_  I ) )  /\  z  e.  ( ( ( B  -  r ) (,) ( B  +  r )
)  \  { B } ) )  -> 
z  e.  D )
315314, 261syldan 457 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  (
( B  -  r
) (,) ( B  +  r ) ) 
C_  I ) )  /\  z  e.  ( ( ( B  -  r ) (,) ( B  +  r )
)  \  { B } ) )  -> 
( ( F `  z )  /  ( G `  z )
)  e.  CC )
316 eqid 2435 . . . . . . . . . 10  |-  ( z  e.  ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  |->  ( ( F `  z
)  /  ( G `
 z ) ) )  =  ( z  e.  ( ( ( B  -  r ) (,) ( B  +  r ) )  \  { B } )  |->  ( ( F `  z
)  /  ( G `
 z ) ) )
317315, 316fmptd 5884 . . . . . . . . 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 )
31854feq2d 5572 . . . . . . . . 9  |-  ( (
ph  /\  (