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

Theorem ioodvbdlimc1lem2OLD 37746
Description: Limit at the lower bound of an open interval, for a function with bounded derivative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) Obsolete version of ioodvbdlimc1lem2 37744 as of 3-Oct-2020. (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
ioodvbdlimc1lem2OLD.a  |-  ( ph  ->  A  e.  RR )
ioodvbdlimc1lem2OLD.b  |-  ( ph  ->  B  e.  RR )
ioodvbdlimc1lem2OLD.altb  |-  ( ph  ->  A  <  B )
ioodvbdlimc1lem2OLD.f  |-  ( ph  ->  F : ( A (,) B ) --> RR )
ioodvbdlimc1lem2OLD.dmdv  |-  ( ph  ->  dom  ( RR  _D  F )  =  ( A (,) B ) )
ioodvbdlimc1lem2OLD.dvbd  |-  ( ph  ->  E. y  e.  RR  A. x  e.  ( A (,) B ) ( abs `  ( ( RR  _D  F ) `
 x ) )  <_  y )
ioodvbdlimc1lem2OLD.y  |-  Y  =  sup ( ran  (
x  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `
 x ) ) ) ,  RR ,  <  )
ioodvbdlimc1lem2OLD.m  |-  M  =  ( ( |_ `  ( 1  /  ( B  -  A )
) )  +  1 )
ioodvbdlimc1lem2OLD.s  |-  S  =  ( j  e.  (
ZZ>= `  M )  |->  ( F `  ( A  +  ( 1  / 
j ) ) ) )
ioodvbdlimc1lem2OLD.r  |-  R  =  ( j  e.  (
ZZ>= `  M )  |->  ( A  +  ( 1  /  j ) ) )
ioodvbdlimc1lem2OLD.n  |-  N  =  if ( M  <_ 
( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 ) ,  ( ( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) ,  M )
ioodvbdlimc1lem2OLD.ch  |-  ( ch  <->  ( ( ( ( (
ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  /\  ( abs `  ( ( S `  j )  -  ( limsup `
 S ) ) )  <  ( x  /  2 ) )  /\  z  e.  ( A (,) B ) )  /\  ( abs `  ( z  -  A
) )  <  (
1  /  j ) ) )
Assertion
Ref Expression
ioodvbdlimc1lem2OLD  |-  ( ph  ->  ( limsup `  S )  e.  ( F lim CC  A
) )
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 ioodvbdlimc1lem2OLD
Dummy variables  b 
k  h  i  l  m  w  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 ioodvbdlimc1lem2OLD.m . . . . . . 7  |-  M  =  ( ( |_ `  ( 1  /  ( B  -  A )
) )  +  1 )
6 ioodvbdlimc1lem2OLD.b . . . . . . . . . . 11  |-  ( ph  ->  B  e.  RR )
7 ioodvbdlimc1lem2OLD.a . . . . . . . . . . 11  |-  ( ph  ->  A  e.  RR )
86, 7resubcld 10054 . . . . . . . . . 10  |-  ( ph  ->  ( B  -  A
)  e.  RR )
9 ioodvbdlimc1lem2OLD.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 ioodvbdlimc1lem2OLD.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* )
327adantr 466 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  A  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, 57readdcld 9677 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( A  +  ( 1  / 
j ) )  e.  RR )
5934, 55elrpd 11345 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  j  e.  RR+ )
6059rpreccld 11358 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( 1  /  j )  e.  RR+ )
6132, 60ltaddrpd 11378 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  A  <  ( A  +  ( 1  /  j ) ) )
6221nn0red 10933 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  RR )
6314, 47readdcld 9677 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0  +  1 )  e.  RR )
6446, 47readdcld 9677 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( |_ `  ( 1  /  ( B  -  A )
) )  +  1 )  e.  RR )
6514ltp1d 10544 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <  ( 0  +  1 ) )
6614, 63, 64, 65, 49ltletrd 9802 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <  ( ( |_ `  ( 1  /  ( B  -  A ) ) )  +  1 ) )
6766, 5syl6breqr 4464 . . . . . . . . . . . 12  |-  ( ph  ->  0  <  M )
6867gt0ne0d 10185 . . . . . . . . . . 11  |-  ( ph  ->  M  =/=  0 )
6962, 68rereccld 10441 . . . . . . . . . 10  |-  ( ph  ->  ( 1  /  M
)  e.  RR )
7069adantr 466 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( 1  /  M )  e.  RR )
7132, 70readdcld 9677 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( A  +  ( 1  /  M ) )  e.  RR )
726adantr 466 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  B  e.  RR )
7362, 67elrpd 11345 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  RR+ )
7473adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  M  e.  RR+ )
75 1red 9665 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  1  e.  RR )
76 0le1 10144 . . . . . . . . . . 11  |-  0  <_  1
7776a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  0  <_  1 )
7874, 59, 75, 77, 53lediv2ad 11370 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( 1  /  j )  <_ 
( 1  /  M
) )
7957, 70, 32, 78leadd2dd 10235 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( A  +  ( 1  / 
j ) )  <_ 
( A  +  ( 1  /  M ) ) )
805eqcomi 2435 . . . . . . . . . . . . 13  |-  ( ( |_ `  ( 1  /  ( B  -  A ) ) )  +  1 )  =  M
8180oveq2i 6316 . . . . . . . . . . . 12  |-  ( 1  /  ( ( |_
`  ( 1  / 
( B  -  A
) ) )  +  1 ) )  =  ( 1  /  M
)
8281, 69syl5eqel 2511 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  /  (
( |_ `  (
1  /  ( B  -  A ) ) )  +  1 ) )  e.  RR )
8313, 15elrpd 11345 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1  /  ( B  -  A )
)  e.  RR+ )
8464, 66elrpd 11345 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( |_ `  ( 1  /  ( B  -  A )
) )  +  1 )  e.  RR+ )
85 1rp 11313 . . . . . . . . . . . . . 14  |-  1  e.  RR+
8685a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  1  e.  RR+ )
87 fllelt 12039 . . . . . . . . . . . . . . 15  |-  ( ( 1  /  ( B  -  A ) )  e.  RR  ->  (
( |_ `  (
1  /  ( B  -  A ) ) )  <_  ( 1  /  ( B  -  A ) )  /\  ( 1  /  ( B  -  A )
)  <  ( ( |_ `  ( 1  / 
( B  -  A
) ) )  +  1 ) ) )
8813, 87syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( |_ `  ( 1  /  ( B  -  A )
) )  <_  (
1  /  ( B  -  A ) )  /\  ( 1  / 
( B  -  A
) )  <  (
( |_ `  (
1  /  ( B  -  A ) ) )  +  1 ) ) )
8988simprd 464 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1  /  ( B  -  A )
)  <  ( ( |_ `  ( 1  / 
( B  -  A
) ) )  +  1 ) )
9083, 84, 86, 89ltdiv2dd 37463 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  /  (
( |_ `  (
1  /  ( B  -  A ) ) )  +  1 ) )  <  ( 1  /  ( 1  / 
( B  -  A
) ) ) )
918recnd 9676 . . . . . . . . . . . . 13  |-  ( ph  ->  ( B  -  A
)  e.  CC )
9291, 12recrecd 10387 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  /  (
1  /  ( B  -  A ) ) )  =  ( B  -  A ) )
9390, 92breqtrd 4448 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  /  (
( |_ `  (
1  /  ( B  -  A ) ) )  +  1 ) )  <  ( B  -  A ) )
9482, 8, 7, 93ltadd2dd 9801 . . . . . . . . . 10  |-  ( ph  ->  ( A  +  ( 1  /  ( ( |_ `  ( 1  /  ( B  -  A ) ) )  +  1 ) ) )  <  ( A  +  ( B  -  A ) ) )
955oveq2i 6316 . . . . . . . . . . . 12  |-  ( 1  /  M )  =  ( 1  /  (
( |_ `  (
1  /  ( B  -  A ) ) )  +  1 ) )
9695oveq2i 6316 . . . . . . . . . . 11  |-  ( A  +  ( 1  /  M ) )  =  ( A  +  ( 1  /  ( ( |_ `  ( 1  /  ( B  -  A ) ) )  +  1 ) ) )
9796a1i 11 . . . . . . . . . 10  |-  ( ph  ->  ( A  +  ( 1  /  M ) )  =  ( A  +  ( 1  / 
( ( |_ `  ( 1  /  ( B  -  A )
) )  +  1 ) ) ) )
987recnd 9676 . . . . . . . . . . . 12  |-  ( ph  ->  A  e.  CC )
996recnd 9676 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  CC )
10098, 99pncan3d 9996 . . . . . . . . . . 11  |-  ( ph  ->  ( A  +  ( B  -  A ) )  =  B )
101100eqcomd 2430 . . . . . . . . . 10  |-  ( ph  ->  B  =  ( A  +  ( B  -  A ) ) )
10294, 97, 1013brtr4d 4454 . . . . . . . . 9  |-  ( ph  ->  ( A  +  ( 1  /  M ) )  <  B )
103102adantr 466 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( A  +  ( 1  /  M ) )  < 
B )
10458, 71, 72, 79, 103lelttrd 9800 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( A  +  ( 1  / 
j ) )  < 
B )
10529, 31, 58, 61, 104eliood 37544 . . . . . 6  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( A  +  ( 1  / 
j ) )  e.  ( A (,) B
) )
10627, 105ffvelrnd 6038 . . . . 5  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( F `  ( A  +  ( 1  /  j ) ) )  e.  RR )
107 ioodvbdlimc1lem2OLD.s . . . . 5  |-  S  =  ( j  e.  (
ZZ>= `  M )  |->  ( F `  ( A  +  ( 1  / 
j ) ) ) )
108106, 107fmptd 6061 . . . 4  |-  ( ph  ->  S : ( ZZ>= `  M ) --> RR )
109 ioodvbdlimc1lem2OLD.dmdv . . . . . 6  |-  ( ph  ->  dom  ( RR  _D  F )  =  ( A (,) B ) )
110 ioodvbdlimc1lem2OLD.dvbd . . . . . 6  |-  ( ph  ->  E. y  e.  RR  A. x  e.  ( A (,) B ) ( abs `  ( ( RR  _D  F ) `
 x ) )  <_  y )
1117, 6, 9, 26, 109, 110dvbdfbdioo 37742 . . . . 5  |-  ( ph  ->  E. b  e.  RR  A. x  e.  ( A (,) B ) ( abs `  ( F `
 x ) )  <_  b )
11262adantr 466 . . . . . . . 8  |-  ( (
ph  /\  A. x  e.  ( A (,) B
) ( abs `  ( F `  x )
)  <_  b )  ->  M  e.  RR )
113 simpr 462 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  j  e.  ( ZZ>= `  M )
)
114107fvmpt2 5973 . . . . . . . . . . . . . 14  |-  ( ( j  e.  ( ZZ>= `  M )  /\  ( F `  ( A  +  ( 1  / 
j ) ) )  e.  RR )  -> 
( S `  j
)  =  ( F `
 ( A  +  ( 1  /  j
) ) ) )
115113, 106, 114syl2anc 665 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( S `  j )  =  ( F `  ( A  +  ( 1  / 
j ) ) ) )
116115fveq2d 5885 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( ZZ>= `  M )
)  ->  ( abs `  ( S `  j
) )  =  ( abs `  ( F `
 ( A  +  ( 1  /  j
) ) ) ) )
117116adantlr 719 . . . . . . . . . . 11  |-  ( ( ( ph  /\  A. x  e.  ( A (,) B ) ( abs `  ( F `  x
) )  <_  b
)  /\  j  e.  ( ZZ>= `  M )
)  ->  ( abs `  ( S `  j
) )  =  ( abs `  ( F `
 ( A  +  ( 1  /  j
) ) ) ) )
118 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 )
119105adantlr 719 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  A. x  e.  ( A (,) B ) ( abs `  ( F `  x
) )  <_  b
)  /\  j  e.  ( ZZ>= `  M )
)  ->  ( A  +  ( 1  / 
j ) )  e.  ( A (,) B
) )
120 fveq2 5881 . . . . . . . . . . . . . . 15  |-  ( x  =  ( A  +  ( 1  /  j
) )  ->  ( F `  x )  =  ( F `  ( A  +  (
1  /  j ) ) ) )
121120fveq2d 5885 . . . . . . . . . . . . . 14  |-  ( x  =  ( A  +  ( 1  /  j
) )  ->  ( abs `  ( F `  x ) )  =  ( abs `  ( F `  ( A  +  ( 1  / 
j ) ) ) ) )
122121breq1d 4433 . . . . . . . . . . . . 13  |-  ( x  =  ( A  +  ( 1  /  j
) )  ->  (
( abs `  ( F `  x )
)  <_  b  <->  ( abs `  ( F `  ( A  +  ( 1  /  j ) ) ) )  <_  b
) )
123122rspccva 3181 . . . . . . . . . . . 12  |-  ( ( A. x  e.  ( A (,) B ) ( abs `  ( F `  x )
)  <_  b  /\  ( A  +  (
1  /  j ) )  e.  ( A (,) B ) )  ->  ( abs `  ( F `  ( A  +  ( 1  / 
j ) ) ) )  <_  b )
124118, 119, 123syl2anc 665 . . . . . . . . . . 11  |-  ( ( ( ph  /\  A. x  e.  ( A (,) B ) ( abs `  ( F `  x
) )  <_  b
)  /\  j  e.  ( ZZ>= `  M )
)  ->  ( abs `  ( F `  ( A  +  ( 1  /  j ) ) ) )  <_  b
)
125117, 124eqbrtrd 4444 . . . . . . . . . 10  |-  ( ( ( ph  /\  A. x  e.  ( A (,) B ) ( abs `  ( F `  x
) )  <_  b
)  /\  j  e.  ( ZZ>= `  M )
)  ->  ( abs `  ( S `  j
) )  <_  b
)
126125a1d 26 . . . . . . . . 9  |-  ( ( ( ph  /\  A. x  e.  ( A (,) B ) ( abs `  ( F `  x
) )  <_  b
)  /\  j  e.  ( ZZ>= `  M )
)  ->  ( M  <_  j  ->  ( abs `  ( S `  j
) )  <_  b
) )
127126ralrimiva 2836 . . . . . . . 8  |-  ( (
ph  /\  A. x  e.  ( A (,) B
) ( abs `  ( F `  x )
)  <_  b )  ->  A. j  e.  (
ZZ>= `  M ) ( M  <_  j  ->  ( abs `  ( S `
 j ) )  <_  b ) )
128 breq1 4426 . . . . . . . . . . 11  |-  ( k  =  M  ->  (
k  <_  j  <->  M  <_  j ) )
129128imbi1d 318 . . . . . . . . . 10  |-  ( k  =  M  ->  (
( k  <_  j  ->  ( abs `  ( S `  j )
)  <_  b )  <->  ( M  <_  j  ->  ( abs `  ( S `
 j ) )  <_  b ) ) )
130129ralbidv 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 )
) )
131130rspcev 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 ) )
132112, 127, 131syl2anc 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 ) )
133132ex 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 ) ) )
134133reximdv 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 )
) )
135111, 134mpd 15 . . . 4  |-  ( ph  ->  E. b  e.  RR  E. k  e.  RR  A. j  e.  ( ZZ>= `  M ) ( k  <_  j  ->  ( abs `  ( S `  j ) )  <_ 
b ) )
1364, 25, 108, 135limsupreOLD 37662 . . 3  |-  ( ph  ->  ( limsup `  S )  e.  RR )
137136recnd 9676 . 2  |-  ( ph  ->  ( limsup `  S )  e.  CC )
138 eluzelre 11176 . . . . . . . . 9  |-  ( j  e.  ( ZZ>= `  N
)  ->  j  e.  RR )
139138adantl 467 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  j  e.  RR )
140 0red 9651 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  0  e.  RR )
14145peano2zd 11050 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( |_ `  ( 1  /  ( B  -  A )
) )  +  1 )  e.  ZZ )
1425, 141syl5eqel 2511 . . . . . . . . . . . . 13  |-  ( ph  ->  M  e.  ZZ )
143142adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  M  e.  ZZ )
144143zred 11047 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  M  e.  RR )
145144adantr 466 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  M  e.  RR )
14667ad2antrr 730 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  0  <  M )
147 ioodvbdlimc1lem2OLD.n . . . . . . . . . . . . . 14  |-  N  =  if ( M  <_ 
( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 ) ,  ( ( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) ,  M )
148 ioodvbdlimc1lem2OLD.y . . . . . . . . . . . . . . . . . . . 20  |-  Y  =  sup ( ran  (
x  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `
 x ) ) ) ,  RR ,  <  )
149 ioomidp 37564 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B )  ->  (
( A  +  B
)  /  2 )  e.  ( A (,) B ) )
1507, 6, 9, 149syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( A  +  B )  /  2
)  e.  ( A (,) B ) )
151 ne0i 3767 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( A  +  B
)  /  2 )  e.  ( A (,) B )  ->  ( A (,) B )  =/=  (/) )
152150, 151syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( A (,) B
)  =/=  (/) )
153 ioossre 11703 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( A (,) B )  C_  RR
154153a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( A (,) B
)  C_  RR )
155 dvfre 22903 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( F : ( A (,) B ) --> RR 
/\  ( A (,) B )  C_  RR )  ->  ( RR  _D  F ) : dom  ( RR  _D  F
) --> RR )
15626, 154, 155syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( RR  _D  F
) : dom  ( RR  _D  F ) --> RR )
157109feq2d 5733 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( RR  _D  F ) : dom  ( RR  _D  F
) --> RR  <->  ( RR  _D  F ) : ( A (,) B ) --> RR ) )
158156, 157mpbid 213 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( RR  _D  F
) : ( A (,) B ) --> RR )
159158ffvelrnda 6037 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( ( RR  _D  F ) `  x )  e.  RR )
160159recnd 9676 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( ( RR  _D  F ) `  x )  e.  CC )
161160abscld 13497 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( A (,) B ) )  ->  ( abs `  ( ( RR  _D  F ) `  x
) )  e.  RR )
162 eqid 2422 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `  x
) ) )  =  ( x  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  x )
) )
163 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 ,  <  )
164152, 161, 110, 162, 163suprnmpt 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 ,  <  ) ) )
165164simpld 460 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  sup ( ran  (
x  e.  ( A (,) B )  |->  ( abs `  ( ( RR  _D  F ) `
 x ) ) ) ,  RR ,  <  )  e.  RR )
166148, 165syl5eqel 2511 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  Y  e.  RR )
167166adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR+ )  ->  Y  e.  RR )
168 rpre 11315 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR+  ->  x  e.  RR )
169168rehalfcld 10866 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  RR+  ->  ( x  /  2 )  e.  RR )
170169adantl 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( x  /  2 )  e.  RR )
171168recnd 9676 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR+  ->  x  e.  CC )
172171adantl 467 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  e.  CC )
173 2cnd 10689 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR+ )  ->  2  e.  CC )
174 rpne0 11324 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  RR+  ->  x  =/=  0 )
175174adantl 467 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  =/=  0 )
176 2ne0 10709 . . . . . . . . . . . . . . . . . . . 20  |-  2  =/=  0
177176a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  RR+ )  ->  2  =/=  0 )
178172, 173, 175, 177divne0d 10406 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( x  /  2 )  =/=  0 )
179167, 170, 178redivcld 10442 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( Y  /  ( x  / 
2 ) )  e.  RR )
180179flcld 12040 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( |_ `  ( Y  /  (
x  /  2 ) ) )  e.  ZZ )
181180peano2zd 11050 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( |_ `  ( Y  / 
( x  /  2
) ) )  +  1 )  e.  ZZ )
182181, 143ifcld 3954 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  if ( M  <_  ( ( |_
`  ( Y  / 
( x  /  2
) ) )  +  1 ) ,  ( ( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) ,  M )  e.  ZZ )
183147, 182syl5eqel 2511 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  N  e.  ZZ )
184183zred 11047 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  N  e.  RR )
185184adantr 466 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  N  e.  RR )
186181zred 11047 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( |_ `  ( Y  / 
( x  /  2
) ) )  +  1 )  e.  RR )
187 max1 11487 . . . . . . . . . . . . . 14  |-  ( ( M  e.  RR  /\  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 )  e.  RR )  ->  M  <_  if ( M  <_  ( ( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) ,  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 ) ,  M ) )
188144, 186, 187syl2anc 665 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  M  <_  if ( M  <_  (
( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) ,  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 ) ,  M ) )
189188, 147syl6breqr 4464 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  M  <_  N )
190189adantr 466 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  M  <_  N )
191 eluzle 11178 . . . . . . . . . . . 12  |-  ( j  e.  ( ZZ>= `  N
)  ->  N  <_  j )
192191adantl 467 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  N  <_  j )
193145, 185, 139, 190, 192letrd 9799 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  M  <_  j )
194140, 145, 139, 146, 193ltletrd 9802 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  0  <  j )
195194gt0ne0d 10185 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  j  =/=  0 )
196139, 195rereccld 10441 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  ( 1  /  j )  e.  RR )
197139, 194recgt0d 10548 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  0  <  ( 1  /  j ) )
198196, 197elrpd 11345 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  ->  ( 1  /  j )  e.  RR+ )
199198adantr 466 . . . . 5  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N ) )  /\  ( abs `  ( ( S `  j )  -  ( limsup `  S
) ) )  < 
( x  /  2
) )  ->  (
1  /  j )  e.  RR+ )
200 ioodvbdlimc1lem2OLD.ch . . . . . . . . 9  |-  ( ch  <->  ( ( ( ( (
ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  /\  ( abs `  ( ( S `  j )  -  ( limsup `
 S ) ) )  <  ( x  /  2 ) )  /\  z  e.  ( A (,) B ) )  /\  ( abs `  ( z  -  A
) )  <  (
1  /  j ) ) )
201200biimpi 197 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  /\  ( abs `  ( ( S `  j )  -  ( limsup `
 S ) ) )  <  ( x  /  2 ) )  /\  z  e.  ( A (,) B ) )  /\  ( abs `  ( z  -  A
) )  <  (
1  /  j ) ) )
202 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  -  A
) )  <  (
1  /  j ) )  ->  ph )
203201, 202syl 17 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ph )
204203, 26syl 17 . . . . . . . . . . . . . . 15  |-  ( ch 
->  F : ( A (,) B ) --> RR )
205201simplrd 761 . . . . . . . . . . . . . . 15  |-  ( ch 
->  z  e.  ( A (,) B ) )
206204, 205ffvelrnd 6038 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( F `  z
)  e.  RR )
207206recnd 9676 . . . . . . . . . . . . 13  |-  ( ch 
->  ( F `  z
)  e.  CC )
208203, 108syl 17 . . . . . . . . . . . . . . 15  |-  ( ch 
->  S : ( ZZ>= `  M ) --> RR )
209 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  -  A
) )  <  (
1  /  j ) )  ->  x  e.  RR+ )
210201, 209syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  x  e.  RR+ )
211 eluz2 11172 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  N  e.  ZZ  /\  M  <_  N ) )
212143, 183, 189, 211syl3anbrc 1189 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  RR+ )  ->  N  e.  ( ZZ>= `  M )
)
213203, 210, 212syl2anc 665 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  N  e.  ( ZZ>=
`  M ) )
214 uzss 11186 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( ZZ>= `  N )  C_  ( ZZ>=
`  M ) )
215213, 214syl 17 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( ZZ>= `  N )  C_  ( ZZ>= `  M )
)
216 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  -  A
) )  <  (
1  /  j ) )  ->  j  e.  ( ZZ>= `  N )
)
217201, 216syl 17 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  j  e.  ( ZZ>=
`  N ) )
218215, 217sseldd 3465 . . . . . . . . . . . . . . 15  |-  ( ch 
->  j  e.  ( ZZ>=
`  M ) )
219208, 218ffvelrnd 6038 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( S `  j
)  e.  RR )
220219recnd 9676 . . . . . . . . . . . . 13  |-  ( ch 
->  ( S `  j
)  e.  CC )
221203, 137syl 17 . . . . . . . . . . . . 13  |-  ( ch 
->  ( limsup `  S )  e.  CC )
222207, 220, 221npncand 10017 . . . . . . . . . . . 12  |-  ( ch 
->  ( ( ( F `
 z )  -  ( S `  j ) )  +  ( ( S `  j )  -  ( limsup `  S
) ) )  =  ( ( F `  z )  -  ( limsup `
 S ) ) )
223222eqcomd 2430 . . . . . . . . . . 11  |-  ( ch 
->  ( ( F `  z )  -  ( limsup `
 S ) )  =  ( ( ( F `  z )  -  ( S `  j ) )  +  ( ( S `  j )  -  ( limsup `
 S ) ) ) )
224223fveq2d 5885 . . . . . . . . . 10  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( limsup `  S ) ) )  =  ( abs `  (
( ( F `  z )  -  ( S `  j )
)  +  ( ( S `  j )  -  ( limsup `  S
) ) ) ) )
225206, 219resubcld 10054 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( ( F `  z )  -  ( S `  j )
)  e.  RR )
226203, 136syl 17 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( limsup `  S )  e.  RR )
227219, 226resubcld 10054 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( ( S `  j )  -  ( limsup `
 S ) )  e.  RR )
228225, 227readdcld 9677 . . . . . . . . . . . . 13  |-  ( ch 
->  ( ( ( F `
 z )  -  ( S `  j ) )  +  ( ( S `  j )  -  ( limsup `  S
) ) )  e.  RR )
229228recnd 9676 . . . . . . . . . . . 12  |-  ( ch 
->  ( ( ( F `
 z )  -  ( S `  j ) )  +  ( ( S `  j )  -  ( limsup `  S
) ) )  e.  CC )
230229abscld 13497 . . . . . . . . . . 11  |-  ( ch 
->  ( abs `  (
( ( F `  z )  -  ( S `  j )
)  +  ( ( S `  j )  -  ( limsup `  S
) ) ) )  e.  RR )
231225recnd 9676 . . . . . . . . . . . . 13  |-  ( ch 
->  ( ( F `  z )  -  ( S `  j )
)  e.  CC )
232231abscld 13497 . . . . . . . . . . . 12  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( S `
 j ) ) )  e.  RR )
233227recnd 9676 . . . . . . . . . . . . 13  |-  ( ch 
->  ( ( S `  j )  -  ( limsup `
 S ) )  e.  CC )
234233abscld 13497 . . . . . . . . . . . 12  |-  ( ch 
->  ( abs `  (
( S `  j
)  -  ( limsup `  S ) ) )  e.  RR )
235232, 234readdcld 9677 . . . . . . . . . . 11  |-  ( ch 
->  ( ( abs `  (
( F `  z
)  -  ( S `
 j ) ) )  +  ( abs `  ( ( S `  j )  -  ( limsup `
 S ) ) ) )  e.  RR )
236210rpred 11348 . . . . . . . . . . 11  |-  ( ch 
->  x  e.  RR )
237231, 233abstrid 13517 . . . . . . . . . . 11  |-  ( ch 
->  ( abs `  (
( ( F `  z )  -  ( S `  j )
)  +  ( ( S `  j )  -  ( limsup `  S
) ) ) )  <_  ( ( abs `  ( ( F `  z )  -  ( S `  j )
) )  +  ( abs `  ( ( S `  j )  -  ( limsup `  S
) ) ) ) )
238236rehalfcld 10866 . . . . . . . . . . . . 13  |-  ( ch 
->  ( x  /  2
)  e.  RR )
239207, 220abssubd 13514 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( S `
 j ) ) )  =  ( abs `  ( ( S `  j )  -  ( F `  z )
) ) )
240203, 218, 115syl2anc 665 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( S `  j
)  =  ( F `
 ( A  +  ( 1  /  j
) ) ) )
241240oveq1d 6320 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( ( S `  j )  -  ( F `  z )
)  =  ( ( F `  ( A  +  ( 1  / 
j ) ) )  -  ( F `  z ) ) )
242241fveq2d 5885 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( abs `  (
( S `  j
)  -  ( F `
 z ) ) )  =  ( abs `  ( ( F `  ( A  +  (
1  /  j ) ) )  -  ( F `  z )
) ) )
243203, 218, 106syl2anc 665 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( F `  ( A  +  ( 1  /  j ) ) )  e.  RR )
244243, 206resubcld 10054 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( ( F `  ( A  +  (
1  /  j ) ) )  -  ( F `  z )
)  e.  RR )
245244recnd 9676 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( ( F `  ( A  +  (
1  /  j ) ) )  -  ( F `  z )
)  e.  CC )
246245abscld 13497 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( abs `  (
( F `  ( A  +  ( 1  /  j ) ) )  -  ( F `
 z ) ) )  e.  RR )
247203, 166syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  Y  e.  RR )
248203, 218, 58syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( A  +  ( 1  /  j ) )  e.  RR )
249153, 205sseldi 3462 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  z  e.  RR )
250248, 249resubcld 10054 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( ( A  +  ( 1  /  j
) )  -  z
)  e.  RR )
251247, 250remulcld 9678 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( Y  x.  (
( A  +  ( 1  /  j ) )  -  z ) )  e.  RR )
252203, 7syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  A  e.  RR )
253203, 6syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  B  e.  RR )
254203, 109syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  dom  ( RR  _D  F )  =  ( A (,) B ) )
255164simprd 464 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  A. x  e.  ( A (,) B ) ( abs `  (
( RR  _D  F
) `  x )
)  <_  sup ( ran  ( x  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  x )
) ) ,  RR ,  <  ) )
256148breq2i 4431 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( abs `  ( ( RR  _D  F ) `
 x ) )  <_  Y  <->  ( abs `  ( ( RR  _D  F ) `  x
) )  <_  sup ( ran  ( x  e.  ( A (,) B
)  |->  ( abs `  (
( RR  _D  F
) `  x )
) ) ,  RR ,  <  ) )
257256ralbii 2853 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ,  <  ) )
258255, 257sylibr 215 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  A. x  e.  ( A (,) B ) ( abs `  (
( RR  _D  F
) `  x )
)  <_  Y )
259203, 258syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  A. x  e.  ( A (,) B ) ( abs `  (
( RR  _D  F
) `  x )
)  <_  Y )
260 fveq2 5881 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  =  x  ->  (
( RR  _D  F
) `  w )  =  ( ( RR 
_D  F ) `  x ) )
261260fveq2d 5885 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  =  x  ->  ( abs `  ( ( RR 
_D  F ) `  w ) )  =  ( abs `  (
( RR  _D  F
) `  x )
) )
262261breq1d 4433 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  x  ->  (
( abs `  (
( RR  _D  F
) `  w )
)  <_  Y  <->  ( abs `  ( ( RR  _D  F ) `  x
) )  <_  Y
) )
263262cbvralv 3054 . . . . . . . . . . . . . . . . . . 19  |-  ( A. w  e.  ( A (,) B ) ( abs `  ( ( RR  _D  F ) `  w
) )  <_  Y  <->  A. x  e.  ( A (,) B ) ( abs `  ( ( RR  _D  F ) `
 x ) )  <_  Y )
264259, 263sylibr 215 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  A. w  e.  ( A (,) B ) ( abs `  (
( RR  _D  F
) `  w )
)  <_  Y )
265249rexrd 9697 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  z  e.  RR* )
266203, 30syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  B  e.  RR* )
267249, 252resubcld 10054 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( z  -  A
)  e.  RR )
268267recnd 9676 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( z  -  A
)  e.  CC )
269268abscld 13497 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( abs `  (
z  -  A ) )  e.  RR )
2703, 218sseldi 3462 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  j  e.  RR )
271203, 218, 56syl2anc 665 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  j  =/=  0
)
272270, 271rereccld 10441 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( 1  /  j
)  e.  RR )
273267leabsd 13476 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( z  -  A
)  <_  ( abs `  ( z  -  A
) ) )
274201simprd 464 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( abs `  (
z  -  A ) )  <  ( 1  /  j ) )
275267, 269, 272, 273, 274lelttrd 9800 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( z  -  A
)  <  ( 1  /  j ) )
276249, 252, 272ltsubadd2d 10218 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( ( z  -  A )  <  (
1  /  j )  <-> 
z  <  ( A  +  ( 1  / 
j ) ) ) )
277275, 276mpbid 213 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  z  <  ( A  +  ( 1  / 
j ) ) )
278203, 218, 104syl2anc 665 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( A  +  ( 1  /  j ) )  <  B )
279265, 266, 248, 277, 278eliood 37544 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( A  +  ( 1  /  j ) )  e.  ( z (,) B ) )
280252, 253, 204, 254, 247, 264, 205, 279dvbdfbdioolem1 37740 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( ( abs `  (
( F `  ( A  +  ( 1  /  j ) ) )  -  ( F `
 z ) ) )  <_  ( Y  x.  ( ( A  +  ( 1  /  j
) )  -  z
) )  /\  ( abs `  ( ( F `
 ( A  +  ( 1  /  j
) ) )  -  ( F `  z ) ) )  <_  ( Y  x.  ( B  -  A ) ) ) )
281280simpld 460 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( abs `  (
( F `  ( A  +  ( 1  /  j ) ) )  -  ( F `
 z ) ) )  <_  ( Y  x.  ( ( A  +  ( 1  /  j
) )  -  z
) ) )
282203, 218, 57syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( 1  /  j
)  e.  RR )
283247, 282remulcld 9678 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( Y  x.  (
1  /  j ) )  e.  RR )
284158, 150ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( RR  _D  F ) `  (
( A  +  B
)  /  2 ) )  e.  RR )
285284recnd 9676 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( RR  _D  F ) `  (
( A  +  B
)  /  2 ) )  e.  CC )
286285abscld 13497 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( abs `  (
( RR  _D  F
) `  ( ( A  +  B )  /  2 ) ) )  e.  RR )
287285absge0d 13505 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  0  <_  ( abs `  ( ( RR  _D  F ) `  (
( A  +  B
)  /  2 ) ) ) )
288 fveq2 5881 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  ( ( A  +  B )  / 
2 )  ->  (
( RR  _D  F
) `  x )  =  ( ( RR 
_D  F ) `  ( ( A  +  B )  /  2
) ) )
289288fveq2d 5885 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  ( ( A  +  B )  / 
2 )  ->  ( abs `  ( ( RR 
_D  F ) `  x ) )  =  ( abs `  (
( RR  _D  F
) `  ( ( A  +  B )  /  2 ) ) ) )
290148eqcomi 2435 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  sup ( ran  ( x  e.  ( A (,) B ) 
|->  ( abs `  (
( RR  _D  F
) `  x )
) ) ,  RR ,  <  )  =  Y
291290a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  ( ( A  +  B )  / 
2 )  ->  sup ( ran  ( x  e.  ( A (,) B
)  |->  ( abs `  (
( RR  _D  F
) `  x )
) ) ,  RR ,  <  )  =  Y )
292289, 291breq12d 4436 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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
) )
293292rspcva 3180 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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 )
294150, 255, 293syl2anc 665 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( abs `  (
( RR  _D  F
) `  ( ( A  +  B )  /  2 ) ) )  <_  Y )
29514, 286, 166, 287, 294letrd 9799 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  0  <_  Y )
296203, 295syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  0  <_  Y )
297203, 28syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  A  e.  RR* )
298 ioogtlb 37541 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  e.  RR*  /\  B  e.  RR*  /\  z  e.  ( A (,) B
) )  ->  A  <  z )
299297, 266, 205, 298syl3anc 1264 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  A  <  z )
300252, 249, 248, 299ltsub2dd 10233 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( ( A  +  ( 1  /  j
) )  -  z
)  <  ( ( A  +  ( 1  /  j ) )  -  A ) )
301203, 98syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  A  e.  CC )
302282recnd 9676 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( 1  /  j
)  e.  CC )
303301, 302pncan2d 9995 . . . . . . . . . . . . . . . . . . . 20  |-  ( ch 
->  ( ( A  +  ( 1  /  j
) )  -  A
)  =  ( 1  /  j ) )
304300, 303breqtrd 4448 . . . . . . . . . . . . . . . . . . 19  |-  ( ch 
->  ( ( A  +  ( 1  /  j
) )  -  z
)  <  ( 1  /  j ) )
305250, 272, 304ltled 9790 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  ( ( A  +  ( 1  /  j
) )  -  z
)  <_  ( 1  /  j ) )
306250, 272, 247, 296, 305lemul2ad 10554 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( Y  x.  (
( A  +  ( 1  /  j ) )  -  z ) )  <_  ( Y  x.  ( 1  /  j
) ) )
307283adantr 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  Y  =  0 )  ->  ( Y  x.  ( 1  /  j ) )  e.  RR )
308238adantr 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  Y  =  0 )  ->  (
x  /  2 )  e.  RR )
309 oveq1 6312 . . . . . . . . . . . . . . . . . . . . 21  |-  ( Y  =  0  ->  ( Y  x.  ( 1  /  j ) )  =  ( 0  x.  ( 1  /  j
) ) )
310302mul02d 9838 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( 0  x.  (
1  /  j ) )  =  0 )
311309, 310sylan9eqr 2485 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  Y  =  0 )  ->  ( Y  x.  ( 1  /  j ) )  =  0 )
312210rphalfcld 11360 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( x  /  2
)  e.  RR+ )
313312rpgt0d 11351 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  0  <  ( x  /  2 ) )
314313adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  Y  =  0 )  ->  0  <  ( x  /  2
) )
315311, 314eqbrtrd 4444 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  Y  =  0 )  ->  ( Y  x.  ( 1  /  j ) )  <  ( x  / 
2 ) )
316307, 308, 315ltled 9790 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  Y  =  0 )  ->  ( Y  x.  ( 1  /  j ) )  <_  ( x  / 
2 ) )
317247adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  -.  Y  =  0 )  ->  Y  e.  RR )
318296adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  -.  Y  =  0 )  -> 
0  <_  Y )
319 neqne 37347 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -.  Y  =  0  ->  Y  =/=  0 )
320319adantl 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  -.  Y  =  0 )  ->  Y  =/=  0 )
321317, 318, 320ne0gt0d 9779 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  -.  Y  =  0 )  -> 
0  <  Y )
322283adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  j ) )  e.  RR )
3233, 213sseldi 3462 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  N  e.  RR )
324 0red 9651 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ch 
->  0  e.  RR )
325203, 210, 144syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ch 
->  M  e.  RR )
326203, 67syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ch 
->  0  <  M )
327203, 210, 189syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ch 
->  M  <_  N )
328324, 325, 323, 326, 327ltletrd 9802 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  0  <  N )
329328gt0ne0d 10185 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  N  =/=  0
)
330323, 329rereccld 10441 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( 1  /  N
)  e.  RR )
331247, 330remulcld 9678 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ch 
->  ( Y  x.  (
1  /  N ) )  e.  RR )
332331adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  N ) )  e.  RR )
333238adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  0  < 
Y )  ->  (
x  /  2 )  e.  RR )
334282adantr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  0  < 
Y )  ->  (
1  /  j )  e.  RR )
335330adantr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  0  < 
Y )  ->  (
1  /  N )  e.  RR )
336247adantr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  0  < 
Y )  ->  Y  e.  RR )
337296adantr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  0  < 
Y )  ->  0  <_  Y )
338323, 328elrpd 11345 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  N  e.  RR+ )
339203, 218, 59syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  j  e.  RR+ )
340 1red 9665 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  1  e.  RR )
34176a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  0  <_  1 )
342217, 191syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ch 
->  N  <_  j )
343338, 339, 340, 341, 342lediv2ad 11370 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ch 
->  ( 1  /  j
)  <_  ( 1  /  N ) )
344343adantr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  0  < 
Y )  ->  (
1  /  j )  <_  ( 1  /  N ) )
345334, 335, 336, 337, 344lemul2ad 10554 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  j ) )  <_  ( Y  x.  ( 1  /  N
) ) )
346236recnd 9676 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ch 
->  x  e.  CC )
347 2cnd 10689 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ch 
->  2  e.  CC )
348210rpne0d 11353 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ch 
->  x  =/=  0
)
349176a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ch 
->  2  =/=  0
)
350346, 347, 348, 349divne0d 10406 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  ( x  /  2
)  =/=  0 )
351247, 238, 350redivcld 10442 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ch 
->  ( Y  /  (
x  /  2 ) )  e.  RR )
352351adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( x  / 
2 ) )  e.  RR )
353 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ch  /\  0  < 
Y )  ->  0  <  Y )
354313adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ch  /\  0  < 
Y )  ->  0  <  ( x  /  2
) )
355336, 333, 353, 354divgt0d 10549 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ch  /\  0  < 
Y )  ->  0  <  ( Y  /  (
x  /  2 ) ) )
356352, 355elrpd 11345 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( x  / 
2 ) )  e.  RR+ )
357356rprecred 11359 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  (
1  /  ( Y  /  ( x  / 
2 ) ) )  e.  RR )
358338adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  0  < 
Y )  ->  N  e.  RR+ )
359 1red 9665 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  0  < 
Y )  ->  1  e.  RR )
36076a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  0  < 
Y )  ->  0  <_  1 )
361351flcld 12040 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ch 
->  ( |_ `  ( Y  /  ( x  / 
2 ) ) )  e.  ZZ )
362361peano2zd 11050 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ch 
->  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 )  e.  ZZ )
363362zred 11047 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 )  e.  RR )
364203, 142syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ch 
->  M  e.  ZZ )
365362, 364ifcld 3954 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ch 
->  if ( M  <_ 
( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 ) ,  ( ( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) ,  M )  e.  ZZ )
366147, 365syl5eqel 2511 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ch 
->  N  e.  ZZ )
367366zred 11047 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  N  e.  RR )
368 flltp1 12042 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( Y  /  ( x  /  2 ) )  e.  RR  ->  ( Y  /  ( x  / 
2 ) )  < 
( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 ) )
369351, 368syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  ( Y  /  (
x  /  2 ) )  <  ( ( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) )
370203, 62syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ch 
->  M  e.  RR )
371 max2 11489 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( M  e.  RR  /\  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 )  e.  RR )  ->  ( ( |_
`  ( Y  / 
( x  /  2
) ) )  +  1 )  <_  if ( M  <_  ( ( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) ,  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 ) ,  M ) )
372370, 363, 371syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ch 
->  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 )  <_  if ( M  <_  ( ( |_
`  ( Y  / 
( x  /  2
) ) )  +  1 ) ,  ( ( |_ `  ( Y  /  ( x  / 
2 ) ) )  +  1 ) ,  M ) )
373372, 147syl6breqr 4464 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ch 
->  ( ( |_ `  ( Y  /  (
x  /  2 ) ) )  +  1 )  <_  N )
374351, 363, 367, 369, 373ltletrd 9802 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ch 
->  ( Y  /  (
x  /  2 ) )  <  N )
375351, 323, 374ltled 9790 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ch 
->  ( Y  /  (
x  /  2 ) )  <_  N )
376375adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( x  / 
2 ) )  <_  N )
377356, 358, 359, 360, 376lediv2ad 11370 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  (
1  /  N )  <_  ( 1  / 
( Y  /  (
x  /  2 ) ) ) )
378335, 357, 336, 337, 377lemul2ad 10554 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  N ) )  <_  ( Y  x.  ( 1  /  ( Y  /  ( x  / 
2 ) ) ) ) )
379336recnd 9676 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  0  < 
Y )  ->  Y  e.  CC )
380352recnd 9676 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( x  / 
2 ) )  e.  CC )
381355gt0ne0d 10185 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( x  / 
2 ) )  =/=  0 )
382379, 380, 381divrecd 10393 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( Y  / 
( x  /  2
) ) )  =  ( Y  x.  (
1  /  ( Y  /  ( x  / 
2 ) ) ) ) )
383333recnd 9676 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  0  < 
Y )  ->  (
x  /  2 )  e.  CC )
384353gt0ne0d 10185 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  0  < 
Y )  ->  Y  =/=  0 )
385350adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ch  /\  0  < 
Y )  ->  (
x  /  2 )  =/=  0 )
386379, 383, 384, 385ddcand 10410 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  /  ( Y  / 
( x  /  2
) ) )  =  ( x  /  2
) )
387382, 386eqtr3d 2465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  ( Y  / 
( x  /  2
) ) ) )  =  ( x  / 
2 ) )
388378, 387breqtrd 4448 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  N ) )  <_  ( x  / 
2 ) )
389322, 332, 333, 345, 388letrd 9799 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ch  /\  0  < 
Y )  ->  ( Y  x.  ( 1  /  j ) )  <_  ( x  / 
2 ) )
390321, 389syldan 472 . . . . . . . . . . . . . . . . . 18  |-  ( ( ch  /\  -.  Y  =  0 )  -> 
( Y  x.  (
1  /  j ) )  <_  ( x  /  2 ) )
391316, 390pm2.61dan 798 . . . . . . . . . . . . . . . . 17  |-  ( ch 
->  ( Y  x.  (
1  /  j ) )  <_  ( x  /  2 ) )
392251, 283, 238, 306, 391letrd 9799 . . . . . . . . . . . . . . . 16  |-  ( ch 
->  ( Y  x.  (
( A  +  ( 1  /  j ) )  -  z ) )  <_  ( x  /  2 ) )
393246, 251, 238, 281, 392letrd 9799 . . . . . . . . . . . . . . 15  |-  ( ch 
->  ( abs `  (
( F `  ( A  +  ( 1  /  j ) ) )  -  ( F `
 z ) ) )  <_  ( x  /  2 ) )
394242, 393eqbrtrd 4444 . . . . . . . . . . . . . 14  |-  ( ch 
->  ( abs `  (
( S `  j
)  -  ( F `
 z ) ) )  <_  ( 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  -  A
) )  <  (
1  /  j ) )  ->  ( abs `  ( ( S `  j )  -  ( limsup `
 S ) ) )  <  ( x  /  2 ) )
397201, 396syl 17 . . . . . . . . . . . . 13  |-  ( ch 
->  ( abs `  (
( S `  j
)  -  ( limsup `  S ) ) )  <  ( x  / 
2 ) )
398232, 234, 238, 238, 395, 397leltaddd 10242 . . . . . . . . . . . 12  |-  ( ch 
->  ( ( abs `  (
( F `  z
)  -  ( S `
 j ) ) )  +  ( abs `  ( ( S `  j )  -  ( limsup `
 S ) ) ) )  <  (
( x  /  2
)  +  ( x  /  2 ) ) )
3993462halvesd 10865 . . . . . . . . . . . 12  |-  ( ch 
->  ( ( x  / 
2 )  +  ( x  /  2 ) )  =  x )
400398, 399breqtrd 4448 . . . . . . . . . . 11  |-  ( ch 
->  ( ( abs `  (
( F `  z
)  -  ( S `
 j ) ) )  +  ( abs `  ( ( S `  j )  -  ( limsup `
 S ) ) ) )  <  x
)
401230, 235, 236, 237, 400lelttrd 9800 . . . . . . . . . 10  |-  ( ch 
->  ( abs `  (
( ( F `  z )  -  ( S `  j )
)  +  ( ( S `  j )  -  ( limsup `  S
) ) ) )  <  x )
402224, 401eqbrtrd 4444 . . . . . . . . 9  |-  ( ch 
->  ( abs `  (
( F `  z
)  -  ( limsup `  S ) ) )  <  x )
403200, 402sylbir 216 . . . . . . . 8  |-  ( ( ( ( ( (
ph  /\  x  e.  RR+ )  /\  j  e.  ( ZZ>= `  N )
)  /\  ( abs `  ( ( S `  j )  -  ( limsup `
 S ) ) )  <  ( x  /  2 ) )  /\  z  e.  ( A (,) B ) )  /\  ( abs `  ( z  -  A
) )  <  (
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  =/=  A  /\  ( abs `  ( z  -  A ) )  < 
( 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  =/= 
A  /\  ( abs `  ( z  -  A
) )  <  (
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  =/=  A  /\  ( abs `  ( z  -  A ) )  < 
( 1  /  j
) )  ->  ( abs `  ( ( F `
 z )  -  ( limsup `  S )
) )  <  x
) )
407 breq2 4427 . . . . . . . . 9  |-  ( y  =  ( 1  / 
j )  ->  (
( abs `  (
z  -  A ) )  <  y  <->  ( abs `  ( z  -  A
) )  <  (
1  /  j ) ) )
408407anbi2d 708 . . . . . . . 8  |-  ( y  =  ( 1  / 
j )  ->  (
( z  =/=  A  /\  ( abs `  (
z  -  A ) )  <  y )  <-> 
( z  =/=  A  /\  ( abs `  (
z  -  A ) )  <  ( 1  /  j ) ) ) )
409408imbi1d 318 . . . . . . 7  |-  ( y  =  ( 1  / 
j )  ->  (
( ( z  =/= 
A  /\  ( abs `  ( z  -  A
) )  <  y
)  ->  ( abs `  ( ( F `  z )  -  ( limsup `
 S ) ) )  <  x )  <-> 
( ( z  =/= 
A  /\  ( abs `  ( z  -  A
) )  <  (
1  /  j ) )  ->  ( abs `  ( ( F `  z )  -  ( limsup `
 S ) ) )  <  x ) ) )
410409ralbidv 2861 . . . . . 6  |-  ( y  =  ( 1  / 
j )  ->  ( A. z  e.  ( A (,) B ) ( ( z  =/=  A  /\  ( abs `  (
z  -  A ) )  <  y )  ->  ( abs `  (
( F `  z
)  -  ( limsup `  S ) ) )  <  x )  <->  A. z  e.  ( A (,) B
) ( ( z  =/=  A  /\  ( abs `  ( z  -  A ) )  < 
( 1  /  j
) )  ->  ( abs `  ( ( F `
 z )  -  ( limsup `  S )
) )  <  x
) ) )
411410rspcev 3182 . . . . 5  |-  ( ( ( 1  /  j
)  e.  RR+  /\  A. z  e.  ( A (,) B ) ( ( z  =/=  A  /\  ( abs `  ( z  -  A ) )  <  ( 1  / 
j ) )  -> 
( abs `  (
( F `  z
)  -  ( limsup `  S ) ) )  <  x ) )  ->  E. y  e.  RR+  A. z  e.  ( A (,) B ) ( ( z  =/=  A  /\  ( abs `  (
z  -  A ) )  <  y )  ->  ( abs `  (
( F `  z
)  -  ( limsup `  S ) ) )  <  x ) )
412199, 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  =/=  A  /\  ( abs `  ( z  -  A ) )  < 
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 )
)
416183, 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 )
422183ad2antrr 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 )
437183adantr 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, 154, 109, 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 ioodvbdlimc1lem2OLD.r . . . . . . . . . . . 12  |-  R  =  ( j  e.  (
ZZ>= `  M )  |->  ( A  +  ( 1  /  j ) ) )
470105, 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
)  |->  A )  e. 
_V
476475a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( j  e.  (
ZZ>= `  M )  |->  A )  e.  _V )
477 eqidd 2423 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( ZZ>= `  M )
)  ->  ( j  e.  ( ZZ>= `  M )  |->  A )  =  ( j  e.  ( ZZ>= `  M )  |->  A ) )
478 eqidd 2423 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  M )
)  /\  j  =  m )  ->  A  =  A )
479 simpr 462 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( ZZ>= `  M )
)  ->  m  e.  ( ZZ>= `  M )
)
4807adantr 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( ZZ>= `  M )
)  ->  A  e.  RR )
481477, 478, 479, 480fvmptd 5970 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( ZZ>= `  M )
)  ->  ( (
j  e.  ( ZZ>= `  M )  |->  A ) `
 m )  =  A )
48223, 142, 476, 98, 481climconst 13606 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( j  e.  (
ZZ>= `  M )  |->  A )  ~~>  A )
483474mptex 6151 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( ZZ>= `  M
)  |->  ( A  +  ( 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, 67, 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 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( j  e.  ( ZZ>= `  M )  |->  A )  =  ( j  e.  ( ZZ>= `  M )  |->  A ) )
492 eqidd 2423 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( ZZ>= `  M )
)  /\  j  =  i )  ->  A  =  A )
493 simpr 462 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  e.  ( ZZ>= `  M )
)
4947adantr 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  A  e.  RR )
495491, 492, 493, 494fvmptd 5970 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( (
j  e.  ( ZZ>= `  M )  |->  A ) `
 i )  =  A )
49698adantr 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  A  e.  CC )
497495, 496eqeltrd 2507 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( (
j  e.  ( ZZ>= `  M )  |->  A ) `
 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 )
50362adantr 466 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  M  e.  RR )
50467adantr 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 )
514469a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  R  =  ( j  e.  (
ZZ>= `  M )  |->  ( A  +  ( 1  /  j ) ) ) )
515499oveq2d 6321 . . . . . . . . . . . . . . . . 17  |-  ( j  =  i  ->  ( A  +  ( 1  /  j ) )  =  ( A  +  ( 1  /  i
) ) )
516515adantl 467 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( ZZ>= `  M )
)  /\  j  =  i )  ->  ( A  +  ( 1  /  j ) )  =  ( A  +  ( 1  /  i
) ) )
517494, 509readdcld 9677 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( A  +  ( 1  / 
i ) )  e.  RR )
518514, 516, 493, 517fvmptd 5970 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( R `  i )  =  ( A  +  ( 1  /  i ) ) )
519495, 510oveq12d 6323 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( (
( j  e.  (
ZZ>= `  M )  |->  A ) `  i )  +  ( ( j  e.  ( ZZ>= `  M
)  |->  ( 1  / 
j ) ) `  i ) )  =  ( A