Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fperdvper Structured version   Unicode version

Theorem fperdvper 37616
Description: The derivative of a periodic function is periodic (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fperdvper.f  |-  ( ph  ->  F : RR --> CC )
fperdvper.t  |-  ( ph  ->  T  e.  RR )
fperdvper.fper  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( x  +  T ) )  =  ( F `  x
) )
fperdvper.g  |-  G  =  ( RR  _D  F
)
Assertion
Ref Expression
fperdvper  |-  ( (
ph  /\  x  e.  dom  G )  ->  (
( x  +  T
)  e.  dom  G  /\  ( G `  (
x  +  T ) )  =  ( G `
 x ) ) )
Distinct variable groups:    x, F    x, T    ph, x
Allowed substitution hint:    G( x)

Proof of Theorem fperdvper
Dummy variables  a 
b  c  d  w  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvbsss 22849 . . . . . . . 8  |-  dom  ( RR  _D  F )  C_  RR
2 id 23 . . . . . . . . 9  |-  ( x  e.  dom  G  ->  x  e.  dom  G )
3 fperdvper.g . . . . . . . . . 10  |-  G  =  ( RR  _D  F
)
43dmeqi 5053 . . . . . . . . 9  |-  dom  G  =  dom  ( RR  _D  F )
52, 4syl6eleq 2521 . . . . . . . 8  |-  ( x  e.  dom  G  ->  x  e.  dom  ( RR 
_D  F ) )
61, 5sseldi 3463 . . . . . . 7  |-  ( x  e.  dom  G  ->  x  e.  RR )
76adantl 468 . . . . . 6  |-  ( (
ph  /\  x  e.  dom  G )  ->  x  e.  RR )
8 fperdvper.t . . . . . . 7  |-  ( ph  ->  T  e.  RR )
98adantr 467 . . . . . 6  |-  ( (
ph  /\  x  e.  dom  G )  ->  T  e.  RR )
107, 9readdcld 9672 . . . . 5  |-  ( (
ph  /\  x  e.  dom  G )  ->  (
x  +  T )  e.  RR )
11 reopn 37350 . . . . . . 7  |-  RR  e.  ( topGen `  ran  (,) )
12 retop 21774 . . . . . . . 8  |-  ( topGen ` 
ran  (,) )  e.  Top
13 ssid 3484 . . . . . . . . 9  |-  RR  C_  RR
1413a1i 11 . . . . . . . 8  |-  ( (
ph  /\  x  e.  dom  G )  ->  RR  C_  RR )
15 uniretop 21775 . . . . . . . . 9  |-  RR  =  U. ( topGen `  ran  (,) )
1615isopn3 20074 . . . . . . . 8  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  RR  C_  RR )  ->  ( RR  e.  ( topGen `  ran  (,) )  <->  ( ( int `  ( topGen `  ran  (,) )
) `  RR )  =  RR ) )
1712, 14, 16sylancr 668 . . . . . . 7  |-  ( (
ph  /\  x  e.  dom  G )  ->  ( RR  e.  ( topGen `  ran  (,) )  <->  ( ( int `  ( topGen `  ran  (,) )
) `  RR )  =  RR ) )
1811, 17mpbii 215 . . . . . 6  |-  ( (
ph  /\  x  e.  dom  G )  ->  (
( int `  ( topGen `
 ran  (,) )
) `  RR )  =  RR )
1918eqcomd 2431 . . . . 5  |-  ( (
ph  /\  x  e.  dom  G )  ->  RR  =  ( ( int `  ( topGen `  ran  (,) )
) `  RR )
)
2010, 19eleqtrd 2513 . . . 4  |-  ( (
ph  /\  x  e.  dom  G )  ->  (
x  +  T )  e.  ( ( int `  ( topGen `  ran  (,) )
) `  RR )
)
215adantl 468 . . . . . . . 8  |-  ( (
ph  /\  x  e.  dom  G )  ->  x  e.  dom  ( RR  _D  F ) )
223fveq1i 5880 . . . . . . . . . 10  |-  ( G `
 x )  =  ( ( RR  _D  F ) `  x
)
2322eqcomi 2436 . . . . . . . . 9  |-  ( ( RR  _D  F ) `
 x )  =  ( G `  x
)
2423a1i 11 . . . . . . . 8  |-  ( (
ph  /\  x  e.  dom  G )  ->  (
( RR  _D  F
) `  x )  =  ( G `  x ) )
25 dvf 22854 . . . . . . . . . . . 12  |-  ( RR 
_D  F ) : dom  ( RR  _D  F ) --> CC
26 ffun 5746 . . . . . . . . . . . 12  |-  ( ( RR  _D  F ) : dom  ( RR 
_D  F ) --> CC 
->  Fun  ( RR  _D  F ) )
2725, 26ax-mp 5 . . . . . . . . . . 11  |-  Fun  ( RR  _D  F )
2827a1i 11 . . . . . . . . . 10  |-  ( ph  ->  Fun  ( RR  _D  F ) )
29 funbrfv2b 5923 . . . . . . . . . 10  |-  ( Fun  ( RR  _D  F
)  ->  ( x
( RR  _D  F
) ( G `  x )  <->  ( x  e.  dom  ( RR  _D  F )  /\  (
( RR  _D  F
) `  x )  =  ( G `  x ) ) ) )
3028, 29syl 17 . . . . . . . . 9  |-  ( ph  ->  ( x ( RR 
_D  F ) ( G `  x )  <-> 
( x  e.  dom  ( RR  _D  F
)  /\  ( ( RR  _D  F ) `  x )  =  ( G `  x ) ) ) )
3130adantr 467 . . . . . . . 8  |-  ( (
ph  /\  x  e.  dom  G )  ->  (
x ( RR  _D  F ) ( G `
 x )  <->  ( x  e.  dom  ( RR  _D  F )  /\  (
( RR  _D  F
) `  x )  =  ( G `  x ) ) ) )
3221, 24, 31mpbir2and 931 . . . . . . 7  |-  ( (
ph  /\  x  e.  dom  G )  ->  x
( RR  _D  F
) ( G `  x ) )
33 eqid 2423 . . . . . . . . 9  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
3433tgioo2 21813 . . . . . . . 8  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
35 eqid 2423 . . . . . . . 8  |-  ( y  e.  ( RR  \  { x } ) 
|->  ( ( ( F `
 y )  -  ( F `  x ) )  /  ( y  -  x ) ) )  =  ( y  e.  ( RR  \  { x } ) 
|->  ( ( ( F `
 y )  -  ( F `  x ) )  /  ( y  -  x ) ) )
36 ax-resscn 9598 . . . . . . . . 9  |-  RR  C_  CC
3736a1i 11 . . . . . . . 8  |-  ( (
ph  /\  x  e.  dom  G )  ->  RR  C_  CC )
38 fperdvper.f . . . . . . . . 9  |-  ( ph  ->  F : RR --> CC )
3938adantr 467 . . . . . . . 8  |-  ( (
ph  /\  x  e.  dom  G )  ->  F : RR --> CC )
4034, 33, 35, 37, 39, 14eldv 22845 . . . . . . 7  |-  ( (
ph  /\  x  e.  dom  G )  ->  (
x ( RR  _D  F ) ( G `
 x )  <->  ( x  e.  ( ( int `  ( topGen `
 ran  (,) )
) `  RR )  /\  ( G `  x
)  e.  ( ( y  e.  ( RR 
\  { x }
)  |->  ( ( ( F `  y )  -  ( F `  x ) )  / 
( y  -  x
) ) ) lim CC  x ) ) ) )
4132, 40mpbid 214 . . . . . 6  |-  ( (
ph  /\  x  e.  dom  G )  ->  (
x  e.  ( ( int `  ( topGen ` 
ran  (,) ) ) `  RR )  /\  ( G `  x )  e.  ( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) lim CC  x ) ) )
4241simprd 465 . . . . 5  |-  ( (
ph  /\  x  e.  dom  G )  ->  ( G `  x )  e.  ( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) lim CC  x ) )
43 eqidd 2424 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( y  e.  ( RR  \  {
( x  +  T
) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) )  =  ( y  e.  ( RR  \  {
( x  +  T
) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) )
44 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  d  ->  ( F `  y )  =  ( F `  d ) )
4544oveq1d 6318 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  d  ->  (
( F `  y
)  -  ( F `
 ( x  +  T ) ) )  =  ( ( F `
 d )  -  ( F `  ( x  +  T ) ) ) )
46 oveq1 6310 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  d  ->  (
y  -  ( x  +  T ) )  =  ( d  -  ( x  +  T
) ) )
4745, 46oveq12d 6321 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  d  ->  (
( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) )  =  ( ( ( F `
 d )  -  ( F `  ( x  +  T ) ) )  /  ( d  -  ( x  +  T ) ) ) )
48 eldifi 3588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( d  e.  ( RR  \  { ( x  +  T ) } )  ->  d  e.  RR )
4948recnd 9671 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( d  e.  ( RR  \  { ( x  +  T ) } )  ->  d  e.  CC )
5049adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  -> 
d  e.  CC )
518recnd 9671 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  T  e.  CC )
5251adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  T  e.  CC )
5350, 52npcand 9992 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  -> 
( ( d  -  T )  +  T
)  =  d )
5453eqcomd 2431 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  -> 
d  =  ( ( d  -  T )  +  T ) )
5554fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  -> 
( F `  d
)  =  ( F `
 ( ( d  -  T )  +  T ) ) )
56 ovex 6331 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( d  -  T )  e. 
_V
5748adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  -> 
d  e.  RR )
588adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  T  e.  RR )
5957, 58resubcld 10049 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  -> 
( d  -  T
)  e.  RR )
6059ex 436 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( d  e.  ( RR  \  { ( x  +  T ) } )  ->  (
d  -  T )  e.  RR ) )
6160imdistani 695 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  -> 
( ph  /\  (
d  -  T )  e.  RR ) )
62 eleq1 2495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  =  ( d  -  T )  ->  (
x  e.  RR  <->  ( d  -  T )  e.  RR ) )
6362anbi2d 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  =  ( d  -  T )  ->  (
( ph  /\  x  e.  RR )  <->  ( ph  /\  ( d  -  T
)  e.  RR ) ) )
64 oveq1 6310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( x  =  ( d  -  T )  ->  (
x  +  T )  =  ( ( d  -  T )  +  T ) )
6564fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  =  ( d  -  T )  ->  ( F `  ( x  +  T ) )  =  ( F `  (
( d  -  T
)  +  T ) ) )
66 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  =  ( d  -  T )  ->  ( F `  x )  =  ( F `  ( d  -  T
) ) )
6765, 66eqeq12d 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  =  ( d  -  T )  ->  (
( F `  (
x  +  T ) )  =  ( F `
 x )  <->  ( F `  ( ( d  -  T )  +  T
) )  =  ( F `  ( d  -  T ) ) ) )
6863, 67imbi12d 322 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  =  ( d  -  T )  ->  (
( ( ph  /\  x  e.  RR )  ->  ( F `  (
x  +  T ) )  =  ( F `
 x ) )  <-> 
( ( ph  /\  ( d  -  T
)  e.  RR )  ->  ( F `  ( ( d  -  T )  +  T
) )  =  ( F `  ( d  -  T ) ) ) ) )
69 fperdvper.fper . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( x  +  T ) )  =  ( F `  x
) )
7068, 69vtoclg 3140 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( d  -  T )  e.  _V  ->  (
( ph  /\  (
d  -  T )  e.  RR )  -> 
( F `  (
( d  -  T
)  +  T ) )  =  ( F `
 ( d  -  T ) ) ) )
7156, 61, 70mpsyl 66 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  -> 
( F `  (
( d  -  T
)  +  T ) )  =  ( F `
 ( d  -  T ) ) )
7255, 71eqtrd 2464 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  -> 
( F `  d
)  =  ( F `
 ( d  -  T ) ) )
7372adantlr 720 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( F `  d )  =  ( F `  ( d  -  T ) ) )
74 simpll 759 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ph )
756ad2antlr 732 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  x  e.  RR )
7674, 75, 69syl2anc 666 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( F `  ( x  +  T
) )  =  ( F `  x ) )
7773, 76oveq12d 6321 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( ( F `  d )  -  ( F `  ( x  +  T
) ) )  =  ( ( F `  ( d  -  T
) )  -  ( F `  x )
) )
7849adantl 468 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  d  e.  CC )
7974, 51syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  T  e.  CC )
807recnd 9671 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  x  e.  dom  G )  ->  x  e.  CC )
8180adantr 467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  x  e.  CC )
8278, 79, 81subsub4d 10019 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( (
d  -  T )  -  x )  =  ( d  -  ( T  +  x )
) )
8379, 81addcomd 9837 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( T  +  x )  =  ( x  +  T ) )
8483oveq2d 6319 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( d  -  ( T  +  x ) )  =  ( d  -  (
x  +  T ) ) )
8582, 84eqtr2d 2465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( d  -  ( x  +  T ) )  =  ( ( d  -  T )  -  x
) )
8677, 85oveq12d 6321 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( (
( F `  d
)  -  ( F `
 ( x  +  T ) ) )  /  ( d  -  ( x  +  T
) ) )  =  ( ( ( F `
 ( d  -  T ) )  -  ( F `  x ) )  /  ( ( d  -  T )  -  x ) ) )
8747, 86sylan9eqr 2486 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  y  =  d )  ->  ( ( ( F `
 y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T ) ) )  =  ( ( ( F `  ( d  -  T ) )  -  ( F `  x ) )  / 
( ( d  -  T )  -  x
) ) )
88 simpr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  d  e.  ( RR  \  { ( x  +  T ) } ) )
8938adantr 467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  F : RR --> CC )
9089, 59ffvelrnd 6036 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  -> 
( F `  (
d  -  T ) )  e.  CC )
9190adantlr 720 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( F `  ( d  -  T
) )  e.  CC )
9239, 7ffvelrnd 6036 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  dom  G )  ->  ( F `  x )  e.  CC )
9392adantr 467 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( F `  x )  e.  CC )
9491, 93subcld 9988 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( ( F `  ( d  -  T ) )  -  ( F `  x ) )  e.  CC )
9578, 79subcld 9988 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( d  -  T )  e.  CC )
9695, 81subcld 9988 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( (
d  -  T )  -  x )  e.  CC )
97 simpr 463 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( d  -  T
)  =  x )  ->  ( d  -  T )  =  x )
9849ad2antlr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( d  -  T
)  =  x )  ->  d  e.  CC )
9979adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( d  -  T
)  =  x )  ->  T  e.  CC )
10081adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( d  -  T
)  =  x )  ->  x  e.  CC )
10198, 99, 100subadd2d 10007 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( d  -  T
)  =  x )  ->  ( ( d  -  T )  =  x  <->  ( x  +  T )  =  d ) )
10297, 101mpbid 214 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( d  -  T
)  =  x )  ->  ( x  +  T )  =  d )
103102eqcomd 2431 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( d  -  T
)  =  x )  ->  d  =  ( x  +  T ) )
104 eldifsni 4124 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( d  e.  ( RR  \  { ( x  +  T ) } )  ->  d  =/=  (
x  +  T ) )
105104ad2antlr 732 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( d  -  T
)  =  x )  ->  d  =/=  (
x  +  T ) )
106105neneqd 2626 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( d  -  T
)  =  x )  ->  -.  d  =  ( x  +  T
) )
107103, 106pm2.65da 579 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  -.  (
d  -  T )  =  x )
108107neqned 2628 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( d  -  T )  =/=  x
)
10995, 81, 108subne0d 9997 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( (
d  -  T )  -  x )  =/=  0 )
11094, 96, 109divcld 10385 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( (
( F `  (
d  -  T ) )  -  ( F `
 x ) )  /  ( ( d  -  T )  -  x ) )  e.  CC )
11143, 87, 88, 110fvmptd 5968 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( (
y  e.  ( RR 
\  { ( x  +  T ) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T
) ) )  / 
( y  -  (
x  +  T ) ) ) ) `  d )  =  ( ( ( F `  ( d  -  T
) )  -  ( F `  x )
)  /  ( ( d  -  T )  -  x ) ) )
112111oveq1d 6318 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( (
( y  e.  ( RR  \  { ( x  +  T ) } )  |->  ( ( ( F `  y
)  -  ( F `
 ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) `
 d )  -  w )  =  ( ( ( ( F `
 ( d  -  T ) )  -  ( F `  x ) )  /  ( ( d  -  T )  -  x ) )  -  w ) )
113112fveq2d 5883 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( abs `  ( ( ( y  e.  ( RR  \  { ( x  +  T ) } ) 
|->  ( ( ( F `
 y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T ) ) ) ) `  d )  -  w ) )  =  ( abs `  (
( ( ( F `
 ( d  -  T ) )  -  ( F `  x ) )  /  ( ( d  -  T )  -  x ) )  -  w ) ) )
114113adantr 467 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( d  =/=  (
x  +  T )  /\  ( abs `  (
d  -  ( x  +  T ) ) )  <  b ) )  ->  ( abs `  ( ( ( y  e.  ( RR  \  { ( x  +  T ) } ) 
|->  ( ( ( F `
 y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T ) ) ) ) `  d )  -  w ) )  =  ( abs `  (
( ( ( F `
 ( d  -  T ) )  -  ( F `  x ) )  /  ( ( d  -  T )  -  x ) )  -  w ) ) )
115114adantllr 724 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  A. c  e.  ( RR  \  {
x } ) ( ( c  =/=  x  /\  ( abs `  (
c  -  x ) )  <  b )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) `  c )  -  w ) )  <  a ) )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( d  =/=  (
x  +  T )  /\  ( abs `  (
d  -  ( x  +  T ) ) )  <  b ) )  ->  ( abs `  ( ( ( y  e.  ( RR  \  { ( x  +  T ) } ) 
|->  ( ( ( F `
 y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T ) ) ) ) `  d )  -  w ) )  =  ( abs `  (
( ( ( F `
 ( d  -  T ) )  -  ( F `  x ) )  /  ( ( d  -  T )  -  x ) )  -  w ) ) )
116 simpllr 768 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  A. c  e.  ( RR  \  {
x } ) ( ( c  =/=  x  /\  ( abs `  (
c  -  x ) )  <  b )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) `  c )  -  w ) )  <  a ) )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  ->  A. c  e.  ( RR  \  { x }
) ( ( c  =/=  x  /\  ( abs `  ( c  -  x ) )  < 
b )  ->  ( abs `  ( ( ( y  e.  ( RR 
\  { x }
)  |->  ( ( ( F `  y )  -  ( F `  x ) )  / 
( y  -  x
) ) ) `  c )  -  w
) )  <  a
) )
11748ad2antlr 732 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  A. c  e.  ( RR  \  {
x } ) ( ( c  =/=  x  /\  ( abs `  (
c  -  x ) )  <  b )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) `  c )  -  w ) )  <  a ) )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  -> 
d  e.  RR )
1188ad4antr 737 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  A. c  e.  ( RR  \  {
x } ) ( ( c  =/=  x  /\  ( abs `  (
c  -  x ) )  <  b )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) `  c )  -  w ) )  <  a ) )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  ->  T  e.  RR )
119117, 118resubcld 10049 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  A. c  e.  ( RR  \  {
x } ) ( ( c  =/=  x  /\  ( abs `  (
c  -  x ) )  <  b )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) `  c )  -  w ) )  <  a ) )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  -> 
( d  -  T
)  e.  RR )
120 elsni 4022 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( d  -  T )  e.  { x }  ->  ( d  -  T
)  =  x )
121107, 120nsyl 125 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  -.  (
d  -  T )  e.  { x }
)
122121adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  ->  -.  ( d  -  T
)  e.  { x } )
123122adantllr 724 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  A. c  e.  ( RR  \  {
x } ) ( ( c  =/=  x  /\  ( abs `  (
c  -  x ) )  <  b )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) `  c )  -  w ) )  <  a ) )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  ->  -.  ( d  -  T
)  e.  { x } )
124119, 123eldifd 3448 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  A. c  e.  ( RR  \  {
x } ) ( ( c  =/=  x  /\  ( abs `  (
c  -  x ) )  <  b )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) `  c )  -  w ) )  <  a ) )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  -> 
( d  -  T
)  e.  ( RR 
\  { x }
) )
125 neeq1 2706 . . . . . . . . . . . . . . . . . . . . 21  |-  ( c  =  ( d  -  T )  ->  (
c  =/=  x  <->  ( d  -  T )  =/=  x
) )
126 oveq1 6310 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( c  =  ( d  -  T )  ->  (
c  -  x )  =  ( ( d  -  T )  -  x ) )
127126fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( c  =  ( d  -  T )  ->  ( abs `  ( c  -  x ) )  =  ( abs `  (
( d  -  T
)  -  x ) ) )
128127breq1d 4431 . . . . . . . . . . . . . . . . . . . . 21  |-  ( c  =  ( d  -  T )  ->  (
( abs `  (
c  -  x ) )  <  b  <->  ( abs `  ( ( d  -  T )  -  x
) )  <  b
) )
129125, 128anbi12d 716 . . . . . . . . . . . . . . . . . . . 20  |-  ( c  =  ( d  -  T )  ->  (
( c  =/=  x  /\  ( abs `  (
c  -  x ) )  <  b )  <-> 
( ( d  -  T )  =/=  x  /\  ( abs `  (
( d  -  T
)  -  x ) )  <  b ) ) )
130 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( c  =  ( d  -  T )  ->  (
( y  e.  ( RR  \  { x } )  |->  ( ( ( F `  y
)  -  ( F `
 x ) )  /  ( y  -  x ) ) ) `
 c )  =  ( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) `  ( d  -  T ) ) )
131130oveq1d 6318 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( c  =  ( d  -  T )  ->  (
( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) `  c )  -  w )  =  ( ( ( y  e.  ( RR  \  { x } ) 
|->  ( ( ( F `
 y )  -  ( F `  x ) )  /  ( y  -  x ) ) ) `  ( d  -  T ) )  -  w ) )
132131fveq2d 5883 . . . . . . . . . . . . . . . . . . . . 21  |-  ( c  =  ( d  -  T )  ->  ( abs `  ( ( ( y  e.  ( RR 
\  { x }
)  |->  ( ( ( F `  y )  -  ( F `  x ) )  / 
( y  -  x
) ) ) `  c )  -  w
) )  =  ( abs `  ( ( ( y  e.  ( RR  \  { x } )  |->  ( ( ( F `  y
)  -  ( F `
 x ) )  /  ( y  -  x ) ) ) `
 ( d  -  T ) )  -  w ) ) )
133132breq1d 4431 . . . . . . . . . . . . . . . . . . . 20  |-  ( c  =  ( d  -  T )  ->  (
( abs `  (
( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) `  c )  -  w ) )  <  a  <->  ( abs `  ( ( ( y  e.  ( RR  \  { x } ) 
|->  ( ( ( F `
 y )  -  ( F `  x ) )  /  ( y  -  x ) ) ) `  ( d  -  T ) )  -  w ) )  <  a ) )
134129, 133imbi12d 322 . . . . . . . . . . . . . . . . . . 19  |-  ( c  =  ( d  -  T )  ->  (
( ( c  =/=  x  /\  ( abs `  ( c  -  x
) )  <  b
)  ->  ( abs `  ( ( ( y  e.  ( RR  \  { x } ) 
|->  ( ( ( F `
 y )  -  ( F `  x ) )  /  ( y  -  x ) ) ) `  c )  -  w ) )  <  a )  <->  ( (
( d  -  T
)  =/=  x  /\  ( abs `  ( ( d  -  T )  -  x ) )  <  b )  -> 
( abs `  (
( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) `  ( d  -  T ) )  -  w ) )  <  a ) ) )
135134rspccva 3182 . . . . . . . . . . . . . . . . . 18  |-  ( ( A. c  e.  ( RR  \  { x } ) ( ( c  =/=  x  /\  ( abs `  ( c  -  x ) )  <  b )  -> 
( abs `  (
( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) `  c )  -  w ) )  <  a )  /\  ( d  -  T
)  e.  ( RR 
\  { x }
) )  ->  (
( ( d  -  T )  =/=  x  /\  ( abs `  (
( d  -  T
)  -  x ) )  <  b )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) `  ( d  -  T ) )  -  w ) )  <  a ) )
136116, 124, 135syl2anc 666 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  A. c  e.  ( RR  \  {
x } ) ( ( c  =/=  x  /\  ( abs `  (
c  -  x ) )  <  b )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) `  c )  -  w ) )  <  a ) )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  -> 
( ( ( d  -  T )  =/=  x  /\  ( abs `  ( ( d  -  T )  -  x
) )  <  b
)  ->  ( abs `  ( ( ( y  e.  ( RR  \  { x } ) 
|->  ( ( ( F `
 y )  -  ( F `  x ) )  /  ( y  -  x ) ) ) `  ( d  -  T ) )  -  w ) )  <  a ) )
137 eqidd 2424 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) )  =  ( y  e.  ( RR  \  { x } ) 
|->  ( ( ( F `
 y )  -  ( F `  x ) )  /  ( y  -  x ) ) ) )
138 simpr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  y  =  ( d  -  T ) )  -> 
y  =  ( d  -  T ) )
139138fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  y  =  ( d  -  T ) )  -> 
( F `  y
)  =  ( F `
 ( d  -  T ) ) )
140139oveq1d 6318 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  y  =  ( d  -  T ) )  -> 
( ( F `  y )  -  ( F `  x )
)  =  ( ( F `  ( d  -  T ) )  -  ( F `  x ) ) )
141138oveq1d 6318 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  y  =  ( d  -  T ) )  -> 
( y  -  x
)  =  ( ( d  -  T )  -  x ) )
142140, 141oveq12d 6321 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  y  =  ( d  -  T ) )  -> 
( ( ( F `
 y )  -  ( F `  x ) )  /  ( y  -  x ) )  =  ( ( ( F `  ( d  -  T ) )  -  ( F `  x ) )  / 
( ( d  -  T )  -  x
) ) )
14348adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  d  e.  RR )
14474, 8syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  T  e.  RR )
145143, 144resubcld 10049 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( d  -  T )  e.  RR )
146145, 121eldifd 3448 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( d  -  T )  e.  ( RR  \  { x } ) )
147137, 142, 146, 110fvmptd 5968 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( (
y  e.  ( RR 
\  { x }
)  |->  ( ( ( F `  y )  -  ( F `  x ) )  / 
( y  -  x
) ) ) `  ( d  -  T
) )  =  ( ( ( F `  ( d  -  T
) )  -  ( F `  x )
)  /  ( ( d  -  T )  -  x ) ) )
148147eqcomd 2431 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( (
( F `  (
d  -  T ) )  -  ( F `
 x ) )  /  ( ( d  -  T )  -  x ) )  =  ( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) `  ( d  -  T ) ) )
149148ad2antrr 731 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  /\  ( ( ( d  -  T )  =/=  x  /\  ( abs `  ( ( d  -  T )  -  x
) )  <  b
)  ->  ( abs `  ( ( ( y  e.  ( RR  \  { x } ) 
|->  ( ( ( F `
 y )  -  ( F `  x ) )  /  ( y  -  x ) ) ) `  ( d  -  T ) )  -  w ) )  <  a ) )  ->  ( ( ( F `  ( d  -  T ) )  -  ( F `  x ) )  / 
( ( d  -  T )  -  x
) )  =  ( ( y  e.  ( RR  \  { x } )  |->  ( ( ( F `  y
)  -  ( F `
 x ) )  /  ( y  -  x ) ) ) `
 ( d  -  T ) ) )
150149oveq1d 6318 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  /\  ( ( ( d  -  T )  =/=  x  /\  ( abs `  ( ( d  -  T )  -  x
) )  <  b
)  ->  ( abs `  ( ( ( y  e.  ( RR  \  { x } ) 
|->  ( ( ( F `
 y )  -  ( F `  x ) )  /  ( y  -  x ) ) ) `  ( d  -  T ) )  -  w ) )  <  a ) )  ->  ( ( ( ( F `  (
d  -  T ) )  -  ( F `
 x ) )  /  ( ( d  -  T )  -  x ) )  -  w )  =  ( ( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) `  ( d  -  T ) )  -  w ) )
151150fveq2d 5883 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  /\  ( ( ( d  -  T )  =/=  x  /\  ( abs `  ( ( d  -  T )  -  x
) )  <  b
)  ->  ( abs `  ( ( ( y  e.  ( RR  \  { x } ) 
|->  ( ( ( F `
 y )  -  ( F `  x ) )  /  ( y  -  x ) ) ) `  ( d  -  T ) )  -  w ) )  <  a ) )  ->  ( abs `  (
( ( ( F `
 ( d  -  T ) )  -  ( F `  x ) )  /  ( ( d  -  T )  -  x ) )  -  w ) )  =  ( abs `  (
( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) `  ( d  -  T ) )  -  w ) ) )
152108adantr 467 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  -> 
( d  -  T
)  =/=  x )
15385eqcomd 2431 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( (
d  -  T )  -  x )  =  ( d  -  (
x  +  T ) ) )
154153adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  -> 
( ( d  -  T )  -  x
)  =  ( d  -  ( x  +  T ) ) )
155154fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  -> 
( abs `  (
( d  -  T
)  -  x ) )  =  ( abs `  ( d  -  (
x  +  T ) ) ) )
156 simpr 463 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  -> 
( abs `  (
d  -  ( x  +  T ) ) )  <  b )
157155, 156eqbrtrd 4442 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  -> 
( abs `  (
( d  -  T
)  -  x ) )  <  b )
158152, 157jca 535 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  -> 
( ( d  -  T )  =/=  x  /\  ( abs `  (
( d  -  T
)  -  x ) )  <  b ) )
159158adantr 467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  /\  ( ( ( d  -  T )  =/=  x  /\  ( abs `  ( ( d  -  T )  -  x
) )  <  b
)  ->  ( abs `  ( ( ( y  e.  ( RR  \  { x } ) 
|->  ( ( ( F `
 y )  -  ( F `  x ) )  /  ( y  -  x ) ) ) `  ( d  -  T ) )  -  w ) )  <  a ) )  ->  ( ( d  -  T )  =/=  x  /\  ( abs `  ( ( d  -  T )  -  x
) )  <  b
) )
160 simpr 463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  /\  ( ( ( d  -  T )  =/=  x  /\  ( abs `  ( ( d  -  T )  -  x
) )  <  b
)  ->  ( abs `  ( ( ( y  e.  ( RR  \  { x } ) 
|->  ( ( ( F `
 y )  -  ( F `  x ) )  /  ( y  -  x ) ) ) `  ( d  -  T ) )  -  w ) )  <  a ) )  ->  ( ( ( d  -  T )  =/=  x  /\  ( abs `  ( ( d  -  T )  -  x ) )  < 
b )  ->  ( abs `  ( ( ( y  e.  ( RR 
\  { x }
)  |->  ( ( ( F `  y )  -  ( F `  x ) )  / 
( y  -  x
) ) ) `  ( d  -  T
) )  -  w
) )  <  a
) )
161159, 160mpd 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  /\  ( ( ( d  -  T )  =/=  x  /\  ( abs `  ( ( d  -  T )  -  x
) )  <  b
)  ->  ( abs `  ( ( ( y  e.  ( RR  \  { x } ) 
|->  ( ( ( F `
 y )  -  ( F `  x ) )  /  ( y  -  x ) ) ) `  ( d  -  T ) )  -  w ) )  <  a ) )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) `  ( d  -  T ) )  -  w ) )  <  a )
162151, 161eqbrtrd 4442 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  /\  ( ( ( d  -  T )  =/=  x  /\  ( abs `  ( ( d  -  T )  -  x
) )  <  b
)  ->  ( abs `  ( ( ( y  e.  ( RR  \  { x } ) 
|->  ( ( ( F `
 y )  -  ( F `  x ) )  /  ( y  -  x ) ) ) `  ( d  -  T ) )  -  w ) )  <  a ) )  ->  ( abs `  (
( ( ( F `
 ( d  -  T ) )  -  ( F `  x ) )  /  ( ( d  -  T )  -  x ) )  -  w ) )  <  a )
163162ex 436 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  -> 
( ( ( ( d  -  T )  =/=  x  /\  ( abs `  ( ( d  -  T )  -  x ) )  < 
b )  ->  ( abs `  ( ( ( y  e.  ( RR 
\  { x }
)  |->  ( ( ( F `  y )  -  ( F `  x ) )  / 
( y  -  x
) ) ) `  ( d  -  T
) )  -  w
) )  <  a
)  ->  ( abs `  ( ( ( ( F `  ( d  -  T ) )  -  ( F `  x ) )  / 
( ( d  -  T )  -  x
) )  -  w
) )  <  a
) )
164163adantllr 724 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  A. c  e.  ( RR  \  {
x } ) ( ( c  =/=  x  /\  ( abs `  (
c  -  x ) )  <  b )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) `  c )  -  w ) )  <  a ) )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  -> 
( ( ( ( d  -  T )  =/=  x  /\  ( abs `  ( ( d  -  T )  -  x ) )  < 
b )  ->  ( abs `  ( ( ( y  e.  ( RR 
\  { x }
)  |->  ( ( ( F `  y )  -  ( F `  x ) )  / 
( y  -  x
) ) ) `  ( d  -  T
) )  -  w
) )  <  a
)  ->  ( abs `  ( ( ( ( F `  ( d  -  T ) )  -  ( F `  x ) )  / 
( ( d  -  T )  -  x
) )  -  w
) )  <  a
) )
165136, 164mpd 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  A. c  e.  ( RR  \  {
x } ) ( ( c  =/=  x  /\  ( abs `  (
c  -  x ) )  <  b )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) `  c )  -  w ) )  <  a ) )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  -> 
( abs `  (
( ( ( F `
 ( d  -  T ) )  -  ( F `  x ) )  /  ( ( d  -  T )  -  x ) )  -  w ) )  <  a )
166165adantrl 721 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  A. c  e.  ( RR  \  {
x } ) ( ( c  =/=  x  /\  ( abs `  (
c  -  x ) )  <  b )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) `  c )  -  w ) )  <  a ) )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( d  =/=  (
x  +  T )  /\  ( abs `  (
d  -  ( x  +  T ) ) )  <  b ) )  ->  ( abs `  ( ( ( ( F `  ( d  -  T ) )  -  ( F `  x ) )  / 
( ( d  -  T )  -  x
) )  -  w
) )  <  a
)
167115, 166eqbrtrd 4442 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  A. c  e.  ( RR  \  {
x } ) ( ( c  =/=  x  /\  ( abs `  (
c  -  x ) )  <  b )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) `  c )  -  w ) )  <  a ) )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( d  =/=  (
x  +  T )  /\  ( abs `  (
d  -  ( x  +  T ) ) )  <  b ) )  ->  ( abs `  ( ( ( y  e.  ( RR  \  { ( x  +  T ) } ) 
|->  ( ( ( F `
 y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T ) ) ) ) `  d )  -  w ) )  <  a )
168167ex 436 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  A. c  e.  ( RR  \  {
x } ) ( ( c  =/=  x  /\  ( abs `  (
c  -  x ) )  <  b )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) `  c )  -  w ) )  <  a ) )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  -> 
( ( d  =/=  ( x  +  T
)  /\  ( abs `  ( d  -  (
x  +  T ) ) )  <  b
)  ->  ( abs `  ( ( ( y  e.  ( RR  \  { ( x  +  T ) } ) 
|->  ( ( ( F `
 y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T ) ) ) ) `  d )  -  w ) )  <  a ) )
169168ralrimiva 2840 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  A. c  e.  ( RR 
\  { x }
) ( ( c  =/=  x  /\  ( abs `  ( c  -  x ) )  < 
b )  ->  ( abs `  ( ( ( y  e.  ( RR 
\  { x }
)  |->  ( ( ( F `  y )  -  ( F `  x ) )  / 
( y  -  x
) ) ) `  c )  -  w
) )  <  a
) )  ->  A. d  e.  ( RR  \  {
( x  +  T
) } ) ( ( d  =/=  (
x  +  T )  /\  ( abs `  (
d  -  ( x  +  T ) ) )  <  b )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
( x  +  T
) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) `
 d )  -  w ) )  < 
a ) )
170 eqidd 2424 . . . . . . . . . . . . . . . . . . 19  |-  ( c  e.  ( RR  \  { x } )  ->  ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) )  =  ( y  e.  ( RR  \  { x } ) 
|->  ( ( ( F `
 y )  -  ( F `  x ) )  /  ( y  -  x ) ) ) )
171 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  c  ->  ( F `  y )  =  ( F `  c ) )
172171oveq1d 6318 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  c  ->  (
( F `  y
)  -  ( F `
 x ) )  =  ( ( F `
 c )  -  ( F `  x ) ) )
173 oveq1 6310 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  c  ->  (
y  -  x )  =  ( c  -  x ) )
174172, 173oveq12d 6321 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  c  ->  (
( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) )  =  ( ( ( F `  c )  -  ( F `  x ) )  / 
( c  -  x
) ) )
175174adantl 468 . . . . . . . . . . . . . . . . . . 19  |-  ( ( c  e.  ( RR 
\  { x }
)  /\  y  =  c )  ->  (
( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) )  =  ( ( ( F `  c )  -  ( F `  x ) )  / 
( c  -  x
) ) )
176 id 23 . . . . . . . . . . . . . . . . . . 19  |-  ( c  e.  ( RR  \  { x } )  ->  c  e.  ( RR  \  { x } ) )
177 ovex 6331 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( F `  c
)  -  ( F `
 x ) )  /  ( c  -  x ) )  e. 
_V
178177a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( c  e.  ( RR  \  { x } )  ->  ( ( ( F `  c )  -  ( F `  x ) )  / 
( c  -  x
) )  e.  _V )
179170, 175, 176, 178fvmptd 5968 . . . . . . . . . . . . . . . . . 18  |-  ( c  e.  ( RR  \  { x } )  ->  ( ( y  e.  ( RR  \  { x } ) 
|->  ( ( ( F `
 y )  -  ( F `  x ) )  /  ( y  -  x ) ) ) `  c )  =  ( ( ( F `  c )  -  ( F `  x ) )  / 
( c  -  x
) ) )
180179oveq1d 6318 . . . . . . . . . . . . . . . . 17  |-  ( c  e.  ( RR  \  { x } )  ->  ( ( ( y  e.  ( RR 
\  { x }
)  |->  ( ( ( F `  y )  -  ( F `  x ) )  / 
( y  -  x
) ) ) `  c )  -  w
)  =  ( ( ( ( F `  c )  -  ( F `  x )
)  /  ( c  -  x ) )  -  w ) )
181180fveq2d 5883 . . . . . . . . . . . . . . . 16  |-  ( c  e.  ( RR  \  { x } )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) `  c )  -  w ) )  =  ( abs `  (
( ( ( F `
 c )  -  ( F `  x ) )  /  ( c  -  x ) )  -  w ) ) )
182181ad2antlr 732 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  A. d  e.  ( RR  \  {
( x  +  T
) } ) ( ( d  =/=  (
x  +  T )  /\  ( abs `  (
d  -  ( x  +  T ) ) )  <  b )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
( x  +  T
) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) `
 d )  -  w ) )  < 
a ) )  /\  c  e.  ( RR  \  { x } ) )  /\  ( c  =/=  x  /\  ( abs `  ( c  -  x ) )  < 
b ) )  -> 
( abs `  (
( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) `  c )  -  w ) )  =  ( abs `  (
( ( ( F `
 c )  -  ( F `  x ) )  /  ( c  -  x ) )  -  w ) ) )
183 simpll 759 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  ph )
184 eldifi 3588 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( c  e.  ( RR  \  { x } )  ->  c  e.  RR )
185184adantl 468 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  c  e.  RR )
186 eleq1 2495 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  =  c  ->  (
x  e.  RR  <->  c  e.  RR ) )
187186anbi2d 709 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  =  c  ->  (
( ph  /\  x  e.  RR )  <->  ( ph  /\  c  e.  RR ) ) )
188 oveq1 6310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  =  c  ->  (
x  +  T )  =  ( c  +  T ) )
189188fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  =  c  ->  ( F `  ( x  +  T ) )  =  ( F `  (
c  +  T ) ) )
190 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  =  c  ->  ( F `  x )  =  ( F `  c ) )
191189, 190eqeq12d 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  =  c  ->  (
( F `  (
x  +  T ) )  =  ( F `
 x )  <->  ( F `  ( c  +  T
) )  =  ( F `  c ) ) )
192187, 191imbi12d 322 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  c  ->  (
( ( ph  /\  x  e.  RR )  ->  ( F `  (
x  +  T ) )  =  ( F `
 x ) )  <-> 
( ( ph  /\  c  e.  RR )  ->  ( F `  (
c  +  T ) )  =  ( F `
 c ) ) ) )
193192, 69chvarv 2069 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  c  e.  RR )  ->  ( F `
 ( c  +  T ) )  =  ( F `  c
) )
194193eqcomd 2431 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  c  e.  RR )  ->  ( F `
 c )  =  ( F `  (
c  +  T ) ) )
195183, 185, 194syl2anc 666 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  ( F `  c )  =  ( F `  ( c  +  T ) ) )
1966ad2antlr 732 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  x  e.  RR )
197183, 196, 69syl2anc 666 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  ( F `  ( x  +  T
) )  =  ( F `  x ) )
198197eqcomd 2431 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  ( F `  x )  =  ( F `  ( x  +  T ) ) )
199195, 198oveq12d 6321 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  ( ( F `  c )  -  ( F `  x ) )  =  ( ( F `  ( c  +  T
) )  -  ( F `  ( x  +  T ) ) ) )
200185recnd 9671 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  c  e.  CC )
20180adantr 467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  x  e.  CC )
202183, 51syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  T  e.  CC )
203200, 201, 202pnpcan2d 10026 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  ( (
c  +  T )  -  ( x  +  T ) )  =  ( c  -  x
) )
204203eqcomd 2431 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  ( c  -  x )  =  ( ( c  +  T
)  -  ( x  +  T ) ) )
205199, 204oveq12d 6321 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  ( (
( F `  c
)  -  ( F `
 x ) )  /  ( c  -  x ) )  =  ( ( ( F `
 ( c  +  T ) )  -  ( F `  ( x  +  T ) ) )  /  ( ( c  +  T )  -  ( x  +  T ) ) ) )
206205oveq1d 6318 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  ( (
( ( F `  c )  -  ( F `  x )
)  /  ( c  -  x ) )  -  w )  =  ( ( ( ( F `  ( c  +  T ) )  -  ( F `  ( x  +  T
) ) )  / 
( ( c  +  T )  -  (
x  +  T ) ) )  -  w
) )
207206fveq2d 5883 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  ( abs `  ( ( ( ( F `  c )  -  ( F `  x ) )  / 
( c  -  x
) )  -  w
) )  =  ( abs `  ( ( ( ( F `  ( c  +  T
) )  -  ( F `  ( x  +  T ) ) )  /  ( ( c  +  T )  -  ( x  +  T
) ) )  -  w ) ) )
208207adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  /\  ( abs `  ( c  -  x ) )  <  b )  -> 
( abs `  (
( ( ( F `
 c )  -  ( F `  x ) )  /  ( c  -  x ) )  -  w ) )  =  ( abs `  (
( ( ( F `
 ( c  +  T ) )  -  ( F `  ( x  +  T ) ) )  /  ( ( c  +  T )  -  ( x  +  T ) ) )  -  w ) ) )
209208adantllr 724 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  A. d  e.  ( RR  \  {
( x  +  T
) } ) ( ( d  =/=  (
x  +  T )  /\  ( abs `  (
d  -  ( x  +  T ) ) )  <  b )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
( x  +  T
) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) `
 d )  -  w ) )  < 
a ) )  /\  c  e.  ( RR  \  { x } ) )  /\  ( abs `  ( c  -  x
) )  <  b
)  ->  ( abs `  ( ( ( ( F `  c )  -  ( F `  x ) )  / 
( c  -  x
) )  -  w
) )  =  ( abs `  ( ( ( ( F `  ( c  +  T
) )  -  ( F `  ( x  +  T ) ) )  /  ( ( c  +  T )  -  ( x  +  T
) ) )  -  w ) ) )
210 simpllr 768 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  A. d  e.  ( RR  \  {
( x  +  T
) } ) ( ( d  =/=  (
x  +  T )  /\  ( abs `  (
d  -  ( x  +  T ) ) )  <  b )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
( x  +  T
) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) `
 d )  -  w ) )  < 
a ) )  /\  c  e.  ( RR  \  { x } ) )  /\  ( abs `  ( c  -  x
) )  <  b
)  ->  A. d  e.  ( RR  \  {
( x  +  T
) } ) ( ( d  =/=  (
x  +  T )  /\  ( abs `  (
d  -  ( x  +  T ) ) )  <  b )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
( x  +  T
) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) `
 d )  -  w ) )  < 
a ) )
211184ad2antlr 732 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  A. d  e.  ( RR  \  {
( x  +  T
) } ) ( ( d  =/=  (
x  +  T )  /\  ( abs `  (
d  -  ( x  +  T ) ) )  <  b )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
( x  +  T
) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) `
 d )  -  w ) )  < 
a ) )  /\  c  e.  ( RR  \  { x } ) )  /\  ( abs `  ( c  -  x
) )  <  b
)  ->  c  e.  RR )
2128ad4antr 737 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  A. d  e.  ( RR  \  {
( x  +  T
) } ) ( ( d  =/=  (
x  +  T )  /\  ( abs `  (
d  -  ( x  +  T ) ) )  <  b )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
( x  +  T
) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) `
 d )  -  w ) )  < 
a ) )  /\  c  e.  ( RR  \  { x } ) )  /\  ( abs `  ( c  -  x
) )  <  b
)  ->  T  e.  RR )
213211, 212readdcld 9672 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  A. d  e.  ( RR  \  {
( x  +  T
) } ) ( ( d  =/=  (
x  +  T )  /\  ( abs `  (
d  -  ( x  +  T ) ) )  <  b )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
( x  +  T
) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) `
 d )  -  w ) )  < 
a ) )  /\  c  e.  ( RR  \  { x } ) )  /\  ( abs `  ( c  -  x
) )  <  b
)  ->  ( c  +  T )  e.  RR )
214 eldifsni 4124 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( c  e.  ( RR  \  { x } )  ->  c  =/=  x
)
215214adantl 468 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  c  =/=  x )
216200, 201, 202, 215addneintr2d 9843 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  ( c  +  T )  =/=  (
x  +  T ) )
217216adantr 467 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  /\  ( abs `  ( c  -  x ) )  <  b )  -> 
( c  +  T
)  =/=  ( x  +  T ) )
218217adantllr 724 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  A. d  e.  ( RR  \  {
( x  +  T
) } ) ( ( d  =/=  (
x  +  T )  /\  ( abs `  (
d  -  ( x  +  T ) ) )  <  b )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
( x  +  T
) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) `
 d )  -  w ) )  < 
a ) )  /\  c  e.  ( RR  \  { x } ) )  /\  ( abs `  ( c  -  x
) )  <  b
)  ->  ( c  +  T )  =/=  (
x  +  T ) )
219 elsni 4022 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( c  +  T )  e.  { ( x  +  T ) }  ->  ( c  +  T )  =  ( x  +  T ) )
220219necon3ai 2653 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( c  +  T )  =/=  ( x  +  T )  ->  -.  ( c  +  T
)  e.  { ( x  +  T ) } )
221218, 220syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  A. d  e.  ( RR  \  {
( x  +  T
) } ) ( ( d  =/=  (
x  +  T )  /\  ( abs `  (
d  -  ( x  +  T ) ) )  <  b )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
( x  +  T
) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) `
 d )  -  w ) )  < 
a ) )  /\  c  e.  ( RR  \  { x } ) )  /\  ( abs `  ( c  -  x
) )  <  b
)  ->  -.  (
c  +  T )  e.  { ( x  +  T ) } )
222213, 221eldifd 3448 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  A. d  e.  ( RR  \  {
( x  +  T
) } ) ( ( d  =/=  (
x  +  T )  /\  ( abs `  (
d  -  ( x  +  T ) ) )  <  b )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
( x  +  T
) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) `
 d )  -  w ) )  < 
a ) )  /\  c  e.  ( RR  \  { x } ) )  /\  ( abs `  ( c  -  x
) )  <  b
)  ->  ( c  +  T )  e.  ( RR  \  { ( x  +  T ) } ) )
223 neeq1 2706 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( d  =  ( c  +  T )  ->  (
d  =/=  ( x  +  T )  <->  ( c  +  T )  =/=  (
x  +  T ) ) )
224 oveq1 6310 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( d  =  ( c  +  T )  ->  (
d  -  ( x  +  T ) )  =  ( ( c  +  T )  -  ( x  +  T
) ) )
225224fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( d  =  ( c  +  T )  ->  ( abs `  ( d  -  ( x  +  T
) ) )  =  ( abs `  (
( c  +  T
)  -  ( x  +  T ) ) ) )
226225breq1d 4431 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( d  =  ( c  +  T )  ->  (
( abs `  (
d  -  ( x  +  T ) ) )  <  b  <->  ( abs `  ( ( c  +  T )  -  (
x  +  T ) ) )  <  b
) )
227223, 226anbi12d 716 . . . . . . . . . . . . . . . . . . . . 21  |-  ( d  =  ( c  +  T )  ->  (
( d  =/=  (
x  +  T )  /\  ( abs `  (
d  -  ( x  +  T ) ) )  <  b )  <-> 
( ( c  +  T )  =/=  (
x  +  T )  /\  ( abs `  (
( c  +  T
)  -  ( x  +  T ) ) )  <  b ) ) )
228 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( d  =  ( c  +  T )  ->  (
( y  e.  ( RR  \  { ( x  +  T ) } )  |->  ( ( ( F `  y
)  -  ( F `
 ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) `
 d )  =  ( ( y  e.  ( RR  \  {
( x  +  T
) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) `
 ( c  +  T ) ) )
229228oveq1d 6318 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( d  =  ( c  +  T )  ->  (
( ( y  e.  ( RR  \  {
( x  +  T
) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) `
 d )  -  w )  =  ( ( ( y  e.  ( RR  \  {
( x  +  T
) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) `
 ( c  +  T ) )  -  w ) )
230229fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( d  =  ( c  +  T )  ->  ( abs `  ( ( ( y  e.  ( RR 
\  { ( x  +  T ) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T
) ) )  / 
( y  -  (
x  +  T ) ) ) ) `  d )  -  w
) )  =  ( abs `  ( ( ( y  e.  ( RR  \  { ( x  +  T ) } )  |->  ( ( ( F `  y
)  -  ( F `
 ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) `
 ( c  +  T ) )  -  w ) ) )
231230breq1d 4431 . . . . . . . . . . . . . . . . . . . . 21  |-  ( d  =  ( c  +  T )  ->  (
( abs `  (
( ( y  e.  ( RR  \  {
( x  +  T
) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) `
 d )  -  w ) )  < 
a  <->  ( abs `  (
( ( y  e.  ( RR  \  {
( x  +  T
) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) `
 ( c  +  T ) )  -  w ) )  < 
a ) )
232227, 231imbi12d 322 . . . . . . . . . . . . . . . . . . . 20  |-  ( d  =  ( c  +  T )  ->  (
( ( d  =/=  ( x  +  T
)  /\  ( abs `  ( d  -  (
x  +  T ) ) )  <  b
)  ->  ( abs `  ( ( ( y  e.  ( RR  \  { ( x  +  T ) } ) 
|->  ( ( ( F `
 y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T ) ) ) ) `  d )  -  w ) )  <  a )  <->  ( (
( c  +  T
)  =/=  ( x  +  T )  /\  ( abs `  ( ( c  +  T )  -  ( x  +  T ) ) )  <  b )  -> 
( abs `  (
( ( y  e.  ( RR  \  {
( x  +  T
) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) `
 ( c  +  T ) )  -  w ) )  < 
a ) ) )
233232rspccva 3182 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A. d  e.  ( RR  \  { ( x  +  T ) } ) ( ( d  =/=  ( x  +  T )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  -> 
( abs `  (
( ( y  e.  ( RR  \  {
( x  +  T
) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) `
 d )  -  w ) )  < 
a )  /\  (
c  +  T )  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( (
( c  +  T
)  =/=  ( x  +  T )  /\  ( abs `  ( ( c  +  T )  -  ( x  +  T ) ) )  <  b )  -> 
( abs `  (
( ( y  e.  ( RR  \  {
( x  +  T
) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) `
 ( c  +  T ) )  -  w ) )  < 
a ) )
234210, 222, 233syl2anc 666 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  A. d  e.  ( RR  \  {
( x  +  T
) } ) ( ( d  =/=  (
x  +  T )  /\  ( abs `  (
d  -  ( x  +  T ) ) )  <  b )  ->  ( abs `  (
( ( y  e.  ( RR  \  {
( x  +  T
) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) `
 d )  -  w ) )  < 
a ) )  /\  c  e.  ( RR  \  { x } ) )  /\  ( abs `  ( c  -  x
) )  <  b
)  ->  ( (
( c  +  T
)  =/=  ( x  +  T )  /\  ( abs `  ( ( c  +  T )  -  ( x  +  T ) ) )  <  b )  -> 
( abs `  (
( ( y  e.  ( RR  \  {
( x  +  T
) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) `
 ( c  +  T ) )  -  w ) )  < 
a ) )
235 eqidd 2424 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  ( y  e.  ( RR  \  {
( x  +  T
) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) )  =  ( y  e.  ( RR  \  {
( x  +  T
) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) )
236 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  =  ( c  +  T )  ->  ( F `  y )  =  ( F `  ( c  +  T
) ) )
237236oveq1d 6318 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( y  =  ( c  +  T )  ->  (
( F `  y
)  -  ( F `
 ( x  +  T ) ) )  =  ( ( F `
 ( c  +  T ) )  -  ( F `  ( x  +  T ) ) ) )
238 oveq1 6310 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( y  =  ( c  +  T )  ->  (
y  -  ( x  +  T ) )  =  ( ( c  +  T )  -  ( x  +  T
) ) )
239237, 238oveq12d 6321 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  =  ( c  +  T )  ->  (
( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) )  =  ( ( ( F `
 ( c  +  T ) )  -  ( F `  ( x  +  T ) ) )  /  ( ( c  +  T )  -  ( x  +  T ) ) ) )
240239adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  /\  y  =  ( c  +  T ) )  -> 
( ( ( F `
 y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T ) ) )  =  ( ( ( F `  ( c  +  T ) )  -  ( F `  ( x  +  T
) ) )  / 
( ( c  +  T )  -  (
x  +  T ) ) ) )
241183, 8syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  T  e.  RR )
242185, 241readdcld 9672 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  ( c  +  T )  e.  RR )
243216, 220syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  -.  (
c  +  T )  e.  { ( x  +  T ) } )
244242, 243eldifd 3448 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  ( c  +  T )  e.  ( RR  \  { ( x  +  T ) } ) )
245205, 177syl6eqelr 2520 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  ( (
( F `  (
c  +  T ) )  -  ( F `
 ( x  +  T ) ) )  /  ( ( c  +  T )  -  ( x  +  T
) ) )  e. 
_V )
246235, 240, 244, 245fvmptd 5968 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  ( (
y  e.  ( RR 
\  { ( x  +  T ) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T
) ) )  / 
( y  -  (
x  +  T ) ) ) ) `  ( c  +  T
) )  =  ( ( ( F `  ( c  +  T
) )  -  ( F `  ( x  +  T ) ) )  /  ( ( c  +  T )  -  ( x  +  T
) ) ) )
247246eqcomd 2431 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  ( (
( F `  (
c  +  T ) )  -  ( F `
 ( x  +  T ) ) )  /  ( ( c  +  T )  -  ( x  +  T
) ) )  =  ( ( y  e.  ( RR  \  {
( x  +  T
) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) `
 ( c  +  T ) ) )
248247ad2antrr 731 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  c  e.  ( RR  \  { x } ) )  /\  ( abs `  ( c  -  x ) )  <  b )  /\  ( ( ( c  +  T )  =/=  ( x  +  T
)  /\  ( abs `  ( ( c  +  T )  -  (
x  +  T ) ) )  <  b
)  ->  ( abs `  ( ( ( y  e.  ( RR  \  { ( x  +  T ) } ) 
|->  ( ( ( F `
 y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T ) ) ) ) `  ( c  +  T ) )  -  w ) )  <  a ) )  ->  ( ( ( F `  ( c  +  T ) )  -  ( F `  ( x  +  T
) ) )  / 
( ( c  +  T )  -  (
x  +  T ) ) )  =  ( ( y  e.  ( RR  \  { ( x  +  T ) } )  |->  ( ( ( F `  y
)  -  ( F `
 ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) `
 ( c  +  T ) ) )
249248oveq1d 6318 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  c  e.  ( RR  \  { x } ) )  /\  ( abs `  ( c  -  x ) )  <  b )  /\  ( ( ( c  +  T )  =/=  ( x  +  T
)  /\  ( abs `  ( ( c  +  T )  -  (
x  +  T ) ) )  <  b
)  ->  ( abs `  ( ( ( y  e.  ( RR  \  { ( x  +  T ) } ) 
|->  ( ( ( F `
 y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T ) ) ) ) `  ( c  +  T ) )  -  w ) )  <  a ) )  ->  ( ( ( ( F `  (
c  +  T ) )  -  ( F `
 ( x  +  T ) ) )  /  ( ( c  +  T )  -  ( x  +  T
) ) )  -  w )  =  ( ( ( y  e.  ( RR  \  {
( x  +  T
) } )  |->  ( ( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) ) ) `
 ( c  +  T ) )  -  w ) )
250249fveq2d 5883 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  x  e.  dom  G
)  /\  c  e.  ( RR  \  { x } ) )  /\  ( abs `  ( c  -  x ) )  <  b )  /\  ( ( ( c  +  T )  =/=  ( x  +  T
)  /\  ( abs `  ( ( c  +  T )  -  (
x  +  T ) ) )  <