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

Theorem lhop2 19852
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 10540 . . 3  |-  QQ  C_  RR
2 lhop2.a . . . 4  |-  ( ph  ->  A  e.  RR* )
3 lhop2.b . . . . 5  |-  ( ph  ->  B  e.  RR )
43rexrd 9090 . . . 4  |-  ( ph  ->  B  e.  RR* )
5 lhop2.l . . . 4  |-  ( ph  ->  A  <  B )
6 qbtwnxr 10742 . . . 4  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  A  < 
B )  ->  E. a  e.  QQ  ( A  < 
a  /\  a  <  B ) )
72, 4, 5, 6syl3anc 1184 . . 3  |-  ( ph  ->  E. a  e.  QQ  ( A  <  a  /\  a  <  B ) )
8 ssrexv 3368 . . 3  |-  ( QQ  C_  RR  ->  ( E. a  e.  QQ  ( A  <  a  /\  a  <  B )  ->  E. a  e.  RR  ( A  < 
a  /\  a  <  B ) ) )
91, 7, 8mpsyl 61 . 2  |-  ( ph  ->  E. a  e.  RR  ( A  <  a  /\  a  <  B ) )
10 simpr 448 . . . . . 6  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  z  e.  ( a (,) B
) )
11 simprl 733 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  a  e.  RR )
1211adantr 452 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  a  e.  RR )
133ad2antrr 707 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  B  e.  RR )
14 elioore 10902 . . . . . . . 8  |-  ( z  e.  ( a (,) B )  ->  z  e.  RR )
1514adantl 453 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  z  e.  RR )
16 iooneg 10973 . . . . . . 7  |-  ( ( a  e.  RR  /\  B  e.  RR  /\  z  e.  RR )  ->  (
z  e.  ( a (,) B )  <->  -u z  e.  ( -u B (,) -u a ) ) )
1712, 13, 15, 16syl3anc 1184 . . . . . 6  |-  ( ( ( 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 202 . . . . 5  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  -u z  e.  ( -u B (,) -u a ) )
1918adantrr 698 . . . 4  |-  ( ( ( 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 . . . . . . . 8  |-  ( ph  ->  F : ( A (,) B ) --> RR )
2120ad2antrr 707 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  F : ( A (,) B ) --> RR )
22 elioore 10902 . . . . . . . . . . . . 13  |-  ( x  e.  ( -u B (,) -u a )  ->  x  e.  RR )
2322adantl 453 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  x  e.  RR )
2423recnd 9070 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  x  e.  CC )
2524negnegd 9358 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -u -u x  =  x
)
26 simpr 448 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  x  e.  ( -u B (,) -u a ) )
2725, 26eqeltrd 2478 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -u -u x  e.  ( -u B (,) -u a
) )
2811adantr 452 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
a  e.  RR )
293ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  B  e.  RR )
3023renegcld 9420 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -u x  e.  RR )
31 iooneg 10973 . . . . . . . . . 10  |-  ( ( 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 1184 . . . . . . . . 9  |-  ( ( ( 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 224 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -u x  e.  ( a (,) B ) )
342adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  A  e.  RR* )
35 simprrl 741 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  A  <  a
)
3611rexrd 9090 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  a  e.  RR* )
37 xrltle 10698 . . . . . . . . . . . 12  |-  ( ( A  e.  RR*  /\  a  e.  RR* )  ->  ( A  <  a  ->  A  <_  a ) )
3834, 36, 37syl2anc 643 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( A  < 
a  ->  A  <_  a ) )
3935, 38mpd 15 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  A  <_  a
)
40 iooss1 10907 . . . . . . . . . 10  |-  ( ( A  e.  RR*  /\  A  <_  a )  ->  (
a (,) B ) 
C_  ( A (,) B ) )
4134, 39, 40syl2anc 643 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( a (,) B )  C_  ( A (,) B ) )
4241sselda 3308 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  -u x  e.  ( a (,) B
) )  ->  -u x  e.  ( A (,) B
) )
4333, 42syldan 457 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -u x  e.  ( A (,) B ) )
4421, 43ffvelrnd 5830 . . . . . 6  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( F `  -u x
)  e.  RR )
4544recnd 9070 . . . . 5  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( F `  -u x
)  e.  CC )
46 lhop2.g . . . . . . . 8  |-  ( ph  ->  G : ( A (,) B ) --> RR )
4746ad2antrr 707 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  G : ( A (,) B ) --> RR )
4847, 43ffvelrnd 5830 . . . . . 6  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( G `  -u x
)  e.  RR )
4948recnd 9070 . . . . 5  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( G `  -u x
)  e.  CC )
50 lhop2.gn0 . . . . . . 7  |-  ( ph  ->  -.  0  e.  ran  G )
5150ad2antrr 707 . . . . . 6  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -.  0  e.  ran  G )
5246adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  G : ( A (,) B ) --> RR )
53 ax-resscn 9003 . . . . . . . . . . . 12  |-  RR  C_  CC
54 fss 5558 . . . . . . . . . . . 12  |-  ( ( G : ( A (,) B ) --> RR 
/\  RR  C_  CC )  ->  G : ( A (,) B ) --> CC )
5552, 53, 54sylancl 644 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  G : ( A (,) B ) --> CC )
5655adantr 452 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  G : ( A (,) B ) --> CC )
57 ffn 5550 . . . . . . . . . 10  |-  ( G : ( A (,) B ) --> CC  ->  G  Fn  ( A (,) B ) )
5856, 57syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  G  Fn  ( A (,) B ) )
59 fnfvelrn 5826 . . . . . . . . 9  |-  ( ( G  Fn  ( A (,) B )  /\  -u x  e.  ( A (,) B ) )  ->  ( G `  -u x )  e.  ran  G )
6058, 43, 59syl2anc 643 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( G `  -u x
)  e.  ran  G
)
61 eleq1 2464 . . . . . . . 8  |-  ( ( G `  -u x
)  =  0  -> 
( ( G `  -u x )  e.  ran  G  <->  0  e.  ran  G
) )
6260, 61syl5ibcom 212 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( G `  -u x )  =  0  ->  0  e.  ran  G ) )
6362necon3bd 2604 . . . . . 6  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( -.  0  e. 
ran  G  ->  ( G `
 -u x )  =/=  0 ) )
6451, 63mpd 15 . . . . 5  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( G `  -u x
)  =/=  0 )
6545, 49, 64divcld 9746 . . . 4  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( F `  -u x )  /  ( G `  -u x ) )  e.  CC )
66 limcresi 19725 . . . . . 6  |-  ( ( z  e.  RR  |->  -u z ) lim CC  B ) 
C_  ( ( ( z  e.  RR  |->  -u z )  |`  (
a (,) B ) ) lim CC  B )
67 ioossre 10928 . . . . . . . 8  |-  ( a (,) B )  C_  RR
68 resmpt 5150 . . . . . . . 8  |-  ( ( a (,) B ) 
C_  RR  ->  ( ( z  e.  RR  |->  -u z )  |`  (
a (,) B ) )  =  ( z  e.  ( a (,) B )  |->  -u z
) )
6967, 68ax-mp 8 . . . . . . 7  |-  ( ( z  e.  RR  |->  -u z )  |`  (
a (,) B ) )  =  ( z  e.  ( a (,) B )  |->  -u z
)
7069oveq1i 6050 . . . . . 6  |-  ( ( ( z  e.  RR  |->  -u z )  |`  (
a (,) B ) ) lim CC  B )  =  ( ( z  e.  ( a (,) B )  |->  -u z
) lim CC  B )
7166, 70sseqtri 3340 . . . . 5  |-  ( ( z  e.  RR  |->  -u z ) lim CC  B ) 
C_  ( ( z  e.  ( a (,) B )  |->  -u z
) lim CC  B )
72 eqid 2404 . . . . . . . 8  |-  ( z  e.  RR  |->  -u z
)  =  ( z  e.  RR  |->  -u z
)
7372negcncf 18901 . . . . . . 7  |-  ( RR  C_  CC  ->  ( z  e.  RR  |->  -u z )  e.  ( RR -cn-> CC ) )
7453, 73mp1i 12 . . . . . 6  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( z  e.  RR  |->  -u z )  e.  ( RR -cn-> CC ) )
753adantr 452 . . . . . 6  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  B  e.  RR )
76 negeq 9254 . . . . . 6  |-  ( z  =  B  ->  -u z  =  -u B )
7774, 75, 76cnmptlimc 19730 . . . . 5  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -u B  e.  ( ( z  e.  RR  |->  -u z ) lim CC  B
) )
7871, 77sseldi 3306 . . . 4  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -u B  e.  ( ( z  e.  ( a (,) B ) 
|->  -u z ) lim CC  B ) )
7975renegcld 9420 . . . . . 6  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -u B  e.  RR )
8011renegcld 9420 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -u a  e.  RR )
8180rexrd 9090 . . . . . 6  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -u a  e.  RR* )
82 simprrr 742 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  a  <  B
)
8311, 75ltnegd 9560 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( a  < 
B  <->  -u B  <  -u a
) )
8482, 83mpbid 202 . . . . . 6  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -u B  <  -u a
)
85 eqid 2404 . . . . . . 7  |-  ( x  e.  ( -u B (,) -u a )  |->  ( F `  -u x
) )  =  ( x  e.  ( -u B (,) -u a )  |->  ( F `  -u x
) )
8644, 85fmptd 5852 . . . . . 6  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( x  e.  ( -u B (,) -u a )  |->  ( F `
 -u x ) ) : ( -u B (,) -u a ) --> RR )
87 eqid 2404 . . . . . . 7  |-  ( x  e.  ( -u B (,) -u a )  |->  ( G `  -u x
) )  =  ( x  e.  ( -u B (,) -u a )  |->  ( G `  -u x
) )
8848, 87fmptd 5852 . . . . . 6  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( x  e.  ( -u B (,) -u a )  |->  ( G `
 -u x ) ) : ( -u B (,) -u a ) --> RR )
89 reex 9037 . . . . . . . . . . . 12  |-  RR  e.  _V
9089prid1 3872 . . . . . . . . . . 11  |-  RR  e.  { RR ,  CC }
9190a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  RR  e.  { RR ,  CC } )
92 neg1cn 10023 . . . . . . . . . . 11  |-  -u 1  e.  CC
9392a1i 11 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -u 1  e.  CC )
9420adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  F : ( A (,) B ) --> RR )
9594ffvelrnda 5829 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  y  e.  ( A (,) B
) )  ->  ( F `  y )  e.  RR )
9695recnd 9070 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  y  e.  ( A (,) B
) )  ->  ( F `  y )  e.  CC )
97 fvex 5701 . . . . . . . . . . 11  |-  ( ( RR  _D  F ) `
 y )  e. 
_V
9897a1i 11 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  y  e.  ( A (,) B
) )  ->  (
( RR  _D  F
) `  y )  e.  _V )
99 ax-1cn 9004 . . . . . . . . . . . 12  |-  1  e.  CC
10099a1i 11 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
1  e.  CC )
101 simpr 448 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  RR )  ->  x  e.  RR )
102101recnd 9070 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  RR )  ->  x  e.  CC )
10399a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  RR )  ->  1  e.  CC )
10491dvmptid 19796 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  ( x  e.  RR  |->  x ) )  =  ( x  e.  RR  |->  1 ) )
105 ioossre 10928 . . . . . . . . . . . . 13  |-  ( -u B (,) -u a )  C_  RR
106105a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( -u B (,) -u a )  C_  RR )
107 eqid 2404 . . . . . . . . . . . . 13  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
108107tgioo2 18787 . . . . . . . . . . . 12  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
109 iooretop 18753 . . . . . . . . . . . . 13  |-  ( -u B (,) -u a )  e.  ( topGen `  ran  (,) )
110109a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( -u B (,) -u a )  e.  ( topGen `  ran  (,) )
)
11191, 102, 103, 104, 106, 108, 107, 110dvmptres 19802 . . . . . . . . . . 11  |-  ( (
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 19805 . . . . . . . . . 10  |-  ( (
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 5738 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  F  =  ( y  e.  ( A (,) B )  |->  ( F `  y ) ) )
114113oveq2d 6056 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  F )  =  ( RR  _D  ( y  e.  ( A (,) B )  |->  ( F `
 y ) ) ) )
115 dvf 19747 . . . . . . . . . . . . 13  |-  ( RR 
_D  F ) : dom  ( RR  _D  F ) --> CC
116 lhop2.if . . . . . . . . . . . . . . 15  |-  ( ph  ->  dom  ( RR  _D  F )  =  ( A (,) B ) )
117116adantr 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  dom  ( RR  _D  F )  =  ( A (,) B ) )
118117feq2d 5540 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( ( RR 
_D  F ) : dom  ( RR  _D  F ) --> CC  <->  ( RR  _D  F ) : ( A (,) B ) --> CC ) )
119115, 118mpbii 203 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  F ) : ( A (,) B ) --> CC )
120119feqmptd 5738 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  F )  =  ( y  e.  ( A (,) B )  |->  ( ( RR  _D  F
) `  y )
) )
121114, 120eqtr3d 2438 . . . . . . . . . 10  |-  ( (
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 5687 . . . . . . . . . 10  |-  ( y  =  -u x  ->  ( F `  y )  =  ( F `  -u x ) )
123 fveq2 5687 . . . . . . . . . 10  |-  ( y  =  -u x  ->  (
( RR  _D  F
) `  y )  =  ( ( RR 
_D  F ) `  -u x ) )
12491, 91, 43, 93, 96, 98, 112, 121, 122, 123dvmptco 19811 . . . . . . . . 9  |-  ( (
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 452 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( RR  _D  F
) : ( A (,) B ) --> CC )
126125, 43ffvelrnd 5830 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( RR  _D  F ) `  -u x
)  e.  CC )
127126, 93mulcomd 9065 . . . . . . . . . . 11  |-  ( ( ( 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 9441 . . . . . . . . . . 11  |-  ( ( ( 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 2436 . . . . . . . . . 10  |-  ( ( ( 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 4255 . . . . . . . . 9  |-  ( (
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 2436 . . . . . . . 8  |-  ( (
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 5031 . . . . . . 7  |-  ( (
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 9260 . . . . . . . 8  |-  -u (
( RR  _D  F
) `  -u x )  e.  _V
134 eqid 2404 . . . . . . . 8  |-  ( 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 5533 . . . . . . 7  |-  dom  (
x  e.  ( -u B (,) -u a )  |->  -u ( ( RR  _D  F ) `  -u x
) )  =  (
-u B (,) -u a
)
136132, 135syl6eq 2452 . . . . . 6  |-  ( (
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 5829 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  y  e.  ( A (,) B
) )  ->  ( G `  y )  e.  RR )
138137recnd 9070 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  y  e.  ( A (,) B
) )  ->  ( G `  y )  e.  CC )
139 fvex 5701 . . . . . . . . . . 11  |-  ( ( RR  _D  G ) `
 y )  e. 
_V
140139a1i 11 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  y  e.  ( A (,) B
) )  ->  (
( RR  _D  G
) `  y )  e.  _V )
14152feqmptd 5738 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  G  =  ( y  e.  ( A (,) B )  |->  ( G `  y ) ) )
142141oveq2d 6056 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  G )  =  ( RR  _D  ( y  e.  ( A (,) B )  |->  ( G `
 y ) ) ) )
143 dvf 19747 . . . . . . . . . . . . 13  |-  ( RR 
_D  G ) : dom  ( RR  _D  G ) --> CC
144 lhop2.ig . . . . . . . . . . . . . . 15  |-  ( ph  ->  dom  ( RR  _D  G )  =  ( A (,) B ) )
145144adantr 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  dom  ( RR  _D  G )  =  ( A (,) B ) )
146145feq2d 5540 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( ( RR 
_D  G ) : dom  ( RR  _D  G ) --> CC  <->  ( RR  _D  G ) : ( A (,) B ) --> CC ) )
147143, 146mpbii 203 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  G ) : ( A (,) B ) --> CC )
148147feqmptd 5738 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  G )  =  ( y  e.  ( A (,) B )  |->  ( ( RR  _D  G
) `  y )
) )
149142, 148eqtr3d 2438 . . . . . . . . . 10  |-  ( (
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 5687 . . . . . . . . . 10  |-  ( y  =  -u x  ->  ( G `  y )  =  ( G `  -u x ) )
151 fveq2 5687 . . . . . . . . . 10  |-  ( y  =  -u x  ->  (
( RR  _D  G
) `  y )  =  ( ( RR 
_D  G ) `  -u x ) )
15291, 91, 43, 93, 138, 140, 112, 149, 150, 151dvmptco 19811 . . . . . . . . 9  |-  ( (
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 452 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( RR  _D  G
) : ( A (,) B ) --> CC )
154153, 43ffvelrnd 5830 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( RR  _D  G ) `  -u x
)  e.  CC )
155154, 93mulcomd 9065 . . . . . . . . . . 11  |-  ( ( ( 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 9441 . . . . . . . . . . 11  |-  ( ( ( 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 2436 . . . . . . . . . 10  |-  ( ( ( 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 4255 . . . . . . . . 9  |-  ( (
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 2436 . . . . . . . 8  |-  ( (
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 5031 . . . . . . 7  |-  ( (
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 9260 . . . . . . . 8  |-  -u (
( RR  _D  G
) `  -u x )  e.  _V
162 eqid 2404 . . . . . . . 8  |-  ( 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 5533 . . . . . . 7  |-  dom  (
x  e.  ( -u B (,) -u a )  |->  -u ( ( RR  _D  G ) `  -u x
) )  =  (
-u B (,) -u a
)
164160, 163syl6eq 2452 . . . . . 6  |-  ( (
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 698 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  ( x  e.  ( -u B (,) -u a )  /\  -u x  =/=  B ) )  ->  -u x  e.  ( A (,) B
) )
166 limcresi 19725 . . . . . . . . 9  |-  ( ( 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 5150 . . . . . . . . . . 11  |-  ( (
-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 . . . . . . . . . 10  |-  ( ( x  e.  RR  |->  -u x )  |`  ( -u B (,) -u a
) )  =  ( x  e.  ( -u B (,) -u a )  |->  -u x )
169168oveq1i 6050 . . . . . . . . 9  |-  ( ( ( 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 3340 . . . . . . . 8  |-  ( ( x  e.  RR  |->  -u x ) lim CC  -u B
)  C_  ( (
x  e.  ( -u B (,) -u a )  |->  -u x ) lim CC  -u B
)
17175recnd 9070 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  B  e.  CC )
172171negnegd 9358 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -u -u B  =  B )
173 eqid 2404 . . . . . . . . . . . 12  |-  ( x  e.  RR  |->  -u x
)  =  ( x  e.  RR  |->  -u x
)
174173negcncf 18901 . . . . . . . . . . 11  |-  ( RR  C_  CC  ->  ( x  e.  RR  |->  -u x )  e.  ( RR -cn-> CC ) )
17553, 174mp1i 12 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( x  e.  RR  |->  -u x )  e.  ( RR -cn-> CC ) )
176 negeq 9254 . . . . . . . . . 10  |-  ( x  =  -u B  ->  -u x  =  -u -u B )
177175, 79, 176cnmptlimc 19730 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -u -u B  e.  ( ( x  e.  RR  |->  -u x ) lim CC  -u B
) )
178172, 177eqeltrrd 2479 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  B  e.  ( ( x  e.  RR  |->  -u x ) lim CC  -u B
) )
179170, 178sseldi 3306 . . . . . . 7  |-  ( (
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 . . . . . . . . 9  |-  ( ph  ->  0  e.  ( F lim
CC  B ) )
181180adantr 452 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  0  e.  ( F lim CC  B ) )
182113oveq1d 6055 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( F lim CC  B )  =  ( ( y  e.  ( A (,) B ) 
|->  ( F `  y
) ) lim CC  B
) )
183181, 182eleqtrd 2480 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  0  e.  ( ( y  e.  ( A (,) B ) 
|->  ( F `  y
) ) lim CC  B
) )
184 eliooord 10926 . . . . . . . . . . . . . 14  |-  ( x  e.  ( -u B (,) -u a )  -> 
( -u B  <  x  /\  x  <  -u a
) )
185184adantl 453 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( -u B  <  x  /\  x  <  -u a
) )
186185simpld 446 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -u B  <  x )
18729, 23, 186ltnegcon1d 9562 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -u x  <  B )
18830, 187ltned 9165 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -u x  =/=  B )
189188neneqd 2583 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -.  -u x  =  B )
190189pm2.21d 100 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( -u x  =  B  ->  ( F `  -u x )  =  0 ) )
191190impr 603 . . . . . . 7  |-  ( ( ( 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 19733 . . . . . 6  |-  ( (
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 . . . . . . . . 9  |-  ( ph  ->  0  e.  ( G lim
CC  B ) )
194193adantr 452 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  0  e.  ( G lim CC  B ) )
195141oveq1d 6055 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( G lim CC  B )  =  ( ( y  e.  ( A (,) B ) 
|->  ( G `  y
) ) lim CC  B
) )
196194, 195eleqtrd 2480 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  0  e.  ( ( y  e.  ( A (,) B ) 
|->  ( G `  y
) ) lim CC  B
) )
197189pm2.21d 100 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( -u x  =  B  ->  ( G `  -u x )  =  0 ) )
198197impr 603 . . . . . . 7  |-  ( ( ( 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 19733 . . . . . 6  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  0  e.  ( ( x  e.  (
-u B (,) -u a
)  |->  ( G `  -u x ) ) lim CC  -u B ) )
20060, 87fmptd 5852 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( x  e.  ( -u B (,) -u a )  |->  ( G `
 -u x ) ) : ( -u B (,) -u a ) --> ran 
G )
201 frn 5556 . . . . . . . 8  |-  ( ( 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 )
202200, 201syl 16 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ran  ( x  e.  ( -u B (,) -u a )  |->  ( G `
 -u x ) ) 
C_  ran  G )
20350adantr 452 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -.  0  e.  ran  G )
204202, 203ssneldd 3311 . . . . . 6  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -.  0  e.  ran  ( x  e.  (
-u B (,) -u a
)  |->  ( G `  -u x ) ) )
205 lhop2.gd0 . . . . . . . 8  |-  ( ph  ->  -.  0  e.  ran  ( RR  _D  G
) )
206205adantr 452 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -.  0  e.  ran  ( RR  _D  G
) )
207159rneqd 5056 . . . . . . . . 9  |-  ( (
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
) ) )
208207eleq2d 2471 . . . . . . . 8  |-  ( (
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
) ) ) )
209162, 161elrnmpti 5080 . . . . . . . . 9  |-  ( 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 ) )
210 eqcom 2406 . . . . . . . . . . 11  |-  ( 0  =  -u ( ( RR 
_D  G ) `  -u x )  <->  -u ( ( RR  _D  G ) `
 -u x )  =  0 )
211154negeq0d 9359 . . . . . . . . . . . 12  |-  ( ( ( 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 ) )
212 ffn 5550 . . . . . . . . . . . . . . 15  |-  ( ( RR  _D  G ) : ( A (,) B ) --> CC  ->  ( RR  _D  G )  Fn  ( A (,) B ) )
213153, 212syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( RR  _D  G
)  Fn  ( A (,) B ) )
214 fnfvelrn 5826 . . . . . . . . . . . . . 14  |-  ( ( ( RR  _D  G
)  Fn  ( A (,) B )  /\  -u x  e.  ( A (,) B ) )  ->  ( ( RR 
_D  G ) `  -u x )  e.  ran  ( RR  _D  G
) )
215213, 43, 214syl2anc 643 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( RR  _D  G ) `  -u x
)  e.  ran  ( RR  _D  G ) )
216 eleq1 2464 . . . . . . . . . . . . 13  |-  ( ( ( RR  _D  G
) `  -u x )  =  0  ->  (
( ( RR  _D  G ) `  -u x
)  e.  ran  ( RR  _D  G )  <->  0  e.  ran  ( RR  _D  G
) ) )
217215, 216syl5ibcom 212 . . . . . . . . . . . 12  |-  ( ( ( 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
) ) )
218211, 217sylbird 227 . . . . . . . . . . 11  |-  ( ( ( 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
) ) )
219210, 218syl5bi 209 . . . . . . . . . 10  |-  ( ( ( 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
) ) )
220219rexlimdva 2790 . . . . . . . . 9  |-  ( (
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 ) ) )
221209, 220syl5bi 209 . . . . . . . 8  |-  ( (
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
) ) )
222208, 221sylbid 207 . . . . . . 7  |-  ( (
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
) ) )
223206, 222mtod 170 . . . . . 6  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -.  0  e.  ran  ( RR  _D  (
x  e.  ( -u B (,) -u a )  |->  ( G `  -u x
) ) ) )
224119ffvelrnda 5829 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  (
( RR  _D  F
) `  z )  e.  CC )
225147ffvelrnda 5829 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  (
( RR  _D  G
) `  z )  e.  CC )
226205ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  -.  0  e.  ran  ( RR 
_D  G ) )
227147, 212syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  G )  Fn  ( A (,) B ) )
228 fnfvelrn 5826 . . . . . . . . . . . . 13  |-  ( ( ( RR  _D  G
)  Fn  ( A (,) B )  /\  z  e.  ( A (,) B ) )  -> 
( ( RR  _D  G ) `  z
)  e.  ran  ( RR  _D  G ) )
229227, 228sylan 458 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  (
( RR  _D  G
) `  z )  e.  ran  ( RR  _D  G ) )
230 eleq1 2464 . . . . . . . . . . . 12  |-  ( ( ( RR  _D  G
) `  z )  =  0  ->  (
( ( RR  _D  G ) `  z
)  e.  ran  ( RR  _D  G )  <->  0  e.  ran  ( RR  _D  G
) ) )
231229, 230syl5ibcom 212 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  (
( ( RR  _D  G ) `  z
)  =  0  -> 
0  e.  ran  ( RR  _D  G ) ) )
232231necon3bd 2604 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  ( -.  0  e.  ran  ( RR  _D  G
)  ->  ( ( RR  _D  G ) `  z )  =/=  0
) )
233226, 232mpd 15 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  (
( RR  _D  G
) `  z )  =/=  0 )
234224, 225, 233divcld 9746 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  (
( ( RR  _D  F ) `  z
)  /  ( ( RR  _D  G ) `
 z ) )  e.  CC )
235 lhop2.c . . . . . . . . 9  |-  ( ph  ->  C  e.  ( ( z  e.  ( A (,) B )  |->  ( ( ( RR  _D  F ) `  z
)  /  ( ( RR  _D  G ) `
 z ) ) ) lim CC  B ) )
236235adantr 452 . . . . . . . 8  |-  ( (
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
) )
237 fveq2 5687 . . . . . . . . 9  |-  ( z  =  -u x  ->  (
( RR  _D  F
) `  z )  =  ( ( RR 
_D  F ) `  -u x ) )
238 fveq2 5687 . . . . . . . . 9  |-  ( z  =  -u x  ->  (
( RR  _D  G
) `  z )  =  ( ( RR 
_D  G ) `  -u x ) )
239237, 238oveq12d 6058 . . . . . . . 8  |-  ( z  =  -u x  ->  (
( ( RR  _D  F ) `  z
)  /  ( ( RR  _D  G ) `
 z ) )  =  ( ( ( RR  _D  F ) `
 -u x )  / 
( ( RR  _D  G ) `  -u x
) ) )
240189pm2.21d 100 . . . . . . . . 9  |-  ( ( ( 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 ) )
241240impr 603 . . . . . . . 8  |-  ( ( ( 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 )
242165, 234, 179, 236, 239, 241limcco 19733 . . . . . . 7  |-  ( (
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 ) )
243 nfcv 2540 . . . . . . . . . . . . 13  |-  F/_ x RR
244 nfcv 2540 . . . . . . . . . . . . 13  |-  F/_ x  _D
245 nfmpt1 4258 . . . . . . . . . . . . 13  |-  F/_ x
( x  e.  (
-u B (,) -u a
)  |->  ( F `  -u x ) )
246243, 244, 245nfov 6063 . . . . . . . . . . . 12  |-  F/_ x
( RR  _D  (
x  e.  ( -u B (,) -u a )  |->  ( F `  -u x
) ) )
247 nfcv 2540 . . . . . . . . . . . 12  |-  F/_ x
y
248246, 247nffv 5694 . . . . . . . . . . 11  |-  F/_ x
( ( RR  _D  ( x  e.  ( -u B (,) -u a
)  |->  ( F `  -u x ) ) ) `
 y )
249 nfcv 2540 . . . . . . . . . . 11  |-  F/_ x  /
250 nfmpt1 4258 . . . . . . . . . . . . 13  |-  F/_ x
( x  e.  (
-u B (,) -u a
)  |->  ( G `  -u x ) )
251243, 244, 250nfov 6063 . . . . . . . . . . . 12  |-  F/_ x
( RR  _D  (
x  e.  ( -u B (,) -u a )  |->  ( G `  -u x
) ) )
252251, 247nffv 5694 . . . . . . . . . . 11  |-  F/_ x
( ( RR  _D  ( x  e.  ( -u B (,) -u a
)  |->  ( G `  -u x ) ) ) `
 y )
253248, 249, 252nfov 6063 . . . . . . . . . 10  |-  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 ) )
254 nfcv 2540 . . . . . . . . . 10  |-  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 ) )
255 fveq2 5687 . . . . . . . . . . 11  |-  ( 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 ) )
256 fveq2 5687 . . . . . . . . . . 11  |-  ( 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 ) )
257255, 256oveq12d 6058 . . . . . . . . . 10  |-  ( 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 ) ) )
258253, 254, 257cbvmpt 4259 . . . . . . . . 9  |-  ( 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 ) ) )
259131fveq1d 5689 . . . . . . . . . . . . 13  |-  ( (
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
) )
260134fvmpt2 5771 . . . . . . . . . . . . . 14  |-  ( ( 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 ) )
261133, 260mpan2 653 . . . . . . . . . . . . 13  |-  ( 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 ) )
262259, 261sylan9eq 2456 . . . . . . . . . . . 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 )  = 
-u ( ( RR 
_D  F ) `  -u x ) )
263159fveq1d 5689 . . . . . . . . . . . . 13  |-  ( (
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
) )
264162fvmpt2 5771 . . . . . . . . . . . . . 14  |-  ( ( 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 ) )
265161, 264mpan2 653 . . . . . . . . . . . . 13  |-  ( 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 ) )
266263, 265sylan9eq 2456 . . . . . . . . . . . 12  |-  ( ( ( 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 ) )
267262, 266oveq12d 6058 . . . . . . . . . . 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 ) )  =  ( -u ( ( RR  _D  F ) `  -u x
)  /  -u (
( RR  _D  G
) `  -u x ) ) )
268205ad2antrr 707 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -.  0  e.  ran  ( RR  _D  G
) )
269217necon3bd 2604 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) )
270268, 269mpd 15 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( RR  _D  G ) `  -u x
)  =/=  0 )
271126, 154, 270div2negd 9761 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) )
272267, 271eqtrd 2436 . . . . . . . . . 10  |-  ( ( ( 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 ) ) )
273272mpteq2dva 4255 . . . . . . . . 9  |-  ( (
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 ) ) ) )
274258, 273syl5eq 2448 . . . . . . . 8  |-  ( (
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 ) ) ) )
275274oveq1d 6055 . . . . . . 7  |-  ( (
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
) )
276242, 275eleqtrrd 2481 . . . . . 6  |-  ( (
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 ) )
27779, 81, 84, 86, 88, 136, 164, 192, 199, 204, 223, 276lhop1 19851 . . . . 5  |-  ( (
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 ) )
278 nffvmpt1 5695 . . . . . . . . 9  |-  F/_ x
( ( x  e.  ( -u B (,) -u a )  |->  ( F `
 -u x ) ) `
 y )
279 nffvmpt1 5695 . . . . . . . . 9  |-  F/_ x
( ( x  e.  ( -u B (,) -u a )  |->  ( G `
 -u x ) ) `
 y )
280278, 249, 279nfov 6063 . . . . . . . 8  |-  F/_ x
( ( ( x  e.  ( -u B (,) -u a )  |->  ( F `  -u x
) ) `  y
)  /  ( ( x  e.  ( -u B (,) -u a )  |->  ( G `  -u x
) ) `  y
) )
281 nfcv 2540 . . . . . . . 8  |-  F/_ y
( ( ( x  e.  ( -u B (,) -u a )  |->  ( F `  -u x
) ) `  x
)  /  ( ( x  e.  ( -u B (,) -u a )  |->  ( G `  -u x
) ) `  x
) )
282 fveq2 5687 . . . . . . . . 9  |-  ( y  =  x  ->  (
( x  e.  (
-u B (,) -u a
)  |->  ( F `  -u x ) ) `  y )  =  ( ( x  e.  (
-u B (,) -u a
)  |->  ( F `  -u x ) ) `  x ) )
283 fveq2 5687 . . . . . . . . 9  |-  ( y  =  x  ->  (
( x  e.  (
-u B (,) -u a
)  |->  ( G `  -u x ) ) `  y )  =  ( ( x  e.  (
-u B (,) -u a
)  |->  ( G `  -u x ) ) `  x ) )
284282, 283oveq12d 6058 . . . . . . . 8  |-  ( 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
) ) )
285280, 281, 284cbvmpt 4259 . . . . . . 7  |-  ( 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 ) ) )
286 fvex 5701 . . . . . . . . . 10  |-  ( F `
 -u x )  e. 
_V
28785fvmpt2 5771 . . . . . . . . . 10  |-  ( ( x  e.  ( -u B (,) -u a )  /\  ( F `  -u x
)  e.  _V )  ->  ( ( x  e.  ( -u B (,) -u a )  |->  ( F `
 -u x ) ) `
 x )  =  ( F `  -u x
) )
28826, 286, 287sylancl 644 . . . . . . . . 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 )  =  ( F `  -u x
) )
289 fvex 5701 . . . . . . . . . 10  |-  ( G `
 -u x )  e. 
_V
29087fvmpt2 5771 . . . . . . . . . 10  |-  ( ( x  e.  ( -u B (,) -u a )  /\  ( G `  -u x
)  e.  _V )  ->  ( ( x  e.  ( -u B (,) -u a )  |->  ( G `
 -u x ) ) `
 x )  =  ( G `  -u x
) )
29126, 289, 290sylancl 644 . . . . . . . . 9  |-  ( ( ( 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
) )
292288, 291oveq12d 6058 . . . . . . . 8  |-  ( ( ( 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 ) ) )
293292mpteq2dva 4255 . . . . . . 7  |-  ( (
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 ) ) ) )
294285, 293syl5eq 2448 . . . . . 6  |-  ( (
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 ) ) ) )
295294oveq1d 6055 . . . . 5  |-  ( (
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
) )
296277, 295eleqtrd 2480 . . . 4  |-  ( (
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 ) )
297 negeq 9254 . . . . . 6  |-  ( x  =  -u z  ->  -u x  =  -u -u z )
298297fveq2d 5691 . . . . 5  |-  ( x  =  -u z  ->  ( F `  -u x )  =  ( F `  -u -u z ) )
299297fveq2d 5691 . . . . 5  |-  ( x  =  -u z  ->  ( G `  -u x )  =  ( G `  -u -u z ) )
300298, 299oveq12d 6058 . . . 4  |-  ( x  =  -u z  ->  (
( F `  -u x
)  /  ( G `
 -u x ) )  =  ( ( F `
 -u -u z )  / 
( G `  -u -u z
) ) )
30179adantr 452 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  -u B  e.  RR )
302 eliooord 10926 . . . . . . . . . . 11  |-  ( z  e.  ( a (,) B )  ->  (
a  <  z  /\  z  <  B ) )
303302adantl 453 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  (
a  <  z  /\  z  <  B ) )
304303simprd 450 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  z  <  B )
30515, 13ltnegd 9560 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  (
z  <  B  <->  -u B  <  -u z ) )
306304, 305mpbid 202 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  -u B  <  -u z )
307301, 306gtned 9164 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  -u z  =/=  -u B )
308307neneqd 2583 . . . . . 6  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  -.  -u z  =  -u B
)
309308pm2.21d 100 . . . . 5  |-  ( ( ( 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 ) )
310309impr 603 . . . 4  |-  ( ( ( 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 )
31119, 65, 78, 296, 300, 310limcco 19733 . . 3  |-  ( (
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 ) )
31215recnd 9070 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  z  e.  CC )
313312negnegd 9358 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  -u -u z  =  z )
314313fveq2d 5691 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  ( F `  -u -u z
)  =  ( F `
 z ) )
315313fveq2d 5691 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  ( G `  -u -u z
)  =  ( G `
 z ) )
316314, 315oveq12d 6058 . . . . . 6  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  (
( F `  -u -u z
)  /  ( G `
 -u -u z ) )  =  ( ( F `
 z )  / 
( G `  z
) ) )
317316mpteq2dva 4255 . . . . 5  |-  ( (
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 )
) ) )
318317oveq1d 6055 . . . 4  |-  ( (
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 ) )
319 resmpt 5150 . . . . . 6  |-  ( ( a (,) B ) 
C_  ( A (,) B )  ->  (
( z  e.  ( A (,) B ) 
|->  ( ( F `  z )  /  ( G `  z )
) )  |`  (
a (,) B ) )  =  ( z  e.  ( a (,) B )  |->  ( ( F `  z )  /  ( G `  z ) ) ) )
32041, 319syl 16 . . . . 5  |-  ( (
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 ) ) ) )
321320oveq1d 6055 . . . 4  |-  ( (
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
) )
322 fss 5558 . . . . . . . . 9  |-  ( ( F : ( A (,) B ) --> RR 
/\  RR  C_  CC )  ->  F : ( A (,) B ) --> CC )
32394, 53, 322sylancl 644 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  F : ( A (,) B ) --> CC )
324323ffvelrnda 5829 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  ( F `  z )  e.  CC )
32555ffvelrnda 5829 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  ( G `  z )  e.  CC )
32650ad2antrr 707 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  -.  0  e.  ran  G )
32755, 57syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  G  Fn  ( A (,) B ) )
328 fnfvelrn 5826 . . . . . . . . . . 11  |-  ( ( G  Fn  ( A (,) B )  /\  z  e.  ( A (,) B ) )  -> 
( G `  z
)  e.  ran  G
)
329327, 328sylan 458 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  ( G `  z )  e.  ran  G )
330 eleq1 2464 . . . . . . . . . 10  |-  ( ( G `  z )  =  0  ->  (
( G `  z
)  e.  ran  G  <->  0  e.  ran  G ) )
331329, 330syl5ibcom 212 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  (
( G `  z
)  =  0  -> 
0  e.  ran  G
) )
332331necon3bd 2604 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  ( -.  0  e.  ran  G  ->  ( G `  z )  =/=  0
) )
333326, 332mpd 15 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  ( G `  z )  =/=  0 )
334324, 325, 333divcld 9746 . . . . . 6  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  (
( F `  z
)  /  ( G `
 z ) )  e.  CC )
335 eqid 2404 . . . . . 6  |-  ( z  e.  ( A (,) B )  |->  ( ( F `  z )  /  ( G `  z ) ) )  =  ( z  e.  ( A (,) B
)  |->  ( ( F `
 z )  / 
( G `  z
) ) )
336334, 335fmptd 5852 . . . . 5  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( z  e.  ( A (,) B
)  |->  ( ( F `
 z )  / 
( G `  z
) ) ) : ( A (,) B
) --> CC )
337 ioossre 10928 . . . . . . 7  |-  ( A (,) B )  C_  RR
338337, 53sstri 3317 . . . . . 6  |-  ( A (,) B )  C_  CC
339338a1i 11 . . . . 5  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( A (,) B )  C_  CC )
340 eqid 2404 . . . . 5  |-  ( (
TopOpen ` fld )t  ( ( A (,) B )  u.  { B } ) )  =  ( ( TopOpen ` fld )t  ( ( A (,) B )  u. 
{ B } ) )
341 ssun2 3471 . . . . . . 7  |-  { B }  C_  ( ( a (,) B )  u. 
{ B } )
342 snssg 3892 . . . . . . . 8  |-  ( B  e.  RR  ->  ( B  e.  ( (
a (,) B )  u.  { B }
)  <->  { B }  C_  ( ( a (,) B )  u.  { B } ) ) )
34375, 342syl 16 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( B  e.  ( ( a (,) B )  u.  { B } )  <->  { B }  C_  ( ( a (,) B )  u. 
{ B } ) ) )
344341, 343mpbiri 225 . . . . . 6  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  B  e.  ( ( a (,) B
)  u.  { B } ) )
345107cnfldtopon 18770 . . . . . . . . 9  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
346337a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( A (,) B )  C_  RR )
34775snssd 3903 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  { B }  C_  RR )
348346, 347unssd 3483 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( ( A (,) B )  u. 
{ B } ) 
C_  RR )
349348, 53syl6ss 3320 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( ( A (,) B )  u. 
{ B } ) 
C_  CC )
350 resttopon 17179 . . . . . . . . 9  |-  ( ( ( TopOpen ` fld )  e.  (TopOn `  CC )  /\  (
( A (,) B
)  u.  { B } )  C_  CC )  ->  ( ( TopOpen ` fld )t  (
( A (,) B
)  u.  { B } ) )  e.  (TopOn `  ( ( A (,) B )  u. 
{ B } ) ) )
351345, 349, 350sylancr 645 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( ( TopOpen ` fld )t  (
( A (,) B
)  u.  { B } ) )  e.  (TopOn `  ( ( A (,) B )  u. 
{ B } ) ) )
352 topontop 16946 . . . . . . . 8  |-  ( ( ( TopOpen ` fld )t  ( ( A (,) B )  u. 
{ B } ) )  e.  (TopOn `  ( ( A (,) B )  u.  { B } ) )  -> 
( ( TopOpen ` fld )t  ( ( A (,) B )  u. 
{ B } ) )  e.  Top )
353351, 352syl 16 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( ( TopOpen ` fld )t  (
( A (,) B
)  u.  { B } ) )  e. 
Top )
354 indi 3547 . . . . . . . . . 10  |-  ( ( a (,)  +oo )  i^i  ( ( A (,) B )  u.  { B } ) )  =  ( ( ( a (,)  +oo )  i^i  ( A (,) B ) )  u.  ( ( a (,)  +oo )  i^i  { B } ) )
355 pnfxr 10669 . . . . . . . . . . . . . 14  |-  +oo  e.  RR*
356355a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  +oo  e.  RR* )
3574adantr 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  B  e.  RR* )
358 iooin 10906 . . . . . . . . . . . . 13  |-  ( ( ( 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
) ) )
35936, 356, 34, 357, 358syl22anc 1185 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( ( a (,)  +oo )  i^i  ( A (,) B ) )  =  ( if ( a  <_  A ,  A ,  a ) (,) if (  +oo  <_  B ,  +oo ,  B
) ) )
360 xrltnle 9100 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  RR*  /\  a  e.  RR* )  ->  ( A  <  a  <->  -.  a  <_  A ) )
36134, 36, 360syl2anc 643 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( A  < 
a  <->  -.  a  <_  A ) )
36235, 361mpbid 202 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -.  a  <_  A )
363 iffalse 3706 . . . . . . . . . . . . . 14  |-  ( -.  a  <_  A  ->  if ( a  <_  A ,  A ,  a )  =  a )
364362, 363syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  if ( a  <_  A ,  A ,  a )  =  a )
365 ltpnf 10677 . . . . . . . . . . . . . . . 16  |-  ( B  e.  RR  ->  B  <  +oo )
36675, 365syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  B  <  +oo )
367 xrltnle 9100 . . . . . . . . . . . . . . . 16  |-  ( ( B  e.  RR*  /\  +oo  e.  RR* )  ->  ( B  <  +oo  <->  -.  +oo  <_  B
) )
368357, 355, 367sylancl 644 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <