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

Theorem lhop1lem 22499
Description: Lemma for lhop1 22500. (Contributed by Mario Carneiro, 29-Dec-2016.)
Hypotheses
Ref Expression
lhop1.a  |-  ( ph  ->  A  e.  RR )
lhop1.b  |-  ( ph  ->  B  e.  RR* )
lhop1.l  |-  ( ph  ->  A  <  B )
lhop1.f  |-  ( ph  ->  F : ( A (,) B ) --> RR )
lhop1.g  |-  ( ph  ->  G : ( A (,) B ) --> RR )
lhop1.if  |-  ( ph  ->  dom  ( RR  _D  F )  =  ( A (,) B ) )
lhop1.ig  |-  ( ph  ->  dom  ( RR  _D  G )  =  ( A (,) B ) )
lhop1.f0  |-  ( ph  ->  0  e.  ( F lim
CC  A ) )
lhop1.g0  |-  ( ph  ->  0  e.  ( G lim
CC  A ) )
lhop1.gn0  |-  ( ph  ->  -.  0  e.  ran  G )
lhop1.gd0  |-  ( ph  ->  -.  0  e.  ran  ( RR  _D  G
) )
lhop1.c  |-  ( ph  ->  C  e.  ( ( z  e.  ( A (,) B )  |->  ( ( ( RR  _D  F ) `  z
)  /  ( ( RR  _D  G ) `
 z ) ) ) lim CC  A ) )
lhop1lem.e  |-  ( ph  ->  E  e.  RR+ )
lhop1lem.d  |-  ( ph  ->  D  e.  RR )
lhop1lem.db  |-  ( ph  ->  D  <_  B )
lhop1lem.x  |-  ( ph  ->  X  e.  ( A (,) D ) )
lhop1lem.t  |-  ( ph  ->  A. t  e.  ( A (,) D ) ( abs `  (
( ( ( RR 
_D  F ) `  t )  /  (
( RR  _D  G
) `  t )
)  -  C ) )  <  E )
lhop1lem.r  |-  R  =  ( A  +  ( r  /  2 ) )
Assertion
Ref Expression
lhop1lem  |-  ( ph  ->  ( abs `  (
( ( F `  X )  /  ( G `  X )
)  -  C ) )  <  ( 2  x.  E ) )
Distinct variable groups:    z, r, B    t, D    ph, r, z   
z, R    t, r, A, z    E, r, t    X, r, z    C, r, t, z    F, r, t, z    G, r, t, z
Allowed substitution hints:    ph( t)    B( t)    D( z, r)    R( t, r)    E( z)    X( t)

Proof of Theorem lhop1lem
Dummy variables  v  x  u  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lhop1.f . . . . . . 7  |-  ( ph  ->  F : ( A (,) B ) --> RR )
2 lhop1.b . . . . . . . . 9  |-  ( ph  ->  B  e.  RR* )
3 lhop1lem.db . . . . . . . . 9  |-  ( ph  ->  D  <_  B )
4 iooss2 11486 . . . . . . . . 9  |-  ( ( B  e.  RR*  /\  D  <_  B )  ->  ( A (,) D )  C_  ( A (,) B ) )
52, 3, 4syl2anc 659 . . . . . . . 8  |-  ( ph  ->  ( A (,) D
)  C_  ( A (,) B ) )
6 lhop1lem.x . . . . . . . 8  |-  ( ph  ->  X  e.  ( A (,) D ) )
75, 6sseldd 3418 . . . . . . 7  |-  ( ph  ->  X  e.  ( A (,) B ) )
81, 7ffvelrnd 5934 . . . . . 6  |-  ( ph  ->  ( F `  X
)  e.  RR )
98recnd 9533 . . . . 5  |-  ( ph  ->  ( F `  X
)  e.  CC )
10 lhop1.g . . . . . . 7  |-  ( ph  ->  G : ( A (,) B ) --> RR )
1110, 7ffvelrnd 5934 . . . . . 6  |-  ( ph  ->  ( G `  X
)  e.  RR )
1211recnd 9533 . . . . 5  |-  ( ph  ->  ( G `  X
)  e.  CC )
13 lhop1.gn0 . . . . . 6  |-  ( ph  ->  -.  0  e.  ran  G )
14 ffn 5639 . . . . . . . . . 10  |-  ( G : ( A (,) B ) --> RR  ->  G  Fn  ( A (,) B ) )
1510, 14syl 16 . . . . . . . . 9  |-  ( ph  ->  G  Fn  ( A (,) B ) )
16 fnfvelrn 5930 . . . . . . . . 9  |-  ( ( G  Fn  ( A (,) B )  /\  X  e.  ( A (,) B ) )  -> 
( G `  X
)  e.  ran  G
)
1715, 7, 16syl2anc 659 . . . . . . . 8  |-  ( ph  ->  ( G `  X
)  e.  ran  G
)
18 eleq1 2454 . . . . . . . 8  |-  ( ( G `  X )  =  0  ->  (
( G `  X
)  e.  ran  G  <->  0  e.  ran  G ) )
1917, 18syl5ibcom 220 . . . . . . 7  |-  ( ph  ->  ( ( G `  X )  =  0  ->  0  e.  ran  G ) )
2019necon3bd 2594 . . . . . 6  |-  ( ph  ->  ( -.  0  e. 
ran  G  ->  ( G `
 X )  =/=  0 ) )
2113, 20mpd 15 . . . . 5  |-  ( ph  ->  ( G `  X
)  =/=  0 )
229, 12, 21divcld 10237 . . . 4  |-  ( ph  ->  ( ( F `  X )  /  ( G `  X )
)  e.  CC )
23 limccl 22364 . . . . 5  |-  ( ( z  e.  ( A (,) B )  |->  ( ( ( RR  _D  F ) `  z
)  /  ( ( RR  _D  G ) `
 z ) ) ) lim CC  A ) 
C_  CC
24 lhop1.c . . . . 5  |-  ( ph  ->  C  e.  ( ( z  e.  ( A (,) B )  |->  ( ( ( RR  _D  F ) `  z
)  /  ( ( RR  _D  G ) `
 z ) ) ) lim CC  A ) )
2523, 24sseldi 3415 . . . 4  |-  ( ph  ->  C  e.  CC )
2622, 25subcld 9844 . . 3  |-  ( ph  ->  ( ( ( F `
 X )  / 
( G `  X
) )  -  C
)  e.  CC )
2726abscld 13269 . 2  |-  ( ph  ->  ( abs `  (
( ( F `  X )  /  ( G `  X )
)  -  C ) )  e.  RR )
28 lhop1lem.e . . 3  |-  ( ph  ->  E  e.  RR+ )
2928rpred 11177 . 2  |-  ( ph  ->  E  e.  RR )
30 2re 10522 . . . 4  |-  2  e.  RR
3130a1i 11 . . 3  |-  ( ph  ->  2  e.  RR )
3231, 29remulcld 9535 . 2  |-  ( ph  ->  ( 2  x.  E
)  e.  RR )
33 cnxmet 21365 . . . . . . . . . . . . 13  |-  ( abs 
o.  -  )  e.  ( *Met `  CC )
3433a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( v  e.  ( TopOpen ` fld )  /\  A  e.  v ) )  -> 
( abs  o.  -  )  e.  ( *Met `  CC ) )
35 simprl 754 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( v  e.  ( TopOpen ` fld )  /\  A  e.  v ) )  -> 
v  e.  ( TopOpen ` fld )
)
36 simprr 755 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( v  e.  ( TopOpen ` fld )  /\  A  e.  v ) )  ->  A  e.  v )
37 eliooord 11505 . . . . . . . . . . . . . . . 16  |-  ( X  e.  ( A (,) D )  ->  ( A  <  X  /\  X  <  D ) )
386, 37syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( A  <  X  /\  X  <  D ) )
3938simpld 457 . . . . . . . . . . . . . 14  |-  ( ph  ->  A  <  X )
40 lhop1.a . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  e.  RR )
41 ioossre 11507 . . . . . . . . . . . . . . . 16  |-  ( A (,) D )  C_  RR
4241, 6sseldi 3415 . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  e.  RR )
43 difrp 11173 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  RR  /\  X  e.  RR )  ->  ( A  <  X  <->  ( X  -  A )  e.  RR+ ) )
4440, 42, 43syl2anc 659 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A  <  X  <->  ( X  -  A )  e.  RR+ ) )
4539, 44mpbid 210 . . . . . . . . . . . . 13  |-  ( ph  ->  ( X  -  A
)  e.  RR+ )
4645adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( v  e.  ( TopOpen ` fld )  /\  A  e.  v ) )  -> 
( X  -  A
)  e.  RR+ )
47 eqid 2382 . . . . . . . . . . . . . 14  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
4847cnfldtopn 21374 . . . . . . . . . . . . 13  |-  ( TopOpen ` fld )  =  ( MetOpen `  ( abs  o.  -  ) )
4948mopni3 21082 . . . . . . . . . . . 12  |-  ( ( ( ( abs  o.  -  )  e.  ( *Met `  CC )  /\  v  e.  (
TopOpen ` fld )  /\  A  e.  v )  /\  ( X  -  A )  e.  RR+ )  ->  E. r  e.  RR+  ( r  < 
( X  -  A
)  /\  ( A
( ball `  ( abs  o. 
-  ) ) r )  C_  v )
)
5034, 35, 36, 46, 49syl31anc 1229 . . . . . . . . . . 11  |-  ( (
ph  /\  ( v  e.  ( TopOpen ` fld )  /\  A  e.  v ) )  ->  E. r  e.  RR+  (
r  <  ( X  -  A )  /\  ( A ( ball `  ( abs  o.  -  ) ) r )  C_  v
) )
51 lhop1lem.r . . . . . . . . . . . . . . . . . . . . . . . 24  |-  R  =  ( A  +  ( r  /  2 ) )
5240adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  A  e.  RR )
53 simprl 754 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
r  e.  RR+ )
5453rpred 11177 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
r  e.  RR )
5554rehalfcld 10702 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( r  /  2
)  e.  RR )
5652, 55readdcld 9534 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( A  +  ( r  /  2 ) )  e.  RR )
5751, 56syl5eqel 2474 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  R  e.  RR )
5857recnd 9533 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  R  e.  CC )
5940recnd 9533 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  A  e.  CC )
6059adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  A  e.  CC )
61 eqid 2382 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( abs 
o.  -  )  =  ( abs  o.  -  )
6261cnmetdval 21363 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R  e.  CC  /\  A  e.  CC )  ->  ( R ( abs 
o.  -  ) A
)  =  ( abs `  ( R  -  A
) ) )
6358, 60, 62syl2anc 659 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R ( abs 
o.  -  ) A
)  =  ( abs `  ( R  -  A
) ) )
6451oveq1i 6206 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( R  -  A )  =  ( ( A  +  ( r  /  2
) )  -  A
)
6554recnd 9533 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
r  e.  CC )
6665halfcld 10700 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( r  /  2
)  e.  CC )
6760, 66pncan2d 9846 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( A  +  ( r  /  2
) )  -  A
)  =  ( r  /  2 ) )
6864, 67syl5eq 2435 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R  -  A
)  =  ( r  /  2 ) )
6968fveq2d 5778 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( abs `  ( R  -  A )
)  =  ( abs `  ( r  /  2
) ) )
7053rphalfcld 11189 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( r  /  2
)  e.  RR+ )
7170rpred 11177 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( r  /  2
)  e.  RR )
7270rpge0d 11181 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
0  <_  ( r  /  2 ) )
7371, 72absidd 13256 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( abs `  (
r  /  2 ) )  =  ( r  /  2 ) )
7463, 69, 733eqtrd 2427 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R ( abs 
o.  -  ) A
)  =  ( r  /  2 ) )
75 rphalflt 11166 . . . . . . . . . . . . . . . . . . . . 21  |-  ( r  e.  RR+  ->  ( r  /  2 )  < 
r )
7653, 75syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( r  /  2
)  <  r )
7774, 76eqbrtrd 4387 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R ( abs 
o.  -  ) A
)  <  r )
7833a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( abs  o.  -  )  e.  ( *Met `  CC ) )
7954rexrd 9554 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
r  e.  RR* )
80 elbl3 20980 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( abs  o.  -  )  e.  ( *Met `  CC )  /\  r  e.  RR* )  /\  ( A  e.  CC  /\  R  e.  CC ) )  -> 
( R  e.  ( A ( ball `  ( abs  o.  -  ) ) r )  <->  ( R
( abs  o.  -  ) A )  <  r
) )
8178, 79, 60, 58, 80syl22anc 1227 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R  e.  ( A ( ball `  ( abs  o.  -  ) ) r )  <->  ( R
( abs  o.  -  ) A )  <  r
) )
8277, 81mpbird 232 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  R  e.  ( A
( ball `  ( abs  o. 
-  ) ) r ) )
8352, 70ltaddrpd 11206 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  A  <  ( A  +  ( r  /  2
) ) )
8483, 51syl6breqr 4407 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  A  <  R )
8542adantr 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  X  e.  RR )
8685, 52resubcld 9905 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( X  -  A
)  e.  RR )
87 simprr 755 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
r  <  ( X  -  A ) )
8871, 54, 86, 76, 87lttrd 9654 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( r  /  2
)  <  ( X  -  A ) )
8952, 71, 85ltaddsub2d 10070 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( A  +  ( r  /  2
) )  <  X  <->  ( r  /  2 )  <  ( X  -  A ) ) )
9088, 89mpbird 232 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( A  +  ( r  /  2 ) )  <  X )
9151, 90syl5eqbr 4400 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  R  <  X )
9252rexrd 9554 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  A  e.  RR* )
9342rexrd 9554 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  X  e.  RR* )
9493adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  X  e.  RR* )
95 elioo2 11491 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  RR*  /\  X  e.  RR* )  ->  ( R  e.  ( A (,) X )  <->  ( R  e.  RR  /\  A  < 
R  /\  R  <  X ) ) )
9692, 94, 95syl2anc 659 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R  e.  ( A (,) X )  <-> 
( R  e.  RR  /\  A  <  R  /\  R  <  X ) ) )
9757, 84, 91, 96mpbir3and 1177 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  R  e.  ( A (,) X ) )
9882, 97elind 3602 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  R  e.  ( ( A ( ball `  ( abs  o.  -  ) ) r )  i^i  ( A (,) X ) ) )
999adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( F `  X
)  e.  CC )
1001adantr 463 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  F : ( A (,) B ) --> RR )
101 lhop1lem.d . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  D  e.  RR )
102101rexrd 9554 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  D  e.  RR* )
10338simprd 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  X  <  D )
10442, 101, 103ltled 9644 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  X  <_  D )
10593, 102, 2, 104, 3xrletrd 11286 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  X  <_  B )
106 iooss2 11486 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( B  e.  RR*  /\  X  <_  B )  ->  ( A (,) X )  C_  ( A (,) B ) )
1072, 105, 106syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( A (,) X
)  C_  ( A (,) B ) )
108107adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( A (,) X
)  C_  ( A (,) B ) )
109108, 97sseldd 3418 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  R  e.  ( A (,) B ) )
110100, 109ffvelrnd 5934 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( F `  R
)  e.  RR )
111110recnd 9533 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( F `  R
)  e.  CC )
11299, 111subcld 9844 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( F `  X )  -  ( F `  R )
)  e.  CC )
11312adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( G `  X
)  e.  CC )
11410adantr 463 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  G : ( A (,) B ) --> RR )
115114, 109ffvelrnd 5934 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( G `  R
)  e.  RR )
116115recnd 9533 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( G `  R
)  e.  CC )
117113, 116subcld 9844 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( G `  X )  -  ( G `  R )
)  e.  CC )
118 lhop1.gd0 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  -.  0  e.  ran  ( RR  _D  G
) )
119118adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  -.  0  e.  ran  ( RR  _D  G ) )
12012adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( G `  X )  e.  CC )
121107sselda 3417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  z  e.  ( A (,) B ) )
12210ffvelrnda 5933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  z  e.  ( A (,) B ) )  ->  ( G `  z )  e.  RR )
123121, 122syldan 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( G `  z )  e.  RR )
124123recnd 9533 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( G `  z )  e.  CC )
125120, 124subeq0ad 9854 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( (
( G `  X
)  -  ( G `
 z ) )  =  0  <->  ( G `  X )  =  ( G `  z ) ) )
126 ioossre 11507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( A (,) B )  C_  RR
127126, 121sseldi 3415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  z  e.  RR )
128127adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
z  e.  RR )
12942ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  ->  X  e.  RR )
130 eliooord 11505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z  e.  ( A (,) X )  ->  ( A  <  z  /\  z  <  X ) )
131130adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( A  <  z  /\  z  < 
X ) )
132131simprd 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  z  <  X )
133132adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
z  <  X )
13440rexrd 9554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  A  e.  RR* )
135134adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  A  e.  RR* )
1362adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  B  e.  RR* )
137131simpld 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  A  <  z )
13893, 102, 2, 103, 3xrltletrd 11285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  X  <  B )
139138adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  X  <  B )
140 iccssioo 11514 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <  z  /\  X  <  B ) )  ->  ( z [,] X )  C_  ( A (,) B ) )
141135, 136, 137, 139, 140syl22anc 1227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( z [,] X )  C_  ( A (,) B ) )
142141adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( z [,] X
)  C_  ( A (,) B ) )
143 ax-resscn 9460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  RR  C_  CC
144143a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  RR  C_  CC )
145 fss 5647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( G : ( A (,) B ) --> RR 
/\  RR  C_  CC )  ->  G : ( A (,) B ) --> CC )
14610, 143, 145sylancl 660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  G : ( A (,) B ) --> CC )
147126a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  ( A (,) B
)  C_  RR )
148 lhop1.ig . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  dom  ( RR  _D  G )  =  ( A (,) B ) )
149 dvcn 22409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( RR  C_  CC  /\  G : ( A (,) B ) --> CC 
/\  ( A (,) B )  C_  RR )  /\  dom  ( RR 
_D  G )  =  ( A (,) B
) )  ->  G  e.  ( ( A (,) B ) -cn-> CC ) )
150144, 146, 147, 148, 149syl31anc 1229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  G  e.  ( ( A (,) B )
-cn-> CC ) )
151 cncffvrn 21487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( RR  C_  CC  /\  G  e.  ( ( A (,) B ) -cn-> CC ) )  ->  ( G  e.  ( ( A (,) B ) -cn-> RR )  <-> 
G : ( A (,) B ) --> RR ) )
152143, 150, 151sylancr 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  ( G  e.  ( ( A (,) B
) -cn-> RR )  <->  G :
( A (,) B
) --> RR ) )
15310, 152mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  G  e.  ( ( A (,) B )
-cn-> RR ) )
154153ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  ->  G  e.  ( ( A (,) B ) -cn-> RR ) )
155 rescncf 21486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( z [,] X ) 
C_  ( A (,) B )  ->  ( G  e.  ( ( A (,) B ) -cn-> RR )  ->  ( G  |`  ( z [,] X
) )  e.  ( ( z [,] X
) -cn-> RR ) ) )
156142, 154, 155sylc 60 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( G  |`  (
z [,] X ) )  e.  ( ( z [,] X )
-cn-> RR ) )
157143a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  ->  RR  C_  CC )
158146ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  ->  G : ( A (,) B ) --> CC )
159126a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( A (,) B
)  C_  RR )
160142, 126syl6ss 3429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( z [,] X
)  C_  RR )
16147tgioo2 21393 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
16247, 161dvres 22400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( RR  C_  CC  /\  G : ( A (,) B ) --> CC )  /\  ( ( A (,) B ) 
C_  RR  /\  (
z [,] X ) 
C_  RR ) )  ->  ( RR  _D  ( G  |`  ( z [,] X ) ) )  =  ( ( RR  _D  G )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( z [,] X ) ) ) )
163157, 158, 159, 160, 162syl22anc 1227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( RR  _D  ( G  |`  ( z [,] X ) ) )  =  ( ( RR 
_D  G )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( z [,] X ) ) ) )
164 iccntr 21411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( z  e.  RR  /\  X  e.  RR )  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( z [,] X ) )  =  ( z (,) X
) )
165128, 129, 164syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( ( int `  ( topGen `
 ran  (,) )
) `  ( z [,] X ) )  =  ( z (,) X
) )
166165reseq2d 5186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( ( RR  _D  G )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( z [,] X ) ) )  =  ( ( RR 
_D  G )  |`  ( z (,) X
) ) )
167163, 166eqtrd 2423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( RR  _D  ( G  |`  ( z [,] X ) ) )  =  ( ( RR 
_D  G )  |`  ( z (,) X
) ) )
168167dmeqd 5118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  ->  dom  ( RR  _D  ( G  |`  ( z [,] X ) ) )  =  dom  ( ( RR  _D  G )  |`  ( z (,) X
) ) )
169 ioossicc 11531 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( z (,) X )  C_  ( z [,] X
)
170169, 142syl5ss 3428 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( z (,) X
)  C_  ( A (,) B ) )
171148ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  ->  dom  ( RR  _D  G
)  =  ( A (,) B ) )
172170, 171sseqtr4d 3454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( z (,) X
)  C_  dom  ( RR 
_D  G ) )
173 ssdmres 5207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( z (,) X ) 
C_  dom  ( RR  _D  G )  <->  dom  ( ( RR  _D  G )  |`  ( z (,) X
) )  =  ( z (,) X ) )
174172, 173sylib 196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  ->  dom  ( ( RR  _D  G )  |`  (
z (,) X ) )  =  ( z (,) X ) )
175168, 174eqtrd 2423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  ->  dom  ( RR  _D  ( G  |`  ( z [,] X ) ) )  =  ( z (,) X ) )
176127rexrd 9554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  z  e.  RR* )
17793adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  X  e.  RR* )
17842adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  X  e.  RR )
179127, 178, 132ltled 9644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  z  <_  X )
180 ubicc2 11558 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( z  e.  RR*  /\  X  e.  RR*  /\  z  <_  X )  ->  X  e.  ( z [,] X
) )
181176, 177, 179, 180syl3anc 1226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  X  e.  ( z [,] X
) )
182 fvres 5788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( X  e.  ( z [,] X )  ->  (
( G  |`  (
z [,] X ) ) `  X )  =  ( G `  X ) )
183181, 182syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( ( G  |`  ( z [,] X ) ) `  X )  =  ( G `  X ) )
184 lbicc2 11557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( z  e.  RR*  /\  X  e.  RR*  /\  z  <_  X )  ->  z  e.  ( z [,] X
) )
185176, 177, 179, 184syl3anc 1226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  z  e.  ( z [,] X
) )
186 fvres 5788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( z  e.  ( z [,] X )  ->  (
( G  |`  (
z [,] X ) ) `  z )  =  ( G `  z ) )
187185, 186syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( ( G  |`  ( z [,] X ) ) `  z )  =  ( G `  z ) )
188183, 187eqeq12d 2404 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( (
( G  |`  (
z [,] X ) ) `  X )  =  ( ( G  |`  ( z [,] X
) ) `  z
)  <->  ( G `  X )  =  ( G `  z ) ) )
189188biimpar 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( ( G  |`  ( z [,] X
) ) `  X
)  =  ( ( G  |`  ( z [,] X ) ) `  z ) )
190189eqcomd 2390 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( ( G  |`  ( z [,] X
) ) `  z
)  =  ( ( G  |`  ( z [,] X ) ) `  X ) )
191128, 129, 133, 156, 175, 190rolle 22476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  ->  E. w  e.  (
z (,) X ) ( ( RR  _D  ( G  |`  ( z [,] X ) ) ) `  w )  =  0 )
192167fveq1d 5776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( ( RR  _D  ( G  |`  ( z [,] X ) ) ) `  w )  =  ( ( ( RR  _D  G )  |`  ( z (,) X
) ) `  w
) )
193 fvres 5788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( w  e.  ( z (,) X )  ->  (
( ( RR  _D  G )  |`  (
z (,) X ) ) `  w )  =  ( ( RR 
_D  G ) `  w ) )
194192, 193sylan9eq 2443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  z  e.  ( A (,) X ) )  /\  ( G `  X )  =  ( G `  z ) )  /\  w  e.  ( z (,) X ) )  -> 
( ( RR  _D  ( G  |`  ( z [,] X ) ) ) `  w )  =  ( ( RR 
_D  G ) `  w ) )
195 dvf 22396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( RR 
_D  G ) : dom  ( RR  _D  G ) --> CC
196148feq2d 5626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  ( ( RR  _D  G ) : dom  ( RR  _D  G
) --> CC  <->  ( RR  _D  G ) : ( A (,) B ) --> CC ) )
197195, 196mpbii 211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  ( RR  _D  G
) : ( A (,) B ) --> CC )
198197ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( RR  _D  G
) : ( A (,) B ) --> CC )
199 ffn 5639 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( RR  _D  G ) : ( A (,) B ) --> CC  ->  ( RR  _D  G )  Fn  ( A (,) B ) )
200198, 199syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( RR  _D  G
)  Fn  ( A (,) B ) )
201200adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  z  e.  ( A (,) X ) )  /\  ( G `  X )  =  ( G `  z ) )  /\  w  e.  ( z (,) X ) )  -> 
( RR  _D  G
)  Fn  ( A (,) B ) )
202170sselda 3417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  z  e.  ( A (,) X ) )  /\  ( G `  X )  =  ( G `  z ) )  /\  w  e.  ( z (,) X ) )  ->  w  e.  ( A (,) B ) )
203 fnfvelrn 5930 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( RR  _D  G
)  Fn  ( A (,) B )  /\  w  e.  ( A (,) B ) )  -> 
( ( RR  _D  G ) `  w
)  e.  ran  ( RR  _D  G ) )
204201, 202, 203syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  z  e.  ( A (,) X ) )  /\  ( G `  X )  =  ( G `  z ) )  /\  w  e.  ( z (,) X ) )  -> 
( ( RR  _D  G ) `  w
)  e.  ran  ( RR  _D  G ) )
205194, 204eqeltrd 2470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  z  e.  ( A (,) X ) )  /\  ( G `  X )  =  ( G `  z ) )  /\  w  e.  ( z (,) X ) )  -> 
( ( RR  _D  ( G  |`  ( z [,] X ) ) ) `  w )  e.  ran  ( RR 
_D  G ) )
206 eleq1 2454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( RR  _D  ( G  |`  ( z [,] X ) ) ) `
 w )  =  0  ->  ( (
( RR  _D  ( G  |`  ( z [,] X ) ) ) `
 w )  e. 
ran  ( RR  _D  G )  <->  0  e.  ran  ( RR  _D  G
) ) )
207205, 206syl5ibcom 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  z  e.  ( A (,) X ) )  /\  ( G `  X )  =  ( G `  z ) )  /\  w  e.  ( z (,) X ) )  -> 
( ( ( RR 
_D  ( G  |`  ( z [,] X
) ) ) `  w )  =  0  ->  0  e.  ran  ( RR  _D  G
) ) )
208207rexlimdva 2874 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( E. w  e.  ( z (,) X
) ( ( RR 
_D  ( G  |`  ( z [,] X
) ) ) `  w )  =  0  ->  0  e.  ran  ( RR  _D  G
) ) )
209191, 208mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
0  e.  ran  ( RR  _D  G ) )
210209ex 432 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( ( G `  X )  =  ( G `  z )  ->  0  e.  ran  ( RR  _D  G ) ) )
211125, 210sylbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( (
( G `  X
)  -  ( G `
 z ) )  =  0  ->  0  e.  ran  ( RR  _D  G ) ) )
212211necon3bd 2594 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( -.  0  e.  ran  ( RR 
_D  G )  -> 
( ( G `  X )  -  ( G `  z )
)  =/=  0 ) )
213119, 212mpd 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( ( G `  X )  -  ( G `  z ) )  =/=  0 )
214213ralrimiva 2796 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  A. z  e.  ( A (,) X ) ( ( G `  X )  -  ( G `  z )
)  =/=  0 )
215214adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  A. z  e.  ( A (,) X ) ( ( G `  X
)  -  ( G `
 z ) )  =/=  0 )
216 fveq2 5774 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  =  R  ->  ( G `  z )  =  ( G `  R ) )
217216oveq2d 6212 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( z  =  R  ->  (
( G `  X
)  -  ( G `
 z ) )  =  ( ( G `
 X )  -  ( G `  R ) ) )
218217neeq1d 2659 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  =  R  ->  (
( ( G `  X )  -  ( G `  z )
)  =/=  0  <->  (
( G `  X
)  -  ( G `
 R ) )  =/=  0 ) )
219218rspcv 3131 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( R  e.  ( A (,) X )  ->  ( A. z  e.  ( A (,) X ) ( ( G `  X
)  -  ( G `
 z ) )  =/=  0  ->  (
( G `  X
)  -  ( G `
 R ) )  =/=  0 ) )
22097, 215, 219sylc 60 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( G `  X )  -  ( G `  R )
)  =/=  0 )
221112, 117, 220divcld 10237 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( ( F `
 X )  -  ( F `  R ) )  /  ( ( G `  X )  -  ( G `  R ) ) )  e.  CC )
22225adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  C  e.  CC )
223221, 222subcld 9844 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( ( ( F `  X )  -  ( F `  R ) )  / 
( ( G `  X )  -  ( G `  R )
) )  -  C
)  e.  CC )
224223abscld 13269 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( abs `  (
( ( ( F `
 X )  -  ( F `  R ) )  /  ( ( G `  X )  -  ( G `  R ) ) )  -  C ) )  e.  RR )
22529adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  E  e.  RR )
226102adantr 463 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  D  e.  RR* )
227103adantr 463 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  X  <  D )
228 iccssioo 11514 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( A  e.  RR*  /\  D  e.  RR* )  /\  ( A  <  R  /\  X  <  D ) )  ->  ( R [,] X )  C_  ( A (,) D ) )
22992, 226, 84, 227, 228syl22anc 1227 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R [,] X
)  C_  ( A (,) D ) )
2305adantr 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( A (,) D
)  C_  ( A (,) B ) )
231229, 230sstrd 3427 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R [,] X
)  C_  ( A (,) B ) )
232 fss 5647 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( F : ( A (,) B ) --> RR 
/\  RR  C_  CC )  ->  F : ( A (,) B ) --> CC )
2331, 143, 232sylancl 660 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  F : ( A (,) B ) --> CC )
234 lhop1.if . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  dom  ( RR  _D  F )  =  ( A (,) B ) )
235 dvcn 22409 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( RR  C_  CC  /\  F : ( A (,) B ) --> CC 
/\  ( A (,) B )  C_  RR )  /\  dom  ( RR 
_D  F )  =  ( A (,) B
) )  ->  F  e.  ( ( A (,) B ) -cn-> CC ) )
236144, 233, 147, 234, 235syl31anc 1229 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  F  e.  ( ( A (,) B )
-cn-> CC ) )
237 cncffvrn 21487 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( RR  C_  CC  /\  F  e.  ( ( A (,) B ) -cn-> CC ) )  ->  ( F  e.  ( ( A (,) B ) -cn-> RR )  <-> 
F : ( A (,) B ) --> RR ) )
238143, 236, 237sylancr 661 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( F  e.  ( ( A (,) B
) -cn-> RR )  <->  F :
( A (,) B
) --> RR ) )
2391, 238mpbird 232 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  F  e.  ( ( A (,) B )
-cn-> RR ) )
240239adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  F  e.  ( ( A (,) B ) -cn-> RR ) )
241 rescncf 21486 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R [,] X ) 
C_  ( A (,) B )  ->  ( F  e.  ( ( A (,) B ) -cn-> RR )  ->  ( F  |`  ( R [,] X
) )  e.  ( ( R [,] X
) -cn-> RR ) ) )
242231, 240, 241sylc 60 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( F  |`  ( R [,] X ) )  e.  ( ( R [,] X ) -cn-> RR ) )
243153adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  G  e.  ( ( A (,) B ) -cn-> RR ) )
244 rescncf 21486 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R [,] X ) 
C_  ( A (,) B )  ->  ( G  e.  ( ( A (,) B ) -cn-> RR )  ->  ( G  |`  ( R [,] X
) )  e.  ( ( R [,] X
) -cn-> RR ) ) )
245231, 243, 244sylc 60 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( G  |`  ( R [,] X ) )  e.  ( ( R [,] X ) -cn-> RR ) )
246143a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  RR  C_  CC )
247233adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  F : ( A (,) B ) --> CC )
248126a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( A (,) B
)  C_  RR )
249 iccssre 11527 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( R  e.  RR  /\  X  e.  RR )  ->  ( R [,] X
)  C_  RR )
25057, 85, 249syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R [,] X
)  C_  RR )
25147, 161dvres 22400 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( RR  C_  CC  /\  F : ( A (,) B ) --> CC )  /\  ( ( A (,) B ) 
C_  RR  /\  ( R [,] X )  C_  RR ) )  ->  ( RR  _D  ( F  |`  ( R [,] X ) ) )  =  ( ( RR  _D  F
)  |`  ( ( int `  ( topGen `  ran  (,) )
) `  ( R [,] X ) ) ) )
252246, 247, 248, 250, 251syl22anc 1227 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( RR  _D  ( F  |`  ( R [,] X ) ) )  =  ( ( RR 
_D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( R [,] X ) ) ) )
253 iccntr 21411 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( R  e.  RR  /\  X  e.  RR )  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( R [,] X ) )  =  ( R (,) X
) )
25457, 85, 253syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( int `  ( topGen `
 ran  (,) )
) `  ( R [,] X ) )  =  ( R (,) X
) )
255254reseq2d 5186 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( RR  _D  F )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( R [,] X ) ) )  =  ( ( RR 
_D  F )  |`  ( R (,) X ) ) )
256252, 255eqtrd 2423 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( RR  _D  ( F  |`  ( R [,] X ) ) )  =  ( ( RR 
_D  F )  |`  ( R (,) X ) ) )
257256dmeqd 5118 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  dom  ( RR  _D  ( F  |`  ( R [,] X ) ) )  =  dom  ( ( RR  _D  F )  |`  ( R (,) X
) ) )
25852, 57, 84ltled 9644 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  A  <_  R )
259 iooss1 11485 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( A  e.  RR*  /\  A  <_  R )  ->  ( R (,) X )  C_  ( A (,) X ) )
26092, 258, 259syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R (,) X
)  C_  ( A (,) X ) )
261104adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  X  <_  D )
262 iooss2 11486 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( D  e.  RR*  /\  X  <_  D )  ->  ( A (,) X )  C_  ( A (,) D ) )
263226, 261, 262syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( A (,) X
)  C_  ( A (,) D ) )
264260, 263sstrd 3427 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R (,) X
)  C_  ( A (,) D ) )
265264, 230sstrd 3427 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R (,) X
)  C_  ( A (,) B ) )
266234adantr 463 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  dom  ( RR  _D  F
)  =  ( A (,) B ) )
267265, 266sseqtr4d 3454 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R (,) X
)  C_  dom  ( RR 
_D  F ) )
268 ssdmres 5207 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( R (,) X ) 
C_  dom  ( RR  _D  F )  <->  dom  ( ( RR  _D  F )  |`  ( R (,) X
) )  =  ( R (,) X ) )
269267, 268sylib 196 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  dom  ( ( RR  _D  F )  |`  ( R (,) X ) )  =  ( R (,) X ) )
270257, 269eqtrd 2423 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  dom  ( RR  _D  ( F  |`  ( R [,] X ) ) )  =  ( R (,) X ) )
271146adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  G : ( A (,) B ) --> CC )
27247, 161dvres 22400 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( RR  C_  CC  /\  G : ( A (,) B ) --> CC )  /\  ( ( A (,) B ) 
C_  RR  /\  ( R [,] X )  C_  RR ) )  ->  ( RR  _D  ( G  |`  ( R [,] X ) ) )  =  ( ( RR  _D  G
)  |`  ( ( int `  ( topGen `  ran  (,) )
) `  ( R [,] X ) ) ) )
273246, 271, 248, 250, 272syl22anc 1227 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( RR  _D  ( G  |`  ( R [,] X ) ) )  =  ( ( RR 
_D  G )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( R [,] X ) ) ) )
274254reseq2d 5186 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( RR  _D  G )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( R [,] X ) ) )  =  ( ( RR 
_D  G )  |`  ( R (,) X ) ) )
275273, 274eqtrd 2423 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( RR  _D  ( G  |`  ( R [,] X ) ) )  =  ( ( RR 
_D  G )  |`  ( R (,) X ) ) )
276275dmeqd 5118 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  dom  ( RR  _D  ( G  |`  ( R [,] X ) ) )  =  dom  ( ( RR  _D  G )  |`  ( R (,) X
) ) )
277148adantr 463 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  dom  ( RR  _D  G
)  =  ( A (,) B ) )
278265, 277sseqtr4d 3454 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R (,) X
)  C_  dom  ( RR 
_D  G ) )
279 ssdmres 5207 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( R (,) X ) 
C_  dom  ( RR  _D  G )  <->  dom  ( ( RR  _D  G )  |`  ( R (,) X
) )  =  ( R (,) X ) )
280278, 279sylib 196 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  dom  ( ( RR  _D  G )  |`  ( R (,) X ) )  =  ( R (,) X ) )
281276, 280eqtrd 2423 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  dom  ( RR  _D  ( G  |`  ( R [,] X ) ) )  =  ( R (,) X ) )
28257, 85, 91, 242, 245, 270, 281cmvth 22477 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  E. w  e.  ( R (,) X ) ( ( ( ( F  |`  ( R [,] X
) ) `  X
)  -  ( ( F  |`  ( R [,] X ) ) `  R ) )  x.  ( ( RR  _D  ( G  |`  ( R [,] X ) ) ) `  w ) )  =  ( ( ( ( G  |`  ( R [,] X ) ) `  X )  -  ( ( G  |`  ( R [,] X
) ) `  R
) )  x.  (
( RR  _D  ( F  |`  ( R [,] X ) ) ) `
 w ) ) )
28357rexrd 9554 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  R  e.  RR* )
284283adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  ->  R  e.  RR* )
28593ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  ->  X  e.  RR* )
28657, 85, 91ltled 9644 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  R  <_  X )
287286adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  ->  R  <_  X )
288 ubicc2 11558 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( R  e.  RR*  /\  X  e.  RR*  /\  R  <_  X )  ->  X  e.  ( R [,] X
) )
289284, 285, 287, 288syl3anc 1226 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  ->  X  e.  ( R [,] X ) )
290 fvres 5788 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( X  e.  ( R [,] X )  ->  (
( F  |`  ( R [,] X ) ) `
 X )  =  ( F `  X
) )
291289, 290syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( F  |`  ( R [,] X ) ) `  X )  =  ( F `  X ) )
292 lbicc2 11557 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( R  e.  RR*  /\  X  e.  RR*  /\  R  <_  X )  ->  R  e.  ( R [,] X
) )
293284, 285, 287, 292syl3anc 1226 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  ->  R  e.  ( R [,] X ) )
294 fvres 5788 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( R  e.  ( R [,] X )  ->  (
( F  |`  ( R [,] X ) ) `
 R )  =  ( F `  R
) )
295293, 294syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( F  |`  ( R [,] X ) ) `  R )  =  ( F `  R ) )
296291, 295oveq12d 6214 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( ( F  |`  ( R [,] X
) ) `  X
)  -  ( ( F  |`  ( R [,] X ) ) `  R ) )  =  ( ( F `  X )  -  ( F `  R )
) )
297275fveq1d 5776 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( RR  _D  ( G  |`  ( R [,] X ) ) ) `  w )  =  ( ( ( RR  _D  G )  |`  ( R (,) X
) ) `  w
) )
298 fvres 5788 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  e.  ( R (,) X )  ->  (
( ( RR  _D  G )  |`  ( R (,) X ) ) `
 w )  =  ( ( RR  _D  G ) `  w
) )
299297, 298sylan9eq 2443 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( RR  _D  ( G  |`  ( R [,] X ) ) ) `  w )  =  ( ( RR 
_D  G ) `  w ) )
300296, 299oveq12d 6214 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( ( ( F  |`  ( R [,] X ) ) `  X )  -  (
( F  |`  ( R [,] X ) ) `
 R ) )  x.  ( ( RR 
_D  ( G  |`  ( R [,] X ) ) ) `  w
) )  =  ( ( ( F `  X )  -  ( F `  R )
)  x.  ( ( RR  _D  G ) `
 w ) ) )
301 fvres 5788 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( X  e.  ( R [,] X )  ->  (
( G  |`  ( R [,] X ) ) `
 X )  =  ( G `  X
) )
302289, 301syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( G  |`  ( R [,] X ) ) `  X )  =  ( G `  X ) )
303 fvres 5788 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( R  e.  ( R [,] X )  ->  (
( G  |`  ( R [,] X ) ) `
 R )  =  ( G `  R
) )
304293, 303syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( G  |`  ( R [,] X ) ) `  R )  =  ( G `  R ) )
305302, 304oveq12d 6214 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( ( G  |`  ( R [,] X
) ) `  X
)  -  ( ( G  |`  ( R [,] X ) ) `  R ) )  =  ( ( G `  X )  -  ( G `  R )
) )
306256fveq1d 5776 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( RR  _D  ( F  |`  ( R [,] X ) ) ) `  w )  =  ( ( ( RR  _D  F )  |`  ( R (,) X
) ) `  w
) )
307 fvres 5788 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w  e.  ( R (,) X )  ->  (
( ( RR  _D  F )  |`  ( R (,) X ) ) `
 w )  =  ( ( RR  _D  F ) `  w
) )
308306, 307sylan9eq 2443 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( RR  _D  ( F  |`  ( R [,] X ) ) ) `  w )  =  ( ( RR 
_D  F ) `  w ) )
309305, 308oveq12d 6214 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( ( ( G  |`  ( R [,] X ) ) `  X )  -  (
( G  |`  ( R [,] X ) ) `
 R ) )  x.  ( ( RR 
_D  ( F  |`  ( R [,] X ) ) ) `  w
) )  =  ( ( ( G `  X )  -  ( G `  R )
)  x.  ( ( RR  _D  F ) `
 w ) ) )
310117adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( G `  X )  -  ( G `  R )
)  e.  CC )
311 dvf 22396 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( RR 
_D  F ) : dom  ( RR  _D  F ) --> CC
312234feq2d 5626 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( ( RR  _D  F ) : dom  ( RR  _D  F
) --> CC  <->  ( RR  _D  F ) : ( A (,) B ) --> CC ) )
313311, 312mpbii 211 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( RR  _D  F
) : ( A (,) B ) --> CC )
314313ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( RR  _D  F
) : ( A (,) B ) --> CC )
315265sselda 3417 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  ->  w  e.  ( A (,) B ) )
316314, 315ffvelrnd 5934 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( RR  _D  F ) `  w
)  e.  CC )
317310, 316mulcomd 9528 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( ( G `
 X )  -  ( G `  R ) )  x.  ( ( RR  _D  F ) `
 w ) )  =  ( ( ( RR  _D  F ) `
 w )  x.  ( ( G `  X )  -  ( G `  R )
) ) )
318309, 317eqtrd 2423 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( ( ( G  |`  ( R [,] X ) ) `  X )  -  (
( G  |`  ( R [,] X ) ) `
 R ) )  x.  ( ( RR 
_D  ( F  |`  ( R [,] X ) ) ) `  w
) )  =  ( ( ( RR  _D  F ) `  w
)  x.  ( ( G `  X )  -  ( G `  R ) ) ) )
319300, 318eqeq12d 2404 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( ( ( ( F  |`  ( R [,] X ) ) `
 X )  -  ( ( F  |`  ( R [,] X ) ) `  R ) )  x.  ( ( RR  _D  ( G  |`  ( R [,] X
) ) ) `  w ) )  =  ( ( ( ( G  |`  ( R [,] X ) ) `  X )  -  (
( G  |`  ( R [,] X ) ) `
 R ) )  x.  ( ( RR 
_D  ( F  |`  ( R [,] X ) ) ) `  w
) )  <->  ( (
( F `  X
)  -  ( F `
 R ) )  x.  ( ( RR 
_D  G ) `  w ) )  =  ( ( ( RR 
_D  F ) `  w )  x.  (
( G `  X
)  -  ( G `
 R ) ) ) ) )
320112adantr 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( F `  X )  -  ( F `  R )
)  e.  CC )
321197ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( RR  _D  G
) : ( A (,) B ) --> CC )
322321, 315ffvelrnd 5934 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( RR  _D  G ) `  w
)  e.  CC )
323220adantr 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( G `  X )  -  ( G `  R )
)  =/=  0 )
324118ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  ->  -.  0  e.  ran  ( RR  _D  G
) )
325321, 199syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( RR  _D  G
)  Fn  ( A (,) B ) )
326325, 315, 203syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( RR  _D  G ) `  w
)  e.  ran  ( RR  _D  G ) )
327 eleq1 2454 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( RR  _D  G
) `  w )  =  0  ->  (
( ( RR  _D  G ) `  w
)  e.  ran  ( RR  _D  G )  <->  0  e.  ran  ( RR  _D  G
) ) )
328326, 327syl5ibcom 220 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( ( RR 
_D  G ) `  w )  =  0  ->  0  e.  ran  ( RR  _D  G
) ) )
329328necon3bd 2594 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( -.  0  e. 
ran  ( RR  _D  G )  ->  (
( RR  _D  G
) `  w )  =/=  0 ) )
330324, 329mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( RR  _D  G ) `  w
)  =/=  0 )
331320, 310, 316, 322, 323, 330divmuleqd 10283 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( ( ( F `  X )  -  ( F `  R ) )  / 
( ( G `  X )  -  ( G `  R )
) )  =  ( ( ( RR  _D  F ) `  w
)  /  ( ( RR  _D  G ) `
 w ) )  <-> 
( ( ( F `
 X )  -  ( F `  R ) )  x.  ( ( RR  _D  G ) `
 w ) )  =  ( ( ( RR  _D  F ) `
 w )  x.  ( ( G `  X )  -  ( G `  R )
) ) ) )
332319, 331bitr4d 256 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( ( ( ( F  |`  ( R [,] X ) ) `
 X )  -  ( ( F  |`  ( R [,] X ) ) `  R ) )  x.  ( ( RR  _D  ( G  |`  ( R [,] X
) ) ) `  w ) )  =  ( ( ( ( G  |`  ( R [,] X ) ) `  X )  -  (
( G  |`  ( R [,] X ) ) `
 R ) )  x.  ( ( RR 
_D  ( F  |`  ( R [,] X ) ) ) `  w
) )  <->  ( (
( F `  X
)  -  ( F `
 R ) )  /  ( ( G `
 X )  -  ( G `  R ) ) )  =  ( ( ( RR  _D  F ) `  w
)  /  ( ( RR  _D  G ) `
 w ) ) ) )
333332rexbidva 2890 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( E. w  e.  ( R (,) X
) ( ( ( ( F  |`  ( R [,] X ) ) `
 X )  -  ( ( F  |`  ( R [,] X ) ) `  R ) )  x.  ( ( RR  _D  ( G  |`  ( R [,] X
) ) ) `  w ) )  =  ( ( ( ( G  |`  ( R [,] X ) ) `  X )  -  (
( G  |`  ( R [,] X ) ) `
 R ) )  x.  ( ( RR 
_D  ( F  |`  ( R [,] X ) ) ) `  w
) )  <->  E. w  e.  ( R (,) X
) ( ( ( F `  X )  -  ( F `  R ) )  / 
( ( G `  X )  -  ( G `  R )
) )  =  ( ( ( RR  _D  F ) `  w
)  /  ( ( RR  _D  G ) `
 w ) ) ) )
334282, 333mpbid 210 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  E. w  e.  ( R (,) X ) ( ( ( F `  X )  -  ( F `  R )
)  /  ( ( G `  X )  -  ( G `  R ) ) )  =  ( ( ( RR  _D  F ) `
 w )  / 
( ( RR  _D  G ) `  w
) ) )
335264sselda 3417 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  ->  w  e.  ( A (,) D ) )
336 lhop1lem.t . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  A. t  e.  ( A (,) D ) ( abs `  (
( ( ( RR 
_D  F ) `  t )  /  (
( RR  _D  G
) `  t )
)  -  C ) )  <  E )
337336ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  ->  A. t  e.  ( A (,) D ) ( abs `  ( ( ( ( RR  _D  F ) `  t
)  /  ( ( RR  _D  G ) `
 t ) )  -  C ) )  <  E )
338 fveq2 5774 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  =  w  ->  (
( RR  _D  F
) `  t )  =  ( ( RR 
_D  F ) `  w ) )
339 fveq2 5774 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  =  w  ->  (
( RR  _D  G
) `  t )  =  ( ( RR 
_D  G ) `  w ) )
340338, 339oveq12d 6214 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( t  =  w  ->  (
( ( RR  _D  F ) `  t
)  /  ( ( RR  _D  G ) `
 t ) )  =  ( ( ( RR  _D  F ) `
 w )  / 
( ( RR  _D  G ) `  w
) ) )
341340oveq1d 6211 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  =  w  ->  (
( ( ( RR 
_D  F ) `  t )  /  (
( RR  _D  G
) `  t )
)  -  C )  =  ( ( ( ( RR  _D  F
) `  w )  /  ( ( RR 
_D  G ) `  w ) )  -  C ) )
342341fveq2d 5778 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  =  w  ->  ( abs `  ( ( ( ( RR  _D  F
) `  t )  /  ( ( RR 
_D  G ) `  t ) )  -  C ) )  =  ( abs `  (
( ( ( RR 
_D  F ) `  w )  /  (
( RR  _D  G
) `  w )
)  -  C ) ) )
343342breq1d 4377 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( t  =  w  ->  (
( abs `  (
( ( ( RR 
_D  F ) `  t )  /  (
( RR  _D  G
) `  t )
)  -  C ) )  <  E  <->  ( abs `  ( ( ( ( RR  _D  F ) `
 w )  / 
( ( RR  _D  G ) `  w
) )  -  C
) )  <  E
) )
344343rspcv 3131 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  ( A (,) D )  ->  ( A. t  e.  ( A (,) D ) ( abs `  ( ( ( ( RR  _D  F ) `  t
)  /  ( ( RR  _D  G ) `
 t ) )  -  C ) )  <  E  ->  ( abs `  ( ( ( ( RR  _D  F
) `  w )  /  ( ( RR 
_D  G ) `  w ) )  -  C ) )  < 
E ) )
345335, 337, 344sylc 60 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( abs `  (
( ( ( RR 
_D  F ) `  w )  /  (
( RR  _D  G
) `  w )
)  -  C ) )  <  E )
346 oveq1 6203 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( F `  X )  -  ( F `  R )
)  /  ( ( G `  X )  -  ( G `  R ) ) )  =  ( ( ( RR  _D  F ) `
 w )  / 
( ( RR  _D  G ) `  w
) )  ->  (
( ( ( F `
 X )  -  ( F `  R ) )  /  ( ( G `  X )  -  ( G `  R ) ) )  -  C )  =  ( ( ( ( RR  _D  F ) `
 w )  / 
( ( RR  _D  G ) `  w
) )  -  C
) )
347346fveq2d 5778 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( F `  X )  -  ( F `  R )
)  /  ( ( G `  X )  -  ( G `  R ) ) )  =  ( ( ( RR  _D  F ) `
 w )  / 
( ( RR  _D  G ) `  w
) )  ->  ( abs `  ( ( ( ( F `  X
)  -  ( F `
 R ) )  /  ( ( G `
 X )  -  ( G `  R ) ) )  -  C
) )  =  ( abs `  ( ( ( ( RR  _D  F ) `  w
)  /  ( ( RR  _D  G ) `
 w ) )  -  C ) ) )
348347breq1d 4377 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( F `  X )  -  ( F `  R )
)  /  ( ( G `  X )  -  ( G `  R ) ) )  =  ( ( ( RR  _D  F ) `
 w )  / 
( ( RR  _D  G ) `  w
) )  ->  (
( abs `  (
( ( ( F `
 X )  -  ( F `  R ) )  /  ( ( G `  X )  -  ( G `  R ) ) )  -  C ) )  <  E  <->  ( abs `  ( ( ( ( RR  _D  F ) `
 w )  / 
( ( RR  _D  G ) `  w
) )  -  C
) )  <  E
) )
349345, 348syl5ibrcom 222 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( ( ( F `  X )  -  ( F `  R ) )  / 
( ( G `  X )  -  ( G `  R )
) )  =  ( ( ( RR  _D  F ) `  w
)  /  ( ( RR  _D  G ) `
 w ) )  ->  ( abs `  (
( ( ( F `
 X )  -  ( F `  R ) )  /  ( ( G `  X )  -  ( G `  R ) ) )  -  C ) )  <  E ) )
350349rexlimdva 2874 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( E. w  e.  ( R (,) X
) ( ( ( F `  X )  -  ( F `  R ) )  / 
( ( G `  X )  -  ( G `  R )
) )  =  ( ( ( RR  _D  F ) `  w
)  /  ( ( RR  _D  G ) `
 w ) )  ->  ( abs `  (
( ( ( F `
 X )  -  ( F `  R ) )  /  ( ( G `  X )  -  ( G `  R ) ) )  -  C ) )  <  E ) )
351334, 350mpd 15 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( abs `  (
( ( ( F `
 X )  -  ( F `  R ) )  /  ( ( G `  X )  -  ( G `  R ) ) )  -  C ) )  <  E )
352224, 225, 351ltled 9644 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( abs `  (
( ( ( F `
 X )  -  ( F `  R ) )  /  ( ( G `  X )  -  ( G `  R ) ) )  -  C ) )  <_  E )
353 fveq2 5774 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( u  =  R  ->  ( F `  u )  =  ( F `  R ) )
354353oveq2d 6212 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( u  =  R  ->  (
( F `  X
)  -  ( F `
 u ) )  =  ( ( F `
 X )  -  ( F `  R ) ) )
355 fveq2 5774 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( u  =  R  ->  ( G `  u )  =  ( G `  R ) )
356355oveq2d 6212 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( u  =  R  ->  (
( G `  X
)  -  ( G `
 u ) )  =  ( ( G `
 X )  -  ( G `  R ) ) )
357354, 356oveq12d 6214 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  =  R  ->  (
( ( F `  X )  -  ( F `  u )
)  /  ( ( G `  X )  -  ( G `  u ) ) )  =  ( ( ( F `  X )  -  ( F `  R ) )  / 
( ( G `  X )  -  ( G `  R )
) ) )
358357oveq1d 6211 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  =  R  ->  (
( ( ( F `
 X )  -  ( F `  u ) )  /  ( ( G `  X )  -  ( G `  u ) ) )  -  C )  =  ( ( ( ( F `  X )  -  ( F `  R ) )  / 
( ( G `  X )  -  ( G `  R )
) )  -  C
) )
359358fveq2d 5778 . . . . . . . . . . . . . . . . . . 19  |-  ( u  =  R  ->  ( abs `  ( ( ( ( F `  X
)  -  ( F `
 u ) )  /  ( ( G `
 X )  -  ( G `  u ) ) )  -  C
) )  =  ( abs `  ( ( ( ( F `  X )  -  ( F `  R )
)  /  ( ( G `  X )  -  ( G `  R ) ) )  -  C ) ) )
360359breq1d 4377 . . . . . . . . . . . . . . . . . 18  |-  ( u  =  R  ->  (
( abs `  (
( ( ( F `
 X )  -  ( F `  u ) )  /  ( ( G `  X )  -  ( G `  u ) ) )  -  C ) )  <_  E  <->  ( abs `  ( ( ( ( F `  X )  -  ( F `  R ) )  / 
( ( G `  X )  -  ( G `  R )
) )  -  C
) )  <_  E
) )
361360rspcev 3135 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e.  ( ( A ( ball `  ( abs  o.  -  ) ) r )  i^i  ( A (,) X ) )  /\  ( abs `  (
( ( ( F `
 X )  -  ( F `  R ) )  /  ( ( G `  X )  -  ( G `  R ) ) )  -  C ) )  <_  E )  ->  E. u  e.  (
( A ( ball `  ( abs  o.  -  ) ) r )  i^i  ( A (,) X ) ) ( abs `  ( ( ( ( F `  X )  -  ( F `  u )
)  /  ( ( G `  X )  -  ( G `  u ) ) )  -  C ) )  <_  E )
36298, 352, 361syl2anc 659 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  E. u  e.  (
( A ( ball `  ( abs  o.  -  ) ) r )  i^i  ( A (,) X ) ) ( abs `  ( ( ( ( F `  X )  -  ( F `  u )
)  /  ( ( G `  X )  -  ( G `  u ) ) )  -  C ) )  <_  E )
363362adantlr 712 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
v  e.  ( TopOpen ` fld )  /\  A  e.  v
) )  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  ->  E. u  e.  (
( A ( ball `  ( abs  o.  -  ) ) r )  i^i  ( A (,) X ) ) ( abs `  ( ( ( ( F `  X )  -  ( F `  u )
)  /  ( ( G `  X )  -  ( G `  u ) ) )  -  C ) )  <_  E )
364 ssrin 3637 . . . . . . . . . . . . . . . . 17  |-  ( ( A ( ball `  ( abs  o.  -  ) ) r )  C_  v  ->  ( ( A (
ball `  ( abs  o. 
-  ) ) r )  i^i  ( A (,) X ) ) 
C_  ( v  i^i  ( A (,) X
) ) )
365 lbioo 11481 . . . . . . . . . . . . . . . . . . . 20  |-  -.  A  e.  ( A (,) X
)
366 disjsn 4004 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( A (,) X
)  i^i  { A } )  =  (/)  <->  -.  A  e.  ( A (,) X ) )
367365, 366mpbir 209 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A (,) X )  i^i  { A }
)  =  (/)
368 disj3 3787 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( A (,) X
)  i^i  { A } )  =  (/)  <->  ( A (,) X )  =  ( ( A (,) X )  \  { A } ) )
369367, 368mpbi 208 . . . . . . . . . . . . . . . . . 18  |-  ( A (,) X )  =  ( ( A (,) X )  \  { A } )
370369ineq2i 3611 . . . . . . . . . . . . . . . . 17  |-  ( v  i^i  ( A (,) X ) )  =  ( v  i^i  (
( A (,) X
)  \  { A } ) )
371364, 370syl6sseq 3463 . . . . . . . . . . . . . . . 16  |-  ( ( A ( ball `  ( abs  o.  -  ) ) r )  C_  v  ->  ( ( A (
ball `  ( abs  o. 
-  ) ) r )  i^i  ( A (,) X ) ) 
C_  ( v  i^i  ( ( A (,) X )  \  { A } ) ) )
372 ssrexv 3479 . . . . . . . . . . . . . . . 16  |-  ( ( ( A ( ball `  ( abs  o.  -  ) ) r )  i^i  ( A (,) X ) )  C_  ( v  i^i  (
( A (,) X
)  \  { A } ) )  -> 
( E. u  e.  ( ( A (
ball `  ( abs  o. 
-  ) ) r )  i^i  ( A (,) X ) ) ( abs `  (
( ( ( F `
 X )  -  ( F `  u ) )  /  ( ( G `  X )  -  ( G `  u ) ) )  -  C ) )  <_  E  ->  E. u  e.  ( v  i^i  (
( A (,) X
)  \  { A } ) ) ( abs `  ( ( ( ( F `  X )  -  ( F `  u )
)  /  ( ( G `  X )  -  ( G `  u ) ) )  -  C ) )  <_  E ) )
373371, 372syl 16 . . . . . . . . . . . . . . 15  |-  ( ( A ( ball `  ( abs  o.  -  ) ) r )  C_  v  ->  ( E. u  e.  ( ( A (
ball `  ( abs  o. 
-  ) ) r )  i^i  ( A (,) X ) ) ( abs `  (
( ( ( F `
 X )  -  ( F `  u ) )  /  ( ( G `  X )  -  ( G `  u ) ) )  -  C ) )  <_  E  ->  E. u  e.  ( v  i^i  (
( A (,) X
)  \  { A } ) ) ( abs `  ( ( ( ( F `  X )  -  ( F `  u )
)  /  ( ( G `  X )  -  ( G `  u ) ) )  -  C ) )  <_  E ) )
374363, 373syl5com 30 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
v  e.  ( TopOpen ` fld )  /\  A  e.  v
) )  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  -> 
( ( A (
ball `  ( abs  o. 
-  ) ) r )  C_  v  ->  E. u  e.  ( v  i^i  ( ( A (,) X )  \  { A } ) ) ( abs `  (
( ( ( F `
 X )  -  ( F `  u ) )  /  ( ( G `  X )  -  ( G `  u ) ) )  -  C ) )  <_  E ) )
375374anassrs 646 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( v  e.  (
TopOpen ` fld )  /\  A  e.  v ) )  /\  r  e.  RR+ )  /\  r  <  ( X  -  A ) )  -> 
( ( A (
ball `  ( abs  o. 
-  ) ) r )  C_  v  ->  E. u  e.  ( v  i^i  ( ( A (,) X )  \  { A } ) ) ( abs `  (
( ( ( F `
 X )  -  ( F `  u ) )  /  ( ( G `  X )  -  ( G `  u ) ) )  -  C ) )  <_  E ) )
376375expimpd 601 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
v  e.  ( TopOpen ` fld )  /\  A  e.  v
) )  /\  r  e.  RR+ )  ->  (
( r  <  ( X  -  A )  /\  ( A ( ball `  ( abs  o.  -  ) ) r ) 
C_  v )  ->  E. u  e.  (
v  i^i  ( ( A (,) X )  \  { A } ) ) ( abs `  (
( ( ( F `
 X )  -  ( F `  u ) )  /  ( ( G `  X )  -  ( G `  u ) ) )  -  C ) )  <_  E ) )
377376rexlimdva 2874 . . . . . . . . . . 11  |-  ( (
ph  /\  ( v  e.  ( TopOpen ` fld )  /\  A  e.  v ) )  -> 
( E. r  e.  RR+  ( r  <  ( X  -  A )  /\  ( A ( ball `  ( abs  o.  -  ) ) r ) 
C_  v )  ->  E. u  e.  (
v  i^i  ( ( A (,) X )  \  { A } ) ) ( abs `  (
( ( ( F `
 X )  -  ( F `  u ) )  /  ( ( G `  X )  -  ( G `  u ) ) )  -  C ) )  <_  E ) )
37850, 377mpd 15 . . . . . . . . . 10  |-  ( (
ph  /\  ( v  e.  ( TopOpen ` fld )  /\  A  e.  v ) )  ->  E. u  e.  (
v  i^i  ( ( A (,) X )  \  { A } ) ) ( abs `  (
( ( ( F `
 X )  -  ( F `  u ) )  /  ( ( G `  X )  -  ( G `  u ) ) )  -  C ) )  <_  E )
379 inss2 3633 . . . . . . . . . . . . . 14  |-  ( v  i^i  ( ( A (,) X )  \  { A } ) ) 
C_  ( ( A (,) X )  \  { A } )
380 difss 3545 . . . . . . . . . . . . . 14  |-  ( ( A (,) X ) 
\  { A }
)  C_  ( A (,) X )
381379, 380sstri 3426 . . . . . . . . . . . . 13  |-  ( v  i^i  ( ( A (,) X )  \  { A } ) ) 
C_  ( A (,) X )
382381sseli 3413 . . . . . . . . . . . 12  |-  ( u  e.  ( v  i^i  ( ( A (,) X )  \  { A } ) )  ->  u  e.  ( A (,) X ) )
383 fveq2 5774 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  u  ->  ( F `  z )  =  ( F `  u ) )
384383oveq2d 6212 . . . . . . . . . . . . . . . . 17  |-  ( z  =  u  ->  (
( F `  X
)  -  ( F `
 z ) )  =  ( ( F `
 X )  -  ( F `  u ) ) )
385 fveq2 5774 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  u  ->  ( G `  z )  =  ( G `  u ) )
386385oveq2d 6212 . . . . . . . . . . . . . . . . 17  |-  ( z  =  u  ->  (
( G `  X
)  -  ( G `
 z ) )  =  ( ( G `
 X )  -  ( G `  u ) ) )
387384, 386oveq12d 6214 . . . . . . . . . . . . . . . 16  |-  ( z  =  u  ->  (
( ( F `  X )  -  ( F `  z )
)  /  ( ( G `  X )  -  ( G `  z ) ) )  =  ( ( ( F `  X )  -  ( F `  u ) )  / 
( ( G `  X )  -  ( G `  u )
) ) )
388 eqid 2382 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( A (,) X )  |->  ( ( ( F `  X
)  -  ( F `
 z ) )  /  ( ( G `
 X )  -  ( G `  z ) ) ) )  =  ( z  e.  ( A (,) X ) 
|->  ( ( ( F `
 X )  -  ( F `  z ) )  /  ( ( G `  X )  -  ( G `  z ) ) ) )
389 ovex 6224 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  X
)  -  ( F `
 u ) )  /  ( ( G `
 X )  -  ( G `  u ) ) )  e.  _V
390387, 388, 389fvmpt 5857 . . . . . . . . . . . . . . 15  |-  ( u  e.  ( A (,) X )  ->  (
( z  e.  ( A (,) X ) 
|->  ( ( ( F `
 X )  -  ( F `  z ) )  /  ( ( G `  X )  -  ( G `  z ) ) ) ) `  u )  =  ( ( ( F `  X )  -  ( F `  u ) )  / 
( ( G `  X )  -  ( G `  u )
) ) )
391390oveq1d 6211 . . . . . . . . . . . . . 14  |-  ( u  e.  ( A (,) X )  ->  (
( ( z  e.  ( A (,) X
)