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

Theorem lhop1lem 19360
Description: Lemma for lhop1 19361. (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 10692 . . . . . . . . 9  |-  ( ( B  e.  RR*  /\  D  <_  B )  ->  ( A (,) D )  C_  ( A (,) B ) )
52, 3, 4syl2anc 642 . . . . . . . 8  |-  ( ph  ->  ( A (,) D
)  C_  ( A (,) B ) )
6 lhop1lem.x . . . . . . . 8  |-  ( ph  ->  X  e.  ( A (,) D ) )
75, 6sseldd 3181 . . . . . . 7  |-  ( ph  ->  X  e.  ( A (,) B ) )
81, 7ffvelrnd 5666 . . . . . 6  |-  ( ph  ->  ( F `  X
)  e.  RR )
98recnd 8861 . . . . 5  |-  ( ph  ->  ( F `  X
)  e.  CC )
10 lhop1.g . . . . . . 7  |-  ( ph  ->  G : ( A (,) B ) --> RR )
1110, 7ffvelrnd 5666 . . . . . 6  |-  ( ph  ->  ( G `  X
)  e.  RR )
1211recnd 8861 . . . . 5  |-  ( ph  ->  ( G `  X
)  e.  CC )
13 lhop1.gn0 . . . . . 6  |-  ( ph  ->  -.  0  e.  ran  G )
14 ffn 5389 . . . . . . . . . 10  |-  ( G : ( A (,) B ) --> RR  ->  G  Fn  ( A (,) B ) )
1510, 14syl 15 . . . . . . . . 9  |-  ( ph  ->  G  Fn  ( A (,) B ) )
16 fnfvelrn 5662 . . . . . . . . 9  |-  ( ( G  Fn  ( A (,) B )  /\  X  e.  ( A (,) B ) )  -> 
( G `  X
)  e.  ran  G
)
1715, 7, 16syl2anc 642 . . . . . . . 8  |-  ( ph  ->  ( G `  X
)  e.  ran  G
)
18 eleq1 2343 . . . . . . . 8  |-  ( ( G `  X )  =  0  ->  (
( G `  X
)  e.  ran  G  <->  0  e.  ran  G ) )
1917, 18syl5ibcom 211 . . . . . . 7  |-  ( ph  ->  ( ( G `  X )  =  0  ->  0  e.  ran  G ) )
2019necon3bd 2483 . . . . . 6  |-  ( ph  ->  ( -.  0  e. 
ran  G  ->  ( G `
 X )  =/=  0 ) )
2113, 20mpd 14 . . . . 5  |-  ( ph  ->  ( G `  X
)  =/=  0 )
229, 12, 21divcld 9536 . . . 4  |-  ( ph  ->  ( ( F `  X )  /  ( G `  X )
)  e.  CC )
23 limccl 19225 . . . . 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 3178 . . . 4  |-  ( ph  ->  C  e.  CC )
2622, 25subcld 9157 . . 3  |-  ( ph  ->  ( ( ( F `
 X )  / 
( G `  X
) )  -  C
)  e.  CC )
2726abscld 11918 . 2  |-  ( ph  ->  ( abs `  (
( ( F `  X )  /  ( G `  X )
)  -  C ) )  e.  RR )
28 lhop1lem.e . . 3  |-  ( ph  ->  E  e.  RR+ )
2928rpred 10390 . 2  |-  ( ph  ->  E  e.  RR )
30 2re 9815 . . . 4  |-  2  e.  RR
3130a1i 10 . . 3  |-  ( ph  ->  2  e.  RR )
3231, 29remulcld 8863 . 2  |-  ( ph  ->  ( 2  x.  E
)  e.  RR )
33 cnxmet 18282 . . . . . . . . . . . . 13  |-  ( abs 
o.  -  )  e.  ( * Met `  CC )
3433a1i 10 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( v  e.  ( TopOpen ` fld )  /\  A  e.  v ) )  -> 
( abs  o.  -  )  e.  ( * Met `  CC ) )
35 simprl 732 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( v  e.  ( TopOpen ` fld )  /\  A  e.  v ) )  -> 
v  e.  ( TopOpen ` fld )
)
36 simprr 733 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( v  e.  ( TopOpen ` fld )  /\  A  e.  v ) )  ->  A  e.  v )
37 eliooord 10710 . . . . . . . . . . . . . . . 16  |-  ( X  e.  ( A (,) D )  ->  ( A  <  X  /\  X  <  D ) )
386, 37syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( A  <  X  /\  X  <  D ) )
3938simpld 445 . . . . . . . . . . . . . 14  |-  ( ph  ->  A  <  X )
40 lhop1.a . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  e.  RR )
41 ioossre 10712 . . . . . . . . . . . . . . . 16  |-  ( A (,) D )  C_  RR
4241, 6sseldi 3178 . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  e.  RR )
43 difrp 10387 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  RR  /\  X  e.  RR )  ->  ( A  <  X  <->  ( X  -  A )  e.  RR+ ) )
4440, 42, 43syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A  <  X  <->  ( X  -  A )  e.  RR+ ) )
4539, 44mpbid 201 . . . . . . . . . . . . 13  |-  ( ph  ->  ( X  -  A
)  e.  RR+ )
4645adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( v  e.  ( TopOpen ` fld )  /\  A  e.  v ) )  -> 
( X  -  A
)  e.  RR+ )
47 eqid 2283 . . . . . . . . . . . . . 14  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
4847cnfldtopn 18291 . . . . . . . . . . . . 13  |-  ( TopOpen ` fld )  =  ( MetOpen `  ( abs  o.  -  ) )
4948mopni3 18040 . . . . . . . . . . . 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 1185 . . . . . . . . . . 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 451 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  A  e.  RR )
53 simprl 732 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
r  e.  RR+ )
5453rpred 10390 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
r  e.  RR )
5554rehalfcld 9958 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( r  /  2
)  e.  RR )
5652, 55readdcld 8862 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( A  +  ( r  /  2 ) )  e.  RR )
5751, 56syl5eqel 2367 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  R  e.  RR )
5857recnd 8861 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  R  e.  CC )
5940recnd 8861 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  A  e.  CC )
6059adantr 451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  A  e.  CC )
61 eqid 2283 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( abs 
o.  -  )  =  ( abs  o.  -  )
6261cnmetdval 18280 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R  e.  CC  /\  A  e.  CC )  ->  ( R ( abs 
o.  -  ) A
)  =  ( abs `  ( R  -  A
) ) )
6358, 60, 62syl2anc 642 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R ( abs 
o.  -  ) A
)  =  ( abs `  ( R  -  A
) ) )
6451oveq1i 5868 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( R  -  A )  =  ( ( A  +  ( r  /  2
) )  -  A
)
6554recnd 8861 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
r  e.  CC )
6665halfcld 9956 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( r  /  2
)  e.  CC )
6760, 66pncan2d 9159 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( A  +  ( r  /  2
) )  -  A
)  =  ( r  /  2 ) )
6864, 67syl5eq 2327 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R  -  A
)  =  ( r  /  2 ) )
6968fveq2d 5529 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( abs `  ( R  -  A )
)  =  ( abs `  ( r  /  2
) ) )
7053rphalfcld 10402 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( r  /  2
)  e.  RR+ )
7170rpred 10390 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( r  /  2
)  e.  RR )
7270rpge0d 10394 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
0  <_  ( r  /  2 ) )
7371, 72absidd 11905 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( abs `  (
r  /  2 ) )  =  ( r  /  2 ) )
7463, 69, 733eqtrd 2319 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R ( abs 
o.  -  ) A
)  =  ( r  /  2 ) )
75 rphalflt 10380 . . . . . . . . . . . . . . . . . . . . 21  |-  ( r  e.  RR+  ->  ( r  /  2 )  < 
r )
7653, 75syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( r  /  2
)  <  r )
7774, 76eqbrtrd 4043 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R ( abs 
o.  -  ) A
)  <  r )
7833a1i 10 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( abs  o.  -  )  e.  ( * Met `  CC ) )
7954rexrd 8881 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
r  e.  RR* )
80 elbl3 17951 . . . . . . . . . . . . . . . . . . . 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 1183 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R  e.  ( A ( ball `  ( abs  o.  -  ) ) r )  <->  ( R
( abs  o.  -  ) A )  <  r
) )
8277, 81mpbird 223 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  R  e.  ( A
( ball `  ( abs  o. 
-  ) ) r ) )
8352, 70ltaddrpd 10419 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  A  <  ( A  +  ( r  /  2
) ) )
8483, 51syl6breqr 4063 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  A  <  R )
8542adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  X  e.  RR )
8685, 52resubcld 9211 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( X  -  A
)  e.  RR )
87 simprr 733 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
r  <  ( X  -  A ) )
8871, 54, 86, 76, 87lttrd 8977 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( r  /  2
)  <  ( X  -  A ) )
8952, 71, 85ltaddsub2d 9373 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( A  +  ( r  /  2
) )  <  X  <->  ( r  /  2 )  <  ( X  -  A ) ) )
9088, 89mpbird 223 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( A  +  ( r  /  2 ) )  <  X )
9151, 90syl5eqbr 4056 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  R  <  X )
9252rexrd 8881 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  A  e.  RR* )
9342rexrd 8881 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  X  e.  RR* )
9493adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  X  e.  RR* )
95 elioo2 10697 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  RR*  /\  X  e.  RR* )  ->  ( R  e.  ( A (,) X )  <->  ( R  e.  RR  /\  A  < 
R  /\  R  <  X ) ) )
9692, 94, 95syl2anc 642 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R  e.  ( A (,) X )  <-> 
( R  e.  RR  /\  A  <  R  /\  R  <  X ) ) )
9757, 84, 91, 96mpbir3and 1135 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  R  e.  ( A (,) X ) )
98 elin 3358 . . . . . . . . . . . . . . . . . 18  |-  ( R  e.  ( ( A ( ball `  ( abs  o.  -  ) ) r )  i^i  ( A (,) X ) )  <-> 
( R  e.  ( A ( ball `  ( abs  o.  -  ) ) r )  /\  R  e.  ( A (,) X
) ) )
9982, 97, 98sylanbrc 645 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  R  e.  ( ( A ( ball `  ( abs  o.  -  ) ) r )  i^i  ( A (,) X ) ) )
1009adantr 451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( F `  X
)  e.  CC )
1011adantr 451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  F : ( A (,) B ) --> RR )
102 lhop1lem.d . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  D  e.  RR )
103102rexrd 8881 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  D  e.  RR* )
10438simprd 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  X  <  D )
10542, 102, 104ltled 8967 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  X  <_  D )
10693, 103, 2, 105, 3xrletrd 10493 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  X  <_  B )
107 iooss2 10692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( B  e.  RR*  /\  X  <_  B )  ->  ( A (,) X )  C_  ( A (,) B ) )
1082, 106, 107syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( A (,) X
)  C_  ( A (,) B ) )
109108adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( A (,) X
)  C_  ( A (,) B ) )
110109, 97sseldd 3181 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  R  e.  ( A (,) B ) )
111101, 110ffvelrnd 5666 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( F `  R
)  e.  RR )
112111recnd 8861 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( F `  R
)  e.  CC )
113100, 112subcld 9157 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( F `  X )  -  ( F `  R )
)  e.  CC )
11412adantr 451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( G `  X
)  e.  CC )
11510adantr 451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  G : ( A (,) B ) --> RR )
116115, 110ffvelrnd 5666 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( G `  R
)  e.  RR )
117116recnd 8861 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( G `  R
)  e.  CC )
118114, 117subcld 9157 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( G `  X )  -  ( G `  R )
)  e.  CC )
119 lhop1.gd0 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  -.  0  e.  ran  ( RR  _D  G
) )
120119adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  -.  0  e.  ran  ( RR  _D  G ) )
12112adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( G `  X )  e.  CC )
122108sselda 3180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  z  e.  ( A (,) B ) )
12310ffvelrnda 5665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  z  e.  ( A (,) B ) )  ->  ( G `  z )  e.  RR )
124122, 123syldan 456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( G `  z )  e.  RR )
125124recnd 8861 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( G `  z )  e.  CC )
126 subeq0 9073 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( G `  X
)  e.  CC  /\  ( G `  z )  e.  CC )  -> 
( ( ( G `
 X )  -  ( G `  z ) )  =  0  <->  ( G `  X )  =  ( G `  z ) ) )
127121, 125, 126syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( (
( G `  X
)  -  ( G `
 z ) )  =  0  <->  ( G `  X )  =  ( G `  z ) ) )
128 ioossre 10712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( A (,) B )  C_  RR
129128, 122sseldi 3178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  z  e.  RR )
130129adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
z  e.  RR )
13142ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  ->  X  e.  RR )
132 eliooord 10710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z  e.  ( A (,) X )  ->  ( A  <  z  /\  z  <  X ) )
133132adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( A  <  z  /\  z  < 
X ) )
134133simprd 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  z  <  X )
135134adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
z  <  X )
13640rexrd 8881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  A  e.  RR* )
137136adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  A  e.  RR* )
1382adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  B  e.  RR* )
139133simpld 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  A  <  z )
14093, 103, 2, 104, 3xrltletrd 10492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  X  <  B )
141140adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  X  <  B )
142 iccssioo 10719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <  z  /\  X  <  B ) )  ->  ( z [,] X )  C_  ( A (,) B ) )
143137, 138, 139, 141, 142syl22anc 1183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( z [,] X )  C_  ( A (,) B ) )
144143adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( z [,] X
)  C_  ( A (,) B ) )
145 ax-resscn 8794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  RR  C_  CC
146145a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  RR  C_  CC )
147 fss 5397 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( G : ( A (,) B ) --> RR 
/\  RR  C_  CC )  ->  G : ( A (,) B ) --> CC )
14810, 145, 147sylancl 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  G : ( A (,) B ) --> CC )
149128a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  ( A (,) B
)  C_  RR )
150 lhop1.ig . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  dom  ( RR  _D  G )  =  ( A (,) B ) )
151 dvcn 19270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( RR  C_  CC  /\  G : ( A (,) B ) --> CC 
/\  ( A (,) B )  C_  RR )  /\  dom  ( RR 
_D  G )  =  ( A (,) B
) )  ->  G  e.  ( ( A (,) B ) -cn-> CC ) )
152146, 148, 149, 150, 151syl31anc 1185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  G  e.  ( ( A (,) B )
-cn-> CC ) )
153 cncffvrn 18402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( RR  C_  CC  /\  G  e.  ( ( A (,) B ) -cn-> CC ) )  ->  ( G  e.  ( ( A (,) B ) -cn-> RR )  <-> 
G : ( A (,) B ) --> RR ) )
154145, 152, 153sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  ( G  e.  ( ( A (,) B
) -cn-> RR )  <->  G :
( A (,) B
) --> RR ) )
15510, 154mpbird 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  G  e.  ( ( A (,) B )
-cn-> RR ) )
156155ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  ->  G  e.  ( ( A (,) B ) -cn-> RR ) )
157 rescncf 18401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( z [,] X ) 
C_  ( A (,) B )  ->  ( G  e.  ( ( A (,) B ) -cn-> RR )  ->  ( G  |`  ( z [,] X
) )  e.  ( ( z [,] X
) -cn-> RR ) ) )
158144, 156, 157sylc 56 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( G  |`  (
z [,] X ) )  e.  ( ( z [,] X )
-cn-> RR ) )
159145a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  ->  RR  C_  CC )
160148ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  ->  G : ( A (,) B ) --> CC )
161128a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( A (,) B
)  C_  RR )
162144, 128syl6ss 3191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( z [,] X
)  C_  RR )
16347tgioo2 18309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
16447, 163dvres 19261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
165159, 160, 161, 162, 164syl22anc 1183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( RR  _D  ( G  |`  ( z [,] X ) ) )  =  ( ( RR 
_D  G )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( z [,] X ) ) ) )
166 iccntr 18326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( z  e.  RR  /\  X  e.  RR )  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( z [,] X ) )  =  ( z (,) X
) )
167130, 131, 166syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( ( int `  ( topGen `
 ran  (,) )
) `  ( z [,] X ) )  =  ( z (,) X
) )
168167reseq2d 4955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( ( RR  _D  G )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( z [,] X ) ) )  =  ( ( RR 
_D  G )  |`  ( z (,) X
) ) )
169165, 168eqtrd 2315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( RR  _D  ( G  |`  ( z [,] X ) ) )  =  ( ( RR 
_D  G )  |`  ( z (,) X
) ) )
170169dmeqd 4881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  ->  dom  ( RR  _D  ( G  |`  ( z [,] X ) ) )  =  dom  ( ( RR  _D  G )  |`  ( z (,) X
) ) )
171 ioossicc 10735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( z (,) X )  C_  ( z [,] X
)
172171, 144syl5ss 3190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( z (,) X
)  C_  ( A (,) B ) )
173150ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  ->  dom  ( RR  _D  G
)  =  ( A (,) B ) )
174172, 173sseqtr4d 3215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( z (,) X
)  C_  dom  ( RR 
_D  G ) )
175 ssdmres 4977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( z (,) X ) 
C_  dom  ( RR  _D  G )  <->  dom  ( ( RR  _D  G )  |`  ( z (,) X
) )  =  ( z (,) X ) )
176174, 175sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  ->  dom  ( ( RR  _D  G )  |`  (
z (,) X ) )  =  ( z (,) X ) )
177170, 176eqtrd 2315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  ->  dom  ( RR  _D  ( G  |`  ( z [,] X ) ) )  =  ( z (,) X ) )
178129rexrd 8881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  z  e.  RR* )
17993adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  X  e.  RR* )
18042adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  X  e.  RR )
181129, 180, 134ltled 8967 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  z  <_  X )
182 ubicc2 10753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( z  e.  RR*  /\  X  e.  RR*  /\  z  <_  X )  ->  X  e.  ( z [,] X
) )
183178, 179, 181, 182syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  X  e.  ( z [,] X
) )
184 fvres 5542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( X  e.  ( z [,] X )  ->  (
( G  |`  (
z [,] X ) ) `  X )  =  ( G `  X ) )
185183, 184syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( ( G  |`  ( z [,] X ) ) `  X )  =  ( G `  X ) )
186 lbicc2 10752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( z  e.  RR*  /\  X  e.  RR*  /\  z  <_  X )  ->  z  e.  ( z [,] X
) )
187178, 179, 181, 186syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  z  e.  ( z [,] X
) )
188 fvres 5542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( z  e.  ( z [,] X )  ->  (
( G  |`  (
z [,] X ) ) `  z )  =  ( G `  z ) )
189187, 188syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( ( G  |`  ( z [,] X ) ) `  z )  =  ( G `  z ) )
190185, 189eqeq12d 2297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( (
( G  |`  (
z [,] X ) ) `  X )  =  ( ( G  |`  ( z [,] X
) ) `  z
)  <->  ( G `  X )  =  ( G `  z ) ) )
191190biimpar 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( ( G  |`  ( z [,] X
) ) `  X
)  =  ( ( G  |`  ( z [,] X ) ) `  z ) )
192191eqcomd 2288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( ( G  |`  ( z [,] X
) ) `  z
)  =  ( ( G  |`  ( z [,] X ) ) `  X ) )
193130, 131, 135, 158, 177, 192rolle 19337 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  ->  E. w  e.  (
z (,) X ) ( ( RR  _D  ( G  |`  ( z [,] X ) ) ) `  w )  =  0 )
194169fveq1d 5527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( ( RR  _D  ( G  |`  ( z [,] X ) ) ) `  w )  =  ( ( ( RR  _D  G )  |`  ( z (,) X
) ) `  w
) )
195 fvres 5542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( w  e.  ( z (,) X )  ->  (
( ( RR  _D  G )  |`  (
z (,) X ) ) `  w )  =  ( ( RR 
_D  G ) `  w ) )
196194, 195sylan9eq 2335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  z  e.  ( A (,) X ) )  /\  ( G `  X )  =  ( G `  z ) )  /\  w  e.  ( z (,) X ) )  -> 
( ( RR  _D  ( G  |`  ( z [,] X ) ) ) `  w )  =  ( ( RR 
_D  G ) `  w ) )
197 dvf 19257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( RR 
_D  G ) : dom  ( RR  _D  G ) --> CC
198150feq2d 5380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  ( ( RR  _D  G ) : dom  ( RR  _D  G
) --> CC  <->  ( RR  _D  G ) : ( A (,) B ) --> CC ) )
199197, 198mpbii 202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  ( RR  _D  G
) : ( A (,) B ) --> CC )
200199ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( RR  _D  G
) : ( A (,) B ) --> CC )
201 ffn 5389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( RR  _D  G ) : ( A (,) B ) --> CC  ->  ( RR  _D  G )  Fn  ( A (,) B ) )
202200, 201syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( RR  _D  G
)  Fn  ( A (,) B ) )
203202adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  z  e.  ( A (,) X ) )  /\  ( G `  X )  =  ( G `  z ) )  /\  w  e.  ( z (,) X ) )  -> 
( RR  _D  G
)  Fn  ( A (,) B ) )
204172sselda 3180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  z  e.  ( A (,) X ) )  /\  ( G `  X )  =  ( G `  z ) )  /\  w  e.  ( z (,) X ) )  ->  w  e.  ( A (,) B ) )
205 fnfvelrn 5662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( RR  _D  G
)  Fn  ( A (,) B )  /\  w  e.  ( A (,) B ) )  -> 
( ( RR  _D  G ) `  w
)  e.  ran  ( RR  _D  G ) )
206203, 204, 205syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  z  e.  ( A (,) X ) )  /\  ( G `  X )  =  ( G `  z ) )  /\  w  e.  ( z (,) X ) )  -> 
( ( RR  _D  G ) `  w
)  e.  ran  ( RR  _D  G ) )
207196, 206eqeltrd 2357 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
208 eleq1 2343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
209207, 208syl5ibcom 211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
210209rexlimdva 2667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
211193, 210mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
0  e.  ran  ( RR  _D  G ) )
212211ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( ( G `  X )  =  ( G `  z )  ->  0  e.  ran  ( RR  _D  G ) ) )
213127, 212sylbid 206 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( (
( G `  X
)  -  ( G `
 z ) )  =  0  ->  0  e.  ran  ( RR  _D  G ) ) )
214213necon3bd 2483 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( -.  0  e.  ran  ( RR 
_D  G )  -> 
( ( G `  X )  -  ( G `  z )
)  =/=  0 ) )
215120, 214mpd 14 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( ( G `  X )  -  ( G `  z ) )  =/=  0 )
216215ralrimiva 2626 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  A. z  e.  ( A (,) X ) ( ( G `  X )  -  ( G `  z )
)  =/=  0 )
217216adantr 451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  A. z  e.  ( A (,) X ) ( ( G `  X
)  -  ( G `
 z ) )  =/=  0 )
218 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  =  R  ->  ( G `  z )  =  ( G `  R ) )
219218oveq2d 5874 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( z  =  R  ->  (
( G `  X
)  -  ( G `
 z ) )  =  ( ( G `
 X )  -  ( G `  R ) ) )
220219neeq1d 2459 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  =  R  ->  (
( ( G `  X )  -  ( G `  z )
)  =/=  0  <->  (
( G `  X
)  -  ( G `
 R ) )  =/=  0 ) )
221220rspcv 2880 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( R  e.  ( A (,) X )  ->  ( A. z  e.  ( A (,) X ) ( ( G `  X
)  -  ( G `
 z ) )  =/=  0  ->  (
( G `  X
)  -  ( G `
 R ) )  =/=  0 ) )
22297, 217, 221sylc 56 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( G `  X )  -  ( G `  R )
)  =/=  0 )
223113, 118, 222divcld 9536 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( ( F `
 X )  -  ( F `  R ) )  /  ( ( G `  X )  -  ( G `  R ) ) )  e.  CC )
22425adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  C  e.  CC )
225223, 224subcld 9157 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( ( ( F `  X )  -  ( F `  R ) )  / 
( ( G `  X )  -  ( G `  R )
) )  -  C
)  e.  CC )
226225abscld 11918 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( abs `  (
( ( ( F `
 X )  -  ( F `  R ) )  /  ( ( G `  X )  -  ( G `  R ) ) )  -  C ) )  e.  RR )
22729adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  E  e.  RR )
228103adantr 451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  D  e.  RR* )
229104adantr 451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  X  <  D )
230 iccssioo 10719 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( A  e.  RR*  /\  D  e.  RR* )  /\  ( A  <  R  /\  X  <  D ) )  ->  ( R [,] X )  C_  ( A (,) D ) )
23192, 228, 84, 229, 230syl22anc 1183 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R [,] X
)  C_  ( A (,) D ) )
2325adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( A (,) D
)  C_  ( A (,) B ) )
233231, 232sstrd 3189 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R [,] X
)  C_  ( A (,) B ) )
234 fss 5397 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( F : ( A (,) B ) --> RR 
/\  RR  C_  CC )  ->  F : ( A (,) B ) --> CC )
2351, 145, 234sylancl 643 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  F : ( A (,) B ) --> CC )
236 lhop1.if . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  dom  ( RR  _D  F )  =  ( A (,) B ) )
237 dvcn 19270 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( RR  C_  CC  /\  F : ( A (,) B ) --> CC 
/\  ( A (,) B )  C_  RR )  /\  dom  ( RR 
_D  F )  =  ( A (,) B
) )  ->  F  e.  ( ( A (,) B ) -cn-> CC ) )
238146, 235, 149, 236, 237syl31anc 1185 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  F  e.  ( ( A (,) B )
-cn-> CC ) )
239 cncffvrn 18402 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( RR  C_  CC  /\  F  e.  ( ( A (,) B ) -cn-> CC ) )  ->  ( F  e.  ( ( A (,) B ) -cn-> RR )  <-> 
F : ( A (,) B ) --> RR ) )
240145, 238, 239sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( F  e.  ( ( A (,) B
) -cn-> RR )  <->  F :
( A (,) B
) --> RR ) )
2411, 240mpbird 223 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  F  e.  ( ( A (,) B )
-cn-> RR ) )
242241adantr 451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  F  e.  ( ( A (,) B ) -cn-> RR ) )
243 rescncf 18401 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R [,] X ) 
C_  ( A (,) B )  ->  ( F  e.  ( ( A (,) B ) -cn-> RR )  ->  ( F  |`  ( R [,] X
) )  e.  ( ( R [,] X
) -cn-> RR ) ) )
244233, 242, 243sylc 56 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( F  |`  ( R [,] X ) )  e.  ( ( R [,] X ) -cn-> RR ) )
245155adantr 451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  G  e.  ( ( A (,) B ) -cn-> RR ) )
246 rescncf 18401 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R [,] X ) 
C_  ( A (,) B )  ->  ( G  e.  ( ( A (,) B ) -cn-> RR )  ->  ( G  |`  ( R [,] X
) )  e.  ( ( R [,] X
) -cn-> RR ) ) )
247233, 245, 246sylc 56 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( G  |`  ( R [,] X ) )  e.  ( ( R [,] X ) -cn-> RR ) )
248145a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  RR  C_  CC )
249235adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  F : ( A (,) B ) --> CC )
250128a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( A (,) B
)  C_  RR )
251 iccssre 10731 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( R  e.  RR  /\  X  e.  RR )  ->  ( R [,] X
)  C_  RR )
25257, 85, 251syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R [,] X
)  C_  RR )
25347, 163dvres 19261 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
254248, 249, 250, 252, 253syl22anc 1183 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( RR  _D  ( F  |`  ( R [,] X ) ) )  =  ( ( RR 
_D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( R [,] X ) ) ) )
255 iccntr 18326 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( R  e.  RR  /\  X  e.  RR )  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( R [,] X ) )  =  ( R (,) X
) )
25657, 85, 255syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( int `  ( topGen `
 ran  (,) )
) `  ( R [,] X ) )  =  ( R (,) X
) )
257256reseq2d 4955 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( RR  _D  F )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( R [,] X ) ) )  =  ( ( RR 
_D  F )  |`  ( R (,) X ) ) )
258254, 257eqtrd 2315 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( RR  _D  ( F  |`  ( R [,] X ) ) )  =  ( ( RR 
_D  F )  |`  ( R (,) X ) ) )
259258dmeqd 4881 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  dom  ( RR  _D  ( F  |`  ( R [,] X ) ) )  =  dom  ( ( RR  _D  F )  |`  ( R (,) X
) ) )
26052, 57, 84ltled 8967 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  A  <_  R )
261 iooss1 10691 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( A  e.  RR*  /\  A  <_  R )  ->  ( R (,) X )  C_  ( A (,) X ) )
26292, 260, 261syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R (,) X
)  C_  ( A (,) X ) )
263105adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  X  <_  D )
264 iooss2 10692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( D  e.  RR*  /\  X  <_  D )  ->  ( A (,) X )  C_  ( A (,) D ) )
265228, 263, 264syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( A (,) X
)  C_  ( A (,) D ) )
266262, 265sstrd 3189 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R (,) X
)  C_  ( A (,) D ) )
267266, 232sstrd 3189 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R (,) X
)  C_  ( A (,) B ) )
268236adantr 451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  dom  ( RR  _D  F
)  =  ( A (,) B ) )
269267, 268sseqtr4d 3215 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R (,) X
)  C_  dom  ( RR 
_D  F ) )
270 ssdmres 4977 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( R (,) X ) 
C_  dom  ( RR  _D  F )  <->  dom  ( ( RR  _D  F )  |`  ( R (,) X
) )  =  ( R (,) X ) )
271269, 270sylib 188 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  dom  ( ( RR  _D  F )  |`  ( R (,) X ) )  =  ( R (,) X ) )
272259, 271eqtrd 2315 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  dom  ( RR  _D  ( F  |`  ( R [,] X ) ) )  =  ( R (,) X ) )
273148adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  G : ( A (,) B ) --> CC )
27447, 163dvres 19261 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
275248, 273, 250, 252, 274syl22anc 1183 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( RR  _D  ( G  |`  ( R [,] X ) ) )  =  ( ( RR 
_D  G )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( R [,] X ) ) ) )
276256reseq2d 4955 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( RR  _D  G )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( R [,] X ) ) )  =  ( ( RR 
_D  G )  |`  ( R (,) X ) ) )
277275, 276eqtrd 2315 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( RR  _D  ( G  |`  ( R [,] X ) ) )  =  ( ( RR 
_D  G )  |`  ( R (,) X ) ) )
278277dmeqd 4881 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  dom  ( RR  _D  ( G  |`  ( R [,] X ) ) )  =  dom  ( ( RR  _D  G )  |`  ( R (,) X
) ) )
279150adantr 451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  dom  ( RR  _D  G
)  =  ( A (,) B ) )
280267, 279sseqtr4d 3215 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R (,) X
)  C_  dom  ( RR 
_D  G ) )
281 ssdmres 4977 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( R (,) X ) 
C_  dom  ( RR  _D  G )  <->  dom  ( ( RR  _D  G )  |`  ( R (,) X
) )  =  ( R (,) X ) )
282280, 281sylib 188 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  dom  ( ( RR  _D  G )  |`  ( R (,) X ) )  =  ( R (,) X ) )
283278, 282eqtrd 2315 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  dom  ( RR  _D  ( G  |`  ( R [,] X ) ) )  =  ( R (,) X ) )
28457, 85, 91, 244, 247, 272, 283cmvth 19338 . . . . . . . . . . . . . . . . . . . 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 ) ) )
28557rexrd 8881 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  R  e.  RR* )
286285adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  ->  R  e.  RR* )
28793ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  ->  X  e.  RR* )
28857, 85, 91ltled 8967 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  R  <_  X )
289288adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  ->  R  <_  X )
290 ubicc2 10753 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( R  e.  RR*  /\  X  e.  RR*  /\  R  <_  X )  ->  X  e.  ( R [,] X
) )
291286, 287, 289, 290syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  ->  X  e.  ( R [,] X ) )
292 fvres 5542 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( X  e.  ( R [,] X )  ->  (
( F  |`  ( R [,] X ) ) `
 X )  =  ( F `  X
) )
293291, 292syl 15 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( F  |`  ( R [,] X ) ) `  X )  =  ( F `  X ) )
294 lbicc2 10752 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( R  e.  RR*  /\  X  e.  RR*  /\  R  <_  X )  ->  R  e.  ( R [,] X
) )
295286, 287, 289, 294syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  ->  R  e.  ( R [,] X ) )
296 fvres 5542 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( R  e.  ( R [,] X )  ->  (
( F  |`  ( R [,] X ) ) `
 R )  =  ( F `  R
) )
297295, 296syl 15 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( F  |`  ( R [,] X ) ) `  R )  =  ( F `  R ) )
298293, 297oveq12d 5876 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( ( F  |`  ( R [,] X
) ) `  X
)  -  ( ( F  |`  ( R [,] X ) ) `  R ) )  =  ( ( F `  X )  -  ( F `  R )
) )
299277fveq1d 5527 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( RR  _D  ( G  |`  ( R [,] X ) ) ) `  w )  =  ( ( ( RR  _D  G )  |`  ( R (,) X
) ) `  w
) )
300 fvres 5542 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  e.  ( R (,) X )  ->  (
( ( RR  _D  G )  |`  ( R (,) X ) ) `
 w )  =  ( ( RR  _D  G ) `  w
) )
301299, 300sylan9eq 2335 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( RR  _D  ( G  |`  ( R [,] X ) ) ) `  w )  =  ( ( RR 
_D  G ) `  w ) )
302298, 301oveq12d 5876 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
303 fvres 5542 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( X  e.  ( R [,] X )  ->  (
( G  |`  ( R [,] X ) ) `
 X )  =  ( G `  X
) )
304291, 303syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( G  |`  ( R [,] X ) ) `  X )  =  ( G `  X ) )
305 fvres 5542 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( R  e.  ( R [,] X )  ->  (
( G  |`  ( R [,] X ) ) `
 R )  =  ( G `  R
) )
306295, 305syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( G  |`  ( R [,] X ) ) `  R )  =  ( G `  R ) )
307304, 306oveq12d 5876 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( ( G  |`  ( R [,] X
) ) `  X
)  -  ( ( G  |`  ( R [,] X ) ) `  R ) )  =  ( ( G `  X )  -  ( G `  R )
) )
308258fveq1d 5527 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( RR  _D  ( F  |`  ( R [,] X ) ) ) `  w )  =  ( ( ( RR  _D  F )  |`  ( R (,) X
) ) `  w
) )
309 fvres 5542 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w  e.  ( R (,) X )  ->  (
( ( RR  _D  F )  |`  ( R (,) X ) ) `
 w )  =  ( ( RR  _D  F ) `  w
) )
310308, 309sylan9eq 2335 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( RR  _D  ( F  |`  ( R [,] X ) ) ) `  w )  =  ( ( RR 
_D  F ) `  w ) )
311307, 310oveq12d 5876 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
312118adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( G `  X )  -  ( G `  R )
)  e.  CC )
313 dvf 19257 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( RR 
_D  F ) : dom  ( RR  _D  F ) --> CC
314236feq2d 5380 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( ( RR  _D  F ) : dom  ( RR  _D  F
) --> CC  <->  ( RR  _D  F ) : ( A (,) B ) --> CC ) )
315313, 314mpbii 202 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( RR  _D  F
) : ( A (,) B ) --> CC )
316315ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( RR  _D  F
) : ( A (,) B ) --> CC )
317267sselda 3180 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  ->  w  e.  ( A (,) B ) )
318316, 317ffvelrnd 5666 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( RR  _D  F ) `  w
)  e.  CC )
319312, 318mulcomd 8856 . . . . . . . . . . . . . . . . . . . . . . . 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 )
) ) )
320311, 319eqtrd 2315 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
321302, 320eqeq12d 2297 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
322113adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( F `  X )  -  ( F `  R )
)  e.  CC )
323199ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( RR  _D  G
) : ( A (,) B ) --> CC )
324323, 317ffvelrnd 5666 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( RR  _D  G ) `  w
)  e.  CC )
325222adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( G `  X )  -  ( G `  R )
)  =/=  0 )
326119ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  ->  -.  0  e.  ran  ( RR  _D  G
) )
327323, 201syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( RR  _D  G
)  Fn  ( A (,) B ) )
328327, 317, 205syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( RR  _D  G ) `  w
)  e.  ran  ( RR  _D  G ) )
329 eleq1 2343 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( RR  _D  G
) `  w )  =  0  ->  (
( ( RR  _D  G ) `  w
)  e.  ran  ( RR  _D  G )  <->  0  e.  ran  ( RR  _D  G
) ) )
330328, 329syl5ibcom 211 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( ( RR 
_D  G ) `  w )  =  0  ->  0  e.  ran  ( RR  _D  G
) ) )
331330necon3bd 2483 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( -.  0  e. 
ran  ( RR  _D  G )  ->  (
( RR  _D  G
) `  w )  =/=  0 ) )
332326, 331mpd 14 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( RR  _D  G ) `  w
)  =/=  0 )
333322, 312, 318, 324, 325, 332divmuleqd 9582 . . . . . . . . . . . . . . . . . . . . . 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 )
) ) ) )
334321, 333bitr4d 247 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
335334rexbidva 2560 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
336284, 335mpbid 201 . . . . . . . . . . . . . . . . . . 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
) ) )
337266sselda 3180 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  ->  w  e.  ( A (,) D ) )
338 lhop1lem.t . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  A. t  e.  ( A (,) D ) ( abs `  (
( ( ( RR 
_D  F ) `  t )  /  (
( RR  _D  G
) `  t )
)  -  C ) )  <  E )
339338ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . 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 )
340 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  =  w  ->  (
( RR  _D  F
) `  t )  =  ( ( RR 
_D  F ) `  w ) )
341 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  =  w  ->  (
( RR  _D  G
) `  t )  =  ( ( RR 
_D  G ) `  w ) )
342340, 341oveq12d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( t  =  w  ->  (
( ( RR  _D  F ) `  t
)  /  ( ( RR  _D  G ) `
 t ) )  =  ( ( ( RR  _D  F ) `
 w )  / 
( ( RR  _D  G ) `  w
) ) )
343342oveq1d 5873 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  =  w  ->  (
( ( ( RR 
_D  F ) `  t )  /  (
( RR  _D  G
) `  t )
)  -  C )  =  ( ( ( ( RR  _D  F
) `  w )  /  ( ( RR 
_D  G ) `  w ) )  -  C ) )
344343fveq2d 5529 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  =  w  ->  ( abs `  ( ( ( ( RR  _D  F
) `  t )  /  ( ( RR 
_D  G ) `  t ) )  -  C ) )  =  ( abs `  (
( ( ( RR 
_D  F ) `  w )  /  (
( RR  _D  G
) `  w )
)  -  C ) ) )
345344breq1d 4033 . . . . . . . . . . . . . . . . . . . . . . 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
) )
346345rspcv 2880 . . . . . . . . . . . . . . . . . . . . . 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 ) )
347337, 339, 346sylc 56 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( abs `  (
( ( ( RR 
_D  F ) `  w )  /  (
( RR  _D  G
) `  w )
)  -  C ) )  <  E )
348 oveq1 5865 . . . . . . . . . . . . . . . . . . . . . . 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
) )
349348fveq2d 5529 . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
350349breq1d 4033 . . . . . . . . . . . . . . . . . . . . 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
) )
351347, 350syl5ibrcom 213 . . . . . . . . . . . . . . . . . . . 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 ) )
352351rexlimdva 2667 . . . . . . . . . . . . . . . . . . 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 ) )
353336, 352mpd 14 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( abs `  (
( ( ( F `
 X )  -  ( F `  R ) )  /  ( ( G `  X )  -  ( G `  R ) ) )  -  C ) )  <  E )
354226, 227, 353ltled 8967 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( abs `  (
( ( ( F `
 X )  -  ( F `  R ) )  /  ( ( G `  X )  -  ( G `  R ) ) )  -  C ) )  <_  E )
355 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( u  =  R  ->  ( F `  u )  =  ( F `  R ) )
356355oveq2d 5874 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( u  =  R  ->  (
( F `  X
)  -  ( F `
 u ) )  =  ( ( F `
 X )  -  ( F `  R ) ) )
357 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( u  =  R  ->  ( G `  u )  =  ( G `  R ) )
358357oveq2d 5874 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( u  =  R  ->  (
( G `  X
)  -  ( G `
 u ) )  =  ( ( G `
 X )  -  ( G `  R ) ) )
359356, 358oveq12d 5876 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  =  R  ->  (
( ( F `  X )  -  ( F `  u )
)  /  ( ( G `  X )  -  ( G `  u ) ) )  =  ( ( ( F `  X )  -  ( F `  R ) )  / 
( ( G `  X )  -  ( G `  R )
) ) )
360359oveq1d 5873 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  =  R  ->  (
( ( ( F `
 X )  -  ( F `  u ) )  /  ( ( G `  X )  -  ( G `  u ) ) )  -  C )  =  ( ( ( ( F `  X )  -  ( F `  R ) )  / 
( ( G `  X )  -  ( G `  R )
) )  -  C
) )
361360fveq2d 5529 . . . . . . . . . . . . . . . . . . 19  |-  ( u  =  R  ->  ( abs `  ( ( ( ( F `  X
)  -  ( F `
 u ) )  /  ( ( G `
 X )  -  ( G `  u ) ) )  -  C
) )  =  ( abs `  ( ( ( ( F `  X )  -  ( F `  R )
)  /  ( ( G `  X )  -  ( G `  R ) ) )  -  C ) ) )
362361breq1d 4033 . . . . . . . . . . . . . . . . . 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
) )
363362rspcev 2884 . . . . . . . . . . . . . . . . 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 )
36499, 354, 363syl2anc 642 . . . . . . . . . . . . . . . 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 )
365364adantlr 695 . . . . . . . . . . . . . . 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 )
366 ssrin 3394 . . . . . . . . . . . . . . . . 17  |-  ( ( A ( ball `  ( abs  o.  -  ) ) r )  C_  v  ->  ( ( A (
ball `  ( abs  o. 
-  ) ) r )  i^i  ( A (,) X ) ) 
C_  ( v  i^i  ( A (,) X
) ) )
367 lbioo 10687 . . . . . . . . . . . . . . . . . . . 20  |-  -.  A  e.  ( A (,) X
)
368 disjsn 3693 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( A (,) X
)  i^i  { A } )  =  (/)  <->  -.  A  e.  ( A (,) X ) )
369367, 368mpbir 200 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A (,) X )  i^i  { A }
)  =  (/)
370 disj3 3499 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( A (,) X
)  i^i  { A } )  =  (/)  <->  ( A (,) X )  =  ( ( A (,) X )  \  { A } ) )
371369, 370mpbi 199 . . . . . . . . . . . . . . . . . 18  |-  ( A (,) X )  =  ( ( A (,) X )  \  { A } )
372371ineq2i 3367 . . . . . . . . . . . . . . . . 17  |-  ( v  i^i  ( A (,) X ) )  =  ( v  i^i  (
( A (,) X
)  \  { A } ) )
373366, 372syl6sseq 3224 . . . . . . . . . . . . . . . 16  |-  ( ( A ( ball `  ( abs  o.  -  ) ) r )  C_  v  ->  ( ( A (
ball `  ( abs  o. 
-  ) ) r )  i^i  ( A (,) X ) ) 
C_  ( v  i^i  ( ( A (,) X )  \  { A } ) ) )
374 ssrexv 3238 . . . . . . . . . . . . . . . 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 ) )
375373, 374syl 15 . . . . . . . . . . . . . . 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 ) )
376365, 375syl5com 26 . . . . . . . . . . . . . 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 ) )
377376anassrs 629 . . . . . . . . . . . . 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 ) )
378377expimpd 586 . . . . . . . . . . . 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 ) )
379378rexlimdva 2667 . . . . . . . . . . 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 ) )
38050, 379mpd 14 . . . . . . . . . 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 )
381 inss2 3390 . . . . . . . . . . . . . 14  |-  ( v  i^i  ( ( A (,) X )  \  { A } ) ) 
C_  ( ( A (,) X )  \  { A } )
382 difss 3303 . . . . . . . . . . . . . 14  |-  ( ( A (,) X ) 
\  { A }
)  C_  ( A (,) X )
383381, 382sstri 3188 . . . . . . . . . . . . 13  |-  ( v  i^i  ( ( A (,) X )  \  { A } ) ) 
C_  ( A (,) X )
384383sseli 3176 . . . . . . . . . . . 12  |-  ( u  e.  ( v  i^i  ( ( A (,) X )  \  { A } ) )  ->  u  e.  ( A (,) X ) )
385 fveq2 5525 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  u  ->  ( F `  z )  =  ( F `  u ) )
386385oveq2d 5874 . . . . . . . . . . . . . . . . 17  |-  ( z  =  u  ->  (
( F `  X
)  -  ( F `
 z ) )  =  ( ( F `
 X )  -  ( F `  u ) ) )
387 fveq2 5525 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  u  ->  ( G `  z )  =  ( G `  u ) )
388387oveq2d 5874 . . . . . . . . . . . . . . . . 17  |-  ( z  =  u  ->  (
( G `  X
)  -  ( G `
 z ) )  =  ( ( G `
 X )  -  ( G `  u ) ) )
389386, 388oveq12d 5876 . . . . . . . . . . . . . . . 16  |-  ( z  =  u  ->  (
( ( F `  X )  -  ( F `  z )
)  /  ( ( G `  X )  -  ( G `  z ) ) )  =  ( ( ( F `  X )  -  ( F `  u ) )  / 
( ( G `  X )  -  ( G `  u )
) ) )
390 eqid 2283 . . . . . . . . . . . . . . . 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 ) ) ) )
391 ovex 5883 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  X
)  -  ( F `
 u ) )  /  ( ( G `
 X )  -  ( G `  u )