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

Theorem pntrlog2bndlem4 24474
Description: Lemma for pntrlog2bnd 24478. 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 11700 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( 1 (,) +oo )  ->  x  e.  RR )
21adantl 472 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  x  e.  RR )
3 1rp 11340 . . . . . . . . . . . . . . . . . . . 20  |-  1  e.  RR+
43a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  1  e.  RR+ )
5 1red 9689 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  1  e.  RR )
6 eliooord 11728 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ( 1 (,) +oo )  ->  ( 1  <  x  /\  x  < +oo ) )
76adantl 472 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1  <  x  /\  x  < +oo ) )
87simpld 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  1  <  x )
95, 2, 8ltled 9814 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  1  <_  x )
102, 4, 9rpgecld 11411 . . . . . . . . . . . . . . . . . 18  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  x  e.  RR+ )
1110rprege0d 11382 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  e.  RR  /\  0  <_  x ) )
12 flge0nn0 12092 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  RR  /\  0  <_  x )  -> 
( |_ `  x
)  e.  NN0 )
1311, 12syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( |_ `  x )  e. 
NN0 )
14 nn0p1nn 10943 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( |_ `  x )  e.  NN0  ->  ( ( |_ `  x )  +  1 )  e.  NN )
1513, 14syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  NN )
1615nnrpd 11373 . . . . . . . . . . . . . . . . . 18  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  RR+ )
1710, 16rpdivcld 11392 . . . . . . . . . . . . . . . . 17  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  e.  RR+ )
18 pntrlog2bnd.r . . . . . . . . . . . . . . . . . 18  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
1918pntrval 24456 . . . . . . . . . . . . . . . . 17  |-  ( ( x  /  ( ( |_ `  x )  +  1 ) )  e.  RR+  ->  ( R `
 ( x  / 
( ( |_ `  x )  +  1 ) ) )  =  ( (ψ `  (
x  /  ( ( |_ `  x )  +  1 ) ) )  -  ( x  /  ( ( |_
`  x )  +  1 ) ) ) )
2017, 19syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( R `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  =  ( (ψ `  ( x  /  (
( |_ `  x
)  +  1 ) ) )  -  (
x  /  ( ( |_ `  x )  +  1 ) ) ) )
212, 15nndivred 10691 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  e.  RR )
22 2re 10712 . . . . . . . . . . . . . . . . . . . 20  |-  2  e.  RR
2322a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  2  e.  RR )
24 flltp1 12074 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  x  <  ( ( |_ `  x )  +  1 ) )
252, 24syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  x  <  ( ( |_ `  x )  +  1 ) )
2615nncnd 10658 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  CC )
2726mulid1d 9691 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( |_ `  x )  +  1 )  x.  1 )  =  ( ( |_
`  x )  +  1 ) )
2825, 27breqtrrd 4445 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  x  <  ( ( ( |_
`  x )  +  1 )  x.  1 ) )
292, 5, 16ltdivmuld 11423 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( x  /  (
( |_ `  x
)  +  1 ) )  <  1  <->  x  <  ( ( ( |_
`  x )  +  1 )  x.  1 ) ) )
3028, 29mpbird 240 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  <  1 )
31 1lt2 10810 . . . . . . . . . . . . . . . . . . . 20  |-  1  <  2
3231a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  1  <  2 )
3321, 5, 23, 30, 32lttrd 9827 . . . . . . . . . . . . . . . . . 18  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  <  2 )
34 chpeq0 24192 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  /  ( ( |_ `  x )  +  1 ) )  e.  RR  ->  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  =  0  <->  ( x  /  ( ( |_
`  x )  +  1 ) )  <  2 ) )
3521, 34syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  =  0  <->  ( x  /  ( ( |_
`  x )  +  1 ) )  <  2 ) )
3633, 35mpbird 240 . . . . . . . . . . . . . . . . 17  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (ψ `  ( x  /  (
( |_ `  x
)  +  1 ) ) )  =  0 )
3736oveq1d 6335 . . . . . . . . . . . . . . . 16  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  -  ( x  / 
( ( |_ `  x )  +  1 ) ) )  =  ( 0  -  (
x  /  ( ( |_ `  x )  +  1 ) ) ) )
3820, 37eqtrd 2496 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( R `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  =  ( 0  -  ( x  /  (
( |_ `  x
)  +  1 ) ) ) )
3938fveq2d 5896 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( R `  ( x  /  (
( |_ `  x
)  +  1 ) ) ) )  =  ( abs `  (
0  -  ( x  /  ( ( |_
`  x )  +  1 ) ) ) ) )
40 0red 9675 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  0  e.  RR )
4117rpge0d 11379 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  0  <_  ( x  /  (
( |_ `  x
)  +  1 ) ) )
4240, 21, 41abssuble0d 13549 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( 0  -  ( x  /  (
( |_ `  x
)  +  1 ) ) ) )  =  ( ( x  / 
( ( |_ `  x )  +  1 ) )  -  0 ) )
4321recnd 9700 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  e.  CC )
4443subid1d 10006 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( x  /  (
( |_ `  x
)  +  1 ) )  -  0 )  =  ( x  / 
( ( |_ `  x )  +  1 ) ) )
4539, 42, 443eqtrd 2500 . . . . . . . . . . . . 13  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( R `  ( x  /  (
( |_ `  x
)  +  1 ) ) ) )  =  ( x  /  (
( |_ `  x
)  +  1 ) ) )
4613nn0red 10960 . . . . . . . . . . . . . . . 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 24470 . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . 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 10961 . . . . . . . . . . . . . . . . 17  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( |_ `  x )  e.  CC )
51 1cnd 9690 . . . . . . . . . . . . . . . . 17  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  1  e.  CC )
5250, 51pncand 10018 . . . . . . . . . . . . . . . 16  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( |_ `  x )  +  1 )  -  1 )  =  ( |_ `  x ) )
5352fveq2d 5896 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( S `  ( (
( |_ `  x
)  +  1 )  -  1 ) )  =  ( S `  ( |_ `  x ) ) )
5447pntsval2 24470 . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . 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 12083 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  RR  ->  ( |_ `  ( |_ `  x ) )  =  ( |_ `  x
) )
572, 56syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( |_ `  ( |_ `  x ) )  =  ( |_ `  x
) )
5857oveq2d 6336 . . . . . . . . . . . . . . . . 17  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1 ... ( |_ `  ( |_ `  x ) ) )  =  ( 1 ... ( |_
`  x ) ) )
5958sumeq1d 13822 . . . . . . . . . . . . . . . 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 2499 . . . . . . . . . . . . . . 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 2506 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( S `  ( (
( |_ `  x
)  +  1 )  -  1 ) )  =  ( S `  x ) )
6252fveq2d 5896 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( T `  ( (
( |_ `  x
)  +  1 )  -  1 ) )  =  ( T `  ( |_ `  x ) ) )
6362oveq2d 6336 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
2  x.  ( T `
 ( ( ( |_ `  x )  +  1 )  - 
1 ) ) )  =  ( 2  x.  ( T `  ( |_ `  x ) ) ) )
6461, 63oveq12d 6338 . . . . . . . . . . . . 13  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( S `  (
( ( |_ `  x )  +  1 )  -  1 ) )  -  ( 2  x.  ( T `  ( ( ( |_
`  x )  +  1 )  -  1 ) ) ) )  =  ( ( S `
 x )  -  ( 2  x.  ( T `  ( |_ `  x ) ) ) ) )
6545, 64oveq12d 6338 . . . . . . . . . . . 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 9700 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  x  e.  CC )
6766div1d 10408 . . . . . . . . . . . . . . . . . 18  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  /  1 )  =  x )
6867fveq2d 5896 . . . . . . . . . . . . . . . . 17  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( R `  ( x  /  1 ) )  =  ( R `  x ) )
6918pntrf 24457 . . . . . . . . . . . . . . . . . . 19  |-  R : RR+
--> RR
7069ffvelrni 6049 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  RR+  ->  ( R `
 x )  e.  RR )
7110, 70syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( R `  x )  e.  RR )
7268, 71eqeltrd 2540 . . . . . . . . . . . . . . . 16  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( R `  ( x  /  1 ) )  e.  RR )
7372recnd 9700 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( R `  ( x  /  1 ) )  e.  CC )
7473abscld 13553 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( R `  ( x  /  1
) ) )  e.  RR )
7574recnd 9700 . . . . . . . . . . . . 13  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( R `  ( x  /  1
) ) )  e.  CC )
7675mul01d 9863 . . . . . . . . . . . 12  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( abs `  ( R `  ( x  /  1 ) ) )  x.  0 )  =  0 )
7765, 76oveq12d 6338 . . . . . . . . . . 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 24467 . . . . . . . . . . . . . . . . 17  |-  S : RR
--> RR
7978ffvelrni 6049 . . . . . . . . . . . . . . . 16  |-  ( x  e.  RR  ->  ( S `  x )  e.  RR )
802, 79syl 17 . . . . . . . . . . . . . . 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 23581 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  e.  RR+  ->  ( log `  a )  e.  RR )
83 remulcl 9655 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( a  e.  RR  /\  ( log `  a )  e.  RR )  -> 
( a  x.  ( log `  a ) )  e.  RR )
8482, 83sylan2 481 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( a  e.  RR  /\  a  e.  RR+ )  -> 
( a  x.  ( log `  a ) )  e.  RR )
85 0red 9675 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( a  e.  RR  /\  -.  a  e.  RR+ )  ->  0  e.  RR )
8684, 85ifclda 3925 . . . . . . . . . . . . . . . . . . 19  |-  ( a  e.  RR  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  e.  RR )
8781, 86fmpti 6073 . . . . . . . . . . . . . . . . . 18  |-  T : RR
--> RR
8887ffvelrni 6049 . . . . . . . . . . . . . . . . 17  |-  ( ( |_ `  x )  e.  RR  ->  ( T `  ( |_ `  x ) )  e.  RR )
8946, 88syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( T `  ( |_ `  x ) )  e.  RR )
9023, 89remulcld 9702 . . . . . . . . . . . . . . 15  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
2  x.  ( T `
 ( |_ `  x ) ) )  e.  RR )
9180, 90resubcld 10080 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( S `  x
)  -  ( 2  x.  ( T `  ( |_ `  x ) ) ) )  e.  RR )
9221, 91remulcld 9702 . . . . . . . . . . . . 13  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( x  /  (
( |_ `  x
)  +  1 ) )  x.  ( ( S `  x )  -  ( 2  x.  ( T `  ( |_ `  x ) ) ) ) )  e.  RR )
9392recnd 9700 . . . . . . . . . . . 12  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( x  /  (
( |_ `  x
)  +  1 ) )  x.  ( ( S `  x )  -  ( 2  x.  ( T `  ( |_ `  x ) ) ) ) )  e.  CC )
9493subid1d 10006 . . . . . . . . . . 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 2496 . . . . . . . . . 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 12072 . . . . . . . . . . . . . 14  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( |_ `  x )  e.  ZZ )
97 fzval3 12020 . . . . . . . . . . . . . 14  |-  ( ( |_ `  x )  e.  ZZ  ->  (
1 ... ( |_ `  x ) )  =  ( 1..^ ( ( |_ `  x )  +  1 ) ) )
9896, 97syl 17 . . . . . . . . . . . . 13  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1 ... ( |_ `  x ) )  =  ( 1..^ ( ( |_ `  x )  +  1 ) ) )
9998eqcomd 2468 . . . . . . . . . . . 12  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1..^ ( ( |_
`  x )  +  1 ) )  =  ( 1 ... ( |_ `  x ) ) )
10010adantr 471 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR+ )
101 elfznn 11863 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
102101adantl 472 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
103102nnrpd 11373 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR+ )
104100, 103rpdivcld 11392 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
10569ffvelrni 6049 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  /  n )  e.  RR+  ->  ( R `
 ( x  /  n ) )  e.  RR )
106104, 105syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  e.  RR )
107106recnd 9700 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  e.  CC )
108107abscld 13553 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( R `  (
x  /  n ) ) )  e.  RR )
109108recnd 9700 . . . . . . . . . . . . . . . 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 11390 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  +  1 )  e.  RR+ )
112100, 111rpdivcld 11392 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  ( n  + 
1 ) )  e.  RR+ )
11369ffvelrni 6049 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  /  ( n  +  1 ) )  e.  RR+  ->  ( R `
 ( x  / 
( n  +  1 ) ) )  e.  RR )
114112, 113syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  (
n  +  1 ) ) )  e.  RR )
115114recnd 9700 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  (
n  +  1 ) ) )  e.  CC )
116115abscld 13553 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( R `  (
x  /  ( n  +  1 ) ) ) )  e.  RR )
117116recnd 9700 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( R `  (
x  /  ( n  +  1 ) ) ) )  e.  CC )
118109, 117negsubdi2d 10033 . . . . . . . . . . . . . . 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 2468 . . . . . . . . . . . . . 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 10658 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  CC )
121 1cnd 9690 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  CC )
122120, 121pncand 10018 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
n  +  1 )  -  1 )  =  n )
123122fveq2d 5896 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( S `  ( ( n  + 
1 )  -  1 ) )  =  ( S `  n ) )
124122fveq2d 5896 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  ( ( n  + 
1 )  -  1 ) )  =  ( T `  n ) )
125 rpre 11342 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  RR+  ->  n  e.  RR )
126 eleq1 2528 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  n  ->  (
a  e.  RR+  <->  n  e.  RR+ ) )
127 id 22 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  n  ->  a  =  n )
128 fveq2 5892 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  n  ->  ( log `  a )  =  ( log `  n
) )
129127, 128oveq12d 6338 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  n  ->  (
a  x.  ( log `  a ) )  =  ( n  x.  ( log `  n ) ) )
130126, 129ifbieq1d 3916 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  n  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  if ( n  e.  RR+ ,  ( n  x.  ( log `  n
) ) ,  0 ) )
131 ovex 6348 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  x.  ( log `  n
) )  e.  _V
132 c0ex 9668 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  _V
133131, 132ifex 3961 . . . . . . . . . . . . . . . . . . . . 21  |-  if ( n  e.  RR+ ,  ( n  x.  ( log `  n ) ) ,  0 )  e.  _V
134130, 81, 133fvmpt 5976 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  RR  ->  ( T `  n )  =  if ( n  e.  RR+ ,  ( n  x.  ( log `  n
) ) ,  0 ) )
135125, 134syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  RR+  ->  ( T `
 n )  =  if ( n  e.  RR+ ,  ( n  x.  ( log `  n
) ) ,  0 ) )
136 iftrue 3899 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  RR+  ->  if ( n  e.  RR+ ,  ( n  x.  ( log `  n ) ) ,  0 )  =  ( n  x.  ( log `  n ) ) )
137135, 136eqtrd 2496 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  RR+  ->  ( T `
 n )  =  ( n  x.  ( log `  n ) ) )
138103, 137syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  n )  =  ( n  x.  ( log `  n ) ) )
139124, 138eqtrd 2496 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  ( ( n  + 
1 )  -  1 ) )  =  ( n  x.  ( log `  n ) ) )
140139oveq2d 6336 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( T `  ( ( n  + 
1 )  -  1 ) ) )  =  ( 2  x.  (
n  x.  ( log `  n ) ) ) )
141123, 140oveq12d 6338 . . . . . . . . . . . . . 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 6338 . . . . . . . . . . . . 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 10080 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  -  ( abs `  ( R `
 ( x  / 
( n  +  1 ) ) ) ) )  e.  RR )
144143recnd 9700 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  -  ( abs `  ( R `
 ( x  / 
( n  +  1 ) ) ) ) )  e.  CC )
145102nnred 10657 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR )
14678ffvelrni 6049 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  RR  ->  ( S `  n )  e.  RR )
147145, 146syl 17 . . . . . . . . . . . . . . . 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 23628 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  n )  e.  RR )
150145, 149remulcld 9702 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  x.  ( log `  n
) )  e.  RR )
151148, 150remulcld 9702 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( n  x.  ( log `  n
) ) )  e.  RR )
152147, 151resubcld 10080 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( S `  n )  -  ( 2  x.  ( n  x.  ( log `  n ) ) ) )  e.  RR )
153152recnd 9700 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( S `  n )  -  ( 2  x.  ( n  x.  ( log `  n ) ) ) )  e.  CC )
154144, 153mulneg1d 10104 . . . . . . . . . . . . 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 2496 . . . . . . . . . . . 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 13828 . . . . . . . . . . 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 12224 . . . . . . . . . . . 12  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1 ... ( |_ `  x ) )  e. 
Fin )
158143, 152remulcld 9702 . . . . . . . . . . . . 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 9700 . . . . . . . . . . . 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 13903 . . . . . . . . . . 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 2496 . . . . . . . . . 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 6338 . . . . . . . . 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 6328 . . . . . . . . . . . . . 14  |-  ( m  =  n  ->  (
x  /  m )  =  ( x  /  n ) )
164163fveq2d 5896 . . . . . . . . . . . . 13  |-  ( m  =  n  ->  ( R `  ( x  /  m ) )  =  ( R `  (
x  /  n ) ) )
165164fveq2d 5896 . . . . . . . . . . . 12  |-  ( m  =  n  ->  ( abs `  ( R `  ( x  /  m
) ) )  =  ( abs `  ( R `  ( x  /  n ) ) ) )
166 oveq1 6327 . . . . . . . . . . . . . 14  |-  ( m  =  n  ->  (
m  -  1 )  =  ( n  - 
1 ) )
167166fveq2d 5896 . . . . . . . . . . . . 13  |-  ( m  =  n  ->  ( S `  ( m  -  1 ) )  =  ( S `  ( n  -  1
) ) )
168166fveq2d 5896 . . . . . . . . . . . . . 14  |-  ( m  =  n  ->  ( T `  ( m  -  1 ) )  =  ( T `  ( n  -  1
) ) )
169168oveq2d 6336 . . . . . . . . . . . . 13  |-  ( m  =  n  ->  (
2  x.  ( T `
 ( m  - 
1 ) ) )  =  ( 2  x.  ( T `  (
n  -  1 ) ) ) )
170167, 169oveq12d 6338 . . . . . . . . . . . 12  |-  ( m  =  n  ->  (
( S `  (
m  -  1 ) )  -  ( 2  x.  ( T `  ( m  -  1
) ) ) )  =  ( ( S `
 ( n  - 
1 ) )  -  ( 2  x.  ( T `  ( n  -  1 ) ) ) ) )
171165, 170jca 539 . . . . . . . . . . 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 6328 . . . . . . . . . . . . . 14  |-  ( m  =  ( n  + 
1 )  ->  (
x  /  m )  =  ( x  / 
( n  +  1 ) ) )
173172fveq2d 5896 . . . . . . . . . . . . 13  |-  ( m  =  ( n  + 
1 )  ->  ( R `  ( x  /  m ) )  =  ( R `  (
x  /  ( n  +  1 ) ) ) )
174173fveq2d 5896 . . . . . . . . . . . 12  |-  ( m  =  ( n  + 
1 )  ->  ( abs `  ( R `  ( x  /  m
) ) )  =  ( abs `  ( R `  ( x  /  ( n  + 
1 ) ) ) ) )
175 oveq1 6327 . . . . . . . . . . . . . 14  |-  ( m  =  ( n  + 
1 )  ->  (
m  -  1 )  =  ( ( n  +  1 )  - 
1 ) )
176175fveq2d 5896 . . . . . . . . . . . . 13  |-  ( m  =  ( n  + 
1 )  ->  ( S `  ( m  -  1 ) )  =  ( S `  ( ( n  + 
1 )  -  1 ) ) )
177175fveq2d 5896 . . . . . . . . . . . . . 14  |-  ( m  =  ( n  + 
1 )  ->  ( T `  ( m  -  1 ) )  =  ( T `  ( ( n  + 
1 )  -  1 ) ) )
178177oveq2d 6336 . . . . . . . . . . . . 13  |-  ( m  =  ( n  + 
1 )  ->  (
2  x.  ( T `
 ( m  - 
1 ) ) )  =  ( 2  x.  ( T `  (
( n  +  1 )  -  1 ) ) ) )
179176, 178oveq12d 6338 . . . . . . . . . . . 12  |-  ( m  =  ( n  + 
1 )  ->  (
( S `  (
m  -  1 ) )  -  ( 2  x.  ( T `  ( m  -  1
) ) ) )  =  ( ( S `
 ( ( n  +  1 )  - 
1 ) )  -  ( 2  x.  ( T `  ( (
n  +  1 )  -  1 ) ) ) ) )
180174, 179jca 539 . . . . . . . . . . 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 6328 . . . . . . . . . . . . . 14  |-  ( m  =  1  ->  (
x  /  m )  =  ( x  / 
1 ) )
182181fveq2d 5896 . . . . . . . . . . . . 13  |-  ( m  =  1  ->  ( R `  ( x  /  m ) )  =  ( R `  (
x  /  1 ) ) )
183182fveq2d 5896 . . . . . . . . . . . 12  |-  ( m  =  1  ->  ( abs `  ( R `  ( x  /  m
) ) )  =  ( abs `  ( R `  ( x  /  1 ) ) ) )
184 oveq1 6327 . . . . . . . . . . . . . . . . 17  |-  ( m  =  1  ->  (
m  -  1 )  =  ( 1  -  1 ) )
185 1m1e0 10711 . . . . . . . . . . . . . . . . 17  |-  ( 1  -  1 )  =  0
186184, 185syl6eq 2512 . . . . . . . . . . . . . . . 16  |-  ( m  =  1  ->  (
m  -  1 )  =  0 )
187186fveq2d 5896 . . . . . . . . . . . . . . 15  |-  ( m  =  1  ->  ( S `  ( m  -  1 ) )  =  ( S ` 
0 ) )
188 0re 9674 . . . . . . . . . . . . . . . 16  |-  0  e.  RR
189 fveq2 5892 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  0  ->  ( |_ `  a )  =  ( |_ `  0
) )
190 0z 10982 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  ZZ
191 flid 12082 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 0  e.  ZZ  ->  ( |_ `  0 )  =  0 )
192190, 191ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( |_
`  0 )  =  0
193189, 192syl6eq 2512 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  0  ->  ( |_ `  a )  =  0 )
194193oveq2d 6336 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  0  ->  (
1 ... ( |_ `  a ) )  =  ( 1 ... 0
) )
195 fz10 11855 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1 ... 0 )  =  (/)
196194, 195syl6eq 2512 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  0  ->  (
1 ... ( |_ `  a ) )  =  (/) )
197196sumeq1d 13822 . . . . . . . . . . . . . . . . . 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 13842 . . . . . . . . . . . . . . . . . 18  |-  sum_ i  e.  (/)  ( (Λ `  i
)  x.  ( ( log `  i )  +  (ψ `  (
a  /  i ) ) ) )  =  0
199197, 198syl6eq 2512 . . . . . . . . . . . . . . . . 17  |-  ( a  =  0  ->  sum_ i  e.  ( 1 ... ( |_ `  a ) ) ( (Λ `  i
)  x.  ( ( log `  i )  +  (ψ `  (
a  /  i ) ) ) )  =  0 )
200199, 47, 132fvmpt 5976 . . . . . . . . . . . . . . . 16  |-  ( 0  e.  RR  ->  ( S `  0 )  =  0 )
201188, 200ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( S `
 0 )  =  0
202187, 201syl6eq 2512 . . . . . . . . . . . . . 14  |-  ( m  =  1  ->  ( S `  ( m  -  1 ) )  =  0 )
203186fveq2d 5896 . . . . . . . . . . . . . . . . 17  |-  ( m  =  1  ->  ( T `  ( m  -  1 ) )  =  ( T ` 
0 ) )
204 rpne0 11351 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  e.  RR+  ->  a  =/=  0 )
205204necon2bi 2666 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  0  ->  -.  a  e.  RR+ )
206205iffalsed 3904 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  0  ->  if ( a  e.  RR+ ,  ( a  x.  ( log `  a ) ) ,  0 )  =  0 )
207206, 81, 132fvmpt 5976 . . . . . . . . . . . . . . . . . 18  |-  ( 0  e.  RR  ->  ( T `  0 )  =  0 )
208188, 207ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( T `
 0 )  =  0
209203, 208syl6eq 2512 . . . . . . . . . . . . . . . 16  |-  ( m  =  1  ->  ( T `  ( m  -  1 ) )  =  0 )
210209oveq2d 6336 . . . . . . . . . . . . . . 15  |-  ( m  =  1  ->  (
2  x.  ( T `
 ( m  - 
1 ) ) )  =  ( 2  x.  0 ) )
211 2t0e0 10799 . . . . . . . . . . . . . . 15  |-  ( 2  x.  0 )  =  0
212210, 211syl6eq 2512 . . . . . . . . . . . . . 14  |-  ( m  =  1  ->  (
2  x.  ( T `
 ( m  - 
1 ) ) )  =  0 )
213202, 212oveq12d 6338 . . . . . . . . . . . . 13  |-  ( m  =  1  ->  (
( S `  (
m  -  1 ) )  -  ( 2  x.  ( T `  ( m  -  1
) ) ) )  =  ( 0  -  0 ) )
214 0m0e0 10752 . . . . . . . . . . . . 13  |-  ( 0  -  0 )  =  0
215213, 214syl6eq 2512 . . . . . . . . . . . 12  |-  ( m  =  1  ->  (
( S `  (
m  -  1 ) )  -  ( 2  x.  ( T `  ( m  -  1
) ) ) )  =  0 )
216183, 215jca 539 . . . . . . . . . . 11  |-  ( m  =  1  ->  (
( abs `  ( R `  ( x  /  m ) ) )  =  ( abs `  ( R `  ( x  /  1 ) ) )  /\  ( ( S `  ( m  -  1 ) )  -  ( 2  x.  ( T `  (
m  -  1 ) ) ) )  =  0 ) )
217 oveq2 6328 . . . . . . . . . . . . . 14  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (
x  /  m )  =  ( x  / 
( ( |_ `  x )  +  1 ) ) )
218217fveq2d 5896 . . . . . . . . . . . . 13  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  ( R `  ( x  /  m ) )  =  ( R `  (
x  /  ( ( |_ `  x )  +  1 ) ) ) )
219218fveq2d 5896 . . . . . . . . . . . 12  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  ( abs `  ( R `  ( x  /  m
) ) )  =  ( abs `  ( R `  ( x  /  ( ( |_
`  x )  +  1 ) ) ) ) )
220 oveq1 6327 . . . . . . . . . . . . . 14  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (
m  -  1 )  =  ( ( ( |_ `  x )  +  1 )  - 
1 ) )
221220fveq2d 5896 . . . . . . . . . . . . 13  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  ( S `  ( m  -  1 ) )  =  ( S `  ( ( ( |_
`  x )  +  1 )  -  1 ) ) )
222220fveq2d 5896 . . . . . . . . . . . . . 14  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  ( T `  ( m  -  1 ) )  =  ( T `  ( ( ( |_
`  x )  +  1 )  -  1 ) ) )
223222oveq2d 6336 . . . . . . . . . . . . 13  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (
2  x.  ( T `
 ( m  - 
1 ) ) )  =  ( 2  x.  ( T `  (
( ( |_ `  x )  +  1 )  -  1 ) ) ) )
224221, 223oveq12d 6338 . . . . . . . . . . . 12  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (
( S `  (
m  -  1 ) )  -  ( 2  x.  ( T `  ( m  -  1
) ) ) )  =  ( ( S `
 ( ( ( |_ `  x )  +  1 )  - 
1 ) )  -  ( 2  x.  ( T `  ( (
( |_ `  x
)  +  1 )  -  1 ) ) ) ) )
225219, 224jca 539 . . . . . . . . . . 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 11228 . . . . . . . . . . . 12  |-  NN  =  ( ZZ>= `  1 )
22715, 226syl6eleq 2550 . . . . . . . . . . 11  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  ( ZZ>= `  1
) )
22810adantr 471 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  x  e.  RR+ )
229 elfznn 11863 . . . . . . . . . . . . . . . . . 18  |-  ( m  e.  ( 1 ... ( ( |_ `  x )  +  1 ) )  ->  m  e.  NN )
230229adantl 472 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  m  e.  NN )
231230nnrpd 11373 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  m  e.  RR+ )
232228, 231rpdivcld 11392 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
x  /  m )  e.  RR+ )
23369ffvelrni 6049 . . . . . . . . . . . . . . 15  |-  ( ( x  /  m )  e.  RR+  ->  ( R `
 ( x  /  m ) )  e.  RR )
234232, 233syl 17 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  ( R `  ( x  /  m ) )  e.  RR )
235234recnd 9700 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  ( R `  ( x  /  m ) )  e.  CC )
236235abscld 13553 . . . . . . . . . . . 12  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  ( abs `  ( R `  ( x  /  m
) ) )  e.  RR )
237236recnd 9700 . . . . . . . . . . 11  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  ( abs `  ( R `  ( x  /  m
) ) )  e.  CC )
238230nnred 10657 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  m  e.  RR )
239 1red 9689 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  1  e.  RR )
240238, 239resubcld 10080 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
m  -  1 )  e.  RR )
24178ffvelrni 6049 . . . . . . . . . . . . . 14  |-  ( ( m  -  1 )  e.  RR  ->  ( S `  ( m  -  1 ) )  e.  RR )
242240, 241syl 17 . . . . . . . . . . . . 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 6049 . . . . . . . . . . . . . . 15  |-  ( ( m  -  1 )  e.  RR  ->  ( T `  ( m  -  1 ) )  e.  RR )
245240, 244syl 17 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  ( T `  ( m  -  1 ) )  e.  RR )
246243, 245remulcld 9702 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
2  x.  ( T `
 ( m  - 
1 ) ) )  e.  RR )
247242, 246resubcld 10080 . . . . . . . . . . . 12  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
( S `  (
m  -  1 ) )  -  ( 2  x.  ( T `  ( m  -  1
) ) ) )  e.  RR )
248247recnd 9700 . . . . . . . . . . 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 13921 . . . . . . . . . 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 9700 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( S `  n )  e.  CC )
25187ffvelrni 6049 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  RR  ->  ( T `  n )  e.  RR )
252145, 251syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  n )  e.  RR )
253148, 252remulcld 9702 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( T `  n ) )  e.  RR )
254253recnd 9700 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( T `  n ) )  e.  CC )
255 1red 9689 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR )
256145, 255resubcld 10080 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  -  1 )  e.  RR )
25778ffvelrni 6049 . . . . . . . . . . . . . . . 16  |-  ( ( n  -  1 )  e.  RR  ->  ( S `  ( n  -  1 ) )  e.  RR )
258256, 257syl 17 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( S `  ( n  -  1 ) )  e.  RR )
259258recnd 9700 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( S `  ( n  -  1 ) )  e.  CC )
26087ffvelrni 6049 . . . . . . . . . . . . . . . . 17  |-  ( ( n  -  1 )  e.  RR  ->  ( T `  ( n  -  1 ) )  e.  RR )
261256, 260syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  ( n  -  1 ) )  e.  RR )
262148, 261remulcld 9702 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( T `  ( n  -  1
) ) )  e.  RR )
263262recnd 9700 . . . . . . . . . . . . . 14  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( T `  ( n  -  1
) ) )  e.  CC )
264250, 254, 259, 263sub4d 10066 . . . . . . . . . . . . 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 6336 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( T `  ( ( n  + 
1 )  -  1 ) ) )  =  ( 2  x.  ( T `  n )
) )
266123, 265oveq12d 6338 . . . . . . . . . . . . . 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 6335 . . . . . . . . . . . . 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 10715 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  2  e.  CC )
269252recnd 9700 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  n )  e.  CC )
270261recnd 9700 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( T `  ( n  -  1 ) )  e.  CC )
271268, 269, 270subdid 10107 . . . . . . . . . . . . . 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 6336 . . . . . . . . . . . . 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 2506 . . . . . . . . . . . 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 6336 . . . . . . . . . . 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 13828 . . . . . . . . . 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 2498 . . . . . . . . 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 13854 . . . . . . . . . 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 10024 . . . . . . . . 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 2505 . . . . . . . 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 23628 . . . . . . . . . 10  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  e.  RR )
281280recnd 9700 . . . . . . . . 9  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  e.  CC )
28266, 281mulcomd 9695 . . . . . . . 8  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  x.  ( log `  x ) )  =  ( ( log `  x
)  x.  x ) )
283279, 282oveq12d 6338 . . . . . . 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 10080 . . . . . . . . . . . 12  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( S `  n )  -  ( S `  ( n  -  1
) ) )  e.  RR )
285252, 261resubcld 10080 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( T `  n )  -  ( T `  ( n  -  1
) ) )  e.  RR )
286148, 285remulcld 9702 . . . . . . . . . . . 12  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( ( T `
 n )  -  ( T `  ( n  -  1 ) ) ) )  e.  RR )
287284, 286resubcld 10080 . . . . . . . . . . 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 9702 . . . . . . . . . 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 13855 . . . . . . . . 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 9700 . . . . . . . 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 23634 . . . . . . . . 9  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  e.  RR+ )
292291rpne0d 11380 . . . . . . . 8  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  =/=  0 )
29310rpne0d 11380 . . . . . . . 8  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  x  =/=  0 )
294290, 281, 66, 292, 293divdiv1d 10447 . . . . . . 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 2499 . . . . . 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 6336 . . . . 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 9700 . . . . . . . . . 10  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( R `  x )  e.  CC )
298297abscld 13553 . . . . . . . . 9  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( R `  x ) )  e.  RR )
299298, 280remulcld 9702 . . . . . . . 8  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( abs `  ( R `  x )
)  x.  ( log `  x ) )  e.  RR )
300108, 284remulcld 9702 . . . . . . . . . 10  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( R `  ( x  /  n
) ) )  x.  ( ( S `  n )  -  ( S `  ( n  -  1 ) ) ) )  e.  RR )
301157, 300fsumrecl 13855 . . . . . . . . 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 11403 . . . . . . . 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 10080 . . . . . . 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 9700 . . . . . 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 10416 . . . . . 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 10454 . . . . 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 9700 . . . . . . . 8  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( abs `  ( R `  x )
)  x.  ( log `  x ) )  e.  CC )
308302recnd 9700 . . . . . . . 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 10045 . . . . . . 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 10715 . . . . . . . . . . . 12  |-  ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  ->  2  e.  CC )
311269, 270subcld 10017 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( T `  n )  -  ( T `  ( n  -  1
) ) )  e.  CC )
312109, 311mulcld 9694 . . . . . . . . . . . 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 13900 . . . . . . . . . . 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 9700 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( S `  n )  -  ( S `  ( n  -  1
) ) )  e.  CC )
315268, 311mulcld 9694 . . . . . . . . . . . . . . 15  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( ( T `
 n )  -  ( T `  ( n  -  1 ) ) ) )  e.  CC )
316314, 315nncand 10022 . . . . . . . . . . . . . 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 6336 . . . . . . . . . . . . 13  |-  ( ( ( T.  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs