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

Theorem pntrlog2bndlem4 23630
Description: Lemma for pntrlog2bnd 23634. 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 11563 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( 1 (,) +oo )  ->  x  e.  RR )
21adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  x  e.  RR )
3 1rp 11228 . . . . . . . . . . . . . . . . . . . 20  |-  1  e.  RR+
43a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  1  e.  RR+ )
5 1red 9609 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  1  e.  RR )
6 eliooord 11588 . . . . . . . . . . . . . . . . . . . . . 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 9731 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  1  <_  x )
102, 4, 9rpgecld 11295 . . . . . . . . . . . . . . . . . 18  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  x  e.  RR+ )
1110rprege0d 11267 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  e.  RR  /\  0  <_  x ) )
12 flge0nn0 11928 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  RR  /\  0  <_  x )  -> 
( |_ `  x
)  e.  NN0 )
1311, 12syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( |_ `  x )  e. 
NN0 )
14 nn0p1nn 10836 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( |_ `  x )  e.  NN0  ->  ( ( |_ `  x )  +  1 )  e.  NN )
1513, 14syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  NN )
1615nnrpd 11259 . . . . . . . . . . . . . . . . . 18  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  RR+ )
1710, 16rpdivcld 11277 . . . . . . . . . . . . . . . . 17  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  e.  RR+ )
18 pntrlog2bnd.r . . . . . . . . . . . . . . . . . 18  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
1918pntrval 23612 . . . . . . . . . . . . . . . . 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 10585 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  e.  RR )
22 2re 10606 . . . . . . . . . . . . . . . . . . . 20  |-  2  e.  RR
2322a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  2  e.  RR )
24 flltp1 11911 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  x  <  ( ( |_ `  x )  +  1 ) )
252, 24syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  x  <  ( ( |_ `  x )  +  1 ) )
2615nncnd 10553 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  CC )
2726mulid1d 9611 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( |_ `  x )  +  1 )  x.  1 )  =  ( ( |_
`  x )  +  1 ) )
2825, 27breqtrrd 4459 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  x  <  ( ( ( |_
`  x )  +  1 )  x.  1 ) )
292, 5, 16ltdivmuld 11307 . . . . . . . . . . . . . . . . . . . 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 10703 . . . . . . . . . . . . . . . . . . . 20  |-  1  <  2
3231a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  1  <  2 )
3321, 5, 23, 30, 32lttrd 9741 . . . . . . . . . . . . . . . . . 18  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  <  2 )
34 chpeq0 23348 . . . . . . . . . . . . . . . . . . 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 6292 . . . . . . . . . . . . . . . 16  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  -  ( x  / 
( ( |_ `  x )  +  1 ) ) )  =  ( 0  -  (
x  /  ( ( |_ `  x )  +  1 ) ) ) )
3820, 37eqtrd 2482 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( R `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  =  ( 0  -  ( x  /  (
( |_ `  x
)  +  1 ) ) ) )
3938fveq2d 5856 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( R `  ( x  /  (
( |_ `  x
)  +  1 ) ) ) )  =  ( abs `  (
0  -  ( x  /  ( ( |_
`  x )  +  1 ) ) ) ) )
40 0red 9595 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  0  e.  RR )
4117rpge0d 11264 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  0  <_  ( x  /  (
( |_ `  x
)  +  1 ) ) )
4240, 21, 41abssuble0d 13238 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( 0  -  ( x  /  (
( |_ `  x
)  +  1 ) ) ) )  =  ( ( x  / 
( ( |_ `  x )  +  1 ) )  -  0 ) )
4321recnd 9620 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  e.  CC )
4443subid1d 9920 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( x  /  (
( |_ `  x
)  +  1 ) )  -  0 )  =  ( x  / 
( ( |_ `  x )  +  1 ) ) )
4539, 42, 443eqtrd 2486 . . . . . . . . . . . . 13  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( R `  ( x  /  (
( |_ `  x
)  +  1 ) ) ) )  =  ( x  /  (
( |_ `  x
)  +  1 ) ) )
4613nn0red 10854 . . . . . . . . . . . . . . . 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 23626 . . . . . . . . . . . . . . . 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 10855 . . . . . . . . . . . . . . . . 17  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( |_ `  x )  e.  CC )
51 1cnd 9610 . . . . . . . . . . . . . . . . 17  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  1  e.  CC )
5250, 51pncand 9932 . . . . . . . . . . . . . . . 16  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( |_ `  x )  +  1 )  -  1 )  =  ( |_ `  x ) )
5352fveq2d 5856 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( S `  ( (
( |_ `  x
)  +  1 )  -  1 ) )  =  ( S `  ( |_ `  x ) ) )
5447pntsval2 23626 . . . . . . . . . . . . . . . . 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 11920 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  RR  ->  ( |_ `  ( |_ `  x ) )  =  ( |_ `  x
) )
572, 56syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( |_ `  ( |_ `  x ) )  =  ( |_ `  x
) )
5857oveq2d 6293 . . . . . . . . . . . . . . . . 17  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1 ... ( |_ `  ( |_ `  x ) ) )  =  ( 1 ... ( |_
`  x ) ) )
5958sumeq1d 13497 . . . . . . . . . . . . . . . 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 2485 . . . . . . . . . . . . . . 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 2492 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( S `  ( (
( |_ `  x
)  +  1 )  -  1 ) )  =  ( S `  x ) )
6252fveq2d 5856 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( T `  ( (
( |_ `  x
)  +  1 )  -  1 ) )  =  ( T `  ( |_ `  x ) ) )
6362oveq2d 6293 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
2  x.  ( T `
 ( ( ( |_ `  x )  +  1 )  - 
1 ) ) )  =  ( 2  x.  ( T `  ( |_ `  x ) ) ) )
6461, 63oveq12d 6295 . . . . . . . . . . . . 13  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( S `  (
( ( |_ `  x )  +  1 )  -  1 ) )  -  ( 2  x.  ( T `  ( ( ( |_
`  x )  +  1 )  -  1 ) ) ) )  =  ( ( S `
 x )  -  ( 2  x.  ( T `  ( |_ `  x ) ) ) ) )
6545, 64oveq12d 6295 . . . . . . . . . . . 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 9620 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  x  e.  CC )
6766div1d 10313 . . . . . . . . . . . . . . . . . 18  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  /  1 )  =  x )
6867fveq2d 5856 . . . . . . . . . . . . . . . . 17  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( R `  ( x  /  1 ) )  =  ( R `  x ) )
6918pntrf 23613 . . . . . . . . . . . . . . . . . . 19  |-  R : RR+
--> RR
7069ffvelrni 6011 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  RR+  ->  ( R `
 x )  e.  RR )
7110, 70syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( R `  x )  e.  RR )
7268, 71eqeltrd 2529 . . . . . . . . . . . . . . . 16  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( R `  ( x  /  1 ) )  e.  RR )
7372recnd 9620 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( R `  ( x  /  1 ) )  e.  CC )
7473abscld 13241 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( R `  ( x  /  1
) ) )  e.  RR )
7574recnd 9620 . . . . . . . . . . . . 13  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( R `  ( x  /  1
) ) )  e.  CC )
7675mul01d 9777 . . . . . . . . . . . 12  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( abs `  ( R `  ( x  /  1 ) ) )  x.  0 )  =  0 )
7765, 76oveq12d 6295 . . . . . . . . . . 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 23623 . . . . . . . . . . . . . . . . 17  |-  S : RR
--> RR
7978ffvelrni 6011 . . . . . . . . . . . . . . . 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 22828 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  e.  RR+  ->  ( log `  a )  e.  RR )
83 remulcl 9575 . . . . . . . . . . . . . . . . . . . . 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 9595 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( a  e.  RR  /\  -.  a  e.  RR+ )  ->  0  e.  RR )
8684, 85ifclda 3954 . . . . . . . . . . . . . . . . . . 19  |-  ( a  e.  RR  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  e.  RR )
8781, 86fmpti 6035 . . . . . . . . . . . . . . . . . 18  |-  T : RR
--> RR
8887ffvelrni 6011 . . . . . . . . . . . . . . . . 17  |-  ( ( |_ `  x )  e.  RR  ->  ( T `  ( |_ `  x ) )  e.  RR )
8946, 88syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( T `  ( |_ `  x ) )  e.  RR )
9023, 89remulcld 9622 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
2  x.  ( T `
 ( |_ `  x ) ) )  e.  RR )
9180, 90resubcld 9988 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( S `  x
)  -  ( 2  x.  ( T `  ( |_ `  x ) ) ) )  e.  RR )
9221, 91remulcld 9622 . . . . . . . . . . . . 13  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( x  /  (
( |_ `  x
)  +  1 ) )  x.  ( ( S `  x )  -  ( 2  x.  ( T `  ( |_ `  x ) ) ) ) )  e.  RR )
9392recnd 9620 . . . . . . . . . . . 12  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( x  /  (
( |_ `  x
)  +  1 ) )  x.  ( ( S `  x )  -  ( 2  x.  ( T `  ( |_ `  x ) ) ) ) )  e.  CC )
9493subid1d 9920 . . . . . . . . . . 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 2482 . . . . . . . . . 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 11909 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( |_ `  x )  e.  ZZ )
97 fzval3 11859 . . . . . . . . . . . . . 14  |-  ( ( |_ `  x )  e.  ZZ  ->  (
1 ... ( |_ `  x ) )  =  ( 1..^ ( ( |_ `  x )  +  1 ) ) )
9896, 97syl 16 . . . . . . . . . . . . 13  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1 ... ( |_ `  x ) )  =  ( 1..^ ( ( |_ `  x )  +  1 ) ) )
9998eqcomd 2449 . . . . . . . . . . . 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 11718 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
102101adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
103102nnrpd 11259 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR+ )
104100, 103rpdivcld 11277 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
10569ffvelrni 6011 . . . . . . . . . . . . . . . . . . . 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 9620 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  e.  CC )
108107abscld 13241 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( R `  (
x  /  n ) ) )  e.  RR )
109108recnd 9620 . . . . . . . . . . . . . . . 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 11275 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  +  1 )  e.  RR+ )
112100, 111rpdivcld 11277 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  ( n  + 
1 ) )  e.  RR+ )
11369ffvelrni 6011 . . . . . . . . . . . . . . . . . . . 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 9620 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  (
n  +  1 ) ) )  e.  CC )
116115abscld 13241 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( R `  (
x  /  ( n  +  1 ) ) ) )  e.  RR )
117116recnd 9620 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( R `  (
x  /  ( n  +  1 ) ) ) )  e.  CC )
118109, 117negsubdi2d 9947 . . . . . . . . . . . . . . 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 2449 . . . . . . . . . . . . . 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 10553 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  CC )
121 1cnd 9610 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  CC )
122120, 121pncand 9932 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
n  +  1 )  -  1 )  =  n )
123122fveq2d 5856 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( S `  ( ( n  + 
1 )  -  1 ) )  =  ( S `  n ) )
124122fveq2d 5856 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  ( ( n  + 
1 )  -  1 ) )  =  ( T `  n ) )
125 rpre 11230 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  RR+  ->  n  e.  RR )
126 eleq1 2513 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  n  ->  (
a  e.  RR+  <->  n  e.  RR+ ) )
127 id 22 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  n  ->  a  =  n )
128 fveq2 5852 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  n  ->  ( log `  a )  =  ( log `  n
) )
129127, 128oveq12d 6295 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  n  ->  (
a  x.  ( log `  a ) )  =  ( n  x.  ( log `  n ) ) )
130126, 129ifbieq1d 3945 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  n  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  if ( n  e.  RR+ ,  ( n  x.  ( log `  n
) ) ,  0 ) )
131 ovex 6305 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  x.  ( log `  n
) )  e.  _V
132 c0ex 9588 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  _V
133131, 132ifex 3991 . . . . . . . . . . . . . . . . . . . . 21  |-  if ( n  e.  RR+ ,  ( n  x.  ( log `  n ) ) ,  0 )  e.  _V
134130, 81, 133fvmpt 5937 . . . . . . . . . . . . . . . . . . . 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 3928 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  RR+  ->  if ( n  e.  RR+ ,  ( n  x.  ( log `  n ) ) ,  0 )  =  ( n  x.  ( log `  n ) ) )
137135, 136eqtrd 2482 . . . . . . . . . . . . . . . . . 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 2482 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  ( ( n  + 
1 )  -  1 ) )  =  ( n  x.  ( log `  n ) ) )
140139oveq2d 6293 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( T `  ( ( n  + 
1 )  -  1 ) ) )  =  ( 2  x.  (
n  x.  ( log `  n ) ) ) )
141123, 140oveq12d 6295 . . . . . . . . . . . . . 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 6295 . . . . . . . . . . . . 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 9988 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  -  ( abs `  ( R `
 ( x  / 
( n  +  1 ) ) ) ) )  e.  RR )
144143recnd 9620 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  -  ( abs `  ( R `
 ( x  / 
( n  +  1 ) ) ) ) )  e.  CC )
145102nnred 10552 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR )
14678ffvelrni 6011 . . . . . . . . . . . . . . . . 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 22873 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  n )  e.  RR )
150145, 149remulcld 9622 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  x.  ( log `  n
) )  e.  RR )
151148, 150remulcld 9622 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( n  x.  ( log `  n
) ) )  e.  RR )
152147, 151resubcld 9988 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( S `  n )  -  ( 2  x.  ( n  x.  ( log `  n ) ) ) )  e.  RR )
153152recnd 9620 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( S `  n )  -  ( 2  x.  ( n  x.  ( log `  n ) ) ) )  e.  CC )
154144, 153mulneg1d 10010 . . . . . . . . . . . . 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 2482 . . . . . . . . . . . 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 13503 . . . . . . . . . . 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 12057 . . . . . . . . . . . 12  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1 ... ( |_ `  x ) )  e. 
Fin )
158143, 152remulcld 9622 . . . . . . . . . . . . 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 9620 . . . . . . . . . . . 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 13576 . . . . . . . . . . 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 2482 . . . . . . . . . 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 6295 . . . . . . . . 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 6285 . . . . . . . . . . . . . 14  |-  ( m  =  n  ->  (
x  /  m )  =  ( x  /  n ) )
164163fveq2d 5856 . . . . . . . . . . . . 13  |-  ( m  =  n  ->  ( R `  ( x  /  m ) )  =  ( R `  (
x  /  n ) ) )
165164fveq2d 5856 . . . . . . . . . . . 12  |-  ( m  =  n  ->  ( abs `  ( R `  ( x  /  m
) ) )  =  ( abs `  ( R `  ( x  /  n ) ) ) )
166 oveq1 6284 . . . . . . . . . . . . . 14  |-  ( m  =  n  ->  (
m  -  1 )  =  ( n  - 
1 ) )
167166fveq2d 5856 . . . . . . . . . . . . 13  |-  ( m  =  n  ->  ( S `  ( m  -  1 ) )  =  ( S `  ( n  -  1
) ) )
168166fveq2d 5856 . . . . . . . . . . . . . 14  |-  ( m  =  n  ->  ( T `  ( m  -  1 ) )  =  ( T `  ( n  -  1
) ) )
169168oveq2d 6293 . . . . . . . . . . . . 13  |-  ( m  =  n  ->  (
2  x.  ( T `
 ( m  - 
1 ) ) )  =  ( 2  x.  ( T `  (
n  -  1 ) ) ) )
170167, 169oveq12d 6295 . . . . . . . . . . . 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 6285 . . . . . . . . . . . . . 14  |-  ( m  =  ( n  + 
1 )  ->  (
x  /  m )  =  ( x  / 
( n  +  1 ) ) )
173172fveq2d 5856 . . . . . . . . . . . . 13  |-  ( m  =  ( n  + 
1 )  ->  ( R `  ( x  /  m ) )  =  ( R `  (
x  /  ( n  +  1 ) ) ) )
174173fveq2d 5856 . . . . . . . . . . . 12  |-  ( m  =  ( n  + 
1 )  ->  ( abs `  ( R `  ( x  /  m
) ) )  =  ( abs `  ( R `  ( x  /  ( n  + 
1 ) ) ) ) )
175 oveq1 6284 . . . . . . . . . . . . . 14  |-  ( m  =  ( n  + 
1 )  ->  (
m  -  1 )  =  ( ( n  +  1 )  - 
1 ) )
176175fveq2d 5856 . . . . . . . . . . . . 13  |-  ( m  =  ( n  + 
1 )  ->  ( S `  ( m  -  1 ) )  =  ( S `  ( ( n  + 
1 )  -  1 ) ) )
177175fveq2d 5856 . . . . . . . . . . . . . 14  |-  ( m  =  ( n  + 
1 )  ->  ( T `  ( m  -  1 ) )  =  ( T `  ( ( n  + 
1 )  -  1 ) ) )
178177oveq2d 6293 . . . . . . . . . . . . 13  |-  ( m  =  ( n  + 
1 )  ->  (
2  x.  ( T `
 ( m  - 
1 ) ) )  =  ( 2  x.  ( T `  (
( n  +  1 )  -  1 ) ) ) )
179176, 178oveq12d 6295 . . . . . . . . . . . 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 6285 . . . . . . . . . . . . . 14  |-  ( m  =  1  ->  (
x  /  m )  =  ( x  / 
1 ) )
182181fveq2d 5856 . . . . . . . . . . . . 13  |-  ( m  =  1  ->  ( R `  ( x  /  m ) )  =  ( R `  (
x  /  1 ) ) )
183182fveq2d 5856 . . . . . . . . . . . 12  |-  ( m  =  1  ->  ( abs `  ( R `  ( x  /  m
) ) )  =  ( abs `  ( R `  ( x  /  1 ) ) ) )
184 oveq1 6284 . . . . . . . . . . . . . . . . 17  |-  ( m  =  1  ->  (
m  -  1 )  =  ( 1  -  1 ) )
185 1m1e0 10605 . . . . . . . . . . . . . . . . 17  |-  ( 1  -  1 )  =  0
186184, 185syl6eq 2498 . . . . . . . . . . . . . . . 16  |-  ( m  =  1  ->  (
m  -  1 )  =  0 )
187186fveq2d 5856 . . . . . . . . . . . . . . 15  |-  ( m  =  1  ->  ( S `  ( m  -  1 ) )  =  ( S ` 
0 ) )
188 0re 9594 . . . . . . . . . . . . . . . 16  |-  0  e.  RR
189 fveq2 5852 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  0  ->  ( |_ `  a )  =  ( |_ `  0
) )
190 0z 10876 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  ZZ
191 flid 11919 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 0  e.  ZZ  ->  ( |_ `  0 )  =  0 )
192190, 191ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( |_
`  0 )  =  0
193189, 192syl6eq 2498 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  0  ->  ( |_ `  a )  =  0 )
194193oveq2d 6293 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  0  ->  (
1 ... ( |_ `  a ) )  =  ( 1 ... 0
) )
195 fz10 11710 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1 ... 0 )  =  (/)
196194, 195syl6eq 2498 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  0  ->  (
1 ... ( |_ `  a ) )  =  (/) )
197196sumeq1d 13497 . . . . . . . . . . . . . . . . . 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 13517 . . . . . . . . . . . . . . . . . 18  |-  sum_ i  e.  (/)  ( (Λ `  i
)  x.  ( ( log `  i )  +  (ψ `  (
a  /  i ) ) ) )  =  0
199197, 198syl6eq 2498 . . . . . . . . . . . . . . . . 17  |-  ( a  =  0  ->  sum_ i  e.  ( 1 ... ( |_ `  a ) ) ( (Λ `  i
)  x.  ( ( log `  i )  +  (ψ `  (
a  /  i ) ) ) )  =  0 )
200199, 47, 132fvmpt 5937 . . . . . . . . . . . . . . . 16  |-  ( 0  e.  RR  ->  ( S `  0 )  =  0 )
201188, 200ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( S `
 0 )  =  0
202187, 201syl6eq 2498 . . . . . . . . . . . . . 14  |-  ( m  =  1  ->  ( S `  ( m  -  1 ) )  =  0 )
203186fveq2d 5856 . . . . . . . . . . . . . . . . 17  |-  ( m  =  1  ->  ( T `  ( m  -  1 ) )  =  ( T ` 
0 ) )
204 rpne0 11239 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  e.  RR+  ->  a  =/=  0 )
205204necon2bi 2678 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  0  ->  -.  a  e.  RR+ )
206205iffalsed 3933 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  0  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  0 )
207206, 81, 132fvmpt 5937 . . . . . . . . . . . . . . . . . 18  |-  ( 0  e.  RR  ->  ( T `  0 )  =  0 )
208188, 207ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( T `
 0 )  =  0
209203, 208syl6eq 2498 . . . . . . . . . . . . . . . 16  |-  ( m  =  1  ->  ( T `  ( m  -  1 ) )  =  0 )
210209oveq2d 6293 . . . . . . . . . . . . . . 15  |-  ( m  =  1  ->  (
2  x.  ( T `
 ( m  - 
1 ) ) )  =  ( 2  x.  0 ) )
211 2t0e0 10692 . . . . . . . . . . . . . . 15  |-  ( 2  x.  0 )  =  0
212210, 211syl6eq 2498 . . . . . . . . . . . . . 14  |-  ( m  =  1  ->  (
2  x.  ( T `
 ( m  - 
1 ) ) )  =  0 )
213202, 212oveq12d 6295 . . . . . . . . . . . . 13  |-  ( m  =  1  ->  (
( S `  (
m  -  1 ) )  -  ( 2  x.  ( T `  ( m  -  1
) ) ) )  =  ( 0  -  0 ) )
214 0m0e0 10646 . . . . . . . . . . . . 13  |-  ( 0  -  0 )  =  0
215213, 214syl6eq 2498 . . . . . . . . . . . 12  |-  ( m  =  1  ->  (
( S `  (
m  -  1 ) )  -  ( 2  x.  ( T `  ( m  -  1
) ) ) )  =  0 )
216183, 215jca 532 . . . . . . . . . . 11  |-  ( m  =  1  ->  (
( abs `  ( R `  ( x  /  m ) ) )  =  ( abs `  ( R `  ( x  /  1 ) ) )  /\  ( ( S `  ( m  -  1 ) )  -  ( 2  x.  ( T `  (
m  -  1 ) ) ) )  =  0 ) )
217 oveq2 6285 . . . . . . . . . . . . . 14  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (
x  /  m )  =  ( x  / 
( ( |_ `  x )  +  1 ) ) )
218217fveq2d 5856 . . . . . . . . . . . . 13  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  ( R `  ( x  /  m ) )  =  ( R `  (
x  /  ( ( |_ `  x )  +  1 ) ) ) )
219218fveq2d 5856 . . . . . . . . . . . 12  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  ( abs `  ( R `  ( x  /  m
) ) )  =  ( abs `  ( R `  ( x  /  ( ( |_
`  x )  +  1 ) ) ) ) )
220 oveq1 6284 . . . . . . . . . . . . . 14  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (
m  -  1 )  =  ( ( ( |_ `  x )  +  1 )  - 
1 ) )
221220fveq2d 5856 . . . . . . . . . . . . 13  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  ( S `  ( m  -  1 ) )  =  ( S `  ( ( ( |_
`  x )  +  1 )  -  1 ) ) )
222220fveq2d 5856 . . . . . . . . . . . . . 14  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  ( T `  ( m  -  1 ) )  =  ( T `  ( ( ( |_
`  x )  +  1 )  -  1 ) ) )
223222oveq2d 6293 . . . . . . . . . . . . 13  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (
2  x.  ( T `
 ( m  - 
1 ) ) )  =  ( 2  x.  ( T `  (
( ( |_ `  x )  +  1 )  -  1 ) ) ) )
224221, 223oveq12d 6295 . . . . . . . . . . . 12  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (
( S `  (
m  -  1 ) )  -  ( 2  x.  ( T `  ( m  -  1
) ) ) )  =  ( ( S `
 ( ( ( |_ `  x )  +  1 )  - 
1 ) )  -  ( 2  x.  ( T `  ( (
( |_ `  x
)  +  1 )  -  1 ) ) ) ) )
225219, 224jca 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 ) ) ) ) ) )
226 nnuz 11120 . . . . . . . . . . . 12  |-  NN  =  ( ZZ>= `  1 )
22715, 226syl6eleq 2539 . . . . . . . . . . 11  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  ( ZZ>= `  1
) )
22810adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  x  e.  RR+ )
229 elfznn 11718 . . . . . . . . . . . . . . . . . 18  |-  ( m  e.  ( 1 ... ( ( |_ `  x )  +  1 ) )  ->  m  e.  NN )
230229adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  m  e.  NN )
231230nnrpd 11259 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  m  e.  RR+ )
232228, 231rpdivcld 11277 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
x  /  m )  e.  RR+ )
23369ffvelrni 6011 . . . . . . . . . . . . . . 15  |-  ( ( x  /  m )  e.  RR+  ->  ( R `
 ( x  /  m ) )  e.  RR )
234232, 233syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  ( R `  ( x  /  m ) )  e.  RR )
235234recnd 9620 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  ( R `  ( x  /  m ) )  e.  CC )
236235abscld 13241 . . . . . . . . . . . 12  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  ( abs `  ( R `  ( x  /  m
) ) )  e.  RR )
237236recnd 9620 . . . . . . . . . . 11  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  ( abs `  ( R `  ( x  /  m
) ) )  e.  CC )
238230nnred 10552 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  m  e.  RR )
239 1red 9609 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  1  e.  RR )
240238, 239resubcld 9988 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
m  -  1 )  e.  RR )
24178ffvelrni 6011 . . . . . . . . . . . . . 14  |-  ( ( m  -  1 )  e.  RR  ->  ( S `  ( m  -  1 ) )  e.  RR )
242240, 241syl 16 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  ( S `  ( m  -  1 ) )  e.  RR )
24322a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  2  e.  RR )
24487ffvelrni 6011 . . . . . . . . . . . . . . 15  |-  ( ( m  -  1 )  e.  RR  ->  ( T `  ( m  -  1 ) )  e.  RR )
245240, 244syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  ( T `  ( m  -  1 ) )  e.  RR )
246243, 245remulcld 9622 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
2  x.  ( T `
 ( m  - 
1 ) ) )  e.  RR )
247242, 246resubcld 9988 . . . . . . . . . . . 12  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
( S `  (
m  -  1 ) )  -  ( 2  x.  ( T `  ( m  -  1
) ) ) )  e.  RR )
248247recnd 9620 . . . . . . . . . . 11  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
( S `  (
m  -  1 ) )  -  ( 2  x.  ( T `  ( m  -  1
) ) ) )  e.  CC )
249171, 180, 216, 225, 227, 237, 248fsumparts 13594 . . . . . . . . . 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 ) ) ) ) ) ) )
250147recnd 9620 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( S `  n )  e.  CC )
25187ffvelrni 6011 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  RR  ->  ( T `  n )  e.  RR )
252145, 251syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  n )  e.  RR )
253148, 252remulcld 9622 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( T `  n ) )  e.  RR )
254253recnd 9620 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( T `  n ) )  e.  CC )
255 1red 9609 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR )
256145, 255resubcld 9988 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  -  1 )  e.  RR )
25778ffvelrni 6011 . . . . . . . . . . . . . . . 16  |-  ( ( n  -  1 )  e.  RR  ->  ( S `  ( n  -  1 ) )  e.  RR )
258256, 257syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( S `  ( n  -  1 ) )  e.  RR )
259258recnd 9620 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( S `  ( n  -  1 ) )  e.  CC )
26087ffvelrni 6011 . . . . . . . . . . . . . . . . 17  |-  ( ( n  -  1 )  e.  RR  ->  ( T `  ( n  -  1 ) )  e.  RR )
261256, 260syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  ( n  -  1 ) )  e.  RR )
262148, 261remulcld 9622 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( T `  ( n  -  1
) ) )  e.  RR )
263262recnd 9620 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( T `  ( n  -  1
) ) )  e.  CC )
264250, 254, 259, 263sub4d 9980 . . . . . . . . . . . . 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 ) ) ) ) ) )
265124oveq2d 6293 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( T `  ( ( n  + 
1 )  -  1 ) ) )  =  ( 2  x.  ( T `  n )
) )
266123, 265oveq12d 6295 . . . . . . . . . . . . . 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 ) ) ) )
267266oveq1d 6292 . . . . . . . . . . . . 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
) ) ) ) ) )
268 2cnd 10609 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  2  e.  CC )
269252recnd 9620 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  n )  e.  CC )
270261recnd 9620 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  ( n  -  1 ) )  e.  CC )
271268, 269, 270subdid 10013 . . . . . . . . . . . . . 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
) ) ) ) )
272271oveq2d 6293 . . . . . . . . . . . . 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 ) ) ) ) ) )
273264, 267, 2723eqtr4d 2492 . . . . . . . . . . . 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 ) ) ) ) ) )
274273oveq2d 6293 . . . . . . . . . . 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 ) ) ) ) ) ) )
27599, 274sumeq12rdv 13503 . . . . . . . . . 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 ) ) ) ) ) ) )
276249, 275eqtr3d 2484 . . . . . . . . 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 ) ) ) ) ) ) )
277157, 159fsumcl 13529 . . . . . . . . . 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 )
27893, 277subnegd 9938 . . . . . . . . 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
) ) ) ) ) ) )
279162, 276, 2783eqtr3rd 2491 . . . . . . . 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 ) ) ) ) ) ) )
28010relogcld 22873 . . . . . . . . . 10  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  e.  RR )
281280recnd 9620 . . . . . . . . 9  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  e.  CC )
28266, 281mulcomd 9615 . . . . . . . 8  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  x.  ( log `  x ) )  =  ( ( log `  x
)  x.  x ) )
283279, 282oveq12d 6295 . . . . . . 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 ) ) )
284147, 258resubcld 9988 . . . . . . . . . . . 12  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( S `  n )  -  ( S `  ( n  -  1
) ) )  e.  RR )
285252, 261resubcld 9988 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( T `  n )  -  ( T `  ( n  -  1
) ) )  e.  RR )
286148, 285remulcld 9622 . . . . . . . . . . . 12  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( ( T `
 n )  -  ( T `  ( n  -  1 ) ) ) )  e.  RR )
287284, 286resubcld 9988 . . . . . . . . . . 11  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( S `  n
)  -  ( S `
 ( n  - 
1 ) ) )  -  ( 2  x.  ( ( T `  n )  -  ( T `  ( n  -  1 ) ) ) ) )  e.  RR )
288108, 287remulcld 9622 . . . . . . . . . 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 )
289157, 288fsumrecl 13530 . . . . . . . . 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 )
290289recnd 9620 . . . . . . . 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 )
2912, 8rplogcld 22879 . . . . . . . . 9  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  e.  RR+ )
292291rpne0d 11265 . . . . . . . 8  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  =/=  0 )
29310rpne0d 11265 . . . . . . . 8  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  x  =/=  0 )
294290, 281, 66, 292, 293divdiv1d 10352 . . . . . . 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 ) ) )
295283, 294eqtr4d 2485 . . . . . 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
) )
296295oveq2d 6293 . . . . 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
) ) )
29771recnd 9620 . . . . . . . . . 10  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( R `  x )  e.  CC )
298297abscld 13241 . . . . . . . . 9  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( R `  x ) )  e.  RR )
299298, 280remulcld 9622 . . . . . . . 8  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( abs `  ( R `  x )
)  x.  ( log `  x ) )  e.  RR )
300108, 284remulcld 9622 . . . . . . . . . 10  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  ( ( S `  n )  -  ( S `  ( n  -  1 ) ) ) )  e.  RR )
301157, 300fsumrecl 13530 . . . . . . . . 9  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( abs `  ( R `  ( x  /  n ) ) )  x.  ( ( S `
 n )  -  ( S `  ( n  -  1 ) ) ) )  e.  RR )
302301, 291rerpdivcld 11287 . . . . . . . 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 )
303299, 302resubcld 9988 . . . . . . 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 )
304303recnd 9620 . . . . . 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 )
305290, 281, 292divcld 10321 . . . . . 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 )
306304, 305, 66, 293divdird 10359 . . . . 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
) ) )
307299recnd 9620 . . . . . . . 8  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( abs `  ( R `  x )
)  x.  ( log `  x ) )  e.  CC )
308302recnd 9620 . . . . . . . 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 )
309307, 308, 305subsubd 9959 . . . . . . 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
) ) ) )
310 2cnd 10609 . . . . . . . . . . . 12  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  2  e.  CC )
311269, 270subcld 9931 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( T `  n )  -  ( T `  ( n  -  1
) ) )  e.  CC )
312109, 311mulcld 9614 . . . . . . . . . . . 12  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  ( ( T `  n )  -  ( T `  ( n  -  1 ) ) ) )  e.  CC )
313157, 310, 312fsummulc2 13573 . . . . . . . . . . 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 ) ) ) ) ) )
314284recnd 9620 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( S `  n )  -  ( S `  ( n  -  1
) ) )  e.  CC )
315268, 311mulcld 9614 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( ( T `
 n )  -  ( T `  ( n  -  1 ) ) ) )  e.  CC )
316314, 315nncand 9936 . . . . . . . . . . . . . 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 ) ) ) ) )
317316oveq2d 6293 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `