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

Theorem lhop2 19901
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 10586 . . 3  |-  QQ  C_  RR
2 lhop2.a . . . 4  |-  ( ph  ->  A  e.  RR* )
3 lhop2.b . . . . 5  |-  ( ph  ->  B  e.  RR )
43rexrd 9136 . . . 4  |-  ( ph  ->  B  e.  RR* )
5 lhop2.l . . . 4  |-  ( ph  ->  A  <  B )
6 qbtwnxr 10788 . . . 4  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  A  < 
B )  ->  E. a  e.  QQ  ( A  < 
a  /\  a  <  B ) )
72, 4, 5, 6syl3anc 1185 . . 3  |-  ( ph  ->  E. a  e.  QQ  ( A  <  a  /\  a  <  B ) )
8 ssrexv 3410 . . 3  |-  ( QQ  C_  RR  ->  ( E. a  e.  QQ  ( A  <  a  /\  a  <  B )  ->  E. a  e.  RR  ( A  < 
a  /\  a  <  B ) ) )
91, 7, 8mpsyl 62 . 2  |-  ( ph  ->  E. a  e.  RR  ( A  <  a  /\  a  <  B ) )
10 simpr 449 . . . . . 6  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  z  e.  ( a (,) B
) )
11 simprl 734 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  a  e.  RR )
1211adantr 453 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  a  e.  RR )
133ad2antrr 708 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  B  e.  RR )
14 elioore 10948 . . . . . . . 8  |-  ( z  e.  ( a (,) B )  ->  z  e.  RR )
1514adantl 454 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  z  e.  RR )
16 iooneg 11019 . . . . . . 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 1185 . . . . . 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 203 . . . . 5  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  -u z  e.  ( -u B (,) -u a ) )
1918adantrr 699 . . . 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 708 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  F : ( A (,) B ) --> RR )
22 elioore 10948 . . . . . . . . . . . . 13  |-  ( x  e.  ( -u B (,) -u a )  ->  x  e.  RR )
2322adantl 454 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  x  e.  RR )
2423recnd 9116 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  x  e.  CC )
2524negnegd 9404 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -u -u x  =  x
)
26 simpr 449 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  x  e.  ( -u B (,) -u a ) )
2725, 26eqeltrd 2512 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -u -u x  e.  ( -u B (,) -u a
) )
2811adantr 453 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
a  e.  RR )
293ad2antrr 708 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  B  e.  RR )
3023renegcld 9466 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -u x  e.  RR )
31 iooneg 11019 . . . . . . . . . 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 1185 . . . . . . . . 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 225 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -u x  e.  ( a (,) B ) )
342adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  A  e.  RR* )
35 simprrl 742 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  A  <  a
)
3611rexrd 9136 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  a  e.  RR* )
37 xrltle 10744 . . . . . . . . . . . 12  |-  ( ( A  e.  RR*  /\  a  e.  RR* )  ->  ( A  <  a  ->  A  <_  a ) )
3834, 36, 37syl2anc 644 . . . . . . . . . . 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 10953 . . . . . . . . . 10  |-  ( ( A  e.  RR*  /\  A  <_  a )  ->  (
a (,) B ) 
C_  ( A (,) B ) )
4134, 39, 40syl2anc 644 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( a (,) B )  C_  ( A (,) B ) )
4241sselda 3350 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  -u x  e.  ( a (,) B
) )  ->  -u x  e.  ( A (,) B
) )
4333, 42syldan 458 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -u x  e.  ( A (,) B ) )
4421, 43ffvelrnd 5873 . . . . . 6  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( F `  -u x
)  e.  RR )
4544recnd 9116 . . . . 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 708 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  G : ( A (,) B ) --> RR )
4847, 43ffvelrnd 5873 . . . . . 6  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( G `  -u x
)  e.  RR )
4948recnd 9116 . . . . 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 708 . . . . . 6  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -.  0  e.  ran  G )
5246adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  G : ( A (,) B ) --> RR )
53 ax-resscn 9049 . . . . . . . . . . . 12  |-  RR  C_  CC
54 fss 5601 . . . . . . . . . . . 12  |-  ( ( G : ( A (,) B ) --> RR 
/\  RR  C_  CC )  ->  G : ( A (,) B ) --> CC )
5552, 53, 54sylancl 645 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  G : ( A (,) B ) --> CC )
5655adantr 453 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  G : ( A (,) B ) --> CC )
57 ffn 5593 . . . . . . . . . 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 5869 . . . . . . . . 9  |-  ( ( G  Fn  ( A (,) B )  /\  -u x  e.  ( A (,) B ) )  ->  ( G `  -u x )  e.  ran  G )
6058, 43, 59syl2anc 644 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( G `  -u x
)  e.  ran  G
)
61 eleq1 2498 . . . . . . . 8  |-  ( ( G `  -u x
)  =  0  -> 
( ( G `  -u x )  e.  ran  G  <->  0  e.  ran  G
) )
6260, 61syl5ibcom 213 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( G `  -u x )  =  0  ->  0  e.  ran  G ) )
6362necon3bd 2640 . . . . . 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 9792 . . . 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 19774 . . . . . 6  |-  ( ( z  e.  RR  |->  -u z ) lim CC  B ) 
C_  ( ( ( z  e.  RR  |->  -u z )  |`  (
a (,) B ) ) lim CC  B )
67 ioossre 10974 . . . . . . . 8  |-  ( a (,) B )  C_  RR
68 resmpt 5193 . . . . . . . 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 6093 . . . . . 6  |-  ( ( ( z  e.  RR  |->  -u z )  |`  (
a (,) B ) ) lim CC  B )  =  ( ( z  e.  ( a (,) B )  |->  -u z
) lim CC  B )
7166, 70sseqtri 3382 . . . . 5  |-  ( ( z  e.  RR  |->  -u z ) lim CC  B ) 
C_  ( ( z  e.  ( a (,) B )  |->  -u z
) lim CC  B )
72 eqid 2438 . . . . . . . 8  |-  ( z  e.  RR  |->  -u z
)  =  ( z  e.  RR  |->  -u z
)
7372negcncf 18950 . . . . . . 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 453 . . . . . 6  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  B  e.  RR )
76 negeq 9300 . . . . . 6  |-  ( z  =  B  ->  -u z  =  -u B )
7774, 75, 76cnmptlimc 19779 . . . . 5  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -u B  e.  ( ( z  e.  RR  |->  -u z ) lim CC  B
) )
7871, 77sseldi 3348 . . . 4  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -u B  e.  ( ( z  e.  ( a (,) B ) 
|->  -u z ) lim CC  B ) )
7975renegcld 9466 . . . . . 6  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -u B  e.  RR )
8011renegcld 9466 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -u a  e.  RR )
8180rexrd 9136 . . . . . 6  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -u a  e.  RR* )
82 simprrr 743 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  a  <  B
)
8311, 75ltnegd 9606 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( a  < 
B  <->  -u B  <  -u a
) )
8482, 83mpbid 203 . . . . . 6  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -u B  <  -u a
)
85 eqid 2438 . . . . . . 7  |-  ( x  e.  ( -u B (,) -u a )  |->  ( F `  -u x
) )  =  ( x  e.  ( -u B (,) -u a )  |->  ( F `  -u x
) )
8644, 85fmptd 5895 . . . . . 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 2438 . . . . . . 7  |-  ( x  e.  ( -u B (,) -u a )  |->  ( G `  -u x
) )  =  ( x  e.  ( -u B (,) -u a )  |->  ( G `  -u x
) )
8848, 87fmptd 5895 . . . . . 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 9083 . . . . . . . . . . . 12  |-  RR  e.  _V
9089prid1 3914 . . . . . . . . . . 11  |-  RR  e.  { RR ,  CC }
9190a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  RR  e.  { RR ,  CC } )
92 neg1cn 10069 . . . . . . . . . . 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 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  F : ( A (,) B ) --> RR )
9594ffvelrnda 5872 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  y  e.  ( A (,) B
) )  ->  ( F `  y )  e.  RR )
9695recnd 9116 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  y  e.  ( A (,) B
) )  ->  ( F `  y )  e.  CC )
97 fvex 5744 . . . . . . . . . . 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 9050 . . . . . . . . . . . 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 449 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  RR )  ->  x  e.  RR )
102101recnd 9116 . . . . . . . . . . . 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 19845 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  ( x  e.  RR  |->  x ) )  =  ( x  e.  RR  |->  1 ) )
105 ioossre 10974 . . . . . . . . . . . . 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 2438 . . . . . . . . . . . . 13  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
108107tgioo2 18836 . . . . . . . . . . . 12  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
109 iooretop 18802 . . . . . . . . . . . . 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 19851 . . . . . . . . . . 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 19854 . . . . . . . . . 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 5781 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  F  =  ( y  e.  ( A (,) B )  |->  ( F `  y ) ) )
114113oveq2d 6099 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  F )  =  ( RR  _D  ( y  e.  ( A (,) B )  |->  ( F `
 y ) ) ) )
115 dvf 19796 . . . . . . . . . . . . 13  |-  ( RR 
_D  F ) : dom  ( RR  _D  F ) --> CC
116 lhop2.if . . . . . . . . . . . . . . 15  |-  ( ph  ->  dom  ( RR  _D  F )  =  ( A (,) B ) )
117116adantr 453 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  dom  ( RR  _D  F )  =  ( A (,) B ) )
118117feq2d 5583 . . . . . . . . . . . . 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 204 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  F ) : ( A (,) B ) --> CC )
120119feqmptd 5781 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  F )  =  ( y  e.  ( A (,) B )  |->  ( ( RR  _D  F
) `  y )
) )
121114, 120eqtr3d 2472 . . . . . . . . . 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 5730 . . . . . . . . . 10  |-  ( y  =  -u x  ->  ( F `  y )  =  ( F `  -u x ) )
123 fveq2 5730 . . . . . . . . . 10  |-  ( y  =  -u x  ->  (
( RR  _D  F
) `  y )  =  ( ( RR 
_D  F ) `  -u x ) )
12491, 91, 43, 93, 96, 98, 112, 121, 122, 123dvmptco 19860 . . . . . . . . 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 453 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( RR  _D  F
) : ( A (,) B ) --> CC )
126125, 43ffvelrnd 5873 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( RR  _D  F ) `  -u x
)  e.  CC )
127126, 93mulcomd 9111 . . . . . . . . . . 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 9487 . . . . . . . . . . 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 2470 . . . . . . . . . 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 4297 . . . . . . . . 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 2470 . . . . . . . 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 5074 . . . . . . 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 9306 . . . . . . . 8  |-  -u (
( RR  _D  F
) `  -u x )  e.  _V
134 eqid 2438 . . . . . . . 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 5576 . . . . . . 7  |-  dom  (
x  e.  ( -u B (,) -u a )  |->  -u ( ( RR  _D  F ) `  -u x
) )  =  (
-u B (,) -u a
)
136132, 135syl6eq 2486 . . . . . 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 5872 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  y  e.  ( A (,) B
) )  ->  ( G `  y )  e.  RR )
138137recnd 9116 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  y  e.  ( A (,) B
) )  ->  ( G `  y )  e.  CC )
139 fvex 5744 . . . . . . . . . . 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 5781 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  G  =  ( y  e.  ( A (,) B )  |->  ( G `  y ) ) )
142141oveq2d 6099 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  G )  =  ( RR  _D  ( y  e.  ( A (,) B )  |->  ( G `
 y ) ) ) )
143 dvf 19796 . . . . . . . . . . . . 13  |-  ( RR 
_D  G ) : dom  ( RR  _D  G ) --> CC
144 lhop2.ig . . . . . . . . . . . . . . 15  |-  ( ph  ->  dom  ( RR  _D  G )  =  ( A (,) B ) )
145144adantr 453 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  dom  ( RR  _D  G )  =  ( A (,) B ) )
146145feq2d 5583 . . . . . . . . . . . . 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 204 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  G ) : ( A (,) B ) --> CC )
148147feqmptd 5781 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( RR  _D  G )  =  ( y  e.  ( A (,) B )  |->  ( ( RR  _D  G
) `  y )
) )
149142, 148eqtr3d 2472 . . . . . . . . . 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 5730 . . . . . . . . . 10  |-  ( y  =  -u x  ->  ( G `  y )  =  ( G `  -u x ) )
151 fveq2 5730 . . . . . . . . . 10  |-  ( y  =  -u x  ->  (
( RR  _D  G
) `  y )  =  ( ( RR 
_D  G ) `  -u x ) )
15291, 91, 43, 93, 138, 140, 112, 149, 150, 151dvmptco 19860 . . . . . . . . 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 453 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( RR  _D  G
) : ( A (,) B ) --> CC )
154153, 43ffvelrnd 5873 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( ( RR  _D  G ) `  -u x
)  e.  CC )
155154, 93mulcomd 9111 . . . . . . . . . . 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 9487 . . . . . . . . . . 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 2470 . . . . . . . . . 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 4297 . . . . . . . . 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 2470 . . . . . . . 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 5074 . . . . . . 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 9306 . . . . . . . 8  |-  -u (
( RR  _D  G
) `  -u x )  e.  _V
162 eqid 2438 . . . . . . . 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 5576 . . . . . . 7  |-  dom  (
x  e.  ( -u B (,) -u a )  |->  -u ( ( RR  _D  G ) `  -u x
) )  =  (
-u B (,) -u a
)
164160, 163syl6eq 2486 . . . . . 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 699 . . . . . . 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 19774 . . . . . . . . 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 5193 . . . . . . . . . . 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 6093 . . . . . . . . 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 3382 . . . . . . . 8  |-  ( ( x  e.  RR  |->  -u x ) lim CC  -u B
)  C_  ( (
x  e.  ( -u B (,) -u a )  |->  -u x ) lim CC  -u B
)
17175recnd 9116 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  B  e.  CC )
172171negnegd 9404 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -u -u B  =  B )
173 eqid 2438 . . . . . . . . . . . 12  |-  ( x  e.  RR  |->  -u x
)  =  ( x  e.  RR  |->  -u x
)
174173negcncf 18950 . . . . . . . . . . 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 9300 . . . . . . . . . 10  |-  ( x  =  -u B  ->  -u x  =  -u -u B )
177175, 79, 176cnmptlimc 19779 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -u -u B  e.  ( ( x  e.  RR  |->  -u x ) lim CC  -u B
) )
178172, 177eqeltrrd 2513 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  B  e.  ( ( x  e.  RR  |->  -u x ) lim CC  -u B
) )
179170, 178sseldi 3348 . . . . . . 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 453 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  0  e.  ( F lim CC  B ) )
182113oveq1d 6098 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( F lim CC  B )  =  ( ( y  e.  ( A (,) B ) 
|->  ( F `  y
) ) lim CC  B
) )
183181, 182eleqtrd 2514 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  0  e.  ( ( y  e.  ( A (,) B ) 
|->  ( F `  y
) ) lim CC  B
) )
184 eliooord 10972 . . . . . . . . . . . . . 14  |-  ( x  e.  ( -u B (,) -u a )  -> 
( -u B  <  x  /\  x  <  -u a
) )
185184adantl 454 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( -u B  <  x  /\  x  <  -u a
) )
186185simpld 447 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -u B  <  x )
18729, 23, 186ltnegcon1d 9608 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -u x  <  B )
18830, 187ltned 9211 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -u x  =/=  B )
189188neneqd 2619 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -.  -u x  =  B )
190189pm2.21d 101 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( -u x  =  B  ->  ( F `  -u x )  =  0 ) )
191190impr 604 . . . . . . 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 19782 . . . . . 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 453 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  0  e.  ( G lim CC  B ) )
195141oveq1d 6098 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( G lim CC  B )  =  ( ( y  e.  ( A (,) B ) 
|->  ( G `  y
) ) lim CC  B
) )
196194, 195eleqtrd 2514 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  0  e.  ( ( y  e.  ( A (,) B ) 
|->  ( G `  y
) ) lim CC  B
) )
197189pm2.21d 101 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  -> 
( -u x  =  B  ->  ( G `  -u x )  =  0 ) )
198197impr 604 . . . . . . 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 19782 . . . . . 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 5895 . . . . . . . 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 5599 . . . . . . . 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 453 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -.  0  e.  ran  G )
204202, 203ssneldd 3353 . . . . . 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 453 . . . . . . 7  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -.  0  e.  ran  ( RR  _D  G
) )
207159rneqd 5099 . . . . . . . . 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 2505 . . . . . . . 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 5123 . . . . . . . . 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 2440 . . . . . . . . . . 11  |-  ( 0  =  -u ( ( RR 
_D  G ) `  -u x )  <->  -u ( ( RR  _D  G ) `
 -u x )  =  0 )
211154negeq0d 9405 . . . . . . . . . . . 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 5593 . . . . . . . . . . . . . . 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 5869 . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . 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 2498 . . . . . . . . . . . . 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 213 . . . . . . . . . . . 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 228 . . . . . . . . . . 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 210 . . . . . . . . . 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 2832 . . . . . . . . 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 210 . . . . . . . 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 208 . . . . . . 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 171 . . . . . 6  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -.  0  e.  ran  ( RR  _D  (
x  e.  ( -u B (,) -u a )  |->  ( G `  -u x
) ) ) )
224119ffvelrnda 5872 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  (
( RR  _D  F
) `  z )  e.  CC )
225147ffvelrnda 5872 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  (
( RR  _D  G
) `  z )  e.  CC )
226205ad2antrr 708 . . . . . . . . . 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 5869 . . . . . . . . . . . . 13  |-  ( ( ( RR  _D  G
)  Fn  ( A (,) B )  /\  z  e.  ( A (,) B ) )  -> 
( ( RR  _D  G ) `  z
)  e.  ran  ( RR  _D  G ) )
229227, 228sylan 459 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  (
( RR  _D  G
) `  z )  e.  ran  ( RR  _D  G ) )
230 eleq1 2498 . . . . . . . . . . . 12  |-  ( ( ( RR  _D  G
) `  z )  =  0  ->  (
( ( RR  _D  G ) `  z
)  e.  ran  ( RR  _D  G )  <->  0  e.  ran  ( RR  _D  G
) ) )
231229, 230syl5ibcom 213 . . . . . . . . . . 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 2640 . . . . . . . . . 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 9792 . . . . . . . 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 453 . . . . . . . 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 5730 . . . . . . . . 9  |-  ( z  =  -u x  ->  (
( RR  _D  F
) `  z )  =  ( ( RR 
_D  F ) `  -u x ) )
238 fveq2 5730 . . . . . . . . 9  |-  ( z  =  -u x  ->  (
( RR  _D  G
) `  z )  =  ( ( RR 
_D  G ) `  -u x ) )
239237, 238oveq12d 6101 . . . . . . . 8  |-  ( z  =  -u x  ->  (
( ( RR  _D  F ) `  z
)  /  ( ( RR  _D  G ) `
 z ) )  =  ( ( ( RR  _D  F ) `
 -u x )  / 
( ( RR  _D  G ) `  -u x
) ) )
240189pm2.21d 101 . . . . . . . . 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 604 . . . . . . . 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 19782 . . . . . . 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 2574 . . . . . . . . . . . . 13  |-  F/_ x RR
244 nfcv 2574 . . . . . . . . . . . . 13  |-  F/_ x  _D
245 nfmpt1 4300 . . . . . . . . . . . . 13  |-  F/_ x
( x  e.  (
-u B (,) -u a
)  |->  ( F `  -u x ) )
246243, 244, 245nfov 6106 . . . . . . . . . . . 12  |-  F/_ x
( RR  _D  (
x  e.  ( -u B (,) -u a )  |->  ( F `  -u x
) ) )
247 nfcv 2574 . . . . . . . . . . . 12  |-  F/_ x
y
248246, 247nffv 5737 . . . . . . . . . . 11  |-  F/_ x
( ( RR  _D  ( x  e.  ( -u B (,) -u a
)  |->  ( F `  -u x ) ) ) `
 y )
249 nfcv 2574 . . . . . . . . . . 11  |-  F/_ x  /
250 nfmpt1 4300 . . . . . . . . . . . . 13  |-  F/_ x
( x  e.  (
-u B (,) -u a
)  |->  ( G `  -u x ) )
251243, 244, 250nfov 6106 . . . . . . . . . . . 12  |-  F/_ x
( RR  _D  (
x  e.  ( -u B (,) -u a )  |->  ( G `  -u x
) ) )
252251, 247nffv 5737 . . . . . . . . . . 11  |-  F/_ x
( ( RR  _D  ( x  e.  ( -u B (,) -u a
)  |->  ( G `  -u x ) ) ) `
 y )
253248, 249, 252nfov 6106 . . . . . . . . . 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 2574 . . . . . . . . . 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 5730 . . . . . . . . . . 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 5730 . . . . . . . . . . 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 6101 . . . . . . . . . 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 4301 . . . . . . . . 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 5732 . . . . . . . . . . . . 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 5814 . . . . . . . . . . . . . 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 654 . . . . . . . . . . . . 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 2490 . . . . . . . . . . . 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 5732 . . . . . . . . . . . . 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 5814 . . . . . . . . . . . . . 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 654 . . . . . . . . . . . . 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 2490 . . . . . . . . . . . 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 6101 . . . . . . . . . . 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 708 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  x  e.  ( -u B (,) -u a ) )  ->  -.  0  e.  ran  ( RR  _D  G
) )
269217necon3bd 2640 . . . . . . . . . . . . 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 9807 . . . . . . . . . . 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 2470 . . . . . . . . . 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 4297 . . . . . . . . 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 2482 . . . . . . . 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 6098 . . . . . . 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 2515 . . . . . 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 19900 . . . . 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 5738 . . . . . . . . 9  |-  F/_ x
( ( x  e.  ( -u B (,) -u a )  |->  ( F `
 -u x ) ) `
 y )
279 nffvmpt1 5738 . . . . . . . . 9  |-  F/_ x
( ( x  e.  ( -u B (,) -u a )  |->  ( G `
 -u x ) ) `
 y )
280278, 249, 279nfov 6106 . . . . . . . 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 2574 . . . . . . . 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 5730 . . . . . . . . 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 5730 . . . . . . . . 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 6101 . . . . . . . 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 4301 . . . . . . 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 5744 . . . . . . . . . 10  |-  ( F `
 -u x )  e. 
_V
28785fvmpt2 5814 . . . . . . . . . 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 645 . . . . . . . . 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 5744 . . . . . . . . . 10  |-  ( G `
 -u x )  e. 
_V
29087fvmpt2 5814 . . . . . . . . . 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 645 . . . . . . . . 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 6101 . . . . . . . 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 4297 . . . . . . 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 2482 . . . . . 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 6098 . . . . 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 2514 . . . 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 9300 . . . . . 6  |-  ( x  =  -u z  ->  -u x  =  -u -u z )
298297fveq2d 5734 . . . . 5  |-  ( x  =  -u z  ->  ( F `  -u x )  =  ( F `  -u -u z ) )
299297fveq2d 5734 . . . . 5  |-  ( x  =  -u z  ->  ( G `  -u x )  =  ( G `  -u -u z ) )
300298, 299oveq12d 6101 . . . 4  |-  ( x  =  -u z  ->  (
( F `  -u x
)  /  ( G `
 -u x ) )  =  ( ( F `
 -u -u z )  / 
( G `  -u -u z
) ) )
30179adantr 453 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  -u B  e.  RR )
302 eliooord 10972 . . . . . . . . . . 11  |-  ( z  e.  ( a (,) B )  ->  (
a  <  z  /\  z  <  B ) )
303302adantl 454 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  (
a  <  z  /\  z  <  B ) )
304303simprd 451 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  z  <  B )
30515, 13ltnegd 9606 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  (
z  <  B  <->  -u B  <  -u z ) )
306304, 305mpbid 203 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  -u B  <  -u z )
307301, 306gtned 9210 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  -u z  =/=  -u B )
308307neneqd 2619 . . . . . 6  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  -.  -u z  =  -u B
)
309308pm2.21d 101 . . . . 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 604 . . . 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 19782 . . 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 9116 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  z  e.  CC )
313312negnegd 9404 . . . . . . . 8  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  -u -u z  =  z )
314313fveq2d 5734 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  ( F `  -u -u z
)  =  ( F `
 z ) )
315313fveq2d 5734 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( a (,) B
) )  ->  ( G `  -u -u z
)  =  ( G `
 z ) )
316314, 315oveq12d 6101 . . . . . 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 4297 . . . . 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 6098 . . . 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 5193 . . . . . 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 6098 . . . 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 5601 . . . . . . . . 9  |-  ( ( F : ( A (,) B ) --> RR 
/\  RR  C_  CC )  ->  F : ( A (,) B ) --> CC )
32394, 53, 322sylancl 645 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  F : ( A (,) B ) --> CC )
324323ffvelrnda 5872 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  ( F `  z )  e.  CC )
32555ffvelrnda 5872 . . . . . . 7  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  ( G `  z )  e.  CC )
32650ad2antrr 708 . . . . . . . 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 5869 . . . . . . . . . . 11  |-  ( ( G  Fn  ( A (,) B )  /\  z  e.  ( A (,) B ) )  -> 
( G `  z
)  e.  ran  G
)
329327, 328sylan 459 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  ( G `  z )  e.  ran  G )
330 eleq1 2498 . . . . . . . . . 10  |-  ( ( G `  z )  =  0  ->  (
( G `  z
)  e.  ran  G  <->  0  e.  ran  G ) )
331329, 330syl5ibcom 213 . . . . . . . . 9  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  (
( G `  z
)  =  0  -> 
0  e.  ran  G
) )
332331necon3bd 2640 . . . . . . . 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 9792 . . . . . 6  |-  ( ( ( ph  /\  (
a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  /\  z  e.  ( A (,) B
) )  ->  (
( F `  z
)  /  ( G `
 z ) )  e.  CC )
335 eqid 2438 . . . . . 6  |-  ( z  e.  ( A (,) B )  |->  ( ( F `  z )  /  ( G `  z ) ) )  =  ( z  e.  ( A (,) B
)  |->  ( ( F `
 z )  / 
( G `  z
) ) )
336334, 335fmptd 5895 . . . . 5  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( z  e.  ( A (,) B
)  |->  ( ( F `
 z )  / 
( G `  z
) ) ) : ( A (,) B
) --> CC )
337 ioossre 10974 . . . . . . 7  |-  ( A (,) B )  C_  RR
338337, 53sstri 3359 . . . . . 6  |-  ( A (,) B )  C_  CC
339338a1i 11 . . . . 5  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( A (,) B )  C_  CC )
340 eqid 2438 . . . . 5  |-  ( (
TopOpen ` fld )t  ( ( A (,) B )  u.  { B } ) )  =  ( ( TopOpen ` fld )t  ( ( A (,) B )  u. 
{ B } ) )
341 ssun2 3513 . . . . . . 7  |-  { B }  C_  ( ( a (,) B )  u. 
{ B } )
342 snssg 3934 . . . . . . . 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 226 . . . . . 6  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  B  e.  ( ( a (,) B
)  u.  { B } ) )
345107cnfldtopon 18819 . . . . . . . . 9  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
346337a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( A (,) B )  C_  RR )
34775snssd 3945 . . . . . . . . . . 11  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  { B }  C_  RR )
348346, 347unssd 3525 . . . . . . . . . 10  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( ( A (,) B )  u. 
{ B } ) 
C_  RR )
349348, 53syl6ss 3362 . . . . . . . . 9  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( ( A (,) B )  u. 
{ B } ) 
C_  CC )
350 resttopon 17227 . . . . . . . . 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 646 . . . . . . . 8  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( ( TopOpen ` fld )t  (
( A (,) B
)  u.  { B } ) )  e.  (TopOn `  ( ( A (,) B )  u. 
{ B } ) ) )
352 topontop 16993 . . . . . . . 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 3589 . . . . . . . . . 10  |-  ( ( a (,)  +oo )  i^i  ( ( A (,) B )  u.  { B } ) )  =  ( ( ( a (,)  +oo )  i^i  ( A (,) B ) )  u.  ( ( a (,)  +oo )  i^i  { B } ) )
355 pnfxr 10715 . . . . . . . . . . . . . 14  |-  +oo  e.  RR*
356355a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  +oo  e.  RR* )
3574adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  B  e.  RR* )
358 iooin 10952 . . . . . . . . . . . . 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 1186 . . . . . . . . . . . 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 9146 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  RR*  /\  a  e.  RR* )  ->  ( A  <  a  <->  -.  a  <_  A ) )
36134, 36, 360syl2anc 644 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  ( A  < 
a  <->  -.  a  <_  A ) )
36235, 361mpbid 203 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  -.  a  <_  A )
363 iffalse 3748 . . . . . . . . . . . . . 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 10723 . . . . . . . . . . . . . . . 16  |-  ( B  e.  RR  ->  B  <  +oo )
36675, 365syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a  <  B ) ) )  ->  B  <  +oo )
367 xrltnle 9146 . . . . . . . . . . . . . . . 16  |-  ( ( B  e.  RR*  /\  +oo  e.  RR* )  ->  ( B  <  +oo  <->  -.  +oo  <_  B
) )
368357, 355, 367sylancl 645 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( a  e.  RR  /\  ( A  <  a  /\  a