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

Theorem fperdvper 31571
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 dvf 22179 . . . . . . . . 9  |-  ( RR 
_D  F ) : dom  ( RR  _D  F ) --> CC
21a1i 11 . . . . . . . 8  |-  ( ph  ->  ( RR  _D  F
) : dom  ( RR  _D  F ) --> CC )
3 fperdvper.g . . . . . . . . . 10  |-  G  =  ( RR  _D  F
)
43a1i 11 . . . . . . . . 9  |-  ( ph  ->  G  =  ( RR 
_D  F ) )
54feq1d 5723 . . . . . . . 8  |-  ( ph  ->  ( G : dom  ( RR  _D  F
) --> CC  <->  ( RR  _D  F ) : dom  ( RR  _D  F
) --> CC ) )
62, 5mpbird 232 . . . . . . 7  |-  ( ph  ->  G : dom  ( RR  _D  F ) --> CC )
76adantr 465 . . . . . 6  |-  ( (
ph  /\  x  e.  dom  G )  ->  G : dom  ( RR  _D  F ) --> CC )
8 id 22 . . . . . . . 8  |-  ( x  e.  dom  G  ->  x  e.  dom  G )
93dmeqi 5210 . . . . . . . . 9  |-  dom  G  =  dom  ( RR  _D  F )
109a1i 11 . . . . . . . 8  |-  ( x  e.  dom  G  ->  dom  G  =  dom  ( RR  _D  F ) )
118, 10eleqtrd 2557 . . . . . . 7  |-  ( x  e.  dom  G  ->  x  e.  dom  ( RR 
_D  F ) )
1211adantl 466 . . . . . 6  |-  ( (
ph  /\  x  e.  dom  G )  ->  x  e.  dom  ( RR  _D  F ) )
137, 12ffvelrnd 6033 . . . . 5  |-  ( (
ph  /\  x  e.  dom  G )  ->  ( G `  x )  e.  CC )
14 dvbsss 22174 . . . . . . . . . . . . 13  |-  dom  ( RR  _D  F )  C_  RR
1514sseli 3505 . . . . . . . . . . . 12  |-  ( x  e.  dom  ( RR 
_D  F )  ->  x  e.  RR )
1611, 15syl 16 . . . . . . . . . . 11  |-  ( x  e.  dom  G  ->  x  e.  RR )
1716adantl 466 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  dom  G )  ->  x  e.  RR )
18 fperdvper.t . . . . . . . . . . 11  |-  ( ph  ->  T  e.  RR )
1918adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  dom  G )  ->  T  e.  RR )
2017, 19readdcld 9635 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  dom  G )  ->  (
x  +  T )  e.  RR )
21 reopn 31376 . . . . . . . . . . . 12  |-  RR  e.  ( topGen `  ran  (,) )
2221a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  dom  G )  ->  RR  e.  ( topGen `  ran  (,) )
)
23 retop 21136 . . . . . . . . . . . . 13  |-  ( topGen ` 
ran  (,) )  e.  Top
2423a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  dom  G )  ->  ( topGen `
 ran  (,) )  e.  Top )
25 ssid 3528 . . . . . . . . . . . . 13  |-  RR  C_  RR
2625a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  dom  G )  ->  RR  C_  RR )
27 uniretop 21137 . . . . . . . . . . . . 13  |-  RR  =  U. ( topGen `  ran  (,) )
2827isopn3 19435 . . . . . . . . . . . 12  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  RR  C_  RR )  ->  ( RR  e.  ( topGen `  ran  (,) )  <->  ( ( int `  ( topGen `  ran  (,) )
) `  RR )  =  RR ) )
2924, 26, 28syl2anc 661 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  dom  G )  ->  ( RR  e.  ( topGen `  ran  (,) )  <->  ( ( int `  ( topGen `  ran  (,) )
) `  RR )  =  RR ) )
3022, 29mpbid 210 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  dom  G )  ->  (
( int `  ( topGen `
 ran  (,) )
) `  RR )  =  RR )
3130eqcomd 2475 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  dom  G )  ->  RR  =  ( ( int `  ( topGen `  ran  (,) )
) `  RR )
)
3220, 31eleqtrd 2557 . . . . . . . 8  |-  ( (
ph  /\  x  e.  dom  G )  ->  (
x  +  T )  e.  ( ( int `  ( topGen `  ran  (,) )
) `  RR )
)
333fveq1i 5873 . . . . . . . . . . . . . . 15  |-  ( G `
 x )  =  ( ( RR  _D  F ) `  x
)
3433eqcomi 2480 . . . . . . . . . . . . . 14  |-  ( ( RR  _D  F ) `
 x )  =  ( G `  x
)
3534a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  dom  G )  ->  (
( RR  _D  F
) `  x )  =  ( G `  x ) )
3612, 35jca 532 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  dom  G )  ->  (
x  e.  dom  ( RR  _D  F )  /\  ( ( RR  _D  F ) `  x
)  =  ( G `
 x ) ) )
37 ffun 5739 . . . . . . . . . . . . . . . 16  |-  ( ( RR  _D  F ) : dom  ( RR 
_D  F ) --> CC 
->  Fun  ( RR  _D  F ) )
381, 37ax-mp 5 . . . . . . . . . . . . . . 15  |-  Fun  ( RR  _D  F )
3938a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  Fun  ( RR  _D  F ) )
40 funbrfv2b 5918 . . . . . . . . . . . . . 14  |-  ( Fun  ( RR  _D  F
)  ->  ( x
( RR  _D  F
) ( G `  x )  <->  ( x  e.  dom  ( RR  _D  F )  /\  (
( RR  _D  F
) `  x )  =  ( G `  x ) ) ) )
4139, 40syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( x ( RR 
_D  F ) ( G `  x )  <-> 
( x  e.  dom  ( RR  _D  F
)  /\  ( ( RR  _D  F ) `  x )  =  ( G `  x ) ) ) )
4241adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  dom  G )  ->  (
x ( RR  _D  F ) ( G `
 x )  <->  ( x  e.  dom  ( RR  _D  F )  /\  (
( RR  _D  F
) `  x )  =  ( G `  x ) ) ) )
4336, 42mpbird 232 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  dom  G )  ->  x
( RR  _D  F
) ( G `  x ) )
44 eqid 2467 . . . . . . . . . . . . 13  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
4544tgioo2 21176 . . . . . . . . . . . 12  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
46 eqid 2467 . . . . . . . . . . . 12  |-  ( y  e.  ( RR  \  { x } ) 
|->  ( ( ( F `
 y )  -  ( F `  x ) )  /  ( y  -  x ) ) )  =  ( y  e.  ( RR  \  { x } ) 
|->  ( ( ( F `
 y )  -  ( F `  x ) )  /  ( y  -  x ) ) )
47 ax-resscn 9561 . . . . . . . . . . . . 13  |-  RR  C_  CC
4847a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  dom  G )  ->  RR  C_  CC )
49 fperdvper.f . . . . . . . . . . . . 13  |-  ( ph  ->  F : RR --> CC )
5049adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  dom  G )  ->  F : RR --> CC )
5145, 44, 46, 48, 50, 26eldv 22170 . . . . . . . . . . 11  |-  ( (
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 ) ) ) )
5243, 51mpbid 210 . . . . . . . . . 10  |-  ( (
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 ) ) )
5352simprd 463 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  dom  G )  ->  ( G `  x )  e.  ( ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) ) lim CC  x ) )
54 nfv 1683 . . . . . . . . . . . 12  |-  F/ w
( ph  /\  x  e.  dom  G )
5550, 48, 17dvlem 22168 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  y  e.  ( RR  \  { x } ) )  ->  ( (
( F `  y
)  -  ( F `
 x ) )  /  ( y  -  x ) )  e.  CC )
5655, 46fmptd 6056 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  dom  G )  ->  (
y  e.  ( RR 
\  { x }
)  |->  ( ( ( F `  y )  -  ( F `  x ) )  / 
( y  -  x
) ) ) : ( RR  \  {
x } ) --> CC )
5748ssdifssd 3647 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  dom  G )  ->  ( RR  \  { x }
)  C_  CC )
5847, 17sseldi 3507 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  dom  G )  ->  x  e.  CC )
5956, 57, 58ellimc3 22151 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  dom  G )  ->  (
w  e.  ( ( y  e.  ( RR 
\  { x }
)  |->  ( ( ( F `  y )  -  ( F `  x ) )  / 
( y  -  x
) ) ) lim CC  x )  <->  ( w  e.  CC  /\  A. a  e.  RR+  E. b  e.  RR+  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 ) ) ) )
60 eqidd 2468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( 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
) ) ) ) )
61 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  =  d  ->  ( F `  y )  =  ( F `  d ) )
6261oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  =  d  ->  (
( F `  y
)  -  ( F `
 ( x  +  T ) ) )  =  ( ( F `
 d )  -  ( F `  ( x  +  T ) ) ) )
63 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  =  d  ->  (
y  -  ( x  +  T ) )  =  ( d  -  ( x  +  T
) ) )
6462, 63oveq12d 6313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  =  d  ->  (
( ( F `  y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T
) ) )  =  ( ( ( F `
 d )  -  ( F `  ( x  +  T ) ) )  /  ( d  -  ( x  +  T ) ) ) )
6564adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  y  =  d )  ->  ( ( ( F `
 y )  -  ( F `  ( x  +  T ) ) )  /  ( y  -  ( x  +  T ) ) )  =  ( ( ( F `  d )  -  ( F `  ( x  +  T
) ) )  / 
( d  -  (
x  +  T ) ) ) )
66 eldifi 3631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( d  e.  ( RR  \  { ( x  +  T ) } )  ->  d  e.  RR )
6747, 66sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( d  e.  ( RR  \  { ( x  +  T ) } )  ->  d  e.  CC )
6867adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  -> 
d  e.  CC )
6947, 18sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  T  e.  CC )
7069adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  T  e.  CC )
7168, 70npcand 9946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  -> 
( ( d  -  T )  +  T
)  =  d )
7271eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  -> 
d  =  ( ( d  -  T )  +  T ) )
7372fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  -> 
( F `  d
)  =  ( F `
 ( ( d  -  T )  +  T ) ) )
74 ovex 6320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( d  -  T )  e. 
_V
7574a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  -> 
( d  -  T
)  e.  _V )
7666adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  -> 
d  e.  RR )
7718adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  T  e.  RR )
7876, 77resubcld 9999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  -> 
( d  -  T
)  e.  RR )
7978ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  ( d  e.  ( RR  \  { ( x  +  T ) } )  ->  (
d  -  T )  e.  RR ) )
8079imdistani 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  -> 
( ph  /\  (
d  -  T )  e.  RR ) )
81 eleq1 2539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  =  ( d  -  T )  ->  (
x  e.  RR  <->  ( d  -  T )  e.  RR ) )
8281anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( x  =  ( d  -  T )  ->  (
( ph  /\  x  e.  RR )  <->  ( ph  /\  ( d  -  T
)  e.  RR ) ) )
83 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( x  =  ( d  -  T )  ->  (
x  +  T )  =  ( ( d  -  T )  +  T ) )
8483fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  =  ( d  -  T )  ->  ( F `  ( x  +  T ) )  =  ( F `  (
( d  -  T
)  +  T ) ) )
85 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( x  =  ( d  -  T )  ->  ( F `  x )  =  ( F `  ( d  -  T
) ) )
8684, 85eqeq12d 2489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( x  =  ( d  -  T )  ->  (
( F `  (
x  +  T ) )  =  ( F `
 x )  <->  ( F `  ( ( d  -  T )  +  T
) )  =  ( F `  ( d  -  T ) ) ) )
8782, 86imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( x  =  ( d  -  T )  ->  (
( ( ph  /\  x  e.  RR )  ->  ( F `  (
x  +  T ) )  =  ( F `
 x ) )  <-> 
( ( ph  /\  ( d  -  T
)  e.  RR )  ->  ( F `  ( ( d  -  T )  +  T
) )  =  ( F `  ( d  -  T ) ) ) ) )
88 fperdvper.fper . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( x  +  T ) )  =  ( F `  x
) )
8988a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( x  e.  _V  ->  (
( ph  /\  x  e.  RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x
) ) )
9087, 89vtoclga 3182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( d  -  T )  e.  _V  ->  (
( ph  /\  (
d  -  T )  e.  RR )  -> 
( F `  (
( d  -  T
)  +  T ) )  =  ( F `
 ( d  -  T ) ) ) )
9175, 80, 90sylc 60 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  -> 
( F `  (
( d  -  T
)  +  T ) )  =  ( F `
 ( d  -  T ) ) )
9273, 91eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  -> 
( F `  d
)  =  ( F `
 ( d  -  T ) ) )
9392adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( F `  d )  =  ( F `  ( d  -  T ) ) )
94 simpll 753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ph )
9517adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  x  e.  RR )
9694, 95, 88syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( F `  ( x  +  T
) )  =  ( F `  x ) )
9793, 96oveq12d 6313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( ( F `  d )  -  ( F `  ( x  +  T
) ) )  =  ( ( F `  ( d  -  T
) )  -  ( F `  x )
) )
9867adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  d  e.  CC )
9994, 69syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  T  e.  CC )
10058adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  x  e.  CC )
10198, 99, 100subsub4d 9973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( (
d  -  T )  -  x )  =  ( d  -  ( T  +  x )
) )
10299, 100addcomd 9793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( T  +  x )  =  ( x  +  T ) )
103102oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( d  -  ( T  +  x ) )  =  ( d  -  (
x  +  T ) ) )
104101, 103eqtr2d 2509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( d  -  ( x  +  T ) )  =  ( ( d  -  T )  -  x
) )
10597, 104oveq12d 6313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( 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 ) ) )
106105adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  y  =  d )  ->  ( ( ( F `
 d )  -  ( F `  ( x  +  T ) ) )  /  ( d  -  ( x  +  T ) ) )  =  ( ( ( F `  ( d  -  T ) )  -  ( F `  x ) )  / 
( ( d  -  T )  -  x
) ) )
10765, 106eqtrd 2508 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( 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
) ) )
108 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  d  e.  ( RR  \  { ( x  +  T ) } ) )
10949adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  F : RR --> CC )
110109, 78ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  -> 
( F `  (
d  -  T ) )  e.  CC )
111110adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( F `  ( d  -  T
) )  e.  CC )
11250, 17ffvelrnd 6033 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  x  e.  dom  G )  ->  ( F `  x )  e.  CC )
113112adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( F `  x )  e.  CC )
114111, 113subcld 9942 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( ( F `  ( d  -  T ) )  -  ( F `  x ) )  e.  CC )
11598, 99subcld 9942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( d  -  T )  e.  CC )
116115, 100subcld 9942 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( (
d  -  T )  -  x )  e.  CC )
117 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( d  -  T
)  =  x )  ->  ( d  -  T )  =  x )
11898adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( d  -  T
)  =  x )  ->  d  e.  CC )
11999adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( d  -  T
)  =  x )  ->  T  e.  CC )
120100adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( d  -  T
)  =  x )  ->  x  e.  CC )
121118, 119, 120subadd2d 9961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( d  -  T
)  =  x )  ->  ( ( d  -  T )  =  x  <->  ( x  +  T )  =  d ) )
122117, 121mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( d  -  T
)  =  x )  ->  ( x  +  T )  =  d )
123122eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( d  -  T
)  =  x )  ->  d  =  ( x  +  T ) )
124 eldifsni 4159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( d  e.  ( RR  \  { ( x  +  T ) } )  ->  d  =/=  (
x  +  T ) )
125124ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( d  -  T
)  =  x )  ->  d  =/=  (
x  +  T ) )
126125neneqd 2669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( d  -  T
)  =  x )  ->  -.  d  =  ( x  +  T
) )
127123, 126pm2.65da 576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  -.  (
d  -  T )  =  x )
128127neqned 2670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( d  -  T )  =/=  x
)
129115, 100, 128subne0d 9951 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( (
d  -  T )  -  x )  =/=  0 )
130114, 116, 129divcld 10332 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( (
( F `  (
d  -  T ) )  -  ( F `
 x ) )  /  ( ( d  -  T )  -  x ) )  e.  CC )
13160, 107, 108, 130fvmptd 5962 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( 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 ) ) )
132131oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 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 ) )
133132fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 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 ) ) )
134133adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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 ) ) )
135134adantllr 718 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( 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 ) ) )
136 simpllr 758 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( 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
) )
13766ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( 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 )
13819ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( 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 )
139137, 138resubcld 9999 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( 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 )
140 elsni 4058 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( d  -  T )  e.  { x }  ->  ( d  -  T
)  =  x )
141140necon3ai 2695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( d  -  T )  =/=  x  ->  -.  ( d  -  T
)  e.  { x } )
142128, 141syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  -.  (
d  -  T )  e.  { x }
)
143142adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  ->  -.  ( d  -  T
)  e.  { x } )
144143adantllr 718 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( 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 } )
145139, 144eldifd 3492 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( 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 }
) )
146 neeq1 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c  =  ( d  -  T )  ->  (
c  =/=  x  <->  ( d  -  T )  =/=  x
) )
147 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( c  =  ( d  -  T )  ->  (
c  -  x )  =  ( ( d  -  T )  -  x ) )
148147fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( c  =  ( d  -  T )  ->  ( abs `  ( c  -  x ) )  =  ( abs `  (
( d  -  T
)  -  x ) ) )
149148breq1d 4463 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( c  =  ( d  -  T )  ->  (
( abs `  (
c  -  x ) )  <  b  <->  ( abs `  ( ( d  -  T )  -  x
) )  <  b
) )
150146, 149anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( c  =  ( d  -  T )  ->  (
( c  =/=  x  /\  ( abs `  (
c  -  x ) )  <  b )  <-> 
( ( d  -  T )  =/=  x  /\  ( abs `  (
( d  -  T
)  -  x ) )  <  b ) ) )
151 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 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 ) ) )
152151oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 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 ) )
153152fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 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 ) ) )
154153breq1d 4463 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( 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 ) )
155150, 154imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 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 ) ) )
156155rspccva 3218 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 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 ) )
157136, 145, 156syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( 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 ) )
158 eqidd 2468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( 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 ) ) ) )
159 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  y  =  ( d  -  T ) )  -> 
y  =  ( d  -  T ) )
160159fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  y  =  ( d  -  T ) )  -> 
( F `  y
)  =  ( F `
 ( d  -  T ) ) )
161160oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  y  =  ( d  -  T ) )  -> 
( ( F `  y )  -  ( F `  x )
)  =  ( ( F `  ( d  -  T ) )  -  ( F `  x ) ) )
162159oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  y  =  ( d  -  T ) )  -> 
( y  -  x
)  =  ( ( d  -  T )  -  x ) )
163161, 162oveq12d 6313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( 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
) ) )
16466adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  d  e.  RR )
16594, 18syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  T  e.  RR )
166164, 165resubcld 9999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( d  -  T )  e.  RR )
167166, 142eldifd 3492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( d  -  T )  e.  ( RR  \  { x } ) )
168158, 163, 167, 130fvmptd 5962 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( 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 ) ) )
169168eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( 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 ) ) )
170169ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( 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 ) ) )
171170oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( 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 ) )
172171fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( 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 ) ) )
173128adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  -> 
( d  -  T
)  =/=  x )
174104eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  ->  ( (
d  -  T )  -  x )  =  ( d  -  (
x  +  T ) ) )
175174adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  -> 
( ( d  -  T )  -  x
)  =  ( d  -  ( x  +  T ) ) )
176175fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  -> 
( abs `  (
( d  -  T
)  -  x ) )  =  ( abs `  ( d  -  (
x  +  T ) ) ) )
177 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  -> 
( abs `  (
d  -  ( x  +  T ) ) )  <  b )
178176, 177eqbrtrd 4473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  -> 
( abs `  (
( d  -  T
)  -  x ) )  <  b )
179173, 178jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  d  e.  ( RR  \  { ( x  +  T ) } ) )  /\  ( abs `  ( d  -  ( x  +  T ) ) )  <  b )  -> 
( ( d  -  T )  =/=  x  /\  ( abs `  (
( d  -  T
)  -  x ) )  <  b ) )
180179adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( 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
) )
181 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( 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
) )
182180, 181mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( 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 )
183172, 182eqbrtrd 4473 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( 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 )
184183ex 434 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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
) )
185184adantllr 718 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( 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
) )
186157, 185mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( 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 )
187186adantrl 715 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( 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
)
188135, 187eqbrtrd 4473 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( 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 )
189188ex 434 . . . . . . . . . . . . . . . . . . . 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 ) } ) )  -> 
( ( 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 ) )
190189ralrimiva 2881 . . . . . . . . . . . . . . . . . . 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
) )  ->  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 ) )
191190ex 434 . . . . . . . . . . . . . . . . . 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
)  ->  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 ) ) )
192 eqidd 2468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( c  e.  ( RR  \  { x } )  ->  ( y  e.  ( RR  \  {
x } )  |->  ( ( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) ) )  =  ( y  e.  ( RR  \  { x } ) 
|->  ( ( ( F `
 y )  -  ( F `  x ) )  /  ( y  -  x ) ) ) )
193 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  =  c  ->  ( F `  y )  =  ( F `  c ) )
194193oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  =  c  ->  (
( F `  y
)  -  ( F `
 x ) )  =  ( ( F `
 c )  -  ( F `  x ) ) )
195 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  =  c  ->  (
y  -  x )  =  ( c  -  x ) )
196194, 195oveq12d 6313 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( y  =  c  ->  (
( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) )  =  ( ( ( F `  c )  -  ( F `  x ) )  / 
( c  -  x
) ) )
197196adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( c  e.  ( RR 
\  { x }
)  /\  y  =  c )  ->  (
( ( F `  y )  -  ( F `  x )
)  /  ( y  -  x ) )  =  ( ( ( F `  c )  -  ( F `  x ) )  / 
( c  -  x
) ) )
198 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( c  e.  ( RR  \  { x } )  ->  c  e.  ( RR  \  { x } ) )
199 ovex 6320 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( F `  c
)  -  ( F `
 x ) )  /  ( c  -  x ) )  e. 
_V
200199a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( c  e.  ( RR  \  { x } )  ->  ( ( ( F `  c )  -  ( F `  x ) )  / 
( c  -  x
) )  e.  _V )
201192, 197, 198, 200fvmptd 5962 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( c  e.  ( RR  \  { x } )  ->  ( ( y  e.  ( RR  \  { x } ) 
|->  ( ( ( F `
 y )  -  ( F `  x ) )  /  ( y  -  x ) ) ) `  c )  =  ( ( ( F `  c )  -  ( F `  x ) )  / 
( c  -  x
) ) )
202201oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( c  e.  ( RR  \  { x } )  ->  ( ( ( y  e.  ( RR 
\  { x }
)  |->  ( ( ( F `  y )  -  ( F `  x ) )  / 
( y  -  x
) ) ) `  c )  -  w
)  =  ( ( ( ( F `  c )  -  ( F `  x )
)  /  ( c  -  x ) )  -  w ) )
203202fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 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 ) ) )
204203ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  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 ) ) )
205204adantllr 718 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( 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 ) ) )
206 simpll 753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  ph )
207198eldifad 3493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( c  e.  ( RR  \  { x } )  ->  c  e.  RR )
208207adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  c  e.  RR )
209 eleq1 2539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( x  =  c  ->  (
x  e.  RR  <->  c  e.  RR ) )
210209anbi2d 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  =  c  ->  (
( ph  /\  x  e.  RR )  <->  ( ph  /\  c  e.  RR ) ) )
211 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( x  =  c  ->  (
x  +  T )  =  ( c  +  T ) )
212211fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( x  =  c  ->  ( F `  ( x  +  T ) )  =  ( F `  (
c  +  T ) ) )
213 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( x  =  c  ->  ( F `  x )  =  ( F `  c ) )
214212, 213eqeq12d 2489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  =  c  ->  (
( F `  (
x  +  T ) )  =  ( F `
 x )  <->  ( F `  ( c  +  T
) )  =  ( F `  c ) ) )
215210, 214imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( x  =  c  ->  (
( ( ph  /\  x  e.  RR )  ->  ( F `  (
x  +  T ) )  =  ( F `
 x ) )  <-> 
( ( ph  /\  c  e.  RR )  ->  ( F `  (
c  +  T ) )  =  ( F `
 c ) ) ) )
216215, 88chvarv 1983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  c  e.  RR )  ->  ( F `
 ( c  +  T ) )  =  ( F `  c
) )
217216eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  c  e.  RR )  ->  ( F `
 c )  =  ( F `  (
c  +  T ) ) )
218206, 208, 217syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  ( F `  c )  =  ( F `  ( c  +  T ) ) )
21917adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  x  e.  RR )
220206, 219, 88syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  ( F `  ( x  +  T
) )  =  ( F `  x ) )
221220eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  ( F `  x )  =  ( F `  ( x  +  T ) ) )
222218, 221oveq12d 6313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  ( ( F `  c )  -  ( F `  x ) )  =  ( ( F `  ( c  +  T
) )  -  ( F `  ( x  +  T ) ) ) )
22347, 208sseldi 3507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  c  e.  CC )
22458adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  x  e.  CC )
225206, 69syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  T  e.  CC )
226223, 224, 225pnpcan2d 9980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  ( (
c  +  T )  -  ( x  +  T ) )  =  ( c  -  x
) )
227226eqcomd 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  ( c  -  x )  =  ( ( c  +  T
)  -  ( x  +  T ) ) )
228222, 227oveq12d 6313 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( 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 ) ) ) )
229228oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( 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
) )
230229fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( 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 ) ) )
231230adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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 ) ) )
232231adantllr 718 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( 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 ) ) )
233 simpllr 758 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( 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 ) )
234207ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( 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 )
23519ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( 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 )
236234, 235readdcld 9635 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( 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 )
237 eldifsni 4159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( c  e.  ( RR  \  { x } )  ->  c  =/=  x
)
238237adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  c  =/=  x )
239223, 224, 225, 238addneintr2d 9799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  ->  ( c  +  T )  =/=  (
x  +  T ) )
240239adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  x  e.  dom  G )  /\  c  e.  ( RR  \  { x } ) )  /\  ( abs `  ( c  -  x ) )  <  b )  -> 
( c  +  T
)  =/=  ( x  +  T ) )
241240adantllr 718 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( 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 ) )
242 elsni 4058 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( c  +  T )  e.  { ( x  +  T ) }  ->  ( c  +  T )  =  ( x  +  T ) )
243242necon3ai 2695 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( c  +  T )  =/=  ( x  +  T )  ->  -.  ( c  +  T
)  e.  { ( x  +  T ) } )
244241, 243syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( 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 ) } )
245236, 244eldifd 3492 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( 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 ) } ) )
246 neeq1 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( d  =  ( c  +  T )  ->  (
d  =/=  ( x  +  T )  <->  ( c  +  T )  =/=  (
x  +  T ) ) )
247 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( d  =  ( c  +  T )  ->  (
d  -  ( x  +  T ) )  =  ( ( c  +  T )  -  ( x  +  T
) ) )
248247fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( d  =  ( c  +  T )  ->  ( abs `  ( d  -  ( x  +  T
) ) )  =  ( abs `  (
( c  +  T
)  -  ( x  +  T ) ) ) )
249248breq1d 4463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( d  =  ( c  +  T )  ->  (
( abs `  (
d  -  ( x  +  T ) ) )  <  b  <->  ( abs `  ( ( c  +  T )  -  (
x  +  T ) ) )  <  b
) )
250246, 249anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( d  =  ( c  +  T )  ->  (
( d  =/=  (
x  +  T )  /\  ( abs `  (
d  -  ( x  +  T ) ) )  <  b )  <-> 
( ( c  +  T )  =/=  (
x  +  T )  /\  ( abs `  (
( c  +  T
)  -  ( x  +  T ) ) )  <  b ) ) )
251 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( 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 ) ) )
252251oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 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 ) )
253252fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 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 ) ) )
254253breq1d 4463 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 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 ) )
255250, 254imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( 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 ) ) )
256255rspccva 3218 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 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 ) )
257233, 245, 256syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( 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 ) )
258 eqidd 2468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( 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
) ) ) ) )
259 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( y  =  ( c  +  T )  ->  ( F `  y )  =  ( F `  ( c  +  T
) ) )
260259oveq1d 6310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( y  =  ( c  +  T )  ->  (
( F `  y
)  -  ( F `
 ( x  +  T