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

Theorem ioodvbdlimc2lem 37081
Description: Limit at the upper bound of an open interval, for a function with bounded derivative. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
ioodvbdlimc2lem.a  |-  ( ph  ->  A  e.  RR )
ioodvbdlimc2lem.b  |-  ( ph  ->  B  e.  RR )
ioodvbdlimc2lem.altb  |-  ( ph  ->  A  <  B )
ioodvbdlimc2lem.f  |-  ( ph  ->  F : ( A (,) B ) --> RR )
ioodvbdlimc2lem.dmdv  |-  ( ph  ->  dom  ( RR  _D  F )  =  ( A (,) B ) )
ioodvbdlimc2lem.dvbd  |-  ( ph  ->  E. y  e.  RR  A. x  e.  ( A (,) B ) ( abs `  ( ( RR  _D  F ) `
 x ) )  <_  y )
ioodvbdlimc2lem.y  |-  Y  =  sup ( ran  (
x  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `
 x ) ) ) ,  RR ,  <  )
ioodvbdlimc2lem.m  |-  M  =  ( ( |_ `  ( 1  /  ( B  -  A )
) )  +  1 )
ioodvbdlimc2lem.s  |-  S  =  ( j  e.  (
ZZ>= `  M )  |->  ( F `  ( B  -  ( 1  / 
j ) ) ) )
ioodvbdlimc2lem.r  |-  R  =  ( j  e.  (
ZZ>= `  M )  |->  ( B  -  ( 1  /  j ) ) )
ioodvbdlimc2lem.n  |-  N  =  if ( M  <_ 
( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 ) ,  ( ( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) ,  M )
ioodvbdlimc2lem.ch  |-  ( ch  <->  ( ( ( ( (
ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  /\  ( abs `  ( ( S `  j )  -  ( limsup `
 S ) ) )  <  ( x  /  2 ) )  /\  z  e.  ( A (,) B ) )  /\  ( abs `  ( z  -  B
) )  <  (
1  /  j ) ) )
Assertion
Ref Expression
ioodvbdlimc2lem  |-  ( ph  ->  ( limsup `  S )  e.  ( F lim CC  B
) )
Distinct variable groups:    A, j, x, z, y    B, j, x, z, y    j, F, x, z, y    j, M, x, y    j, N, z    R, j, x, y   
x, S, j, y, z    x, Y    ph, x, j, z, y
Allowed substitution hints:    ch( x, y, z, j)    R( z)    M( z)    N( x, y)    Y( y, z, j)

Proof of Theorem ioodvbdlimc2lem
Dummy variables  b 
k  h  i  l  w  m  c  a are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uzssz 11064 . . . . . 6  |-  ( ZZ>= `  M )  C_  ZZ
2 zssre 10832 . . . . . 6  |-  ZZ  C_  RR
31, 2sstri 3450 . . . . 5  |-  ( ZZ>= `  M )  C_  RR
43a1i 11 . . . 4  |-  ( ph  ->  ( ZZ>= `  M )  C_  RR )
5 ioodvbdlimc2lem.m . . . . . . 7  |-  M  =  ( ( |_ `  ( 1  /  ( B  -  A )
) )  +  1 )
6 ioodvbdlimc2lem.b . . . . . . . . . . 11  |-  ( ph  ->  B  e.  RR )
7 ioodvbdlimc2lem.a . . . . . . . . . . 11  |-  ( ph  ->  A  e.  RR )
86, 7resubcld 9948 . . . . . . . . . 10  |-  ( ph  ->  ( B  -  A
)  e.  RR )
9 ioodvbdlimc2lem.altb . . . . . . . . . . . 12  |-  ( ph  ->  A  <  B )
107, 6posdifd 10099 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  <  B  <->  0  <  ( B  -  A ) ) )
119, 10mpbid 210 . . . . . . . . . . 11  |-  ( ph  ->  0  <  ( B  -  A ) )
1211gt0ne0d 10077 . . . . . . . . . 10  |-  ( ph  ->  ( B  -  A
)  =/=  0 )
138, 12rereccld 10332 . . . . . . . . 9  |-  ( ph  ->  ( 1  /  ( B  -  A )
)  e.  RR )
14 0red 9547 . . . . . . . . . 10  |-  ( ph  ->  0  e.  RR )
158, 11recgt0d 10440 . . . . . . . . . 10  |-  ( ph  ->  0  <  ( 1  /  ( B  -  A ) ) )
1614, 13, 15ltled 9685 . . . . . . . . 9  |-  ( ph  ->  0  <_  ( 1  /  ( B  -  A ) ) )
17 flge0nn0 11905 . . . . . . . . 9  |-  ( ( ( 1  /  ( B  -  A )
)  e.  RR  /\  0  <_  ( 1  / 
( B  -  A
) ) )  -> 
( |_ `  (
1  /  ( B  -  A ) ) )  e.  NN0 )
1813, 16, 17syl2anc 659 . . . . . . . 8  |-  ( ph  ->  ( |_ `  (
1  /  ( B  -  A ) ) )  e.  NN0 )
19 peano2nn0 10797 . . . . . . . 8  |-  ( ( |_ `  ( 1  /  ( B  -  A ) ) )  e.  NN0  ->  ( ( |_ `  ( 1  /  ( B  -  A ) ) )  +  1 )  e. 
NN0 )
2018, 19syl 17 . . . . . . 7  |-  ( ph  ->  ( ( |_ `  ( 1  /  ( B  -  A )
) )  +  1 )  e.  NN0 )
215, 20syl5eqel 2494 . . . . . 6  |-  ( ph  ->  M  e.  NN0 )
2221nn0zd 10926 . . . . 5  |-  ( ph  ->  M  e.  ZZ )
23 eqid 2402 . . . . . 6  |-  ( ZZ>= `  M )  =  (
ZZ>= `  M )
2423uzsup 11941 . . . . 5  |-  ( M  e.  ZZ  ->  sup ( ( ZZ>= `  M
) ,  RR* ,  <  )  = +oo )
2522, 24syl 17 . . . 4  |-  ( ph  ->  sup ( ( ZZ>= `  M ) ,  RR* ,  <  )  = +oo )
26 ioodvbdlimc2lem.f . . . . . . 7  |-  ( ph  ->  F : ( A (,) B ) --> RR )
2726adantr 463 . . . . . 6  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  F :
( A (,) B
) --> RR )
287rexrd 9593 . . . . . . . 8  |-  ( ph  ->  A  e.  RR* )
2928adantr 463 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  A  e.  RR* )
306rexrd 9593 . . . . . . . 8  |-  ( ph  ->  B  e.  RR* )
3130adantr 463 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  B  e.  RR* )
326adantr 463 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  B  e.  RR )
33 eluzelre 11055 . . . . . . . . . 10  |-  ( j  e.  ( ZZ>= `  M
)  ->  j  e.  RR )
3433adantl 464 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  j  e.  RR )
35 0red 9547 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  0  e.  RR )
36 0red 9547 . . . . . . . . . . . . 13  |-  ( j  e.  ( ZZ>= `  M
)  ->  0  e.  RR )
37 1red 9561 . . . . . . . . . . . . 13  |-  ( j  e.  ( ZZ>= `  M
)  ->  1  e.  RR )
3836, 37readdcld 9573 . . . . . . . . . . . 12  |-  ( j  e.  ( ZZ>= `  M
)  ->  ( 0  +  1 )  e.  RR )
3938adantl 464 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( 0  +  1 )  e.  RR )
4036ltp1d 10436 . . . . . . . . . . . 12  |-  ( j  e.  ( ZZ>= `  M
)  ->  0  <  ( 0  +  1 ) )
4140adantl 464 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  0  <  ( 0  +  1 ) )
42 eluzel2 11050 . . . . . . . . . . . . . 14  |-  ( j  e.  ( ZZ>= `  M
)  ->  M  e.  ZZ )
4342zred 10928 . . . . . . . . . . . . 13  |-  ( j  e.  ( ZZ>= `  M
)  ->  M  e.  RR )
4443adantl 464 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  M  e.  RR )
4513flcld 11885 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( |_ `  (
1  /  ( B  -  A ) ) )  e.  ZZ )
4645zred 10928 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( |_ `  (
1  /  ( B  -  A ) ) )  e.  RR )
47 1red 9561 . . . . . . . . . . . . . . 15  |-  ( ph  ->  1  e.  RR )
4818nn0ge0d 10816 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  <_  ( |_ `  ( 1  /  ( B  -  A )
) ) )
4914, 46, 47, 48leadd1dd 10126 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0  +  1 )  <_  ( ( |_ `  ( 1  / 
( B  -  A
) ) )  +  1 ) )
5049, 5syl6breqr 4434 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 0  +  1 )  <_  M )
5150adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( 0  +  1 )  <_  M )
52 eluzle 11057 . . . . . . . . . . . . 13  |-  ( j  e.  ( ZZ>= `  M
)  ->  M  <_  j )
5352adantl 464 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  M  <_  j )
5439, 44, 34, 51, 53letrd 9693 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( 0  +  1 )  <_ 
j )
5535, 39, 34, 41, 54ltletrd 9696 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  0  <  j )
5655gt0ne0d 10077 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  j  =/=  0 )
5734, 56rereccld 10332 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( 1  /  j )  e.  RR )
5832, 57resubcld 9948 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( B  -  ( 1  / 
j ) )  e.  RR )
597adantr 463 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  A  e.  RR )
6021nn0red 10814 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  RR )
6114, 47readdcld 9573 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0  +  1 )  e.  RR )
6246, 47readdcld 9573 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( |_ `  ( 1  /  ( B  -  A )
) )  +  1 )  e.  RR )
6314ltp1d 10436 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <  ( 0  +  1 ) )
6414, 61, 62, 63, 49ltletrd 9696 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <  ( ( |_ `  ( 1  /  ( B  -  A ) ) )  +  1 ) )
6564, 5syl6breqr 4434 . . . . . . . . . . . 12  |-  ( ph  ->  0  <  M )
6665gt0ne0d 10077 . . . . . . . . . . 11  |-  ( ph  ->  M  =/=  0 )
6760, 66rereccld 10332 . . . . . . . . . 10  |-  ( ph  ->  ( 1  /  M
)  e.  RR )
6867adantr 463 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( 1  /  M )  e.  RR )
6932, 68resubcld 9948 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( B  -  ( 1  /  M ) )  e.  RR )
705eqcomi 2415 . . . . . . . . . . . . 13  |-  ( ( |_ `  ( 1  /  ( B  -  A ) ) )  +  1 )  =  M
7170oveq2i 6245 . . . . . . . . . . . 12  |-  ( 1  /  ( ( |_
`  ( 1  / 
( B  -  A
) ) )  +  1 ) )  =  ( 1  /  M
)
7271, 67syl5eqel 2494 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  /  (
( |_ `  (
1  /  ( B  -  A ) ) )  +  1 ) )  e.  RR )
7313, 15elrpd 11219 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1  /  ( B  -  A )
)  e.  RR+ )
7462, 64elrpd 11219 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( |_ `  ( 1  /  ( B  -  A )
) )  +  1 )  e.  RR+ )
75 1rp 11187 . . . . . . . . . . . . . 14  |-  1  e.  RR+
7675a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  1  e.  RR+ )
77 fllelt 11884 . . . . . . . . . . . . . . 15  |-  ( ( 1  /  ( B  -  A ) )  e.  RR  ->  (
( |_ `  (
1  /  ( B  -  A ) ) )  <_  ( 1  /  ( B  -  A ) )  /\  ( 1  /  ( B  -  A )
)  <  ( ( |_ `  ( 1  / 
( B  -  A
) ) )  +  1 ) ) )
7813, 77syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( |_ `  ( 1  /  ( B  -  A )
) )  <_  (
1  /  ( B  -  A ) )  /\  ( 1  / 
( B  -  A
) )  <  (
( |_ `  (
1  /  ( B  -  A ) ) )  +  1 ) ) )
7978simprd 461 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1  /  ( B  -  A )
)  <  ( ( |_ `  ( 1  / 
( B  -  A
) ) )  +  1 ) )
8073, 74, 76, 79ltdiv2dd 36838 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  /  (
( |_ `  (
1  /  ( B  -  A ) ) )  +  1 ) )  <  ( 1  /  ( 1  / 
( B  -  A
) ) ) )
818recnd 9572 . . . . . . . . . . . . 13  |-  ( ph  ->  ( B  -  A
)  e.  CC )
8281, 12recrecd 10278 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  /  (
1  /  ( B  -  A ) ) )  =  ( B  -  A ) )
8380, 82breqtrd 4418 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  /  (
( |_ `  (
1  /  ( B  -  A ) ) )  +  1 ) )  <  ( B  -  A ) )
8472, 8, 6, 83ltsub2dd 10125 . . . . . . . . . 10  |-  ( ph  ->  ( B  -  ( B  -  A )
)  <  ( B  -  ( 1  / 
( ( |_ `  ( 1  /  ( B  -  A )
) )  +  1 ) ) ) )
856recnd 9572 . . . . . . . . . . 11  |-  ( ph  ->  B  e.  CC )
867recnd 9572 . . . . . . . . . . 11  |-  ( ph  ->  A  e.  CC )
8785, 86nncand 9892 . . . . . . . . . 10  |-  ( ph  ->  ( B  -  ( B  -  A )
)  =  A )
8871oveq2i 6245 . . . . . . . . . . 11  |-  ( B  -  ( 1  / 
( ( |_ `  ( 1  /  ( B  -  A )
) )  +  1 ) ) )  =  ( B  -  (
1  /  M ) )
8988a1i 11 . . . . . . . . . 10  |-  ( ph  ->  ( B  -  (
1  /  ( ( |_ `  ( 1  /  ( B  -  A ) ) )  +  1 ) ) )  =  ( B  -  ( 1  /  M ) ) )
9084, 87, 893brtr3d 4423 . . . . . . . . 9  |-  ( ph  ->  A  <  ( B  -  ( 1  /  M ) ) )
9190adantr 463 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  A  <  ( B  -  ( 1  /  M ) ) )
9260, 65elrpd 11219 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  RR+ )
9392adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  M  e.  RR+ )
9434, 55elrpd 11219 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  j  e.  RR+ )
95 1red 9561 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  1  e.  RR )
96 0le1 10036 . . . . . . . . . . 11  |-  0  <_  1
9796a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  0  <_  1 )
9893, 94, 95, 97, 53lediv2ad 11244 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( 1  /  j )  <_ 
( 1  /  M
) )
9957, 68, 32, 98lesub2dd 10129 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( B  -  ( 1  /  M ) )  <_ 
( B  -  (
1  /  j ) ) )
10059, 69, 58, 91, 99ltletrd 9696 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  A  <  ( B  -  ( 1  /  j ) ) )
10194rpreccld 11232 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( 1  /  j )  e.  RR+ )
10232, 101ltsubrpd 11250 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( B  -  ( 1  / 
j ) )  < 
B )
10329, 31, 58, 100, 102eliood 36881 . . . . . 6  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( B  -  ( 1  / 
j ) )  e.  ( A (,) B
) )
10427, 103ffvelrnd 5966 . . . . 5  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( F `  ( B  -  (
1  /  j ) ) )  e.  RR )
105 ioodvbdlimc2lem.s . . . . 5  |-  S  =  ( j  e.  (
ZZ>= `  M )  |->  ( F `  ( B  -  ( 1  / 
j ) ) ) )
106104, 105fmptd 5989 . . . 4  |-  ( ph  ->  S : ( ZZ>= `  M ) --> RR )
107 ioodvbdlimc2lem.dmdv . . . . . 6  |-  ( ph  ->  dom  ( RR  _D  F )  =  ( A (,) B ) )
108 ioodvbdlimc2lem.dvbd . . . . . 6  |-  ( ph  ->  E. y  e.  RR  A. x  e.  ( A (,) B ) ( abs `  ( ( RR  _D  F ) `
 x ) )  <_  y )
1097, 6, 9, 26, 107, 108dvbdfbdioo 37077 . . . . 5  |-  ( ph  ->  E. b  e.  RR  A. x  e.  ( A (,) B ) ( abs `  ( F `
 x ) )  <_  b )
11060adantr 463 . . . . . . . 8  |-  ( (
ph  /\  A. x  e.  ( A (,) B
) ( abs `  ( F `  x )
)  <_  b )  ->  M  e.  RR )
111 simpr 459 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  j  e.  ( ZZ>= `  M )
)
112105fvmpt2 5897 . . . . . . . . . . . . . 14  |-  ( ( j  e.  ( ZZ>= `  M )  /\  ( F `  ( B  -  ( 1  / 
j ) ) )  e.  RR )  -> 
( S `  j
)  =  ( F `
 ( B  -  ( 1  /  j
) ) ) )
113111, 104, 112syl2anc 659 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( S `  j )  =  ( F `  ( B  -  ( 1  / 
j ) ) ) )
114113fveq2d 5809 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( abs `  ( S `  j
) )  =  ( abs `  ( F `
 ( B  -  ( 1  /  j
) ) ) ) )
115114adantlr 713 . . . . . . . . . . 11  |-  ( ( ( ph  /\  A. x  e.  ( A (,) B ) ( abs `  ( F `  x
) )  <_  b
)  /\  j  e.  ( ZZ>= `  M )
)  ->  ( abs `  ( S `  j
) )  =  ( abs `  ( F `
 ( B  -  ( 1  /  j
) ) ) ) )
116 simplr 754 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  A. x  e.  ( A (,) B ) ( abs `  ( F `  x
) )  <_  b
)  /\  j  e.  ( ZZ>= `  M )
)  ->  A. x  e.  ( A (,) B
) ( abs `  ( F `  x )
)  <_  b )
117103adantlr 713 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  A. x  e.  ( A (,) B ) ( abs `  ( F `  x
) )  <_  b
)  /\  j  e.  ( ZZ>= `  M )
)  ->  ( B  -  ( 1  / 
j ) )  e.  ( A (,) B
) )
118 fveq2 5805 . . . . . . . . . . . . . . 15  |-  ( x  =  ( B  -  ( 1  /  j
) )  ->  ( F `  x )  =  ( F `  ( B  -  (
1  /  j ) ) ) )
119118fveq2d 5809 . . . . . . . . . . . . . 14  |-  ( x  =  ( B  -  ( 1  /  j
) )  ->  ( abs `  ( F `  x ) )  =  ( abs `  ( F `  ( B  -  ( 1  / 
j ) ) ) ) )
120119breq1d 4404 . . . . . . . . . . . . 13  |-  ( x  =  ( B  -  ( 1  /  j
) )  ->  (
( abs `  ( F `  x )
)  <_  b  <->  ( abs `  ( F `  ( B  -  ( 1  /  j ) ) ) )  <_  b
) )
121120rspccva 3158 . . . . . . . . . . . 12  |-  ( ( A. x  e.  ( A (,) B ) ( abs `  ( F `  x )
)  <_  b  /\  ( B  -  (
1  /  j ) )  e.  ( A (,) B ) )  ->  ( abs `  ( F `  ( B  -  ( 1  / 
j ) ) ) )  <_  b )
122116, 117, 121syl2anc 659 . . . . . . . . . . 11  |-  ( ( ( ph  /\  A. x  e.  ( A (,) B ) ( abs `  ( F `  x
) )  <_  b
)  /\  j  e.  ( ZZ>= `  M )
)  ->  ( abs `  ( F `  ( B  -  ( 1  /  j ) ) ) )  <_  b
)
123115, 122eqbrtrd 4414 . . . . . . . . . 10  |-  ( ( ( ph  /\  A. x  e.  ( A (,) B ) ( abs `  ( F `  x
) )  <_  b
)  /\  j  e.  ( ZZ>= `  M )
)  ->  ( abs `  ( S `  j
) )  <_  b
)
124123a1d 25 . . . . . . . . 9  |-  ( ( ( ph  /\  A. x  e.  ( A (,) B ) ( abs `  ( F `  x
) )  <_  b
)  /\  j  e.  ( ZZ>= `  M )
)  ->  ( M  <_  j  ->  ( abs `  ( S `  j
) )  <_  b
) )
125124ralrimiva 2817 . . . . . . . 8  |-  ( (
ph  /\  A. x  e.  ( A (,) B
) ( abs `  ( F `  x )
)  <_  b )  ->  A. j  e.  (
ZZ>= `  M ) ( M  <_  j  ->  ( abs `  ( S `
 j ) )  <_  b ) )
126 breq1 4397 . . . . . . . . . . 11  |-  ( k  =  M  ->  (
k  <_  j  <->  M  <_  j ) )
127126imbi1d 315 . . . . . . . . . 10  |-  ( k  =  M  ->  (
( k  <_  j  ->  ( abs `  ( S `  j )
)  <_  b )  <->  ( M  <_  j  ->  ( abs `  ( S `
 j ) )  <_  b ) ) )
128127ralbidv 2842 . . . . . . . . 9  |-  ( k  =  M  ->  ( A. j  e.  ( ZZ>=
`  M ) ( k  <_  j  ->  ( abs `  ( S `
 j ) )  <_  b )  <->  A. j  e.  ( ZZ>= `  M )
( M  <_  j  ->  ( abs `  ( S `  j )
)  <_  b )
) )
129128rspcev 3159 . . . . . . . 8  |-  ( ( M  e.  RR  /\  A. j  e.  ( ZZ>= `  M ) ( M  <_  j  ->  ( abs `  ( S `  j ) )  <_ 
b ) )  ->  E. k  e.  RR  A. j  e.  ( ZZ>= `  M ) ( k  <_  j  ->  ( abs `  ( S `  j ) )  <_ 
b ) )
130110, 125, 129syl2anc 659 . . . . . . 7  |-  ( (
ph  /\  A. x  e.  ( A (,) B
) ( abs `  ( F `  x )
)  <_  b )  ->  E. k  e.  RR  A. j  e.  ( ZZ>= `  M ) ( k  <_  j  ->  ( abs `  ( S `  j ) )  <_ 
b ) )
131130ex 432 . . . . . 6  |-  ( ph  ->  ( A. x  e.  ( A (,) B
) ( abs `  ( F `  x )
)  <_  b  ->  E. k  e.  RR  A. j  e.  ( ZZ>= `  M ) ( k  <_  j  ->  ( abs `  ( S `  j ) )  <_ 
b ) ) )
132131reximdv 2877 . . . . 5  |-  ( ph  ->  ( E. b  e.  RR  A. x  e.  ( A (,) B
) ( abs `  ( F `  x )
)  <_  b  ->  E. b  e.  RR  E. k  e.  RR  A. j  e.  ( ZZ>= `  M )
( k  <_  j  ->  ( abs `  ( S `  j )
)  <_  b )
) )
133109, 132mpd 15 . . . 4  |-  ( ph  ->  E. b  e.  RR  E. k  e.  RR  A. j  e.  ( ZZ>= `  M ) ( k  <_  j  ->  ( abs `  ( S `  j ) )  <_ 
b ) )
1344, 25, 106, 133limsupre 36997 . . 3  |-  ( ph  ->  ( limsup `  S )  e.  RR )
135134recnd 9572 . 2  |-  ( ph  ->  ( limsup `  S )  e.  CC )
136 eluzelre 11055 . . . . . . . . 9  |-  ( j  e.  ( ZZ>= `  N
)  ->  j  e.  RR )
137136adantl 464 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  j  e.  RR )
138 0red 9547 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  0  e.  RR )
13945peano2zd 10931 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( |_ `  ( 1  /  ( B  -  A )
) )  +  1 )  e.  ZZ )
1405, 139syl5eqel 2494 . . . . . . . . . . . . 13  |-  ( ph  ->  M  e.  ZZ )
141140adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  M  e.  ZZ )
142141zred 10928 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  M  e.  RR )
143142adantr 463 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  M  e.  RR )
14465ad2antrr 724 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  0  <  M )
145 ioodvbdlimc2lem.n . . . . . . . . . . . . . 14  |-  N  =  if ( M  <_ 
( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 ) ,  ( ( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) ,  M )
146 ioodvbdlimc2lem.y . . . . . . . . . . . . . . . . . . . 20  |-  Y  =  sup ( ran  (
x  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `
 x ) ) ) ,  RR ,  <  )
147 ioomidp 36904 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  (
( A  +  B
)  /  2 )  e.  ( A (,) B ) )
1487, 6, 9, 147syl3anc 1230 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( A  +  B )  /  2
)  e.  ( A (,) B ) )
149 ne0i 3743 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( A  +  B
)  /  2 )  e.  ( A (,) B )  ->  ( A (,) B )  =/=  (/) )
150148, 149syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( A (,) B
)  =/=  (/) )
151 ioossre 11557 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( A (,) B )  C_  RR
152151a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( A (,) B
)  C_  RR )
153 dvfre 22538 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( F : ( A (,) B ) --> RR 
/\  ( A (,) B )  C_  RR )  ->  ( RR  _D  F ) : dom  ( RR  _D  F
) --> RR )
15426, 152, 153syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( RR  _D  F
) : dom  ( RR  _D  F ) --> RR )
155107feq2d 5657 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( RR  _D  F ) : dom  ( RR  _D  F
) --> RR  <->  ( RR  _D  F ) : ( A (,) B ) --> RR ) )
156154, 155mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( RR  _D  F
) : ( A (,) B ) --> RR )
157156ffvelrnda 5965 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( ( RR  _D  F ) `  x )  e.  RR )
158157recnd 9572 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( ( RR  _D  F ) `  x )  e.  CC )
159158abscld 13323 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( abs `  ( ( RR  _D  F ) `  x
) )  e.  RR )
160 eqid 2402 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `  x
) ) )  =  ( x  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  x )
) )
161 eqid 2402 . . . . . . . . . . . . . . . . . . . . . 22  |-  sup ( ran  ( x  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  x )
) ) ,  RR ,  <  )  =  sup ( ran  ( x  e.  ( A (,) B
)  |->  ( abs `  (
( RR  _D  F
) `  x )
) ) ,  RR ,  <  )
162150, 159, 108, 160, 161suprnmpt 36807 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ,  <  ) ) )
163162simpld 457 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  sup ( ran  (
x  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `
 x ) ) ) ,  RR ,  <  )  e.  RR )
164146, 163syl5eqel 2494 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  Y  e.  RR )
165164adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR+ )  ->  Y  e.  RR )
166 rpre 11189 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR+  ->  x  e.  RR )
167166rehalfcld 10746 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  RR+  ->  ( x  /  2 )  e.  RR )
168167adantl 464 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( x  /  2 )  e.  RR )
169166recnd 9572 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR+  ->  x  e.  CC )
170169adantl 464 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  e.  CC )
171 2cnd 10569 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR+ )  ->  2  e.  CC )
172 rpne0 11198 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR+  ->  x  =/=  0 )
173172adantl 464 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  =/=  0 )
174 2ne0 10589 . . . . . . . . . . . . . . . . . . . 20  |-  2  =/=  0
175174a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR+ )  ->  2  =/=  0 )
176170, 171, 173, 175divne0d 10297 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( x  /  2 )  =/=  0 )
177165, 168, 176redivcld 10333 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( Y  /  ( x  / 
2 ) )  e.  RR )
178177flcld 11885 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( |_ `  ( Y  /  (
x  /  2 ) ) )  e.  ZZ )
179178peano2zd 10931 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( |_ `  ( Y  / 
( x  /  2
) ) )  +  1 )  e.  ZZ )
180179, 141ifcld 3927 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  if ( M  <_  ( ( |_
`  ( Y  / 
( x  /  2
) ) )  +  1 ) ,  ( ( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) ,  M )  e.  ZZ )
181145, 180syl5eqel 2494 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  N  e.  ZZ )
182181zred 10928 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  N  e.  RR )
183182adantr 463 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  N  e.  RR )
184179zred 10928 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( |_ `  ( Y  / 
( x  /  2
) ) )  +  1 )  e.  RR )
185 max1 11357 . . . . . . . . . . . . . 14  |-  ( ( M  e.  RR  /\  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 )  e.  RR )  ->  M  <_  if ( M  <_  ( ( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) ,  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 ) ,  M ) )
186142, 184, 185syl2anc 659 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  M  <_  if ( M  <_  (
( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) ,  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 ) ,  M ) )
187186, 145syl6breqr 4434 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  M  <_  N )
188187adantr 463 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  M  <_  N )
189 eluzle 11057 . . . . . . . . . . . 12  |-  ( j  e.  ( ZZ>= `  N
)  ->  N  <_  j )
190189adantl 464 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  N  <_  j )
191143, 183, 137, 188, 190letrd 9693 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  M  <_  j )
192138, 143, 137, 144, 191ltletrd 9696 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  0  <  j )
193192gt0ne0d 10077 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  j  =/=  0 )
194137, 193rereccld 10332 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  ( 1  /  j )  e.  RR )
195137, 192recgt0d 10440 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  0  <  ( 1  /  j ) )
196194, 195elrpd 11219 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  ( 1  /  j )  e.  RR+ )
197196adantr 463 . . . . 5  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N ) )  /\  ( abs `  ( ( S `  j )  -  ( limsup `  S
) ) )  < 
( x  /  2
) )  ->  (
1  /  j )  e.  RR+ )
198 ioodvbdlimc2lem.ch . . . . . . . . 9  |-  ( ch  <->  ( ( ( ( (
ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  /\  ( abs `  ( ( S `  j )  -  ( limsup `
 S ) ) )  <  ( x  /  2 ) )  /\  z  e.  ( A (,) B ) )  /\  ( abs `  ( z  -  B
) )  <  (
1  /  j ) ) )
199198biimpi 194 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  /\  ( abs `  ( ( S `  j )  -  ( limsup `
 S ) ) )  <  ( x  /  2 ) )  /\  z  e.  ( A (,) B ) )  /\  ( abs `  ( z  -  B
) )  <  (
1  /  j ) ) )
200 simp-5l 770 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  /\  ( abs `  ( ( S `  j )  -  ( limsup `
 S ) ) )  <  ( x  /  2 ) )  /\  z  e.  ( A (,) B ) )  /\  ( abs `  ( z  -  B
) )  <  (
1  /  j ) )  ->  ph )
201199, 200syl 17 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ph )
202201, 26syl 17 . . . . . . . . . . . . . . 15  |-  ( ch 
->  F : ( A (,) B ) --> RR )
203199simplrd 755 . . . . . . . . . . . . . . 15  |-  ( ch 
->  z  e.  ( A (,) B ) )
204202, 203ffvelrnd 5966 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( F `  z
)  e.  RR )
205204recnd 9572 . . . . . . . . . . . . 13  |-  ( ch 
->  ( F `  z
)  e.  CC )
206201, 106syl 17 . . . . . . . . . . . . . . 15  |-  ( ch 
->  S : ( ZZ>= `  M ) --> RR )
207 simp-5r 771 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  /\  ( abs `  ( ( S `  j )  -  ( limsup `
 S ) ) )  <  ( x  /  2 ) )  /\  z  e.  ( A (,) B ) )  /\  ( abs `  ( z  -  B
) )  <  (
1  /  j ) )  ->  x  e.  RR+ )
208199, 207syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  x  e.  RR+ )
209 eluz2 11051 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  N  e.  ZZ  /\  M  <_  N ) )
210141, 181, 187, 209syl3anbrc 1181 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR+ )  ->  N  e.  ( ZZ>= `  M )
)
211201, 208, 210syl2anc 659 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  N  e.  ( ZZ>=
`  M ) )
212 uzss 11065 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( ZZ>= `  N )  C_  ( ZZ>=
`  M ) )
213211, 212syl 17 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( ZZ>= `  N )  C_  ( ZZ>= `  M )
)
214 simp-4r 769 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  /\  ( abs `  ( ( S `  j )  -  ( limsup `
 S ) ) )  <  ( x  /  2 ) )  /\  z  e.  ( A (,) B ) )  /\  ( abs `  ( z  -  B
) )  <  (
1  /  j ) )  ->  j  e.  ( ZZ>= `  N )
)
215199, 214syl 17 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  j  e.  ( ZZ>=
`  N ) )
216213, 215sseldd 3442 . . . . . . . . . . . . . . 15  |-  ( ch 
->  j  e.  ( ZZ>=
`  M ) )
217206, 216ffvelrnd 5966 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( S `  j
)  e.  RR )
218217recnd 9572 . . . . . . . . . . . . 13  |-  ( ch 
->  ( S `  j
)  e.  CC )
219201, 135syl 17 . . . . . . . . . . . . 13  |-  ( ch 
->  ( limsup `  S )  e.  CC )
220205, 218, 219npncand 9911 . . . . . . . . . . . 12  |-  ( ch 
->  ( ( ( F `
 z )  -  ( S `  j ) )  +  ( ( S `  j )  -  ( limsup `  S
) ) )  =  ( ( F `  z )  -  ( limsup `
 S ) ) )
221220eqcomd 2410 . . . . . . . . . . 11  |-  ( ch 
->  ( ( F `  z )  -  ( limsup `
 S ) )  =  ( ( ( F `  z )  -  ( S `  j ) )  +  ( ( S `  j )  -  ( limsup `
 S ) ) ) )
222221fveq2d 5809 . . . . . . . . . 10  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( limsup `  S ) ) )  =  ( abs `  (
( ( F `  z )  -  ( S `  j )
)  +  ( ( S `  j )  -  ( limsup `  S
) ) ) ) )
223204, 217resubcld 9948 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( ( F `  z )  -  ( S `  j )
)  e.  RR )
224201, 134syl 17 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( limsup `  S )  e.  RR )
225217, 224resubcld 9948 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( ( S `  j )  -  ( limsup `
 S ) )  e.  RR )
226223, 225readdcld 9573 . . . . . . . . . . . . 13  |-  ( ch 
->  ( ( ( F `
 z )  -  ( S `  j ) )  +  ( ( S `  j )  -  ( limsup `  S
) ) )  e.  RR )
227226recnd 9572 . . . . . . . . . . . 12  |-  ( ch 
->  ( ( ( F `
 z )  -  ( S `  j ) )  +  ( ( S `  j )  -  ( limsup `  S
) ) )  e.  CC )
228227abscld 13323 . . . . . . . . . . 11  |-  ( ch 
->  ( abs `  (
( ( F `  z )  -  ( S `  j )
)  +  ( ( S `  j )  -  ( limsup `  S
) ) ) )  e.  RR )
229223recnd 9572 . . . . . . . . . . . . 13  |-  ( ch 
->  ( ( F `  z )  -  ( S `  j )
)  e.  CC )
230229abscld 13323 . . . . . . . . . . . 12  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( S `
 j ) ) )  e.  RR )
231225recnd 9572 . . . . . . . . . . . . 13  |-  ( ch 
->  ( ( S `  j )  -  ( limsup `
 S ) )  e.  CC )
232231abscld 13323 . . . . . . . . . . . 12  |-  ( ch 
->  ( abs `  (
( S `  j
)  -  ( limsup `  S ) ) )  e.  RR )
233230, 232readdcld 9573 . . . . . . . . . . 11  |-  ( ch 
->  ( ( abs `  (
( F `  z
)  -  ( S `
 j ) ) )  +  ( abs `  ( ( S `  j )  -  ( limsup `
 S ) ) ) )  e.  RR )
234208rpred 11222 . . . . . . . . . . 11  |-  ( ch 
->  x  e.  RR )
235229, 231abstrid 13343 . . . . . . . . . . 11  |-  ( ch 
->  ( abs `  (
( ( F `  z )  -  ( S `  j )
)  +  ( ( S `  j )  -  ( limsup `  S
) ) ) )  <_  ( ( abs `  ( ( F `  z )  -  ( S `  j )
) )  +  ( abs `  ( ( S `  j )  -  ( limsup `  S
) ) ) ) )
236234rehalfcld 10746 . . . . . . . . . . . . 13  |-  ( ch 
->  ( x  /  2
)  e.  RR )
237201, 216, 113syl2anc 659 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( S `  j
)  =  ( F `
 ( B  -  ( 1  /  j
) ) ) )
238237oveq2d 6250 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( ( F `  z )  -  ( S `  j )
)  =  ( ( F `  z )  -  ( F `  ( B  -  (
1  /  j ) ) ) ) )
239238fveq2d 5809 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( S `
 j ) ) )  =  ( abs `  ( ( F `  z )  -  ( F `  ( B  -  ( 1  / 
j ) ) ) ) ) )
240239, 230eqeltrrd 2491 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( F `
 ( B  -  ( 1  /  j
) ) ) ) )  e.  RR )
241201, 164syl 17 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  Y  e.  RR )
242151, 203sseldi 3439 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  z  e.  RR )
243201, 216, 58syl2anc 659 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( B  -  (
1  /  j ) )  e.  RR )
244242, 243resubcld 9948 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( z  -  ( B  -  ( 1  /  j ) ) )  e.  RR )
245241, 244remulcld 9574 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( Y  x.  (
z  -  ( B  -  ( 1  / 
j ) ) ) )  e.  RR )
246201, 7syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  A  e.  RR )
247201, 6syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  B  e.  RR )
248201, 107syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  dom  ( RR  _D  F )  =  ( A (,) B ) )
249162simprd 461 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  A. x  e.  ( A (,) B ) ( abs `  (
( RR  _D  F
) `  x )
)  <_  sup ( ran  ( x  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  x )
) ) ,  RR ,  <  ) )
250146breq2i 4402 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( abs `  ( ( RR  _D  F ) `
 x ) )  <_  Y  <->  ( abs `  ( ( RR  _D  F ) `  x
) )  <_  sup ( ran  ( x  e.  ( A (,) B
)  |->  ( abs `  (
( RR  _D  F
) `  x )
) ) ,  RR ,  <  ) )
251250ralbii 2834 . . . . . . . . . . . . . . . . . . . 20  |-  ( A. x  e.  ( A (,) B ) ( abs `  ( ( RR  _D  F ) `  x
) )  <_  Y  <->  A. x  e.  ( A (,) B ) ( abs `  ( ( RR  _D  F ) `
 x ) )  <_  sup ( ran  (
x  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `
 x ) ) ) ,  RR ,  <  ) )
252249, 251sylibr 212 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A. x  e.  ( A (,) B ) ( abs `  (
( RR  _D  F
) `  x )
)  <_  Y )
253201, 252syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  A. x  e.  ( A (,) B ) ( abs `  (
( RR  _D  F
) `  x )
)  <_  Y )
254 fveq2 5805 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  =  x  ->  (
( RR  _D  F
) `  w )  =  ( ( RR 
_D  F ) `  x ) )
255254fveq2d 5809 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  x  ->  ( abs `  ( ( RR 
_D  F ) `  w ) )  =  ( abs `  (
( RR  _D  F
) `  x )
) )
256255breq1d 4404 . . . . . . . . . . . . . . . . . . 19  |-  ( w  =  x  ->  (
( abs `  (
( RR  _D  F
) `  w )
)  <_  Y  <->  ( abs `  ( ( RR  _D  F ) `  x
) )  <_  Y
) )
257256cbvralv 3033 . . . . . . . . . . . . . . . . . 18  |-  ( A. w  e.  ( A (,) B ) ( abs `  ( ( RR  _D  F ) `  w
) )  <_  Y  <->  A. x  e.  ( A (,) B ) ( abs `  ( ( RR  _D  F ) `
 x ) )  <_  Y )
258253, 257sylibr 212 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  A. w  e.  ( A (,) B ) ( abs `  (
( RR  _D  F
) `  w )
)  <_  Y )
259201, 216, 103syl2anc 659 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( B  -  (
1  /  j ) )  e.  ( A (,) B ) )
260243rexrd 9593 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( B  -  (
1  /  j ) )  e.  RR* )
261201, 30syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  B  e.  RR* )
2623, 216sseldi 3439 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  j  e.  RR )
263201, 216, 56syl2anc 659 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  j  =/=  0
)
264262, 263rereccld 10332 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( 1  /  j
)  e.  RR )
265247, 242resubcld 9948 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( B  -  z
)  e.  RR )
266242, 247resubcld 9948 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( z  -  B
)  e.  RR )
267266recnd 9572 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( z  -  B
)  e.  CC )
268267abscld 13323 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( abs `  (
z  -  B ) )  e.  RR )
269265leabsd 13302 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( B  -  z
)  <_  ( abs `  ( B  -  z
) ) )
270201, 85syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  B  e.  CC )
271242recnd 9572 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  z  e.  CC )
272270, 271abssubd 13340 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( abs `  ( B  -  z )
)  =  ( abs `  ( z  -  B
) ) )
273269, 272breqtrd 4418 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( B  -  z
)  <_  ( abs `  ( z  -  B
) ) )
274199simprd 461 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( abs `  (
z  -  B ) )  <  ( 1  /  j ) )
275265, 268, 264, 273, 274lelttrd 9694 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( B  -  z
)  <  ( 1  /  j ) )
276247, 242, 264, 275ltsub23d 10117 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( B  -  (
1  /  j ) )  <  z )
277201, 28syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  A  e.  RR* )
278 iooltub 36898 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  z  e.  ( A (,) B
) )  ->  z  <  B )
279277, 261, 203, 278syl3anc 1230 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  z  <  B )
280260, 261, 242, 276, 279eliood 36881 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  z  e.  (
( B  -  (
1  /  j ) ) (,) B ) )
281246, 247, 202, 248, 241, 258, 259, 280dvbdfbdioolem1 37075 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( ( abs `  (
( F `  z
)  -  ( F `
 ( B  -  ( 1  /  j
) ) ) ) )  <_  ( Y  x.  ( z  -  ( B  -  ( 1  /  j ) ) ) )  /\  ( abs `  ( ( F `
 z )  -  ( F `  ( B  -  ( 1  / 
j ) ) ) ) )  <_  ( Y  x.  ( B  -  A ) ) ) )
282281simpld 457 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( F `
 ( B  -  ( 1  /  j
) ) ) ) )  <_  ( Y  x.  ( z  -  ( B  -  ( 1  /  j ) ) ) ) )
283201, 216, 57syl2anc 659 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( 1  /  j
)  e.  RR )
284241, 283remulcld 9574 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( Y  x.  (
1  /  j ) )  e.  RR )
285156, 148ffvelrnd 5966 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( RR  _D  F ) `  (
( A  +  B
)  /  2 ) )  e.  RR )
286285recnd 9572 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( RR  _D  F ) `  (
( A  +  B
)  /  2 ) )  e.  CC )
287286abscld 13323 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( abs `  (
( RR  _D  F
) `  ( ( A  +  B )  /  2 ) ) )  e.  RR )
288286absge0d 13331 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  0  <_  ( abs `  ( ( RR  _D  F ) `  (
( A  +  B
)  /  2 ) ) ) )
289 fveq2 5805 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  ( ( A  +  B )  / 
2 )  ->  (
( RR  _D  F
) `  x )  =  ( ( RR 
_D  F ) `  ( ( A  +  B )  /  2
) ) )
290289fveq2d 5809 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  ( ( A  +  B )  / 
2 )  ->  ( abs `  ( ( RR 
_D  F ) `  x ) )  =  ( abs `  (
( RR  _D  F
) `  ( ( A  +  B )  /  2 ) ) ) )
291146eqcomi 2415 . . . . . . . . . . . . . . . . . . . . . . 23  |-  sup ( ran  ( x  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  x )
) ) ,  RR ,  <  )  =  Y
292291a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  ( ( A  +  B )  / 
2 )  ->  sup ( ran  ( x  e.  ( A (,) B
)  |->  ( abs `  (
( RR  _D  F
) `  x )
) ) ,  RR ,  <  )  =  Y )
293290, 292breq12d 4407 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  ( ( A  +  B )  / 
2 )  ->  (
( abs `  (
( RR  _D  F
) `  x )
)  <_  sup ( ran  ( x  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  x )
) ) ,  RR ,  <  )  <->  ( abs `  ( ( RR  _D  F ) `  (
( A  +  B
)  /  2 ) ) )  <_  Y
) )
294293rspcva 3157 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  +  B )  /  2
)  e.  ( A (,) B )  /\  A. x  e.  ( A (,) B ) ( abs `  ( ( RR  _D  F ) `
 x ) )  <_  sup ( ran  (
x  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `
 x ) ) ) ,  RR ,  <  ) )  ->  ( abs `  ( ( RR 
_D  F ) `  ( ( A  +  B )  /  2
) ) )  <_  Y )
295148, 249, 294syl2anc 659 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( abs `  (
( RR  _D  F
) `  ( ( A  +  B )  /  2 ) ) )  <_  Y )
29614, 287, 164, 288, 295letrd 9693 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  0  <_  Y )
297201, 296syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  0  <_  Y )
298283recnd 9572 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( 1  /  j
)  e.  CC )
299 sub31 36832 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( z  e.  CC  /\  B  e.  CC  /\  (
1  /  j )  e.  CC )  -> 
( z  -  ( B  -  ( 1  /  j ) ) )  =  ( ( 1  /  j )  -  ( B  -  z ) ) )
300271, 270, 298, 299syl3anc 1230 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( z  -  ( B  -  ( 1  /  j ) ) )  =  ( ( 1  /  j )  -  ( B  -  z ) ) )
301242, 247posdifd 10099 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( z  <  B  <->  0  <  ( B  -  z ) ) )
302279, 301mpbid 210 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  0  <  ( B  -  z ) )
303265, 302elrpd 11219 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( B  -  z
)  e.  RR+ )
304283, 303ltsubrpd 11250 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( ( 1  / 
j )  -  ( B  -  z )
)  <  ( 1  /  j ) )
305300, 304eqbrtrd 4414 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( z  -  ( B  -  ( 1  /  j ) ) )  <  ( 1  /  j ) )
306244, 283, 305ltled 9685 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( z  -  ( B  -  ( 1  /  j ) ) )  <_  ( 1  /  j ) )
307244, 283, 241, 297, 306lemul2ad 10446 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( Y  x.  (
z  -  ( B  -  ( 1  / 
j ) ) ) )  <_  ( Y  x.  ( 1  /  j
) ) )
308284adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  Y  =  0 )  ->  ( Y  x.  ( 1  /  j ) )  e.  RR )
309236adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  Y  =  0 )  ->  (
x  /  2 )  e.  RR )
310 oveq1 6241 . . . . . . . . . . . . . . . . . . . 20  |-  ( Y  =  0  ->  ( Y  x.  ( 1  /  j ) )  =  ( 0  x.  ( 1  /  j
) ) )
311298mul02d 9732 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( 0  x.  (
1  /  j ) )  =  0 )
312310, 311sylan9eqr 2465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  Y  =  0 )  ->  ( Y  x.  ( 1  /  j ) )  =  0 )
313208rphalfcld 11234 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( x  /  2
)  e.  RR+ )
314313rpgt0d 11225 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  0  <  ( x  /  2 ) )
315314adantr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  Y  =  0 )  ->  0  <  ( x  /  2
) )
316312, 315eqbrtrd 4414 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  Y  =  0 )  ->  ( Y  x.  ( 1  /  j ) )  <  ( x  / 
2 ) )
317308, 309, 316ltled 9685 . . . . . . . . . . . . . . . . 17  |-  ( ( ch  /\  Y  =  0 )  ->  ( Y  x.  ( 1  /  j ) )  <_  ( x  / 
2 ) )
318241adantr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  -.  Y  =  0 )  ->  Y  e.  RR )
319297adantr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  -.  Y  =  0 )  -> 
0  <_  Y )
320 neqne 36791 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  Y  =  0  ->  Y  =/=  0 )
321320adantl 464 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  -.  Y  =  0 )  ->  Y  =/=  0 )
322318, 319, 321ne0gt0d 9674 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  -.  Y  =  0 )  -> 
0  <  Y )
323284adantr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  j ) )  e.  RR )
3243, 211sseldi 3439 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  N  e.  RR )
325 0red 9547 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  0  e.  RR )
326201, 208, 142syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  M  e.  RR )
327201, 65syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  0  <  M )
328201, 208, 187syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  M  <_  N )
329325, 326, 324, 327, 328ltletrd 9696 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  0  <  N )
330329gt0ne0d 10077 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  N  =/=  0
)
331324, 330rereccld 10332 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( 1  /  N
)  e.  RR )
332241, 331remulcld 9574 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( Y  x.  (
1  /  N ) )  e.  RR )
333332adantr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  N ) )  e.  RR )
334236adantr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  0  < 
Y )  ->  (
x  /  2 )  e.  RR )
335283adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  0  < 
Y )  ->  (
1  /  j )  e.  RR )
336331adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  0  < 
Y )  ->  (
1  /  N )  e.  RR )
337241adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  0  < 
Y )  ->  Y  e.  RR )
338297adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  0  < 
Y )  ->  0  <_  Y )
339324, 329elrpd 11219 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  N  e.  RR+ )
340201, 216, 94syl2anc 659 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  j  e.  RR+ )
341 1red 9561 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  1  e.  RR )
34296a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  0  <_  1 )
343215, 189syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  N  <_  j )
344339, 340, 341, 342, 343lediv2ad 11244 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( 1  /  j
)  <_  ( 1  /  N ) )
345344adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  0  < 
Y )  ->  (
1  /  j )  <_  ( 1  /  N ) )
346335, 336, 337, 338, 345lemul2ad 10446 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  j ) )  <_  ( Y  x.  ( 1  /  N
) ) )
347234recnd 9572 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  x  e.  CC )
348 2cnd 10569 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  2  e.  CC )
349208rpne0d 11227 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  x  =/=  0
)
350174a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  2  =/=  0
)
351347, 348, 349, 350divne0d 10297 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ch 
->  ( x  /  2
)  =/=  0 )
352241, 236, 351redivcld 10333 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  ( Y  /  (
x  /  2 ) )  e.  RR )
353352adantr 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( x  / 
2 ) )  e.  RR )
354 simpr 459 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ch  /\  0  < 
Y )  ->  0  <  Y )
355314adantr 463 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ch  /\  0  < 
Y )  ->  0  <  ( x  /  2
) )
356337, 334, 354, 355divgt0d 10441 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  0  < 
Y )  ->  0  <  ( Y  /  (
x  /  2 ) ) )
357353, 356elrpd 11219 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( x  / 
2 ) )  e.  RR+ )
358357rprecred 11233 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  0  < 
Y )  ->  (
1  /  ( Y  /  ( x  / 
2 ) ) )  e.  RR )
359339adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  N  e.  RR+ )
360 1red 9561 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  1  e.  RR )
36196a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  0  <_  1 )
362352flcld 11885 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ch 
->  ( |_ `  ( Y  /  ( x  / 
2 ) ) )  e.  ZZ )
363362peano2zd 10931 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 )  e.  ZZ )
364363zred 10928 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ch 
->  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 )  e.  RR )
365201, 140syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ch 
->  M  e.  ZZ )
366363, 365ifcld 3927 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ch 
->  if ( M  <_ 
( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 ) ,  ( ( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) ,  M )  e.  ZZ )
367145, 366syl5eqel 2494 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  N  e.  ZZ )
368367zred 10928 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ch 
->  N  e.  RR )
369 flltp1 11887 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( Y  /  ( x  /  2 ) )  e.  RR  ->  ( Y  /  ( x  / 
2 ) )  < 
( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 ) )
370352, 369syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ch 
->  ( Y  /  (
x  /  2 ) )  <  ( ( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) )
371201, 60syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ch 
->  M  e.  RR )
372 max2 11359 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( M  e.  RR  /\  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 )  e.  RR )  ->  ( ( |_
`  ( Y  / 
( x  /  2
) ) )  +  1 )  <_  if ( M  <_  ( ( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) ,  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 ) ,  M ) )
373371, 364, 372syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 )  <_  if ( M  <_  ( ( |_
`  ( Y  / 
( x  /  2
) ) )  +  1 ) ,  ( ( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) ,  M ) )
374373, 145syl6breqr 4434 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ch 
->  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 )  <_  N )
375352, 364, 368, 370, 374ltletrd 9696 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  ( Y  /  (
x  /  2 ) )  <  N )
376352, 324, 375ltled 9685 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( Y  /  (
x  /  2 ) )  <_  N )
377376adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( x  / 
2 ) )  <_  N )
378357, 359, 360, 361, 377lediv2ad 11244 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  0  < 
Y )  ->  (
1  /  N )  <_  ( 1  / 
( Y  /  (
x  /  2 ) ) ) )
379336, 358, 337, 338, 378lemul2ad 10446 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  N ) )  <_  ( Y  x.  ( 1  /  ( Y  /  ( x  / 
2 ) ) ) ) )
380337recnd 9572 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  Y  e.  CC )
381353recnd 9572 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( x  / 
2 ) )  e.  CC )
382356gt0ne0d 10077 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( x  / 
2 ) )  =/=  0 )
383380, 381, 382divrecd 10284 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( Y  / 
( x  /  2
) ) )  =  ( Y  x.  (
1  /  ( Y  /  ( x  / 
2 ) ) ) ) )
384334recnd 9572 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  (
x  /  2 )  e.  CC )
385354gt0ne0d 10077 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  Y  =/=  0 )
386351adantr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  (
x  /  2 )  =/=  0 )
387380, 384, 385, 386ddcand 10301 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( Y  / 
( x  /  2
) ) )  =  ( x  /  2
) )
388383, 387eqtr3d 2445 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  ( Y  / 
( x  /  2
) ) ) )  =  ( x  / 
2 ) )
389379, 388breqtrd 4418 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  N ) )  <_  ( x  / 
2 ) )
390323, 333, 334, 346, 389letrd 9693 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  j ) )  <_  ( x  / 
2 ) )
391322, 390syldan 468 . . . . . . . . . . . . . . . . 17  |-  ( ( ch  /\  -.  Y  =  0 )  -> 
( Y  x.  (
1  /  j ) )  <_  ( x  /  2 ) )
392317, 391pm2.61dan 792 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( Y  x.  (
1  /  j ) )  <_  ( x  /  2 ) )
393245, 284, 236, 307, 392letrd 9693 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( Y  x.  (
z  -  ( B  -  ( 1  / 
j ) ) ) )  <_  ( x  /  2 ) )
394240, 245, 236, 282, 393letrd 9693 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( F `
 ( B  -  ( 1  /  j
) ) ) ) )  <_  ( x  /  2 ) )
395239, 394eqbrtrd 4414 . . . . . . . . . . . . 13  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( S `
 j ) ) )  <_  ( x  /  2 ) )
396 simpllr 761 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  /\  ( abs `  ( ( S `  j )  -  ( limsup `
 S ) ) )  <  ( x  /  2 ) )  /\  z  e.  ( A (,) B ) )  /\  ( abs `  ( z  -  B
) )  <  (
1  /  j ) )  ->  ( abs `  ( ( S `  j )  -  ( limsup `
 S ) ) )  <  ( x  /  2 ) )
397199, 396syl 17 . . . . . . . . . . . . 13  |-  ( ch 
->  ( abs `  (
( S `  j
)  -  ( limsup `  S ) ) )  <  ( x  / 
2 ) )
398230, 232, 236, 236, 395, 397leltaddd 10133 . . . . . . . . . . . 12  |-  ( ch 
->  ( ( abs `  (
( F `  z
)  -  ( S `
 j ) ) )  +  ( abs `  ( ( S `  j )  -  ( limsup `
 S ) ) ) )  <  (
( x  /  2
)  +  ( x  /  2 ) ) )
3993472halvesd 10745 . . . . . . . . . . . 12  |-  ( ch 
->  ( ( x  / 
2 )  +  ( x  /  2 ) )  =  x )
400398, 399breqtrd 4418 . . . . . . . . . . 11  |-  ( ch 
->  ( ( abs `  (
( F `  z
)  -  ( S `
 j ) ) )  +  ( abs `  ( ( S `  j )  -  ( limsup `
 S ) ) ) )  <  x
)
401228, 233, 234, 235, 400lelttrd 9694 . . . . . . . . . 10  |-  ( ch 
->  ( abs `  (
( ( F `  z )  -  ( S `  j )
)  +  ( ( S `  j )  -  ( limsup `  S
) ) ) )  <  x )
402222, 401eqbrtrd 4414 . . . . . . . . 9  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( limsup `  S ) ) )  <  x )
403198, 402sylbir 213 . . . . . . . 8  |-  ( ( ( ( ( (
ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  /\  ( abs `  ( ( S `  j )  -  ( limsup `
 S ) ) )  <  ( x  /  2 ) )  /\  z  e.  ( A (,) B ) )  /\  ( abs `  ( z  -  B
) )  <  (
1  /  j ) )  ->  ( abs `  ( ( F `  z )  -  ( limsup `
 S ) ) )  <  x )
404403adantrl 714 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  /\  ( abs `  ( ( S `  j )  -  ( limsup `
 S ) ) )  <  ( x  /  2 ) )  /\  z  e.  ( A (,) B ) )  /\  ( z  =/=  B  /\  ( abs `  ( z  -  B ) )  < 
( 1  /  j
) ) )  -> 
( abs `  (
( F `  z
)  -  ( limsup `  S ) ) )  <  x )
405404ex 432 . . . . . 6  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>=
`  N ) )  /\  ( abs `  (
( S `  j
)  -  ( limsup `  S ) ) )  <  ( x  / 
2 ) )  /\  z  e.  ( A (,) B ) )  -> 
( ( z  =/= 
B  /\  ( abs `  ( z  -  B
) )  <  (
1  /  j ) )  ->  ( abs `  ( ( F `  z )  -  ( limsup `
 S ) ) )  <  x ) )
406405ralrimiva 2817 . . . . 5  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N ) )  /\  ( abs `  ( ( S `  j )  -  ( limsup `  S
) ) )  < 
( x  /  2
) )  ->  A. z  e.  ( A (,) B
) ( ( z  =/=  B  /\  ( abs `  ( z  -  B ) )  < 
( 1  /  j
) )  ->  ( abs `  ( ( F `
 z )  -  ( limsup `  S )
) )  <  x
) )
407 breq2 4398 . . . . . . . . 9  |-  ( y  =  ( 1  / 
j )  ->  (
( abs `  (
z  -  B ) )  <  y  <->  ( abs `  ( z  -  B
) )  <  (
1  /  j ) ) )
408407anbi2d 702 . . . . . . . 8  |-  ( y  =  ( 1  / 
j )  ->  (
( z  =/=  B  /\  ( abs `  (
z  -  B ) )  <  y )  <-> 
( z  =/=  B  /\  ( abs `  (
z  -  B ) )  <  ( 1  /  j ) ) ) )
409408imbi1d 315 . . . . . . 7  |-  ( y  =  ( 1  / 
j )  ->  (
( ( z  =/= 
B  /\  ( abs `  ( z  -  B
) )  <  y
)  ->  ( abs `  ( ( F `  z )  -  ( limsup `
 S ) ) )  <  x )  <-> 
( ( z  =/= 
B  /\  ( abs `  ( z  -  B
) )  <  (
1  /  j ) )  ->  ( abs `  ( ( F `  z )  -  ( limsup `
 S ) ) )  <  x ) ) )
410409ralbidv 2842 . . . . . 6  |-  ( y  =  ( 1  / 
j )  ->  ( A. z  e.  ( A (,) B ) ( ( z  =/=  B  /\  ( abs `  (
z  -  B ) )  <  y )  ->  ( abs `  (
( F `  z
)  -  ( limsup `  S ) ) )  <  x )  <->  A. z  e.  ( A (,) B
) ( ( z  =/=  B  /\  ( abs `  ( z  -  B ) )  < 
( 1  /  j
) )  ->  ( abs `  ( ( F `
 z )  -  ( limsup `  S )
) )  <  x
) ) )
411410rspcev 3159 . . . . 5  |-  ( ( ( 1  /  j
)  e.  RR+  /\  A. z  e.  ( A (,) B ) ( ( z  =/=  B  /\  ( abs `  ( z  -  B ) )  <  ( 1  / 
j ) )  -> 
( abs `  (
( F `  z
)  -  ( limsup `  S ) ) )  <  x ) )  ->  E. y  e.  RR+  A. z  e.  ( A (,) B ) ( ( z  =/=  B  /\  ( abs `  (
z  -  B ) )  <  y )  ->  ( abs `  (
( F `  z
)  -  ( limsup `  S ) ) )  <  x ) )
412197, 406, 411syl2anc 659 . . . 4  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N ) )  /\  ( abs `  ( ( S `  j )  -  ( limsup `  S
) ) )  < 
( x  /  2
) )  ->  E. y  e.  RR+  A. z  e.  ( A (,) B
) ( ( z  =/=  B  /\  ( abs `  ( z  -  B ) )  < 
y )  ->  ( abs `  ( ( F `
 z )  -  ( limsup `  S )
) )  <  x
) )
413 simpr 459 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  <_  N )  ->  b  <_  N )
414413iftrued 3892 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  <_  N )  ->  if ( b  <_  N ,  N ,  b )  =  N )
415 uzid 11059 . . . . . . . . . . . 12  |-  ( N  e.  ZZ  ->  N  e.  ( ZZ>= `  N )
)
416181, 415syl 17 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  N  e.  ( ZZ>= `  N )
)
417416adantr 463 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  <_  N )  ->  N  e.  ( ZZ>= `  N )
)
418414, 417eqeltrd 2490 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  <_  N )  ->  if ( b  <_  N ,  N ,  b )  e.  ( ZZ>= `  N
) )
419418adantlr 713 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  b  <_  N )  ->  if ( b  <_  N ,  N ,  b )  e.  ( ZZ>= `  N )
)
420 iffalse 3893 . . . . . . . . . 10  |-  ( -.  b  <_  N  ->  if ( b  <_  N ,  N ,  b )  =  b )
421420adantl 464 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  if (
b  <_  N ,  N ,  b )  =  b )
422181ad2antrr 724 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  N  e.  ZZ )
423 simplr 754 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  b  e.  ZZ )
424422zred 10928 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  N  e.  RR )
425423zred 10928 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  b  e.  RR )
426 simpr 459 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  -.  b  <_  N )
427424, 425ltnled 9684 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  ( N  <  b  <->  -.  b  <_  N ) )
428426, 427mpbird 232 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  N  <  b )
429424, 425, 428ltled 9685 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  N  <_  b )
430 eluz2 11051 . . . . . . . . . 10  |-  ( b  e.  ( ZZ>= `  N
)  <->  ( N  e.  ZZ  /\  b  e.  ZZ  /\  N  <_ 
b ) )
431422, 423, 429, 430syl3anbrc 1181 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  b  e.  ( ZZ>= `  N )
)
432421, 431eqeltrd 2490 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  if (
b  <_  N ,  N ,  b )  e.  ( ZZ>= `  N )
)
433419, 432pm2.61dan 792 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  ->  if ( b  <_  N ,  N ,  b )  e.  ( ZZ>= `  N
) )
434433adantr 463 . . . . . 6  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  A. c  e.  (
ZZ>= `  b ) ( ( S `  c
)  e.  CC  /\  ( abs `  ( ( S `  c )  -  ( limsup `  S
) ) )  < 
( x  /  2
) ) )  ->  if ( b  <_  N ,  N ,  b )  e.  ( ZZ>= `  N
) )
435 simpr 459 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  A. c  e.  (
ZZ>= `  b ) ( ( S `  c
)  e.  CC  /\  ( abs `  ( ( S `  c )  -  ( limsup `  S
) ) )  < 
( x  /  2
) ) )  ->  A. c  e.  ( ZZ>=
`  b ) ( ( S `  c
)  e.  CC  /\  ( abs `  ( ( S `  c )  -  ( limsup `  S
) ) )  < 
( x  /  2
) ) )
436 simpr 459 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  ->  b  e.  ZZ )
437181adantr 463 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  ->  N  e.  ZZ )
438437, 436ifcld 3927 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  ->  if ( b  <_  N ,  N ,  b )  e.  ZZ )
439436zred 10928 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  ->  b  e.  RR )
440437zred 10928 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  ->  N  e.  RR )
441 max1 11357 . . . . . . . . . . 11  |-  ( ( b  e.  RR  /\  N  e.  RR )  ->  b  <_  if (
b  <_  N ,  N ,  b )
)
442439, 440, 441syl2anc 659 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  ->  b  <_  if ( b  <_  N ,  N , 
b ) )
443 eluz2 11051 . . . . . . . . . 10  |-  ( if ( b  <_  N ,  N ,  b )  e.  ( ZZ>= `  b
)  <->  ( b  e.  ZZ  /\  if ( b  <_  N ,  N ,  b )  e.  ZZ  /\  b  <_  if ( b  <_  N ,  N ,  b ) ) )
444436, 438, 442, 443syl3anbrc 1181 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  ->  if ( b  <_  N ,  N ,  b )  e.  ( ZZ>= `  b
) )
445444adantr 463 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  A. c  e.  (
ZZ>= `  b ) ( ( S `  c
)  e.  CC  /\  ( abs `  ( ( S `  c )  -  ( limsup `  S
) ) )  < 
( x  /  2
) ) )  ->  if ( b  <_  N ,  N ,  b )  e.  ( ZZ>= `  b
) )
446 fveq2 5805 . . . . . . . . . . 11  |-  ( c  =  if ( b  <_  N ,  N ,  b )  -> 
( S `  c
)  =  ( S `
 if ( b  <_  N ,  N ,  b ) ) )
447446eleq1d 2471 . . . . . . . . . 10  |-  ( c  =  if ( b  <_  N ,  N ,  b )  -> 
( ( S `  c )  e.  CC  <->  ( S `  if ( b  <_  N ,  N ,  b )
)  e.  CC ) )
448446oveq1d 6249 . . . . . . . . . . . 12  |-  ( c  =  if ( b  <_  N ,  N ,  b )  -> 
( ( S `  c )  -  ( limsup `
 S ) )  =  ( ( S `
 if ( b  <_  N ,  N ,  b ) )  -  ( limsup `  S
) ) )
449448fveq2d 5809 . . . . . . . . . . 11  |-  ( c  =  if ( b  <_  N ,  N ,  b )  -> 
( abs `  (
( S `  c
)  -  ( limsup `  S ) ) )  =  ( abs `  (
( S `  if ( b  <_  N ,  N ,  b ) )  -  ( limsup `  S ) ) ) )
450449breq1d 4404 . . . . . . . . . 10  |-  ( c  =  if ( b  <_  N ,  N ,  b )  -> 
( ( abs `  (
( S `  c
)  -  ( limsup `  S ) ) )  <  ( x  / 
2 )  <->  ( abs `  ( ( S `  if ( b  <_  N ,  N ,  b ) )  -  ( limsup `  S ) ) )  <  ( x  / 
2 ) ) )
451447, 450anbi12d 709 . . . . . . . . 9  |-  ( c  =  if ( b  <_  N ,  N ,  b )  -> 
( ( ( S `
 c )  e.  CC  /\  ( abs `  ( ( S `  c )  -  ( limsup `
 S ) ) )  <  ( x  /  2 ) )  <-> 
( ( S `  if ( b  <_  N ,  N ,  b ) )  e.  CC  /\  ( abs `  ( ( S `  if ( b  <_  N ,  N ,  b )
)  -  ( limsup `  S ) ) )  <  ( x  / 
2 ) ) ) )
452451rspccva 3158 . . . . . . . 8  |-  ( ( A. c  e.  (
ZZ>= `  b ) ( ( S `  c
)  e.  CC  /\  ( abs `  ( ( S `  c )  -  ( limsup `  S
) ) )  < 
( x  /  2
) )  /\  if ( b  <_  N ,  N ,  b )  e.  ( ZZ>= `  b
) )  ->  (
( S `  if ( b  <_  N ,  N ,  b ) )  e.  CC  /\  ( abs `  ( ( S `  if ( b  <_  N ,  N ,  b )
)  -  ( limsup `  S ) ) )  <  ( x  / 
2 ) ) )
453435, 445, 452syl2anc 659 . . . . . . 7  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  A. c  e.  (
ZZ>= `  b ) ( ( S `  c
)  e.  CC  /\  ( abs `  ( ( S `  c )  -  ( limsup `  S
) ) )  < 
( x  /  2
) ) )  -> 
( ( S `  if ( b  <_  N ,  N ,  b ) )  e.  CC  /\  ( abs `  ( ( S `  if ( b  <_  N ,  N ,  b )
)  -  ( limsup `  S ) ) )  <  ( x  / 
2 ) ) )
454453simprd 461 . . . . . 6  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  A. c  e.  (
ZZ>= `  b ) ( ( S `  c
)  e.  CC  /\  ( abs `  ( ( S `  c )  -  ( limsup `  S
) ) )  < 
( x  /  2
) ) )  -> 
( abs `  (
( S `  if ( b  <_  N ,  N ,  b ) )  -  ( limsup `  S ) ) )  <  ( x  / 
2 ) )
455 fveq2 5805 . . . . . . . . . 10  |-  ( j  =  if ( b  <_  N ,  N ,  b )  -> 
( S `  j
)  =  ( S `
 if ( b  <_  N ,  N ,  b ) ) )
456455oveq1d 6249 . . . . . . . . 9  |-  ( j  =  if ( b  <_  N ,  N ,  b )  -> 
( ( S `  j )  -  ( limsup `
 S ) )  =  ( ( S `
 if ( b  <_  N ,  N ,  b ) )  -  ( limsup `  S
) ) )
457456fveq2d 5809 . . . . . . . 8  |-  ( j  =  if ( b  <_  N ,  N ,  b )  -> 
( abs `  (
( S `  j
)  -  ( limsup `  S ) ) )  =  ( abs `  (
( S `  if ( b  <_  N ,  N ,  b ) )  -  ( limsup `  S ) ) ) )
458457breq1d 4404 . . . . . . 7  |-  ( j  =  if ( b  <_  N ,  N ,  b )  -> 
( ( abs `  (
( S `  j
)  -  ( limsup `  S ) ) )  <  ( x  / 
2 )  <->  ( abs `  ( ( S `  if ( b  <_  N ,  N ,  b ) )  -  ( limsup `  S ) ) )  <  ( x  / 
2 ) ) )
459458rspcev 3159 . . . . . 6  |-  ( ( if ( b  <_  N ,  N , 
b )  e.  (
ZZ>= `  N )  /\  ( abs `  ( ( S `  if ( b  <_  N ,  N ,  b )
)  -  ( limsup `  S ) ) )  <  ( x  / 
2 ) )  ->  E. j  e.  ( ZZ>=
`  N ) ( abs `  ( ( S `  j )  -  ( limsup `  S
) ) )  < 
( x  /  2
) )
460434, 454, 459syl2anc 659 . . . . 5  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  A. c  e.  (
ZZ>= `  b ) ( ( S `  c
)  e.  CC  /\  ( abs `  ( ( S `  c )  -  ( limsup `  S
) ) )  < 
( x  /  2
) ) )  ->  E. j  e.  ( ZZ>=
`  N ) ( abs `  ( ( S `  j )  -  ( limsup `  S
) ) )  < 
( x  /  2
) )
461 ax-resscn 9499 . . . . . . . . . . . . . 14  |-  RR  C_  CC
462461a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  RR  C_  CC )
46326, 462fssd 5679 . . . . . . . . . . . . . 14  |-  ( ph  ->  F : ( A (,) B ) --> CC )
464 dvcn 22508 . . . . . . . . . . . . . 14  |-  ( ( ( RR  C_  CC  /\  F : ( A (,) B ) --> CC 
/\  ( A (,) B )  C_  RR )  /\  dom  ( RR 
_D  F )  =  ( A (,) B
) )  ->  F  e.  ( ( A (,) B ) -cn-> CC ) )
465462, 463, 152, 107, 464syl31anc 1233 . . . . . . . . . . . . 13  |-  ( ph  ->  F  e.  ( ( A (,) B )
-cn-> CC ) )
466 cncffvrn 21586 . . . . . . . . . . . . 13  |-  ( ( RR  C_  CC  /\  F  e.  ( ( A (,) B ) -cn-> CC ) )  ->  ( F  e.  ( ( A (,) B ) -cn-> RR )  <-> 
F : ( A (,) B ) --> RR ) )
467462, 465, 466syl2anc 659 . . . . . . . . . . . 12  |-  ( ph  ->  ( F  e.  ( ( A (,) B
) -cn-> RR )  <->  F :
( A (,) B
) --> RR ) )
46826, 467mpbird 232 . . . . . . . . . . 11  |-  ( ph  ->  F  e.  ( ( A (,) B )
-cn-> RR ) )
469 ioodvbdlimc2lem.r . . . . . . . . . . . 12  |-  R  =  ( j  e.  (
ZZ>= `  M )  |->  ( B  -  ( 1  /  j ) ) )
470103, 469fmptd 5989 . . . . . . . . . . 11  |-  ( ph  ->  R : ( ZZ>= `  M ) --> ( A (,) B ) )
471 eqid 2402 . . . . . . . . . . 11  |-  ( j  e.  ( ZZ>= `  M
)  |->  ( F `  ( R `  j ) ) )  =  ( j  e.  ( ZZ>= `  M )  |->  ( F `
 ( R `  j ) ) )
472 climrel 13371 . . . . . . . . . . . . 13  |-  Rel  ~~>
473472a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  Rel  ~~>  )
474 fvex 5815 . . . . . . . . . . . . . . . . 17  |-  ( ZZ>= `  M )  e.  _V
475474mptex 6080 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( ZZ>= `  M
)  |->  B )  e. 
_V
476475a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( j  e.  (
ZZ>= `  M )  |->  B )  e.  _V )
477 eqidd 2403 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( ZZ>= `  M )
)  ->  ( j  e.  ( ZZ>= `  M )  |->  B )  =  ( j  e.  ( ZZ>= `  M )  |->  B ) )
478 eqidd 2403 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  M )
)  /\  j  =  m )  ->  B  =  B )
479 simpr 459 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( ZZ>= `  M )
)  ->  m  e.  ( ZZ>= `  M )
)
4806adantr 463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( ZZ>= `  M )
)  ->  B  e.  RR )
481477, 478, 479, 480fvmptd 5894 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( ZZ>= `  M )
)  ->  ( (
j  e.  ( ZZ>= `  M )  |->  B ) `
 m )  =  B )
48223, 22, 476, 85, 481climconst 13422 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( j  e.  (
ZZ>= `  M )  |->  B )  ~~>  B )
483474mptex 6080 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( ZZ>= `  M
)  |->  ( B  -  ( 1  /  j
) ) )  e. 
_V
484469, 483eqeltri 2486 . . . . . . . . . . . . . . 15  |-  R  e. 
_V
485484a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  R  e.  _V )
486 1cnd 9562 . . . . . . . . . . . . . . 15  |-  ( ph  ->  1  e.  CC )
487 elnnnn0b 10801 . . . . . . . . . . . . . . . 16  |-  ( M  e.  NN  <->  ( M  e.  NN0  /\  0  < 
M ) )
48821, 65, 487sylanbrc 662 . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  e.  NN )
489 divcnvg 36983 . . . . . . . . . . . . . . 15  |-  ( ( 1  e.  CC  /\  M  e.  NN )  ->  ( j  e.  (
ZZ>= `  M )  |->  ( 1  /  j ) )  ~~>  0 )
490486, 488, 489syl2anc 659 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( j  e.  (
ZZ>= `  M )  |->  ( 1  /  j ) )  ~~>  0 )
491 eqidd 2403 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( j  e.  ( ZZ>= `  M )  |->  B )  =  ( j  e.  ( ZZ>= `  M )  |->  B ) )
492 eqidd 2403 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( ZZ>= `  M )
)  /\  j  =  i )  ->  B  =  B )
493 simpr 459 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  e.  ( ZZ>= `  M )
)
4946adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  B  e.  RR )
495491, 492, 493, 494fvmptd 5894 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( (
j  e.  ( ZZ>= `  M )  |->  B ) `
 i )  =  B )
496495, 494eqeltrd 2490 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( (
j  e.  ( ZZ>= `  M )  |->  B ) `
 i )  e.  RR )
497496recnd 9572 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( (
j  e.  ( ZZ>= `  M )  |->  B ) `
 i )  e.  CC )
498 eqidd 2403 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( j  e.  ( ZZ>= `  M )  |->  ( 1  /  j
) )  =  ( j  e.  ( ZZ>= `  M )  |->  ( 1  /  j ) ) )
499 oveq2 6242 . . . . . . . . . . . . . . . . 17  |-  ( j  =  i  ->  (
1  /  j )  =  ( 1  / 
i ) )
500499adantl 464 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( ZZ>= `  M )
)  /\  j  =  i )  ->  (
1  /  j )  =  ( 1  / 
i ) )
5013, 493sseldi 3439 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  e.  RR )
502 0red 9547 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  0  e.  RR )
50360adantr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  M  e.  RR )
50465adantr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  0  <  M )
505 eluzle 11057 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( ZZ>= `  M
)  ->  M  <_  i )
506505adantl 464 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  M  <_  i )
507502, 503, 501, 504, 506ltletrd 9696 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  0  <  i )
508507gt0ne0d 10077 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  =/=  0 )
509501, 508rereccld 10332 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( 1  /  i )  e.  RR )
510498, 500, 493, 509fvmptd 5894 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( (
j  e.  ( ZZ>= `  M )  |->  ( 1  /  j ) ) `
 i )  =  ( 1  /  i
) )
511501recnd 9572 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  e.  CC )
512511, 508reccld 10274 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( 1  /  i )  e.  CC )
513510, 512eqeltrd 2490 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( (
j  e.  ( ZZ>= `  M )  |->  ( 1  /  j ) ) `
 i )  e.  CC )
514499oveq2d 6250 . . . . . . . . . . . . . . . . 17  |-  ( j  =  i  ->  ( B  -  ( 1  /  j ) )  =  ( B  -  ( 1  /  i
) ) )
515 ovex 6262 . . . . . . . . . . . . . . . . 17  |-  ( B  -  ( 1  / 
i ) )  e. 
_V
516514, 469, 515fvmpt 5888 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( ZZ>= `  M
)  ->  ( R `  i )  =  ( B  -  ( 1  /  i ) ) )
517516adantl 464 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( R `  i )  =  ( B  -  ( 1  /  i ) ) )
518495, 510oveq12d 6252 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( (
( j  e.  (
ZZ>= `  M )  |->  B ) `  i )  -  ( ( j  e.  ( ZZ>= `  M
)  |->  ( 1  / 
j ) ) `  i ) )  =  ( B  -  (
1  /  i ) ) )
519517, 518eqtr4d 2446 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( R `  i )  =  ( ( ( j  e.  ( ZZ>= `  M )  |->  B ) `  i
)  -  ( ( j  e.  ( ZZ>= `  M )  |->  ( 1  /  j ) ) `
 i ) ) )
52023, 22, 482, 485, 490, 497, 513, 519climsub 13512 . . . . . . . . . . . . 13  |-  ( ph  ->  R  ~~>  ( B  - 
0 ) )
52185subid1d 9876 . . . . . . . . . . . . 13  |-  ( ph  ->  ( B  -  0 )  =  B )
522520, 521breqtrd