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

Theorem fourierdlem45 31775
Description: If  F has bounded derivative on  ( A (,) B ) and  R is a convergent sequence, with values in  ( A (,) B ), then the composition of  F and  R is a sequence converging to its  limsup. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem45.a  |-  ( ph  ->  A  e.  RR )
fourierdlem45.b  |-  ( ph  ->  B  e.  RR )
fourierdlem45.altb  |-  ( ph  ->  A  <  B )
fourierdlem45.f  |-  ( ph  ->  F  e.  ( ( A (,) B )
-cn-> RR ) )
fourierdlem45.dmdv  |-  ( ph  ->  dom  ( RR  _D  F )  =  ( A (,) B ) )
fourierdlem45.dvbd  |-  ( ph  ->  E. y  e.  RR  A. x  e.  ( A (,) B ) ( abs `  ( ( RR  _D  F ) `
 x ) )  <_  y )
fourierdlem45.m  |-  ( ph  ->  M  e.  ZZ )
fourierdlem45.r  |-  ( ph  ->  R : ( ZZ>= `  M ) --> ( A (,) B ) )
fourierdlem45.s  |-  S  =  ( j  e.  (
ZZ>= `  M )  |->  ( F `  ( R `
 j ) ) )
fourierdlem45.rcnv  |-  ( ph  ->  R  e.  dom  ~~>  )
fourierdlem45.k  |-  K  =  sup ( { k  e.  ( ZZ>= `  M
)  |  A. i  e.  ( ZZ>= `  k )
( abs `  (
( R `  i
)  -  ( R `
 k ) ) )  <  ( x  /  ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) } ,  RR ,  `'  <  )
Assertion
Ref Expression
fourierdlem45  |-  ( ph  ->  S  ~~>  ( limsup `  S
) )
Distinct variable groups:    A, i,
k, x, z    y, A, i, x, z    B, i, k, x, z    y, B    i, F, j, x   
k, F, z    y, F    i, K, j    k, K    y, K    i, M, j, x    k, M    R, i, j    R, k    y, R    S, i, k, x    ph, i, j, x    ph, k    ph, y
Allowed substitution hints:    ph( z)    A( j)    B( j)    R( x, z)    S( y, z, j)    K( x, z)    M( y, z)

Proof of Theorem fourierdlem45
Dummy variable  w is distinct from all other variables.
StepHypRef Expression
1 eqid 2467 . 2  |-  ( ZZ>= `  M )  =  (
ZZ>= `  M )
2 fourierdlem45.f . . . . . 6  |-  ( ph  ->  F  e.  ( ( A (,) B )
-cn-> RR ) )
3 cncff 21265 . . . . . 6  |-  ( F  e.  ( ( A (,) B ) -cn-> RR )  ->  F :
( A (,) B
) --> RR )
42, 3syl 16 . . . . 5  |-  ( ph  ->  F : ( A (,) B ) --> RR )
54adantr 465 . . . 4  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  F :
( A (,) B
) --> RR )
6 fourierdlem45.r . . . . 5  |-  ( ph  ->  R : ( ZZ>= `  M ) --> ( A (,) B ) )
76ffvelrnda 6032 . . . 4  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( R `  j )  e.  ( A (,) B ) )
85, 7ffvelrnd 6033 . . 3  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( F `  ( R `  j
) )  e.  RR )
9 fourierdlem45.s . . 3  |-  S  =  ( j  e.  (
ZZ>= `  M )  |->  ( F `  ( R `
 j ) ) )
108, 9fmptd 6056 . 2  |-  ( ph  ->  S : ( ZZ>= `  M ) --> RR )
11 ssrab2 3590 . . . . 5  |-  { k  e.  ( ZZ>= `  M
)  |  A. i  e.  ( ZZ>= `  k )
( abs `  (
( R `  i
)  -  ( R `
 k ) ) )  <  ( x  /  ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) }  C_  ( ZZ>= `  M )
12 fourierdlem45.k . . . . . 6  |-  K  =  sup ( { k  e.  ( ZZ>= `  M
)  |  A. i  e.  ( ZZ>= `  k )
( abs `  (
( R `  i
)  -  ( R `
 k ) ) )  <  ( x  /  ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) } ,  RR ,  `'  <  )
1311a1i 11 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  { k  e.  ( ZZ>= `  M )  |  A. i  e.  (
ZZ>= `  k ) ( abs `  ( ( R `  i )  -  ( R `  k ) ) )  <  ( x  / 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) }  C_  ( ZZ>= `  M )
)
14 rpre 11238 . . . . . . . . . . . . 13  |-  ( x  e.  RR+  ->  x  e.  RR )
1514adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  e.  RR )
16 fveq2 5872 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  x  ->  (
( RR  _D  F
) `  z )  =  ( ( RR 
_D  F ) `  x ) )
1716fveq2d 5876 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  x  ->  ( abs `  ( ( RR 
_D  F ) `  z ) )  =  ( abs `  (
( RR  _D  F
) `  x )
) )
1817cbvmptv 4544 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `  z
) ) )  =  ( x  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  x )
) )
1918rneqi 5235 . . . . . . . . . . . . . . . 16  |-  ran  (
z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `
 z ) ) )  =  ran  (
x  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `
 x ) ) )
2019supeq1i 7919 . . . . . . . . . . . . . . 15  |-  sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  =  sup ( ran  ( x  e.  ( A (,) B
)  |->  ( abs `  (
( RR  _D  F
) `  x )
) ) ,  RR ,  <  )
21 fourierdlem45.a . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A  e.  RR )
22 fourierdlem45.b . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  B  e.  RR )
23 fourierdlem45.altb . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A  <  B )
24 ioomidp 31441 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  (
( A  +  B
)  /  2 )  e.  ( A (,) B ) )
2521, 22, 23, 24syl3anc 1228 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( A  +  B )  /  2
)  e.  ( A (,) B ) )
26 ne0i 3796 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  +  B
)  /  2 )  e.  ( A (,) B )  ->  ( A (,) B )  =/=  (/) )
2725, 26syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( A (,) B
)  =/=  (/) )
28 ioossre 11598 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( A (,) B )  C_  RR
2928a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( A (,) B
)  C_  RR )
30 dvfre 22222 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F : ( A (,) B ) --> RR 
/\  ( A (,) B )  C_  RR )  ->  ( RR  _D  F ) : dom  ( RR  _D  F
) --> RR )
314, 29, 30syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( RR  _D  F
) : dom  ( RR  _D  F ) --> RR )
32 fourierdlem45.dmdv . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  dom  ( RR  _D  F )  =  ( A (,) B ) )
3332feq2d 5724 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( RR  _D  F ) : dom  ( RR  _D  F
) --> RR  <->  ( RR  _D  F ) : ( A (,) B ) --> RR ) )
3431, 33mpbid 210 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( RR  _D  F
) : ( A (,) B ) --> RR )
35 ax-resscn 9561 . . . . . . . . . . . . . . . . . . . . 21  |-  RR  C_  CC
3635a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  RR  C_  CC )
3734, 36fssd 5746 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( RR  _D  F
) : ( A (,) B ) --> CC )
3837ffvelrnda 6032 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( ( RR  _D  F ) `  x )  e.  CC )
3938abscld 13247 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( abs `  ( ( RR  _D  F ) `  x
) )  e.  RR )
40 fourierdlem45.dvbd . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  E. y  e.  RR  A. x  e.  ( A (,) B ) ( abs `  ( ( RR  _D  F ) `
 x ) )  <_  y )
41 eqid 2467 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `  x
) ) )  =  ( x  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  x )
) )
42 eqid 2467 . . . . . . . . . . . . . . . . 17  |-  sup ( ran  ( x  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  x )
) ) ,  RR ,  <  )  =  sup ( ran  ( x  e.  ( A (,) B
)  |->  ( abs `  (
( RR  _D  F
) `  x )
) ) ,  RR ,  <  )
4327, 39, 40, 41, 42suprnmpt 31352 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( sup ( ran  ( x  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  x )
) ) ,  RR ,  <  )  e.  RR  /\ 
A. x  e.  ( A (,) B ) ( abs `  (
( RR  _D  F
) `  x )
)  <_  sup ( ran  ( x  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  x )
) ) ,  RR ,  <  ) ) )
4443simpld 459 . . . . . . . . . . . . . . 15  |-  ( ph  ->  sup ( ran  (
x  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `
 x ) ) ) ,  RR ,  <  )  e.  RR )
4520, 44syl5eqel 2559 . . . . . . . . . . . . . 14  |-  ( ph  ->  sup ( ran  (
z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `
 z ) ) ) ,  RR ,  <  )  e.  RR )
4645adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  e.  RR )
47 peano2re 9764 . . . . . . . . . . . . 13  |-  ( sup ( ran  ( z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `  z
) ) ) ,  RR ,  <  )  e.  RR  ->  ( sup ( ran  ( z  e.  ( A (,) B
)  |->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 )  e.  RR )
4846, 47syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( sup ( ran  ( z  e.  ( A (,) B
)  |->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 )  e.  RR )
49 0red 9609 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  e.  RR )
50 1red 9623 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  1  e.  RR )
5149, 50readdcld 9635 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 0  +  1 )  e.  RR )
5245, 47syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 )  e.  RR )
5349ltp1d 10488 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  <  ( 0  +  1 ) )
5437, 25ffvelrnd 6033 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( RR  _D  F ) `  (
( A  +  B
)  /  2 ) )  e.  CC )
5554abscld 13247 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( abs `  (
( RR  _D  F
) `  ( ( A  +  B )  /  2 ) ) )  e.  RR )
5654absge0d 13255 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  0  <_  ( abs `  ( ( RR  _D  F ) `  (
( A  +  B
)  /  2 ) ) ) )
5743simprd 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A. x  e.  ( A (,) B ) ( abs `  (
( RR  _D  F
) `  x )
)  <_  sup ( ran  ( x  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  x )
) ) ,  RR ,  <  ) )
58 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  x  ->  (
( RR  _D  F
) `  y )  =  ( ( RR 
_D  F ) `  x ) )
5958fveq2d 5876 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  x  ->  ( abs `  ( ( RR 
_D  F ) `  y ) )  =  ( abs `  (
( RR  _D  F
) `  x )
) )
6020a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  x  ->  sup ( ran  ( z  e.  ( A (,) B
)  |->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  =  sup ( ran  ( x  e.  ( A (,) B
)  |->  ( abs `  (
( RR  _D  F
) `  x )
) ) ,  RR ,  <  ) )
6159, 60breq12d 4466 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  x  ->  (
( abs `  (
( RR  _D  F
) `  y )
)  <_  sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  <->  ( abs `  ( ( RR  _D  F ) `  x
) )  <_  sup ( ran  ( x  e.  ( A (,) B
)  |->  ( abs `  (
( RR  _D  F
) `  x )
) ) ,  RR ,  <  ) ) )
6261cbvralv 3093 . . . . . . . . . . . . . . . . . . 19  |-  ( A. y  e.  ( A (,) B ) ( abs `  ( ( RR  _D  F ) `  y
) )  <_  sup ( ran  ( z  e.  ( A (,) B
)  |->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  <->  A. x  e.  ( A (,) B
) ( abs `  (
( RR  _D  F
) `  x )
)  <_  sup ( ran  ( x  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  x )
) ) ,  RR ,  <  ) )
6357, 62sylibr 212 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A. y  e.  ( A (,) B ) ( abs `  (
( RR  _D  F
) `  y )
)  <_  sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  ) )
64 fveq2 5872 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( ( A  +  B )  / 
2 )  ->  (
( RR  _D  F
) `  y )  =  ( ( RR 
_D  F ) `  ( ( A  +  B )  /  2
) ) )
6564fveq2d 5876 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  ( ( A  +  B )  / 
2 )  ->  ( abs `  ( ( RR 
_D  F ) `  y ) )  =  ( abs `  (
( RR  _D  F
) `  ( ( A  +  B )  /  2 ) ) ) )
6665breq1d 4463 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  ( ( A  +  B )  / 
2 )  ->  (
( abs `  (
( RR  _D  F
) `  y )
)  <_  sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  <->  ( abs `  ( ( RR  _D  F ) `  (
( A  +  B
)  /  2 ) ) )  <_  sup ( ran  ( z  e.  ( A (,) B
)  |->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  ) ) )
6766rspcva 3217 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  +  B )  /  2
)  e.  ( A (,) B )  /\  A. y  e.  ( A (,) B ) ( abs `  ( ( RR  _D  F ) `
 y ) )  <_  sup ( ran  (
z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `
 z ) ) ) ,  RR ,  <  ) )  ->  ( abs `  ( ( RR 
_D  F ) `  ( ( A  +  B )  /  2
) ) )  <_  sup ( ran  ( z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `  z
) ) ) ,  RR ,  <  )
)
6825, 63, 67syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( abs `  (
( RR  _D  F
) `  ( ( A  +  B )  /  2 ) ) )  <_  sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  ) )
6949, 55, 45, 56, 68letrd 9750 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  0  <_  sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  ) )
7049, 45, 50, 69leadd1dd 10178 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 0  +  1 )  <_  ( sup ( ran  ( z  e.  ( A (,) B
)  |->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) )
7149, 51, 52, 53, 70ltletrd 9753 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <  ( sup ( ran  ( z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `  z
) ) ) ,  RR ,  <  )  +  1 ) )
7249, 71gtned 9731 . . . . . . . . . . . . 13  |-  ( ph  ->  ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 )  =/=  0 )
7372adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( sup ( ran  ( z  e.  ( A (,) B
)  |->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 )  =/=  0 )
7415, 48, 73redivcld 10384 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( x  /  ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) )  e.  RR )
75 rpgt0 11243 . . . . . . . . . . . . 13  |-  ( x  e.  RR+  ->  0  < 
x )
7675adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  0  <  x )
7771adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  0  <  ( sup ( ran  (
z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `
 z ) ) ) ,  RR ,  <  )  +  1 ) )
7815, 48, 76, 77divgt0d 10493 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  0  <  ( x  /  ( sup ( ran  ( z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `  z
) ) ) ,  RR ,  <  )  +  1 ) ) )
7974, 78elrpd 11266 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( x  /  ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) )  e.  RR+ )
80 fourierdlem45.m . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  ZZ )
8180adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  M  e.  ZZ )
82 fourierdlem45.rcnv . . . . . . . . . . . 12  |-  ( ph  ->  R  e.  dom  ~~>  )
8382adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  R  e.  dom 
~~>  )
841climcau 13473 . . . . . . . . . . 11  |-  ( ( M  e.  ZZ  /\  R  e.  dom  ~~>  )  ->  A. w  e.  RR+  E. k  e.  ( ZZ>= `  M ) A. i  e.  ( ZZ>=
`  k ) ( abs `  ( ( R `  i )  -  ( R `  k ) ) )  <  w )
8581, 83, 84syl2anc 661 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  A. w  e.  RR+  E. k  e.  ( ZZ>= `  M ) A. i  e.  ( ZZ>=
`  k ) ( abs `  ( ( R `  i )  -  ( R `  k ) ) )  <  w )
86 breq2 4457 . . . . . . . . . . . . 13  |-  ( w  =  ( x  / 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) )  ->  (
( abs `  (
( R `  i
)  -  ( R `
 k ) ) )  <  w  <->  ( abs `  ( ( R `  i )  -  ( R `  k )
) )  <  (
x  /  ( sup ( ran  ( z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `  z
) ) ) ,  RR ,  <  )  +  1 ) ) ) )
8786ralbidv 2906 . . . . . . . . . . . 12  |-  ( w  =  ( x  / 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) )  ->  ( A. i  e.  ( ZZ>=
`  k ) ( abs `  ( ( R `  i )  -  ( R `  k ) ) )  <  w  <->  A. i  e.  ( ZZ>= `  k )
( abs `  (
( R `  i
)  -  ( R `
 k ) ) )  <  ( x  /  ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) ) )
8887rexbidv 2978 . . . . . . . . . . 11  |-  ( w  =  ( x  / 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) )  ->  ( E. k  e.  ( ZZ>=
`  M ) A. i  e.  ( ZZ>= `  k ) ( abs `  ( ( R `  i )  -  ( R `  k )
) )  <  w  <->  E. k  e.  ( ZZ>= `  M ) A. i  e.  ( ZZ>= `  k )
( abs `  (
( R `  i
)  -  ( R `
 k ) ) )  <  ( x  /  ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) ) )
8988rspcva 3217 . . . . . . . . . 10  |-  ( ( ( x  /  ( sup ( ran  ( z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `  z
) ) ) ,  RR ,  <  )  +  1 ) )  e.  RR+  /\  A. w  e.  RR+  E. k  e.  ( ZZ>= `  M ) A. i  e.  ( ZZ>=
`  k ) ( abs `  ( ( R `  i )  -  ( R `  k ) ) )  <  w )  ->  E. k  e.  ( ZZ>=
`  M ) A. i  e.  ( ZZ>= `  k ) ( abs `  ( ( R `  i )  -  ( R `  k )
) )  <  (
x  /  ( sup ( ran  ( z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `  z
) ) ) ,  RR ,  <  )  +  1 ) ) )
9079, 85, 89syl2anc 661 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  E. k  e.  ( ZZ>= `  M ) A. i  e.  ( ZZ>=
`  k ) ( abs `  ( ( R `  i )  -  ( R `  k ) ) )  <  ( x  / 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) )
91 nfv 1683 . . . . . . . . . 10  |-  F/ k ( ph  /\  x  e.  RR+ )
92 id 22 . . . . . . . . . . 11  |-  ( A. i  e.  ( ZZ>= `  k ) ( abs `  ( ( R `  i )  -  ( R `  k )
) )  <  (
x  /  ( sup ( ran  ( z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `  z
) ) ) ,  RR ,  <  )  +  1 ) )  ->  A. i  e.  (
ZZ>= `  k ) ( abs `  ( ( R `  i )  -  ( R `  k ) ) )  <  ( x  / 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) )
9392a1ii 27 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( k  e.  ( ZZ>= `  M )  ->  ( A. i  e.  ( ZZ>= `  k )
( abs `  (
( R `  i
)  -  ( R `
 k ) ) )  <  ( x  /  ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) )  ->  A. i  e.  ( ZZ>= `  k )
( abs `  (
( R `  i
)  -  ( R `
 k ) ) )  <  ( x  /  ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) ) ) )
9491, 93reximdai 2936 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( E. k  e.  ( ZZ>= `  M ) A. i  e.  ( ZZ>= `  k )
( abs `  (
( R `  i
)  -  ( R `
 k ) ) )  <  ( x  /  ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) )  ->  E. k  e.  ( ZZ>= `  M ) A. i  e.  ( ZZ>=
`  k ) ( abs `  ( ( R `  i )  -  ( R `  k ) ) )  <  ( x  / 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) ) )
9590, 94mpd 15 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  E. k  e.  ( ZZ>= `  M ) A. i  e.  ( ZZ>=
`  k ) ( abs `  ( ( R `  i )  -  ( R `  k ) ) )  <  ( x  / 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) )
96 rabn0 3810 . . . . . . . 8  |-  ( { k  e.  ( ZZ>= `  M )  |  A. i  e.  ( ZZ>= `  k ) ( abs `  ( ( R `  i )  -  ( R `  k )
) )  <  (
x  /  ( sup ( ran  ( z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `  z
) ) ) ,  RR ,  <  )  +  1 ) ) }  =/=  (/)  <->  E. k  e.  ( ZZ>= `  M ) A. i  e.  ( ZZ>=
`  k ) ( abs `  ( ( R `  i )  -  ( R `  k ) ) )  <  ( x  / 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) )
9795, 96sylibr 212 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  { k  e.  ( ZZ>= `  M )  |  A. i  e.  (
ZZ>= `  k ) ( abs `  ( ( R `  i )  -  ( R `  k ) ) )  <  ( x  / 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) }  =/=  (/) )
98 infmssuzcl 11177 . . . . . . 7  |-  ( ( { k  e.  (
ZZ>= `  M )  | 
A. i  e.  (
ZZ>= `  k ) ( abs `  ( ( R `  i )  -  ( R `  k ) ) )  <  ( x  / 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) }  C_  ( ZZ>= `  M )  /\  { k  e.  (
ZZ>= `  M )  | 
A. i  e.  (
ZZ>= `  k ) ( abs `  ( ( R `  i )  -  ( R `  k ) ) )  <  ( x  / 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) }  =/=  (/) )  ->  sup ( { k  e.  (
ZZ>= `  M )  | 
A. i  e.  (
ZZ>= `  k ) ( abs `  ( ( R `  i )  -  ( R `  k ) ) )  <  ( x  / 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) } ,  RR ,  `'  <  )  e.  { k  e.  ( ZZ>= `  M )  |  A. i  e.  (
ZZ>= `  k ) ( abs `  ( ( R `  i )  -  ( R `  k ) ) )  <  ( x  / 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) } )
9913, 97, 98syl2anc 661 . . . . . 6  |-  ( (
ph  /\  x  e.  RR+ )  ->  sup ( { k  e.  (
ZZ>= `  M )  | 
A. i  e.  (
ZZ>= `  k ) ( abs `  ( ( R `  i )  -  ( R `  k ) ) )  <  ( x  / 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) } ,  RR ,  `'  <  )  e.  { k  e.  ( ZZ>= `  M )  |  A. i  e.  (
ZZ>= `  k ) ( abs `  ( ( R `  i )  -  ( R `  k ) ) )  <  ( x  / 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) } )
10012, 99syl5eqel 2559 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  K  e.  { k  e.  ( ZZ>= `  M )  |  A. i  e.  ( ZZ>= `  k ) ( abs `  ( ( R `  i )  -  ( R `  k )
) )  <  (
x  /  ( sup ( ran  ( z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `  z
) ) ) ,  RR ,  <  )  +  1 ) ) } )
10111, 100sseldi 3507 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  K  e.  ( ZZ>= `  M )
)
1029a1i 11 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  S  =  ( j  e.  (
ZZ>= `  M )  |->  ( F `  ( R `
 j ) ) ) )
103 fveq2 5872 . . . . . . . . . . 11  |-  ( j  =  i  ->  ( R `  j )  =  ( R `  i ) )
104103fveq2d 5876 . . . . . . . . . 10  |-  ( j  =  i  ->  ( F `  ( R `  j ) )  =  ( F `  ( R `  i )
) )
105104adantl 466 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  j  =  i )  ->  ( F `  ( R `  j )
)  =  ( F `
 ( R `  i ) ) )
106 uzss 11114 . . . . . . . . . . . 12  |-  ( K  e.  ( ZZ>= `  M
)  ->  ( ZZ>= `  K )  C_  ( ZZ>=
`  M ) )
107101, 106syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ZZ>= `  K )  C_  ( ZZ>=
`  M ) )
108107adantr 465 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( ZZ>= `  K )  C_  ( ZZ>=
`  M ) )
109 simpr 461 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  i  e.  ( ZZ>= `  K )
)
110108, 109sseldd 3510 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  i  e.  ( ZZ>= `  M )
)
1114ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  F :
( A (,) B
) --> RR )
1126ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  R :
( ZZ>= `  M ) --> ( A (,) B ) )
113112, 110ffvelrnd 6033 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( R `  i )  e.  ( A (,) B ) )
114111, 113ffvelrnd 6033 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( F `  ( R `  i
) )  e.  RR )
115102, 105, 110, 114fvmptd 5962 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( S `  i )  =  ( F `  ( R `
 i ) ) )
116 fveq2 5872 . . . . . . . . . . 11  |-  ( j  =  K  ->  ( R `  j )  =  ( R `  K ) )
117116fveq2d 5876 . . . . . . . . . 10  |-  ( j  =  K  ->  ( F `  ( R `  j ) )  =  ( F `  ( R `  K )
) )
118117adantl 466 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  j  =  K )  ->  ( F `  ( R `  j )
)  =  ( F `
 ( R `  K ) ) )
119101adantr 465 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  K  e.  ( ZZ>= `  M )
)
120112, 119ffvelrnd 6033 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( R `  K )  e.  ( A (,) B ) )
121111, 120ffvelrnd 6033 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( F `  ( R `  K
) )  e.  RR )
122102, 118, 119, 121fvmptd 5962 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( S `  K )  =  ( F `  ( R `
 K ) ) )
123115, 122oveq12d 6313 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( ( S `  i )  -  ( S `  K ) )  =  ( ( F `  ( R `  i ) )  -  ( F `
 ( R `  K ) ) ) )
124123fveq2d 5876 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( abs `  ( ( S `  i )  -  ( S `  K )
) )  =  ( abs `  ( ( F `  ( R `
 i ) )  -  ( F `  ( R `  K ) ) ) ) )
125114recnd 9634 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( F `  ( R `  i
) )  e.  CC )
126121recnd 9634 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( F `  ( R `  K
) )  e.  CC )
127125, 126subcld 9942 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( ( F `  ( R `  i ) )  -  ( F `  ( R `
 K ) ) )  e.  CC )
128127abscld 13247 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( abs `  ( ( F `  ( R `  i ) )  -  ( F `
 ( R `  K ) ) ) )  e.  RR )
129128adantr 465 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( abs `  (
( F `  ( R `  i )
)  -  ( F `
 ( R `  K ) ) ) )  e.  RR )
13045ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  e.  RR )
131130adantr 465 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  ->  sup ( ran  ( z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `  z
) ) ) ,  RR ,  <  )  e.  RR )
13228a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( A (,) B )  C_  RR )
1336adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  R :
( ZZ>= `  M ) --> ( A (,) B ) )
134133, 101ffvelrnd 6033 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( R `  K )  e.  ( A (,) B ) )
135132, 134sseldd 3510 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( R `  K )  e.  RR )
136135ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( R `  K
)  e.  RR )
13728, 113sseldi 3507 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( R `  i )  e.  RR )
138137adantr 465 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( R `  i
)  e.  RR )
139136, 138resubcld 9999 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( ( R `  K )  -  ( R `  i )
)  e.  RR )
140131, 139remulcld 9636 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  x.  (
( R `  K
)  -  ( R `
 i ) ) )  e.  RR )
14114ad2antlr 726 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  x  e.  RR )
142141adantr 465 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  ->  x  e.  RR )
14335, 114sseldi 3507 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( F `  ( R `  i
) )  e.  CC )
144143adantr 465 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( F `  ( R `  i )
)  e.  CC )
145126adantr 465 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( F `  ( R `  K )
)  e.  CC )
146144, 145abssubd 13264 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( abs `  (
( F `  ( R `  i )
)  -  ( F `
 ( R `  K ) ) ) )  =  ( abs `  ( ( F `  ( R `  K ) )  -  ( F `
 ( R `  i ) ) ) ) )
14721ad3antrrr 729 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  ->  A  e.  RR )
14822ad3antrrr 729 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  ->  B  e.  RR )
149111adantr 465 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  ->  F : ( A (,) B ) --> RR )
15032ad3antrrr 729 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  ->  dom  ( RR  _D  F
)  =  ( A (,) B ) )
15163ad3antrrr 729 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  ->  A. y  e.  ( A (,) B ) ( abs `  ( ( RR  _D  F ) `
 y ) )  <_  sup ( ran  (
z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `
 z ) ) ) ,  RR ,  <  ) )
152113adantr 465 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( R `  i
)  e.  ( A (,) B ) )
153137rexrd 9655 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( R `  i )  e.  RR* )
154153adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( R `  i
)  e.  RR* )
15522rexrd 9655 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  e.  RR* )
156155adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( ZZ>= `  K )
)  ->  B  e.  RR* )
157156adantlr 714 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  B  e.  RR* )
158157adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  ->  B  e.  RR* )
159 simpr 461 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( R `  i
)  <  ( R `  K ) )
16021rexrd 9655 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  e.  RR* )
161160adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  A  e.  RR* )
162155adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  B  e.  RR* )
163 iooltub 31435 . . . . . . . . . . . . . 14  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( R `
 K )  e.  ( A (,) B
) )  ->  ( R `  K )  <  B )
164161, 162, 134, 163syl3anc 1228 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( R `  K )  <  B
)
165164ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( R `  K
)  <  B )
166154, 158, 136, 159, 165eliood 31418 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( R `  K
)  e.  ( ( R `  i ) (,) B ) )
167147, 148, 149, 150, 131, 151, 152, 166dvbdfbdioolem1 31581 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( ( abs `  (
( F `  ( R `  K )
)  -  ( F `
 ( R `  i ) ) ) )  <_  ( sup ( ran  ( z  e.  ( A (,) B
)  |->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  x.  (
( R `  K
)  -  ( R `
 i ) ) )  /\  ( abs `  ( ( F `  ( R `  K ) )  -  ( F `
 ( R `  i ) ) ) )  <_  ( sup ( ran  ( z  e.  ( A (,) B
)  |->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  x.  ( B  -  A )
) ) )
168167simpld 459 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( abs `  (
( F `  ( R `  K )
)  -  ( F `
 ( R `  i ) ) ) )  <_  ( sup ( ran  ( z  e.  ( A (,) B
)  |->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  x.  (
( R `  K
)  -  ( R `
 i ) ) ) )
169146, 168eqbrtrd 4473 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( abs `  (
( F `  ( R `  i )
)  -  ( F `
 ( R `  K ) ) ) )  <_  ( sup ( ran  ( z  e.  ( A (,) B
)  |->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  x.  (
( R `  K
)  -  ( R `
 i ) ) ) )
170131, 47syl 16 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 )  e.  RR )
171170, 139jca 532 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 )  e.  RR  /\  ( ( R `  K )  -  ( R `  i )
)  e.  RR ) )
172 remulcl 9589 . . . . . . . . . 10  |-  ( ( ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 )  e.  RR  /\  ( ( R `  K )  -  ( R `  i )
)  e.  RR )  ->  ( ( sup ( ran  ( z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `  z
) ) ) ,  RR ,  <  )  +  1 )  x.  ( ( R `  K )  -  ( R `  i )
) )  e.  RR )
173171, 172syl 16 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 )  x.  ( ( R `  K )  -  ( R `  i ) ) )  e.  RR )
174138, 136posdifd 10151 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( ( R `  i )  <  ( R `  K )  <->  0  <  ( ( R `
 K )  -  ( R `  i ) ) ) )
175159, 174mpbid 210 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
0  <  ( ( R `  K )  -  ( R `  i ) ) )
176139, 175elrpd 11266 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( ( R `  K )  -  ( R `  i )
)  e.  RR+ )
177 1rp 11236 . . . . . . . . . . . 12  |-  1  e.  RR+
178177a1i 11 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
1  e.  RR+ )
179131, 178ltaddrpd 11297 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  ->  sup ( ran  ( z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `  z
) ) ) ,  RR ,  <  )  <  ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) )
180131, 170, 176, 179ltmul1dd 11319 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  x.  (
( R `  K
)  -  ( R `
 i ) ) )  <  ( ( sup ( ran  (
z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `
 z ) ) ) ,  RR ,  <  )  +  1 )  x.  ( ( R `
 K )  -  ( R `  i ) ) ) )
18128a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( A (,) B )  C_  RR )
182181, 113sseldd 3510 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( R `  i )  e.  RR )
18328, 120sseldi 3507 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( R `  K )  e.  RR )
184182, 183resubcld 9999 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( ( R `  i )  -  ( R `  K ) )  e.  RR )
18535, 184sseldi 3507 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( ( R `  i )  -  ( R `  K ) )  e.  CC )
186185abscld 13247 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( abs `  ( ( R `  i )  -  ( R `  K )
) )  e.  RR )
187186adantr 465 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( abs `  (
( R `  i
)  -  ( R `
 K ) ) )  e.  RR )
18874ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( x  /  ( sup ( ran  ( z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `  z
) ) ) ,  RR ,  <  )  +  1 ) )  e.  RR )
189139leabsd 13226 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( ( R `  K )  -  ( R `  i )
)  <_  ( abs `  ( ( R `  K )  -  ( R `  i )
) ) )
19035, 136sseldi 3507 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( R `  K
)  e.  CC )
19135, 137sseldi 3507 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( R `  i )  e.  CC )
192191adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( R `  i
)  e.  CC )
193190, 192abssubd 13264 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( abs `  (
( R `  K
)  -  ( R `
 i ) ) )  =  ( abs `  ( ( R `  i )  -  ( R `  K )
) ) )
194189, 193breqtrd 4477 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( ( R `  K )  -  ( R `  i )
)  <_  ( abs `  ( ( R `  i )  -  ( R `  K )
) ) )
195 fveq2 5872 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  K  ->  ( ZZ>=
`  k )  =  ( ZZ>= `  K )
)
196 raleq 3063 . . . . . . . . . . . . . . . . . 18  |-  ( (
ZZ>= `  k )  =  ( ZZ>= `  K )  ->  ( A. i  e.  ( ZZ>= `  k )
( abs `  (
( R `  i
)  -  ( R `
 k ) ) )  <  ( x  /  ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) )  <->  A. i  e.  ( ZZ>= `  K )
( abs `  (
( R `  i
)  -  ( R `
 k ) ) )  <  ( x  /  ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) ) )
197195, 196syl 16 . . . . . . . . . . . . . . . . 17  |-  ( k  =  K  ->  ( A. i  e.  ( ZZ>=
`  k ) ( abs `  ( ( R `  i )  -  ( R `  k ) ) )  <  ( x  / 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) )  <->  A. i  e.  ( ZZ>= `  K )
( abs `  (
( R `  i
)  -  ( R `
 k ) ) )  <  ( x  /  ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) ) )
198 fveq2 5872 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  K  ->  ( R `  k )  =  ( R `  K ) )
199198oveq2d 6311 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  K  ->  (
( R `  i
)  -  ( R `
 k ) )  =  ( ( R `
 i )  -  ( R `  K ) ) )
200199fveq2d 5876 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  K  ->  ( abs `  ( ( R `
 i )  -  ( R `  k ) ) )  =  ( abs `  ( ( R `  i )  -  ( R `  K ) ) ) )
201200breq1d 4463 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  K  ->  (
( abs `  (
( R `  i
)  -  ( R `
 k ) ) )  <  ( x  /  ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) )  <->  ( abs `  ( ( R `  i )  -  ( R `  K )
) )  <  (
x  /  ( sup ( ran  ( z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `  z
) ) ) ,  RR ,  <  )  +  1 ) ) ) )
202201ralbidv 2906 . . . . . . . . . . . . . . . . 17  |-  ( k  =  K  ->  ( A. i  e.  ( ZZ>=
`  K ) ( abs `  ( ( R `  i )  -  ( R `  k ) ) )  <  ( x  / 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) )  <->  A. i  e.  ( ZZ>= `  K )
( abs `  (
( R `  i
)  -  ( R `
 K ) ) )  <  ( x  /  ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) ) )
203197, 202bitrd 253 . . . . . . . . . . . . . . . 16  |-  ( k  =  K  ->  ( A. i  e.  ( ZZ>=
`  k ) ( abs `  ( ( R `  i )  -  ( R `  k ) ) )  <  ( x  / 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) )  <->  A. i  e.  ( ZZ>= `  K )
( abs `  (
( R `  i
)  -  ( R `
 K ) ) )  <  ( x  /  ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) ) )
204203elrab 3266 . . . . . . . . . . . . . . 15  |-  ( K  e.  { k  e.  ( ZZ>= `  M )  |  A. i  e.  (
ZZ>= `  k ) ( abs `  ( ( R `  i )  -  ( R `  k ) ) )  <  ( x  / 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) }  <->  ( K  e.  ( ZZ>= `  M )  /\  A. i  e.  (
ZZ>= `  K ) ( abs `  ( ( R `  i )  -  ( R `  K ) ) )  <  ( x  / 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) ) )
205100, 204sylib 196 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( K  e.  ( ZZ>= `  M )  /\  A. i  e.  (
ZZ>= `  K ) ( abs `  ( ( R `  i )  -  ( R `  K ) ) )  <  ( x  / 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) ) )
206205simprd 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  A. i  e.  ( ZZ>= `  K )
( abs `  (
( R `  i
)  -  ( R `
 K ) ) )  <  ( x  /  ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) )
207206r19.21bi 2836 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( abs `  ( ( R `  i )  -  ( R `  K )
) )  <  (
x  /  ( sup ( ran  ( z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `  z
) ) ) ,  RR ,  <  )  +  1 ) ) )
208207adantr 465 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( abs `  (
( R `  i
)  -  ( R `
 K ) ) )  <  ( x  /  ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) )
209139, 187, 188, 194, 208lelttrd 9751 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( ( R `  K )  -  ( R `  i )
)  <  ( x  /  ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) )
21052, 71elrpd 11266 . . . . . . . . . . . 12  |-  ( ph  ->  ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 )  e.  RR+ )
211210ad3antrrr 729 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 )  e.  RR+ )
212139, 142, 211ltmuldiv2d 11312 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( ( ( sup ( ran  ( z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `  z
) ) ) ,  RR ,  <  )  +  1 )  x.  ( ( R `  K )  -  ( R `  i )
) )  <  x  <->  ( ( R `  K
)  -  ( R `
 i ) )  <  ( x  / 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) ) )
213209, 212mpbird 232 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 )  x.  ( ( R `  K )  -  ( R `  i ) ) )  <  x )
214140, 173, 142, 180, 213lttrd 9754 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  x.  (
( R `  K
)  -  ( R `
 i ) ) )  <  x )
215129, 140, 142, 169, 214lelttrd 9751 . . . . . . 7  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  <  ( R `  K ) )  -> 
( abs `  (
( F `  ( R `  i )
)  -  ( F `
 ( R `  K ) ) ) )  <  x )
216 fveq2 5872 . . . . . . . . . . . . . . 15  |-  ( ( R `  i )  =  ( R `  K )  ->  ( F `  ( R `  i ) )  =  ( F `  ( R `  K )
) )
217216oveq1d 6310 . . . . . . . . . . . . . 14  |-  ( ( R `  i )  =  ( R `  K )  ->  (
( F `  ( R `  i )
)  -  ( F `
 ( R `  K ) ) )  =  ( ( F `
 ( R `  K ) )  -  ( F `  ( R `
 K ) ) ) )
218217adantl 466 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  =  ( R `  K ) )  -> 
( ( F `  ( R `  i ) )  -  ( F `
 ( R `  K ) ) )  =  ( ( F `
 ( R `  K ) )  -  ( F `  ( R `
 K ) ) ) )
219126subidd 9930 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( ( F `  ( R `  K ) )  -  ( F `  ( R `
 K ) ) )  =  0 )
220219adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  =  ( R `  K ) )  -> 
( ( F `  ( R `  K ) )  -  ( F `
 ( R `  K ) ) )  =  0 )
221218, 220eqtrd 2508 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  =  ( R `  K ) )  -> 
( ( F `  ( R `  i ) )  -  ( F `
 ( R `  K ) ) )  =  0 )
222221fveq2d 5876 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  =  ( R `  K ) )  -> 
( abs `  (
( F `  ( R `  i )
)  -  ( F `
 ( R `  K ) ) ) )  =  ( abs `  0 ) )
223 eqidd 2468 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  =  ( R `  K ) )  -> 
0  =  0 )
224223abs00bd 13104 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  =  ( R `  K ) )  -> 
( abs `  0
)  =  0 )
225222, 224eqtrd 2508 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  =  ( R `  K ) )  -> 
( abs `  (
( F `  ( R `  i )
)  -  ( F `
 ( R `  K ) ) ) )  =  0 )
22676ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  =  ( R `  K ) )  -> 
0  <  x )
227225, 226eqbrtrd 4473 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  i )  =  ( R `  K ) )  -> 
( abs `  (
( F `  ( R `  i )
)  -  ( F `
 ( R `  K ) ) ) )  <  x )
228227adantlr 714 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>=
`  K ) )  /\  -.  ( R `
 i )  < 
( R `  K
) )  /\  ( R `  i )  =  ( R `  K ) )  -> 
( abs `  (
( F `  ( R `  i )
)  -  ( F `
 ( R `  K ) ) ) )  <  x )
229 simpll 753 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>=
`  K ) )  /\  -.  ( R `
 i )  < 
( R `  K
) )  /\  -.  ( R `  i )  =  ( R `  K ) )  -> 
( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) ) )
230229, 183syl 16 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>=
`  K ) )  /\  -.  ( R `
 i )  < 
( R `  K
) )  /\  -.  ( R `  i )  =  ( R `  K ) )  -> 
( R `  K
)  e.  RR )
231229, 137syl 16 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>=
`  K ) )  /\  -.  ( R `
 i )  < 
( R `  K
) )  /\  -.  ( R `  i )  =  ( R `  K ) )  -> 
( R `  i
)  e.  RR )
232 id 22 . . . . . . . . . . . . 13  |-  ( ( R `  K )  =  ( R `  i )  ->  ( R `  K )  =  ( R `  i ) )
233232eqcomd 2475 . . . . . . . . . . . 12  |-  ( ( R `  K )  =  ( R `  i )  ->  ( R `  i )  =  ( R `  K ) )
234233necon3bi 2696 . . . . . . . . . . 11  |-  ( -.  ( R `  i
)  =  ( R `
 K )  -> 
( R `  K
)  =/=  ( R `
 i ) )
235234adantl 466 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>=
`  K ) )  /\  -.  ( R `
 i )  < 
( R `  K
) )  /\  -.  ( R `  i )  =  ( R `  K ) )  -> 
( R `  K
)  =/=  ( R `
 i ) )
236 simplr 754 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>=
`  K ) )  /\  -.  ( R `
 i )  < 
( R `  K
) )  /\  -.  ( R `  i )  =  ( R `  K ) )  ->  -.  ( R `  i
)  <  ( R `  K ) )
237230, 231, 235, 236lttri5d 31399 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>=
`  K ) )  /\  -.  ( R `
 i )  < 
( R `  K
) )  /\  -.  ( R `  i )  =  ( R `  K ) )  -> 
( R `  K
)  <  ( R `  i ) )
238128adantr 465 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( abs `  (
( F `  ( R `  i )
)  -  ( F `
 ( R `  K ) ) ) )  e.  RR )
239130, 184remulcld 9636 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( sup ( ran  ( z  e.  ( A (,) B
)  |->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  x.  (
( R `  i
)  -  ( R `
 K ) ) )  e.  RR )
240239adantr 465 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  x.  (
( R `  i
)  -  ( R `
 K ) ) )  e.  RR )
241141adantr 465 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  ->  x  e.  RR )
24221ad3antrrr 729 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  ->  A  e.  RR )
24322ad3antrrr 729 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  ->  B  e.  RR )
244111adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  ->  F : ( A (,) B ) --> RR )
24532ad3antrrr 729 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  ->  dom  ( RR  _D  F
)  =  ( A (,) B ) )
24645ad3antrrr 729 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  ->  sup ( ran  ( z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `  z
) ) ) ,  RR ,  <  )  e.  RR )
24763ad3antrrr 729 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  ->  A. y  e.  ( A (,) B ) ( abs `  ( ( RR  _D  F ) `
 y ) )  <_  sup ( ran  (
z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `
 z ) ) ) ,  RR ,  <  ) )
248120adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( R `  K
)  e.  ( A (,) B ) )
249135rexrd 9655 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( R `  K )  e.  RR* )
250249ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( R `  K
)  e.  RR* )
251243rexrd 9655 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  ->  B  e.  RR* )
252137adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( R `  i
)  e.  RR )
253 simpr 461 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( R `  K
)  <  ( R `  i ) )
254160adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  K )
)  ->  A  e.  RR* )
255254adantlr 714 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  A  e.  RR* )
256 iooltub 31435 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  ( R `
 i )  e.  ( A (,) B
) )  ->  ( R `  i )  <  B )
257255, 157, 113, 256syl3anc 1228 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( R `  i )  <  B
)
258257adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( R `  i
)  <  B )
259250, 251, 252, 253, 258eliood 31418 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( R `  i
)  e.  ( ( R `  K ) (,) B ) )
260242, 243, 244, 245, 246, 247, 248, 259dvbdfbdioolem1 31581 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( ( abs `  (
( F `  ( R `  i )
)  -  ( F `
 ( R `  K ) ) ) )  <_  ( sup ( ran  ( z  e.  ( A (,) B
)  |->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  x.  (
( R `  i
)  -  ( R `
 K ) ) )  /\  ( abs `  ( ( F `  ( R `  i ) )  -  ( F `
 ( R `  K ) ) ) )  <_  ( sup ( ran  ( z  e.  ( A (,) B
)  |->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  x.  ( B  -  A )
) ) )
261260simpld 459 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( abs `  (
( F `  ( R `  i )
)  -  ( F `
 ( R `  K ) ) ) )  <_  ( sup ( ran  ( z  e.  ( A (,) B
)  |->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  x.  (
( R `  i
)  -  ( R `
 K ) ) ) )
262 1red 9623 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
1  e.  RR )
263246, 262readdcld 9635 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 )  e.  RR )
264183adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( R `  K
)  e.  RR )
265252, 264resubcld 9999 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( ( R `  i )  -  ( R `  K )
)  e.  RR )
266263, 265remulcld 9636 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 )  x.  ( ( R `  i )  -  ( R `  K ) ) )  e.  RR )
267246, 47syl 16 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 )  e.  RR )
268264, 252posdifd 10151 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( ( R `  K )  <  ( R `  i )  <->  0  <  ( ( R `
 i )  -  ( R `  K ) ) ) )
269253, 268mpbid 210 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
0  <  ( ( R `  i )  -  ( R `  K ) ) )
270265, 269elrpd 11266 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( ( R `  i )  -  ( R `  K )
)  e.  RR+ )
271246ltp1d 10488 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  ->  sup ( ran  ( z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `  z
) ) ) ,  RR ,  <  )  <  ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) )
272246, 267, 270, 271ltmul1dd 11319 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  x.  (
( R `  i
)  -  ( R `
 K ) ) )  <  ( ( sup ( ran  (
z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `
 z ) ) ) ,  RR ,  <  )  +  1 )  x.  ( ( R `
 i )  -  ( R `  K ) ) ) )
273186adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( abs `  (
( R `  i
)  -  ( R `
 K ) ) )  e.  RR )
27474ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( x  /  ( sup ( ran  ( z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `  z
) ) ) ,  RR ,  <  )  +  1 ) )  e.  RR )
275265leabsd 13226 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( ( R `  i )  -  ( R `  K )
)  <_  ( abs `  ( ( R `  i )  -  ( R `  K )
) ) )
276207adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( abs `  (
( R `  i
)  -  ( R `
 K ) ) )  <  ( x  /  ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) )
277265, 273, 274, 275, 276lelttrd 9751 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( ( R `  i )  -  ( R `  K )
)  <  ( x  /  ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) )
278210ad3antrrr 729 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 )  e.  RR+ )
279265, 241, 278ltmuldiv2d 11312 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( ( ( sup ( ran  ( z  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `  z
) ) ) ,  RR ,  <  )  +  1 )  x.  ( ( R `  i )  -  ( R `  K )
) )  <  x  <->  ( ( R `  i
)  -  ( R `
 K ) )  <  ( x  / 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 ) ) ) )
280277, 279mpbird 232 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( ( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  +  1 )  x.  ( ( R `  i )  -  ( R `  K ) ) )  <  x )
281240, 266, 241, 272, 280lttrd 9754 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( sup ( ran  ( z  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  z )
) ) ,  RR ,  <  )  x.  (
( R `  i
)  -  ( R `
 K ) ) )  <  x )
282238, 240, 241, 261, 281lelttrd 9751 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  ( R `  K )  <  ( R `  i ) )  -> 
( abs `  (
( F `  ( R `  i )
)  -  ( F `
 ( R `  K ) ) ) )  <  x )
283229, 237, 282syl2anc 661 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>=
`  K ) )  /\  -.  ( R `
 i )  < 
( R `  K
) )  /\  -.  ( R `  i )  =  ( R `  K ) )  -> 
( abs `  (
( F `  ( R `  i )
)  -  ( F `
 ( R `  K ) ) ) )  <  x )
284228, 283pm2.61dan 789 . . . . . . 7  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K ) )  /\  -.  ( R `  i
)  <  ( R `  K ) )  -> 
( abs `  (
( F `  ( R `  i )
)  -  ( F `
 ( R `  K ) ) ) )  <  x )
285215, 284pm2.61dan 789 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( abs `  ( ( F `  ( R `  i ) )  -  ( F `
 ( R `  K ) ) ) )  <  x )
286124, 285eqbrtrd 4473 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  i  e.  ( ZZ>= `  K )
)  ->  ( abs `  ( ( S `  i )  -  ( S `  K )
) )  <  x
)
287286ralrimiva 2881 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  A. i  e.  ( ZZ>= `  K )
( abs `  (
( S `  i
)  -  ( S `
 K ) ) )  <  x )
288 raleq 3063 . . . . . . 7  |-  ( (
ZZ>= `  k )  =  ( ZZ>= `  K )  ->  ( A. i  e.  ( ZZ>= `  k )
( abs `  (
( S `  i
)  -  ( S `
 k ) ) )  <  x  <->  A. i  e.  ( ZZ>= `  K )
( abs `  (
( S `  i
)  -  ( S `
 k ) ) )  <  x ) )
289195, 288syl 16 . . . . . 6  |-  ( k  =  K  ->  ( A. i  e.  ( ZZ>=
`  k ) ( abs `  ( ( S `  i )  -  ( S `  k ) ) )  <  x  <->  A. i  e.  ( ZZ>= `  K )
( abs `  (
( S `  i
)  -  ( S `
 k ) ) )  <  x ) )
290 fveq2 5872 . . . . . . . . . 10  |-  ( k  =  K  ->  ( S `  k )  =  ( S `  K ) )
291290oveq2d 6311 . . . . . . . . 9  |-  ( k  =  K  ->  (
( S `  i
)  -  ( S `
 k ) )  =  ( ( S `
 i )  -  ( S `  K ) ) )
292291fveq2d 5876 . . . . . . . 8  |-  ( k  =  K  ->  ( abs `  ( ( S `
 i )  -  ( S `  k ) ) )  =  ( abs `  ( ( S `  i )  -  ( S `  K ) ) ) )
293292breq1d 4463 . . . . . . 7  |-  ( k  =  K  ->  (
( abs `  (
( S `  i
)  -  ( S `
 k ) ) )  <  x  <->  ( abs `  ( ( S `  i )  -  ( S `  K )
) )  <  x
) )
294293ralbidv 2906 . . . . . 6  |-  ( k  =  K  ->  ( A. i  e.  ( ZZ>=
`  K ) ( abs `