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

Theorem lhop2 19362
Description: L'Hôpital's Rule for limits from the right. If  F and  G are differentiable real functions on  ( A ,  B ), and 
F and  G both approach 0 at  B, and  G ( x ) and  G'  ( x ) are not zero on  ( A ,  B ), 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, 29-Dec-2016.)
Hypotheses
Ref Expression
lhop2.a  |-  ( ph  ->  A  e.  RR* )
lhop2.b  |-  ( ph  ->  B  e.  RR )
lhop2.l  |-  ( ph  ->  A  <  B )
lhop2.f  |-  ( ph  ->  F : ( A (,) B ) --> RR )
lhop2.g  |-  ( ph  ->  G : ( A (,) B ) --> RR )
lhop2.if  |-  ( ph  ->  dom  ( RR  _D  F )  =  ( A (,) B ) )
lhop2.ig  |-  ( ph  ->  dom  ( RR  _D  G )  =  ( A (,) B ) )
lhop2.f0  |-  ( ph  ->  0  e.  ( F lim
CC  B ) )
lhop2.g0  |-  ( ph  ->  0  e.  ( G lim
CC  B ) )
lhop2.gn0  |-  ( ph  ->  -.  0  e.  ran  G )
lhop2.gd0  |-  ( ph  ->  -.  0  e.  ran  ( RR  _D  G
) )
lhop2.c  |-  ( ph  ->  C  e.  ( ( z  e.  ( A (,) B )  |->  ( ( ( RR  _D  F ) `  z
)  /  ( ( RR  _D  G ) `
 z ) ) ) lim CC  B ) )
Assertion
Ref Expression
lhop2  |-  ( ph  ->  C  e.  ( ( z  e.  ( A (,) B )  |->  ( ( F `  z
)  /  ( G `
 z ) ) ) lim CC  B ) )
Distinct variable groups:    z, A    z, B    z, C    ph, z    z, F    z, G

Proof of Theorem lhop2
Dummy variables  x  a  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 qssre 10326 . . 3  |-  QQ  C_  RR
2 lhop2.a . . . 4  |-  ( ph  ->  A  e.  RR* )
3 lhop2.b . . . . 5  |-  ( ph  ->  B  e.  RR )
43rexrd 8881 . . . 4  |-  ( ph  ->  B  e.  RR* )
5 lhop2.l . . . 4  |-  ( ph  ->  A  <  B )
6 qbtwnxr 10527 . . . 4  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  A  < 
B )  ->  E. a  e.  QQ  ( A  < 
a  /\  a  <  B ) )
72, 4, 5, 6syl3anc 1182 . . 3  |-  ( ph  ->  E. a  e.  QQ  ( A  <  a  /\  a  <  B ) )
8 ssrexv 3238 . . 3  |-  ( QQ  C_  RR  ->  ( E. a  e.  QQ  ( A  <  a  /\  a  <  B )  ->  E. a  e.  RR  ( A  < 
a  /\  a  <  B ) ) )
91, 7, 8mpsyl 59 . 2  |-  ( ph  ->  E. a  e.  RR  ( A  <  a  /\  a  <  B ) )
10 simpr 447 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  z  e.  ( a (,) B
) )
11 simprl 732 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  a  e.  RR )
1211adantr 451 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  a  e.  RR )
133ad2antrr 706 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  B  e.  RR )
14 elioore 10686 . . . . . . . . . 10  |-  ( z  e.  ( a (,) B )  ->  z  e.  RR )
1514adantl 452 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  z  e.  RR )
16 iooneg 10756 . . . . . . . . 9  |-  ( ( a  e.  RR  /\  B  e.  RR  /\  z  e.  RR )  ->  (
z  e.  ( a (,) B )  <->  -u z  e.  ( -u B (,) -u a ) ) )
1712, 13, 15, 16syl3anc 1182 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  (
z  e.  ( a (,) B )  <->  -u z  e.  ( -u B (,) -u a ) ) )
1810, 17mpbid 201 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  -u z  e.  ( -u B (,) -u a ) )
1918adantrr 697 . . . . . 6  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  ( z  e.  ( a (,) B )  /\  -u z  =/=  -u B ) )  ->  -u z  e.  (
-u B (,) -u a
) )
20 lhop2.f . . . . . . . . . 10  |-  ( ph  ->  F : ( A (,) B ) --> RR )
2120ad2antrr 706 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  F : ( A (,) B ) --> RR )
22 elioore 10686 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( -u B (,) -u a )  ->  x  e.  RR )
2322adantl 452 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  x  e.  RR )
2423recnd 8861 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  x  e.  CC )
2524negnegd 9148 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -u -u x  =  x
)
26 simpr 447 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  x  e.  ( -u B (,) -u a ) )
2725, 26eqeltrd 2357 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -u -u x  e.  ( -u B (,) -u a
) )
2811adantr 451 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
a  e.  RR )
293ad2antrr 706 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  B  e.  RR )
3023renegcld 9210 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -u x  e.  RR )
31 iooneg 10756 . . . . . . . . . . . 12  |-  ( ( a  e.  RR  /\  B  e.  RR  /\  -u x  e.  RR )  ->  ( -u x  e.  ( a (,) B )  <->  -u -u x  e.  ( -u B (,) -u a ) ) )
3228, 29, 30, 31syl3anc 1182 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( -u x  e.  ( a (,) B )  <->  -u -u x  e.  (
-u B (,) -u a
) ) )
3327, 32mpbird 223 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -u x  e.  ( a (,) B ) )
342adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  A  e.  RR* )
35 simprrl 740 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  A  <  a
)
3611rexrd 8881 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  a  e.  RR* )
37 xrltle 10483 . . . . . . . . . . . . . 14  |-  ( ( A  e.  RR*  /\  a  e.  RR* )  ->  ( A  <  a  ->  A  <_  a ) )
3834, 36, 37syl2anc 642 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( A  < 
a  ->  A  <_  a ) )
3935, 38mpd 14 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  A  <_  a
)
40 iooss1 10691 . . . . . . . . . . . 12  |-  ( ( A  e.  RR*  /\  A  <_  a )  ->  (
a (,) B ) 
C_  ( A (,) B ) )
4134, 39, 40syl2anc 642 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( a (,) B )  C_  ( A (,) B ) )
4241sselda 3180 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  -u x  e.  ( a (,) B
) )  ->  -u x  e.  ( A (,) B
) )
4333, 42syldan 456 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -u x  e.  ( A (,) B ) )
4421, 43ffvelrnd 5666 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( F `  -u x
)  e.  RR )
4544recnd 8861 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( F `  -u x
)  e.  CC )
46 lhop2.g . . . . . . . . . 10  |-  ( ph  ->  G : ( A (,) B ) --> RR )
4746ad2antrr 706 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  G : ( A (,) B ) --> RR )
4847, 43ffvelrnd 5666 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( G `  -u x
)  e.  RR )
4948recnd 8861 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( G `  -u x
)  e.  CC )
50 lhop2.gn0 . . . . . . . . 9  |-  ( ph  ->  -.  0  e.  ran  G )
5150ad2antrr 706 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -.  0  e.  ran  G )
5246adantr 451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  G : ( A (,) B ) --> RR )
53 ax-resscn 8794 . . . . . . . . . . . . . 14  |-  RR  C_  CC
54 fss 5397 . . . . . . . . . . . . . 14  |-  ( ( G : ( A (,) B ) --> RR 
/\  RR  C_  CC )  ->  G : ( A (,) B ) --> CC )
5552, 53, 54sylancl 643 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  G : ( A (,) B ) --> CC )
5655adantr 451 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  G : ( A (,) B ) --> CC )
57 ffn 5389 . . . . . . . . . . . 12  |-  ( G : ( A (,) B ) --> CC  ->  G  Fn  ( A (,) B ) )
5856, 57syl 15 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  G  Fn  ( A (,) B ) )
59 fnfvelrn 5662 . . . . . . . . . . 11  |-  ( ( G  Fn  ( A (,) B )  /\  -u x  e.  ( A (,) B ) )  ->  ( G `  -u x )  e.  ran  G )
6058, 43, 59syl2anc 642 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( G `  -u x
)  e.  ran  G
)
61 eleq1 2343 . . . . . . . . . 10  |-  ( ( G `  -u x
)  =  0  -> 
( ( G `  -u x )  e.  ran  G  <->  0  e.  ran  G
) )
6260, 61syl5ibcom 211 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( G `  -u x )  =  0  ->  0  e.  ran  G ) )
6362necon3bd 2483 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( -.  0  e. 
ran  G  ->  ( G `
 -u x )  =/=  0 ) )
6451, 63mpd 14 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( G `  -u x
)  =/=  0 )
6545, 49, 64divcld 9536 . . . . . 6  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( F `  -u x )  /  ( G `  -u x ) )  e.  CC )
66 limcresi 19235 . . . . . . . 8  |-  ( ( z  e.  RR  |->  -u z ) lim CC  B ) 
C_  ( ( ( z  e.  RR  |->  -u z )  |`  (
a (,) B ) ) lim CC  B )
67 ioossre 10712 . . . . . . . . . 10  |-  ( a (,) B )  C_  RR
68 resmpt 5000 . . . . . . . . . 10  |-  ( ( a (,) B ) 
C_  RR  ->  ( ( z  e.  RR  |->  -u z )  |`  (
a (,) B ) )  =  ( z  e.  ( a (,) B )  |->  -u z
) )
6967, 68ax-mp 8 . . . . . . . . 9  |-  ( ( z  e.  RR  |->  -u z )  |`  (
a (,) B ) )  =  ( z  e.  ( a (,) B )  |->  -u z
)
7069oveq1i 5868 . . . . . . . 8  |-  ( ( ( z  e.  RR  |->  -u z )  |`  (
a (,) B ) ) lim CC  B )  =  ( ( z  e.  ( a (,) B )  |->  -u z
) lim CC  B )
7166, 70sseqtri 3210 . . . . . . 7  |-  ( ( z  e.  RR  |->  -u z ) lim CC  B ) 
C_  ( ( z  e.  ( a (,) B )  |->  -u z
) lim CC  B )
72 eqid 2283 . . . . . . . . . 10  |-  ( z  e.  RR  |->  -u z
)  =  ( z  e.  RR  |->  -u z
)
7372negcncf 18421 . . . . . . . . 9  |-  ( RR  C_  CC  ->  ( z  e.  RR  |->  -u z )  e.  ( RR -cn-> CC ) )
7453, 73mp1i 11 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( z  e.  RR  |->  -u z )  e.  ( RR -cn-> CC ) )
753adantr 451 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  B  e.  RR )
76 negeq 9044 . . . . . . . 8  |-  ( z  =  B  ->  -u z  =  -u B )
7774, 75, 76cnmptlimc 19240 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -u B  e.  ( ( z  e.  RR  |->  -u z ) lim CC  B
) )
7871, 77sseldi 3178 . . . . . 6  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -u B  e.  ( ( z  e.  ( a (,) B ) 
|->  -u z ) lim CC  B ) )
7975renegcld 9210 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -u B  e.  RR )
8011renegcld 9210 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -u a  e.  RR )
8180rexrd 8881 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -u a  e.  RR* )
82 simprrr 741 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  a  <  B
)
8311, 75ltnegd 9350 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( a  < 
B  <->  -u B  <  -u a
) )
8482, 83mpbid 201 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -u B  <  -u a
)
85 eqid 2283 . . . . . . . . 9  |-  ( x  e.  ( -u B (,) -u a )  |->  ( F `  -u x
) )  =  ( x  e.  ( -u B (,) -u a )  |->  ( F `  -u x
) )
8644, 85fmptd 5684 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( x  e.  ( -u B (,) -u a )  |->  ( F `
 -u x ) ) : ( -u B (,) -u a ) --> RR )
87 eqid 2283 . . . . . . . . 9  |-  ( x  e.  ( -u B (,) -u a )  |->  ( G `  -u x
) )  =  ( x  e.  ( -u B (,) -u a )  |->  ( G `  -u x
) )
8848, 87fmptd 5684 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( x  e.  ( -u B (,) -u a )  |->  ( G `
 -u x ) ) : ( -u B (,) -u a ) --> RR )
89 reex 8828 . . . . . . . . . . . . . 14  |-  RR  e.  _V
9089prid1 3734 . . . . . . . . . . . . 13  |-  RR  e.  { RR ,  CC }
9190a1i 10 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  RR  e.  { RR ,  CC } )
92 neg1cn 9813 . . . . . . . . . . . . 13  |-  -u 1  e.  CC
9392a1i 10 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -u 1  e.  CC )
9420adantr 451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  F : ( A (,) B ) --> RR )
9594ffvelrnda 5665 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  y  e.  ( A (,) B
) )  ->  ( F `  y )  e.  RR )
9695recnd 8861 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  y  e.  ( A (,) B
) )  ->  ( F `  y )  e.  CC )
97 fvex 5539 . . . . . . . . . . . . 13  |-  ( ( RR  _D  F ) `
 y )  e. 
_V
9897a1i 10 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  y  e.  ( A (,) B
) )  ->  (
( RR  _D  F
) `  y )  e.  _V )
99 ax-1cn 8795 . . . . . . . . . . . . . 14  |-  1  e.  CC
10099a1i 10 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
1  e.  CC )
101 simpr 447 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  RR )  ->  x  e.  RR )
102101recnd 8861 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  RR )  ->  x  e.  CC )
10399a1i 10 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  RR )  ->  1  e.  CC )
10491dvmptid 19306 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  ( x  e.  RR  |->  x ) )  =  ( x  e.  RR  |->  1 ) )
105 ioossre 10712 . . . . . . . . . . . . . . 15  |-  ( -u B (,) -u a )  C_  RR
106105a1i 10 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( -u B (,) -u a )  C_  RR )
107 eqid 2283 . . . . . . . . . . . . . . 15  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
108107tgioo2 18309 . . . . . . . . . . . . . 14  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
109 iooretop 18275 . . . . . . . . . . . . . . 15  |-  ( -u B (,) -u a )  e.  ( topGen `  ran  (,) )
110109a1i 10 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( -u B (,) -u a )  e.  ( topGen `  ran  (,) )
)
11191, 102, 103, 104, 106, 108, 107, 110dvmptres 19312 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  ( x  e.  ( -u B (,) -u a
)  |->  x ) )  =  ( x  e.  ( -u B (,) -u a )  |->  1 ) )
11291, 24, 100, 111dvmptneg 19315 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  ( x  e.  ( -u B (,) -u a
)  |->  -u x ) )  =  ( x  e.  ( -u B (,) -u a )  |->  -u 1
) )
11394feqmptd 5575 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  F  =  ( y  e.  ( A (,) B )  |->  ( F `  y ) ) )
114113oveq2d 5874 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  F )  =  ( RR  _D  ( y  e.  ( A (,) B )  |->  ( F `
 y ) ) ) )
115 dvf 19257 . . . . . . . . . . . . . . 15  |-  ( RR 
_D  F ) : dom  ( RR  _D  F ) --> CC
116 lhop2.if . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  dom  ( RR  _D  F )  =  ( A (,) B ) )
117116adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  dom  ( RR  _D  F )  =  ( A (,) B ) )
118117feq2d 5380 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( ( RR 
_D  F ) : dom  ( RR  _D  F ) --> CC  <->  ( RR  _D  F ) : ( A (,) B ) --> CC ) )
119115, 118mpbii 202 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  F ) : ( A (,) B ) --> CC )
120119feqmptd 5575 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  F )  =  ( y  e.  ( A (,) B )  |->  ( ( RR  _D  F
) `  y )
) )
121114, 120eqtr3d 2317 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  ( y  e.  ( A (,) B ) 
|->  ( F `  y
) ) )  =  ( y  e.  ( A (,) B ) 
|->  ( ( RR  _D  F ) `  y
) ) )
122 fveq2 5525 . . . . . . . . . . . 12  |-  ( y  =  -u x  ->  ( F `  y )  =  ( F `  -u x ) )
123 fveq2 5525 . . . . . . . . . . . 12  |-  ( y  =  -u x  ->  (
( RR  _D  F
) `  y )  =  ( ( RR 
_D  F ) `  -u x ) )
12491, 91, 43, 93, 96, 98, 112, 121, 122, 123dvmptco 19321 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  ( x  e.  ( -u B (,) -u a
)  |->  ( F `  -u x ) ) )  =  ( x  e.  ( -u B (,) -u a )  |->  ( ( ( RR  _D  F
) `  -u x )  x.  -u 1 ) ) )
125119adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( RR  _D  F
) : ( A (,) B ) --> CC )
126125, 43ffvelrnd 5666 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( RR  _D  F ) `  -u x
)  e.  CC )
127126, 93mulcomd 8856 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( ( RR 
_D  F ) `  -u x )  x.  -u 1
)  =  ( -u
1  x.  ( ( RR  _D  F ) `
 -u x ) ) )
128126mulm1d 9231 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( -u 1  x.  (
( RR  _D  F
) `  -u x ) )  =  -u (
( RR  _D  F
) `  -u x ) )
129127, 128eqtrd 2315 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( ( RR 
_D  F ) `  -u x )  x.  -u 1
)  =  -u (
( RR  _D  F
) `  -u x ) )
130129mpteq2dva 4106 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( x  e.  ( -u B (,) -u a )  |->  ( ( ( RR  _D  F
) `  -u x )  x.  -u 1 ) )  =  ( x  e.  ( -u B (,) -u a )  |->  -u (
( RR  _D  F
) `  -u x ) ) )
131124, 130eqtrd 2315 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  ( x  e.  ( -u B (,) -u a
)  |->  ( F `  -u x ) ) )  =  ( x  e.  ( -u B (,) -u a )  |->  -u (
( RR  _D  F
) `  -u x ) ) )
132131dmeqd 4881 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  dom  ( RR  _D  ( x  e.  (
-u B (,) -u a
)  |->  ( F `  -u x ) ) )  =  dom  ( x  e.  ( -u B (,) -u a )  |->  -u ( ( RR  _D  F ) `  -u x
) ) )
133 negex 9050 . . . . . . . . . 10  |-  -u (
( RR  _D  F
) `  -u x )  e.  _V
134 eqid 2283 . . . . . . . . . 10  |-  ( x  e.  ( -u B (,) -u a )  |->  -u ( ( RR  _D  F ) `  -u x
) )  =  ( x  e.  ( -u B (,) -u a )  |->  -u ( ( RR  _D  F ) `  -u x
) )
135133, 134dmmpti 5373 . . . . . . . . 9  |-  dom  (
x  e.  ( -u B (,) -u a )  |->  -u ( ( RR  _D  F ) `  -u x
) )  =  (
-u B (,) -u a
)
136132, 135syl6eq 2331 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  dom  ( RR  _D  ( x  e.  (
-u B (,) -u a
)  |->  ( F `  -u x ) ) )  =  ( -u B (,) -u a ) )
13752ffvelrnda 5665 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  y  e.  ( A (,) B
) )  ->  ( G `  y )  e.  RR )
138137recnd 8861 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  y  e.  ( A (,) B
) )  ->  ( G `  y )  e.  CC )
139 fvex 5539 . . . . . . . . . . . . 13  |-  ( ( RR  _D  G ) `
 y )  e. 
_V
140139a1i 10 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  y  e.  ( A (,) B
) )  ->  (
( RR  _D  G
) `  y )  e.  _V )
14152feqmptd 5575 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  G  =  ( y  e.  ( A (,) B )  |->  ( G `  y ) ) )
142141oveq2d 5874 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  G )  =  ( RR  _D  ( y  e.  ( A (,) B )  |->  ( G `
 y ) ) ) )
143 dvf 19257 . . . . . . . . . . . . . . 15  |-  ( RR 
_D  G ) : dom  ( RR  _D  G ) --> CC
144 lhop2.ig . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  dom  ( RR  _D  G )  =  ( A (,) B ) )
145144adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  dom  ( RR  _D  G )  =  ( A (,) B ) )
146145feq2d 5380 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( ( RR 
_D  G ) : dom  ( RR  _D  G ) --> CC  <->  ( RR  _D  G ) : ( A (,) B ) --> CC ) )
147143, 146mpbii 202 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  G ) : ( A (,) B ) --> CC )
148147feqmptd 5575 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  G )  =  ( y  e.  ( A (,) B )  |->  ( ( RR  _D  G
) `  y )
) )
149142, 148eqtr3d 2317 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  ( y  e.  ( A (,) B ) 
|->  ( G `  y
) ) )  =  ( y  e.  ( A (,) B ) 
|->  ( ( RR  _D  G ) `  y
) ) )
150 fveq2 5525 . . . . . . . . . . . 12  |-  ( y  =  -u x  ->  ( G `  y )  =  ( G `  -u x ) )
151 fveq2 5525 . . . . . . . . . . . 12  |-  ( y  =  -u x  ->  (
( RR  _D  G
) `  y )  =  ( ( RR 
_D  G ) `  -u x ) )
15291, 91, 43, 93, 138, 140, 112, 149, 150, 151dvmptco 19321 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  ( x  e.  ( -u B (,) -u a
)  |->  ( G `  -u x ) ) )  =  ( x  e.  ( -u B (,) -u a )  |->  ( ( ( RR  _D  G
) `  -u x )  x.  -u 1 ) ) )
153147adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( RR  _D  G
) : ( A (,) B ) --> CC )
154153, 43ffvelrnd 5666 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( RR  _D  G ) `  -u x
)  e.  CC )
155154, 93mulcomd 8856 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( ( RR 
_D  G ) `  -u x )  x.  -u 1
)  =  ( -u
1  x.  ( ( RR  _D  G ) `
 -u x ) ) )
156154mulm1d 9231 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( -u 1  x.  (
( RR  _D  G
) `  -u x ) )  =  -u (
( RR  _D  G
) `  -u x ) )
157155, 156eqtrd 2315 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( ( RR 
_D  G ) `  -u x )  x.  -u 1
)  =  -u (
( RR  _D  G
) `  -u x ) )
158157mpteq2dva 4106 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( x  e.  ( -u B (,) -u a )  |->  ( ( ( RR  _D  G
) `  -u x )  x.  -u 1 ) )  =  ( x  e.  ( -u B (,) -u a )  |->  -u (
( RR  _D  G
) `  -u x ) ) )
159152, 158eqtrd 2315 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  ( x  e.  ( -u B (,) -u a
)  |->  ( G `  -u x ) ) )  =  ( x  e.  ( -u B (,) -u a )  |->  -u (
( RR  _D  G
) `  -u x ) ) )
160159dmeqd 4881 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  dom  ( RR  _D  ( x  e.  (
-u B (,) -u a
)  |->  ( G `  -u x ) ) )  =  dom  ( x  e.  ( -u B (,) -u a )  |->  -u ( ( RR  _D  G ) `  -u x
) ) )
161 negex 9050 . . . . . . . . . 10  |-  -u (
( RR  _D  G
) `  -u x )  e.  _V
162 eqid 2283 . . . . . . . . . 10  |-  ( x  e.  ( -u B (,) -u a )  |->  -u ( ( RR  _D  G ) `  -u x
) )  =  ( x  e.  ( -u B (,) -u a )  |->  -u ( ( RR  _D  G ) `  -u x
) )
163161, 162dmmpti 5373 . . . . . . . . 9  |-  dom  (
x  e.  ( -u B (,) -u a )  |->  -u ( ( RR  _D  G ) `  -u x
) )  =  (
-u B (,) -u a
)
164160, 163syl6eq 2331 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  dom  ( RR  _D  ( x  e.  (
-u B (,) -u a
)  |->  ( G `  -u x ) ) )  =  ( -u B (,) -u a ) )
16543adantrr 697 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  ( x  e.  ( -u B (,) -u a )  /\  -u x  =/=  B ) )  ->  -u x  e.  ( A (,) B
) )
166 limcresi 19235 . . . . . . . . . . 11  |-  ( ( x  e.  RR  |->  -u x ) lim CC  -u B
)  C_  ( (
( x  e.  RR  |->  -u x )  |`  ( -u B (,) -u a
) ) lim CC  -u B
)
167 resmpt 5000 . . . . . . . . . . . . 13  |-  ( (
-u B (,) -u a
)  C_  RR  ->  ( ( x  e.  RR  |->  -u x )  |`  ( -u B (,) -u a
) )  =  ( x  e.  ( -u B (,) -u a )  |->  -u x ) )
168105, 167ax-mp 8 . . . . . . . . . . . 12  |-  ( ( x  e.  RR  |->  -u x )  |`  ( -u B (,) -u a
) )  =  ( x  e.  ( -u B (,) -u a )  |->  -u x )
169168oveq1i 5868 . . . . . . . . . . 11  |-  ( ( ( x  e.  RR  |->  -u x )  |`  ( -u B (,) -u a
) ) lim CC  -u B
)  =  ( ( x  e.  ( -u B (,) -u a )  |->  -u x ) lim CC  -u B
)
170166, 169sseqtri 3210 . . . . . . . . . 10  |-  ( ( x  e.  RR  |->  -u x ) lim CC  -u B
)  C_  ( (
x  e.  ( -u B (,) -u a )  |->  -u x ) lim CC  -u B
)
17175recnd 8861 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  B  e.  CC )
172171negnegd 9148 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -u -u B  =  B )
173 eqid 2283 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  |->  -u x
)  =  ( x  e.  RR  |->  -u x
)
174173negcncf 18421 . . . . . . . . . . . . 13  |-  ( RR  C_  CC  ->  ( x  e.  RR  |->  -u x )  e.  ( RR -cn-> CC ) )
17553, 174mp1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( x  e.  RR  |->  -u x )  e.  ( RR -cn-> CC ) )
176 negeq 9044 . . . . . . . . . . . 12  |-  ( x  =  -u B  ->  -u x  =  -u -u B )
177175, 79, 176cnmptlimc 19240 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -u -u B  e.  ( ( x  e.  RR  |->  -u x ) lim CC  -u B
) )
178172, 177eqeltrrd 2358 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  B  e.  ( ( x  e.  RR  |->  -u x ) lim CC  -u B
) )
179170, 178sseldi 3178 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  B  e.  ( ( x  e.  (
-u B (,) -u a
)  |->  -u x ) lim CC  -u B ) )
180 lhop2.f0 . . . . . . . . . . 11  |-  ( ph  ->  0  e.  ( F lim
CC  B ) )
181180adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  0  e.  ( F lim CC  B ) )
182113oveq1d 5873 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( F lim CC  B )  =  ( ( y  e.  ( A (,) B ) 
|->  ( F `  y
) ) lim CC  B
) )
183181, 182eleqtrd 2359 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  0  e.  ( ( y  e.  ( A (,) B ) 
|->  ( F `  y
) ) lim CC  B
) )
184 eliooord 10710 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( -u B (,) -u a )  -> 
( -u B  <  x  /\  x  <  -u a
) )
185184adantl 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( -u B  <  x  /\  x  <  -u a
) )
186185simpld 445 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -u B  <  x )
18729, 23, 186ltnegcon1d 9352 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -u x  <  B )
18830, 187ltned 8955 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -u x  =/=  B )
189188neneqd 2462 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -.  -u x  =  B )
190189pm2.21d 98 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( -u x  =  B  ->  ( F `  -u x )  =  0 ) )
191190impr 602 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  ( x  e.  ( -u B (,) -u a )  /\  -u x  =  B ) )  ->  ( F `  -u x )  =  0 )
192165, 96, 179, 183, 122, 191limcco 19243 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  0  e.  ( ( x  e.  (
-u B (,) -u a
)  |->  ( F `  -u x ) ) lim CC  -u B ) )
193 lhop2.g0 . . . . . . . . . . 11  |-  ( ph  ->  0  e.  ( G lim
CC  B ) )
194193adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  0  e.  ( G lim CC  B ) )
195141oveq1d 5873 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( G lim CC  B )  =  ( ( y  e.  ( A (,) B ) 
|->  ( G `  y
) ) lim CC  B
) )
196194, 195eleqtrd 2359 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  0  e.  ( ( y  e.  ( A (,) B ) 
|->  ( G `  y
) ) lim CC  B
) )
197189pm2.21d 98 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( -u x  =  B  ->  ( G `  -u x )  =  0 ) )
198197impr 602 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  ( x  e.  ( -u B (,) -u a )  /\  -u x  =  B ) )  ->  ( G `  -u x )  =  0 )
199165, 138, 179, 196, 150, 198limcco 19243 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  0  e.  ( ( x  e.  (
-u B (,) -u a
)  |->  ( G `  -u x ) ) lim CC  -u B ) )
20050adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -.  0  e.  ran  G )
20160, 87fmptd 5684 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( x  e.  ( -u B (,) -u a )  |->  ( G `
 -u x ) ) : ( -u B (,) -u a ) --> ran 
G )
202 frn 5395 . . . . . . . . . . 11  |-  ( ( x  e.  ( -u B (,) -u a )  |->  ( G `  -u x
) ) : (
-u B (,) -u a
) --> ran  G  ->  ran  ( x  e.  (
-u B (,) -u a
)  |->  ( G `  -u x ) )  C_  ran  G )
203201, 202syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ran  ( x  e.  ( -u B (,) -u a )  |->  ( G `
 -u x ) ) 
C_  ran  G )
204203sseld 3179 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( 0  e. 
ran  ( x  e.  ( -u B (,) -u a )  |->  ( G `
 -u x ) )  ->  0  e.  ran  G ) )
205200, 204mtod 168 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -.  0  e.  ran  ( x  e.  (
-u B (,) -u a
)  |->  ( G `  -u x ) ) )
206 lhop2.gd0 . . . . . . . . . 10  |-  ( ph  ->  -.  0  e.  ran  ( RR  _D  G
) )
207206adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -.  0  e.  ran  ( RR  _D  G
) )
208159rneqd 4906 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ran  ( RR  _D  ( x  e.  (
-u B (,) -u a
)  |->  ( G `  -u x ) ) )  =  ran  ( x  e.  ( -u B (,) -u a )  |->  -u ( ( RR  _D  G ) `  -u x
) ) )
209208eleq2d 2350 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( 0  e. 
ran  ( RR  _D  ( x  e.  ( -u B (,) -u a
)  |->  ( G `  -u x ) ) )  <->  0  e.  ran  (
x  e.  ( -u B (,) -u a )  |->  -u ( ( RR  _D  G ) `  -u x
) ) ) )
210162, 161elrnmpti 4930 . . . . . . . . . . 11  |-  ( 0  e.  ran  ( x  e.  ( -u B (,) -u a )  |->  -u ( ( RR  _D  G ) `  -u x
) )  <->  E. x  e.  ( -u B (,) -u a ) 0  = 
-u ( ( RR 
_D  G ) `  -u x ) )
211 eqcom 2285 . . . . . . . . . . . . 13  |-  ( 0  =  -u ( ( RR 
_D  G ) `  -u x )  <->  -u ( ( RR  _D  G ) `
 -u x )  =  0 )
212154negeq0d 9149 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( ( RR 
_D  G ) `  -u x )  =  0  <->  -u ( ( RR  _D  G ) `  -u x
)  =  0 ) )
213 ffn 5389 . . . . . . . . . . . . . . . . 17  |-  ( ( RR  _D  G ) : ( A (,) B ) --> CC  ->  ( RR  _D  G )  Fn  ( A (,) B ) )
214153, 213syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( RR  _D  G
)  Fn  ( A (,) B ) )
215 fnfvelrn 5662 . . . . . . . . . . . . . . . 16  |-  ( ( ( RR  _D  G
)  Fn  ( A (,) B )  /\  -u x  e.  ( A (,) B ) )  ->  ( ( RR 
_D  G ) `  -u x )  e.  ran  ( RR  _D  G
) )
216214, 43, 215syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( RR  _D  G ) `  -u x
)  e.  ran  ( RR  _D  G ) )
217 eleq1 2343 . . . . . . . . . . . . . . 15  |-  ( ( ( RR  _D  G
) `  -u x )  =  0  ->  (
( ( RR  _D  G ) `  -u x
)  e.  ran  ( RR  _D  G )  <->  0  e.  ran  ( RR  _D  G
) ) )
218216, 217syl5ibcom 211 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( ( RR 
_D  G ) `  -u x )  =  0  ->  0  e.  ran  ( RR  _D  G
) ) )
219212, 218sylbird 226 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( -u ( ( RR 
_D  G ) `  -u x )  =  0  ->  0  e.  ran  ( RR  _D  G
) ) )
220211, 219syl5bi 208 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( 0  =  -u ( ( RR  _D  G ) `  -u x
)  ->  0  e.  ran  ( RR  _D  G
) ) )
221220rexlimdva 2667 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( E. x  e.  ( -u B (,) -u a ) 0  = 
-u ( ( RR 
_D  G ) `  -u x )  ->  0  e.  ran  ( RR  _D  G ) ) )
222210, 221syl5bi 208 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( 0  e. 
ran  ( x  e.  ( -u B (,) -u a )  |->  -u (
( RR  _D  G
) `  -u x ) )  ->  0  e.  ran  ( RR  _D  G
) ) )
223209, 222sylbid 206 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( 0  e. 
ran  ( RR  _D  ( x  e.  ( -u B (,) -u a
)  |->  ( G `  -u x ) ) )  ->  0  e.  ran  ( RR  _D  G
) ) )
224207, 223mtod 168 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -.  0  e.  ran  ( RR  _D  (
x  e.  ( -u B (,) -u a )  |->  ( G `  -u x
) ) ) )
225119ffvelrnda 5665 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  (
( RR  _D  F
) `  z )  e.  CC )
226147ffvelrnda 5665 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  (
( RR  _D  G
) `  z )  e.  CC )
227206ad2antrr 706 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  -.  0  e.  ran  ( RR 
_D  G ) )
228147, 213syl 15 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  G )  Fn  ( A (,) B ) )
229 fnfvelrn 5662 . . . . . . . . . . . . . . 15  |-  ( ( ( RR  _D  G
)  Fn  ( A (,) B )  /\  z  e.  ( A (,) B ) )  -> 
( ( RR  _D  G ) `  z
)  e.  ran  ( RR  _D  G ) )
230228, 229sylan 457 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  (
( RR  _D  G
) `  z )  e.  ran  ( RR  _D  G ) )
231 eleq1 2343 . . . . . . . . . . . . . 14  |-  ( ( ( RR  _D  G
) `  z )  =  0  ->  (
( ( RR  _D  G ) `  z
)  e.  ran  ( RR  _D  G )  <->  0  e.  ran  ( RR  _D  G
) ) )
232230, 231syl5ibcom 211 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  (
( ( RR  _D  G ) `  z
)  =  0  -> 
0  e.  ran  ( RR  _D  G ) ) )
233232necon3bd 2483 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  ( -.  0  e.  ran  ( RR  _D  G
)  ->  ( ( RR  _D  G ) `  z )  =/=  0
) )
234227, 233mpd 14 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  (
( RR  _D  G
) `  z )  =/=  0 )
235225, 226, 234divcld 9536 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  (
( ( RR  _D  F ) `  z
)  /  ( ( RR  _D  G ) `
 z ) )  e.  CC )
236 lhop2.c . . . . . . . . . . 11  |-  ( ph  ->  C  e.  ( ( z  e.  ( A (,) B )  |->  ( ( ( RR  _D  F ) `  z
)  /  ( ( RR  _D  G ) `
 z ) ) ) lim CC  B ) )
237236adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  C  e.  ( ( z  e.  ( A (,) B ) 
|->  ( ( ( RR 
_D  F ) `  z )  /  (
( RR  _D  G
) `  z )
) ) lim CC  B
) )
238 fveq2 5525 . . . . . . . . . . 11  |-  ( z  =  -u x  ->  (
( RR  _D  F
) `  z )  =  ( ( RR 
_D  F ) `  -u x ) )
239 fveq2 5525 . . . . . . . . . . 11  |-  ( z  =  -u x  ->  (
( RR  _D  G
) `  z )  =  ( ( RR 
_D  G ) `  -u x ) )
240238, 239oveq12d 5876 . . . . . . . . . 10  |-  ( z  =  -u x  ->  (
( ( RR  _D  F ) `  z
)  /  ( ( RR  _D  G ) `
 z ) )  =  ( ( ( RR  _D  F ) `
 -u x )  / 
( ( RR  _D  G ) `  -u x
) ) )
241189pm2.21d 98 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( -u x  =  B  ->  ( ( ( RR  _D  F ) `
 -u x )  / 
( ( RR  _D  G ) `  -u x
) )  =  C ) )
242241impr 602 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  ( x  e.  ( -u B (,) -u a )  /\  -u x  =  B ) )  ->  ( (
( RR  _D  F
) `  -u x )  /  ( ( RR 
_D  G ) `  -u x ) )  =  C )
243165, 235, 179, 237, 240, 242limcco 19243 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  C  e.  ( ( x  e.  (
-u B (,) -u a
)  |->  ( ( ( RR  _D  F ) `
 -u x )  / 
( ( RR  _D  G ) `  -u x
) ) ) lim CC  -u B ) )
244 nfcv 2419 . . . . . . . . . . . . . . 15  |-  F/_ x RR
245 nfcv 2419 . . . . . . . . . . . . . . 15  |-  F/_ x  _D
246 nfmpt1 4109 . . . . . . . . . . . . . . 15  |-  F/_ x
( x  e.  (
-u B (,) -u a
)  |->  ( F `  -u x ) )
247244, 245, 246nfov 5881 . . . . . . . . . . . . . 14  |-  F/_ x
( RR  _D  (
x  e.  ( -u B (,) -u a )  |->  ( F `  -u x
) ) )
248 nfcv 2419 . . . . . . . . . . . . . 14  |-  F/_ x
y
249247, 248nffv 5532 . . . . . . . . . . . . 13  |-  F/_ x
( ( RR  _D  ( x  e.  ( -u B (,) -u a
)  |->  ( F `  -u x ) ) ) `
 y )
250 nfcv 2419 . . . . . . . . . . . . 13  |-  F/_ x  /
251 nfmpt1 4109 . . . . . . . . . . . . . . 15  |-  F/_ x
( x  e.  (
-u B (,) -u a
)  |->  ( G `  -u x ) )
252244, 245, 251nfov 5881 . . . . . . . . . . . . . 14  |-  F/_ x
( RR  _D  (
x  e.  ( -u B (,) -u a )  |->  ( G `  -u x
) ) )
253252, 248nffv 5532 . . . . . . . . . . . . 13  |-  F/_ x
( ( RR  _D  ( x  e.  ( -u B (,) -u a
)  |->  ( G `  -u x ) ) ) `
 y )
254249, 250, 253nfov 5881 . . . . . . . . . . . 12  |-  F/_ x
( ( ( RR 
_D  ( x  e.  ( -u B (,) -u a )  |->  ( F `
 -u x ) ) ) `  y )  /  ( ( RR 
_D  ( x  e.  ( -u B (,) -u a )  |->  ( G `
 -u x ) ) ) `  y ) )
255 nfcv 2419 . . . . . . . . . . . 12  |-  F/_ y
( ( ( RR 
_D  ( x  e.  ( -u B (,) -u a )  |->  ( F `
 -u x ) ) ) `  x )  /  ( ( RR 
_D  ( x  e.  ( -u B (,) -u a )  |->  ( G `
 -u x ) ) ) `  x ) )
256 fveq2 5525 . . . . . . . . . . . . 13  |-  ( y  =  x  ->  (
( RR  _D  (
x  e.  ( -u B (,) -u a )  |->  ( F `  -u x
) ) ) `  y )  =  ( ( RR  _D  (
x  e.  ( -u B (,) -u a )  |->  ( F `  -u x
) ) ) `  x ) )
257 fveq2 5525 . . . . . . . . . . . . 13  |-  ( y  =  x  ->  (
( RR  _D  (
x  e.  ( -u B (,) -u a )  |->  ( G `  -u x
) ) ) `  y )  =  ( ( RR  _D  (
x  e.  ( -u B (,) -u a )  |->  ( G `  -u x
) ) ) `  x ) )
258256, 257oveq12d 5876 . . . . . . . . . . . 12  |-  ( y  =  x  ->  (
( ( RR  _D  ( x  e.  ( -u B (,) -u a
)  |->  ( F `  -u x ) ) ) `
 y )  / 
( ( RR  _D  ( x  e.  ( -u B (,) -u a
)  |->  ( G `  -u x ) ) ) `
 y ) )  =  ( ( ( RR  _D  ( x  e.  ( -u B (,) -u a )  |->  ( F `  -u x
) ) ) `  x )  /  (
( RR  _D  (
x  e.  ( -u B (,) -u a )  |->  ( G `  -u x
) ) ) `  x ) ) )
259254, 255, 258cbvmpt 4110 . . . . . . . . . . 11  |-  ( y  e.  ( -u B (,) -u a )  |->  ( ( ( RR  _D  ( x  e.  ( -u B (,) -u a
)  |->  ( F `  -u x ) ) ) `
 y )  / 
( ( RR  _D  ( x  e.  ( -u B (,) -u a
)  |->  ( G `  -u x ) ) ) `
 y ) ) )  =  ( x  e.  ( -u B (,) -u a )  |->  ( ( ( RR  _D  ( x  e.  ( -u B (,) -u a
)  |->  ( F `  -u x ) ) ) `
 x )  / 
( ( RR  _D  ( x  e.  ( -u B (,) -u a
)  |->  ( G `  -u x ) ) ) `
 x ) ) )
260131fveq1d 5527 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( ( RR 
_D  ( x  e.  ( -u B (,) -u a )  |->  ( F `
 -u x ) ) ) `  x )  =  ( ( x  e.  ( -u B (,) -u a )  |->  -u ( ( RR  _D  F ) `  -u x
) ) `  x
) )
261134fvmpt2 5608 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  ( -u B (,) -u a )  /\  -u ( ( RR  _D  F ) `  -u x
)  e.  _V )  ->  ( ( x  e.  ( -u B (,) -u a )  |->  -u (
( RR  _D  F
) `  -u x ) ) `  x )  =  -u ( ( RR 
_D  F ) `  -u x ) )
262133, 261mpan2 652 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( -u B (,) -u a )  -> 
( ( x  e.  ( -u B (,) -u a )  |->  -u (
( RR  _D  F
) `  -u x ) ) `  x )  =  -u ( ( RR 
_D  F ) `  -u x ) )
263260, 262sylan9eq 2335 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( RR  _D  ( x  e.  ( -u B (,) -u a
)  |->  ( F `  -u x ) ) ) `
 x )  = 
-u ( ( RR 
_D  F ) `  -u x ) )
264159fveq1d 5527 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( ( RR 
_D  ( x  e.  ( -u B (,) -u a )  |->  ( G `
 -u x ) ) ) `  x )  =  ( ( x  e.  ( -u B (,) -u a )  |->  -u ( ( RR  _D  G ) `  -u x
) ) `  x
) )
265162fvmpt2 5608 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  ( -u B (,) -u a )  /\  -u ( ( RR  _D  G ) `  -u x
)  e.  _V )  ->  ( ( x  e.  ( -u B (,) -u a )  |->  -u (
( RR  _D  G
) `  -u x ) ) `  x )  =  -u ( ( RR 
_D  G ) `  -u x ) )
266161, 265mpan2 652 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( -u B (,) -u a )  -> 
( ( x  e.  ( -u B (,) -u a )  |->  -u (
( RR  _D  G
) `  -u x ) ) `  x )  =  -u ( ( RR 
_D  G ) `  -u x ) )
267264, 266sylan9eq 2335 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( RR  _D  ( x  e.  ( -u B (,) -u a
)  |->  ( G `  -u x ) ) ) `
 x )  = 
-u ( ( RR 
_D  G ) `  -u x ) )
268263, 267oveq12d 5876 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( ( RR 
_D  ( x  e.  ( -u B (,) -u a )  |->  ( F `
 -u x ) ) ) `  x )  /  ( ( RR 
_D  ( x  e.  ( -u B (,) -u a )  |->  ( G `
 -u x ) ) ) `  x ) )  =  ( -u ( ( RR  _D  F ) `  -u x
)  /  -u (
( RR  _D  G
) `  -u x ) ) )
269206ad2antrr 706 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -.  0  e.  ran  ( RR  _D  G
) )
270218necon3bd 2483 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( -.  0  e. 
ran  ( RR  _D  G )  ->  (
( RR  _D  G
) `  -u x )  =/=  0 ) )
271269, 270mpd 14 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( RR  _D  G ) `  -u x
)  =/=  0 )
272126, 154, 271div2negd 9551 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( -u ( ( RR 
_D  F ) `  -u x )  /  -u (
( RR  _D  G
) `  -u x ) )  =  ( ( ( RR  _D  F
) `  -u x )  /  ( ( RR 
_D  G ) `  -u x ) ) )
273268, 272eqtrd 2315 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( ( RR 
_D  ( x  e.  ( -u B (,) -u a )  |->  ( F `
 -u x ) ) ) `  x )  /  ( ( RR 
_D  ( x  e.  ( -u B (,) -u a )  |->  ( G `
 -u x ) ) ) `  x ) )  =  ( ( ( RR  _D  F
) `  -u x )  /  ( ( RR 
_D  G ) `  -u x ) ) )
274273mpteq2dva 4106 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( x  e.  ( -u B (,) -u a )  |->  ( ( ( RR  _D  (
x  e.  ( -u B (,) -u a )  |->  ( F `  -u x
) ) ) `  x )  /  (
( RR  _D  (
x  e.  ( -u B (,) -u a )  |->  ( G `  -u x
) ) ) `  x ) ) )  =  ( x  e.  ( -u B (,) -u a )  |->  ( ( ( RR  _D  F
) `  -u x )  /  ( ( RR 
_D  G ) `  -u x ) ) ) )
275259, 274syl5eq 2327 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( y  e.  ( -u B (,) -u a )  |->  ( ( ( RR  _D  (
x  e.  ( -u B (,) -u a )  |->  ( F `  -u x
) ) ) `  y )  /  (
( RR  _D  (
x  e.  ( -u B (,) -u a )  |->  ( G `  -u x
) ) ) `  y ) ) )  =  ( x  e.  ( -u B (,) -u a )  |->  ( ( ( RR  _D  F
) `  -u x )  /  ( ( RR 
_D  G ) `  -u x ) ) ) )
276275oveq1d 5873 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( ( y  e.  ( -u B (,) -u a )  |->  ( ( ( RR  _D  ( x  e.  ( -u B (,) -u a
)  |->  ( F `  -u x ) ) ) `
 y )  / 
( ( RR  _D  ( x  e.  ( -u B (,) -u a
)  |->  ( G `  -u x ) ) ) `
 y ) ) ) lim CC  -u B
)  =  ( ( x  e.  ( -u B (,) -u a )  |->  ( ( ( RR  _D  F ) `  -u x
)  /  ( ( RR  _D  G ) `
 -u x ) ) ) lim CC  -u B
) )
277243, 276eleqtrrd 2360 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  C  e.  ( ( y  e.  (
-u B (,) -u a
)  |->  ( ( ( RR  _D  ( x  e.  ( -u B (,) -u a )  |->  ( F `  -u x
) ) ) `  y )  /  (
( RR  _D  (
x  e.  ( -u B (,) -u a )  |->  ( G `  -u x
) ) ) `  y ) ) ) lim
CC  -u B ) )
27879, 81, 84, 86, 88, 136, 164, 192, 199, 205, 224, 277lhop1 19361 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  C  e.  ( ( y  e.  (
-u B (,) -u a
)  |->  ( ( ( x  e.  ( -u B (,) -u a )  |->  ( F `  -u x
) ) `  y
)  /  ( ( x  e.  ( -u B (,) -u a )  |->  ( G `  -u x
) ) `  y
) ) ) lim CC  -u B ) )
279 nffvmpt1 5533 . . . . . . . . . . 11  |-  F/_ x
( ( x  e.  ( -u B (,) -u a )  |->  ( F `
 -u x ) ) `
 y )
280 nffvmpt1 5533 . . . . . . . . . . 11  |-  F/_ x
( ( x  e.  ( -u B (,) -u a )  |->  ( G `
 -u x ) ) `
 y )
281279, 250, 280nfov 5881 . . . . . . . . . 10  |-  F/_ x
( ( ( x  e.  ( -u B (,) -u a )  |->  ( F `  -u x
) ) `  y
)  /  ( ( x  e.  ( -u B (,) -u a )  |->  ( G `  -u x
) ) `  y
) )
282 nfcv 2419 . . . . . . . . . 10  |-  F/_ y
( ( ( x  e.  ( -u B (,) -u a )  |->  ( F `  -u x
) ) `  x
)  /  ( ( x  e.  ( -u B (,) -u a )  |->  ( G `  -u x
) ) `  x
) )
283 fveq2 5525 . . . . . . . . . . 11  |-  ( y  =  x  ->  (
( x  e.  (
-u B (,) -u a
)  |->  ( F `  -u x ) ) `  y )  =  ( ( x  e.  (
-u B (,) -u a
)  |->  ( F `  -u x ) ) `  x ) )
284 fveq2 5525 . . . . . . . . . . 11  |-  ( y  =  x  ->  (
( x  e.  (
-u B (,) -u a
)  |->  ( G `  -u x ) ) `  y )  =  ( ( x  e.  (
-u B (,) -u a
)  |->  ( G `  -u x ) ) `  x ) )
285283, 284oveq12d 5876 . . . . . . . . . 10  |-  ( y  =  x  ->  (
( ( x  e.  ( -u B (,) -u a )  |->  ( F `
 -u x ) ) `
 y )  / 
( ( x  e.  ( -u B (,) -u a )  |->  ( G `
 -u x ) ) `
 y ) )  =  ( ( ( x  e.  ( -u B (,) -u a )  |->  ( F `  -u x
) ) `  x
)  /  ( ( x  e.  ( -u B (,) -u a )  |->  ( G `  -u x
) ) `  x
) ) )
286281, 282, 285cbvmpt 4110 . . . . . . . . 9  |-  ( y  e.  ( -u B (,) -u a )  |->  ( ( ( x  e.  ( -u B (,) -u a )  |->  ( F `
 -u x ) ) `
 y )  / 
( ( x  e.  ( -u B (,) -u a )  |->  ( G `
 -u x ) ) `
 y ) ) )  =  ( x  e.  ( -u B (,) -u a )  |->  ( ( ( x  e.  ( -u B (,) -u a )  |->  ( F `
 -u x ) ) `
 x )  / 
( ( x  e.  ( -u B (,) -u a )  |->  ( G `
 -u x ) ) `
 x ) ) )
287 fvex 5539 . . . . . . . . . . . 12  |-  ( F `
 -u x )  e. 
_V
28885fvmpt2 5608 . . . . . . . . . . . 12  |-  ( ( x  e.  ( -u B (,) -u a )  /\  ( F `  -u x
)  e.  _V )  ->  ( ( x  e.  ( -u B (,) -u a )  |->  ( F `
 -u x ) ) `
 x )  =  ( F `  -u x
) )
28926, 287, 288sylancl 643 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( x  e.  ( -u B (,) -u a )  |->  ( F `
 -u x ) ) `
 x )  =  ( F `  -u x
) )
290 fvex 5539 . . . . . . . . . . . 12  |-  ( G `
 -u x )  e. 
_V
29187fvmpt2 5608 . . . . . . . . . . . 12  |-  ( ( x  e.  ( -u B (,) -u a )  /\  ( G `  -u x
)  e.  _V )  ->  ( ( x  e.  ( -u B (,) -u a )  |->  ( G `
 -u x ) ) `
 x )  =  ( G `  -u x
) )
29226, 290, 291sylancl 643 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( x  e.  ( -u B (,) -u a )  |->  ( G `
 -u x ) ) `
 x )  =  ( G `  -u x
) )
293289, 292oveq12d 5876 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( ( x  e.  ( -u B (,) -u a )  |->  ( F `  -u x
) ) `  x
)  /  ( ( x  e.  ( -u B (,) -u a )  |->  ( G `  -u x
) ) `  x
) )  =  ( ( F `  -u x
)  /  ( G `
 -u x ) ) )
294293mpteq2dva 4106 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( x  e.  ( -u B (,) -u a )  |->  ( ( ( x  e.  (
-u B (,) -u a
)  |->  ( F `  -u x ) ) `  x )  /  (
( x  e.  (
-u B (,) -u a
)  |->  ( G `  -u x ) ) `  x ) ) )  =  ( x  e.  ( -u B (,) -u a )  |->  ( ( F `  -u x
)  /  ( G `
 -u x ) ) ) )
295286, 294syl5eq 2327 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( y  e.  ( -u B (,) -u a )  |->  ( ( ( x  e.  (
-u B (,) -u a
)  |->  ( F `  -u x ) ) `  y )  /  (
( x  e.  (
-u B (,) -u a
)  |->  ( G `  -u x ) ) `  y ) ) )  =  ( x  e.  ( -u B (,) -u a )  |->  ( ( F `  -u x
)  /  ( G `
 -u x ) ) ) )
296295oveq1d 5873 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( ( y  e.  ( -u B (,) -u a )  |->  ( ( ( x  e.  ( -u B (,) -u a )  |->  ( F `
 -u x ) ) `
 y )  / 
( ( x  e.  ( -u B (,) -u a )  |->  ( G `
 -u x ) ) `
 y ) ) ) lim CC  -u B
)  =  ( ( x  e.  ( -u B (,) -u a )  |->  ( ( F `  -u x
)  /  ( G `
 -u x ) ) ) lim CC  -u B
) )
297278, 296eleqtrd 2359 . . . . . 6  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  C  e.  ( ( x  e.  (
-u B (,) -u a
)  |->  ( ( F `
 -u x )  / 
( G `  -u x
) ) ) lim CC  -u B ) )
298 negeq 9044 . . . . . . . 8  |-  ( x  =  -u z  ->  -u x  =  -u -u z )
299298fveq2d 5529 . . . . . . 7  |-  ( x  =  -u z  ->  ( F `  -u x )  =  ( F `  -u -u z ) )
300298fveq2d 5529 . . . . . . 7  |-  ( x  =  -u z  ->  ( G `  -u x )  =  ( G `  -u -u z ) )
301299, 300oveq12d 5876 . . . . . 6  |-  ( x  =  -u z  ->  (
( F `  -u x
)  /  ( G `
 -u x ) )  =  ( ( F `
 -u -u z )  / 
( G `  -u -u z
) ) )
30279adantr 451 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  -u B  e.  RR )
303 eliooord 10710 . . . . . . . . . . . . 13  |-  ( z  e.  ( a (,) B )  ->  (
a  <  z  /\  z  <  B ) )
304303adantl 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  (
a  <  z  /\  z  <  B ) )
305304simprd 449 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  z  <  B )
30615, 13ltnegd 9350 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  (
z  <  B  <->  -u B  <  -u z ) )
307305, 306mpbid 201 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  -u B  <  -u z )
308302, 307gtned 8954 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  -u z  =/=  -u B )
309308neneqd 2462 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  -.  -u z  =  -u B
)
310309pm2.21d 98 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  ( -u z  =  -u B  ->  ( ( F `  -u -u z )  /  ( G `  -u -u z
) )  =  C ) )
311310impr 602 . . . . . 6  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  ( z  e.  ( a (,) B )  /\  -u z  =  -u B ) )  ->  ( ( F `
 -u -u z )  / 
( G `  -u -u z
) )  =  C )
31219, 65, 78, 297, 301, 311limcco 19243 . . . . 5  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  C  e.  ( ( z  e.  ( a (,) B ) 
|->  ( ( F `  -u -u z )  /  ( G `  -u -u z
) ) ) lim CC  B ) )
31315recnd 8861 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  z  e.  CC )
314313negnegd 9148 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  -u -u z  =  z )
315314fveq2d 5529 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  ( F `  -u -u z
)  =  ( F `
 z ) )
316314fveq2d 5529 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  ( G `  -u -u z
)  =  ( G `
 z ) )
317315, 316oveq12d 5876 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  (
( F `  -u -u z
)  /  ( G `
 -u -u z ) )  =  ( ( F `
 z )  / 
( G `  z
) ) )
318317mpteq2dva 4106 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( z  e.  ( a (,) B
)  |->  ( ( F `
 -u -u z )  / 
( G `  -u -u z
) ) )  =  ( z  e.  ( a (,) B ) 
|->  ( ( F `  z )  /  ( G `  z )
) ) )
319318oveq1d 5873 . . . . . 6  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( ( z  e.  ( a (,) B )  |->  ( ( F `  -u -u z
)  /  ( G `
 -u -u z ) ) ) lim CC  B )  =  ( ( z  e.  ( a (,) B )  |->  ( ( F `  z )  /  ( G `  z ) ) ) lim
CC  B ) )
320 resmpt 5000 . . . . . . . 8  |-  ( ( a (,) B ) 
C_  ( A (,) B )  ->  (
( z  e.  ( A (,) B ) 
|->  ( ( F `  z )  /  ( G `  z )
) )  |`  (
a (,) B ) )  =  ( z  e.  ( a (,) B )  |->  ( ( F `  z )  /  ( G `  z ) ) ) )
32141, 320syl 15 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( ( z  e.  ( A (,) B )  |->  ( ( F `  z )  /  ( G `  z ) ) )  |`  ( a (,) B
) )  =  ( z  e.  ( a (,) B )  |->  ( ( F `  z
)  /  ( G `
 z ) ) ) )
322321oveq1d 5873 . . . . . 6  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( ( ( z  e.  ( A (,) B )  |->  ( ( F `  z
)  /  ( G `
 z ) ) )  |`  ( a (,) B ) ) lim CC  B )  =  ( ( z  e.  ( a (,) B ) 
|->  ( ( F `  z )  /  ( G `  z )
) ) lim CC  B
) )
323 fss 5397 . . . . . . . . . . 11  |-  ( ( F : ( A (,) B ) --> RR 
/\  RR  C_  CC )  ->  F : ( A (,) B ) --> CC )
32494, 53, 323sylancl 643 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  F : ( A (,) B ) --> CC )
325324ffvelrnda 5665 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  ( F `  z )  e.  CC )
32655ffvelrnda 5665 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  ( G `  z )  e.  CC )
32750ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  -.  0  e.  ran  G )
32855, 57syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  G  Fn  ( A (,) B ) )
329 fnfvelrn 5662 . . . . . . . . . . . . 13  |-  ( ( G  Fn  ( A (,) B )  /\  z  e.  ( A (,) B ) )  -> 
( G `  z
)  e.  ran  G
)
330328, 329sylan 457 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  ( G `  z )  e.  ran  G )
331 eleq1 2343 . . . . . . . . . . . 12  |-  ( ( G `  z )  =  0  ->  (
( G `  z
)  e.  ran  G  <->  0  e.  ran  G ) )
332330, 331syl5ibcom 211 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  (
( G `  z
)  =  0  -> 
0  e.  ran  G
) )
333332necon3bd 2483 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  ( -.  0  e.  ran  G  ->  ( G `  z )  =/=  0
) )
334327, 333mpd 14 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  ( G `  z )  =/=  0 )
335325, 326, 334divcld 9536 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  (
( F `  z
)  /  ( G `
 z ) )  e.  CC )
336 eqid 2283 . . . . . . . 8  |-  ( z  e.  ( A (,) B )  |->  ( ( F `  z )  /  ( G `  z ) ) )  =  ( z  e.  ( A (,) B
)  |->  ( ( F `
 z )  / 
( G `  z
) ) )
337335, 336fmptd 5684 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( z  e.  ( A (,) B
)  |->  ( ( F `
 z )  / 
( G `  z
) ) ) : ( A (,) B
) --> CC )
338 ioossre 10712 . . . . . . . . 9  |-  ( A (,) B )  C_  RR
339338, 53sstri 3188 . . . . . . . 8  |-  ( A (,) B )  C_  CC
340339a1i 10 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( A (,) B )  C_  CC )
341 eqid 2283 . . . . . . 7  |-  ( (
TopOpen ` fld )t  ( ( A (,) B )  u.  { B } ) )  =  ( ( TopOpen ` fld )t  ( ( A (,) B )  u. 
{ B } ) )
342 ssun2 3339 . . . . . . . . 9  |-  { B }  C_  ( ( a (,) B )  u. 
{ B } )
343 snssg 3754 . . . . . . . . . 10  |-  ( B  e.  RR  ->  ( B  e.  ( (
a (,) B )  u.  { B }
)  <->  { B }  C_  ( ( a (,) B )  u.  { B } ) ) )
34475, 343syl 15 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( B  e.  ( ( a (,) B )  u.  { B } )  <->  { B }  C_  ( ( a (,) B )  u. 
{ B } ) ) )
345342, 344mpbiri 224 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  B  e.  ( ( a (,) B
)  u.  { B } ) )
346107cnfldtopon 18292 . . . . . . . . . . 11  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
347338a1i 10 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( A (,) B )  C_  RR )
34875snssd 3760 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  { B }  C_  RR )
349347, 348unssd 3351 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( ( A (,) B )  u. 
{ B } ) 
C_  RR )
350349, 53syl6ss 3191 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( ( A (,) B )  u. 
{ B } ) 
C_  CC )
351 resttopon 16892 . . . . . . . . . . 11  |-  ( ( ( TopOpen ` fld )  e.  (TopOn `  CC )  /\  (
( A (,) B
)  u.  { B } )  C_  CC )  ->  ( ( TopOpen ` fld )t  (
( A (,) B
)  u.  { B } ) )  e.  (TopOn `  ( ( A (,) B )  u. 
{ B } ) ) )
352346, 350, 351sylancr 644 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( ( TopOpen ` fld )t  (
( A (,) B
)  u.  { B } ) )  e.  (TopOn `  ( ( A (,) B )  u. 
{ B } ) ) )
353 topontop 16664 . . . . . . . . . 10  |-  ( ( ( TopOpen ` fld )t  ( ( A (,) B )  u. 
{ B } ) )  e.  (TopOn `  ( ( A (,) B )  u.  { B } ) )  -> 
( ( TopOpen ` fld )t  ( ( A (,) B )  u. 
{ B } ) )  e.  Top )
354352, 353syl 15 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( ( TopOpen ` fld )t  (
( A (,) B
)  u.  { B } ) )  e. 
Top )
355 indi 3415 . . . . . . . . . . . 12  |-  ( ( a (,)  +oo )  i^i  ( ( A (,) B )  u.  { B } ) )  =  ( ( ( a (,)  +oo )  i^i  ( A (,) B ) )  u.  ( ( a (,)  +oo )  i^i  { B } ) )
356 pnfxr 10455 . . . . . . . . . . . . . . . 16  |-  +oo  e.  RR*
357356a1i 10 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  +oo  e.  RR* )
3584adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  B  e.  RR* )
359 iooin 10690 . . . . . . . . . . . . . . 15  |-  ( ( ( a  e.  RR*  /\ 
+oo  e.  RR* )  /\  ( A  e.  RR*  /\  B  e.  RR* ) )  -> 
( ( a (,) 
+oo )  i^i  ( A (,) B ) )  =  ( if ( a  <_  A ,  A ,  a ) (,) if (  +oo  <_  B ,  +oo ,  B
) ) )
36036, 357, 34, 358, 359syl22anc 1183 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( ( a (,)  +oo )  i^i  ( A (,) B ) )  =  ( if ( a  <_  A ,  A ,  a ) (,) if (  +oo  <_  B ,  +oo ,  B
) ) )
361 xrltnle 8891 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  RR*  /\  a  e.  RR* )  ->  ( A  <  a  <->  -.  a  <_  A ) )
36234, 36, 361syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( A  < 
a  <->  -.  a  <_  A ) )
36335, 362mpbid 201 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -.  a  <_  A )
364 iffalse 3572 . . . . . . . . . . . . . . . 16  |-  ( -.  a  <_  A  ->  if ( a  <_  A ,  A ,  a )  =  a )
365363, 364syl 15 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  if ( a  <_  A ,  A ,  a )  =  a