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

Theorem lhop1lem 19889
Description: Lemma for lhop1 19890. (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 10944 . . . . . . . . 9  |-  ( ( B  e.  RR*  /\  D  <_  B )  ->  ( A (,) D )  C_  ( A (,) B ) )
52, 3, 4syl2anc 643 . . . . . . . 8  |-  ( ph  ->  ( A (,) D
)  C_  ( A (,) B ) )
6 lhop1lem.x . . . . . . . 8  |-  ( ph  ->  X  e.  ( A (,) D ) )
75, 6sseldd 3341 . . . . . . 7  |-  ( ph  ->  X  e.  ( A (,) B ) )
81, 7ffvelrnd 5863 . . . . . 6  |-  ( ph  ->  ( F `  X
)  e.  RR )
98recnd 9106 . . . . 5  |-  ( ph  ->  ( F `  X
)  e.  CC )
10 lhop1.g . . . . . . 7  |-  ( ph  ->  G : ( A (,) B ) --> RR )
1110, 7ffvelrnd 5863 . . . . . 6  |-  ( ph  ->  ( G `  X
)  e.  RR )
1211recnd 9106 . . . . 5  |-  ( ph  ->  ( G `  X
)  e.  CC )
13 lhop1.gn0 . . . . . 6  |-  ( ph  ->  -.  0  e.  ran  G )
14 ffn 5583 . . . . . . . . . 10  |-  ( G : ( A (,) B ) --> RR  ->  G  Fn  ( A (,) B ) )
1510, 14syl 16 . . . . . . . . 9  |-  ( ph  ->  G  Fn  ( A (,) B ) )
16 fnfvelrn 5859 . . . . . . . . 9  |-  ( ( G  Fn  ( A (,) B )  /\  X  e.  ( A (,) B ) )  -> 
( G `  X
)  e.  ran  G
)
1715, 7, 16syl2anc 643 . . . . . . . 8  |-  ( ph  ->  ( G `  X
)  e.  ran  G
)
18 eleq1 2495 . . . . . . . 8  |-  ( ( G `  X )  =  0  ->  (
( G `  X
)  e.  ran  G  <->  0  e.  ran  G ) )
1917, 18syl5ibcom 212 . . . . . . 7  |-  ( ph  ->  ( ( G `  X )  =  0  ->  0  e.  ran  G ) )
2019necon3bd 2635 . . . . . 6  |-  ( ph  ->  ( -.  0  e. 
ran  G  ->  ( G `
 X )  =/=  0 ) )
2113, 20mpd 15 . . . . 5  |-  ( ph  ->  ( G `  X
)  =/=  0 )
229, 12, 21divcld 9782 . . . 4  |-  ( ph  ->  ( ( F `  X )  /  ( G `  X )
)  e.  CC )
23 limccl 19754 . . . . 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 3338 . . . 4  |-  ( ph  ->  C  e.  CC )
2622, 25subcld 9403 . . 3  |-  ( ph  ->  ( ( ( F `
 X )  / 
( G `  X
) )  -  C
)  e.  CC )
2726abscld 12230 . 2  |-  ( ph  ->  ( abs `  (
( ( F `  X )  /  ( G `  X )
)  -  C ) )  e.  RR )
28 lhop1lem.e . . 3  |-  ( ph  ->  E  e.  RR+ )
2928rpred 10640 . 2  |-  ( ph  ->  E  e.  RR )
30 2re 10061 . . . 4  |-  2  e.  RR
3130a1i 11 . . 3  |-  ( ph  ->  2  e.  RR )
3231, 29remulcld 9108 . 2  |-  ( ph  ->  ( 2  x.  E
)  e.  RR )
33 cnxmet 18799 . . . . . . . . . . . . 13  |-  ( abs 
o.  -  )  e.  ( * Met `  CC )
3433a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( v  e.  ( TopOpen ` fld )  /\  A  e.  v ) )  -> 
( abs  o.  -  )  e.  ( * Met `  CC ) )
35 simprl 733 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( v  e.  ( TopOpen ` fld )  /\  A  e.  v ) )  -> 
v  e.  ( TopOpen ` fld )
)
36 simprr 734 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( v  e.  ( TopOpen ` fld )  /\  A  e.  v ) )  ->  A  e.  v )
37 eliooord 10962 . . . . . . . . . . . . . . . 16  |-  ( X  e.  ( A (,) D )  ->  ( A  <  X  /\  X  <  D ) )
386, 37syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( A  <  X  /\  X  <  D ) )
3938simpld 446 . . . . . . . . . . . . . 14  |-  ( ph  ->  A  <  X )
40 lhop1.a . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  e.  RR )
41 ioossre 10964 . . . . . . . . . . . . . . . 16  |-  ( A (,) D )  C_  RR
4241, 6sseldi 3338 . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  e.  RR )
43 difrp 10637 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  RR  /\  X  e.  RR )  ->  ( A  <  X  <->  ( X  -  A )  e.  RR+ ) )
4440, 42, 43syl2anc 643 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A  <  X  <->  ( X  -  A )  e.  RR+ ) )
4539, 44mpbid 202 . . . . . . . . . . . . 13  |-  ( ph  ->  ( X  -  A
)  e.  RR+ )
4645adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( v  e.  ( TopOpen ` fld )  /\  A  e.  v ) )  -> 
( X  -  A
)  e.  RR+ )
47 eqid 2435 . . . . . . . . . . . . . 14  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
4847cnfldtopn 18808 . . . . . . . . . . . . 13  |-  ( TopOpen ` fld )  =  ( MetOpen `  ( abs  o.  -  ) )
4948mopni3 18516 . . . . . . . . . . . 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 1187 . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  A  e.  RR )
53 simprl 733 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
r  e.  RR+ )
5453rpred 10640 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
r  e.  RR )
5554rehalfcld 10206 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( r  /  2
)  e.  RR )
5652, 55readdcld 9107 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( A  +  ( r  /  2 ) )  e.  RR )
5751, 56syl5eqel 2519 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  R  e.  RR )
5857recnd 9106 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  R  e.  CC )
5940recnd 9106 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  A  e.  CC )
6059adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  A  e.  CC )
61 eqid 2435 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( abs 
o.  -  )  =  ( abs  o.  -  )
6261cnmetdval 18797 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R  e.  CC  /\  A  e.  CC )  ->  ( R ( abs 
o.  -  ) A
)  =  ( abs `  ( R  -  A
) ) )
6358, 60, 62syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R ( abs 
o.  -  ) A
)  =  ( abs `  ( R  -  A
) ) )
6451oveq1i 6083 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( R  -  A )  =  ( ( A  +  ( r  /  2
) )  -  A
)
6554recnd 9106 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
r  e.  CC )
6665halfcld 10204 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( r  /  2
)  e.  CC )
6760, 66pncan2d 9405 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( A  +  ( r  /  2
) )  -  A
)  =  ( r  /  2 ) )
6864, 67syl5eq 2479 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R  -  A
)  =  ( r  /  2 ) )
6968fveq2d 5724 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( abs `  ( R  -  A )
)  =  ( abs `  ( r  /  2
) ) )
7053rphalfcld 10652 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( r  /  2
)  e.  RR+ )
7170rpred 10640 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( r  /  2
)  e.  RR )
7270rpge0d 10644 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
0  <_  ( r  /  2 ) )
7371, 72absidd 12217 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( abs `  (
r  /  2 ) )  =  ( r  /  2 ) )
7463, 69, 733eqtrd 2471 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R ( abs 
o.  -  ) A
)  =  ( r  /  2 ) )
75 rphalflt 10630 . . . . . . . . . . . . . . . . . . . . 21  |-  ( r  e.  RR+  ->  ( r  /  2 )  < 
r )
7653, 75syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( r  /  2
)  <  r )
7774, 76eqbrtrd 4224 . . . . . . . . . . . . . . . . . . 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 9126 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
r  e.  RR* )
80 elbl3 18414 . . . . . . . . . . . . . . . . . . . 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 1185 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R  e.  ( A ( ball `  ( abs  o.  -  ) ) r )  <->  ( R
( abs  o.  -  ) A )  <  r
) )
8277, 81mpbird 224 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  R  e.  ( A
( ball `  ( abs  o. 
-  ) ) r ) )
8352, 70ltaddrpd 10669 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  A  <  ( A  +  ( r  /  2
) ) )
8483, 51syl6breqr 4244 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  A  <  R )
8542adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  X  e.  RR )
8685, 52resubcld 9457 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( X  -  A
)  e.  RR )
87 simprr 734 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
r  <  ( X  -  A ) )
8871, 54, 86, 76, 87lttrd 9223 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( r  /  2
)  <  ( X  -  A ) )
8952, 71, 85ltaddsub2d 9619 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( A  +  ( r  /  2
) )  <  X  <->  ( r  /  2 )  <  ( X  -  A ) ) )
9088, 89mpbird 224 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( A  +  ( r  /  2 ) )  <  X )
9151, 90syl5eqbr 4237 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  R  <  X )
9252rexrd 9126 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  A  e.  RR* )
9342rexrd 9126 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  X  e.  RR* )
9493adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  X  e.  RR* )
95 elioo2 10949 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  RR*  /\  X  e.  RR* )  ->  ( R  e.  ( A (,) X )  <->  ( R  e.  RR  /\  A  < 
R  /\  R  <  X ) ) )
9692, 94, 95syl2anc 643 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R  e.  ( A (,) X )  <-> 
( R  e.  RR  /\  A  <  R  /\  R  <  X ) ) )
9757, 84, 91, 96mpbir3and 1137 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  R  e.  ( A (,) X ) )
98 elin 3522 . . . . . . . . . . . . . . . . . 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 646 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  R  e.  ( ( A ( ball `  ( abs  o.  -  ) ) r )  i^i  ( A (,) X ) ) )
1009adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( F `  X
)  e.  CC )
1011adantr 452 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  F : ( A (,) B ) --> RR )
102 lhop1lem.d . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  D  e.  RR )
103102rexrd 9126 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  D  e.  RR* )
10438simprd 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  X  <  D )
10542, 102, 104ltled 9213 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  X  <_  D )
10693, 103, 2, 105, 3xrletrd 10744 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  X  <_  B )
107 iooss2 10944 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( B  e.  RR*  /\  X  <_  B )  ->  ( A (,) X )  C_  ( A (,) B ) )
1082, 106, 107syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( A (,) X
)  C_  ( A (,) B ) )
109108adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( A (,) X
)  C_  ( A (,) B ) )
110109, 97sseldd 3341 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  R  e.  ( A (,) B ) )
111101, 110ffvelrnd 5863 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( F `  R
)  e.  RR )
112111recnd 9106 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( F `  R
)  e.  CC )
113100, 112subcld 9403 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( F `  X )  -  ( F `  R )
)  e.  CC )
11412adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( G `  X
)  e.  CC )
11510adantr 452 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  G : ( A (,) B ) --> RR )
116115, 110ffvelrnd 5863 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( G `  R
)  e.  RR )
117116recnd 9106 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( G `  R
)  e.  CC )
118114, 117subcld 9403 . . . . . . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  -.  0  e.  ran  ( RR  _D  G ) )
12112adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( G `  X )  e.  CC )
122108sselda 3340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  z  e.  ( A (,) B ) )
12310ffvelrnda 5862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  z  e.  ( A (,) B ) )  ->  ( G `  z )  e.  RR )
124122, 123syldan 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( G `  z )  e.  RR )
125124recnd 9106 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( G `  z )  e.  CC )
126121, 125subeq0ad 9413 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( (
( G `  X
)  -  ( G `
 z ) )  =  0  <->  ( G `  X )  =  ( G `  z ) ) )
127 ioossre 10964 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( A (,) B )  C_  RR
128127, 122sseldi 3338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  z  e.  RR )
129128adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
z  e.  RR )
13042ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  ->  X  e.  RR )
131 eliooord 10962 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z  e.  ( A (,) X )  ->  ( A  <  z  /\  z  <  X ) )
132131adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( A  <  z  /\  z  < 
X ) )
133132simprd 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  z  <  X )
134133adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
z  <  X )
13540rexrd 9126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  A  e.  RR* )
136135adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  A  e.  RR* )
1372adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  B  e.  RR* )
138132simpld 446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  A  <  z )
13993, 103, 2, 104, 3xrltletrd 10743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  X  <  B )
140139adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  X  <  B )
141 iccssioo 10971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <  z  /\  X  <  B ) )  ->  ( z [,] X )  C_  ( A (,) B ) )
142136, 137, 138, 140, 141syl22anc 1185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( z [,] X )  C_  ( A (,) B ) )
143142adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( z [,] X
)  C_  ( A (,) B ) )
144 ax-resscn 9039 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  RR  C_  CC
145144a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  RR  C_  CC )
146 fss 5591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( G : ( A (,) B ) --> RR 
/\  RR  C_  CC )  ->  G : ( A (,) B ) --> CC )
14710, 144, 146sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  G : ( A (,) B ) --> CC )
148127a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  ( A (,) B
)  C_  RR )
149 lhop1.ig . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  dom  ( RR  _D  G )  =  ( A (,) B ) )
150 dvcn 19799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( RR  C_  CC  /\  G : ( A (,) B ) --> CC 
/\  ( A (,) B )  C_  RR )  /\  dom  ( RR 
_D  G )  =  ( A (,) B
) )  ->  G  e.  ( ( A (,) B ) -cn-> CC ) )
151145, 147, 148, 149, 150syl31anc 1187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  G  e.  ( ( A (,) B )
-cn-> CC ) )
152 cncffvrn 18920 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( RR  C_  CC  /\  G  e.  ( ( A (,) B ) -cn-> CC ) )  ->  ( G  e.  ( ( A (,) B ) -cn-> RR )  <-> 
G : ( A (,) B ) --> RR ) )
153144, 151, 152sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  ( G  e.  ( ( A (,) B
) -cn-> RR )  <->  G :
( A (,) B
) --> RR ) )
15410, 153mpbird 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  G  e.  ( ( A (,) B )
-cn-> RR ) )
155154ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  ->  G  e.  ( ( A (,) B ) -cn-> RR ) )
156 rescncf 18919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( z [,] X ) 
C_  ( A (,) B )  ->  ( G  e.  ( ( A (,) B ) -cn-> RR )  ->  ( G  |`  ( z [,] X
) )  e.  ( ( z [,] X
) -cn-> RR ) ) )
157143, 155, 156sylc 58 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( G  |`  (
z [,] X ) )  e.  ( ( z [,] X )
-cn-> RR ) )
158144a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  ->  RR  C_  CC )
159147ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  ->  G : ( A (,) B ) --> CC )
160127a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( A (,) B
)  C_  RR )
161143, 127syl6ss 3352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( z [,] X
)  C_  RR )
16247tgioo2 18826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
16347, 162dvres 19790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
164158, 159, 160, 161, 163syl22anc 1185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( RR  _D  ( G  |`  ( z [,] X ) ) )  =  ( ( RR 
_D  G )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( z [,] X ) ) ) )
165 iccntr 18844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( z  e.  RR  /\  X  e.  RR )  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( z [,] X ) )  =  ( z (,) X
) )
166129, 130, 165syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( ( int `  ( topGen `
 ran  (,) )
) `  ( z [,] X ) )  =  ( z (,) X
) )
167166reseq2d 5138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( ( RR  _D  G )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( z [,] X ) ) )  =  ( ( RR 
_D  G )  |`  ( z (,) X
) ) )
168164, 167eqtrd 2467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( RR  _D  ( G  |`  ( z [,] X ) ) )  =  ( ( RR 
_D  G )  |`  ( z (,) X
) ) )
169168dmeqd 5064 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  ->  dom  ( RR  _D  ( G  |`  ( z [,] X ) ) )  =  dom  ( ( RR  _D  G )  |`  ( z (,) X
) ) )
170 ioossicc 10988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( z (,) X )  C_  ( z [,] X
)
171170, 143syl5ss 3351 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( z (,) X
)  C_  ( A (,) B ) )
172149ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  ->  dom  ( RR  _D  G
)  =  ( A (,) B ) )
173171, 172sseqtr4d 3377 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( z (,) X
)  C_  dom  ( RR 
_D  G ) )
174 ssdmres 5160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( z (,) X ) 
C_  dom  ( RR  _D  G )  <->  dom  ( ( RR  _D  G )  |`  ( z (,) X
) )  =  ( z (,) X ) )
175173, 174sylib 189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  ->  dom  ( ( RR  _D  G )  |`  (
z (,) X ) )  =  ( z (,) X ) )
176169, 175eqtrd 2467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  ->  dom  ( RR  _D  ( G  |`  ( z [,] X ) ) )  =  ( z (,) X ) )
177128rexrd 9126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  z  e.  RR* )
17893adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  X  e.  RR* )
17942adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  X  e.  RR )
180128, 179, 133ltled 9213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  z  <_  X )
181 ubicc2 11006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( z  e.  RR*  /\  X  e.  RR*  /\  z  <_  X )  ->  X  e.  ( z [,] X
) )
182177, 178, 180, 181syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  X  e.  ( z [,] X
) )
183 fvres 5737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( X  e.  ( z [,] X )  ->  (
( G  |`  (
z [,] X ) ) `  X )  =  ( G `  X ) )
184182, 183syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( ( G  |`  ( z [,] X ) ) `  X )  =  ( G `  X ) )
185 lbicc2 11005 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( z  e.  RR*  /\  X  e.  RR*  /\  z  <_  X )  ->  z  e.  ( z [,] X
) )
186177, 178, 180, 185syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  z  e.  ( z [,] X
) )
187 fvres 5737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( z  e.  ( z [,] X )  ->  (
( G  |`  (
z [,] X ) ) `  z )  =  ( G `  z ) )
188186, 187syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( ( G  |`  ( z [,] X ) ) `  z )  =  ( G `  z ) )
189184, 188eqeq12d 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( (
( G  |`  (
z [,] X ) ) `  X )  =  ( ( G  |`  ( z [,] X
) ) `  z
)  <->  ( G `  X )  =  ( G `  z ) ) )
190189biimpar 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( ( G  |`  ( z [,] X
) ) `  X
)  =  ( ( G  |`  ( z [,] X ) ) `  z ) )
191190eqcomd 2440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( ( G  |`  ( z [,] X
) ) `  z
)  =  ( ( G  |`  ( z [,] X ) ) `  X ) )
192129, 130, 134, 157, 176, 191rolle 19866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  ->  E. w  e.  (
z (,) X ) ( ( RR  _D  ( G  |`  ( z [,] X ) ) ) `  w )  =  0 )
193168fveq1d 5722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( ( RR  _D  ( G  |`  ( z [,] X ) ) ) `  w )  =  ( ( ( RR  _D  G )  |`  ( z (,) X
) ) `  w
) )
194 fvres 5737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( w  e.  ( z (,) X )  ->  (
( ( RR  _D  G )  |`  (
z (,) X ) ) `  w )  =  ( ( RR 
_D  G ) `  w ) )
195193, 194sylan9eq 2487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  z  e.  ( A (,) X ) )  /\  ( G `  X )  =  ( G `  z ) )  /\  w  e.  ( z (,) X ) )  -> 
( ( RR  _D  ( G  |`  ( z [,] X ) ) ) `  w )  =  ( ( RR 
_D  G ) `  w ) )
196 dvf 19786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( RR 
_D  G ) : dom  ( RR  _D  G ) --> CC
197149feq2d 5573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  ( ( RR  _D  G ) : dom  ( RR  _D  G
) --> CC  <->  ( RR  _D  G ) : ( A (,) B ) --> CC ) )
198196, 197mpbii 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  ( RR  _D  G
) : ( A (,) B ) --> CC )
199198ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( RR  _D  G
) : ( A (,) B ) --> CC )
200 ffn 5583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( RR  _D  G ) : ( A (,) B ) --> CC  ->  ( RR  _D  G )  Fn  ( A (,) B ) )
201199, 200syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
( RR  _D  G
)  Fn  ( A (,) B ) )
202201adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  z  e.  ( A (,) X ) )  /\  ( G `  X )  =  ( G `  z ) )  /\  w  e.  ( z (,) X ) )  -> 
( RR  _D  G
)  Fn  ( A (,) B ) )
203171sselda 3340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  z  e.  ( A (,) X ) )  /\  ( G `  X )  =  ( G `  z ) )  /\  w  e.  ( z (,) X ) )  ->  w  e.  ( A (,) B ) )
204 fnfvelrn 5859 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( RR  _D  G
)  Fn  ( A (,) B )  /\  w  e.  ( A (,) B ) )  -> 
( ( RR  _D  G ) `  w
)  e.  ran  ( RR  _D  G ) )
205202, 203, 204syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  z  e.  ( A (,) X ) )  /\  ( G `  X )  =  ( G `  z ) )  /\  w  e.  ( z (,) X ) )  -> 
( ( RR  _D  G ) `  w
)  e.  ran  ( RR  _D  G ) )
206195, 205eqeltrd 2509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
207 eleq1 2495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
208206, 207syl5ibcom 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
209208rexlimdva 2822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
210192, 209mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  z  e.  ( A (,) X
) )  /\  ( G `  X )  =  ( G `  z ) )  -> 
0  e.  ran  ( RR  _D  G ) )
211210ex 424 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( ( G `  X )  =  ( G `  z )  ->  0  e.  ran  ( RR  _D  G ) ) )
212126, 211sylbid 207 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( (
( G `  X
)  -  ( G `
 z ) )  =  0  ->  0  e.  ran  ( RR  _D  G ) ) )
213212necon3bd 2635 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( -.  0  e.  ran  ( RR 
_D  G )  -> 
( ( G `  X )  -  ( G `  z )
)  =/=  0 ) )
214120, 213mpd 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  z  e.  ( A (,) X ) )  ->  ( ( G `  X )  -  ( G `  z ) )  =/=  0 )
215214ralrimiva 2781 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  A. z  e.  ( A (,) X ) ( ( G `  X )  -  ( G `  z )
)  =/=  0 )
216215adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  A. z  e.  ( A (,) X ) ( ( G `  X
)  -  ( G `
 z ) )  =/=  0 )
217 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  =  R  ->  ( G `  z )  =  ( G `  R ) )
218217oveq2d 6089 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( z  =  R  ->  (
( G `  X
)  -  ( G `
 z ) )  =  ( ( G `
 X )  -  ( G `  R ) ) )
219218neeq1d 2611 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  =  R  ->  (
( ( G `  X )  -  ( G `  z )
)  =/=  0  <->  (
( G `  X
)  -  ( G `
 R ) )  =/=  0 ) )
220219rspcv 3040 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( R  e.  ( A (,) X )  ->  ( A. z  e.  ( A (,) X ) ( ( G `  X
)  -  ( G `
 z ) )  =/=  0  ->  (
( G `  X
)  -  ( G `
 R ) )  =/=  0 ) )
22197, 216, 220sylc 58 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( G `  X )  -  ( G `  R )
)  =/=  0 )
222113, 118, 221divcld 9782 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( ( F `
 X )  -  ( F `  R ) )  /  ( ( G `  X )  -  ( G `  R ) ) )  e.  CC )
22325adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  C  e.  CC )
224222, 223subcld 9403 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( ( ( F `  X )  -  ( F `  R ) )  / 
( ( G `  X )  -  ( G `  R )
) )  -  C
)  e.  CC )
225224abscld 12230 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( abs `  (
( ( ( F `
 X )  -  ( F `  R ) )  /  ( ( G `  X )  -  ( G `  R ) ) )  -  C ) )  e.  RR )
22629adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  E  e.  RR )
227103adantr 452 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  D  e.  RR* )
228104adantr 452 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  X  <  D )
229 iccssioo 10971 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( A  e.  RR*  /\  D  e.  RR* )  /\  ( A  <  R  /\  X  <  D ) )  ->  ( R [,] X )  C_  ( A (,) D ) )
23092, 227, 84, 228, 229syl22anc 1185 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R [,] X
)  C_  ( A (,) D ) )
2315adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( A (,) D
)  C_  ( A (,) B ) )
232230, 231sstrd 3350 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R [,] X
)  C_  ( A (,) B ) )
233 fss 5591 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( F : ( A (,) B ) --> RR 
/\  RR  C_  CC )  ->  F : ( A (,) B ) --> CC )
2341, 144, 233sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  F : ( A (,) B ) --> CC )
235 lhop1.if . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  dom  ( RR  _D  F )  =  ( A (,) B ) )
236 dvcn 19799 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( RR  C_  CC  /\  F : ( A (,) B ) --> CC 
/\  ( A (,) B )  C_  RR )  /\  dom  ( RR 
_D  F )  =  ( A (,) B
) )  ->  F  e.  ( ( A (,) B ) -cn-> CC ) )
237145, 234, 148, 235, 236syl31anc 1187 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  F  e.  ( ( A (,) B )
-cn-> CC ) )
238 cncffvrn 18920 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( RR  C_  CC  /\  F  e.  ( ( A (,) B ) -cn-> CC ) )  ->  ( F  e.  ( ( A (,) B ) -cn-> RR )  <-> 
F : ( A (,) B ) --> RR ) )
239144, 237, 238sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( F  e.  ( ( A (,) B
) -cn-> RR )  <->  F :
( A (,) B
) --> RR ) )
2401, 239mpbird 224 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  F  e.  ( ( A (,) B )
-cn-> RR ) )
241240adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  F  e.  ( ( A (,) B ) -cn-> RR ) )
242 rescncf 18919 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R [,] X ) 
C_  ( A (,) B )  ->  ( F  e.  ( ( A (,) B ) -cn-> RR )  ->  ( F  |`  ( R [,] X
) )  e.  ( ( R [,] X
) -cn-> RR ) ) )
243232, 241, 242sylc 58 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( F  |`  ( R [,] X ) )  e.  ( ( R [,] X ) -cn-> RR ) )
244154adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  G  e.  ( ( A (,) B ) -cn-> RR ) )
245 rescncf 18919 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R [,] X ) 
C_  ( A (,) B )  ->  ( G  e.  ( ( A (,) B ) -cn-> RR )  ->  ( G  |`  ( R [,] X
) )  e.  ( ( R [,] X
) -cn-> RR ) ) )
246232, 244, 245sylc 58 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( G  |`  ( R [,] X ) )  e.  ( ( R [,] X ) -cn-> RR ) )
247144a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  RR  C_  CC )
248234adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  F : ( A (,) B ) --> CC )
249127a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( A (,) B
)  C_  RR )
250 iccssre 10984 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( R  e.  RR  /\  X  e.  RR )  ->  ( R [,] X
)  C_  RR )
25157, 85, 250syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R [,] X
)  C_  RR )
25247, 162dvres 19790 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
253247, 248, 249, 251, 252syl22anc 1185 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( RR  _D  ( F  |`  ( R [,] X ) ) )  =  ( ( RR 
_D  F )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( R [,] X ) ) ) )
254 iccntr 18844 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( R  e.  RR  /\  X  e.  RR )  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( R [,] X ) )  =  ( R (,) X
) )
25557, 85, 254syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( int `  ( topGen `
 ran  (,) )
) `  ( R [,] X ) )  =  ( R (,) X
) )
256255reseq2d 5138 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( RR  _D  F )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( R [,] X ) ) )  =  ( ( RR 
_D  F )  |`  ( R (,) X ) ) )
257253, 256eqtrd 2467 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( RR  _D  ( F  |`  ( R [,] X ) ) )  =  ( ( RR 
_D  F )  |`  ( R (,) X ) ) )
258257dmeqd 5064 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  dom  ( RR  _D  ( F  |`  ( R [,] X ) ) )  =  dom  ( ( RR  _D  F )  |`  ( R (,) X
) ) )
25952, 57, 84ltled 9213 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  A  <_  R )
260 iooss1 10943 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( A  e.  RR*  /\  A  <_  R )  ->  ( R (,) X )  C_  ( A (,) X ) )
26192, 259, 260syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R (,) X
)  C_  ( A (,) X ) )
262105adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  X  <_  D )
263 iooss2 10944 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( D  e.  RR*  /\  X  <_  D )  ->  ( A (,) X )  C_  ( A (,) D ) )
264227, 262, 263syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( A (,) X
)  C_  ( A (,) D ) )
265261, 264sstrd 3350 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R (,) X
)  C_  ( A (,) D ) )
266265, 231sstrd 3350 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R (,) X
)  C_  ( A (,) B ) )
267235adantr 452 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  dom  ( RR  _D  F
)  =  ( A (,) B ) )
268266, 267sseqtr4d 3377 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R (,) X
)  C_  dom  ( RR 
_D  F ) )
269 ssdmres 5160 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( R (,) X ) 
C_  dom  ( RR  _D  F )  <->  dom  ( ( RR  _D  F )  |`  ( R (,) X
) )  =  ( R (,) X ) )
270268, 269sylib 189 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  dom  ( ( RR  _D  F )  |`  ( R (,) X ) )  =  ( R (,) X ) )
271258, 270eqtrd 2467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  dom  ( RR  _D  ( F  |`  ( R [,] X ) ) )  =  ( R (,) X ) )
272147adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  G : ( A (,) B ) --> CC )
27347, 162dvres 19790 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
274247, 272, 249, 251, 273syl22anc 1185 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( RR  _D  ( G  |`  ( R [,] X ) ) )  =  ( ( RR 
_D  G )  |`  ( ( int `  ( topGen `
 ran  (,) )
) `  ( R [,] X ) ) ) )
275255reseq2d 5138 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( RR  _D  G )  |`  (
( int `  ( topGen `
 ran  (,) )
) `  ( R [,] X ) ) )  =  ( ( RR 
_D  G )  |`  ( R (,) X ) ) )
276274, 275eqtrd 2467 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( RR  _D  ( G  |`  ( R [,] X ) ) )  =  ( ( RR 
_D  G )  |`  ( R (,) X ) ) )
277276dmeqd 5064 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  dom  ( RR  _D  ( G  |`  ( R [,] X ) ) )  =  dom  ( ( RR  _D  G )  |`  ( R (,) X
) ) )
278149adantr 452 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  dom  ( RR  _D  G
)  =  ( A (,) B ) )
279266, 278sseqtr4d 3377 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( R (,) X
)  C_  dom  ( RR 
_D  G ) )
280 ssdmres 5160 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( R (,) X ) 
C_  dom  ( RR  _D  G )  <->  dom  ( ( RR  _D  G )  |`  ( R (,) X
) )  =  ( R (,) X ) )
281279, 280sylib 189 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  dom  ( ( RR  _D  G )  |`  ( R (,) X ) )  =  ( R (,) X ) )
282277, 281eqtrd 2467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  dom  ( RR  _D  ( G  |`  ( R [,] X ) ) )  =  ( R (,) X ) )
28357, 85, 91, 243, 246, 271, 282cmvth 19867 . . . . . . . . . . . . . . . . . . . 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 ) ) )
28457rexrd 9126 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  R  e.  RR* )
285284adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  ->  R  e.  RR* )
28693ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  ->  X  e.  RR* )
28757, 85, 91ltled 9213 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  ->  R  <_  X )
288287adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  ->  R  <_  X )
289 ubicc2 11006 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( R  e.  RR*  /\  X  e.  RR*  /\  R  <_  X )  ->  X  e.  ( R [,] X
) )
290285, 286, 288, 289syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  ->  X  e.  ( R [,] X ) )
291 fvres 5737 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( X  e.  ( R [,] X )  ->  (
( F  |`  ( R [,] X ) ) `
 X )  =  ( F `  X
) )
292290, 291syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( F  |`  ( R [,] X ) ) `  X )  =  ( F `  X ) )
293 lbicc2 11005 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( R  e.  RR*  /\  X  e.  RR*  /\  R  <_  X )  ->  R  e.  ( R [,] X
) )
294285, 286, 288, 293syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  ->  R  e.  ( R [,] X ) )
295 fvres 5737 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( R  e.  ( R [,] X )  ->  (
( F  |`  ( R [,] X ) ) `
 R )  =  ( F `  R
) )
296294, 295syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( F  |`  ( R [,] X ) ) `  R )  =  ( F `  R ) )
297292, 296oveq12d 6091 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( ( F  |`  ( R [,] X
) ) `  X
)  -  ( ( F  |`  ( R [,] X ) ) `  R ) )  =  ( ( F `  X )  -  ( F `  R )
) )
298276fveq1d 5722 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( RR  _D  ( G  |`  ( R [,] X ) ) ) `  w )  =  ( ( ( RR  _D  G )  |`  ( R (,) X
) ) `  w
) )
299 fvres 5737 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  e.  ( R (,) X )  ->  (
( ( RR  _D  G )  |`  ( R (,) X ) ) `
 w )  =  ( ( RR  _D  G ) `  w
) )
300298, 299sylan9eq 2487 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( RR  _D  ( G  |`  ( R [,] X ) ) ) `  w )  =  ( ( RR 
_D  G ) `  w ) )
301297, 300oveq12d 6091 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
302 fvres 5737 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( X  e.  ( R [,] X )  ->  (
( G  |`  ( R [,] X ) ) `
 X )  =  ( G `  X
) )
303290, 302syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( G  |`  ( R [,] X ) ) `  X )  =  ( G `  X ) )
304 fvres 5737 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( R  e.  ( R [,] X )  ->  (
( G  |`  ( R [,] X ) ) `
 R )  =  ( G `  R
) )
305294, 304syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( G  |`  ( R [,] X ) ) `  R )  =  ( G `  R ) )
306303, 305oveq12d 6091 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( ( G  |`  ( R [,] X
) ) `  X
)  -  ( ( G  |`  ( R [,] X ) ) `  R ) )  =  ( ( G `  X )  -  ( G `  R )
) )
307257fveq1d 5722 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( ( RR  _D  ( F  |`  ( R [,] X ) ) ) `  w )  =  ( ( ( RR  _D  F )  |`  ( R (,) X
) ) `  w
) )
308 fvres 5737 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( w  e.  ( R (,) X )  ->  (
( ( RR  _D  F )  |`  ( R (,) X ) ) `
 w )  =  ( ( RR  _D  F ) `  w
) )
309307, 308sylan9eq 2487 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( RR  _D  ( F  |`  ( R [,] X ) ) ) `  w )  =  ( ( RR 
_D  F ) `  w ) )
310306, 309oveq12d 6091 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
311118adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( G `  X )  -  ( G `  R )
)  e.  CC )
312 dvf 19786 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( RR 
_D  F ) : dom  ( RR  _D  F ) --> CC
313235feq2d 5573 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( ( RR  _D  F ) : dom  ( RR  _D  F
) --> CC  <->  ( RR  _D  F ) : ( A (,) B ) --> CC ) )
314312, 313mpbii 203 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( RR  _D  F
) : ( A (,) B ) --> CC )
315314ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( RR  _D  F
) : ( A (,) B ) --> CC )
316266sselda 3340 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  ->  w  e.  ( A (,) B ) )
317315, 316ffvelrnd 5863 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( RR  _D  F ) `  w
)  e.  CC )
318311, 317mulcomd 9101 . . . . . . . . . . . . . . . . . . . . . . . 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 )
) ) )
319310, 318eqtrd 2467 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
320301, 319eqeq12d 2449 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
321113adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( F `  X )  -  ( F `  R )
)  e.  CC )
322198ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( RR  _D  G
) : ( A (,) B ) --> CC )
323322, 316ffvelrnd 5863 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( RR  _D  G ) `  w
)  e.  CC )
324221adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( G `  X )  -  ( G `  R )
)  =/=  0 )
325119ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  ->  -.  0  e.  ran  ( RR  _D  G
) )
326322, 200syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( RR  _D  G
)  Fn  ( A (,) B ) )
327326, 316, 204syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( RR  _D  G ) `  w
)  e.  ran  ( RR  _D  G ) )
328 eleq1 2495 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( RR  _D  G
) `  w )  =  0  ->  (
( ( RR  _D  G ) `  w
)  e.  ran  ( RR  _D  G )  <->  0  e.  ran  ( RR  _D  G
) ) )
329327, 328syl5ibcom 212 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( ( RR 
_D  G ) `  w )  =  0  ->  0  e.  ran  ( RR  _D  G
) ) )
330329necon3bd 2635 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( -.  0  e. 
ran  ( RR  _D  G )  ->  (
( RR  _D  G
) `  w )  =/=  0 ) )
331325, 330mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( ( RR  _D  G ) `  w
)  =/=  0 )
332321, 311, 317, 323, 324, 331divmuleqd 9828 . . . . . . . . . . . . . . . . . . . . . 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 )
) ) ) )
333320, 332bitr4d 248 . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
334333rexbidva 2714 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
335283, 334mpbid 202 . . . . . . . . . . . . . . . . . . 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
) ) )
336265sselda 3340 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  ->  w  e.  ( A (,) D ) )
337 lhop1lem.t . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  A. t  e.  ( A (,) D ) ( abs `  (
( ( ( RR 
_D  F ) `  t )  /  (
( RR  _D  G
) `  t )
)  -  C ) )  <  E )
338337ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . 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 )
339 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  =  w  ->  (
( RR  _D  F
) `  t )  =  ( ( RR 
_D  F ) `  w ) )
340 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  =  w  ->  (
( RR  _D  G
) `  t )  =  ( ( RR 
_D  G ) `  w ) )
341339, 340oveq12d 6091 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( t  =  w  ->  (
( ( RR  _D  F ) `  t
)  /  ( ( RR  _D  G ) `
 t ) )  =  ( ( ( RR  _D  F ) `
 w )  / 
( ( RR  _D  G ) `  w
) ) )
342341oveq1d 6088 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  =  w  ->  (
( ( ( RR 
_D  F ) `  t )  /  (
( RR  _D  G
) `  t )
)  -  C )  =  ( ( ( ( RR  _D  F
) `  w )  /  ( ( RR 
_D  G ) `  w ) )  -  C ) )
343342fveq2d 5724 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  =  w  ->  ( abs `  ( ( ( ( RR  _D  F
) `  t )  /  ( ( RR 
_D  G ) `  t ) )  -  C ) )  =  ( abs `  (
( ( ( RR 
_D  F ) `  w )  /  (
( RR  _D  G
) `  w )
)  -  C ) ) )
344343breq1d 4214 . . . . . . . . . . . . . . . . . . . . . . 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
) )
345344rspcv 3040 . . . . . . . . . . . . . . . . . . . . . 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 ) )
346336, 338, 345sylc 58 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
r  e.  RR+  /\  r  <  ( X  -  A
) ) )  /\  w  e.  ( R (,) X ) )  -> 
( abs `  (
( ( ( RR 
_D  F ) `  w )  /  (
( RR  _D  G
) `  w )
)  -  C ) )  <  E )
347 oveq1 6080 . . . . . . . . . . . . . . . . . . . . . . 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
) )
348347fveq2d 5724 . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
349348breq1d 4214 . . . . . . . . . . . . . . . . . . . . 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
) )
350346, 349syl5ibrcom 214 . . . . . . . . . . . . . . . . . . . 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 ) )
351350rexlimdva 2822 . . . . . . . . . . . . . . . . . . 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 ) )
352335, 351mpd 15 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( abs `  (
( ( ( F `
 X )  -  ( F `  R ) )  /  ( ( G `  X )  -  ( G `  R ) ) )  -  C ) )  <  E )
353225, 226, 352ltled 9213 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( r  e.  RR+  /\  r  < 
( X  -  A
) ) )  -> 
( abs `  (
( ( ( F `
 X )  -  ( F `  R ) )  /  ( ( G `  X )  -  ( G `  R ) ) )  -  C ) )  <_  E )
354 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( u  =  R  ->  ( F `  u )  =  ( F `  R ) )
355354oveq2d 6089 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( u  =  R  ->  (
( F `  X
)  -  ( F `
 u ) )  =  ( ( F `
 X )  -  ( F `  R ) ) )
356 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( u  =  R  ->  ( G `  u )  =  ( G `  R ) )
357356oveq2d 6089 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( u  =  R  ->  (
( G `  X
)  -  ( G `
 u ) )  =  ( ( G `
 X )  -  ( G `  R ) ) )
358355, 357oveq12d 6091 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  =  R  ->  (
( ( F `  X )  -  ( F `  u )
)  /  ( ( G `  X )  -  ( G `  u ) ) )  =  ( ( ( F `  X )  -  ( F `  R ) )  / 
( ( G `  X )  -  ( G `  R )
) ) )
359358oveq1d 6088 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  =  R  ->  (
( ( ( F `
 X )  -  ( F `  u ) )  /  ( ( G `  X )  -  ( G `  u ) ) )  -  C )  =  ( ( ( ( F `  X )  -  ( F `  R ) )  / 
( ( G `  X )  -  ( G `  R )
) )  -  C
) )
360359fveq2d 5724 . . . . . . . . . . . . . . . . . . 19  |-  ( u  =  R  ->  ( abs `  ( ( ( ( F `  X
)  -  ( F `
 u ) )  /  ( ( G `
 X )  -  ( G `  u ) ) )  -  C
) )  =  ( abs `  ( ( ( ( F `  X )  -  ( F `  R )
)  /  ( ( G `  X )  -  ( G `  R ) ) )  -  C ) ) )
361360breq1d 4214 . . . . . . . . . . . . . . . . . 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
) )
362361rspcev 3044 . . . . . . . . . . . . . . . . 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 )
36399, 353, 362syl2anc 643 . . . . . . . . . . . . . . . 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 )
364363adantlr 696 . . . . . . . . . . . . . . 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 )
365 ssrin 3558 . . . . . . . . . . . . . . . . 17  |-  ( ( A ( ball `  ( abs  o.  -  ) ) r )  C_  v  ->  ( ( A (
ball `  ( abs  o. 
-  ) ) r )  i^i  ( A (,) X ) ) 
C_  ( v  i^i  ( A (,) X
) ) )
366 lbioo 10939 . . . . . . . . . . . . . . . . . . . 20  |-  -.  A  e.  ( A (,) X
)
367 disjsn 3860 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( A (,) X
)  i^i  { A } )  =  (/)  <->  -.  A  e.  ( A (,) X ) )
368366, 367mpbir 201 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A (,) X )  i^i  { A }
)  =  (/)
369 disj3 3664 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( A (,) X
)  i^i  { A } )  =  (/)  <->  ( A (,) X )  =  ( ( A (,) X )  \  { A } ) )
370368, 369mpbi 200 . . . . . . . . . . . . . . . . . 18  |-  ( A (,) X )  =  ( ( A (,) X )  \  { A } )
371370ineq2i 3531 . . . . . . . . . . . . . . . . 17  |-  ( v  i^i  ( A (,) X ) )  =  ( v  i^i  (
( A (,) X
)  \  { A } ) )
372365, 371syl6sseq 3386 . . . . . . . . . . . . . . . 16  |-  ( ( A ( ball `  ( abs  o.  -  ) ) r )  C_  v  ->  ( ( A (
ball `  ( abs  o. 
-  ) ) r )  i^i  ( A (,) X ) ) 
C_  ( v  i^i  ( ( A (,) X )  \  { A } ) ) )
373 ssrexv 3400 . . . . . . . . . . . . . . . 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 ) )
374372, 373syl 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 ) )
375364, 374syl5com 28 . . . . . . . . . . . . . 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 ) )
376375anassrs 630 . . . . . . . . . . . . 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 ) )
377376expimpd 587 . . . . . . . . . . . 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 ) )
378377rexlimdva 2822 . . . . . . . . . . 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 ) )
37950, 378mpd 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 )
380 inss2 3554 . . . . . . . . . . . . . 14  |-  ( v  i^i  ( ( A (,) X )  \  { A } ) ) 
C_  ( ( A (,) X )  \  { A } )
381 difss 3466 . . . . . . . . . . . . . 14  |-  ( ( A (,) X ) 
\  { A }
)  C_  ( A (,) X )
382380, 381sstri 3349 . . . . . . . . . . . . 13  |-  ( v  i^i  ( ( A (,) X )  \  { A } ) ) 
C_  ( A (,) X )
383382sseli 3336 . . . . . . . . . . . 12  |-  ( u  e.  ( v  i^i  ( ( A (,) X )  \  { A } ) )  ->  u  e.  ( A (,) X ) )
384 fveq2 5720 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  u  ->  ( F `  z )  =  ( F `  u ) )
385384oveq2d 6089 . . . . . . . . . . . . . . . . 17  |-  ( z  =  u  ->  (
( F `  X
)  -  ( F `
 z ) )  =  ( ( F `
 X )  -  ( F `  u ) ) )
386 fveq2 5720 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  u  ->  ( G `  z )  =  ( G `  u ) )
387386oveq2d 6089 . . . . . . . . . . . . . . . . 17  |-  ( z  =  u  ->  (
( G `  X
)  -  ( G `
 z ) )  =  ( ( G `
 X )  -  ( G `  u ) ) )
388385, 387oveq12d 6091 . . . . . . . . . . . . . . . 16  |-  ( z  =  u  ->  (
( ( F `  X )  -  ( F `  z )
)  /  ( ( G `  X )  -  ( G `  z ) ) )  =  ( ( ( F `  X )  -  ( F `  u ) )  / 
( ( G `  X )  -  ( G `  u )
) ) )
389 eqid 2435 . . . . . . . . . . . . . . . 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 ) ) ) )
390 ovex 6098 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  X
)  -  ( F `
 u ) )  /  ( ( G `
 X )  -  ( G `  u ) ) )  e.  _V
391388, 389, 390fvmpt 5798 . . . . . . . . . . . . . . 15  |-  ( u  e.  ( A (,) X )  ->  (
( z  e.  ( A (,) X ) 
|->  ( ( ( F `
 X )  -  ( F `  z ) )  /  ( ( G `  X )  -  ( G `  z ) ) ) ) `  u )