MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pntrlog2bndlem4 Structured version   Unicode version

Theorem pntrlog2bndlem4 22961
Description: Lemma for pntrlog2bnd 22965. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.)
Hypotheses
Ref Expression
pntsval.1  |-  S  =  ( a  e.  RR  |->  sum_ i  e.  ( 1 ... ( |_ `  a ) ) ( (Λ `  i )  x.  ( ( log `  i
)  +  (ψ `  ( a  /  i
) ) ) ) )
pntrlog2bnd.r  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
pntrlog2bnd.t  |-  T  =  ( a  e.  RR  |->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 ) )
Assertion
Ref Expression
pntrlog2bndlem4  |-  ( x  e.  ( 1 (,) +oo )  |->  ( ( ( ( abs `  ( R `  x )
)  x.  ( log `  x ) )  -  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( ( T `
 n )  -  ( T `  ( n  -  1 ) ) ) ) ) )  /  x ) )  e.  <_O(1)
Distinct variable groups:    i, a, n, x    S, n, x    R, n, x    T, n
Allowed substitution hints:    R( i, a)    S( i, a)    T( x, i, a)

Proof of Theorem pntrlog2bndlem4
Dummy variables  c  m  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elioore 11440 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( 1 (,) +oo )  ->  x  e.  RR )
21adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  x  e.  RR )
3 1rp 11105 . . . . . . . . . . . . . . . . . . . 20  |-  1  e.  RR+
43a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  1  e.  RR+ )
5 1red 9511 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  1  e.  RR )
6 eliooord 11465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( 1 (,) +oo )  ->  ( 1  <  x  /\  x  < +oo ) )
76adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1  <  x  /\  x  < +oo ) )
87simpld 459 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  1  <  x )
95, 2, 8ltled 9632 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  1  <_  x )
102, 4, 9rpgecld 11172 . . . . . . . . . . . . . . . . . 18  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  x  e.  RR+ )
1110rprege0d 11144 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  e.  RR  /\  0  <_  x ) )
12 flge0nn0 11782 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  RR  /\  0  <_  x )  -> 
( |_ `  x
)  e.  NN0 )
1311, 12syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( |_ `  x )  e. 
NN0 )
14 nn0p1nn 10729 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( |_ `  x )  e.  NN0  ->  ( ( |_ `  x )  +  1 )  e.  NN )
1513, 14syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  NN )
1615nnrpd 11136 . . . . . . . . . . . . . . . . . 18  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  RR+ )
1710, 16rpdivcld 11154 . . . . . . . . . . . . . . . . 17  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  e.  RR+ )
18 pntrlog2bnd.r . . . . . . . . . . . . . . . . . 18  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
1918pntrval 22943 . . . . . . . . . . . . . . . . 17  |-  ( ( x  /  ( ( |_ `  x )  +  1 ) )  e.  RR+  ->  ( R `
 ( x  / 
( ( |_ `  x )  +  1 ) ) )  =  ( (ψ `  (
x  /  ( ( |_ `  x )  +  1 ) ) )  -  ( x  /  ( ( |_
`  x )  +  1 ) ) ) )
2017, 19syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( R `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  =  ( (ψ `  ( x  /  (
( |_ `  x
)  +  1 ) ) )  -  (
x  /  ( ( |_ `  x )  +  1 ) ) ) )
212, 15nndivred 10480 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  e.  RR )
22 2re 10501 . . . . . . . . . . . . . . . . . . . 20  |-  2  e.  RR
2322a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  2  e.  RR )
24 flltp1 11766 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  x  <  ( ( |_ `  x )  +  1 ) )
252, 24syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  x  <  ( ( |_ `  x )  +  1 ) )
2615nncnd 10448 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  CC )
2726mulid1d 9513 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( |_ `  x )  +  1 )  x.  1 )  =  ( ( |_
`  x )  +  1 ) )
2825, 27breqtrrd 4425 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  x  <  ( ( ( |_
`  x )  +  1 )  x.  1 ) )
292, 5, 16ltdivmuld 11184 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( x  /  (
( |_ `  x
)  +  1 ) )  <  1  <->  x  <  ( ( ( |_
`  x )  +  1 )  x.  1 ) ) )
3028, 29mpbird 232 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  <  1 )
31 1lt2 10598 . . . . . . . . . . . . . . . . . . . 20  |-  1  <  2
3231a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  1  <  2 )
3321, 5, 23, 30, 32lttrd 9642 . . . . . . . . . . . . . . . . . 18  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  <  2 )
34 chpeq0 22679 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  /  ( ( |_ `  x )  +  1 ) )  e.  RR  ->  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  =  0  <->  ( x  /  ( ( |_
`  x )  +  1 ) )  <  2 ) )
3521, 34syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  =  0  <->  ( x  /  ( ( |_
`  x )  +  1 ) )  <  2 ) )
3633, 35mpbird 232 . . . . . . . . . . . . . . . . 17  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (ψ `  ( x  /  (
( |_ `  x
)  +  1 ) ) )  =  0 )
3736oveq1d 6214 . . . . . . . . . . . . . . . 16  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  -  ( x  / 
( ( |_ `  x )  +  1 ) ) )  =  ( 0  -  (
x  /  ( ( |_ `  x )  +  1 ) ) ) )
3820, 37eqtrd 2495 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( R `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  =  ( 0  -  ( x  /  (
( |_ `  x
)  +  1 ) ) ) )
3938fveq2d 5802 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( R `  ( x  /  (
( |_ `  x
)  +  1 ) ) ) )  =  ( abs `  (
0  -  ( x  /  ( ( |_
`  x )  +  1 ) ) ) ) )
40 0red 9497 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  0  e.  RR )
4117rpge0d 11141 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  0  <_  ( x  /  (
( |_ `  x
)  +  1 ) ) )
4240, 21, 41abssuble0d 13036 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( 0  -  ( x  /  (
( |_ `  x
)  +  1 ) ) ) )  =  ( ( x  / 
( ( |_ `  x )  +  1 ) )  -  0 ) )
4321recnd 9522 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  e.  CC )
4443subid1d 9818 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( x  /  (
( |_ `  x
)  +  1 ) )  -  0 )  =  ( x  / 
( ( |_ `  x )  +  1 ) ) )
4539, 42, 443eqtrd 2499 . . . . . . . . . . . . 13  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( R `  ( x  /  (
( |_ `  x
)  +  1 ) ) ) )  =  ( x  /  (
( |_ `  x
)  +  1 ) ) )
4613nn0red 10747 . . . . . . . . . . . . . . . 16  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( |_ `  x )  e.  RR )
47 pntsval.1 . . . . . . . . . . . . . . . . 17  |-  S  =  ( a  e.  RR  |->  sum_ i  e.  ( 1 ... ( |_ `  a ) ) ( (Λ `  i )  x.  ( ( log `  i
)  +  (ψ `  ( a  /  i
) ) ) ) )
4847pntsval2 22957 . . . . . . . . . . . . . . . 16  |-  ( ( |_ `  x )  e.  RR  ->  ( S `  ( |_ `  x ) )  = 
sum_ n  e.  (
1 ... ( |_ `  ( |_ `  x ) ) ) ( ( (Λ `  n )  x.  ( log `  n
) )  +  sum_ m  e.  { y  e.  NN  |  y  ||  n }  ( (Λ `  m )  x.  (Λ `  ( n  /  m
) ) ) ) )
4946, 48syl 16 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( S `  ( |_ `  x ) )  = 
sum_ n  e.  (
1 ... ( |_ `  ( |_ `  x ) ) ) ( ( (Λ `  n )  x.  ( log `  n
) )  +  sum_ m  e.  { y  e.  NN  |  y  ||  n }  ( (Λ `  m )  x.  (Λ `  ( n  /  m
) ) ) ) )
5013nn0cnd 10748 . . . . . . . . . . . . . . . . 17  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( |_ `  x )  e.  CC )
51 1cnd 9512 . . . . . . . . . . . . . . . . 17  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  1  e.  CC )
5250, 51pncand 9830 . . . . . . . . . . . . . . . 16  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( |_ `  x )  +  1 )  -  1 )  =  ( |_ `  x ) )
5352fveq2d 5802 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( S `  ( (
( |_ `  x
)  +  1 )  -  1 ) )  =  ( S `  ( |_ `  x ) ) )
5447pntsval2 22957 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  RR  ->  ( S `  x )  =  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  x.  ( log `  n ) )  + 
sum_ m  e.  { y  e.  NN  |  y 
||  n }  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) ) ) )
552, 54syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( S `  x )  =  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  x.  ( log `  n ) )  + 
sum_ m  e.  { y  e.  NN  |  y 
||  n }  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) ) ) )
56 flidm 11774 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  RR  ->  ( |_ `  ( |_ `  x ) )  =  ( |_ `  x
) )
572, 56syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( |_ `  ( |_ `  x ) )  =  ( |_ `  x
) )
5857oveq2d 6215 . . . . . . . . . . . . . . . . 17  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1 ... ( |_ `  ( |_ `  x ) ) )  =  ( 1 ... ( |_
`  x ) ) )
5958sumeq1d 13295 . . . . . . . . . . . . . . . 16  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  ( |_ `  x ) ) ) ( ( (Λ `  n
)  x.  ( log `  n ) )  + 
sum_ m  e.  { y  e.  NN  |  y 
||  n }  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) ) )  =  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  ( log `  n ) )  + 
sum_ m  e.  { y  e.  NN  |  y 
||  n }  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) ) ) )
6055, 59eqtr4d 2498 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( S `  x )  =  sum_ n  e.  ( 1 ... ( |_
`  ( |_ `  x ) ) ) ( ( (Λ `  n
)  x.  ( log `  n ) )  + 
sum_ m  e.  { y  e.  NN  |  y 
||  n }  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) ) ) )
6149, 53, 603eqtr4d 2505 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( S `  ( (
( |_ `  x
)  +  1 )  -  1 ) )  =  ( S `  x ) )
6252fveq2d 5802 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( T `  ( (
( |_ `  x
)  +  1 )  -  1 ) )  =  ( T `  ( |_ `  x ) ) )
6362oveq2d 6215 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
2  x.  ( T `
 ( ( ( |_ `  x )  +  1 )  - 
1 ) ) )  =  ( 2  x.  ( T `  ( |_ `  x ) ) ) )
6461, 63oveq12d 6217 . . . . . . . . . . . . 13  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( S `  (
( ( |_ `  x )  +  1 )  -  1 ) )  -  ( 2  x.  ( T `  ( ( ( |_
`  x )  +  1 )  -  1 ) ) ) )  =  ( ( S `
 x )  -  ( 2  x.  ( T `  ( |_ `  x ) ) ) ) )
6545, 64oveq12d 6217 . . . . . . . . . . . 12  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( abs `  ( R `  ( x  /  ( ( |_
`  x )  +  1 ) ) ) )  x.  ( ( S `  ( ( ( |_ `  x
)  +  1 )  -  1 ) )  -  ( 2  x.  ( T `  (
( ( |_ `  x )  +  1 )  -  1 ) ) ) ) )  =  ( ( x  /  ( ( |_
`  x )  +  1 ) )  x.  ( ( S `  x )  -  (
2  x.  ( T `
 ( |_ `  x ) ) ) ) ) )
662recnd 9522 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  x  e.  CC )
6766div1d 10209 . . . . . . . . . . . . . . . . . 18  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  /  1 )  =  x )
6867fveq2d 5802 . . . . . . . . . . . . . . . . 17  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( R `  ( x  /  1 ) )  =  ( R `  x ) )
6918pntrf 22944 . . . . . . . . . . . . . . . . . . 19  |-  R : RR+
--> RR
7069ffvelrni 5950 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  RR+  ->  ( R `
 x )  e.  RR )
7110, 70syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( R `  x )  e.  RR )
7268, 71eqeltrd 2542 . . . . . . . . . . . . . . . 16  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( R `  ( x  /  1 ) )  e.  RR )
7372recnd 9522 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( R `  ( x  /  1 ) )  e.  CC )
7473abscld 13039 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( R `  ( x  /  1
) ) )  e.  RR )
7574recnd 9522 . . . . . . . . . . . . 13  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( R `  ( x  /  1
) ) )  e.  CC )
7675mul01d 9678 . . . . . . . . . . . 12  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( abs `  ( R `  ( x  /  1 ) ) )  x.  0 )  =  0 )
7765, 76oveq12d 6217 . . . . . . . . . . 11  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( abs `  ( R `  ( x  /  ( ( |_
`  x )  +  1 ) ) ) )  x.  ( ( S `  ( ( ( |_ `  x
)  +  1 )  -  1 ) )  -  ( 2  x.  ( T `  (
( ( |_ `  x )  +  1 )  -  1 ) ) ) ) )  -  ( ( abs `  ( R `  (
x  /  1 ) ) )  x.  0 ) )  =  ( ( ( x  / 
( ( |_ `  x )  +  1 ) )  x.  (
( S `  x
)  -  ( 2  x.  ( T `  ( |_ `  x ) ) ) ) )  -  0 ) )
7847pntsf 22954 . . . . . . . . . . . . . . . . 17  |-  S : RR
--> RR
7978ffvelrni 5950 . . . . . . . . . . . . . . . 16  |-  ( x  e.  RR  ->  ( S `  x )  e.  RR )
802, 79syl 16 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( S `  x )  e.  RR )
81 pntrlog2bnd.t . . . . . . . . . . . . . . . . . . 19  |-  T  =  ( a  e.  RR  |->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 ) )
82 relogcl 22159 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  e.  RR+  ->  ( log `  a )  e.  RR )
83 remulcl 9477 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( a  e.  RR  /\  ( log `  a )  e.  RR )  -> 
( a  x.  ( log `  a ) )  e.  RR )
8482, 83sylan2 474 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( a  e.  RR  /\  a  e.  RR+ )  -> 
( a  x.  ( log `  a ) )  e.  RR )
85 0red 9497 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( a  e.  RR  /\  -.  a  e.  RR+ )  ->  0  e.  RR )
8684, 85ifclda 3928 . . . . . . . . . . . . . . . . . . 19  |-  ( a  e.  RR  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  e.  RR )
8781, 86fmpti 5974 . . . . . . . . . . . . . . . . . 18  |-  T : RR
--> RR
8887ffvelrni 5950 . . . . . . . . . . . . . . . . 17  |-  ( ( |_ `  x )  e.  RR  ->  ( T `  ( |_ `  x ) )  e.  RR )
8946, 88syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( T `  ( |_ `  x ) )  e.  RR )
9023, 89remulcld 9524 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
2  x.  ( T `
 ( |_ `  x ) ) )  e.  RR )
9180, 90resubcld 9886 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( S `  x
)  -  ( 2  x.  ( T `  ( |_ `  x ) ) ) )  e.  RR )
9221, 91remulcld 9524 . . . . . . . . . . . . 13  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( x  /  (
( |_ `  x
)  +  1 ) )  x.  ( ( S `  x )  -  ( 2  x.  ( T `  ( |_ `  x ) ) ) ) )  e.  RR )
9392recnd 9522 . . . . . . . . . . . 12  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( x  /  (
( |_ `  x
)  +  1 ) )  x.  ( ( S `  x )  -  ( 2  x.  ( T `  ( |_ `  x ) ) ) ) )  e.  CC )
9493subid1d 9818 . . . . . . . . . . 11  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( x  / 
( ( |_ `  x )  +  1 ) )  x.  (
( S `  x
)  -  ( 2  x.  ( T `  ( |_ `  x ) ) ) ) )  -  0 )  =  ( ( x  / 
( ( |_ `  x )  +  1 ) )  x.  (
( S `  x
)  -  ( 2  x.  ( T `  ( |_ `  x ) ) ) ) ) )
9577, 94eqtrd 2495 . . . . . . . . . 10  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( abs `  ( R `  ( x  /  ( ( |_
`  x )  +  1 ) ) ) )  x.  ( ( S `  ( ( ( |_ `  x
)  +  1 )  -  1 ) )  -  ( 2  x.  ( T `  (
( ( |_ `  x )  +  1 )  -  1 ) ) ) ) )  -  ( ( abs `  ( R `  (
x  /  1 ) ) )  x.  0 ) )  =  ( ( x  /  (
( |_ `  x
)  +  1 ) )  x.  ( ( S `  x )  -  ( 2  x.  ( T `  ( |_ `  x ) ) ) ) ) )
962flcld 11764 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( |_ `  x )  e.  ZZ )
97 fzval3 11721 . . . . . . . . . . . . . 14  |-  ( ( |_ `  x )  e.  ZZ  ->  (
1 ... ( |_ `  x ) )  =  ( 1..^ ( ( |_ `  x )  +  1 ) ) )
9896, 97syl 16 . . . . . . . . . . . . 13  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1 ... ( |_ `  x ) )  =  ( 1..^ ( ( |_ `  x )  +  1 ) ) )
9998eqcomd 2462 . . . . . . . . . . . 12  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1..^ ( ( |_
`  x )  +  1 ) )  =  ( 1 ... ( |_ `  x ) ) )
10010adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR+ )
101 elfznn 11594 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
102101adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
103102nnrpd 11136 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR+ )
104100, 103rpdivcld 11154 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
10569ffvelrni 5950 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  /  n )  e.  RR+  ->  ( R `
 ( x  /  n ) )  e.  RR )
106104, 105syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  e.  RR )
107106recnd 9522 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  e.  CC )
108107abscld 13039 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( R `  (
x  /  n ) ) )  e.  RR )
109108recnd 9522 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( R `  (
x  /  n ) ) )  e.  CC )
1103a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR+ )
111103, 110rpaddcld 11152 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  +  1 )  e.  RR+ )
112100, 111rpdivcld 11154 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  ( n  + 
1 ) )  e.  RR+ )
11369ffvelrni 5950 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  /  ( n  +  1 ) )  e.  RR+  ->  ( R `
 ( x  / 
( n  +  1 ) ) )  e.  RR )
114112, 113syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  (
n  +  1 ) ) )  e.  RR )
115114recnd 9522 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  (
n  +  1 ) ) )  e.  CC )
116115abscld 13039 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( R `  (
x  /  ( n  +  1 ) ) ) )  e.  RR )
117116recnd 9522 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( R `  (
x  /  ( n  +  1 ) ) ) )  e.  CC )
118109, 117negsubdi2d 9845 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  -u ( ( abs `  ( R `
 ( x  /  n ) ) )  -  ( abs `  ( R `  ( x  /  ( n  + 
1 ) ) ) ) )  =  ( ( abs `  ( R `  ( x  /  ( n  + 
1 ) ) ) )  -  ( abs `  ( R `  (
x  /  n ) ) ) ) )
119118eqcomd 2462 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  (
n  +  1 ) ) ) )  -  ( abs `  ( R `
 ( x  /  n ) ) ) )  =  -u (
( abs `  ( R `  ( x  /  n ) ) )  -  ( abs `  ( R `  ( x  /  ( n  + 
1 ) ) ) ) ) )
120102nncnd 10448 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  CC )
121 1cnd 9512 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  CC )
122120, 121pncand 9830 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
n  +  1 )  -  1 )  =  n )
123122fveq2d 5802 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( S `  ( ( n  + 
1 )  -  1 ) )  =  ( S `  n ) )
124122fveq2d 5802 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  ( ( n  + 
1 )  -  1 ) )  =  ( T `  n ) )
125 rpre 11107 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  RR+  ->  n  e.  RR )
126 eleq1 2526 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  n  ->  (
a  e.  RR+  <->  n  e.  RR+ ) )
127 id 22 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  n  ->  a  =  n )
128 fveq2 5798 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  n  ->  ( log `  a )  =  ( log `  n
) )
129127, 128oveq12d 6217 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  n  ->  (
a  x.  ( log `  a ) )  =  ( n  x.  ( log `  n ) ) )
130126, 129ifbieq1d 3919 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  n  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  if ( n  e.  RR+ ,  ( n  x.  ( log `  n
) ) ,  0 ) )
131 ovex 6224 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  x.  ( log `  n
) )  e.  _V
132 c0ex 9490 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  _V
133131, 132ifex 3965 . . . . . . . . . . . . . . . . . . . . 21  |-  if ( n  e.  RR+ ,  ( n  x.  ( log `  n ) ) ,  0 )  e.  _V
134130, 81, 133fvmpt 5882 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  RR  ->  ( T `  n )  =  if ( n  e.  RR+ ,  ( n  x.  ( log `  n
) ) ,  0 ) )
135125, 134syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  RR+  ->  ( T `
 n )  =  if ( n  e.  RR+ ,  ( n  x.  ( log `  n
) ) ,  0 ) )
136 iftrue 3904 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  RR+  ->  if ( n  e.  RR+ ,  ( n  x.  ( log `  n ) ) ,  0 )  =  ( n  x.  ( log `  n ) ) )
137135, 136eqtrd 2495 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  RR+  ->  ( T `
 n )  =  ( n  x.  ( log `  n ) ) )
138103, 137syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  n )  =  ( n  x.  ( log `  n ) ) )
139124, 138eqtrd 2495 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  ( ( n  + 
1 )  -  1 ) )  =  ( n  x.  ( log `  n ) ) )
140139oveq2d 6215 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( T `  ( ( n  + 
1 )  -  1 ) ) )  =  ( 2  x.  (
n  x.  ( log `  n ) ) ) )
141123, 140oveq12d 6217 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( S `  ( (
n  +  1 )  -  1 ) )  -  ( 2  x.  ( T `  (
( n  +  1 )  -  1 ) ) ) )  =  ( ( S `  n )  -  (
2  x.  ( n  x.  ( log `  n
) ) ) ) )
142119, 141oveq12d 6217 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( abs `  ( R `  ( x  /  ( n  + 
1 ) ) ) )  -  ( abs `  ( R `  (
x  /  n ) ) ) )  x.  ( ( S `  ( ( n  + 
1 )  -  1 ) )  -  (
2  x.  ( T `
 ( ( n  +  1 )  - 
1 ) ) ) ) )  =  (
-u ( ( abs `  ( R `  (
x  /  n ) ) )  -  ( abs `  ( R `  ( x  /  (
n  +  1 ) ) ) ) )  x.  ( ( S `
 n )  -  ( 2  x.  (
n  x.  ( log `  n ) ) ) ) ) )
143108, 116resubcld 9886 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  -  ( abs `  ( R `
 ( x  / 
( n  +  1 ) ) ) ) )  e.  RR )
144143recnd 9522 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  -  ( abs `  ( R `
 ( x  / 
( n  +  1 ) ) ) ) )  e.  CC )
145102nnred 10447 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR )
14678ffvelrni 5950 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  RR  ->  ( S `  n )  e.  RR )
147145, 146syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( S `  n )  e.  RR )
14822a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  2  e.  RR )
149103relogcld 22204 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  n )  e.  RR )
150145, 149remulcld 9524 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  x.  ( log `  n
) )  e.  RR )
151148, 150remulcld 9524 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( n  x.  ( log `  n
) ) )  e.  RR )
152147, 151resubcld 9886 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( S `  n )  -  ( 2  x.  ( n  x.  ( log `  n ) ) ) )  e.  RR )
153152recnd 9522 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( S `  n )  -  ( 2  x.  ( n  x.  ( log `  n ) ) ) )  e.  CC )
154144, 153mulneg1d 9907 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( -u (
( abs `  ( R `  ( x  /  n ) ) )  -  ( abs `  ( R `  ( x  /  ( n  + 
1 ) ) ) ) )  x.  (
( S `  n
)  -  ( 2  x.  ( n  x.  ( log `  n
) ) ) ) )  =  -u (
( ( abs `  ( R `  ( x  /  n ) ) )  -  ( abs `  ( R `  ( x  /  ( n  + 
1 ) ) ) ) )  x.  (
( S `  n
)  -  ( 2  x.  ( n  x.  ( log `  n
) ) ) ) ) )
155142, 154eqtrd 2495 . . . . . . . . . . . 12  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( abs `  ( R `  ( x  /  ( n  + 
1 ) ) ) )  -  ( abs `  ( R `  (
x  /  n ) ) ) )  x.  ( ( S `  ( ( n  + 
1 )  -  1 ) )  -  (
2  x.  ( T `
 ( ( n  +  1 )  - 
1 ) ) ) ) )  =  -u ( ( ( abs `  ( R `  (
x  /  n ) ) )  -  ( abs `  ( R `  ( x  /  (
n  +  1 ) ) ) ) )  x.  ( ( S `
 n )  -  ( 2  x.  (
n  x.  ( log `  n ) ) ) ) ) )
15699, 155sumeq12rdv 13301 . . . . . . . . . . 11  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1..^ ( ( |_ `  x )  +  1 ) ) ( ( ( abs `  ( R `  (
x  /  ( n  +  1 ) ) ) )  -  ( abs `  ( R `  ( x  /  n
) ) ) )  x.  ( ( S `
 ( ( n  +  1 )  - 
1 ) )  -  ( 2  x.  ( T `  ( (
n  +  1 )  -  1 ) ) ) ) )  = 
sum_ n  e.  (
1 ... ( |_ `  x ) ) -u ( ( ( abs `  ( R `  (
x  /  n ) ) )  -  ( abs `  ( R `  ( x  /  (
n  +  1 ) ) ) ) )  x.  ( ( S `
 n )  -  ( 2  x.  (
n  x.  ( log `  n ) ) ) ) ) )
157 fzfid 11911 . . . . . . . . . . . 12  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1 ... ( |_ `  x ) )  e. 
Fin )
158143, 152remulcld 9524 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( abs `  ( R `  ( x  /  n ) ) )  -  ( abs `  ( R `  ( x  /  ( n  + 
1 ) ) ) ) )  x.  (
( S `  n
)  -  ( 2  x.  ( n  x.  ( log `  n
) ) ) ) )  e.  RR )
159158recnd 9522 . . . . . . . . . . . 12  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( abs `  ( R `  ( x  /  n ) ) )  -  ( abs `  ( R `  ( x  /  ( n  + 
1 ) ) ) ) )  x.  (
( S `  n
)  -  ( 2  x.  ( n  x.  ( log `  n
) ) ) ) )  e.  CC )
160157, 159fsumneg 13371 . . . . . . . . . . 11  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) )
-u ( ( ( abs `  ( R `
 ( x  /  n ) ) )  -  ( abs `  ( R `  ( x  /  ( n  + 
1 ) ) ) ) )  x.  (
( S `  n
)  -  ( 2  x.  ( n  x.  ( log `  n
) ) ) ) )  =  -u sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( abs `  ( R `  (
x  /  n ) ) )  -  ( abs `  ( R `  ( x  /  (
n  +  1 ) ) ) ) )  x.  ( ( S `
 n )  -  ( 2  x.  (
n  x.  ( log `  n ) ) ) ) ) )
161156, 160eqtrd 2495 . . . . . . . . . 10  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1..^ ( ( |_ `  x )  +  1 ) ) ( ( ( abs `  ( R `  (
x  /  ( n  +  1 ) ) ) )  -  ( abs `  ( R `  ( x  /  n
) ) ) )  x.  ( ( S `
 ( ( n  +  1 )  - 
1 ) )  -  ( 2  x.  ( T `  ( (
n  +  1 )  -  1 ) ) ) ) )  = 
-u sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( ( abs `  ( R `  (
x  /  n ) ) )  -  ( abs `  ( R `  ( x  /  (
n  +  1 ) ) ) ) )  x.  ( ( S `
 n )  -  ( 2  x.  (
n  x.  ( log `  n ) ) ) ) ) )
16295, 161oveq12d 6217 . . . . . . . . 9  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( ( abs `  ( R `  (
x  /  ( ( |_ `  x )  +  1 ) ) ) )  x.  (
( S `  (
( ( |_ `  x )  +  1 )  -  1 ) )  -  ( 2  x.  ( T `  ( ( ( |_
`  x )  +  1 )  -  1 ) ) ) ) )  -  ( ( abs `  ( R `
 ( x  / 
1 ) ) )  x.  0 ) )  -  sum_ n  e.  ( 1..^ ( ( |_
`  x )  +  1 ) ) ( ( ( abs `  ( R `  ( x  /  ( n  + 
1 ) ) ) )  -  ( abs `  ( R `  (
x  /  n ) ) ) )  x.  ( ( S `  ( ( n  + 
1 )  -  1 ) )  -  (
2  x.  ( T `
 ( ( n  +  1 )  - 
1 ) ) ) ) ) )  =  ( ( ( x  /  ( ( |_
`  x )  +  1 ) )  x.  ( ( S `  x )  -  (
2  x.  ( T `
 ( |_ `  x ) ) ) ) )  -  -u sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( abs `  ( R `  (
x  /  n ) ) )  -  ( abs `  ( R `  ( x  /  (
n  +  1 ) ) ) ) )  x.  ( ( S `
 n )  -  ( 2  x.  (
n  x.  ( log `  n ) ) ) ) ) ) )
163 oveq2 6207 . . . . . . . . . . . . . 14  |-  ( m  =  n  ->  (
x  /  m )  =  ( x  /  n ) )
164163fveq2d 5802 . . . . . . . . . . . . 13  |-  ( m  =  n  ->  ( R `  ( x  /  m ) )  =  ( R `  (
x  /  n ) ) )
165164fveq2d 5802 . . . . . . . . . . . 12  |-  ( m  =  n  ->  ( abs `  ( R `  ( x  /  m
) ) )  =  ( abs `  ( R `  ( x  /  n ) ) ) )
166 oveq1 6206 . . . . . . . . . . . . . 14  |-  ( m  =  n  ->  (
m  -  1 )  =  ( n  - 
1 ) )
167166fveq2d 5802 . . . . . . . . . . . . 13  |-  ( m  =  n  ->  ( S `  ( m  -  1 ) )  =  ( S `  ( n  -  1
) ) )
168166fveq2d 5802 . . . . . . . . . . . . . 14  |-  ( m  =  n  ->  ( T `  ( m  -  1 ) )  =  ( T `  ( n  -  1
) ) )
169168oveq2d 6215 . . . . . . . . . . . . 13  |-  ( m  =  n  ->  (
2  x.  ( T `
 ( m  - 
1 ) ) )  =  ( 2  x.  ( T `  (
n  -  1 ) ) ) )
170167, 169oveq12d 6217 . . . . . . . . . . . 12  |-  ( m  =  n  ->  (
( S `  (
m  -  1 ) )  -  ( 2  x.  ( T `  ( m  -  1
) ) ) )  =  ( ( S `
 ( n  - 
1 ) )  -  ( 2  x.  ( T `  ( n  -  1 ) ) ) ) )
171165, 170jca 532 . . . . . . . . . . 11  |-  ( m  =  n  ->  (
( abs `  ( R `  ( x  /  m ) ) )  =  ( abs `  ( R `  ( x  /  n ) ) )  /\  ( ( S `
 ( m  - 
1 ) )  -  ( 2  x.  ( T `  ( m  -  1 ) ) ) )  =  ( ( S `  (
n  -  1 ) )  -  ( 2  x.  ( T `  ( n  -  1
) ) ) ) ) )
172 oveq2 6207 . . . . . . . . . . . . . 14  |-  ( m  =  ( n  + 
1 )  ->  (
x  /  m )  =  ( x  / 
( n  +  1 ) ) )
173172fveq2d 5802 . . . . . . . . . . . . 13  |-  ( m  =  ( n  + 
1 )  ->  ( R `  ( x  /  m ) )  =  ( R `  (
x  /  ( n  +  1 ) ) ) )
174173fveq2d 5802 . . . . . . . . . . . 12  |-  ( m  =  ( n  + 
1 )  ->  ( abs `  ( R `  ( x  /  m
) ) )  =  ( abs `  ( R `  ( x  /  ( n  + 
1 ) ) ) ) )
175 oveq1 6206 . . . . . . . . . . . . . 14  |-  ( m  =  ( n  + 
1 )  ->  (
m  -  1 )  =  ( ( n  +  1 )  - 
1 ) )
176175fveq2d 5802 . . . . . . . . . . . . 13  |-  ( m  =  ( n  + 
1 )  ->  ( S `  ( m  -  1 ) )  =  ( S `  ( ( n  + 
1 )  -  1 ) ) )
177175fveq2d 5802 . . . . . . . . . . . . . 14  |-  ( m  =  ( n  + 
1 )  ->  ( T `  ( m  -  1 ) )  =  ( T `  ( ( n  + 
1 )  -  1 ) ) )
178177oveq2d 6215 . . . . . . . . . . . . 13  |-  ( m  =  ( n  + 
1 )  ->  (
2  x.  ( T `
 ( m  - 
1 ) ) )  =  ( 2  x.  ( T `  (
( n  +  1 )  -  1 ) ) ) )
179176, 178oveq12d 6217 . . . . . . . . . . . 12  |-  ( m  =  ( n  + 
1 )  ->  (
( S `  (
m  -  1 ) )  -  ( 2  x.  ( T `  ( m  -  1
) ) ) )  =  ( ( S `
 ( ( n  +  1 )  - 
1 ) )  -  ( 2  x.  ( T `  ( (
n  +  1 )  -  1 ) ) ) ) )
180174, 179jca 532 . . . . . . . . . . 11  |-  ( m  =  ( n  + 
1 )  ->  (
( abs `  ( R `  ( x  /  m ) ) )  =  ( abs `  ( R `  ( x  /  ( n  + 
1 ) ) ) )  /\  ( ( S `  ( m  -  1 ) )  -  ( 2  x.  ( T `  (
m  -  1 ) ) ) )  =  ( ( S `  ( ( n  + 
1 )  -  1 ) )  -  (
2  x.  ( T `
 ( ( n  +  1 )  - 
1 ) ) ) ) ) )
181 oveq2 6207 . . . . . . . . . . . . . 14  |-  ( m  =  1  ->  (
x  /  m )  =  ( x  / 
1 ) )
182181fveq2d 5802 . . . . . . . . . . . . 13  |-  ( m  =  1  ->  ( R `  ( x  /  m ) )  =  ( R `  (
x  /  1 ) ) )
183182fveq2d 5802 . . . . . . . . . . . 12  |-  ( m  =  1  ->  ( abs `  ( R `  ( x  /  m
) ) )  =  ( abs `  ( R `  ( x  /  1 ) ) ) )
184 oveq1 6206 . . . . . . . . . . . . . . . . 17  |-  ( m  =  1  ->  (
m  -  1 )  =  ( 1  -  1 ) )
185 1m1e0 10500 . . . . . . . . . . . . . . . . 17  |-  ( 1  -  1 )  =  0
186184, 185syl6eq 2511 . . . . . . . . . . . . . . . 16  |-  ( m  =  1  ->  (
m  -  1 )  =  0 )
187186fveq2d 5802 . . . . . . . . . . . . . . 15  |-  ( m  =  1  ->  ( S `  ( m  -  1 ) )  =  ( S ` 
0 ) )
188 0re 9496 . . . . . . . . . . . . . . . 16  |-  0  e.  RR
189 fveq2 5798 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  0  ->  ( |_ `  a )  =  ( |_ `  0
) )
190 0z 10767 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  ZZ
191 flid 11773 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 0  e.  ZZ  ->  ( |_ `  0 )  =  0 )
192190, 191ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( |_
`  0 )  =  0
193189, 192syl6eq 2511 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  0  ->  ( |_ `  a )  =  0 )
194193oveq2d 6215 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  0  ->  (
1 ... ( |_ `  a ) )  =  ( 1 ... 0
) )
195 fz10 11586 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1 ... 0 )  =  (/)
196194, 195syl6eq 2511 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  0  ->  (
1 ... ( |_ `  a ) )  =  (/) )
197196sumeq1d 13295 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  0  ->  sum_ i  e.  ( 1 ... ( |_ `  a ) ) ( (Λ `  i
)  x.  ( ( log `  i )  +  (ψ `  (
a  /  i ) ) ) )  = 
sum_ i  e.  (/)  ( (Λ `  i )  x.  ( ( log `  i
)  +  (ψ `  ( a  /  i
) ) ) ) )
198 sum0 13315 . . . . . . . . . . . . . . . . . 18  |-  sum_ i  e.  (/)  ( (Λ `  i
)  x.  ( ( log `  i )  +  (ψ `  (
a  /  i ) ) ) )  =  0
199197, 198syl6eq 2511 . . . . . . . . . . . . . . . . 17  |-  ( a  =  0  ->  sum_ i  e.  ( 1 ... ( |_ `  a ) ) ( (Λ `  i
)  x.  ( ( log `  i )  +  (ψ `  (
a  /  i ) ) ) )  =  0 )
200199, 47, 132fvmpt 5882 . . . . . . . . . . . . . . . 16  |-  ( 0  e.  RR  ->  ( S `  0 )  =  0 )
201188, 200ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( S `
 0 )  =  0
202187, 201syl6eq 2511 . . . . . . . . . . . . . 14  |-  ( m  =  1  ->  ( S `  ( m  -  1 ) )  =  0 )
203186fveq2d 5802 . . . . . . . . . . . . . . . . 17  |-  ( m  =  1  ->  ( T `  ( m  -  1 ) )  =  ( T ` 
0 ) )
204 rpne0 11116 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  e.  RR+  ->  a  =/=  0 )
205204necon2bi 2688 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  0  ->  -.  a  e.  RR+ )
206 iffalse 3906 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  a  e.  RR+  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  0 )
207205, 206syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  0  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  0 )
208207, 81, 132fvmpt 5882 . . . . . . . . . . . . . . . . . 18  |-  ( 0  e.  RR  ->  ( T `  0 )  =  0 )
209188, 208ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( T `
 0 )  =  0
210203, 209syl6eq 2511 . . . . . . . . . . . . . . . 16  |-  ( m  =  1  ->  ( T `  ( m  -  1 ) )  =  0 )
211210oveq2d 6215 . . . . . . . . . . . . . . 15  |-  ( m  =  1  ->  (
2  x.  ( T `
 ( m  - 
1 ) ) )  =  ( 2  x.  0 ) )
212 2t0e0 10587 . . . . . . . . . . . . . . 15  |-  ( 2  x.  0 )  =  0
213211, 212syl6eq 2511 . . . . . . . . . . . . . 14  |-  ( m  =  1  ->  (
2  x.  ( T `
 ( m  - 
1 ) ) )  =  0 )
214202, 213oveq12d 6217 . . . . . . . . . . . . 13  |-  ( m  =  1  ->  (
( S `  (
m  -  1 ) )  -  ( 2  x.  ( T `  ( m  -  1
) ) ) )  =  ( 0  -  0 ) )
215 0m0e0 10541 . . . . . . . . . . . . 13  |-  ( 0  -  0 )  =  0
216214, 215syl6eq 2511 . . . . . . . . . . . 12  |-  ( m  =  1  ->  (
( S `  (
m  -  1 ) )  -  ( 2  x.  ( T `  ( m  -  1
) ) ) )  =  0 )
217183, 216jca 532 . . . . . . . . . . 11  |-  ( m  =  1  ->  (
( abs `  ( R `  ( x  /  m ) ) )  =  ( abs `  ( R `  ( x  /  1 ) ) )  /\  ( ( S `  ( m  -  1 ) )  -  ( 2  x.  ( T `  (
m  -  1 ) ) ) )  =  0 ) )
218 oveq2 6207 . . . . . . . . . . . . . 14  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (
x  /  m )  =  ( x  / 
( ( |_ `  x )  +  1 ) ) )
219218fveq2d 5802 . . . . . . . . . . . . 13  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  ( R `  ( x  /  m ) )  =  ( R `  (
x  /  ( ( |_ `  x )  +  1 ) ) ) )
220219fveq2d 5802 . . . . . . . . . . . 12  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  ( abs `  ( R `  ( x  /  m
) ) )  =  ( abs `  ( R `  ( x  /  ( ( |_
`  x )  +  1 ) ) ) ) )
221 oveq1 6206 . . . . . . . . . . . . . 14  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (
m  -  1 )  =  ( ( ( |_ `  x )  +  1 )  - 
1 ) )
222221fveq2d 5802 . . . . . . . . . . . . 13  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  ( S `  ( m  -  1 ) )  =  ( S `  ( ( ( |_
`  x )  +  1 )  -  1 ) ) )
223221fveq2d 5802 . . . . . . . . . . . . . 14  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  ( T `  ( m  -  1 ) )  =  ( T `  ( ( ( |_
`  x )  +  1 )  -  1 ) ) )
224223oveq2d 6215 . . . . . . . . . . . . 13  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (
2  x.  ( T `
 ( m  - 
1 ) ) )  =  ( 2  x.  ( T `  (
( ( |_ `  x )  +  1 )  -  1 ) ) ) )
225222, 224oveq12d 6217 . . . . . . . . . . . 12  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (
( S `  (
m  -  1 ) )  -  ( 2  x.  ( T `  ( m  -  1
) ) ) )  =  ( ( S `
 ( ( ( |_ `  x )  +  1 )  - 
1 ) )  -  ( 2  x.  ( T `  ( (
( |_ `  x
)  +  1 )  -  1 ) ) ) ) )
226220, 225jca 532 . . . . . . . . . . 11  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (
( abs `  ( R `  ( x  /  m ) ) )  =  ( abs `  ( R `  ( x  /  ( ( |_
`  x )  +  1 ) ) ) )  /\  ( ( S `  ( m  -  1 ) )  -  ( 2  x.  ( T `  (
m  -  1 ) ) ) )  =  ( ( S `  ( ( ( |_
`  x )  +  1 )  -  1 ) )  -  (
2  x.  ( T `
 ( ( ( |_ `  x )  +  1 )  - 
1 ) ) ) ) ) )
227 nnuz 11006 . . . . . . . . . . . 12  |-  NN  =  ( ZZ>= `  1 )
22815, 227syl6eleq 2552 . . . . . . . . . . 11  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  ( ZZ>= `  1
) )
22910adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  x  e.  RR+ )
230 elfznn 11594 . . . . . . . . . . . . . . . . . 18  |-  ( m  e.  ( 1 ... ( ( |_ `  x )  +  1 ) )  ->  m  e.  NN )
231230adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  m  e.  NN )
232231nnrpd 11136 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  m  e.  RR+ )
233229, 232rpdivcld 11154 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
x  /  m )  e.  RR+ )
23469ffvelrni 5950 . . . . . . . . . . . . . . 15  |-  ( ( x  /  m )  e.  RR+  ->  ( R `
 ( x  /  m ) )  e.  RR )
235233, 234syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  ( R `  ( x  /  m ) )  e.  RR )
236235recnd 9522 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  ( R `  ( x  /  m ) )  e.  CC )
237236abscld 13039 . . . . . . . . . . . 12  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  ( abs `  ( R `  ( x  /  m
) ) )  e.  RR )
238237recnd 9522 . . . . . . . . . . 11  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  ( abs `  ( R `  ( x  /  m
) ) )  e.  CC )
239231nnred 10447 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  m  e.  RR )
240 1red 9511 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  1  e.  RR )
241239, 240resubcld 9886 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
m  -  1 )  e.  RR )
24278ffvelrni 5950 . . . . . . . . . . . . . 14  |-  ( ( m  -  1 )  e.  RR  ->  ( S `  ( m  -  1 ) )  e.  RR )
243241, 242syl 16 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  ( S `  ( m  -  1 ) )  e.  RR )
24422a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  2  e.  RR )
24587ffvelrni 5950 . . . . . . . . . . . . . . 15  |-  ( ( m  -  1 )  e.  RR  ->  ( T `  ( m  -  1 ) )  e.  RR )
246241, 245syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  ( T `  ( m  -  1 ) )  e.  RR )
247244, 246remulcld 9524 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
2  x.  ( T `
 ( m  - 
1 ) ) )  e.  RR )
248243, 247resubcld 9886 . . . . . . . . . . . 12  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
( S `  (
m  -  1 ) )  -  ( 2  x.  ( T `  ( m  -  1
) ) ) )  e.  RR )
249248recnd 9522 . . . . . . . . . . 11  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
( S `  (
m  -  1 ) )  -  ( 2  x.  ( T `  ( m  -  1
) ) ) )  e.  CC )
250171, 180, 217, 226, 228, 238, 249fsumparts 13386 . . . . . . . . . 10  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1..^ ( ( |_ `  x )  +  1 ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( ( S `  ( ( n  +  1 )  -  1 ) )  -  ( 2  x.  ( T `  (
( n  +  1 )  -  1 ) ) ) )  -  ( ( S `  ( n  -  1
) )  -  (
2  x.  ( T `
 ( n  - 
1 ) ) ) ) ) )  =  ( ( ( ( abs `  ( R `
 ( x  / 
( ( |_ `  x )  +  1 ) ) ) )  x.  ( ( S `
 ( ( ( |_ `  x )  +  1 )  - 
1 ) )  -  ( 2  x.  ( T `  ( (
( |_ `  x
)  +  1 )  -  1 ) ) ) ) )  -  ( ( abs `  ( R `  ( x  /  1 ) ) )  x.  0 ) )  -  sum_ n  e.  ( 1..^ ( ( |_ `  x )  +  1 ) ) ( ( ( abs `  ( R `  (
x  /  ( n  +  1 ) ) ) )  -  ( abs `  ( R `  ( x  /  n
) ) ) )  x.  ( ( S `
 ( ( n  +  1 )  - 
1 ) )  -  ( 2  x.  ( T `  ( (
n  +  1 )  -  1 ) ) ) ) ) ) )
251147recnd 9522 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( S `  n )  e.  CC )
25287ffvelrni 5950 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  RR  ->  ( T `  n )  e.  RR )
253145, 252syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  n )  e.  RR )
254148, 253remulcld 9524 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( T `  n ) )  e.  RR )
255254recnd 9522 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( T `  n ) )  e.  CC )
256 1red 9511 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR )
257145, 256resubcld 9886 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  -  1 )  e.  RR )
25878ffvelrni 5950 . . . . . . . . . . . . . . . 16  |-  ( ( n  -  1 )  e.  RR  ->  ( S `  ( n  -  1 ) )  e.  RR )
259257, 258syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( S `  ( n  -  1 ) )  e.  RR )
260259recnd 9522 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( S `  ( n  -  1 ) )  e.  CC )
26187ffvelrni 5950 . . . . . . . . . . . . . . . . 17  |-  ( ( n  -  1 )  e.  RR  ->  ( T `  ( n  -  1 ) )  e.  RR )
262257, 261syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  ( n  -  1 ) )  e.  RR )
263148, 262remulcld 9524 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( T `  ( n  -  1
) ) )  e.  RR )
264263recnd 9522 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( T `  ( n  -  1
) ) )  e.  CC )
265251, 255, 260, 264sub4d 9878 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( S `  n
)  -  ( 2  x.  ( T `  n ) ) )  -  ( ( S `
 ( n  - 
1 ) )  -  ( 2  x.  ( T `  ( n  -  1 ) ) ) ) )  =  ( ( ( S `
 n )  -  ( S `  ( n  -  1 ) ) )  -  ( ( 2  x.  ( T `
 n ) )  -  ( 2  x.  ( T `  (
n  -  1 ) ) ) ) ) )
266124oveq2d 6215 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( T `  ( ( n  + 
1 )  -  1 ) ) )  =  ( 2  x.  ( T `  n )
) )
267123, 266oveq12d 6217 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( S `  ( (
n  +  1 )  -  1 ) )  -  ( 2  x.  ( T `  (
( n  +  1 )  -  1 ) ) ) )  =  ( ( S `  n )  -  (
2  x.  ( T `
 n ) ) ) )
268267oveq1d 6214 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( S `  (
( n  +  1 )  -  1 ) )  -  ( 2  x.  ( T `  ( ( n  + 
1 )  -  1 ) ) ) )  -  ( ( S `
 ( n  - 
1 ) )  -  ( 2  x.  ( T `  ( n  -  1 ) ) ) ) )  =  ( ( ( S `
 n )  -  ( 2  x.  ( T `  n )
) )  -  (
( S `  (
n  -  1 ) )  -  ( 2  x.  ( T `  ( n  -  1
) ) ) ) ) )
269 2cnd 10504 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  2  e.  CC )
270253recnd 9522 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  n )  e.  CC )
271262recnd 9522 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  ( n  -  1 ) )  e.  CC )
272269, 270, 271subdid 9910 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( ( T `
 n )  -  ( T `  ( n  -  1 ) ) ) )  =  ( ( 2  x.  ( T `  n )
)  -  ( 2  x.  ( T `  ( n  -  1
) ) ) ) )
273272oveq2d 6215 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( S `  n
)  -  ( S `
 ( n  - 
1 ) ) )  -  ( 2  x.  ( ( T `  n )  -  ( T `  ( n  -  1 ) ) ) ) )  =  ( ( ( S `
 n )  -  ( S `  ( n  -  1 ) ) )  -  ( ( 2  x.  ( T `
 n ) )  -  ( 2  x.  ( T `  (
n  -  1 ) ) ) ) ) )
274265, 268, 2733eqtr4d 2505 . . . . . . . . . . . 12  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( S `  (
( n  +  1 )  -  1 ) )  -  ( 2  x.  ( T `  ( ( n  + 
1 )  -  1 ) ) ) )  -  ( ( S `
 ( n  - 
1 ) )  -  ( 2  x.  ( T `  ( n  -  1 ) ) ) ) )  =  ( ( ( S `
 n )  -  ( S `  ( n  -  1 ) ) )  -  ( 2  x.  ( ( T `
 n )  -  ( T `  ( n  -  1 ) ) ) ) ) )
275274oveq2d 6215 . . . . . . . . . . 11  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  ( ( ( S `
 ( ( n  +  1 )  - 
1 ) )  -  ( 2  x.  ( T `  ( (
n  +  1 )  -  1 ) ) ) )  -  (
( S `  (
n  -  1 ) )  -  ( 2  x.  ( T `  ( n  -  1
) ) ) ) ) )  =  ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( ( S `  n )  -  ( S `  ( n  -  1
) ) )  -  ( 2  x.  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) ) ) ) ) )
27699, 275sumeq12rdv 13301 . . . . . . . . . 10  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1..^ ( ( |_ `  x )  +  1 ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( ( S `  ( ( n  +  1 )  -  1 ) )  -  ( 2  x.  ( T `  (
( n  +  1 )  -  1 ) ) ) )  -  ( ( S `  ( n  -  1
) )  -  (
2  x.  ( T `
 ( n  - 
1 ) ) ) ) ) )  = 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( ( S `  n )  -  ( S `  ( n  -  1
) ) )  -  ( 2  x.  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) ) ) ) ) )
277250, 276eqtr3d 2497 . . . . . . . . 9  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( ( abs `  ( R `  (
x  /  ( ( |_ `  x )  +  1 ) ) ) )  x.  (
( S `  (
( ( |_ `  x )  +  1 )  -  1 ) )  -  ( 2  x.  ( T `  ( ( ( |_
`  x )  +  1 )  -  1 ) ) ) ) )  -  ( ( abs `  ( R `
 ( x  / 
1 ) ) )  x.  0 ) )  -  sum_ n  e.  ( 1..^ ( ( |_
`  x )  +  1 ) ) ( ( ( abs `  ( R `  ( x  /  ( n  + 
1 ) ) ) )  -  ( abs `  ( R `  (
x  /  n ) ) ) )  x.  ( ( S `  ( ( n  + 
1 )  -  1 ) )  -  (
2  x.  ( T `
 ( ( n  +  1 )  - 
1 ) ) ) ) ) )  = 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( ( S `  n )  -  ( S `  ( n  -  1
) ) )  -  ( 2  x.  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) ) ) ) ) )
278157, 159fsumcl 13327 . . . . . . . . . 10  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( abs `  ( R `  (
x  /  n ) ) )  -  ( abs `  ( R `  ( x  /  (
n  +  1 ) ) ) ) )  x.  ( ( S `
 n )  -  ( 2  x.  (
n  x.  ( log `  n ) ) ) ) )  e.  CC )
27993, 278subnegd 9836 . . . . . . . . 9  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( x  / 
( ( |_ `  x )  +  1 ) )  x.  (
( S `  x
)  -  ( 2  x.  ( T `  ( |_ `  x ) ) ) ) )  -  -u sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( ( abs `  ( R `  (
x  /  n ) ) )  -  ( abs `  ( R `  ( x  /  (
n  +  1 ) ) ) ) )  x.  ( ( S `
 n )  -  ( 2  x.  (
n  x.  ( log `  n ) ) ) ) ) )  =  ( ( ( x  /  ( ( |_
`  x )  +  1 ) )  x.  ( ( S `  x )  -  (
2  x.  ( T `
 ( |_ `  x ) ) ) ) )  +  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( ( abs `  ( R `  ( x  /  n ) ) )  -  ( abs `  ( R `  ( x  /  ( n  + 
1 ) ) ) ) )  x.  (
( S `  n
)  -  ( 2  x.  ( n  x.  ( log `  n
) ) ) ) ) ) )
280162, 277, 2793eqtr3rd 2504 . . . . . . . 8  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( x  / 
( ( |_ `  x )  +  1 ) )  x.  (
( S `  x
)  -  ( 2  x.  ( T `  ( |_ `  x ) ) ) ) )  +  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( ( abs `  ( R `  (
x  /  n ) ) )  -  ( abs `  ( R `  ( x  /  (
n  +  1 ) ) ) ) )  x.  ( ( S `
 n )  -  ( 2  x.  (
n  x.  ( log `  n ) ) ) ) ) )  = 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( ( S `  n )  -  ( S `  ( n  -  1
) ) )  -  ( 2  x.  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) ) ) ) ) )
28110relogcld 22204 . . . . . . . . . 10  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  e.  RR )
282281recnd 9522 . . . . . . . . 9  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  e.  CC )
28366, 282mulcomd 9517 . . . . . . . 8  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  x.  ( log `  x ) )  =  ( ( log `  x
)  x.  x ) )
284280, 283oveq12d 6217 . . . . . . 7  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( ( x  /  ( ( |_
`  x )  +  1 ) )  x.  ( ( S `  x )  -  (
2  x.  ( T `
 ( |_ `  x ) ) ) ) )  +  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( ( abs `  ( R `  ( x  /  n ) ) )  -  ( abs `  ( R `  ( x  /  ( n  + 
1 ) ) ) ) )  x.  (
( S `  n
)  -  ( 2  x.  ( n  x.  ( log `  n
) ) ) ) ) )  /  (
x  x.  ( log `  x ) ) )  =  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( ( S `  n )  -  ( S `  ( n  -  1
) ) )  -  ( 2  x.  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) ) ) ) )  / 
( ( log `  x
)  x.  x ) ) )
285147, 259resubcld 9886 . . . . . . . . . . . 12  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( S `  n )  -  ( S `  ( n  -  1
) ) )  e.  RR )
286253, 262resubcld 9886 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( T `  n )  -  ( T `  ( n  -  1
) ) )  e.  RR )
287148, 286remulcld 9524 . . . . . . . . . . . 12  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( ( T `
 n )  -  ( T `  ( n  -  1 ) ) ) )  e.  RR )
288285, 287resubcld 9886 . . . . . . . . . . 11  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( S `  n
)  -  ( S `
 ( n  - 
1 ) ) )  -  ( 2  x.  ( ( T `  n )  -  ( T `  ( n  -  1 ) ) ) ) )  e.  RR )
289108, 288remulcld 9524 . . . . . . . . . 10  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  ( ( ( S `
 n )  -  ( S `  ( n  -  1 ) ) )  -  ( 2  x.  ( ( T `
 n )  -  ( T `  ( n  -  1 ) ) ) ) ) )  e.  RR )
290157, 289fsumrecl 13328 . . . . . . . . 9  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( ( S `  n )  -  ( S `  ( n  -  1
) ) )  -  ( 2  x.  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) ) ) ) )  e.  RR )
291290recnd 9522 . . . . . . . 8  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( ( S `  n )  -  ( S `  ( n  -  1
) ) )  -  ( 2  x.  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) ) ) ) )  e.  CC )
2922, 8rplogcld 22210 . . . . . . . . 9  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  e.  RR+ )
293292rpne0d 11142 . . . . . . . 8  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  =/=  0 )
29410rpne0d 11142 . . . . . . . 8  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  x  =/=  0 )
295291, 282, 66, 293, 294divdiv1d 10248 . . . . . . 7  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( ( S `  n )  -  ( S `  ( n  -  1
) ) )  -  ( 2  x.  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) ) ) ) )  / 
( log `  x
) )  /  x
)  =  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( ( ( S `  n )  -  ( S `  ( n  -  1
) ) )  -  ( 2  x.  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) ) ) ) )  / 
( ( log `  x
)  x.  x ) ) )
296284, 295eqtr4d 2498 . . . . . 6  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( ( x  /  ( ( |_
`  x )  +  1 ) )  x.  ( ( S `  x )  -  (
2  x.  ( T `
 ( |_ `  x ) ) ) ) )  +  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( ( abs `  ( R `  ( x  /  n ) ) )  -  ( abs `  ( R `  ( x  /  ( n  + 
1 ) ) ) ) )  x.  (
( S `  n
)  -  ( 2  x.  ( n  x.  ( log `  n
) ) ) ) ) )  /  (
x  x.  ( log `  x ) ) )  =  ( ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( ( ( S `  n )  -  ( S `  ( n  -  1
) ) )  -  ( 2  x.  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) ) ) ) )  / 
( log `  x
) )  /  x
) )
297296oveq2d 6215 . . . . 5  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( ( ( abs `  ( R `
 x ) )  x.  ( log `  x
) )  -  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( S `
 n )  -  ( S `  ( n  -  1 ) ) ) )  /  ( log `  x ) ) )  /  x )  +  ( ( ( ( x  /  (
( |_ `  x
)  +  1 ) )  x.  ( ( S `  x )  -  ( 2  x.  ( T `  ( |_ `  x ) ) ) ) )  + 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( ( abs `  ( R `  ( x  /  n ) ) )  -  ( abs `  ( R `  ( x  /  ( n  + 
1 ) ) ) ) )  x.  (
( S `  n
)  -  ( 2  x.  ( n  x.  ( log `  n
) ) ) ) ) )  /  (
x  x.  ( log `  x ) ) ) )  =  ( ( ( ( ( abs `  ( R `  x
) )  x.  ( log `  x ) )  -  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( S `
 n )  -  ( S `  ( n  -  1 ) ) ) )  /  ( log `  x ) ) )  /  x )  +  ( ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( ( ( S `  n )  -  ( S `  ( n  -  1
) ) )  -  ( 2  x.  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) ) ) ) )  / 
( log `  x
) )  /  x
) ) )
29871recnd 9522 . . . . . . . . . 10  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( R `  x )  e.  CC )
299298abscld 13039 . . . . . . . . 9  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( R `  x ) )  e.  RR )
300299, 281remulcld 9524 . . . . . . . 8  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( abs `  ( R `  x )
)  x.  ( log `  x ) )  e.  RR )
301108, 285remulcld 9524 . . . . . . . . . 10  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  ( ( S `  n )  -  ( S `  ( n  -  1 ) ) ) )  e.  RR )
302157, 301fsumrecl 13328 . . . . . . . . 9  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( S `
 n )  -  ( S `  ( n  -  1 ) ) ) )  e.  RR )
303302, 292rerpdivcld 11164 . . . . . . . 8  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( S `
 n )  -  ( S `  ( n  -  1 ) ) ) )  /  ( log `  x ) )  e.  RR )
304300, 303resubcld 9886 . . . . . . 7  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( abs `  ( R `  x )
)  x.  ( log `  x ) )  -  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( S `
 n )  -  ( S `  ( n  -  1 ) ) ) )  /  ( log `  x ) ) )  e.  RR )
305304recnd 9522 . . . . . 6  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( abs `  ( R `  x )
)  x.  ( log `  x ) )  -  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( S `
 n )  -  ( S `  ( n  -  1 ) ) ) )  /  ( log `  x ) ) )  e.  CC )
306291, 282, 293divcld 10217 . . . . . 6  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( ( S `  n )  -  ( S `  ( n  -  1
) ) )  -  ( 2  x.  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) ) ) ) )  / 
( log `  x
) )  e.  CC )
307305, 306, 66, 294divdird 10255 . . . . 5  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( ( ( abs `  ( R `
 x ) )  x.  ( log `  x
) )  -  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( S `
 n )  -  ( S `  ( n  -  1 ) ) ) )  /  ( log `  x ) ) )  +  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( ( ( S `  n )  -  ( S `  ( n  -  1
) ) )  -  ( 2  x.  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) ) ) ) )  / 
( log `  x
) ) )  /  x )  =  ( ( ( ( ( abs `  ( R `
 x ) )  x.  ( log `  x
) )  -  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( S `
 n )  -  ( S `  ( n  -  1 ) ) ) )  /  ( log `  x ) ) )  /  x )  +  ( ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( ( ( S `  n )  -  ( S `  ( n  -  1
) ) )  -  ( 2  x.  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) ) ) ) )  / 
( log `  x
) )  /  x
) ) )
308300recnd 9522 . . . . . . . 8  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( abs `  ( R `  x )
)  x.  ( log `  x ) )  e.  CC )
309303recnd 9522 . . . . . . . 8  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( S `
 n )  -  ( S `  ( n  -  1 ) ) ) )  /  ( log `  x ) )  e.  CC )
310308, 309, 306subsubd 9857 . . . . . . 7  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( abs `  ( R `  x )
)  x.  ( log `  x ) )  -  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( S `
 n )  -  ( S `  ( n  -  1 ) ) ) )  /  ( log `  x ) )  -  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( ( S `  n )  -  ( S `  ( n  -  1
) ) )  -  ( 2  x.  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) ) ) ) )  / 
( log `  x
) ) ) )  =  ( ( ( ( abs `  ( R `  x )
)  x.  ( log `  x ) )  -  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( S `
 n )  -  ( S `  ( n  -  1 ) ) ) )  /  ( log `  x ) ) )  +  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( ( ( S `  n )  -  ( S `  ( n  -  1
) ) )  -  ( 2  x.  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) ) ) ) )  / 
( log `  x
) ) ) )
311 2cnd 10504 . . . . . . . . . . . 12  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  2  e.  CC )
312270, 271subcld 9829 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( T `  n )  -  ( T `  ( n  -  1
) ) )  e.  CC )
313109, 312mulcld 9516 . . . . . . . . . . . 12  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  ( ( T `  n )  -  ( T `  ( n  -  1 ) ) ) )  e.  CC )
314157, 311, 313fsummulc2 13368 . . . . . . . . . . 11  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
2  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( T `
 n )  -  ( T `  ( n  -  1 ) ) ) ) )  = 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( 2  x.  ( ( abs `  ( R `
 ( x  /  n ) ) )  x.  ( ( T `
 n )  -  ( T `  ( n  -  1 ) ) ) ) ) )
315285recnd 9522 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( S `  n )  -  ( S `  ( n  -  1
) ) )  e.  CC )
316269, 312mulcld 9516 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( ( T `
 n )  -  ( T `  ( n  -  1 ) ) ) )  e.  CC )
317315, 316nncand 9834 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( S `  n
)  -  ( S `
 ( n  - 
1 ) ) )  -  ( ( ( S `  n )  -  ( S `  ( n  -  1
) ) )  -  ( 2  x.  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) ) ) ) )  =  ( 2  x.  (
( T `  n
)  -  ( T `
 ( n  - 
1 ) ) ) ) )
318317oveq2d 6215 . . . . . . . . . . . . 13