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

Theorem ioodvbdlimc2lemOLD 37749
Description: Limit at the upper bound of an open interval, for a function with bounded derivative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) Obsolete version of ioodvbdlimc2lem 37748 as of 3-Oct-2020. (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
ioodvbdlimc2lemOLD.a  |-  ( ph  ->  A  e.  RR )
ioodvbdlimc2lemOLD.b  |-  ( ph  ->  B  e.  RR )
ioodvbdlimc2lemOLD.altb  |-  ( ph  ->  A  <  B )
ioodvbdlimc2lemOLD.f  |-  ( ph  ->  F : ( A (,) B ) --> RR )
ioodvbdlimc2lemOLD.dmdv  |-  ( ph  ->  dom  ( RR  _D  F )  =  ( A (,) B ) )
ioodvbdlimc2lemOLD.dvbd  |-  ( ph  ->  E. y  e.  RR  A. x  e.  ( A (,) B ) ( abs `  ( ( RR  _D  F ) `
 x ) )  <_  y )
ioodvbdlimc2lemOLD.y  |-  Y  =  sup ( ran  (
x  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `
 x ) ) ) ,  RR ,  <  )
ioodvbdlimc2lemOLD.m  |-  M  =  ( ( |_ `  ( 1  /  ( B  -  A )
) )  +  1 )
ioodvbdlimc2lemOLD.s  |-  S  =  ( j  e.  (
ZZ>= `  M )  |->  ( F `  ( B  -  ( 1  / 
j ) ) ) )
ioodvbdlimc2lemOLD.r  |-  R  =  ( j  e.  (
ZZ>= `  M )  |->  ( B  -  ( 1  /  j ) ) )
ioodvbdlimc2lemOLD.n  |-  N  =  if ( M  <_ 
( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 ) ,  ( ( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) ,  M )
ioodvbdlimc2lemOLD.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
ioodvbdlimc2lemOLD  |-  ( 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 ioodvbdlimc2lemOLD
Dummy variables  b 
k  h  i  l  w  m  c  a are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uzssz 11185 . . . . . 6  |-  ( ZZ>= `  M )  C_  ZZ
2 zssre 10951 . . . . . 6  |-  ZZ  C_  RR
31, 2sstri 3473 . . . . 5  |-  ( ZZ>= `  M )  C_  RR
43a1i 11 . . . 4  |-  ( ph  ->  ( ZZ>= `  M )  C_  RR )
5 ioodvbdlimc2lemOLD.m . . . . . . 7  |-  M  =  ( ( |_ `  ( 1  /  ( B  -  A )
) )  +  1 )
6 ioodvbdlimc2lemOLD.b . . . . . . . . . . 11  |-  ( ph  ->  B  e.  RR )
7 ioodvbdlimc2lemOLD.a . . . . . . . . . . 11  |-  ( ph  ->  A  e.  RR )
86, 7resubcld 10054 . . . . . . . . . 10  |-  ( ph  ->  ( B  -  A
)  e.  RR )
9 ioodvbdlimc2lemOLD.altb . . . . . . . . . . . 12  |-  ( ph  ->  A  <  B )
107, 6posdifd 10207 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  <  B  <->  0  <  ( B  -  A ) ) )
119, 10mpbid 213 . . . . . . . . . . 11  |-  ( ph  ->  0  <  ( B  -  A ) )
1211gt0ne0d 10185 . . . . . . . . . 10  |-  ( ph  ->  ( B  -  A
)  =/=  0 )
138, 12rereccld 10441 . . . . . . . . 9  |-  ( ph  ->  ( 1  /  ( B  -  A )
)  e.  RR )
14 0red 9651 . . . . . . . . . 10  |-  ( ph  ->  0  e.  RR )
158, 11recgt0d 10548 . . . . . . . . . 10  |-  ( ph  ->  0  <  ( 1  /  ( B  -  A ) ) )
1614, 13, 15ltled 9790 . . . . . . . . 9  |-  ( ph  ->  0  <_  ( 1  /  ( B  -  A ) ) )
17 flge0nn0 12060 . . . . . . . . 9  |-  ( ( ( 1  /  ( B  -  A )
)  e.  RR  /\  0  <_  ( 1  / 
( B  -  A
) ) )  -> 
( |_ `  (
1  /  ( B  -  A ) ) )  e.  NN0 )
1813, 16, 17syl2anc 665 . . . . . . . 8  |-  ( ph  ->  ( |_ `  (
1  /  ( B  -  A ) ) )  e.  NN0 )
19 peano2nn0 10917 . . . . . . . 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 2511 . . . . . 6  |-  ( ph  ->  M  e.  NN0 )
2221nn0zd 11045 . . . . 5  |-  ( ph  ->  M  e.  ZZ )
23 eqid 2422 . . . . . 6  |-  ( ZZ>= `  M )  =  (
ZZ>= `  M )
2423uzsup 12096 . . . . 5  |-  ( M  e.  ZZ  ->  sup ( ( ZZ>= `  M
) ,  RR* ,  <  )  = +oo )
2522, 24syl 17 . . . 4  |-  ( ph  ->  sup ( ( ZZ>= `  M ) ,  RR* ,  <  )  = +oo )
26 ioodvbdlimc2lemOLD.f . . . . . . 7  |-  ( ph  ->  F : ( A (,) B ) --> RR )
2726adantr 466 . . . . . 6  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  F :
( A (,) B
) --> RR )
287rexrd 9697 . . . . . . . 8  |-  ( ph  ->  A  e.  RR* )
2928adantr 466 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  A  e.  RR* )
306rexrd 9697 . . . . . . . 8  |-  ( ph  ->  B  e.  RR* )
3130adantr 466 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  B  e.  RR* )
326adantr 466 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  B  e.  RR )
33 eluzelre 11176 . . . . . . . . . 10  |-  ( j  e.  ( ZZ>= `  M
)  ->  j  e.  RR )
3433adantl 467 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  j  e.  RR )
35 0red 9651 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  0  e.  RR )
36 0red 9651 . . . . . . . . . . . . 13  |-  ( j  e.  ( ZZ>= `  M
)  ->  0  e.  RR )
37 1red 9665 . . . . . . . . . . . . 13  |-  ( j  e.  ( ZZ>= `  M
)  ->  1  e.  RR )
3836, 37readdcld 9677 . . . . . . . . . . . 12  |-  ( j  e.  ( ZZ>= `  M
)  ->  ( 0  +  1 )  e.  RR )
3938adantl 467 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( 0  +  1 )  e.  RR )
4036ltp1d 10544 . . . . . . . . . . . 12  |-  ( j  e.  ( ZZ>= `  M
)  ->  0  <  ( 0  +  1 ) )
4140adantl 467 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  0  <  ( 0  +  1 ) )
42 eluzel2 11171 . . . . . . . . . . . . . 14  |-  ( j  e.  ( ZZ>= `  M
)  ->  M  e.  ZZ )
4342zred 11047 . . . . . . . . . . . . 13  |-  ( j  e.  ( ZZ>= `  M
)  ->  M  e.  RR )
4443adantl 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  M  e.  RR )
4513flcld 12040 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( |_ `  (
1  /  ( B  -  A ) ) )  e.  ZZ )
4645zred 11047 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( |_ `  (
1  /  ( B  -  A ) ) )  e.  RR )
47 1red 9665 . . . . . . . . . . . . . . 15  |-  ( ph  ->  1  e.  RR )
4818nn0ge0d 10935 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  <_  ( |_ `  ( 1  /  ( B  -  A )
) ) )
4914, 46, 47, 48leadd1dd 10234 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0  +  1 )  <_  ( ( |_ `  ( 1  / 
( B  -  A
) ) )  +  1 ) )
5049, 5syl6breqr 4464 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 0  +  1 )  <_  M )
5150adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( 0  +  1 )  <_  M )
52 eluzle 11178 . . . . . . . . . . . . 13  |-  ( j  e.  ( ZZ>= `  M
)  ->  M  <_  j )
5352adantl 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  M  <_  j )
5439, 44, 34, 51, 53letrd 9799 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( 0  +  1 )  <_ 
j )
5535, 39, 34, 41, 54ltletrd 9802 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  0  <  j )
5655gt0ne0d 10185 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  j  =/=  0 )
5734, 56rereccld 10441 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( 1  /  j )  e.  RR )
5832, 57resubcld 10054 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( B  -  ( 1  / 
j ) )  e.  RR )
597adantr 466 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  A  e.  RR )
6021nn0red 10933 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  RR )
6114, 47readdcld 9677 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0  +  1 )  e.  RR )
6246, 47readdcld 9677 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( |_ `  ( 1  /  ( B  -  A )
) )  +  1 )  e.  RR )
6314ltp1d 10544 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <  ( 0  +  1 ) )
6414, 61, 62, 63, 49ltletrd 9802 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <  ( ( |_ `  ( 1  /  ( B  -  A ) ) )  +  1 ) )
6564, 5syl6breqr 4464 . . . . . . . . . . . 12  |-  ( ph  ->  0  <  M )
6665gt0ne0d 10185 . . . . . . . . . . 11  |-  ( ph  ->  M  =/=  0 )
6760, 66rereccld 10441 . . . . . . . . . 10  |-  ( ph  ->  ( 1  /  M
)  e.  RR )
6867adantr 466 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( 1  /  M )  e.  RR )
6932, 68resubcld 10054 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( B  -  ( 1  /  M ) )  e.  RR )
705eqcomi 2435 . . . . . . . . . . . . 13  |-  ( ( |_ `  ( 1  /  ( B  -  A ) ) )  +  1 )  =  M
7170oveq2i 6316 . . . . . . . . . . . 12  |-  ( 1  /  ( ( |_
`  ( 1  / 
( B  -  A
) ) )  +  1 ) )  =  ( 1  /  M
)
7271, 67syl5eqel 2511 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  /  (
( |_ `  (
1  /  ( B  -  A ) ) )  +  1 ) )  e.  RR )
7313, 15elrpd 11345 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1  /  ( B  -  A )
)  e.  RR+ )
7462, 64elrpd 11345 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( |_ `  ( 1  /  ( B  -  A )
) )  +  1 )  e.  RR+ )
75 1rp 11313 . . . . . . . . . . . . . 14  |-  1  e.  RR+
7675a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  1  e.  RR+ )
77 fllelt 12039 . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1  /  ( B  -  A )
)  <  ( ( |_ `  ( 1  / 
( B  -  A
) ) )  +  1 ) )
8073, 74, 76, 79ltdiv2dd 37463 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  /  (
( |_ `  (
1  /  ( B  -  A ) ) )  +  1 ) )  <  ( 1  /  ( 1  / 
( B  -  A
) ) ) )
818recnd 9676 . . . . . . . . . . . . 13  |-  ( ph  ->  ( B  -  A
)  e.  CC )
8281, 12recrecd 10387 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  /  (
1  /  ( B  -  A ) ) )  =  ( B  -  A ) )
8380, 82breqtrd 4448 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  /  (
( |_ `  (
1  /  ( B  -  A ) ) )  +  1 ) )  <  ( B  -  A ) )
8472, 8, 6, 83ltsub2dd 10233 . . . . . . . . . 10  |-  ( ph  ->  ( B  -  ( B  -  A )
)  <  ( B  -  ( 1  / 
( ( |_ `  ( 1  /  ( B  -  A )
) )  +  1 ) ) ) )
856recnd 9676 . . . . . . . . . . 11  |-  ( ph  ->  B  e.  CC )
867recnd 9676 . . . . . . . . . . 11  |-  ( ph  ->  A  e.  CC )
8785, 86nncand 9998 . . . . . . . . . 10  |-  ( ph  ->  ( B  -  ( B  -  A )
)  =  A )
8871oveq2i 6316 . . . . . . . . . . 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 4453 . . . . . . . . 9  |-  ( ph  ->  A  <  ( B  -  ( 1  /  M ) ) )
9190adantr 466 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  A  <  ( B  -  ( 1  /  M ) ) )
9260, 65elrpd 11345 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  RR+ )
9392adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  M  e.  RR+ )
9434, 55elrpd 11345 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  j  e.  RR+ )
95 1red 9665 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  1  e.  RR )
96 0le1 10144 . . . . . . . . . . 11  |-  0  <_  1
9796a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  0  <_  1 )
9893, 94, 95, 97, 53lediv2ad 11370 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( 1  /  j )  <_ 
( 1  /  M
) )
9957, 68, 32, 98lesub2dd 10237 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( B  -  ( 1  /  M ) )  <_ 
( B  -  (
1  /  j ) ) )
10059, 69, 58, 91, 99ltletrd 9802 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  A  <  ( B  -  ( 1  /  j ) ) )
10194rpreccld 11358 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( 1  /  j )  e.  RR+ )
10232, 101ltsubrpd 11377 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( B  -  ( 1  / 
j ) )  < 
B )
10329, 31, 58, 100, 102eliood 37544 . . . . . 6  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( B  -  ( 1  / 
j ) )  e.  ( A (,) B
) )
10427, 103ffvelrnd 6038 . . . . 5  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( F `  ( B  -  (
1  /  j ) ) )  e.  RR )
105 ioodvbdlimc2lemOLD.s . . . . 5  |-  S  =  ( j  e.  (
ZZ>= `  M )  |->  ( F `  ( B  -  ( 1  / 
j ) ) ) )
106104, 105fmptd 6061 . . . 4  |-  ( ph  ->  S : ( ZZ>= `  M ) --> RR )
107 ioodvbdlimc2lemOLD.dmdv . . . . . 6  |-  ( ph  ->  dom  ( RR  _D  F )  =  ( A (,) B ) )
108 ioodvbdlimc2lemOLD.dvbd . . . . . 6  |-  ( ph  ->  E. y  e.  RR  A. x  e.  ( A (,) B ) ( abs `  ( ( RR  _D  F ) `
 x ) )  <_  y )
1097, 6, 9, 26, 107, 108dvbdfbdioo 37742 . . . . 5  |-  ( ph  ->  E. b  e.  RR  A. x  e.  ( A (,) B ) ( abs `  ( F `
 x ) )  <_  b )
11060adantr 466 . . . . . . . 8  |-  ( (
ph  /\  A. x  e.  ( A (,) B
) ( abs `  ( F `  x )
)  <_  b )  ->  M  e.  RR )
111 simpr 462 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  j  e.  ( ZZ>= `  M )
)
112105fvmpt2 5973 . . . . . . . . . . . . . 14  |-  ( ( j  e.  ( ZZ>= `  M )  /\  ( F `  ( B  -  ( 1  / 
j ) ) )  e.  RR )  -> 
( S `  j
)  =  ( F `
 ( B  -  ( 1  /  j
) ) ) )
113111, 104, 112syl2anc 665 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( S `  j )  =  ( F `  ( B  -  ( 1  / 
j ) ) ) )
114113fveq2d 5885 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( abs `  ( S `  j
) )  =  ( abs `  ( F `
 ( B  -  ( 1  /  j
) ) ) ) )
115114adantlr 719 . . . . . . . . . . 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 760 . . . . . . . . . . . 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 719 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  A. x  e.  ( A (,) B ) ( abs `  ( F `  x
) )  <_  b
)  /\  j  e.  ( ZZ>= `  M )
)  ->  ( B  -  ( 1  / 
j ) )  e.  ( A (,) B
) )
118 fveq2 5881 . . . . . . . . . . . . . . 15  |-  ( x  =  ( B  -  ( 1  /  j
) )  ->  ( F `  x )  =  ( F `  ( B  -  (
1  /  j ) ) ) )
119118fveq2d 5885 . . . . . . . . . . . . . 14  |-  ( x  =  ( B  -  ( 1  /  j
) )  ->  ( abs `  ( F `  x ) )  =  ( abs `  ( F `  ( B  -  ( 1  / 
j ) ) ) ) )
120119breq1d 4433 . . . . . . . . . . . . 13  |-  ( x  =  ( B  -  ( 1  /  j
) )  ->  (
( abs `  ( F `  x )
)  <_  b  <->  ( abs `  ( F `  ( B  -  ( 1  /  j ) ) ) )  <_  b
) )
121120rspccva 3181 . . . . . . . . . . . 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 665 . . . . . . . . . . 11  |-  ( ( ( ph  /\  A. x  e.  ( A (,) B ) ( abs `  ( F `  x
) )  <_  b
)  /\  j  e.  ( ZZ>= `  M )
)  ->  ( abs `  ( F `  ( B  -  ( 1  /  j ) ) ) )  <_  b
)
123115, 122eqbrtrd 4444 . . . . . . . . . 10  |-  ( ( ( ph  /\  A. x  e.  ( A (,) B ) ( abs `  ( F `  x
) )  <_  b
)  /\  j  e.  ( ZZ>= `  M )
)  ->  ( abs `  ( S `  j
) )  <_  b
)
124123a1d 26 . . . . . . . . 9  |-  ( ( ( ph  /\  A. x  e.  ( A (,) B ) ( abs `  ( F `  x
) )  <_  b
)  /\  j  e.  ( ZZ>= `  M )
)  ->  ( M  <_  j  ->  ( abs `  ( S `  j
) )  <_  b
) )
125124ralrimiva 2836 . . . . . . . 8  |-  ( (
ph  /\  A. x  e.  ( A (,) B
) ( abs `  ( F `  x )
)  <_  b )  ->  A. j  e.  (
ZZ>= `  M ) ( M  <_  j  ->  ( abs `  ( S `
 j ) )  <_  b ) )
126 breq1 4426 . . . . . . . . . . 11  |-  ( k  =  M  ->  (
k  <_  j  <->  M  <_  j ) )
127126imbi1d 318 . . . . . . . . . 10  |-  ( k  =  M  ->  (
( k  <_  j  ->  ( abs `  ( S `  j )
)  <_  b )  <->  ( M  <_  j  ->  ( abs `  ( S `
 j ) )  <_  b ) ) )
128127ralbidv 2861 . . . . . . . . 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 3182 . . . . . . . 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 665 . . . . . . 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 435 . . . . . 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 2896 . . . . 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, 133limsupreOLD 37662 . . 3  |-  ( ph  ->  ( limsup `  S )  e.  RR )
135134recnd 9676 . 2  |-  ( ph  ->  ( limsup `  S )  e.  CC )
136 eluzelre 11176 . . . . . . . . 9  |-  ( j  e.  ( ZZ>= `  N
)  ->  j  e.  RR )
137136adantl 467 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  j  e.  RR )
138 0red 9651 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  0  e.  RR )
13945peano2zd 11050 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( |_ `  ( 1  /  ( B  -  A )
) )  +  1 )  e.  ZZ )
1405, 139syl5eqel 2511 . . . . . . . . . . . . 13  |-  ( ph  ->  M  e.  ZZ )
141140adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  M  e.  ZZ )
142141zred 11047 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  M  e.  RR )
143142adantr 466 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  M  e.  RR )
14465ad2antrr 730 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  0  <  M )
145 ioodvbdlimc2lemOLD.n . . . . . . . . . . . . . 14  |-  N  =  if ( M  <_ 
( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 ) ,  ( ( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) ,  M )
146 ioodvbdlimc2lemOLD.y . . . . . . . . . . . . . . . . . . . 20  |-  Y  =  sup ( ran  (
x  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `
 x ) ) ) ,  RR ,  <  )
147 ioomidp 37564 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  (
( A  +  B
)  /  2 )  e.  ( A (,) B ) )
1487, 6, 9, 147syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( A  +  B )  /  2
)  e.  ( A (,) B ) )
149 ne0i 3767 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( A  +  B
)  /  2 )  e.  ( A (,) B )  ->  ( A (,) B )  =/=  (/) )
150148, 149syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( A (,) B
)  =/=  (/) )
151 ioossre 11703 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( A (,) B )  C_  RR
152151a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( A (,) B
)  C_  RR )
153 dvfre 22903 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( F : ( A (,) B ) --> RR 
/\  ( A (,) B )  C_  RR )  ->  ( RR  _D  F ) : dom  ( RR  _D  F
) --> RR )
15426, 152, 153syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( RR  _D  F
) : dom  ( RR  _D  F ) --> RR )
155107feq2d 5733 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( RR  _D  F ) : dom  ( RR  _D  F
) --> RR  <->  ( RR  _D  F ) : ( A (,) B ) --> RR ) )
156154, 155mpbid 213 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( RR  _D  F
) : ( A (,) B ) --> RR )
157156ffvelrnda 6037 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( ( RR  _D  F ) `  x )  e.  RR )
158157recnd 9676 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( ( RR  _D  F ) `  x )  e.  CC )
159158abscld 13497 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( abs `  ( ( RR  _D  F ) `  x
) )  e.  RR )
160 eqid 2422 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `  x
) ) )  =  ( x  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  x )
) )
161 eqid 2422 . . . . . . . . . . . . . . . . . . . . . 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 37399 . . . . . . . . . . . . . . . . . . . . 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 460 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  sup ( ran  (
x  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `
 x ) ) ) ,  RR ,  <  )  e.  RR )
164146, 163syl5eqel 2511 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  Y  e.  RR )
165164adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR+ )  ->  Y  e.  RR )
166 rpre 11315 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR+  ->  x  e.  RR )
167166rehalfcld 10866 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  RR+  ->  ( x  /  2 )  e.  RR )
168167adantl 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( x  /  2 )  e.  RR )
169166recnd 9676 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR+  ->  x  e.  CC )
170169adantl 467 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  e.  CC )
171 2cnd 10689 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR+ )  ->  2  e.  CC )
172 rpne0 11324 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR+  ->  x  =/=  0 )
173172adantl 467 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  =/=  0 )
174 2ne0 10709 . . . . . . . . . . . . . . . . . . . 20  |-  2  =/=  0
175174a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR+ )  ->  2  =/=  0 )
176170, 171, 173, 175divne0d 10406 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( x  /  2 )  =/=  0 )
177165, 168, 176redivcld 10442 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( Y  /  ( x  / 
2 ) )  e.  RR )
178177flcld 12040 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( |_ `  ( Y  /  (
x  /  2 ) ) )  e.  ZZ )
179178peano2zd 11050 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( |_ `  ( Y  / 
( x  /  2
) ) )  +  1 )  e.  ZZ )
180179, 141ifcld 3954 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  if ( M  <_  ( ( |_
`  ( Y  / 
( x  /  2
) ) )  +  1 ) ,  ( ( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) ,  M )  e.  ZZ )
181145, 180syl5eqel 2511 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  N  e.  ZZ )
182181zred 11047 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  N  e.  RR )
183182adantr 466 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  N  e.  RR )
184179zred 11047 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( |_ `  ( Y  / 
( x  /  2
) ) )  +  1 )  e.  RR )
185 max1 11487 . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  M  <_  if ( M  <_  (
( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) ,  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 ) ,  M ) )
187186, 145syl6breqr 4464 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  M  <_  N )
188187adantr 466 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  M  <_  N )
189 eluzle 11178 . . . . . . . . . . . 12  |-  ( j  e.  ( ZZ>= `  N
)  ->  N  <_  j )
190189adantl 467 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  N  <_  j )
191143, 183, 137, 188, 190letrd 9799 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  M  <_  j )
192138, 143, 137, 144, 191ltletrd 9802 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  0  <  j )
193192gt0ne0d 10185 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  j  =/=  0 )
194137, 193rereccld 10441 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  ( 1  /  j )  e.  RR )
195137, 192recgt0d 10548 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  0  <  ( 1  /  j ) )
196194, 195elrpd 11345 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  ( 1  /  j )  e.  RR+ )
197196adantr 466 . . . . 5  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N ) )  /\  ( abs `  ( ( S `  j )  -  ( limsup `  S
) ) )  < 
( x  /  2
) )  ->  (
1  /  j )  e.  RR+ )
198 ioodvbdlimc2lemOLD.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 197 . . . . . . . . . . . . . . . . 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 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 ) )  ->  ph )
201199, 200syl 17 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ph )
202201, 26syl 17 . . . . . . . . . . . . . . 15  |-  ( ch 
->  F : ( A (,) B ) --> RR )
203199simplrd 761 . . . . . . . . . . . . . . 15  |-  ( ch 
->  z  e.  ( A (,) B ) )
204202, 203ffvelrnd 6038 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( F `  z
)  e.  RR )
205204recnd 9676 . . . . . . . . . . . . 13  |-  ( ch 
->  ( F `  z
)  e.  CC )
206201, 106syl 17 . . . . . . . . . . . . . . 15  |-  ( ch 
->  S : ( ZZ>= `  M ) --> RR )
207 simp-5r 777 . . . . . . . . . . . . . . . . . . 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 11172 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  N  e.  ZZ  /\  M  <_  N ) )
210141, 181, 187, 209syl3anbrc 1189 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR+ )  ->  N  e.  ( ZZ>= `  M )
)
211201, 208, 210syl2anc 665 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  N  e.  ( ZZ>=
`  M ) )
212 uzss 11186 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( ZZ>= `  N )  C_  ( ZZ>=
`  M ) )
213211, 212syl 17 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( ZZ>= `  N )  C_  ( ZZ>= `  M )
)
214 simp-4r 775 . . . . . . . . . . . . . . . . 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 3465 . . . . . . . . . . . . . . 15  |-  ( ch 
->  j  e.  ( ZZ>=
`  M ) )
217206, 216ffvelrnd 6038 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( S `  j
)  e.  RR )
218217recnd 9676 . . . . . . . . . . . . 13  |-  ( ch 
->  ( S `  j
)  e.  CC )
219201, 135syl 17 . . . . . . . . . . . . 13  |-  ( ch 
->  ( limsup `  S )  e.  CC )
220205, 218, 219npncand 10017 . . . . . . . . . . . 12  |-  ( ch 
->  ( ( ( F `
 z )  -  ( S `  j ) )  +  ( ( S `  j )  -  ( limsup `  S
) ) )  =  ( ( F `  z )  -  ( limsup `
 S ) ) )
221220eqcomd 2430 . . . . . . . . . . 11  |-  ( ch 
->  ( ( F `  z )  -  ( limsup `
 S ) )  =  ( ( ( F `  z )  -  ( S `  j ) )  +  ( ( S `  j )  -  ( limsup `
 S ) ) ) )
222221fveq2d 5885 . . . . . . . . . 10  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( limsup `  S ) ) )  =  ( abs `  (
( ( F `  z )  -  ( S `  j )
)  +  ( ( S `  j )  -  ( limsup `  S
) ) ) ) )
223204, 217resubcld 10054 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( ( F `  z )  -  ( S `  j )
)  e.  RR )
224201, 134syl 17 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( limsup `  S )  e.  RR )
225217, 224resubcld 10054 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( ( S `  j )  -  ( limsup `
 S ) )  e.  RR )
226223, 225readdcld 9677 . . . . . . . . . . . . 13  |-  ( ch 
->  ( ( ( F `
 z )  -  ( S `  j ) )  +  ( ( S `  j )  -  ( limsup `  S
) ) )  e.  RR )
227226recnd 9676 . . . . . . . . . . . 12  |-  ( ch 
->  ( ( ( F `
 z )  -  ( S `  j ) )  +  ( ( S `  j )  -  ( limsup `  S
) ) )  e.  CC )
228227abscld 13497 . . . . . . . . . . 11  |-  ( ch 
->  ( abs `  (
( ( F `  z )  -  ( S `  j )
)  +  ( ( S `  j )  -  ( limsup `  S
) ) ) )  e.  RR )
229223recnd 9676 . . . . . . . . . . . . 13  |-  ( ch 
->  ( ( F `  z )  -  ( S `  j )
)  e.  CC )
230229abscld 13497 . . . . . . . . . . . 12  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( S `
 j ) ) )  e.  RR )
231225recnd 9676 . . . . . . . . . . . . 13  |-  ( ch 
->  ( ( S `  j )  -  ( limsup `
 S ) )  e.  CC )
232231abscld 13497 . . . . . . . . . . . 12  |-  ( ch 
->  ( abs `  (
( S `  j
)  -  ( limsup `  S ) ) )  e.  RR )
233230, 232readdcld 9677 . . . . . . . . . . 11  |-  ( ch 
->  ( ( abs `  (
( F `  z
)  -  ( S `
 j ) ) )  +  ( abs `  ( ( S `  j )  -  ( limsup `
 S ) ) ) )  e.  RR )
234208rpred 11348 . . . . . . . . . . 11  |-  ( ch 
->  x  e.  RR )
235229, 231abstrid 13517 . . . . . . . . . . 11  |-  ( ch 
->  ( abs `  (
( ( F `  z )  -  ( S `  j )
)  +  ( ( S `  j )  -  ( limsup `  S
) ) ) )  <_  ( ( abs `  ( ( F `  z )  -  ( S `  j )
) )  +  ( abs `  ( ( S `  j )  -  ( limsup `  S
) ) ) ) )
236234rehalfcld 10866 . . . . . . . . . . . . 13  |-  ( ch 
->  ( x  /  2
)  e.  RR )
237201, 216, 113syl2anc 665 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( S `  j
)  =  ( F `
 ( B  -  ( 1  /  j
) ) ) )
238237oveq2d 6321 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( ( F `  z )  -  ( S `  j )
)  =  ( ( F `  z )  -  ( F `  ( B  -  (
1  /  j ) ) ) ) )
239238fveq2d 5885 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( S `
 j ) ) )  =  ( abs `  ( ( F `  z )  -  ( F `  ( B  -  ( 1  / 
j ) ) ) ) ) )
240239, 230eqeltrrd 2508 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( F `
 ( B  -  ( 1  /  j
) ) ) ) )  e.  RR )
241201, 164syl 17 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  Y  e.  RR )
242151, 203sseldi 3462 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  z  e.  RR )
243201, 216, 58syl2anc 665 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( B  -  (
1  /  j ) )  e.  RR )
244242, 243resubcld 10054 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( z  -  ( B  -  ( 1  /  j ) ) )  e.  RR )
245241, 244remulcld 9678 . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . . . . . . . . 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 4431 . . . . . . . . . . . . . . . . . . . . 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 2853 . . . . . . . . . . . . . . . . . . . 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 215 . . . . . . . . . . . . . . . . . . 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 5881 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  =  x  ->  (
( RR  _D  F
) `  w )  =  ( ( RR 
_D  F ) `  x ) )
255254fveq2d 5885 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  x  ->  ( abs `  ( ( RR 
_D  F ) `  w ) )  =  ( abs `  (
( RR  _D  F
) `  x )
) )
256255breq1d 4433 . . . . . . . . . . . . . . . . . . 19  |-  ( w  =  x  ->  (
( abs `  (
( RR  _D  F
) `  w )
)  <_  Y  <->  ( abs `  ( ( RR  _D  F ) `  x
) )  <_  Y
) )
257256cbvralv 3054 . . . . . . . . . . . . . . . . . 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 215 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  A. w  e.  ( A (,) B ) ( abs `  (
( RR  _D  F
) `  w )
)  <_  Y )
259201, 216, 103syl2anc 665 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( B  -  (
1  /  j ) )  e.  ( A (,) B ) )
260243rexrd 9697 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( B  -  (
1  /  j ) )  e.  RR* )
261201, 30syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  B  e.  RR* )
2623, 216sseldi 3462 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  j  e.  RR )
263201, 216, 56syl2anc 665 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  j  =/=  0
)
264262, 263rereccld 10441 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( 1  /  j
)  e.  RR )
265247, 242resubcld 10054 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( B  -  z
)  e.  RR )
266242, 247resubcld 10054 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( z  -  B
)  e.  RR )
267266recnd 9676 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( z  -  B
)  e.  CC )
268267abscld 13497 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( abs `  (
z  -  B ) )  e.  RR )
269265leabsd 13476 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( B  -  z
)  <_  ( abs `  ( B  -  z
) ) )
270201, 85syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  B  e.  CC )
271242recnd 9676 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  z  e.  CC )
272270, 271abssubd 13514 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( abs `  ( B  -  z )
)  =  ( abs `  ( z  -  B
) ) )
273269, 272breqtrd 4448 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( B  -  z
)  <_  ( abs `  ( z  -  B
) ) )
274199simprd 464 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( abs `  (
z  -  B ) )  <  ( 1  /  j ) )
275265, 268, 264, 273, 274lelttrd 9800 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( B  -  z
)  <  ( 1  /  j ) )
276247, 242, 264, 275ltsub23d 10225 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( B  -  (
1  /  j ) )  <  z )
277201, 28syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  A  e.  RR* )
278 iooltub 37559 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  z  e.  ( A (,) B
) )  ->  z  <  B )
279277, 261, 203, 278syl3anc 1264 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  z  <  B )
280260, 261, 242, 276, 279eliood 37544 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  z  e.  (
( B  -  (
1  /  j ) ) (,) B ) )
281246, 247, 202, 248, 241, 258, 259, 280dvbdfbdioolem1 37740 . . . . . . . . . . . . . . . 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 460 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( F `
 ( B  -  ( 1  /  j
) ) ) ) )  <_  ( Y  x.  ( z  -  ( B  -  ( 1  /  j ) ) ) ) )
283201, 216, 57syl2anc 665 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( 1  /  j
)  e.  RR )
284241, 283remulcld 9678 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( Y  x.  (
1  /  j ) )  e.  RR )
285156, 148ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( RR  _D  F ) `  (
( A  +  B
)  /  2 ) )  e.  RR )
286285recnd 9676 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( RR  _D  F ) `  (
( A  +  B
)  /  2 ) )  e.  CC )
287286abscld 13497 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( abs `  (
( RR  _D  F
) `  ( ( A  +  B )  /  2 ) ) )  e.  RR )
288286absge0d 13505 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  0  <_  ( abs `  ( ( RR  _D  F ) `  (
( A  +  B
)  /  2 ) ) ) )
289 fveq2 5881 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  ( ( A  +  B )  / 
2 )  ->  (
( RR  _D  F
) `  x )  =  ( ( RR 
_D  F ) `  ( ( A  +  B )  /  2
) ) )
290289fveq2d 5885 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  ( ( A  +  B )  / 
2 )  ->  ( abs `  ( ( RR 
_D  F ) `  x ) )  =  ( abs `  (
( RR  _D  F
) `  ( ( A  +  B )  /  2 ) ) ) )
291146eqcomi 2435 . . . . . . . . . . . . . . . . . . . . . . 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 4436 . . . . . . . . . . . . . . . . . . . . 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 3180 . . . . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( abs `  (
( RR  _D  F
) `  ( ( A  +  B )  /  2 ) ) )  <_  Y )
29614, 287, 164, 288, 295letrd 9799 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  0  <_  Y )
297201, 296syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  0  <_  Y )
298283recnd 9676 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( 1  /  j
)  e.  CC )
299 sub31 37458 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( z  e.  CC  /\  B  e.  CC  /\  (
1  /  j )  e.  CC )  -> 
( z  -  ( B  -  ( 1  /  j ) ) )  =  ( ( 1  /  j )  -  ( B  -  z ) ) )
300271, 270, 298, 299syl3anc 1264 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( z  -  ( B  -  ( 1  /  j ) ) )  =  ( ( 1  /  j )  -  ( B  -  z ) ) )
301242, 247posdifd 10207 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( z  <  B  <->  0  <  ( B  -  z ) ) )
302279, 301mpbid 213 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  0  <  ( B  -  z ) )
303265, 302elrpd 11345 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( B  -  z
)  e.  RR+ )
304283, 303ltsubrpd 11377 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( ( 1  / 
j )  -  ( B  -  z )
)  <  ( 1  /  j ) )
305300, 304eqbrtrd 4444 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( z  -  ( B  -  ( 1  /  j ) ) )  <  ( 1  /  j ) )
306244, 283, 305ltled 9790 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( z  -  ( B  -  ( 1  /  j ) ) )  <_  ( 1  /  j ) )
307244, 283, 241, 297, 306lemul2ad 10554 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( Y  x.  (
z  -  ( B  -  ( 1  / 
j ) ) ) )  <_  ( Y  x.  ( 1  /  j
) ) )
308284adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  Y  =  0 )  ->  ( Y  x.  ( 1  /  j ) )  e.  RR )
309236adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  Y  =  0 )  ->  (
x  /  2 )  e.  RR )
310 oveq1 6312 . . . . . . . . . . . . . . . . . . . 20  |-  ( Y  =  0  ->  ( Y  x.  ( 1  /  j ) )  =  ( 0  x.  ( 1  /  j
) ) )
311298mul02d 9838 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( 0  x.  (
1  /  j ) )  =  0 )
312310, 311sylan9eqr 2485 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  Y  =  0 )  ->  ( Y  x.  ( 1  /  j ) )  =  0 )
313208rphalfcld 11360 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( x  /  2
)  e.  RR+ )
314313rpgt0d 11351 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  0  <  ( x  /  2 ) )
315314adantr 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  Y  =  0 )  ->  0  <  ( x  /  2
) )
316312, 315eqbrtrd 4444 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  Y  =  0 )  ->  ( Y  x.  ( 1  /  j ) )  <  ( x  / 
2 ) )
317308, 309, 316ltled 9790 . . . . . . . . . . . . . . . . 17  |-  ( ( ch  /\  Y  =  0 )  ->  ( Y  x.  ( 1  /  j ) )  <_  ( x  / 
2 ) )
318241adantr 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  -.  Y  =  0 )  ->  Y  e.  RR )
319297adantr 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  -.  Y  =  0 )  -> 
0  <_  Y )
320 neqne 37347 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  Y  =  0  ->  Y  =/=  0 )
321320adantl 467 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  -.  Y  =  0 )  ->  Y  =/=  0 )
322318, 319, 321ne0gt0d 9779 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  -.  Y  =  0 )  -> 
0  <  Y )
323284adantr 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  j ) )  e.  RR )
3243, 211sseldi 3462 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  N  e.  RR )
325 0red 9651 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  0  e.  RR )
326201, 208, 142syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  M  e.  RR )
327201, 65syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  0  <  M )
328201, 208, 187syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  M  <_  N )
329325, 326, 324, 327, 328ltletrd 9802 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  0  <  N )
330329gt0ne0d 10185 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  N  =/=  0
)
331324, 330rereccld 10441 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( 1  /  N
)  e.  RR )
332241, 331remulcld 9678 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( Y  x.  (
1  /  N ) )  e.  RR )
333332adantr 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  N ) )  e.  RR )
334236adantr 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  0  < 
Y )  ->  (
x  /  2 )  e.  RR )
335283adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  0  < 
Y )  ->  (
1  /  j )  e.  RR )
336331adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  0  < 
Y )  ->  (
1  /  N )  e.  RR )
337241adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  0  < 
Y )  ->  Y  e.  RR )
338297adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  0  < 
Y )  ->  0  <_  Y )
339324, 329elrpd 11345 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  N  e.  RR+ )
340201, 216, 94syl2anc 665 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  j  e.  RR+ )
341 1red 9665 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  1  e.  RR )
34296a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  0  <_  1 )
343215, 189syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  N  <_  j )
344339, 340, 341, 342, 343lediv2ad 11370 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( 1  /  j
)  <_  ( 1  /  N ) )
345344adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  0  < 
Y )  ->  (
1  /  j )  <_  ( 1  /  N ) )
346335, 336, 337, 338, 345lemul2ad 10554 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  j ) )  <_  ( Y  x.  ( 1  /  N
) ) )
347234recnd 9676 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  x  e.  CC )
348 2cnd 10689 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  2  e.  CC )
349208rpne0d 11353 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  x  =/=  0
)
350174a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  2  =/=  0
)
351347, 348, 349, 350divne0d 10406 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ch 
->  ( x  /  2
)  =/=  0 )
352241, 236, 351redivcld 10442 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  ( Y  /  (
x  /  2 ) )  e.  RR )
353352adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( x  / 
2 ) )  e.  RR )
354 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ch  /\  0  < 
Y )  ->  0  <  Y )
355314adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ch  /\  0  < 
Y )  ->  0  <  ( x  /  2
) )
356337, 334, 354, 355divgt0d 10549 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  0  < 
Y )  ->  0  <  ( Y  /  (
x  /  2 ) ) )
357353, 356elrpd 11345 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( x  / 
2 ) )  e.  RR+ )
358357rprecred 11359 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  0  < 
Y )  ->  (
1  /  ( Y  /  ( x  / 
2 ) ) )  e.  RR )
359339adantr 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  N  e.  RR+ )
360 1red 9665 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  1  e.  RR )
36196a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  0  <_  1 )
362352flcld 12040 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ch 
->  ( |_ `  ( Y  /  ( x  / 
2 ) ) )  e.  ZZ )
363362peano2zd 11050 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 )  e.  ZZ )
364363zred 11047 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ch 
->  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 )  e.  RR )
365201, 140syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ch 
->  M  e.  ZZ )
366363, 365ifcld 3954 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ch 
->  if ( M  <_ 
( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 ) ,  ( ( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) ,  M )  e.  ZZ )
367145, 366syl5eqel 2511 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  N  e.  ZZ )
368367zred 11047 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ch 
->  N  e.  RR )
369 flltp1 12042 . . . . . . . . . . . . . . . . . . . . . . . . . 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 11489 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 )  <_  if ( M  <_  ( ( |_
`  ( Y  / 
( x  /  2
) ) )  +  1 ) ,  ( ( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) ,  M ) )
374373, 145syl6breqr 4464 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ch 
->  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 )  <_  N )
375352, 364, 368, 370, 374ltletrd 9802 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  ( Y  /  (
x  /  2 ) )  <  N )
376352, 324, 375ltled 9790 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  ( Y  /  (
x  /  2 ) )  <_  N )
377376adantr 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( x  / 
2 ) )  <_  N )
378357, 359, 360, 361, 377lediv2ad 11370 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  0  < 
Y )  ->  (
1  /  N )  <_  ( 1  / 
( Y  /  (
x  /  2 ) ) ) )
379336, 358, 337, 338, 378lemul2ad 10554 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  N ) )  <_  ( Y  x.  ( 1  /  ( Y  /  ( x  / 
2 ) ) ) ) )
380337recnd 9676 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  Y  e.  CC )
381353recnd 9676 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( x  / 
2 ) )  e.  CC )
382356gt0ne0d 10185 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( x  / 
2 ) )  =/=  0 )
383380, 381, 382divrecd 10393 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( Y  / 
( x  /  2
) ) )  =  ( Y  x.  (
1  /  ( Y  /  ( x  / 
2 ) ) ) ) )
384334recnd 9676 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  (
x  /  2 )  e.  CC )
385354gt0ne0d 10185 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  Y  =/=  0 )
386351adantr 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  (
x  /  2 )  =/=  0 )
387380, 384, 385, 386ddcand 10410 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( Y  / 
( x  /  2
) ) )  =  ( x  /  2
) )
388383, 387eqtr3d 2465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  ( Y  / 
( x  /  2
) ) ) )  =  ( x  / 
2 ) )
389379, 388breqtrd 4448 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  N ) )  <_  ( x  / 
2 ) )
390323, 333, 334, 346, 389letrd 9799 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  j ) )  <_  ( x  / 
2 ) )
391322, 390syldan 472 . . . . . . . . . . . . . . . . 17  |-  ( ( ch  /\  -.  Y  =  0 )  -> 
( Y  x.  (
1  /  j ) )  <_  ( x  /  2 ) )
392317, 391pm2.61dan 798 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( Y  x.  (
1  /  j ) )  <_  ( x  /  2 ) )
393245, 284, 236, 307, 392letrd 9799 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( Y  x.  (
z  -  ( B  -  ( 1  / 
j ) ) ) )  <_  ( x  /  2 ) )
394240, 245, 236, 282, 393letrd 9799 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( F `
 ( B  -  ( 1  /  j
) ) ) ) )  <_  ( x  /  2 ) )
395239, 394eqbrtrd 4444 . . . . . . . . . . . . 13  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( S `
 j ) ) )  <_  ( x  /  2 ) )
396 simpllr 767 . . . . . . . . . . . . . 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 10242 . . . . . . . . . . . 12  |-  ( ch 
->  ( ( abs `  (
( F `  z
)  -  ( S `
 j ) ) )  +  ( abs `  ( ( S `  j )  -  ( limsup `
 S ) ) ) )  <  (
( x  /  2
)  +  ( x  /  2 ) ) )
3993472halvesd 10865 . . . . . . . . . . . 12  |-  ( ch 
->  ( ( x  / 
2 )  +  ( x  /  2 ) )  =  x )
400398, 399breqtrd 4448 . . . . . . . . . . 11  |-  ( ch 
->  ( ( abs `  (
( F `  z
)  -  ( S `
 j ) ) )  +  ( abs `  ( ( S `  j )  -  ( limsup `
 S ) ) ) )  <  x
)
401228, 233, 234, 235, 400lelttrd 9800 . . . . . . . . . 10  |-  ( ch 
->  ( abs `  (
( ( F `  z )  -  ( S `  j )
)  +  ( ( S `  j )  -  ( limsup `  S
) ) ) )  <  x )
402222, 401eqbrtrd 4444 . . . . . . . . 9  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( limsup `  S ) ) )  <  x )
403198, 402sylbir 216 . . . . . . . 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 720 . . . . . . 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 435 . . . . . 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 2836 . . . . 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 4427 . . . . . . . . 9  |-  ( y  =  ( 1  / 
j )  ->  (
( abs `  (
z  -  B ) )  <  y  <->  ( abs `  ( z  -  B
) )  <  (
1  /  j ) ) )
408407anbi2d 708 . . . . . . . 8  |-  ( y  =  ( 1  / 
j )  ->  (
( z  =/=  B  /\  ( abs `  (
z  -  B ) )  <  y )  <-> 
( z  =/=  B  /\  ( abs `  (
z  -  B ) )  <  ( 1  /  j ) ) ) )
409408imbi1d 318 . . . . . . 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 2861 . . . . . 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 3182 . . . . 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 665 . . . 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 462 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  <_  N )  ->  b  <_  N )
414413iftrued 3919 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  <_  N )  ->  if ( b  <_  N ,  N ,  b )  =  N )
415 uzid 11180 . . . . . . . . . . . 12  |-  ( N  e.  ZZ  ->  N  e.  ( ZZ>= `  N )
)
416181, 415syl 17 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  N  e.  ( ZZ>= `  N )
)
417416adantr 466 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  <_  N )  ->  N  e.  ( ZZ>= `  N )
)
418414, 417eqeltrd 2507 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  <_  N )  ->  if ( b  <_  N ,  N ,  b )  e.  ( ZZ>= `  N
) )
419418adantlr 719 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  b  <_  N )  ->  if ( b  <_  N ,  N ,  b )  e.  ( ZZ>= `  N )
)
420 iffalse 3920 . . . . . . . . . 10  |-  ( -.  b  <_  N  ->  if ( b  <_  N ,  N ,  b )  =  b )
421420adantl 467 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  if (
b  <_  N ,  N ,  b )  =  b )
422181ad2antrr 730 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  N  e.  ZZ )
423 simplr 760 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  b  e.  ZZ )
424422zred 11047 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  N  e.  RR )
425423zred 11047 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  b  e.  RR )
426 simpr 462 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  -.  b  <_  N )
427424, 425ltnled 9789 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  ( N  <  b  <->  -.  b  <_  N ) )
428426, 427mpbird 235 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  N  <  b )
429424, 425, 428ltled 9790 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  N  <_  b )
430 eluz2 11172 . . . . . . . . . 10  |-  ( b  e.  ( ZZ>= `  N
)  <->  ( N  e.  ZZ  /\  b  e.  ZZ  /\  N  <_ 
b ) )
431422, 423, 429, 430syl3anbrc 1189 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  b  e.  ( ZZ>= `  N )
)
432421, 431eqeltrd 2507 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  /\  -.  b  <_  N
)  ->  if (
b  <_  N ,  N ,  b )  e.  ( ZZ>= `  N )
)
433419, 432pm2.61dan 798 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  ->  if ( b  <_  N ,  N ,  b )  e.  ( ZZ>= `  N
) )
434433adantr 466 . . . . . 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 462 . . . . . . . 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 462 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  ->  b  e.  ZZ )
437181adantr 466 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  ->  N  e.  ZZ )
438437, 436ifcld 3954 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  ->  if ( b  <_  N ,  N ,  b )  e.  ZZ )
439436zred 11047 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  ->  b  e.  RR )
440437zred 11047 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  ->  N  e.  RR )
441 max1 11487 . . . . . . . . . . 11  |-  ( ( b  e.  RR  /\  N  e.  RR )  ->  b  <_  if (
b  <_  N ,  N ,  b )
)
442439, 440, 441syl2anc 665 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  ->  b  <_  if ( b  <_  N ,  N , 
b ) )
443 eluz2 11172 . . . . . . . . . 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 1189 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  b  e.  ZZ )  ->  if ( b  <_  N ,  N ,  b )  e.  ( ZZ>= `  b
) )
445444adantr 466 . . . . . . . 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 5881 . . . . . . . . . . 11  |-  ( c  =  if ( b  <_  N ,  N ,  b )  -> 
( S `  c
)  =  ( S `
 if ( b  <_  N ,  N ,  b ) ) )
447446eleq1d 2491 . . . . . . . . . 10  |-  ( c  =  if ( b  <_  N ,  N ,  b )  -> 
( ( S `  c )  e.  CC  <->  ( S `  if ( b  <_  N ,  N ,  b )
)  e.  CC ) )
448446oveq1d 6320 . . . . . . . . . . . 12  |-  ( c  =  if ( b  <_  N ,  N ,  b )  -> 
( ( S `  c )  -  ( limsup `
 S ) )  =  ( ( S `
 if ( b  <_  N ,  N ,  b ) )  -  ( limsup `  S
) ) )
449448fveq2d 5885 . . . . . . . . . . 11  |-  ( c  =  if ( b  <_  N ,  N ,  b )  -> 
( abs `  (
( S `  c
)  -  ( limsup `  S ) ) )  =  ( abs `  (
( S `  if ( b  <_  N ,  N ,  b ) )  -  ( limsup `  S ) ) ) )
450449breq1d 4433 . . . . . . . . . 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 715 . . . . . . . . 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 3181 . . . . . . . 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 665 . . . . . . 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 464 . . . . . 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 5881 . . . . . . . . . 10  |-  ( j  =  if ( b  <_  N ,  N ,  b )  -> 
( S `  j
)  =  ( S `
 if ( b  <_  N ,  N ,  b ) ) )
456455oveq1d 6320 . . . . . . . . 9  |-  ( j  =  if ( b  <_  N ,  N ,  b )  -> 
( ( S `  j )  -  ( limsup `
 S ) )  =  ( ( S `
 if ( b  <_  N ,  N ,  b ) )  -  ( limsup `  S
) ) )
457456fveq2d 5885 . . . . . . . 8  |-  ( j  =  if ( b  <_  N ,  N ,  b )  -> 
( abs `  (
( S `  j
)  -  ( limsup `  S ) ) )  =  ( abs `  (
( S `  if ( b  <_  N ,  N ,  b ) )  -  ( limsup `  S ) ) ) )
458457breq1d 4433 . . . . . . 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 3182 . . . . . 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 665 . . . . 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 9603 . . . . . . . . . . . . . 14  |-  RR  C_  CC
462461a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  RR  C_  CC )
46326, 462fssd 5755 . . . . . . . . . . . . . 14  |-  ( ph  ->  F : ( A (,) B ) --> CC )
464 dvcn 22873 . . . . . . . . . . . . . 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 1267 . . . . . . . . . . . . 13  |-  ( ph  ->  F  e.  ( ( A (,) B )
-cn-> CC ) )
466 cncffvrn 21928 . . . . . . . . . . . . 13  |-  ( ( RR  C_  CC  /\  F  e.  ( ( A (,) B ) -cn-> CC ) )  ->  ( F  e.  ( ( A (,) B ) -cn-> RR )  <-> 
F : ( A (,) B ) --> RR ) )
467462, 465, 466syl2anc 665 . . . . . . . . . . . 12  |-  ( ph  ->  ( F  e.  ( ( A (,) B
) -cn-> RR )  <->  F :
( A (,) B
) --> RR ) )
46826, 467mpbird 235 . . . . . . . . . . 11  |-  ( ph  ->  F  e.  ( ( A (,) B )
-cn-> RR ) )
469 ioodvbdlimc2lemOLD.r . . . . . . . . . . . 12  |-  R  =  ( j  e.  (
ZZ>= `  M )  |->  ( B  -  ( 1  /  j ) ) )
470103, 469fmptd 6061 . . . . . . . . . . 11  |-  ( ph  ->  R : ( ZZ>= `  M ) --> ( A (,) B ) )
471 eqid 2422 . . . . . . . . . . 11  |-  ( j  e.  ( ZZ>= `  M
)  |->  ( F `  ( R `  j ) ) )  =  ( j  e.  ( ZZ>= `  M )  |->  ( F `
 ( R `  j ) ) )
472 climrel 13555 . . . . . . . . . . . . 13  |-  Rel  ~~>
473472a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  Rel  ~~>  )
474 fvex 5891 . . . . . . . . . . . . . . . . 17  |-  ( ZZ>= `  M )  e.  _V
475474mptex 6151 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( ZZ>= `  M
)  |->  B )  e. 
_V
476475a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( j  e.  (
ZZ>= `  M )  |->  B )  e.  _V )
477 eqidd 2423 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( ZZ>= `  M )
)  ->  ( j  e.  ( ZZ>= `  M )  |->  B )  =  ( j  e.  ( ZZ>= `  M )  |->  B ) )
478 eqidd 2423 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  M )
)  /\  j  =  m )  ->  B  =  B )
479 simpr 462 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( ZZ>= `  M )
)  ->  m  e.  ( ZZ>= `  M )
)
4806adantr 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( ZZ>= `  M )
)  ->  B  e.  RR )
481477, 478, 479, 480fvmptd 5970 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( ZZ>= `  M )
)  ->  ( (
j  e.  ( ZZ>= `  M )  |->  B ) `
 m )  =  B )
48223, 22, 476, 85, 481climconst 13606 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( j  e.  (
ZZ>= `  M )  |->  B )  ~~>  B )
483474mptex 6151 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( ZZ>= `  M
)  |->  ( B  -  ( 1  /  j
) ) )  e. 
_V
484469, 483eqeltri 2503 . . . . . . . . . . . . . . 15  |-  R  e. 
_V
485484a1i 11 . . . . . . . . . . . . . 14  |-  ( ph  ->  R  e.  _V )
486 1cnd 9666 . . . . . . . . . . . . . . 15  |-  ( ph  ->  1  e.  CC )
487 elnnnn0b 10921 . . . . . . . . . . . . . . . 16  |-  ( M  e.  NN  <->  ( M  e.  NN0  /\  0  < 
M ) )
48821, 65, 487sylanbrc 668 . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  e.  NN )
489 divcnvg 37647 . . . . . . . . . . . . . . 15  |-  ( ( 1  e.  CC  /\  M  e.  NN )  ->  ( j  e.  (
ZZ>= `  M )  |->  ( 1  /  j ) )  ~~>  0 )
490486, 488, 489syl2anc 665 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( j  e.  (
ZZ>= `  M )  |->  ( 1  /  j ) )  ~~>  0 )
491 eqidd 2423 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( j  e.  ( ZZ>= `  M )  |->  B )  =  ( j  e.  ( ZZ>= `  M )  |->  B ) )
492 eqidd 2423 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( ZZ>= `  M )
)  /\  j  =  i )  ->  B  =  B )
493 simpr 462 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  e.  ( ZZ>= `  M )
)
4946adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  B  e.  RR )
495491, 492, 493, 494fvmptd 5970 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( (
j  e.  ( ZZ>= `  M )  |->  B ) `
 i )  =  B )
496495, 494eqeltrd 2507 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( (
j  e.  ( ZZ>= `  M )  |->  B ) `
 i )  e.  RR )
497496recnd 9676 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( (
j  e.  ( ZZ>= `  M )  |->  B ) `
 i )  e.  CC )
498 eqidd 2423 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( j  e.  ( ZZ>= `  M )  |->  ( 1  /  j
) )  =  ( j  e.  ( ZZ>= `  M )  |->  ( 1  /  j ) ) )
499 oveq2 6313 . . . . . . . . . . . . . . . . 17  |-  ( j  =  i  ->  (
1  /  j )  =  ( 1  / 
i ) )
500499adantl 467 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( ZZ>= `  M )
)  /\  j  =  i )  ->  (
1  /  j )  =  ( 1  / 
i ) )
5013, 493sseldi 3462 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  e.  RR )
502 0red 9651 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  0  e.  RR )
50360adantr 466 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  M  e.  RR )
50465adantr 466 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  0  <  M )
505 eluzle 11178 . . . . . . . . . . . . . . . . . . . 20  |-  ( i  e.  ( ZZ>= `  M
)  ->  M  <_  i )
506505adantl 467 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  M  <_  i )
507502, 503, 501, 504, 506ltletrd 9802 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  0  <  i )
508507gt0ne0d 10185 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  =/=  0 )
509501, 508rereccld 10441 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( 1  /  i )  e.  RR )
510498, 500, 493, 509fvmptd 5970 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( (
j  e.  ( ZZ>= `  M )  |->  ( 1  /  j ) ) `
 i )  =  ( 1  /  i
) )
511501recnd 9676 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  e.  CC )
512511, 508reccld 10383 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( 1  /  i )  e.  CC )
513510, 512eqeltrd 2507 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( (
j  e.  ( ZZ>= `  M )  |->  ( 1  /  j ) ) `
 i )  e.  CC )
514499oveq2d 6321 . . . . . . . . . . . . . . . . 17  |-  ( j  =  i  ->  ( B  -  ( 1  /  j ) )  =  ( B  -  ( 1  /  i
) ) )
515 ovex 6333 . . . . . . . . . . . . . . . . 17  |-  ( B  -  ( 1  / 
i ) )  e. 
_V
516514, 469, 515fvmpt 5964 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( ZZ>= `  M
)  ->  ( R `  i )  =  ( B  -  ( 1  /  i ) ) )
517516adantl 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( R `  i )  =  ( B  -  ( 1  /  i ) ) )
518495, 510oveq12d 6323 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( (
( j  e.  (
ZZ>= `  M )  |->  B ) `  i )  -  ( ( j  e.  ( ZZ>= `  M
)  |->  ( 1  / 
j ) ) `  i ) )  =  ( B  -  (
1  /  i ) ) )
519517, 518eqtr4d 2466 . . . . . . . . . . . . . 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 13696 . . . . . . . . . . . . 13  |-  ( ph  ->  R  ~~>  ( B  - 
0 ) )
52185subid1d 9982 . . . . . . . . . . . . 13  |-  ( ph  ->  ( B  -  0 )  =  B )<