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

Theorem selberg34r 20720
Description: The sum of selberg3r 20718 and selberg4r 20719. (Contributed by Mario Carneiro, 31-May-2016.)
Hypothesis
Ref Expression
pntrval.r  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
Assertion
Ref Expression
selberg34r  |-  ( x  e.  ( 1 (,) 
+oo )  |->  ( ( ( ( R `  x )  x.  ( log `  x ) )  -  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( R `  ( x  /  n
) )  x.  ( sum_ m  e.  { y  e.  NN  |  y 
||  n }  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) )  /  ( log `  x ) ) )  /  x ) )  e.  O ( 1 )
Distinct variable groups:    m, a, n, x    y, m, R, n, x
Allowed substitution hint:    R( a)

Proof of Theorem selberg34r
Dummy variable  k is distinct from all other variables.
StepHypRef Expression
1 2re 9815 . . . . . . . . . 10  |-  2  e.  RR
21a1i 10 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  2  e.  RR )
3 elioore 10686 . . . . . . . . . . . . 13  |-  ( x  e.  ( 1 (,) 
+oo )  ->  x  e.  RR )
43adantl 452 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  RR )
5 1rp 10358 . . . . . . . . . . . . 13  |-  1  e.  RR+
65a1i 10 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  RR+ )
76rpred 10390 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  RR )
8 eliooord 10710 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( 1 (,) 
+oo )  ->  (
1  <  x  /\  x  <  +oo ) )
98adantl 452 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  <  x  /\  x  <  +oo ) )
109simpld 445 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  <  x )
117, 4, 10ltled 8967 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  <_  x )
124, 6, 11rpgecld 10425 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  RR+ )
13 pntrval.r . . . . . . . . . . . . 13  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
1413pntrf 20712 . . . . . . . . . . . 12  |-  R : RR+
--> RR
1514ffvelrni 5664 . . . . . . . . . . 11  |-  ( x  e.  RR+  ->  ( R `
 x )  e.  RR )
1612, 15syl 15 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( R `  x )  e.  RR )
1712relogcld 19974 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  RR )
1816, 17remulcld 8863 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( R `  x
)  x.  ( log `  x ) )  e.  RR )
192, 18remulcld 8863 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  ( ( R `  x )  x.  ( log `  x
) ) )  e.  RR )
2019recnd 8861 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  ( ( R `  x )  x.  ( log `  x
) ) )  e.  CC )
214, 10rplogcld 19980 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  RR+ )
222, 21rerpdivcld 10417 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  /  ( log `  x ) )  e.  RR )
2322recnd 8861 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  /  ( log `  x ) )  e.  CC )
24 fzfid 11035 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1 ... ( |_ `  x ) )  e. 
Fin )
2512adantr 451 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR+ )
26 elfznn 10819 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
2726adantl 452 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
2827nnrpd 10389 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR+ )
2925, 28rpdivcld 10407 . . . . . . . . . . . 12  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
3014ffvelrni 5664 . . . . . . . . . . . 12  |-  ( ( x  /  n )  e.  RR+  ->  ( R `
 ( x  /  n ) )  e.  RR )
3129, 30syl 15 . . . . . . . . . . 11  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  e.  RR )
32 fzfid 11035 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1 ... n )  e. 
Fin )
33 sgmss 20344 . . . . . . . . . . . . . . 15  |-  ( n  e.  NN  ->  { y  e.  NN  |  y 
||  n }  C_  ( 1 ... n
) )
3427, 33syl 15 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  { y  e.  NN  |  y  ||  n }  C_  ( 1 ... n ) )
35 ssfi 7083 . . . . . . . . . . . . . 14  |-  ( ( ( 1 ... n
)  e.  Fin  /\  { y  e.  NN  | 
y  ||  n }  C_  ( 1 ... n
) )  ->  { y  e.  NN  |  y 
||  n }  e.  Fin )
3632, 34, 35syl2anc 642 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  { y  e.  NN  |  y  ||  n }  e.  Fin )
37 ssrab2 3258 . . . . . . . . . . . . . . . 16  |-  { y  e.  NN  |  y 
||  n }  C_  NN
38 simpr 447 . . . . . . . . . . . . . . . 16  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  {
y  e.  NN  | 
y  ||  n }
)  ->  m  e.  { y  e.  NN  | 
y  ||  n }
)
3937, 38sseldi 3178 . . . . . . . . . . . . . . 15  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  {
y  e.  NN  | 
y  ||  n }
)  ->  m  e.  NN )
40 vmacl 20356 . . . . . . . . . . . . . . 15  |-  ( m  e.  NN  ->  (Λ `  m )  e.  RR )
4139, 40syl 15 . . . . . . . . . . . . . 14  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  {
y  e.  NN  | 
y  ||  n }
)  ->  (Λ `  m
)  e.  RR )
42 dvdsdivcl 20421 . . . . . . . . . . . . . . . . 17  |-  ( ( n  e.  NN  /\  m  e.  { y  e.  NN  |  y  ||  n } )  ->  (
n  /  m )  e.  { y  e.  NN  |  y  ||  n } )
4327, 42sylan 457 . . . . . . . . . . . . . . . 16  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  {
y  e.  NN  | 
y  ||  n }
)  ->  ( n  /  m )  e.  {
y  e.  NN  | 
y  ||  n }
)
4437, 43sseldi 3178 . . . . . . . . . . . . . . 15  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  {
y  e.  NN  | 
y  ||  n }
)  ->  ( n  /  m )  e.  NN )
45 vmacl 20356 . . . . . . . . . . . . . . 15  |-  ( ( n  /  m )  e.  NN  ->  (Λ `  ( n  /  m
) )  e.  RR )
4644, 45syl 15 . . . . . . . . . . . . . 14  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  {
y  e.  NN  | 
y  ||  n }
)  ->  (Λ `  (
n  /  m ) )  e.  RR )
4741, 46remulcld 8863 . . . . . . . . . . . . 13  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  {
y  e.  NN  | 
y  ||  n }
)  ->  ( (Λ `  m )  x.  (Λ `  ( n  /  m
) ) )  e.  RR )
4836, 47fsumrecl 12207 . . . . . . . . . . . 12  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e. 
{ y  e.  NN  |  y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  e.  RR )
49 vmacl 20356 . . . . . . . . . . . . . 14  |-  ( n  e.  NN  ->  (Λ `  n )  e.  RR )
5027, 49syl 15 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n
)  e.  RR )
5128relogcld 19974 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  n )  e.  RR )
5250, 51remulcld 8863 . . . . . . . . . . . 12  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  ( log `  n ) )  e.  RR )
5348, 52resubcld 9211 . . . . . . . . . . 11  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( sum_ m  e.  { y  e.  NN  |  y  ||  n }  ( (Λ `  m )  x.  (Λ `  ( n  /  m
) ) )  -  ( (Λ `  n )  x.  ( log `  n
) ) )  e.  RR )
5431, 53remulcld 8863 . . . . . . . . . 10  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( R `  ( x  /  n ) )  x.  ( sum_ m  e.  {
y  e.  NN  | 
y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) )  e.  RR )
5524, 54fsumrecl 12207 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( R `  ( x  /  n
) )  x.  ( sum_ m  e.  { y  e.  NN  |  y 
||  n }  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) )  e.  RR )
5655recnd 8861 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( R `  ( x  /  n
) )  x.  ( sum_ m  e.  { y  e.  NN  |  y 
||  n }  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) )  e.  CC )
5723, 56mulcld 8855 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( R `  ( x  /  n
) )  x.  ( sum_ m  e.  { y  e.  NN  |  y 
||  n }  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) ) )  e.  CC )
5820, 57subcld 9157 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  x.  (
( R `  x
)  x.  ( log `  x ) ) )  -  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( R `  ( x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) ) ) )  e.  CC )
594recnd 8861 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  CC )
60 2cn 9816 . . . . . . 7  |-  2  e.  CC
6160a1i 10 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  2  e.  CC )
6212rpne0d 10395 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  =/=  0 )
63 2ne0 9829 . . . . . . 7  |-  2  =/=  0
6463a1i 10 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  2  =/=  0 )
6558, 59, 61, 62, 64divdiv32d 9561 . . . . 5  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( 2  x.  ( ( R `
 x )  x.  ( log `  x
) ) )  -  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( R `  ( x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) ) ) )  /  x )  /  2
)  =  ( ( ( ( 2  x.  ( ( R `  x )  x.  ( log `  x ) ) )  -  ( ( 2  /  ( log `  x ) )  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( R `  (
x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n }  ( (Λ `  m )  x.  (Λ `  ( n  /  m
) ) )  -  ( (Λ `  n )  x.  ( log `  n
) ) ) ) ) )  /  2
)  /  x ) )
6658, 59, 62divcld 9536 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( 2  x.  ( ( R `  x )  x.  ( log `  x ) ) )  -  ( ( 2  /  ( log `  x ) )  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( R `  (
x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n }  ( (Λ `  m )  x.  (Λ `  ( n  /  m
) ) )  -  ( (Λ `  n )  x.  ( log `  n
) ) ) ) ) )  /  x
)  e.  CC )
6766, 61, 64divrecd 9539 . . . . 5  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( 2  x.  ( ( R `
 x )  x.  ( log `  x
) ) )  -  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( R `  ( x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) ) ) )  /  x )  /  2
)  =  ( ( ( ( 2  x.  ( ( R `  x )  x.  ( log `  x ) ) )  -  ( ( 2  /  ( log `  x ) )  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( R `  (
x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n }  ( (Λ `  m )  x.  (Λ `  ( n  /  m
) ) )  -  ( (Λ `  n )  x.  ( log `  n
) ) ) ) ) )  /  x
)  x.  ( 1  /  2 ) ) )
6820, 57, 61, 64divsubdird 9575 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( 2  x.  ( ( R `  x )  x.  ( log `  x ) ) )  -  ( ( 2  /  ( log `  x ) )  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( R `  (
x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n }  ( (Λ `  m )  x.  (Λ `  ( n  /  m
) ) )  -  ( (Λ `  n )  x.  ( log `  n
) ) ) ) ) )  /  2
)  =  ( ( ( 2  x.  (
( R `  x
)  x.  ( log `  x ) ) )  /  2 )  -  ( ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( R `  ( x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) ) )  /  2
) ) )
6918recnd 8861 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( R `  x
)  x.  ( log `  x ) )  e.  CC )
7069, 61, 64divcan3d 9541 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  x.  (
( R `  x
)  x.  ( log `  x ) ) )  /  2 )  =  ( ( R `  x )  x.  ( log `  x ) ) )
7121rpcnd 10392 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  CC )
7221rpne0d 10395 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  =/=  0 )
7361, 71, 56, 72div32d 9559 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( R `  ( x  /  n
) )  x.  ( sum_ m  e.  { y  e.  NN  |  y 
||  n }  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) ) )  =  ( 2  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( R `  ( x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) )  /  ( log `  x ) ) ) )
7473oveq1d 5873 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( R `  ( x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) ) )  /  2
)  =  ( ( 2  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( R `  ( x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) )  /  ( log `  x ) ) )  /  2 ) )
7555, 21rerpdivcld 10417 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( R `  (
x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n }  ( (Λ `  m )  x.  (Λ `  ( n  /  m
) ) )  -  ( (Λ `  n )  x.  ( log `  n
) ) ) )  /  ( log `  x
) )  e.  RR )
7675recnd 8861 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( R `  (
x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n }  ( (Λ `  m )  x.  (Λ `  ( n  /  m
) ) )  -  ( (Λ `  n )  x.  ( log `  n
) ) ) )  /  ( log `  x
) )  e.  CC )
7776, 61, 64divcan3d 9541 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( R `  (
x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n }  ( (Λ `  m )  x.  (Λ `  ( n  /  m
) ) )  -  ( (Λ `  n )  x.  ( log `  n
) ) ) )  /  ( log `  x
) ) )  / 
2 )  =  (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( R `  (
x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n }  ( (Λ `  m )  x.  (Λ `  ( n  /  m
) ) )  -  ( (Λ `  n )  x.  ( log `  n
) ) ) )  /  ( log `  x
) ) )
7874, 77eqtrd 2315 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( R `  ( x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) ) )  /  2
)  =  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( R `  ( x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) )  /  ( log `  x ) ) )
7970, 78oveq12d 5876 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( 2  x.  ( ( R `  x )  x.  ( log `  x ) ) )  /  2 )  -  ( ( ( 2  /  ( log `  x ) )  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( R `  (
x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n }  ( (Λ `  m )  x.  (Λ `  ( n  /  m
) ) )  -  ( (Λ `  n )  x.  ( log `  n
) ) ) ) )  /  2 ) )  =  ( ( ( R `  x
)  x.  ( log `  x ) )  -  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( R `  ( x  /  n
) )  x.  ( sum_ m  e.  { y  e.  NN  |  y 
||  n }  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) )  /  ( log `  x ) ) ) )
8068, 79eqtrd 2315 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( 2  x.  ( ( R `  x )  x.  ( log `  x ) ) )  -  ( ( 2  /  ( log `  x ) )  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( R `  (
x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n }  ( (Λ `  m )  x.  (Λ `  ( n  /  m
) ) )  -  ( (Λ `  n )  x.  ( log `  n
) ) ) ) ) )  /  2
)  =  ( ( ( R `  x
)  x.  ( log `  x ) )  -  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( R `  ( x  /  n
) )  x.  ( sum_ m  e.  { y  e.  NN  |  y 
||  n }  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) )  /  ( log `  x ) ) ) )
8180oveq1d 5873 . . . . 5  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( 2  x.  ( ( R `
 x )  x.  ( log `  x
) ) )  -  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( R `  ( x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) ) ) )  / 
2 )  /  x
)  =  ( ( ( ( R `  x )  x.  ( log `  x ) )  -  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( R `  ( x  /  n
) )  x.  ( sum_ m  e.  { y  e.  NN  |  y 
||  n }  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) )  /  ( log `  x ) ) )  /  x ) )
8265, 67, 813eqtr3d 2323 . . . 4  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( 2  x.  ( ( R `
 x )  x.  ( log `  x
) ) )  -  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( R `  ( x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) ) ) )  /  x )  x.  (
1  /  2 ) )  =  ( ( ( ( R `  x )  x.  ( log `  x ) )  -  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( R `  ( x  /  n
) )  x.  ( sum_ m  e.  { y  e.  NN  |  y 
||  n }  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) )  /  ( log `  x ) ) )  /  x ) )
8382mpteq2dva 4106 . . 3  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( ( ( 2  x.  ( ( R `  x )  x.  ( log `  x
) ) )  -  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( R `  ( x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) ) ) )  /  x )  x.  (
1  /  2 ) ) )  =  ( x  e.  ( 1 (,)  +oo )  |->  ( ( ( ( R `  x )  x.  ( log `  x ) )  -  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( R `  ( x  /  n
) )  x.  ( sum_ m  e.  { y  e.  NN  |  y 
||  n }  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) )  /  ( log `  x ) ) )  /  x ) ) )
8422, 55remulcld 8863 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( R `  ( x  /  n
) )  x.  ( sum_ m  e.  { y  e.  NN  |  y 
||  n }  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) ) )  e.  RR )
8519, 84resubcld 9211 . . . . 5  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  x.  (
( R `  x
)  x.  ( log `  x ) ) )  -  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( R `  ( x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) ) ) )  e.  RR )
8685, 12rerpdivcld 10417 . . . 4  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( 2  x.  ( ( R `  x )  x.  ( log `  x ) ) )  -  ( ( 2  /  ( log `  x ) )  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( R `  (
x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n }  ( (Λ `  m )  x.  (Λ `  ( n  /  m
) ) )  -  ( (Λ `  n )  x.  ( log `  n
) ) ) ) ) )  /  x
)  e.  RR )
87 1re 8837 . . . . . 6  |-  1  e.  RR
8887a1i 10 . . . . 5  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  RR )
8988rehalfcld 9958 . . . 4  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  /  2 )  e.  RR )
9031recnd 8861 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  e.  CC )
9148recnd 8861 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e. 
{ y  e.  NN  |  y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  e.  CC )
9250recnd 8861 . . . . . . . . . . . . . . . . . 18  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n
)  e.  CC )
9351recnd 8861 . . . . . . . . . . . . . . . . . 18  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  n )  e.  CC )
9492, 93mulcld 8855 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  ( log `  n ) )  e.  CC )
9590, 91, 94subdid 9235 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( R `  ( x  /  n ) )  x.  ( sum_ m  e.  {
y  e.  NN  | 
y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) )  =  ( ( ( R `  (
x  /  n ) )  x.  sum_ m  e.  { y  e.  NN  |  y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) ) )  -  ( ( R `  ( x  /  n ) )  x.  ( (Λ `  n
)  x.  ( log `  n ) ) ) ) )
9690, 92, 93mul12d 9021 . . . . . . . . . . . . . . . . . 18  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( R `  ( x  /  n ) )  x.  ( (Λ `  n
)  x.  ( log `  n ) ) )  =  ( (Λ `  n
)  x.  ( ( R `  ( x  /  n ) )  x.  ( log `  n
) ) ) )
9792, 90, 93mulassd 8858 . . . . . . . . . . . . . . . . . 18  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  x.  ( R `  (
x  /  n ) ) )  x.  ( log `  n ) )  =  ( (Λ `  n
)  x.  ( ( R `  ( x  /  n ) )  x.  ( log `  n
) ) ) )
9896, 97eqtr4d 2318 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( R `  ( x  /  n ) )  x.  ( (Λ `  n
)  x.  ( log `  n ) ) )  =  ( ( (Λ `  n )  x.  ( R `  ( x  /  n ) ) )  x.  ( log `  n
) ) )
9998oveq2d 5874 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( R `  (
x  /  n ) )  x.  sum_ m  e.  { y  e.  NN  |  y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) ) )  -  ( ( R `  ( x  /  n ) )  x.  ( (Λ `  n
)  x.  ( log `  n ) ) ) )  =  ( ( ( R `  (
x  /  n ) )  x.  sum_ m  e.  { y  e.  NN  |  y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) ) )  -  ( ( (Λ `  n )  x.  ( R `  (
x  /  n ) ) )  x.  ( log `  n ) ) ) )
10095, 99eqtrd 2315 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( R `  ( x  /  n ) )  x.  ( sum_ m  e.  {
y  e.  NN  | 
y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) )  =  ( ( ( R `  (
x  /  n ) )  x.  sum_ m  e.  { y  e.  NN  |  y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) ) )  -  ( ( (Λ `  n )  x.  ( R `  (
x  /  n ) ) )  x.  ( log `  n ) ) ) )
101100sumeq2dv 12176 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( R `  ( x  /  n
) )  x.  ( sum_ m  e.  { y  e.  NN  |  y 
||  n }  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) )  =  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( R `
 ( x  /  n ) )  x. 
sum_ m  e.  { y  e.  NN  |  y 
||  n }  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) ) )  -  ( ( (Λ `  n )  x.  ( R `  (
x  /  n ) ) )  x.  ( log `  n ) ) ) )
10290, 91mulcld 8855 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( R `  ( x  /  n ) )  x. 
sum_ m  e.  { y  e.  NN  |  y 
||  n }  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) ) )  e.  CC )
10392, 90mulcld 8855 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  ( R `  ( x  /  n ) ) )  e.  CC )
104103, 93mulcld 8855 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  x.  ( R `  (
x  /  n ) ) )  x.  ( log `  n ) )  e.  CC )
10524, 102, 104fsumsub 12250 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( R `
 ( x  /  n ) )  x. 
sum_ m  e.  { y  e.  NN  |  y 
||  n }  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) ) )  -  ( ( (Λ `  n )  x.  ( R `  (
x  /  n ) ) )  x.  ( log `  n ) ) )  =  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( R `  ( x  /  n ) )  x.  sum_ m  e.  {
y  e.  NN  | 
y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) ) )  -  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) ) ) )
10647recnd 8861 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  {
y  e.  NN  | 
y  ||  n }
)  ->  ( (Λ `  m )  x.  (Λ `  ( n  /  m
) ) )  e.  CC )
10736, 90, 106fsummulc2 12246 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( R `  ( x  /  n ) )  x. 
sum_ m  e.  { y  e.  NN  |  y 
||  n }  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) ) )  =  sum_ m  e.  { y  e.  NN  |  y  ||  n } 
( ( R `  ( x  /  n
) )  x.  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) ) ) )
108107sumeq2dv 12176 . . . . . . . . . . . . . . . 16  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( R `  ( x  /  n
) )  x.  sum_ m  e.  { y  e.  NN  |  y  ||  n }  ( (Λ `  m )  x.  (Λ `  ( n  /  m
) ) ) )  =  sum_ n  e.  ( 1 ... ( |_
`  x ) )
sum_ m  e.  { y  e.  NN  |  y 
||  n }  (
( R `  (
x  /  n ) )  x.  ( (Λ `  m )  x.  (Λ `  ( n  /  m
) ) ) ) )
109 oveq2 5866 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  ( m  x.  k )  ->  (
x  /  n )  =  ( x  / 
( m  x.  k
) ) )
110109fveq2d 5529 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  ( m  x.  k )  ->  ( R `  ( x  /  n ) )  =  ( R `  (
x  /  ( m  x.  k ) ) ) )
111 oveq1 5865 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  ( m  x.  k )  ->  (
n  /  m )  =  ( ( m  x.  k )  /  m ) )
112111fveq2d 5529 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  ( m  x.  k )  ->  (Λ `  ( n  /  m
) )  =  (Λ `  ( ( m  x.  k )  /  m
) ) )
113112oveq2d 5874 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  ( m  x.  k )  ->  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  =  ( (Λ `  m
)  x.  (Λ `  (
( m  x.  k
)  /  m ) ) ) )
114110, 113oveq12d 5876 . . . . . . . . . . . . . . . . 17  |-  ( n  =  ( m  x.  k )  ->  (
( R `  (
x  /  n ) )  x.  ( (Λ `  m )  x.  (Λ `  ( n  /  m
) ) ) )  =  ( ( R `
 ( x  / 
( m  x.  k
) ) )  x.  ( (Λ `  m
)  x.  (Λ `  (
( m  x.  k
)  /  m ) ) ) ) )
11531adantrr 697 . . . . . . . . . . . . . . . . . . 19  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  m  e.  { y  e.  NN  |  y  ||  n } ) )  -> 
( R `  (
x  /  n ) )  e.  RR )
11641anasss 628 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  m  e.  { y  e.  NN  |  y  ||  n } ) )  -> 
(Λ `  m )  e.  RR )
11746anasss 628 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  m  e.  { y  e.  NN  |  y  ||  n } ) )  -> 
(Λ `  ( n  /  m ) )  e.  RR )
118116, 117remulcld 8863 . . . . . . . . . . . . . . . . . . 19  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  m  e.  { y  e.  NN  |  y  ||  n } ) )  -> 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  e.  RR )
119115, 118remulcld 8863 . . . . . . . . . . . . . . . . . 18  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  m  e.  { y  e.  NN  |  y  ||  n } ) )  -> 
( ( R `  ( x  /  n
) )  x.  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) ) )  e.  RR )
120119recnd 8861 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  m  e.  { y  e.  NN  |  y  ||  n } ) )  -> 
( ( R `  ( x  /  n
) )  x.  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) ) )  e.  CC )
121114, 4, 120dvdsflsumcom 20428 . . . . . . . . . . . . . . . 16  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) )
sum_ m  e.  { y  e.  NN  |  y 
||  n }  (
( R `  (
x  /  n ) )  x.  ( (Λ `  m )  x.  (Λ `  ( n  /  m
) ) ) )  =  sum_ m  e.  ( 1 ... ( |_
`  x ) )
sum_ k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) ( ( R `  ( x  /  (
m  x.  k ) ) )  x.  (
(Λ `  m )  x.  (Λ `  ( (
m  x.  k )  /  m ) ) ) ) )
12259ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  x  e.  CC )
123 elfznn 10819 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( m  e.  ( 1 ... ( |_ `  x
) )  ->  m  e.  NN )
124123adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  m  e.  NN )
125124nnrpd 10389 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  m  e.  RR+ )
126125adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  m  e.  RR+ )
127126rpcnd 10392 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  m  e.  CC )
128 elfznn 10819 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( k  e.  ( 1 ... ( |_ `  (
x  /  m ) ) )  ->  k  e.  NN )
129128adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  k  e.  NN )
130129nncnd 9762 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  k  e.  CC )
131126rpne0d 10395 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  m  =/=  0 )
132129nnne0d 9790 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  k  =/=  0 )
133122, 127, 130, 131, 132divdiv1d 9567 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( (
x  /  m )  /  k )  =  ( x  /  (
m  x.  k ) ) )
134133eqcomd 2288 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( x  /  ( m  x.  k ) )  =  ( ( x  /  m )  /  k
) )
135134fveq2d 5529 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( R `  ( x  /  (
m  x.  k ) ) )  =  ( R `  ( ( x  /  m )  /  k ) ) )
136130, 127, 131divcan3d 9541 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( (
m  x.  k )  /  m )  =  k )
137136fveq2d 5529 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  (Λ `  (
( m  x.  k
)  /  m ) )  =  (Λ `  k
) )
138137oveq2d 5874 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( (Λ `  m )  x.  (Λ `  ( ( m  x.  k )  /  m
) ) )  =  ( (Λ `  m
)  x.  (Λ `  k
) ) )
139135, 138oveq12d 5876 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( ( R `  ( x  /  ( m  x.  k ) ) )  x.  ( (Λ `  m
)  x.  (Λ `  (
( m  x.  k
)  /  m ) ) ) )  =  ( ( R `  ( ( x  /  m )  /  k
) )  x.  (
(Λ `  m )  x.  (Λ `  k )
) ) )
14012ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  x  e.  RR+ )
141140, 126rpdivcld 10407 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( x  /  m )  e.  RR+ )
142129nnrpd 10389 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  k  e.  RR+ )
143141, 142rpdivcld 10407 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( (
x  /  m )  /  k )  e.  RR+ )
14414ffvelrni 5664 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( x  /  m
)  /  k )  e.  RR+  ->  ( R `
 ( ( x  /  m )  / 
k ) )  e.  RR )
145143, 144syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( R `  ( ( x  /  m )  /  k
) )  e.  RR )
146145recnd 8861 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( R `  ( ( x  /  m )  /  k
) )  e.  CC )
147124, 40syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  m
)  e.  RR )
148147recnd 8861 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  m
)  e.  CC )
149148adantr 451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  (Λ `  m
)  e.  CC )
150 vmacl 20356 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  e.  NN  ->  (Λ `  k )  e.  RR )
151129, 150syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  (Λ `  k
)  e.  RR )
152151recnd 8861 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  (Λ `  k
)  e.  CC )
153149, 152mulcld 8855 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( (Λ `  m )  x.  (Λ `  k ) )  e.  CC )
154146, 153mulcomd 8856 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( ( R `  ( (
x  /  m )  /  k ) )  x.  ( (Λ `  m
)  x.  (Λ `  k
) ) )  =  ( ( (Λ `  m
)  x.  (Λ `  k
) )  x.  ( R `  ( (
x  /  m )  /  k ) ) ) )
155149, 152, 146mulassd 8858 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( (
(Λ `  m )  x.  (Λ `  k )
)  x.  ( R `
 ( ( x  /  m )  / 
k ) ) )  =  ( (Λ `  m
)  x.  ( (Λ `  k )  x.  ( R `  ( (
x  /  m )  /  k ) ) ) ) )
156139, 154, 1553eqtrd 2319 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( ( R `  ( x  /  ( m  x.  k ) ) )  x.  ( (Λ `  m
)  x.  (Λ `  (
( m  x.  k
)  /  m ) ) ) )  =  ( (Λ `  m
)  x.  ( (Λ `  k )  x.  ( R `  ( (
x  /  m )  /  k ) ) ) ) )
157156sumeq2dv 12176 . . . . . . . . . . . . . . . . . 18  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m ) ) ) ( ( R `  ( x  /  (
m  x.  k ) ) )  x.  (
(Λ `  m )  x.  (Λ `  ( (
m  x.  k )  /  m ) ) ) )  =  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m
) ) ) ( (Λ `  m )  x.  ( (Λ `  k
)  x.  ( R `
 ( ( x  /  m )  / 
k ) ) ) ) )
158 fzfid 11035 . . . . . . . . . . . . . . . . . . 19  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1 ... ( |_ `  ( x  /  m
) ) )  e. 
Fin )
159151, 145remulcld 8863 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( (Λ `  k )  x.  ( R `  ( (
x  /  m )  /  k ) ) )  e.  RR )
160159recnd 8861 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( (Λ `  k )  x.  ( R `  ( (
x  /  m )  /  k ) ) )  e.  CC )
161158, 148, 160fsummulc2 12246 . . . . . . . . . . . . . . . . . 18  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  m )  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m
) ) ) ( (Λ `  k )  x.  ( R `  (
( x  /  m
)  /  k ) ) ) )  = 
sum_ k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) ( (Λ `  m
)  x.  ( (Λ `  k )  x.  ( R `  ( (
x  /  m )  /  k ) ) ) ) )
162157, 161eqtr4d 2318 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m ) ) ) ( ( R `  ( x  /  (
m  x.  k ) ) )  x.  (
(Λ `  m )  x.  (Λ `  ( (
m  x.  k )  /  m ) ) ) )  =  ( (Λ `  m )  x.  sum_ k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) ( (Λ `  k
)  x.  ( R `
 ( ( x  /  m )  / 
k ) ) ) ) )
163162sumeq2dv 12176 . . . . . . . . . . . . . . . 16  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  x ) )
sum_ k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) ( ( R `  ( x  /  (
m  x.  k ) ) )  x.  (
(Λ `  m )  x.  (Λ `  ( (
m  x.  k )  /  m ) ) ) )  =  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  m )  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m
) ) ) ( (Λ `  k )  x.  ( R `  (
( x  /  m
)  /  k ) ) ) ) )
164108, 121, 1633eqtrd 2319 . . . . . . . . . . . . . . 15  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( R `  ( x  /  n
) )  x.  sum_ m  e.  { y  e.  NN  |  y  ||  n }  ( (Λ `  m )  x.  (Λ `  ( n  /  m
) ) ) )  =  sum_ m  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  m
)  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m ) ) ) ( (Λ `  k
)  x.  ( R `
 ( ( x  /  m )  / 
k ) ) ) ) )
165164oveq1d 5873 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( R `  (
x  /  n ) )  x.  sum_ m  e.  { y  e.  NN  |  y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) ) )  -  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) ) )  =  ( sum_ m  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  m
)  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m ) ) ) ( (Λ `  k
)  x.  ( R `
 ( ( x  /  m )  / 
k ) ) ) )  -  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) ) ) )
166101, 105, 1653eqtrd 2319 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( R `  ( x  /  n
) )  x.  ( sum_ m  e.  { y  e.  NN  |  y 
||  n }  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) )  =  ( sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  m )  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m
) ) ) ( (Λ `  k )  x.  ( R `  (
( x  /  m
)  /  k ) ) ) )  -  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) ) ) )
167166oveq2d 5874 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( R `  ( x  /  n
) )  x.  ( sum_ m  e.  { y  e.  NN  |  y 
||  n }  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) ) )  =  ( ( 2  /  ( log `  x ) )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  m
)  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m ) ) ) ( (Λ `  k
)  x.  ( R `
 ( ( x  /  m )  / 
k ) ) ) )  -  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) ) ) ) )
168158, 159fsumrecl 12207 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m ) ) ) ( (Λ `  k
)  x.  ( R `
 ( ( x  /  m )  / 
k ) ) )  e.  RR )
169147, 168remulcld 8863 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  m )  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m
) ) ) ( (Λ `  k )  x.  ( R `  (
( x  /  m
)  /  k ) ) ) )  e.  RR )
17024, 169fsumrecl 12207 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  m
)  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m ) ) ) ( (Λ `  k
)  x.  ( R `
 ( ( x  /  m )  / 
k ) ) ) )  e.  RR )
171170recnd 8861 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  m
)  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m ) ) ) ( (Λ `  k
)  x.  ( R `
 ( ( x  /  m )  / 
k ) ) ) )  e.  CC )
17250, 31remulcld 8863 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  ( R `  ( x  /  n ) ) )  e.  RR )
173172, 51remulcld 8863 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  x.  ( R `  (
x  /  n ) ) )  x.  ( log `  n ) )  e.  RR )
17424, 173fsumrecl 12207 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) )  e.  RR )
175174recnd 8861 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) )  e.  CC )
17623, 171, 175subdid 9235 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  m
)  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m ) ) ) ( (Λ `  k
)  x.  ( R `
 ( ( x  /  m )  / 
k ) ) ) )  -  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) ) ) )  =  ( ( ( 2  /  ( log `  x ) )  x. 
sum_ m  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  m )  x.  sum_ k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) ( (Λ `  k
)  x.  ( R `
 ( ( x  /  m )  / 
k ) ) ) ) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) ) ) ) )
177167, 176eqtrd 2315 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( R `  ( x  /  n
) )  x.  ( sum_ m  e.  { y  e.  NN  |  y 
||  n }  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) ) )  =  ( ( ( 2  / 
( log `  x
) )  x.  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  m )  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m
) ) ) ( (Λ `  k )  x.  ( R `  (
( x  /  m
)  /  k ) ) ) ) )  -  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  x.  ( R `  (
x  /  n ) ) )  x.  ( log `  n ) ) ) ) )
178177oveq2d 5874 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  x.  (
( R `  x
)  x.  ( log `  x ) ) )  -  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( R `  ( x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) ) ) )  =  ( ( 2  x.  ( ( R `  x )  x.  ( log `  x ) ) )  -  ( ( ( 2  /  ( log `  x ) )  x.  sum_ m  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  m
)  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m ) ) ) ( (Λ `  k
)  x.  ( R `
 ( ( x  /  m )  / 
k ) ) ) ) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) ) ) ) ) )
17923, 171mulcld 8855 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ m  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  m
)  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m ) ) ) ( (Λ `  k
)  x.  ( R `
 ( ( x  /  m )  / 
k ) ) ) ) )  e.  CC )
18022, 174remulcld 8863 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) ) )  e.  RR )
181180recnd 8861 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) ) )  e.  CC )
18220, 179, 181subsub3d 9187 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  x.  (
( R `  x
)  x.  ( log `  x ) ) )  -  ( ( ( 2  /  ( log `  x ) )  x. 
sum_ m  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  m )  x.  sum_ k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) ( (Λ `  k
)  x.  ( R `
 ( ( x  /  m )  / 
k ) ) ) ) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) ) ) ) )  =  ( ( ( 2  x.  (
( R `  x
)  x.  ( log `  x ) ) )  +  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  x.  ( R `  (
x  /  n ) ) )  x.  ( log `  n ) ) ) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ m  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  m
)  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m ) ) ) ( (Λ `  k
)  x.  ( R `
 ( ( x  /  m )  / 
k ) ) ) ) ) ) )
183178, 182eqtrd 2315 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  x.  (
( R `  x
)  x.  ( log `  x ) ) )  -  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( R `  ( x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) ) ) )  =  ( ( ( 2  x.  ( ( R `
 x )  x.  ( log `  x
) ) )  +  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  x.  ( R `  (
x  /  n ) ) )  x.  ( log `  n ) ) ) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ m  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  m
)  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m ) ) ) ( (Λ `  k
)  x.  ( R `
 ( ( x  /  m )  / 
k ) ) ) ) ) ) )
184692timesd 9954 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  ( ( R `  x )  x.  ( log `  x
) ) )  =  ( ( ( R `
 x )  x.  ( log `  x
) )  +  ( ( R `  x
)  x.  ( log `  x ) ) ) )
185184oveq1d 5873 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  x.  (
( R `  x
)  x.  ( log `  x ) ) )  +  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  x.  ( R `  (
x  /  n ) ) )  x.  ( log `  n ) ) ) )  =  ( ( ( ( R `
 x )  x.  ( log `  x
) )  +  ( ( R `  x
)  x.  ( log `  x ) ) )  +  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  x.  ( R `  (
x  /  n ) ) )  x.  ( log `  n ) ) ) ) )
18669, 181, 69add32d 9034 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( R `
 x )  x.  ( log `  x
) )  +  ( ( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) ) ) )  +  ( ( R `
 x )  x.  ( log `  x
) ) )  =  ( ( ( ( R `  x )  x.  ( log `  x
) )  +  ( ( R `  x
)  x.  ( log `  x ) ) )  +  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  x.  ( R `  (
x  /  n ) ) )  x.  ( log `  n ) ) ) ) )
187185, 186eqtr4d 2318 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  x.  (
( R `  x
)  x.  ( log `  x ) ) )  +  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  x.  ( R `  (
x  /  n ) ) )  x.  ( log `  n ) ) ) )  =  ( ( ( ( R `
 x )  x.  ( log `  x
) )  +  ( ( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) ) ) )  +  ( ( R `
 x )  x.  ( log `  x
) ) ) )
188187oveq1d 5873 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( 2  x.  ( ( R `  x )  x.  ( log `  x ) ) )  +  ( ( 2  /  ( log `  x ) )  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) ) ) )  -  ( ( 2  /  ( log `  x
) )  x.  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  m )  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m
) ) ) ( (Λ `  k )  x.  ( R `  (
( x  /  m
)  /  k ) ) ) ) ) )  =  ( ( ( ( ( R `
 x )  x.  ( log `  x
) )  +  ( ( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) ) ) )  +  ( ( R `
 x )  x.  ( log `  x
) ) )  -  ( ( 2  / 
( log `  x
) )  x.  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  m )  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m
) ) ) ( (Λ `  k )  x.  ( R `  (
( x  /  m
)  /  k ) ) ) ) ) ) )
18918, 180readdcld 8862 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( R `  x )  x.  ( log `  x ) )  +  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  x.  ( R `  (
x  /  n ) ) )  x.  ( log `  n ) ) ) )  e.  RR )
190189recnd 8861 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( R `  x )  x.  ( log `  x ) )  +  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  x.  ( R `  (
x  /  n ) ) )  x.  ( log `  n ) ) ) )  e.  CC )
191190, 69, 179addsubassd 9177 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( ( R `  x )  x.  ( log `  x
) )  +  ( ( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) ) ) )  +  ( ( R `
 x )  x.  ( log `  x
) ) )  -  ( ( 2  / 
( log `  x
) )  x.  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  m )  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m
) ) ) ( (Λ `  k )  x.  ( R `  (
( x  /  m
)  /  k ) ) ) ) ) )  =  ( ( ( ( R `  x )  x.  ( log `  x ) )  +  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  x.  ( R `  (
x  /  n ) ) )  x.  ( log `  n ) ) ) )  +  ( ( ( R `  x )  x.  ( log `  x ) )  -  ( ( 2  /  ( log `  x
) )  x.  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  m )  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m
) ) ) ( (Λ `  k )  x.  ( R `  (
( x  /  m
)  /  k ) ) ) ) ) ) ) )
192183, 188, 1913eqtrd 2319 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  x.  (
( R `  x
)  x.  ( log `  x ) ) )  -  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( R `  ( x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) ) ) )  =  ( ( ( ( R `  x )  x.  ( log `  x
) )  +  ( ( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) ) ) )  +  ( ( ( R `  x )  x.  ( log `  x
) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ m  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  m
)  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m ) ) ) ( (Λ `  k
)  x.  ( R `
 ( ( x  /  m )  / 
k ) ) ) ) ) ) ) )
193192oveq1d 5873 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( 2  x.  ( ( R `  x )  x.  ( log `  x ) ) )  -  ( ( 2  /  ( log `  x ) )  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( R `  (
x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n }  ( (Λ `  m )  x.  (Λ `  ( n  /  m
) ) )  -  ( (Λ `  n )  x.  ( log `  n
) ) ) ) ) )  /  x
)  =  ( ( ( ( ( R `
 x )  x.  ( log `  x
) )  +  ( ( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) ) ) )  +  ( ( ( R `  x )  x.  ( log `  x
) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ m  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  m
)  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m ) ) ) ( (Λ `  k
)  x.  ( R `
 ( ( x  /  m )  / 
k ) ) ) ) ) ) )  /  x ) )
19469, 179subcld 9157 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( R `  x )  x.  ( log `  x ) )  -  ( ( 2  /  ( log `  x
) )  x.  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  m )  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m
) ) ) ( (Λ `  k )  x.  ( R `  (
( x  /  m
)  /  k ) ) ) ) ) )  e.  CC )
195190, 194, 59, 62divdird 9574 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( ( R `  x )  x.  ( log `  x
) )  +  ( ( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) ) ) )  +  ( ( ( R `  x )  x.  ( log `  x
) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ m  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  m
)  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m ) ) ) ( (Λ `  k
)  x.  ( R `
 ( ( x  /  m )  / 
k ) ) ) ) ) ) )  /  x )  =  ( ( ( ( ( R `  x
)  x.  ( log `  x ) )  +  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  x.  ( R `  (
x  /  n ) ) )  x.  ( log `  n ) ) ) )  /  x
)  +  ( ( ( ( R `  x )  x.  ( log `  x ) )  -  ( ( 2  /  ( log `  x
) )  x.  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  m )  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m
) ) ) ( (Λ `  k )  x.  ( R `  (
( x  /  m
)  /  k ) ) ) ) ) )  /  x ) ) )
196193, 195eqtrd 2315 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( 2  x.  ( ( R `  x )  x.  ( log `  x ) ) )  -  ( ( 2  /  ( log `  x ) )  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( R `  (
x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n }  ( (Λ `  m )  x.  (Λ `  ( n  /  m
) ) )  -  ( (Λ `  n )  x.  ( log `  n
) ) ) ) ) )  /  x
)  =  ( ( ( ( ( R `
 x )  x.  ( log `  x
) )  +  ( ( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) ) ) )  /  x )  +  ( ( ( ( R `  x )  x.  ( log `  x
) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ m  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  m
)  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m ) ) ) ( (Λ `  k
)  x.  ( R `
 ( ( x  /  m )  / 
k ) ) ) ) ) )  /  x ) ) )
197196mpteq2dva 4106 . . . . 5  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( ( 2  x.  ( ( R `
 x )  x.  ( log `  x
) ) )  -  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( R `  ( x  /  n ) )  x.  ( sum_ m  e.  { y  e.  NN  |  y  ||  n } 
( (Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  -  ( (Λ `  n
)  x.  ( log `  n ) ) ) ) ) )  /  x ) )  =  ( x  e.  ( 1 (,)  +oo )  |->  ( ( ( ( ( R `  x
)  x.  ( log `  x ) )  +  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  x.  ( R `  (
x  /  n ) ) )  x.  ( log `  n ) ) ) )  /  x
)  +  ( ( ( ( R `  x )  x.  ( log `  x ) )  -  ( ( 2  /  ( log `  x
) )  x.  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  m )  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m
) ) ) ( (Λ `  k )  x.  ( R `  (
( x  /  m
)  /  k ) ) ) ) ) )  /  x ) ) ) )
198189, 12rerpdivcld 10417 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( R `
 x )  x.  ( log `  x
) )  +  ( ( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) ) ) )  /  x )  e.  RR )
19922, 170remulcld 8863 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ m  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  m
)  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m ) ) ) ( (Λ `  k
)  x.  ( R `
 ( ( x  /  m )  / 
k ) ) ) ) )  e.  RR )
20018, 199resubcld 9211 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( R `  x )  x.  ( log `  x ) )  -  ( ( 2  /  ( log `  x
) )  x.  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  m )  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m
) ) ) ( (Λ `  k )  x.  ( R `  (
( x  /  m
)  /  k ) ) ) ) ) )  e.  RR )
201200, 12rerpdivcld 10417 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( R `
 x )  x.  ( log `  x
) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ m  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  m
)  x.  sum_ k  e.  ( 1 ... ( |_ `  ( x  /  m ) ) ) ( (Λ `  k
)  x.  ( R `
 ( ( x  /  m )  / 
k ) ) ) ) ) )  /  x )  e.  RR )
20213selberg3r 20718 . . . . . . 7  |-  ( x  e.  ( 1 (,) 
+oo )  |->  ( ( ( ( R `  x )  x.  ( log `  x ) )  +  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  x.  ( R `  (
x  /  n ) ) )  x.  ( log `  n ) ) ) )  /  x
) )  e.  O
( 1 )
203202a1i 10 . . . . . 6  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( ( ( R `  x )  x.  ( log `  x
) )  +  ( ( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) ) ) )  /  x ) )  e.  O ( 1 ) )
20413selberg4r 20719 . . . . . . 7  |-  ( x  e.  ( 1 (,) 
+oo )  |->  ( ( ( ( R `  x )  x.  ( log `  x ) )  -  ( ( 2  /  ( log `  x
) )  x.  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  m )  x.  sum_ k  e.  ( 1