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

Theorem ioodvbdlimc2lem 37672
Description: Limit at the upper bound of an open interval, for a function with bounded derivative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 3-Oct-2020.)
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 11180 . . . . . 6  |-  ( ZZ>= `  M )  C_  ZZ
2 zssre 10946 . . . . . 6  |-  ZZ  C_  RR
31, 2sstri 3474 . . . . 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 10049 . . . . . . . . . 10  |-  ( ph  ->  ( B  -  A
)  e.  RR )
9 ioodvbdlimc2lem.altb . . . . . . . . . . . 12  |-  ( ph  ->  A  <  B )
107, 6posdifd 10202 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  <  B  <->  0  <  ( B  -  A ) ) )
119, 10mpbid 214 . . . . . . . . . . 11  |-  ( ph  ->  0  <  ( B  -  A ) )
1211gt0ne0d 10180 . . . . . . . . . 10  |-  ( ph  ->  ( B  -  A
)  =/=  0 )
138, 12rereccld 10436 . . . . . . . . 9  |-  ( ph  ->  ( 1  /  ( B  -  A )
)  e.  RR )
14 0red 9646 . . . . . . . . . 10  |-  ( ph  ->  0  e.  RR )
158, 11recgt0d 10543 . . . . . . . . . 10  |-  ( ph  ->  0  <  ( 1  /  ( B  -  A ) ) )
1614, 13, 15ltled 9785 . . . . . . . . 9  |-  ( ph  ->  0  <_  ( 1  /  ( B  -  A ) ) )
17 flge0nn0 12055 . . . . . . . . 9  |-  ( ( ( 1  /  ( B  -  A )
)  e.  RR  /\  0  <_  ( 1  / 
( B  -  A
) ) )  -> 
( |_ `  (
1  /  ( B  -  A ) ) )  e.  NN0 )
1813, 16, 17syl2anc 666 . . . . . . . 8  |-  ( ph  ->  ( |_ `  (
1  /  ( B  -  A ) ) )  e.  NN0 )
19 peano2nn0 10912 . . . . . . . 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 2515 . . . . . 6  |-  ( ph  ->  M  e.  NN0 )
2221nn0zd 11040 . . . . 5  |-  ( ph  ->  M  e.  ZZ )
23 eqid 2423 . . . . . 6  |-  ( ZZ>= `  M )  =  (
ZZ>= `  M )
2423uzsup 12091 . . . . 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 467 . . . . . 6  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  F :
( A (,) B
) --> RR )
287rexrd 9692 . . . . . . . 8  |-  ( ph  ->  A  e.  RR* )
2928adantr 467 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  A  e.  RR* )
306rexrd 9692 . . . . . . . 8  |-  ( ph  ->  B  e.  RR* )
3130adantr 467 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  B  e.  RR* )
326adantr 467 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  B  e.  RR )
33 eluzelre 11171 . . . . . . . . . 10  |-  ( j  e.  ( ZZ>= `  M
)  ->  j  e.  RR )
3433adantl 468 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  j  e.  RR )
35 0red 9646 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  0  e.  RR )
36 0red 9646 . . . . . . . . . . . . 13  |-  ( j  e.  ( ZZ>= `  M
)  ->  0  e.  RR )
37 1red 9660 . . . . . . . . . . . . 13  |-  ( j  e.  ( ZZ>= `  M
)  ->  1  e.  RR )
3836, 37readdcld 9672 . . . . . . . . . . . 12  |-  ( j  e.  ( ZZ>= `  M
)  ->  ( 0  +  1 )  e.  RR )
3938adantl 468 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( 0  +  1 )  e.  RR )
4036ltp1d 10539 . . . . . . . . . . . 12  |-  ( j  e.  ( ZZ>= `  M
)  ->  0  <  ( 0  +  1 ) )
4140adantl 468 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  0  <  ( 0  +  1 ) )
42 eluzel2 11166 . . . . . . . . . . . . . 14  |-  ( j  e.  ( ZZ>= `  M
)  ->  M  e.  ZZ )
4342zred 11042 . . . . . . . . . . . . 13  |-  ( j  e.  ( ZZ>= `  M
)  ->  M  e.  RR )
4443adantl 468 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  M  e.  RR )
4513flcld 12035 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( |_ `  (
1  /  ( B  -  A ) ) )  e.  ZZ )
4645zred 11042 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( |_ `  (
1  /  ( B  -  A ) ) )  e.  RR )
47 1red 9660 . . . . . . . . . . . . . . 15  |-  ( ph  ->  1  e.  RR )
4818nn0ge0d 10930 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  <_  ( |_ `  ( 1  /  ( B  -  A )
) ) )
4914, 46, 47, 48leadd1dd 10229 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0  +  1 )  <_  ( ( |_ `  ( 1  / 
( B  -  A
) ) )  +  1 ) )
5049, 5syl6breqr 4462 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 0  +  1 )  <_  M )
5150adantr 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( 0  +  1 )  <_  M )
52 eluzle 11173 . . . . . . . . . . . . 13  |-  ( j  e.  ( ZZ>= `  M
)  ->  M  <_  j )
5352adantl 468 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  M  <_  j )
5439, 44, 34, 51, 53letrd 9794 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( 0  +  1 )  <_ 
j )
5535, 39, 34, 41, 54ltletrd 9797 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  0  <  j )
5655gt0ne0d 10180 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  j  =/=  0 )
5734, 56rereccld 10436 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( 1  /  j )  e.  RR )
5832, 57resubcld 10049 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( B  -  ( 1  / 
j ) )  e.  RR )
597adantr 467 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  A  e.  RR )
6021nn0red 10928 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  RR )
6114, 47readdcld 9672 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0  +  1 )  e.  RR )
6246, 47readdcld 9672 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( |_ `  ( 1  /  ( B  -  A )
) )  +  1 )  e.  RR )
6314ltp1d 10539 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <  ( 0  +  1 ) )
6414, 61, 62, 63, 49ltletrd 9797 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <  ( ( |_ `  ( 1  /  ( B  -  A ) ) )  +  1 ) )
6564, 5syl6breqr 4462 . . . . . . . . . . . 12  |-  ( ph  ->  0  <  M )
6665gt0ne0d 10180 . . . . . . . . . . 11  |-  ( ph  ->  M  =/=  0 )
6760, 66rereccld 10436 . . . . . . . . . 10  |-  ( ph  ->  ( 1  /  M
)  e.  RR )
6867adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( 1  /  M )  e.  RR )
6932, 68resubcld 10049 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( B  -  ( 1  /  M ) )  e.  RR )
705eqcomi 2436 . . . . . . . . . . . . 13  |-  ( ( |_ `  ( 1  /  ( B  -  A ) ) )  +  1 )  =  M
7170oveq2i 6314 . . . . . . . . . . . 12  |-  ( 1  /  ( ( |_
`  ( 1  / 
( B  -  A
) ) )  +  1 ) )  =  ( 1  /  M
)
7271, 67syl5eqel 2515 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  /  (
( |_ `  (
1  /  ( B  -  A ) ) )  +  1 ) )  e.  RR )
7313, 15elrpd 11340 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1  /  ( B  -  A )
)  e.  RR+ )
7462, 64elrpd 11340 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( |_ `  ( 1  /  ( B  -  A )
) )  +  1 )  e.  RR+ )
75 1rp 11308 . . . . . . . . . . . . . 14  |-  1  e.  RR+
7675a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  1  e.  RR+ )
77 fllelt 12034 . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1  /  ( B  -  A )
)  <  ( ( |_ `  ( 1  / 
( B  -  A
) ) )  +  1 ) )
8073, 74, 76, 79ltdiv2dd 37395 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  /  (
( |_ `  (
1  /  ( B  -  A ) ) )  +  1 ) )  <  ( 1  /  ( 1  / 
( B  -  A
) ) ) )
818recnd 9671 . . . . . . . . . . . . 13  |-  ( ph  ->  ( B  -  A
)  e.  CC )
8281, 12recrecd 10382 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  /  (
1  /  ( B  -  A ) ) )  =  ( B  -  A ) )
8380, 82breqtrd 4446 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  /  (
( |_ `  (
1  /  ( B  -  A ) ) )  +  1 ) )  <  ( B  -  A ) )
8472, 8, 6, 83ltsub2dd 10228 . . . . . . . . . 10  |-  ( ph  ->  ( B  -  ( B  -  A )
)  <  ( B  -  ( 1  / 
( ( |_ `  ( 1  /  ( B  -  A )
) )  +  1 ) ) ) )
856recnd 9671 . . . . . . . . . . 11  |-  ( ph  ->  B  e.  CC )
867recnd 9671 . . . . . . . . . . 11  |-  ( ph  ->  A  e.  CC )
8785, 86nncand 9993 . . . . . . . . . 10  |-  ( ph  ->  ( B  -  ( B  -  A )
)  =  A )
8871oveq2i 6314 . . . . . . . . . . 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 4451 . . . . . . . . 9  |-  ( ph  ->  A  <  ( B  -  ( 1  /  M ) ) )
9190adantr 467 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  A  <  ( B  -  ( 1  /  M ) ) )
9260, 65elrpd 11340 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  RR+ )
9392adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  M  e.  RR+ )
9434, 55elrpd 11340 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  j  e.  RR+ )
95 1red 9660 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  1  e.  RR )
96 0le1 10139 . . . . . . . . . . 11  |-  0  <_  1
9796a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  0  <_  1 )
9893, 94, 95, 97, 53lediv2ad 11365 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( 1  /  j )  <_ 
( 1  /  M
) )
9957, 68, 32, 98lesub2dd 10232 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( B  -  ( 1  /  M ) )  <_ 
( B  -  (
1  /  j ) ) )
10059, 69, 58, 91, 99ltletrd 9797 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  A  <  ( B  -  ( 1  /  j ) ) )
10194rpreccld 11353 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( 1  /  j )  e.  RR+ )
10232, 101ltsubrpd 11372 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( B  -  ( 1  / 
j ) )  < 
B )
10329, 31, 58, 100, 102eliood 37470 . . . . . 6  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( B  -  ( 1  / 
j ) )  e.  ( A (,) B
) )
10427, 103ffvelrnd 6036 . . . . 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 6059 . . . 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 37666 . . . . 5  |-  ( ph  ->  E. b  e.  RR  A. x  e.  ( A (,) B ) ( abs `  ( F `
 x ) )  <_  b )
11060adantr 467 . . . . . . . 8  |-  ( (
ph  /\  A. x  e.  ( A (,) B
) ( abs `  ( F `  x )
)  <_  b )  ->  M  e.  RR )
111 simpr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  j  e.  ( ZZ>= `  M )
)
112105fvmpt2 5971 . . . . . . . . . . . . . 14  |-  ( ( j  e.  ( ZZ>= `  M )  /\  ( F `  ( B  -  ( 1  / 
j ) ) )  e.  RR )  -> 
( S `  j
)  =  ( F `
 ( B  -  ( 1  /  j
) ) ) )
113111, 104, 112syl2anc 666 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( S `  j )  =  ( F `  ( B  -  ( 1  / 
j ) ) ) )
114113fveq2d 5883 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( abs `  ( S `  j
) )  =  ( abs `  ( F `
 ( B  -  ( 1  /  j
) ) ) ) )
115114adantlr 720 . . . . . . . . . . 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 761 . . . . . . . . . . . 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 720 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  A. x  e.  ( A (,) B ) ( abs `  ( F `  x
) )  <_  b
)  /\  j  e.  ( ZZ>= `  M )
)  ->  ( B  -  ( 1  / 
j ) )  e.  ( A (,) B
) )
118 fveq2 5879 . . . . . . . . . . . . . . 15  |-  ( x  =  ( B  -  ( 1  /  j
) )  ->  ( F `  x )  =  ( F `  ( B  -  (
1  /  j ) ) ) )
119118fveq2d 5883 . . . . . . . . . . . . . 14  |-  ( x  =  ( B  -  ( 1  /  j
) )  ->  ( abs `  ( F `  x ) )  =  ( abs `  ( F `  ( B  -  ( 1  / 
j ) ) ) ) )
120119breq1d 4431 . . . . . . . . . . . . 13  |-  ( x  =  ( B  -  ( 1  /  j
) )  ->  (
( abs `  ( F `  x )
)  <_  b  <->  ( abs `  ( F `  ( B  -  ( 1  /  j ) ) ) )  <_  b
) )
121120rspccva 3182 . . . . . . . . . . . 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 666 . . . . . . . . . . 11  |-  ( ( ( ph  /\  A. x  e.  ( A (,) B ) ( abs `  ( F `  x
) )  <_  b
)  /\  j  e.  ( ZZ>= `  M )
)  ->  ( abs `  ( F `  ( B  -  ( 1  /  j ) ) ) )  <_  b
)
123115, 122eqbrtrd 4442 . . . . . . . . . 10  |-  ( ( ( ph  /\  A. x  e.  ( A (,) B ) ( abs `  ( F `  x
) )  <_  b
)  /\  j  e.  ( ZZ>= `  M )
)  ->  ( abs `  ( S `  j
) )  <_  b
)
124123a1d 27 . . . . . . . . 9  |-  ( ( ( ph  /\  A. x  e.  ( A (,) B ) ( abs `  ( F `  x
) )  <_  b
)  /\  j  e.  ( ZZ>= `  M )
)  ->  ( M  <_  j  ->  ( abs `  ( S `  j
) )  <_  b
) )
125124ralrimiva 2840 . . . . . . . 8  |-  ( (
ph  /\  A. x  e.  ( A (,) B
) ( abs `  ( F `  x )
)  <_  b )  ->  A. j  e.  (
ZZ>= `  M ) ( M  <_  j  ->  ( abs `  ( S `
 j ) )  <_  b ) )
126 breq1 4424 . . . . . . . . . . 11  |-  ( k  =  M  ->  (
k  <_  j  <->  M  <_  j ) )
127126imbi1d 319 . . . . . . . . . 10  |-  ( k  =  M  ->  (
( k  <_  j  ->  ( abs `  ( S `  j )
)  <_  b )  <->  ( M  <_  j  ->  ( abs `  ( S `
 j ) )  <_  b ) ) )
128127ralbidv 2865 . . . . . . . . 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 3183 . . . . . . . 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 666 . . . . . . 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 436 . . . . . 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 2900 . . . . 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 37585 . . 3  |-  ( ph  ->  ( limsup `  S )  e.  RR )
135134recnd 9671 . 2  |-  ( ph  ->  ( limsup `  S )  e.  CC )
136 eluzelre 11171 . . . . . . . . 9  |-  ( j  e.  ( ZZ>= `  N
)  ->  j  e.  RR )
137136adantl 468 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  j  e.  RR )
138 0red 9646 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  0  e.  RR )
13945peano2zd 11045 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( |_ `  ( 1  /  ( B  -  A )
) )  +  1 )  e.  ZZ )
1405, 139syl5eqel 2515 . . . . . . . . . . . . 13  |-  ( ph  ->  M  e.  ZZ )
141140adantr 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  M  e.  ZZ )
142141zred 11042 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  M  e.  RR )
143142adantr 467 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  M  e.  RR )
14465ad2antrr 731 . . . . . . . . . 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 37490 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  (
( A  +  B
)  /  2 )  e.  ( A (,) B ) )
1487, 6, 9, 147syl3anc 1265 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( A  +  B )  /  2
)  e.  ( A (,) B ) )
149 ne0i 3768 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( A  +  B
)  /  2 )  e.  ( A (,) B )  ->  ( A (,) B )  =/=  (/) )
150148, 149syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( A (,) B
)  =/=  (/) )
151 ioossre 11698 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( A (,) B )  C_  RR
152151a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( A (,) B
)  C_  RR )
153 dvfre 22897 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( F : ( A (,) B ) --> RR 
/\  ( A (,) B )  C_  RR )  ->  ( RR  _D  F ) : dom  ( RR  _D  F
) --> RR )
15426, 152, 153syl2anc 666 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( RR  _D  F
) : dom  ( RR  _D  F ) --> RR )
155107feq2d 5731 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( RR  _D  F ) : dom  ( RR  _D  F
) --> RR  <->  ( RR  _D  F ) : ( A (,) B ) --> RR ) )
156154, 155mpbid 214 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( RR  _D  F
) : ( A (,) B ) --> RR )
157156ffvelrnda 6035 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( ( RR  _D  F ) `  x )  e.  RR )
158157recnd 9671 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( ( RR  _D  F ) `  x )  e.  CC )
159158abscld 13491 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( abs `  ( ( RR  _D  F ) `  x
) )  e.  RR )
160 eqid 2423 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `  x
) ) )  =  ( x  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  x )
) )
161 eqid 2423 . . . . . . . . . . . . . . . . . . . . . 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 37332 . . . . . . . . . . . . . . . . . . . . 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 461 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  sup ( ran  (
x  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `
 x ) ) ) ,  RR ,  <  )  e.  RR )
164146, 163syl5eqel 2515 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  Y  e.  RR )
165164adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR+ )  ->  Y  e.  RR )
166 rpre 11310 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR+  ->  x  e.  RR )
167166rehalfcld 10861 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  RR+  ->  ( x  /  2 )  e.  RR )
168167adantl 468 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( x  /  2 )  e.  RR )
169166recnd 9671 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR+  ->  x  e.  CC )
170169adantl 468 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  e.  CC )
171 2cnd 10684 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR+ )  ->  2  e.  CC )
172 rpne0 11319 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR+  ->  x  =/=  0 )
173172adantl 468 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  =/=  0 )
174 2ne0 10704 . . . . . . . . . . . . . . . . . . . 20  |-  2  =/=  0
175174a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR+ )  ->  2  =/=  0 )
176170, 171, 173, 175divne0d 10401 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( x  /  2 )  =/=  0 )
177165, 168, 176redivcld 10437 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( Y  /  ( x  / 
2 ) )  e.  RR )
178177flcld 12035 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( |_ `  ( Y  /  (
x  /  2 ) ) )  e.  ZZ )
179178peano2zd 11045 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( |_ `  ( Y  / 
( x  /  2
) ) )  +  1 )  e.  ZZ )
180179, 141ifcld 3953 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  if ( M  <_  ( ( |_
`  ( Y  / 
( x  /  2
) ) )  +  1 ) ,  ( ( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) ,  M )  e.  ZZ )
181145, 180syl5eqel 2515 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  N  e.  ZZ )
182181zred 11042 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  N  e.  RR )
183182adantr 467 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  N  e.  RR )
184179zred 11042 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( |_ `  ( Y  / 
( x  /  2
) ) )  +  1 )  e.  RR )
185 max1 11482 . . . . . . . . . . . . . 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 666 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  M  <_  if ( M  <_  (
( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) ,  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 ) ,  M ) )
187186, 145syl6breqr 4462 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  M  <_  N )
188187adantr 467 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  M  <_  N )
189 eluzle 11173 . . . . . . . . . . . 12  |-  ( j  e.  ( ZZ>= `  N
)  ->  N  <_  j )
190189adantl 468 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  N  <_  j )
191143, 183, 137, 188, 190letrd 9794 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  M  <_  j )
192138, 143, 137, 144, 191ltletrd 9797 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  0  <  j )
193192gt0ne0d 10180 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  j  =/=  0 )
194137, 193rereccld 10436 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  ( 1  /  j )  e.  RR )
195137, 192recgt0d 10543 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  0  <  ( 1  /  j ) )
196194, 195elrpd 11340 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  ( 1  /  j )  e.  RR+ )
197196adantr 467 . . . . 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 198 . . . . . . . . . . . . . . . . 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 777 . . . . . . . . . . . . . . . . 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 762 . . . . . . . . . . . . . . 15  |-  ( ch 
->  z  e.  ( A (,) B ) )
204202, 203ffvelrnd 6036 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( F `  z
)  e.  RR )
205204recnd 9671 . . . . . . . . . . . . 13  |-  ( ch 
->  ( F `  z
)  e.  CC )
206201, 106syl 17 . . . . . . . . . . . . . . 15  |-  ( ch 
->  S : ( ZZ>= `  M ) --> RR )
207 simp-5r 778 . . . . . . . . . . . . . . . . . . 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 11167 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  N  e.  ZZ  /\  M  <_  N ) )
210141, 181, 187, 209syl3anbrc 1190 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR+ )  ->  N  e.  ( ZZ>= `  M )
)
211201, 208, 210syl2anc 666 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  N  e.  ( ZZ>=
`  M ) )
212 uzss 11181 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( ZZ>= `  N )  C_  ( ZZ>=
`  M ) )
213211, 212syl 17 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( ZZ>= `  N )  C_  ( ZZ>= `  M )
)
214 simp-4r 776 . . . . . . . . . . . . . . . . 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 3466 . . . . . . . . . . . . . . 15  |-  ( ch 
->  j  e.  ( ZZ>=
`  M ) )
217206, 216ffvelrnd 6036 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( S `  j
)  e.  RR )
218217recnd 9671 . . . . . . . . . . . . 13  |-  ( ch 
->  ( S `  j
)  e.  CC )
219201, 135syl 17 . . . . . . . . . . . . 13  |-  ( ch 
->  ( limsup `  S )  e.  CC )
220205, 218, 219npncand 10012 . . . . . . . . . . . 12  |-  ( ch 
->  ( ( ( F `
 z )  -  ( S `  j ) )  +  ( ( S `  j )  -  ( limsup `  S
) ) )  =  ( ( F `  z )  -  ( limsup `
 S ) ) )
221220eqcomd 2431 . . . . . . . . . . 11  |-  ( ch 
->  ( ( F `  z )  -  ( limsup `
 S ) )  =  ( ( ( F `  z )  -  ( S `  j ) )  +  ( ( S `  j )  -  ( limsup `
 S ) ) ) )
222221fveq2d 5883 . . . . . . . . . 10  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( limsup `  S ) ) )  =  ( abs `  (
( ( F `  z )  -  ( S `  j )
)  +  ( ( S `  j )  -  ( limsup `  S
) ) ) ) )
223204, 217resubcld 10049 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( ( F `  z )  -  ( S `  j )
)  e.  RR )
224201, 134syl 17 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( limsup `  S )  e.  RR )
225217, 224resubcld 10049 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( ( S `  j )  -  ( limsup `
 S ) )  e.  RR )
226223, 225readdcld 9672 . . . . . . . . . . . . 13  |-  ( ch 
->  ( ( ( F `
 z )  -  ( S `  j ) )  +  ( ( S `  j )  -  ( limsup `  S
) ) )  e.  RR )
227226recnd 9671 . . . . . . . . . . . 12  |-  ( ch 
->  ( ( ( F `
 z )  -  ( S `  j ) )  +  ( ( S `  j )  -  ( limsup `  S
) ) )  e.  CC )
228227abscld 13491 . . . . . . . . . . 11  |-  ( ch 
->  ( abs `  (
( ( F `  z )  -  ( S `  j )
)  +  ( ( S `  j )  -  ( limsup `  S
) ) ) )  e.  RR )
229223recnd 9671 . . . . . . . . . . . . 13  |-  ( ch 
->  ( ( F `  z )  -  ( S `  j )
)  e.  CC )
230229abscld 13491 . . . . . . . . . . . 12  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( S `
 j ) ) )  e.  RR )
231225recnd 9671 . . . . . . . . . . . . 13  |-  ( ch 
->  ( ( S `  j )  -  ( limsup `
 S ) )  e.  CC )
232231abscld 13491 . . . . . . . . . . . 12  |-  ( ch 
->  ( abs `  (
( S `  j
)  -  ( limsup `  S ) ) )  e.  RR )
233230, 232readdcld 9672 . . . . . . . . . . 11  |-  ( ch 
->  ( ( abs `  (
( F `  z
)  -  ( S `
 j ) ) )  +  ( abs `  ( ( S `  j )  -  ( limsup `
 S ) ) ) )  e.  RR )
234208rpred 11343 . . . . . . . . . . 11  |-  ( ch 
->  x  e.  RR )
235229, 231abstrid 13511 . . . . . . . . . . 11  |-  ( ch 
->  ( abs `  (
( ( F `  z )  -  ( S `  j )
)  +  ( ( S `  j )  -  ( limsup `  S
) ) ) )  <_  ( ( abs `  ( ( F `  z )  -  ( S `  j )
) )  +  ( abs `  ( ( S `  j )  -  ( limsup `  S
) ) ) ) )
236234rehalfcld 10861 . . . . . . . . . . . . 13  |-  ( ch 
->  ( x  /  2
)  e.  RR )
237201, 216, 113syl2anc 666 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( S `  j
)  =  ( F `
 ( B  -  ( 1  /  j
) ) ) )
238237oveq2d 6319 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( ( F `  z )  -  ( S `  j )
)  =  ( ( F `  z )  -  ( F `  ( B  -  (
1  /  j ) ) ) ) )
239238fveq2d 5883 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( S `
 j ) ) )  =  ( abs `  ( ( F `  z )  -  ( F `  ( B  -  ( 1  / 
j ) ) ) ) ) )
240239, 230eqeltrrd 2512 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( F `
 ( B  -  ( 1  /  j
) ) ) ) )  e.  RR )
241201, 164syl 17 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  Y  e.  RR )
242151, 203sseldi 3463 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  z  e.  RR )
243201, 216, 58syl2anc 666 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( B  -  (
1  /  j ) )  e.  RR )
244242, 243resubcld 10049 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( z  -  ( B  -  ( 1  /  j ) ) )  e.  RR )
245241, 244remulcld 9673 . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . . . . . 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 4429 . . . . . . . . . . . . . . . . . . . . 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 2857 . . . . . . . . . . . . . . . . . . . 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 216 . . . . . . . . . . . . . . . . . . 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 5879 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  =  x  ->  (
( RR  _D  F
) `  w )  =  ( ( RR 
_D  F ) `  x ) )
255254fveq2d 5883 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  x  ->  ( abs `  ( ( RR 
_D  F ) `  w ) )  =  ( abs `  (
( RR  _D  F
) `  x )
) )
256255breq1d 4431 . . . . . . . . . . . . . . . . . . 19  |-  ( w  =  x  ->  (
( abs `  (
( RR  _D  F
) `  w )
)  <_  Y  <->  ( abs `  ( ( RR  _D  F ) `  x
) )  <_  Y
) )
257256cbvralv 3056 . . . . . . . . . . . . . . . . . 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 216 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  A. w  e.  ( A (,) B ) ( abs `  (
( RR  _D  F
) `  w )
)  <_  Y )
259201, 216, 103syl2anc 666 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( B  -  (
1  /  j ) )  e.  ( A (,) B ) )
260243rexrd 9692 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( B  -  (
1  /  j ) )  e.  RR* )
261201, 30syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  B  e.  RR* )
2623, 216sseldi 3463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  j  e.  RR )
263201, 216, 56syl2anc 666 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  j  =/=  0
)
264262, 263rereccld 10436 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( 1  /  j
)  e.  RR )
265247, 242resubcld 10049 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( B  -  z
)  e.  RR )
266242, 247resubcld 10049 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( z  -  B
)  e.  RR )
267266recnd 9671 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( z  -  B
)  e.  CC )
268267abscld 13491 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( abs `  (
z  -  B ) )  e.  RR )
269265leabsd 13470 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( B  -  z
)  <_  ( abs `  ( B  -  z
) ) )
270201, 85syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  B  e.  CC )
271242recnd 9671 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  z  e.  CC )
272270, 271abssubd 13508 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( abs `  ( B  -  z )
)  =  ( abs `  ( z  -  B
) ) )
273269, 272breqtrd 4446 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( B  -  z
)  <_  ( abs `  ( z  -  B
) ) )
274199simprd 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( abs `  (
z  -  B ) )  <  ( 1  /  j ) )
275265, 268, 264, 273, 274lelttrd 9795 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( B  -  z
)  <  ( 1  /  j ) )
276247, 242, 264, 275ltsub23d 10220 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( B  -  (
1  /  j ) )  <  z )
277201, 28syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  A  e.  RR* )
278 iooltub 37485 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  z  e.  ( A (,) B
) )  ->  z  <  B )
279277, 261, 203, 278syl3anc 1265 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  z  <  B )
280260, 261, 242, 276, 279eliood 37470 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  z  e.  (
( B  -  (
1  /  j ) ) (,) B ) )
281246, 247, 202, 248, 241, 258, 259, 280dvbdfbdioolem1 37664 . . . . . . . . . . . . . . . 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 461 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( F `
 ( B  -  ( 1  /  j
) ) ) ) )  <_  ( Y  x.  ( z  -  ( B  -  ( 1  /  j ) ) ) ) )
283201, 216, 57syl2anc 666 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( 1  /  j
)  e.  RR )
284241, 283remulcld 9673 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( Y  x.  (
1  /  j ) )  e.  RR )
285156, 148ffvelrnd 6036 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( RR  _D  F ) `  (
( A  +  B
)  /  2 ) )  e.  RR )
286285recnd 9671 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( RR  _D  F ) `  (
( A  +  B
)  /  2 ) )  e.  CC )
287286abscld 13491 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( abs `  (
( RR  _D  F
) `  ( ( A  +  B )  /  2 ) ) )  e.  RR )
288286absge0d 13499 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  0  <_  ( abs `  ( ( RR  _D  F ) `  (
( A  +  B
)  /  2 ) ) ) )
289 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  ( ( A  +  B )  / 
2 )  ->  (
( RR  _D  F
) `  x )  =  ( ( RR 
_D  F ) `  ( ( A  +  B )  /  2
) ) )
290289fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  ( ( A  +  B )  / 
2 )  ->  ( abs `  ( ( RR 
_D  F ) `  x ) )  =  ( abs `  (
( RR  _D  F
) `  ( ( A  +  B )  /  2 ) ) ) )
291146eqcomi 2436 . . . . . . . . . . . . . . . . . . . . . . 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 4434 . . . . . . . . . . . . . . . . . . . . 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 3181 . . . . . . . . . . . . . . . . . . . 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 666 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( abs `  (
( RR  _D  F
) `  ( ( A  +  B )  /  2 ) ) )  <_  Y )
29614, 287, 164, 288, 295letrd 9794 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  0  <_  Y )
297201, 296syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  0  <_  Y )
298283recnd 9671 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( 1  /  j
)  e.  CC )
299 sub31 37390 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( z  e.  CC  /\  B  e.  CC  /\  (
1  /  j )  e.  CC )  -> 
( z  -  ( B  -  ( 1  /  j ) ) )  =  ( ( 1  /  j )  -  ( B  -  z ) ) )
300271, 270, 298, 299syl3anc 1265 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( z  -  ( B  -  ( 1  /  j ) ) )  =  ( ( 1  /  j )  -  ( B  -  z ) ) )
301242, 247posdifd 10202 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( z  <  B  <->  0  <  ( B  -  z ) ) )
302279, 301mpbid 214 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  0  <  ( B  -  z ) )
303265, 302elrpd 11340 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( B  -  z
)  e.  RR+ )
304283, 303ltsubrpd 11372 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( ( 1  / 
j )  -  ( B  -  z )
)  <  ( 1  /  j ) )
305300, 304eqbrtrd 4442 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( z  -  ( B  -  ( 1  /  j ) ) )  <  ( 1  /  j ) )
306244, 283, 305ltled 9785 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( z  -  ( B  -  ( 1  /  j ) ) )  <_  ( 1  /  j ) )
307244, 283, 241, 297, 306lemul2ad 10549 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( Y  x.  (
z  -  ( B  -  ( 1  / 
j ) ) ) )  <_  ( Y  x.  ( 1  /  j
) ) )
308284adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  Y  =  0 )  ->  ( Y  x.  ( 1  /  j ) )  e.  RR )
309236adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  Y  =  0 )  ->  (
x  /  2 )  e.  RR )
310 oveq1 6310 . . . . . . . . . . . . . . . . . . . 20  |-  ( Y  =  0  ->  ( Y  x.  ( 1  /  j ) )  =  ( 0  x.  ( 1  /  j
) ) )
311298mul02d 9833 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( 0  x.  (
1  /  j ) )  =  0 )
312310, 311sylan9eqr 2486 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  Y  =  0 )  ->  ( Y  x.  ( 1  /  j ) )  =  0 )
313208rphalfcld 11355 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( x  /  2
)  e.  RR+ )
314313rpgt0d 11346 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  0  <  ( x  /  2 ) )
315314adantr 467 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  Y  =  0 )  ->  0  <  ( x  /  2
) )
316312, 315eqbrtrd 4442 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  Y  =  0 )  ->  ( Y  x.  ( 1  /  j ) )  <  ( x  / 
2 ) )
317308, 309, 316ltled 9785 . . . . . . . . . . . . . . . . 17  |-  ( ( ch  /\  Y  =  0 )  ->  ( Y  x.  ( 1  /  j ) )  <_  ( x  / 
2 ) )
318241adantr 467 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  -.  Y  =  0 )  ->  Y  e.  RR )
319297adantr 467 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  -.  Y  =  0 )  -> 
0  <_  Y )
320 neqne 37279 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  Y  =  0  ->  Y  =/=  0 )
321320adantl 468 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  -.  Y  =  0 )  ->  Y  =/=  0 )
322318, 319, 321ne0gt0d 9774 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  -.  Y  =  0 )  -> 
0  <  Y )
323284adantr 467 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  j ) )  e.  RR )
3243, 211sseldi 3463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  N  e.  RR )
325 0red 9646 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  0  e.  RR )
326201, 208, 142syl2anc 666 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  M  e.  RR )
327201, 65syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  0  <  M )
328201, 208, 187syl2anc 666 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  M  <_  N )
329325, 326, 324, 327, 328ltletrd 9797 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  0  <  N )
330329gt0ne0d 10180 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  N  =/=  0
)
331324, 330rereccld 10436 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( 1  /  N
)  e.  RR )
332241, 331remulcld 9673 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( Y  x.  (
1  /  N ) )  e.  RR )
333332adantr 467 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  N ) )  e.  RR )
334236adantr 467 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  0  < 
Y )  ->  (
x  /  2 )  e.  RR )
335283adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  0  < 
Y )  ->  (
1  /  j )  e.  RR )
336331adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  0  < 
Y )  ->  (
1  /  N )  e.  RR )
337241adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  0  < 
Y )  ->  Y  e.  RR )
338297adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  0  < 
Y )  ->  0  <_  Y )
339324, 329elrpd 11340 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  N  e.  RR+ )
340201, 216, 94syl2anc 666 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  j  e.  RR+ )
341 1red 9660 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  1  e.  RR )
34296a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  0  <_  1 )
343215, 189syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  N  <_  j )
344339, 340, 341, 342, 343lediv2ad 11365 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( 1  /  j
)  <_  ( 1  /  N ) )
345344adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  0  < 
Y )  ->  (
1  /  j )  <_  ( 1  /  N ) )
346335, 336, 337, 338, 345lemul2ad 10549 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  j ) )  <_  ( Y  x.  ( 1  /  N
) ) )
347234recnd 9671 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  x  e.  CC )
348 2cnd 10684 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  2  e.  CC )
349208rpne0d 11348 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  x  =/=  0
)
350174a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  2  =/=  0
)
351347, 348, 349, 350divne0d 10401 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ch 
->  ( x  /  2
)  =/=  0 )
352241, 236, 351redivcld 10437 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  ( Y  /  (
x  /  2 ) )  e.  RR )
353352adantr 467 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( x  / 
2 ) )  e.  RR )
354 simpr 463 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ch  /\  0  < 
Y )  ->  0  <  Y )
355314adantr 467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ch  /\  0  < 
Y )  ->  0  <  ( x  /  2
) )
356337, 334, 354, 355divgt0d 10544 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  0  < 
Y )  ->  0  <  ( Y  /  (
x  /  2 ) ) )
357353, 356elrpd 11340 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( x  / 
2 ) )  e.  RR+ )
358357rprecred 11354 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  0  < 
Y )  ->  (
1  /  ( Y  /  ( x  / 
2 ) ) )  e.  RR )
359339adantr 467 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  N  e.  RR+ )
360 1red 9660 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  1  e.  RR )
36196a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  0  <_  1 )
362352flcld 12035 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ch 
->  ( |_ `  ( Y  /  ( x  / 
2 ) ) )  e.  ZZ )
363362peano2zd 11045 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 )  e.  ZZ )
364363zred 11042 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ch 
->  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 )  e.  RR )
365201, 140syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ch 
->  M  e.  ZZ )
366363, 365ifcld 3953 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ch 
->  if ( M  <_ 
( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 ) ,  ( ( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) ,  M )  e.  ZZ )
367145, 366syl5eqel 2515 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  N  e.  ZZ )
368367zred 11042 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ch 
->  N  e.  RR )
369 flltp1 12037 . . . . . . . . . . . . . . . . . . . . . . . . . 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 11484 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 666 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 )  <_  if ( M  <_  ( ( |_
`  ( Y  / 
( x  /  2
) ) )  +  1 ) ,  ( ( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) ,  M ) )
374373, 145syl6breqr 4462 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ch 
->  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 )  <_  N )
375352, 364, 368, 370, 374ltletrd 9797 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  ( Y  /  (
x  /  2 ) )  <  N )
376352, 324, 375ltled 9785 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( Y  /  (
x  /  2 ) )  <_  N )
377376adantr 467 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( x  / 
2 ) )  <_  N )
378357, 359, 360, 361, 377lediv2ad 11365 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  0  < 
Y )  ->  (
1  /  N )  <_  ( 1  / 
( Y  /  (
x  /  2 ) ) ) )
379336, 358, 337, 338, 378lemul2ad 10549 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  N ) )  <_  ( Y  x.  ( 1  /  ( Y  /  ( x  / 
2 ) ) ) ) )
380337recnd 9671 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  Y  e.  CC )
381353recnd 9671 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( x  / 
2 ) )  e.  CC )
382356gt0ne0d 10180 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( x  / 
2 ) )  =/=  0 )
383380, 381, 382divrecd 10388 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( Y  / 
( x  /  2
) ) )  =  ( Y  x.  (
1  /  ( Y  /  ( x  / 
2 ) ) ) ) )
384334recnd 9671 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  (
x  /  2 )  e.  CC )
385354gt0ne0d 10180 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  Y  =/=  0 )
386351adantr 467 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  (
x  /  2 )  =/=  0 )
387380, 384, 385, 386ddcand 10405 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( Y  / 
( x  /  2
) ) )  =  ( x  /  2
) )
388383, 387eqtr3d 2466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  ( Y  / 
( x  /  2
) ) ) )  =  ( x  / 
2 ) )
389379, 388breqtrd 4446 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  N ) )  <_  ( x  / 
2 ) )
390323, 333, 334, 346, 389letrd 9794 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  j ) )  <_  ( x  / 
2 ) )
391322, 390syldan 473 . . . . . . . . . . . . . . . . 17  |-  ( ( ch  /\  -.  Y  =  0 )  -> 
( Y  x.  (
1  /  j ) )  <_  ( x  /  2 ) )
392317, 391pm2.61dan 799 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( Y  x.  (
1  /  j ) )  <_  ( x  /  2 ) )
393245, 284, 236, 307, 392letrd 9794 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( Y  x.  (
z  -  ( B  -  ( 1  / 
j ) ) ) )  <_  ( x  /  2 ) )
394240, 245, 236, 282, 393letrd 9794 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( F `
 ( B  -  ( 1  /  j
) ) ) ) )  <_  ( x  /  2 ) )
395239, 394eqbrtrd 4442 . . . . . . . . . . . . 13  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( S `
 j ) ) )  <_  ( x  /  2 ) )
396 simpllr 768 . . . . . . . . . . . . . 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 10237 . . . . . . . . . . . 12  |-  ( ch 
->  ( ( abs `  (
( F `  z
)  -  ( S `
 j ) ) )  +  ( abs `  ( ( S `  j )  -  ( limsup `
 S ) ) ) )  <  (
( x  /  2
)  +  ( x  /  2 ) ) )
3993472halvesd 10860 . . . . . . . . . . . 12  |-  ( ch 
->  ( ( x  / 
2 )  +  ( x  /  2 ) )  =  x )
400398, 399breqtrd 4446 . . . . . . . . . . 11  |-  ( ch 
->  ( ( abs `  (
( F `  z
)  -  ( S `
 j ) ) )  +  ( abs `  ( ( S `  j )  -  ( limsup `
 S ) ) ) )  <  x
)
401228, 233, 234, 235, 400lelttrd 9795 . . . . . . . . . 10  |-  ( ch 
->  ( abs `  (
( ( F `  z )  -  ( S `  j )
)  +  ( ( S `  j )  -  ( limsup `  S
) ) ) )  <  x )
402222, 401eqbrtrd 4442 . . . . . . . . 9  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( limsup `  S ) ) )  <  x )
403198, 402sylbir 217 . . . . . . . 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 721 . . . . . . 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 436 . . . . . 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 2840 . . . . 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 4425 . . . . . . . . 9  |-  ( y  =  ( 1  / 
j )  ->  (
( abs `  (
z  -  B ) )  <  y  <->  ( abs `  ( z  -  B
) )  <  (
1  /  j ) ) )
408407anbi2d 709 . . . . . . . 8  |-  ( y  =  ( 1  / 
j )  ->  (
( z  =/=  B  /\  ( abs `  (
z  -  B ) )  <  y )  <-> 
( z  =/=  B  /\  ( abs `  (
z  -  B ) )  <  ( 1  /  j ) ) ) )
409408imbi1d 319 . . . . . . 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 2865 . . . . . 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 3183 . . . . 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 666 . . . 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 463 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  <_  N )  ->  b  <_  N )
414413iftrued 3918 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  <_  N )  ->  if ( b  <_  N ,  N ,  b )  =  N )
415 uzid 11175 . . . . . . . . . . . 12  |-  ( N  e.  ZZ  ->  N  e.  ( ZZ>= `  N )
)
416181, 415syl 17 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  N  e.  ( ZZ>= `  N )
)
417416adantr 467 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  <_  N )  ->  N  e.  ( ZZ>= `  N )
)
418414, 417eqeltrd 2511 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  <_  N )  ->  if ( b  <_  N ,  N ,  b )  e.  ( ZZ>= `  N
) )
419418adantlr 720 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  b  <_  N )  ->  if ( b  <_  N ,  N ,  b )  e.  ( ZZ>= `  N )
)
420 iffalse 3919 . . . . . . . . . 10  |-  ( -.  b  <_  N  ->  if ( b  <_  N ,  N ,  b )  =  b )
421420adantl 468 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  if (
b  <_  N ,  N ,  b )  =  b )
422181ad2antrr 731 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  N  e.  ZZ )
423 simplr 761 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  b  e.  ZZ )
424422zred 11042 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  N  e.  RR )
425423zred 11042 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  b  e.  RR )
426 simpr 463 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  -.  b  <_  N )
427424, 425ltnled 9784 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  ( N  <  b  <->  -.  b  <_  N ) )
428426, 427mpbird 236 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  N  <  b )
429424, 425, 428ltled 9785 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  N  <_  b )
430 eluz2 11167 . . . . . . . . . 10  |-  ( b  e.  ( ZZ>= `  N
)  <->  ( N  e.  ZZ  /\  b  e.  ZZ  /\  N  <_ 
b ) )
431422, 423, 429, 430syl3anbrc 1190 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  b  e.  ( ZZ>= `  N )
)
432421, 431eqeltrd 2511 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  if (
b  <_  N ,  N ,  b )  e.  ( ZZ>= `  N )
)
433419, 432pm2.61dan 799 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  ->  if ( b  <_  N ,  N ,  b )  e.  ( ZZ>= `  N
) )
434433adantr 467 . . . . . 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 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
) ) )  ->  A. c  e.  ( ZZ>=
`  b ) ( ( S `  c
)  e.  CC  /\  ( abs `  ( ( S `  c )  -  ( limsup `  S
) ) )  < 
( x  /  2
) ) )
436 simpr 463 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  ->  b  e.  ZZ )
437181adantr 467 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  ->  N  e.  ZZ )
438437, 436ifcld 3953 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  ->  if ( b  <_  N ,  N ,  b )  e.  ZZ )
439436zred 11042 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  ->  b  e.  RR )
440437zred 11042 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  ->  N  e.  RR )
441 max1 11482 . . . . . . . . . . 11  |-  ( ( b  e.  RR  /\  N  e.  RR )  ->  b  <_  if (
b  <_  N ,  N ,  b )
)
442439, 440, 441syl2anc 666 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  ->  b  <_  if ( b  <_  N ,  N , 
b ) )
443 eluz2 11167 . . . . . . . . . 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 1190 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  ->  if ( b  <_  N ,  N ,  b )  e.  ( ZZ>= `  b
) )
445444adantr 467 . . . . . . . 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 5879 . . . . . . . . . . 11  |-  ( c  =  if ( b  <_  N ,  N ,  b )  -> 
( S `  c
)  =  ( S `
 if ( b  <_  N ,  N ,  b ) ) )
447446eleq1d 2492 . . . . . . . . . 10  |-  ( c  =  if ( b  <_  N ,  N ,  b )  -> 
( ( S `  c )  e.  CC  <->  ( S `  if ( b  <_  N ,  N ,  b )
)  e.  CC ) )
448446oveq1d 6318 . . . . . . . . . . . 12  |-  ( c  =  if ( b  <_  N ,  N ,  b )  -> 
( ( S `  c )  -  ( limsup `
 S ) )  =  ( ( S `
 if ( b  <_  N ,  N ,  b ) )  -  ( limsup `  S
) ) )
449448fveq2d 5883 . . . . . . . . . . 11  |-  ( c  =  if ( b  <_  N ,  N ,  b )  -> 
( abs `  (
( S `  c
)  -  ( limsup `  S ) ) )  =  ( abs `  (
( S `  if ( b  <_  N ,  N ,  b ) )  -  ( limsup `  S ) ) ) )
450449breq1d 4431 . . . . . . . . . 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 716 . . . . . . . . 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 3182 . . . . . . . 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 666 . . . . . . 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 465 . . . . . 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 5879 . . . . . . . . . 10  |-  ( j  =  if ( b  <_  N ,  N ,  b )  -> 
( S `  j
)  =  ( S `
 if ( b  <_  N ,  N ,  b ) ) )
456455oveq1d 6318 . . . . . . . . 9  |-  ( j  =  if ( b  <_  N ,  N ,  b )  -> 
( ( S `  j )  -  ( limsup `
 S ) )  =  ( ( S `
 if ( b  <_  N ,  N ,  b ) )  -  ( limsup `  S
) ) )
457456fveq2d 5883 . . . . . . . 8  |-  ( j  =  if ( b  <_  N ,  N ,  b )  -> 
( abs `  (
( S `  j
)  -  ( limsup `  S ) ) )  =  ( abs `  (
( S `  if ( b  <_  N ,  N ,  b ) )  -  ( limsup `  S ) ) ) )
458457breq1d 4431 . . . . . . 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 3183 . . . . . 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 666 . . . . 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 9598 . . . . . . . . . . . . . 14  |-  RR  C_  CC
462461a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  RR  C_  CC )
46326, 462fssd 5753 . . . . . . . . . . . . . 14  |-  ( ph  ->  F : ( A (,) B ) --> CC )
464 dvcn 22867 . . . . . . . . . . . . . 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 1268 . . . . . . . . . . . . 13  |-  ( ph  ->  F  e.  ( ( A (,) B )
-cn-> CC ) )
466 cncffvrn 21922 . . . . . . . . . . . . 13  |-  ( ( RR  C_  CC  /\  F  e.  ( ( A (,) B ) -cn-> CC ) )  ->  ( F  e.  ( ( A (,) B ) -cn-> RR )  <-> 
F : ( A (,) B ) --> RR ) )
467462, 465, 466syl2anc 666 . . . . . . . . . . . 12  |-  ( ph  ->  ( F  e.  ( ( A (,) B
) -cn-> RR )  <->  F :
( A (,) B
) --> RR ) )
46826, 467mpbird 236 . . . . . . . . . . 11  |-  ( ph  ->  F  e.  ( ( A (,) B )
-cn-> RR ) )
469 ioodvbdlimc2lem.r . . . . . . . . . . . 12  |-  R  =  ( j  e.  (
ZZ>= `  M )  |->  ( B  -  ( 1  /  j ) ) )
470103, 469fmptd 6059 . . . . . . . . . . 11  |-  ( ph  ->  R : ( ZZ>= `  M ) --> ( A (,) B ) )
471 eqid 2423 . . . . . . . . . . 11  |-  ( j  e.  ( ZZ>= `  M
)  |->  ( F `  ( R `  j ) ) )  =  ( j  e.  ( ZZ>= `  M )  |->  ( F `
 ( R `  j ) ) )
472 climrel 13549 . . . . . . . . . . . . 13  |-  Rel  ~~>
473472a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  Rel  ~~>  )
474 fvex 5889 . . . . . . . . . . . . . . . . 17  |-  ( ZZ>= `  M )  e.  _V
475474mptex 6149 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( ZZ>= `  M
)  |->  B )  e. 
_V
476475a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( j  e.  (
ZZ>= `  M )  |->  B )  e.  _V )
477 eqidd 2424 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( ZZ>= `  M )
)  ->  ( j  e.  ( ZZ>= `  M )  |->  B )  =  ( j  e.  ( ZZ>= `  M )  |->  B ) )
478 eqidd 2424 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  M )
)  /\  j  =  m )  ->  B  =  B )
479 simpr 463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( ZZ>= `  M )
)  ->  m  e.  ( ZZ>= `  M )
)
4806adantr 467 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( ZZ>= `  M )
)  ->  B  e.  RR )
481477, 478, 479, 480fvmptd 5968 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( ZZ>= `  M )
)  ->  ( (
j  e.  ( ZZ>= `  M )  |->  B ) `
 m )  =  B )
48223, 22, 476, 85, 481climconst 13600 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( j  e.  (
ZZ>= `  M )  |->  B )  ~~>  B )
483474mptex 6149 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( ZZ>= `  M
)  |->  ( B  -  ( 1  /  j
) ) )  e. 
_V
484469, 483eqeltri 2507 . . . . . . . . . . . . . . 15  |-  R  e. 
_V
485484a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  R  e.  _V )
486 1cnd 9661 . . . . . . . . . . . . . . 15  |-  ( ph  ->  1  e.  CC )
487 elnnnn0b 10916 . . . . . . . . . . . . . . . 16  |-  ( M  e.  NN  <->  ( M  e.  NN0  /\  0  < 
M ) )
48821, 65, 487sylanbrc 669 . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  e.  NN )
489 divcnvg 37571 . . . . . . . . . . . . . . 15  |-  ( ( 1  e.  CC  /\  M  e.  NN )  ->  ( j  e.  (
ZZ>= `  M )  |->  ( 1  /  j ) )  ~~>  0 )
490486, 488, 489syl2anc 666 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( j  e.  (
ZZ>= `  M )  |->  ( 1  /  j ) )  ~~>  0 )
491 eqidd 2424 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( j  e.  ( ZZ>= `  M )  |->  B )  =  ( j  e.  ( ZZ>= `  M )  |->  B ) )
492 eqidd 2424 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( ZZ>= `  M )
)  /\  j  =  i )  ->  B  =  B )
493 simpr 463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  e.  ( ZZ>= `  M )
)
4946adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  B  e.  RR )
495491, 492, 493, 494fvmptd 5968 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( (
j  e.  ( ZZ>= `  M )  |->  B ) `
 i )  =  B )
496495, 494eqeltrd 2511 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( (
j  e.  ( ZZ>= `  M )  |->  B ) `
 i )  e.  RR )
497496recnd 9671 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( (
j  e.  ( ZZ>= `  M )  |->  B ) `
 i )  e.  CC )
498 eqidd 2424 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( j  e.  ( ZZ>= `  M )  |->  ( 1  /  j
) )  =  ( j  e.  ( ZZ>= `  M )  |->  ( 1  /  j ) ) )
499 oveq2 6311 . . . . . . . . . . . . . . . . 17  |-  ( j  =  i  ->  (
1  /  j )  =  ( 1  / 
i ) )
500499adantl 468 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( ZZ>= `  M )
)  /\  j  =  i )  ->  (
1  /  j )  =  ( 1  / 
i ) )
5013, 493sseldi 3463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  e.  RR )
502 0red 9646 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  0  e.  RR )
50360adantr 467 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  M  e.  RR )
50465adantr 467 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  0  <  M )
505 eluzle 11173 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( ZZ>= `  M
)  ->  M  <_  i )
506505adantl 468 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  M  <_  i )
507502, 503, 501, 504, 506ltletrd 9797 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  0  <  i )
508507gt0ne0d 10180 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  =/=  0 )
509501, 508rereccld 10436 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( 1  /  i )  e.  RR )
510498, 500, 493, 509fvmptd 5968 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( (
j  e.  ( ZZ>= `  M )  |->  ( 1  /  j ) ) `
 i )  =  ( 1  /  i
) )
511501recnd 9671 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  e.  CC )
512511, 508reccld 10378 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( 1  /  i )  e.  CC )
513510, 512eqeltrd 2511 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( (
j  e.  ( ZZ>= `  M )  |->  ( 1  /  j ) ) `
 i )  e.  CC )
514499oveq2d 6319 . . . . . . . . . . . . . . . . 17  |-  ( j  =  i  ->  ( B  -  ( 1  /  j ) )  =  ( B  -  ( 1  /  i
) ) )
515 ovex 6331 . . . . . . . . . . . . . . . . 17  |-  ( B  -  ( 1  / 
i ) )  e. 
_V
516514, 469, 515fvmpt 5962 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( ZZ>= `  M
)  ->  ( R `  i )  =  ( B  -  ( 1  /  i ) ) )
517516adantl 468 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( R `  i )  =  ( B  -  ( 1  /  i ) ) )
518495, 510oveq12d 6321 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( (
( j  e.  (
ZZ>= `  M )  |->  B ) `  i )  -  ( ( j  e.  ( ZZ>= `  M
)  |->  ( 1  / 
j ) ) `  i ) )  =  ( B  -  (
1  /  i ) ) )
519517, 518eqtr4d 2467 . . . . . . . . . . . . . 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 13690 . . . . . . . . . . . . 13  |-  ( ph  ->  R  ~~>  ( B  - 
0 ) )
52185subid1d 9977 . . . . . . . . . . . . 13  |-  ( ph  ->  ( B  -  0 )  =  B )
522520, 521breqtrd 4446