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

Theorem pntrlog2bndlem4 20745
Description: Lemma for pntrlog2bnd 20749. 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 10702 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( 1 (,) 
+oo )  ->  x  e.  RR )
21adantl 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  RR )
3 1rp 10374 . . . . . . . . . . . . . . . . . . . 20  |-  1  e.  RR+
43a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  RR+ )
5 1re 8853 . . . . . . . . . . . . . . . . . . . . 21  |-  1  e.  RR
65a1i 10 . . . . . . . . . . . . . . . . . . . 20  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  RR )
7 eliooord 10726 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( 1 (,) 
+oo )  ->  (
1  <  x  /\  x  <  +oo ) )
87adantl 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  <  x  /\  x  <  +oo ) )
98simpld 445 . . . . . . . . . . . . . . . . . . . 20  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  <  x )
106, 2, 9ltled 8983 . . . . . . . . . . . . . . . . . . 19  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  <_  x )
112, 4, 10rpgecld 10441 . . . . . . . . . . . . . . . . . 18  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  RR+ )
1211rprege0d 10413 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  e.  RR  /\  0  <_  x ) )
13 flge0nn0 10964 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  RR  /\  0  <_  x )  -> 
( |_ `  x
)  e.  NN0 )
1412, 13syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( |_ `  x )  e. 
NN0 )
15 nn0p1nn 10019 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( |_ `  x )  e.  NN0  ->  ( ( |_ `  x )  +  1 )  e.  NN )
1614, 15syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  NN )
1716nnrpd 10405 . . . . . . . . . . . . . . . . . 18  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  RR+ )
1811, 17rpdivcld 10423 . . . . . . . . . . . . . . . . 17  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  e.  RR+ )
19 pntrlog2bnd.r . . . . . . . . . . . . . . . . . 18  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
2019pntrval 20727 . . . . . . . . . . . . . . . . 17  |-  ( ( x  /  ( ( |_ `  x )  +  1 ) )  e.  RR+  ->  ( R `
 ( x  / 
( ( |_ `  x )  +  1 ) ) )  =  ( (ψ `  (
x  /  ( ( |_ `  x )  +  1 ) ) )  -  ( x  /  ( ( |_
`  x )  +  1 ) ) ) )
2118, 20syl 15 . . . . . . . . . . . . . . . 16  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( R `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  =  ( (ψ `  ( x  /  (
( |_ `  x
)  +  1 ) ) )  -  (
x  /  ( ( |_ `  x )  +  1 ) ) ) )
222, 16nndivred 9810 . . . . . . . . . . . . . . . . . . 19  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  e.  RR )
23 2re 9831 . . . . . . . . . . . . . . . . . . . 20  |-  2  e.  RR
2423a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  2  e.  RR )
25 flltp1 10948 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  x  <  ( ( |_ `  x )  +  1 ) )
262, 25syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  <  ( ( |_ `  x )  +  1 ) )
2716nncnd 9778 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  CC )
2827mulid1d 8868 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( |_ `  x )  +  1 )  x.  1 )  =  ( ( |_
`  x )  +  1 ) )
2926, 28breqtrrd 4065 . . . . . . . . . . . . . . . . . . . 20  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  <  ( ( ( |_
`  x )  +  1 )  x.  1 ) )
302, 6, 17ltdivmuld 10453 . . . . . . . . . . . . . . . . . . . 20  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( x  /  (
( |_ `  x
)  +  1 ) )  <  1  <->  x  <  ( ( ( |_
`  x )  +  1 )  x.  1 ) ) )
3129, 30mpbird 223 . . . . . . . . . . . . . . . . . . 19  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  <  1 )
32 1lt2 9902 . . . . . . . . . . . . . . . . . . . 20  |-  1  <  2
3332a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  <  2 )
3422, 6, 24, 31, 33lttrd 8993 . . . . . . . . . . . . . . . . . 18  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  <  2 )
35 chpeq0 20463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  /  ( ( |_ `  x )  +  1 ) )  e.  RR  ->  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  =  0  <->  ( x  /  ( ( |_
`  x )  +  1 ) )  <  2 ) )
3622, 35syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  =  0  <->  ( x  /  ( ( |_
`  x )  +  1 ) )  <  2 ) )
3734, 36mpbird 223 . . . . . . . . . . . . . . . . 17  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (ψ `  ( x  /  (
( |_ `  x
)  +  1 ) ) )  =  0 )
3837oveq1d 5889 . . . . . . . . . . . . . . . 16  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  -  ( x  / 
( ( |_ `  x )  +  1 ) ) )  =  ( 0  -  (
x  /  ( ( |_ `  x )  +  1 ) ) ) )
3921, 38eqtrd 2328 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( R `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  =  ( 0  -  ( x  /  (
( |_ `  x
)  +  1 ) ) ) )
4039fveq2d 5545 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( abs `  ( R `  ( x  /  (
( |_ `  x
)  +  1 ) ) ) )  =  ( abs `  (
0  -  ( x  /  ( ( |_
`  x )  +  1 ) ) ) ) )
41 0re 8854 . . . . . . . . . . . . . . . 16  |-  0  e.  RR
4241a1i 10 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  e.  RR )
4318rpge0d 10410 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <_  ( x  /  (
( |_ `  x
)  +  1 ) ) )
4442, 22, 43abssuble0d 11931 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( abs `  ( 0  -  ( x  /  (
( |_ `  x
)  +  1 ) ) ) )  =  ( ( x  / 
( ( |_ `  x )  +  1 ) )  -  0 ) )
4522recnd 8877 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  e.  CC )
4645subid1d 9162 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( x  /  (
( |_ `  x
)  +  1 ) )  -  0 )  =  ( x  / 
( ( |_ `  x )  +  1 ) ) )
4740, 44, 463eqtrd 2332 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( abs `  ( R `  ( x  /  (
( |_ `  x
)  +  1 ) ) ) )  =  ( x  /  (
( |_ `  x
)  +  1 ) ) )
4814nn0red 10035 . . . . . . . . . . . . . . . 16  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( |_ `  x )  e.  RR )
49 pntsval.1 . . . . . . . . . . . . . . . . 17  |-  S  =  ( a  e.  RR  |->  sum_ i  e.  ( 1 ... ( |_ `  a ) ) ( (Λ `  i )  x.  ( ( log `  i
)  +  (ψ `  ( a  /  i
) ) ) ) )
5049pntsval2 20741 . . . . . . . . . . . . . . . 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
) ) ) ) )
5148, 50syl 15 . . . . . . . . . . . . . . 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
) ) ) ) )
5214nn0cnd 10036 . . . . . . . . . . . . . . . . 17  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( |_ `  x )  e.  CC )
53 ax-1cn 8811 . . . . . . . . . . . . . . . . . 18  |-  1  e.  CC
5453a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  CC )
5552, 54pncand 9174 . . . . . . . . . . . . . . . 16  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( |_ `  x )  +  1 )  -  1 )  =  ( |_ `  x ) )
5655fveq2d 5545 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( S `  ( (
( |_ `  x
)  +  1 )  -  1 ) )  =  ( S `  ( |_ `  x ) ) )
5749pntsval2 20741 . . . . . . . . . . . . . . . . 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 ) ) ) ) )
582, 57syl 15 . . . . . . . . . . . . . . . 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 ) ) ) ) )
59 flidm 10956 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  RR  ->  ( |_ `  ( |_ `  x ) )  =  ( |_ `  x
) )
602, 59syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( |_ `  ( |_ `  x ) )  =  ( |_ `  x
) )
6160oveq2d 5890 . . . . . . . . . . . . . . . . 17  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1 ... ( |_ `  ( |_ `  x ) ) )  =  ( 1 ... ( |_
`  x ) ) )
6261sumeq1d 12190 . . . . . . . . . . . . . . . 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 ) ) ) ) )
6358, 62eqtr4d 2331 . . . . . . . . . . . . . . 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 ) ) ) ) )
6451, 56, 633eqtr4d 2338 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( S `  ( (
( |_ `  x
)  +  1 )  -  1 ) )  =  ( S `  x ) )
6555fveq2d 5545 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( T `  ( (
( |_ `  x
)  +  1 )  -  1 ) )  =  ( T `  ( |_ `  x ) ) )
6665oveq2d 5890 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  ( T `
 ( ( ( |_ `  x )  +  1 )  - 
1 ) ) )  =  ( 2  x.  ( T `  ( |_ `  x ) ) ) )
6764, 66oveq12d 5892 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( S `  (
( ( |_ `  x )  +  1 )  -  1 ) )  -  ( 2  x.  ( T `  ( ( ( |_
`  x )  +  1 )  -  1 ) ) ) )  =  ( ( S `
 x )  -  ( 2  x.  ( T `  ( |_ `  x ) ) ) ) )
6847, 67oveq12d 5892 . . . . . . . . . . . 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 ) ) ) ) ) )
692recnd 8877 . . . . . . . . . . . . . . . . . . 19  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  CC )
7069div1d 9544 . . . . . . . . . . . . . . . . . 18  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  /  1 )  =  x )
7170fveq2d 5545 . . . . . . . . . . . . . . . . 17  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( R `  ( x  /  1 ) )  =  ( R `  x ) )
7219pntrf 20728 . . . . . . . . . . . . . . . . . . 19  |-  R : RR+
--> RR
7372ffvelrni 5680 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  RR+  ->  ( R `
 x )  e.  RR )
7411, 73syl 15 . . . . . . . . . . . . . . . . 17  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( R `  x )  e.  RR )
7571, 74eqeltrd 2370 . . . . . . . . . . . . . . . 16  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( R `  ( x  /  1 ) )  e.  RR )
7675recnd 8877 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( R `  ( x  /  1 ) )  e.  CC )
7776abscld 11934 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( abs `  ( R `  ( x  /  1
) ) )  e.  RR )
7877recnd 8877 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( abs `  ( R `  ( x  /  1
) ) )  e.  CC )
7978mul01d 9027 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( abs `  ( R `  ( x  /  1 ) ) )  x.  0 )  =  0 )
8068, 79oveq12d 5892 . . . . . . . . . . 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 ) )
8149pntsf 20738 . . . . . . . . . . . . . . . . 17  |-  S : RR
--> RR
8281ffvelrni 5680 . . . . . . . . . . . . . . . 16  |-  ( x  e.  RR  ->  ( S `  x )  e.  RR )
832, 82syl 15 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( S `  x )  e.  RR )
84 pntrlog2bnd.t . . . . . . . . . . . . . . . . . . 19  |-  T  =  ( a  e.  RR  |->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 ) )
85 relogcl 19948 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  e.  RR+  ->  ( log `  a )  e.  RR )
86 remulcl 8838 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( a  e.  RR  /\  ( log `  a )  e.  RR )  -> 
( a  x.  ( log `  a ) )  e.  RR )
8785, 86sylan2 460 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( a  e.  RR  /\  a  e.  RR+ )  -> 
( a  x.  ( log `  a ) )  e.  RR )
8841a1i 10 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( a  e.  RR  /\  -.  a  e.  RR+ )  ->  0  e.  RR )
8987, 88ifclda 3605 . . . . . . . . . . . . . . . . . . 19  |-  ( a  e.  RR  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  e.  RR )
9084, 89fmpti 5699 . . . . . . . . . . . . . . . . . 18  |-  T : RR
--> RR
9190ffvelrni 5680 . . . . . . . . . . . . . . . . 17  |-  ( ( |_ `  x )  e.  RR  ->  ( T `  ( |_ `  x ) )  e.  RR )
9248, 91syl 15 . . . . . . . . . . . . . . . 16  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( T `  ( |_ `  x ) )  e.  RR )
9324, 92remulcld 8879 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  ( T `
 ( |_ `  x ) ) )  e.  RR )
9483, 93resubcld 9227 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( S `  x
)  -  ( 2  x.  ( T `  ( |_ `  x ) ) ) )  e.  RR )
9522, 94remulcld 8879 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( x  /  (
( |_ `  x
)  +  1 ) )  x.  ( ( S `  x )  -  ( 2  x.  ( T `  ( |_ `  x ) ) ) ) )  e.  RR )
9695recnd 8877 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( x  /  (
( |_ `  x
)  +  1 ) )  x.  ( ( S `  x )  -  ( 2  x.  ( T `  ( |_ `  x ) ) ) ) )  e.  CC )
9796subid1d 9162 . . . . . . . . . . 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 ) ) ) ) ) )
9880, 97eqtrd 2328 . . . . . . . . . 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 ) ) ) ) ) )
992flcld 10946 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( |_ `  x )  e.  ZZ )
100 fzval3 10927 . . . . . . . . . . . . . 14  |-  ( ( |_ `  x )  e.  ZZ  ->  (
1 ... ( |_ `  x ) )  =  ( 1..^ ( ( |_ `  x )  +  1 ) ) )
10199, 100syl 15 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1 ... ( |_ `  x ) )  =  ( 1..^ ( ( |_ `  x )  +  1 ) ) )
102101eqcomd 2301 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1..^ ( ( |_
`  x )  +  1 ) )  =  ( 1 ... ( |_ `  x ) ) )
10311adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR+ )
104 elfznn 10835 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
105104adantl 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
106105nnrpd 10405 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR+ )
107103, 106rpdivcld 10423 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
10872ffvelrni 5680 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  /  n )  e.  RR+  ->  ( R `
 ( x  /  n ) )  e.  RR )
109107, 108syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  e.  RR )
110109recnd 8877 . . . . . . . . . . . . . . . . . 18  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  e.  CC )
111110abscld 11934 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( R `  (
x  /  n ) ) )  e.  RR )
112111recnd 8877 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( R `  (
x  /  n ) ) )  e.  CC )
1133a1i 10 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR+ )
114106, 113rpaddcld 10421 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  +  1 )  e.  RR+ )
115103, 114rpdivcld 10423 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  ( n  + 
1 ) )  e.  RR+ )
11672ffvelrni 5680 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  /  ( n  +  1 ) )  e.  RR+  ->  ( R `
 ( x  / 
( n  +  1 ) ) )  e.  RR )
117115, 116syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  (
n  +  1 ) ) )  e.  RR )
118117recnd 8877 . . . . . . . . . . . . . . . . . 18  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  (
n  +  1 ) ) )  e.  CC )
119118abscld 11934 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( R `  (
x  /  ( n  +  1 ) ) ) )  e.  RR )
120119recnd 8877 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( R `  (
x  /  ( n  +  1 ) ) ) )  e.  CC )
121112, 120negsubdi2d 9189 . . . . . . . . . . . . . . 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 ) ) ) ) )
122121eqcomd 2301 . . . . . . . . . . . . . 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 ) ) ) ) ) )
123105nncnd 9778 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  CC )
12453a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  CC )
125123, 124pncand 9174 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
n  +  1 )  -  1 )  =  n )
126125fveq2d 5545 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( S `  ( ( n  + 
1 )  -  1 ) )  =  ( S `  n ) )
127125fveq2d 5545 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  ( ( n  + 
1 )  -  1 ) )  =  ( T `  n ) )
128 rpre 10376 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  RR+  ->  n  e.  RR )
129 eleq1 2356 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  n  ->  (
a  e.  RR+  <->  n  e.  RR+ ) )
130 id 19 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  n  ->  a  =  n )
131 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  n  ->  ( log `  a )  =  ( log `  n
) )
132130, 131oveq12d 5892 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  n  ->  (
a  x.  ( log `  a ) )  =  ( n  x.  ( log `  n ) ) )
133 eqidd 2297 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  n  ->  0  =  0 )
134129, 132, 133ifbieq12d 3600 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  n  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  if ( n  e.  RR+ ,  ( n  x.  ( log `  n
) ) ,  0 ) )
135 ovex 5899 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  x.  ( log `  n
) )  e.  _V
136 c0ex 8848 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  _V
137135, 136ifex 3636 . . . . . . . . . . . . . . . . . . . . 21  |-  if ( n  e.  RR+ ,  ( n  x.  ( log `  n ) ) ,  0 )  e.  _V
138134, 84, 137fvmpt 5618 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  RR  ->  ( T `  n )  =  if ( n  e.  RR+ ,  ( n  x.  ( log `  n
) ) ,  0 ) )
139128, 138syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  RR+  ->  ( T `
 n )  =  if ( n  e.  RR+ ,  ( n  x.  ( log `  n
) ) ,  0 ) )
140 iftrue 3584 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  RR+  ->  if ( n  e.  RR+ ,  ( n  x.  ( log `  n ) ) ,  0 )  =  ( n  x.  ( log `  n ) ) )
141139, 140eqtrd 2328 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  RR+  ->  ( T `
 n )  =  ( n  x.  ( log `  n ) ) )
142106, 141syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  n )  =  ( n  x.  ( log `  n ) ) )
143127, 142eqtrd 2328 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  ( ( n  + 
1 )  -  1 ) )  =  ( n  x.  ( log `  n ) ) )
144143oveq2d 5890 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( T `  ( ( n  + 
1 )  -  1 ) ) )  =  ( 2  x.  (
n  x.  ( log `  n ) ) ) )
145126, 144oveq12d 5892 . . . . . . . . . . . . . 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
) ) ) ) )
146122, 145oveq12d 5892 . . . . . . . . . . . . 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 ) ) ) ) ) )
147111, 119resubcld 9227 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  -  ( abs `  ( R `
 ( x  / 
( n  +  1 ) ) ) ) )  e.  RR )
148147recnd 8877 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  -  ( abs `  ( R `
 ( x  / 
( n  +  1 ) ) ) ) )  e.  CC )
149105nnred 9777 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR )
15081ffvelrni 5680 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  RR  ->  ( S `  n )  e.  RR )
151149, 150syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( S `  n )  e.  RR )
15223a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  2  e.  RR )
153106relogcld 19990 . . . . . . . . . . . . . . . . . 18  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  n )  e.  RR )
154149, 153remulcld 8879 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  x.  ( log `  n
) )  e.  RR )
155152, 154remulcld 8879 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( n  x.  ( log `  n
) ) )  e.  RR )
156151, 155resubcld 9227 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( S `  n )  -  ( 2  x.  ( n  x.  ( log `  n ) ) ) )  e.  RR )
157156recnd 8877 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( S `  n )  -  ( 2  x.  ( n  x.  ( log `  n ) ) ) )  e.  CC )
158148, 157mulneg1d 9248 . . . . . . . . . . . . 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
) ) ) ) ) )
159146, 158eqtrd 2328 . . . . . . . . . . . 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 ) ) ) ) ) )
160102, 159sumeq12rdv 12196 . . . . . . . . . . 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 ) ) ) ) ) )
161 fzfid 11051 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1 ... ( |_ `  x ) )  e. 
Fin )
162147, 156remulcld 8879 . . . . . . . . . . . . 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 )
163162recnd 8877 . . . . . . . . . . . 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 )
164161, 163fsumneg 12265 . . . . . . . . . . 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 ) ) ) ) ) )
165160, 164eqtrd 2328 . . . . . . . . . 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 ) ) ) ) ) )
16698, 165oveq12d 5892 . . . . . . . . 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 ) ) ) ) ) ) )
167 oveq2 5882 . . . . . . . . . . . . . 14  |-  ( m  =  n  ->  (
x  /  m )  =  ( x  /  n ) )
168167fveq2d 5545 . . . . . . . . . . . . 13  |-  ( m  =  n  ->  ( R `  ( x  /  m ) )  =  ( R `  (
x  /  n ) ) )
169168fveq2d 5545 . . . . . . . . . . . 12  |-  ( m  =  n  ->  ( abs `  ( R `  ( x  /  m
) ) )  =  ( abs `  ( R `  ( x  /  n ) ) ) )
170 oveq1 5881 . . . . . . . . . . . . . 14  |-  ( m  =  n  ->  (
m  -  1 )  =  ( n  - 
1 ) )
171170fveq2d 5545 . . . . . . . . . . . . 13  |-  ( m  =  n  ->  ( S `  ( m  -  1 ) )  =  ( S `  ( n  -  1
) ) )
172170fveq2d 5545 . . . . . . . . . . . . . 14  |-  ( m  =  n  ->  ( T `  ( m  -  1 ) )  =  ( T `  ( n  -  1
) ) )
173172oveq2d 5890 . . . . . . . . . . . . 13  |-  ( m  =  n  ->  (
2  x.  ( T `
 ( m  - 
1 ) ) )  =  ( 2  x.  ( T `  (
n  -  1 ) ) ) )
174171, 173oveq12d 5892 . . . . . . . . . . . 12  |-  ( m  =  n  ->  (
( S `  (
m  -  1 ) )  -  ( 2  x.  ( T `  ( m  -  1
) ) ) )  =  ( ( S `
 ( n  - 
1 ) )  -  ( 2  x.  ( T `  ( n  -  1 ) ) ) ) )
175169, 174jca 518 . . . . . . . . . . 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
) ) ) ) ) )
176 oveq2 5882 . . . . . . . . . . . . . 14  |-  ( m  =  ( n  + 
1 )  ->  (
x  /  m )  =  ( x  / 
( n  +  1 ) ) )
177176fveq2d 5545 . . . . . . . . . . . . 13  |-  ( m  =  ( n  + 
1 )  ->  ( R `  ( x  /  m ) )  =  ( R `  (
x  /  ( n  +  1 ) ) ) )
178177fveq2d 5545 . . . . . . . . . . . 12  |-  ( m  =  ( n  + 
1 )  ->  ( abs `  ( R `  ( x  /  m
) ) )  =  ( abs `  ( R `  ( x  /  ( n  + 
1 ) ) ) ) )
179 oveq1 5881 . . . . . . . . . . . . . 14  |-  ( m  =  ( n  + 
1 )  ->  (
m  -  1 )  =  ( ( n  +  1 )  - 
1 ) )
180179fveq2d 5545 . . . . . . . . . . . . 13  |-  ( m  =  ( n  + 
1 )  ->  ( S `  ( m  -  1 ) )  =  ( S `  ( ( n  + 
1 )  -  1 ) ) )
181179fveq2d 5545 . . . . . . . . . . . . . 14  |-  ( m  =  ( n  + 
1 )  ->  ( T `  ( m  -  1 ) )  =  ( T `  ( ( n  + 
1 )  -  1 ) ) )
182181oveq2d 5890 . . . . . . . . . . . . 13  |-  ( m  =  ( n  + 
1 )  ->  (
2  x.  ( T `
 ( m  - 
1 ) ) )  =  ( 2  x.  ( T `  (
( n  +  1 )  -  1 ) ) ) )
183180, 182oveq12d 5892 . . . . . . . . . . . 12  |-  ( m  =  ( n  + 
1 )  ->  (
( S `  (
m  -  1 ) )  -  ( 2  x.  ( T `  ( m  -  1
) ) ) )  =  ( ( S `
 ( ( n  +  1 )  - 
1 ) )  -  ( 2  x.  ( T `  ( (
n  +  1 )  -  1 ) ) ) ) )
184178, 183jca 518 . . . . . . . . . . 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 ) ) ) ) ) )
185 oveq2 5882 . . . . . . . . . . . . . 14  |-  ( m  =  1  ->  (
x  /  m )  =  ( x  / 
1 ) )
186185fveq2d 5545 . . . . . . . . . . . . 13  |-  ( m  =  1  ->  ( R `  ( x  /  m ) )  =  ( R `  (
x  /  1 ) ) )
187186fveq2d 5545 . . . . . . . . . . . 12  |-  ( m  =  1  ->  ( abs `  ( R `  ( x  /  m
) ) )  =  ( abs `  ( R `  ( x  /  1 ) ) ) )
188 oveq1 5881 . . . . . . . . . . . . . . . . 17  |-  ( m  =  1  ->  (
m  -  1 )  =  ( 1  -  1 ) )
18953subidi 9133 . . . . . . . . . . . . . . . . 17  |-  ( 1  -  1 )  =  0
190188, 189syl6eq 2344 . . . . . . . . . . . . . . . 16  |-  ( m  =  1  ->  (
m  -  1 )  =  0 )
191190fveq2d 5545 . . . . . . . . . . . . . . 15  |-  ( m  =  1  ->  ( S `  ( m  -  1 ) )  =  ( S ` 
0 ) )
192 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  0  ->  ( |_ `  a )  =  ( |_ `  0
) )
193 0z 10051 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  ZZ
194 flid 10955 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 0  e.  ZZ  ->  ( |_ `  0 )  =  0 )
195193, 194ax-mp 8 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( |_
`  0 )  =  0
196192, 195syl6eq 2344 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  0  ->  ( |_ `  a )  =  0 )
197196oveq2d 5890 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  0  ->  (
1 ... ( |_ `  a ) )  =  ( 1 ... 0
) )
198 fz10 10830 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1 ... 0 )  =  (/)
199197, 198syl6eq 2344 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  0  ->  (
1 ... ( |_ `  a ) )  =  (/) )
200199sumeq1d 12190 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  0  ->  sum_ i  e.  ( 1 ... ( |_ `  a ) ) ( (Λ `  i
)  x.  ( ( log `  i )  +  (ψ `  (
a  /  i ) ) ) )  = 
sum_ i  e.  (/)  ( (Λ `  i )  x.  ( ( log `  i
)  +  (ψ `  ( a  /  i
) ) ) ) )
201 sum0 12210 . . . . . . . . . . . . . . . . . 18  |-  sum_ i  e.  (/)  ( (Λ `  i
)  x.  ( ( log `  i )  +  (ψ `  (
a  /  i ) ) ) )  =  0
202200, 201syl6eq 2344 . . . . . . . . . . . . . . . . 17  |-  ( a  =  0  ->  sum_ i  e.  ( 1 ... ( |_ `  a ) ) ( (Λ `  i
)  x.  ( ( log `  i )  +  (ψ `  (
a  /  i ) ) ) )  =  0 )
203202, 49, 136fvmpt 5618 . . . . . . . . . . . . . . . 16  |-  ( 0  e.  RR  ->  ( S `  0 )  =  0 )
20441, 203ax-mp 8 . . . . . . . . . . . . . . 15  |-  ( S `
 0 )  =  0
205191, 204syl6eq 2344 . . . . . . . . . . . . . 14  |-  ( m  =  1  ->  ( S `  ( m  -  1 ) )  =  0 )
206190fveq2d 5545 . . . . . . . . . . . . . . . . 17  |-  ( m  =  1  ->  ( T `  ( m  -  1 ) )  =  ( T ` 
0 ) )
207 rpne0 10385 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  e.  RR+  ->  a  =/=  0 )
208207necon2bi 2505 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  0  ->  -.  a  e.  RR+ )
209 iffalse 3585 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  a  e.  RR+  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  0 )
210208, 209syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  0  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  0 )
211210, 84, 136fvmpt 5618 . . . . . . . . . . . . . . . . . 18  |-  ( 0  e.  RR  ->  ( T `  0 )  =  0 )
21241, 211ax-mp 8 . . . . . . . . . . . . . . . . 17  |-  ( T `
 0 )  =  0
213206, 212syl6eq 2344 . . . . . . . . . . . . . . . 16  |-  ( m  =  1  ->  ( T `  ( m  -  1 ) )  =  0 )
214213oveq2d 5890 . . . . . . . . . . . . . . 15  |-  ( m  =  1  ->  (
2  x.  ( T `
 ( m  - 
1 ) ) )  =  ( 2  x.  0 ) )
215 2cn 9832 . . . . . . . . . . . . . . . 16  |-  2  e.  CC
216215mul01i 9018 . . . . . . . . . . . . . . 15  |-  ( 2  x.  0 )  =  0
217214, 216syl6eq 2344 . . . . . . . . . . . . . 14  |-  ( m  =  1  ->  (
2  x.  ( T `
 ( m  - 
1 ) ) )  =  0 )
218205, 217oveq12d 5892 . . . . . . . . . . . . 13  |-  ( m  =  1  ->  (
( S `  (
m  -  1 ) )  -  ( 2  x.  ( T `  ( m  -  1
) ) ) )  =  ( 0  -  0 ) )
219 0cn 8847 . . . . . . . . . . . . . 14  |-  0  e.  CC
220219subidi 9133 . . . . . . . . . . . . 13  |-  ( 0  -  0 )  =  0
221218, 220syl6eq 2344 . . . . . . . . . . . 12  |-  ( m  =  1  ->  (
( S `  (
m  -  1 ) )  -  ( 2  x.  ( T `  ( m  -  1
) ) ) )  =  0 )
222187, 221jca 518 . . . . . . . . . . 11  |-  ( m  =  1  ->  (
( abs `  ( R `  ( x  /  m ) ) )  =  ( abs `  ( R `  ( x  /  1 ) ) )  /\  ( ( S `  ( m  -  1 ) )  -  ( 2  x.  ( T `  (
m  -  1 ) ) ) )  =  0 ) )
223 oveq2 5882 . . . . . . . . . . . . . 14  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (
x  /  m )  =  ( x  / 
( ( |_ `  x )  +  1 ) ) )
224223fveq2d 5545 . . . . . . . . . . . . 13  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  ( R `  ( x  /  m ) )  =  ( R `  (
x  /  ( ( |_ `  x )  +  1 ) ) ) )
225224fveq2d 5545 . . . . . . . . . . . 12  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  ( abs `  ( R `  ( x  /  m
) ) )  =  ( abs `  ( R `  ( x  /  ( ( |_
`  x )  +  1 ) ) ) ) )
226 oveq1 5881 . . . . . . . . . . . . . 14  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (
m  -  1 )  =  ( ( ( |_ `  x )  +  1 )  - 
1 ) )
227226fveq2d 5545 . . . . . . . . . . . . 13  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  ( S `  ( m  -  1 ) )  =  ( S `  ( ( ( |_
`  x )  +  1 )  -  1 ) ) )
228226fveq2d 5545 . . . . . . . . . . . . . 14  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  ( T `  ( m  -  1 ) )  =  ( T `  ( ( ( |_
`  x )  +  1 )  -  1 ) ) )
229228oveq2d 5890 . . . . . . . . . . . . 13  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (
2  x.  ( T `
 ( m  - 
1 ) ) )  =  ( 2  x.  ( T `  (
( ( |_ `  x )  +  1 )  -  1 ) ) ) )
230227, 229oveq12d 5892 . . . . . . . . . . . 12  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (
( S `  (
m  -  1 ) )  -  ( 2  x.  ( T `  ( m  -  1
) ) ) )  =  ( ( S `
 ( ( ( |_ `  x )  +  1 )  - 
1 ) )  -  ( 2  x.  ( T `  ( (
( |_ `  x
)  +  1 )  -  1 ) ) ) ) )
231225, 230jca 518 . . . . . . . . . . 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 ) ) ) ) ) )
232 nnuz 10279 . . . . . . . . . . . 12  |-  NN  =  ( ZZ>= `  1 )
23316, 232syl6eleq 2386 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  ( ZZ>= `  1
) )
23411adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  x  e.  RR+ )
235 elfznn 10835 . . . . . . . . . . . . . . . . . 18  |-  ( m  e.  ( 1 ... ( ( |_ `  x )  +  1 ) )  ->  m  e.  NN )
236235adantl 452 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  m  e.  NN )
237236nnrpd 10405 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  m  e.  RR+ )
238234, 237rpdivcld 10423 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
x  /  m )  e.  RR+ )
23972ffvelrni 5680 . . . . . . . . . . . . . . 15  |-  ( ( x  /  m )  e.  RR+  ->  ( R `
 ( x  /  m ) )  e.  RR )
240238, 239syl 15 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  ( R `  ( x  /  m ) )  e.  RR )
241240recnd 8877 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  ( R `  ( x  /  m ) )  e.  CC )
242241abscld 11934 . . . . . . . . . . . 12  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  ( abs `  ( R `  ( x  /  m
) ) )  e.  RR )
243242recnd 8877 . . . . . . . . . . 11  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  ( abs `  ( R `  ( x  /  m
) ) )  e.  CC )
244236nnred 9777 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  m  e.  RR )
2455a1i 10 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  1  e.  RR )
246244, 245resubcld 9227 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
m  -  1 )  e.  RR )
24781ffvelrni 5680 . . . . . . . . . . . . . 14  |-  ( ( m  -  1 )  e.  RR  ->  ( S `  ( m  -  1 ) )  e.  RR )
248246, 247syl 15 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  ( S `  ( m  -  1 ) )  e.  RR )
24923a1i 10 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  2  e.  RR )
25090ffvelrni 5680 . . . . . . . . . . . . . . 15  |-  ( ( m  -  1 )  e.  RR  ->  ( T `  ( m  -  1 ) )  e.  RR )
251246, 250syl 15 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  ( T `  ( m  -  1 ) )  e.  RR )
252249, 251remulcld 8879 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
2  x.  ( T `
 ( m  - 
1 ) ) )  e.  RR )
253248, 252resubcld 9227 . . . . . . . . . . . 12  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
( S `  (
m  -  1 ) )  -  ( 2  x.  ( T `  ( m  -  1
) ) ) )  e.  RR )
254253recnd 8877 . . . . . . . . . . 11  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
( S `  (
m  -  1 ) )  -  ( 2  x.  ( T `  ( m  -  1
) ) ) )  e.  CC )
255175, 184, 222, 231, 233, 243, 254fsumparts 12280 . . . . . . . . . 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 ) ) ) ) ) ) )
256151recnd 8877 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( S `  n )  e.  CC )
25790ffvelrni 5680 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  RR  ->  ( T `  n )  e.  RR )
258149, 257syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  n )  e.  RR )
259152, 258remulcld 8879 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( T `  n ) )  e.  RR )
260259recnd 8877 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( T `  n ) )  e.  CC )
2615a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR )
262149, 261resubcld 9227 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  -  1 )  e.  RR )
26381ffvelrni 5680 . . . . . . . . . . . . . . . 16  |-  ( ( n  -  1 )  e.  RR  ->  ( S `  ( n  -  1 ) )  e.  RR )
264262, 263syl 15 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( S `  ( n  -  1 ) )  e.  RR )
265264recnd 8877 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( S `  ( n  -  1 ) )  e.  CC )
26690ffvelrni 5680 . . . . . . . . . . . . . . . . 17  |-  ( ( n  -  1 )  e.  RR  ->  ( T `  ( n  -  1 ) )  e.  RR )
267262, 266syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  ( n  -  1 ) )  e.  RR )
268152, 267remulcld 8879 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( T `  ( n  -  1
) ) )  e.  RR )
269268recnd 8877 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( T `  ( n  -  1
) ) )  e.  CC )
270256, 260, 265, 269sub4d 9222 . . . . . . . . . . . . 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 ) ) ) ) ) )
271127oveq2d 5890 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( T `  ( ( n  + 
1 )  -  1 ) ) )  =  ( 2  x.  ( T `  n )
) )
272126, 271oveq12d 5892 . . . . . . . . . . . . . 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 ) ) ) )
273272oveq1d 5889 . . . . . . . . . . . . 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
) ) ) ) ) )
274215a1i 10 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  2  e.  CC )
275258recnd 8877 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  n )  e.  CC )
276267recnd 8877 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  ( n  -  1 ) )  e.  CC )
277274, 275, 276subdid 9251 . . . . . . . . . . . . . 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
) ) ) ) )
278277oveq2d 5890 . . . . . . . . . . . . 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 ) ) ) ) ) )
279270, 273, 2783eqtr4d 2338 . . . . . . . . . . . 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 ) ) ) ) ) )
280279oveq2d 5890 . . . . . . . . . . 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 ) ) ) ) ) ) )
281102, 280sumeq12rdv 12196 . . . . . . . . . 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 ) ) ) ) ) ) )
282255, 281eqtr3d 2330 . . . . . . . . 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 ) ) ) ) ) ) )
283161, 163fsumcl 12222 . . . . . . . . . 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 )
28496, 283subnegd 9180 . . . . . . . . 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
) ) ) ) ) ) )
285166, 282, 2843eqtr3rd 2337 . . . . . . . 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 ) ) ) ) ) ) )
28611relogcld 19990 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  RR )
287286recnd 8877 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  CC )
28869, 287mulcomd 8872 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  x.  ( log `  x ) )  =  ( ( log `  x
)  x.  x ) )
289285, 288oveq12d 5892 . . . . . . 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 ) ) )
290151, 264resubcld 9227 . . . . . . . . . . . 12  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( S `  n )  -  ( S `  ( n  -  1
) ) )  e.  RR )
291258, 267resubcld 9227 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( T `  n )  -  ( T `  ( n  -  1
) ) )  e.  RR )
292152, 291remulcld 8879 . . . . . . . . . . . 12  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( ( T `
 n )  -  ( T `  ( n  -  1 ) ) ) )  e.  RR )
293290, 292resubcld 9227 . . . . . . . . . . 11  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( S `  n
)  -  ( S `
 ( n  - 
1 ) ) )  -  ( 2  x.  ( ( T `  n )  -  ( T `  ( n  -  1 ) ) ) ) )  e.  RR )
294111, 293remulcld 8879 . . . . . . . . . 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 )
295161, 294fsumrecl 12223 . . . . . . . . 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 )
296295recnd 8877 . . . . . . . 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 )
2972, 9rplogcld 19996 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  RR+ )
298297rpne0d 10411 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  =/=  0 )
29911rpne0d 10411 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  =/=  0 )
300296, 287, 69, 298, 299divdiv1d 9583 . . . . . . 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 ) ) )
301289, 300eqtr4d 2331 . . . . . 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
) )
302301oveq2d 5890 . . . . 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
) ) )
30374recnd 8877 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( R `  x )  e.  CC )
304303abscld 11934 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( abs `  ( R `  x ) )  e.  RR )
305304, 286remulcld 8879 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( abs `  ( R `  x )
)  x.  ( log `  x ) )  e.  RR )
306111, 290remulcld 8879 . . . . . . . . . 10  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  ( ( S `  n )  -  ( S `  ( n  -  1 ) ) ) )  e.  RR )
307161, 306fsumrecl 12223 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( S `
 n )  -  ( S `  ( n  -  1 ) ) ) )  e.  RR )
308307, 297rerpdivcld 10433 . . . . . . . 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 )
309305, 308resubcld 9227 . . . . . . 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 )
310309recnd 8877 . . . . . 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 )
311296, 287, 298divcld 9552 . . . . . 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 )
312310, 311, 69, 299divdird 9590 . . . . 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
) ) )
313305recnd 8877 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( abs `  ( R `  x )
)  x.  ( log `  x ) )  e.  CC )
314308recnd 8877 . . . . . . . 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 )
315313, 314, 311subsubd 9201 . . . . . . 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
) ) ) )
316215a1i 10 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  2  e.  CC )
317275, 276subcld 9173 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( T `  n )  -  ( T `  ( n  -  1
) ) )  e.  CC )
318112, 317mulcld 8871 . . . . . . . . . . . 12  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  ( ( T `  n )  -  ( T `  ( n  -  1 ) ) ) )  e.  CC )
319161, 316, 318fsummulc2 12262 . . . . . . . . . . 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 ) ) ) ) ) )
320290recnd 8877 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( S `  n )  -  ( S `  ( n  -  1
) ) )  e.  CC )
321274, 317mulcld 8871 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( ( T `
 n )  -  ( T `  ( n  -  1 ) ) ) )  e.  CC )
322320, 321nncand 9178 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( S `  n
)  -  ( S `
 ( n  - 
1 ) ) )  -  (