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

Theorem selberg34r 21270
Description: The sum of selberg3r 21268 and selberg4r 21269. (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 10074 . . . . . . . . . 10  |-  2  e.  RR
21a1i 11 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  2  e.  RR )
3 elioore 10951 . . . . . . . . . . . . 13  |-  ( x  e.  ( 1 (,) 
+oo )  ->  x  e.  RR )
43adantl 454 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  RR )
5 1rp 10621 . . . . . . . . . . . . 13  |-  1  e.  RR+
65a1i 11 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  RR+ )
76rpred 10653 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  RR )
8 eliooord 10975 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( 1 (,) 
+oo )  ->  (
1  <  x  /\  x  <  +oo ) )
98adantl 454 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  <  x  /\  x  <  +oo ) )
109simpld 447 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  <  x )
117, 4, 10ltled 9226 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  <_  x )
124, 6, 11rpgecld 10688 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  RR+ )
13 pntrval.r . . . . . . . . . . . . 13  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
1413pntrf 21262 . . . . . . . . . . . 12  |-  R : RR+
--> RR
1514ffvelrni 5872 . . . . . . . . . . 11  |-  ( x  e.  RR+  ->  ( R `
 x )  e.  RR )
1612, 15syl 16 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( R `  x )  e.  RR )
1712relogcld 20523 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  RR )
1816, 17remulcld 9121 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( R `  x
)  x.  ( log `  x ) )  e.  RR )
192, 18remulcld 9121 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  ( ( R `  x )  x.  ( log `  x
) ) )  e.  RR )
2019recnd 9119 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  ( ( R `  x )  x.  ( log `  x
) ) )  e.  CC )
214, 10rplogcld 20529 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  RR+ )
222, 21rerpdivcld 10680 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  /  ( log `  x ) )  e.  RR )
2322recnd 9119 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  /  ( log `  x ) )  e.  CC )
24 fzfid 11317 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1 ... ( |_ `  x ) )  e. 
Fin )
2512adantr 453 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR+ )
26 elfznn 11085 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
2726adantl 454 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
2827nnrpd 10652 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR+ )
2925, 28rpdivcld 10670 . . . . . . . . . . . 12  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
3014ffvelrni 5872 . . . . . . . . . . . 12  |-  ( ( x  /  n )  e.  RR+  ->  ( R `
 ( x  /  n ) )  e.  RR )
3129, 30syl 16 . . . . . . . . . . 11  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  e.  RR )
32 fzfid 11317 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1 ... n )  e. 
Fin )
33 sgmss 20894 . . . . . . . . . . . . . . 15  |-  ( n  e.  NN  ->  { y  e.  NN  |  y 
||  n }  C_  ( 1 ... n
) )
3427, 33syl 16 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  { y  e.  NN  |  y  ||  n }  C_  ( 1 ... n ) )
35 ssfi 7332 . . . . . . . . . . . . . 14  |-  ( ( ( 1 ... n
)  e.  Fin  /\  { y  e.  NN  | 
y  ||  n }  C_  ( 1 ... n
) )  ->  { y  e.  NN  |  y 
||  n }  e.  Fin )
3632, 34, 35syl2anc 644 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  { y  e.  NN  |  y  ||  n }  e.  Fin )
37 ssrab2 3430 . . . . . . . . . . . . . . . 16  |-  { y  e.  NN  |  y 
||  n }  C_  NN
38 simpr 449 . . . . . . . . . . . . . . . 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 3348 . . . . . . . . . . . . . . 15  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  {
y  e.  NN  | 
y  ||  n }
)  ->  m  e.  NN )
40 vmacl 20906 . . . . . . . . . . . . . . 15  |-  ( m  e.  NN  ->  (Λ `  m )  e.  RR )
4139, 40syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  {
y  e.  NN  | 
y  ||  n }
)  ->  (Λ `  m
)  e.  RR )
42 dvdsdivcl 20971 . . . . . . . . . . . . . . . . 17  |-  ( ( n  e.  NN  /\  m  e.  { y  e.  NN  |  y  ||  n } )  ->  (
n  /  m )  e.  { y  e.  NN  |  y  ||  n } )
4327, 42sylan 459 . . . . . . . . . . . . . . . 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 3348 . . . . . . . . . . . . . . 15  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  {
y  e.  NN  | 
y  ||  n }
)  ->  ( n  /  m )  e.  NN )
45 vmacl 20906 . . . . . . . . . . . . . . 15  |-  ( ( n  /  m )  e.  NN  ->  (Λ `  ( n  /  m
) )  e.  RR )
4644, 45syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  {
y  e.  NN  | 
y  ||  n }
)  ->  (Λ `  (
n  /  m ) )  e.  RR )
4741, 46remulcld 9121 . . . . . . . . . . . . 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 12533 . . . . . . . . . . . 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 20906 . . . . . . . . . . . . . 14  |-  ( n  e.  NN  ->  (Λ `  n )  e.  RR )
5027, 49syl 16 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n
)  e.  RR )
5128relogcld 20523 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  n )  e.  RR )
5250, 51remulcld 9121 . . . . . . . . . . . 12  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  ( log `  n ) )  e.  RR )
5348, 52resubcld 9470 . . . . . . . . . . 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 9121 . . . . . . . . . 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 12533 . . . . . . . . 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 9119 . . . . . . . 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 9113 . . . . . . 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 9416 . . . . . 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 9119 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  CC )
60 2cn 10075 . . . . . . 7  |-  2  e.  CC
6160a1i 11 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  2  e.  CC )
6212rpne0d 10658 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  =/=  0 )
63 2ne0 10088 . . . . . . 7  |-  2  =/=  0
6463a1i 11 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  2  =/=  0 )
6558, 59, 61, 62, 64divdiv32d 9820 . . . . 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 9795 . . . . . 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 9798 . . . . 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 9834 . . . . . . 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 9119 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( R `  x
)  x.  ( log `  x ) )  e.  CC )
7069, 61, 64divcan3d 9800 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  x.  (
( R `  x
)  x.  ( log `  x ) ) )  /  2 )  =  ( ( R `  x )  x.  ( log `  x ) ) )
7121rpcnd 10655 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  CC )
7221rpne0d 10658 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  =/=  0 )
7361, 71, 56, 72div32d 9818 . . . . . . . . . 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 6099 . . . . . . . . 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 10680 . . . . . . . . . . 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 9119 . . . . . . . . . 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 9800 . . . . . . . . 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 2470 . . . . . . . 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 6102 . . . . . . 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 2470 . . . . . 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 6099 . . . . 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 2478 . . . 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 4298 . . 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 9121 . . . . . 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 9470 . . . . 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 10680 . . . 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 9095 . . . . . 6  |-  1  e.  RR
8887a1i 11 . . . . 5  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  RR )
8988rehalfcld 10219 . . . 4  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  /  2 )  e.  RR )
9031recnd 9119 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  e.  CC )
9148recnd 9119 . . . . . . . . . . . . . . . . 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 9119 . . . . . . . . . . . . . . . . . 18  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n
)  e.  CC )
9351recnd 9119 . . . . . . . . . . . . . . . . . 18  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  n )  e.  CC )
9492, 93mulcld 9113 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  ( log `  n ) )  e.  CC )
9590, 91, 94subdid 9494 . . . . . . . . . . . . . . . 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 9280 . . . . . . . . . . . . . . . . . 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 9116 . . . . . . . . . . . . . . . . . 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 2473 . . . . . . . . . . . . . . . . 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 6100 . . . . . . . . . . . . . . . 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 2470 . . . . . . . . . . . . . . 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 12502 . . . . . . . . . . . . . 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 9113 . . . . . . . . . . . . . . 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 9113 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  ( R `  ( x  /  n ) ) )  e.  CC )
104103, 93mulcld 9113 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  x.  ( R `  (
x  /  n ) ) )  x.  ( log `  n ) )  e.  CC )
10524, 102, 104fsumsub 12576 . . . . . . . . . . . . . 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 9119 . . . . . . . . . . . . . . . . . 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 12572 . . . . . . . . . . . . . . . . 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 12502 . . . . . . . . . . . . . . . 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 6092 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  ( m  x.  k )  ->  (
x  /  n )  =  ( x  / 
( m  x.  k
) ) )
110109fveq2d 5735 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  ( m  x.  k )  ->  ( R `  ( x  /  n ) )  =  ( R `  (
x  /  ( m  x.  k ) ) ) )
111 oveq1 6091 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  ( m  x.  k )  ->  (
n  /  m )  =  ( ( m  x.  k )  /  m ) )
112111fveq2d 5735 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  ( m  x.  k )  ->  (Λ `  ( n  /  m
) )  =  (Λ `  ( ( m  x.  k )  /  m
) ) )
113112oveq2d 6100 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  ( m  x.  k )  ->  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  =  ( (Λ `  m
)  x.  (Λ `  (
( m  x.  k
)  /  m ) ) ) )
114110, 113oveq12d 6102 . . . . . . . . . . . . . . . . 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 699 . . . . . . . . . . . . . . . . . . 19  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  m  e.  { y  e.  NN  |  y  ||  n } ) )  -> 
( R `  (
x  /  n ) )  e.  RR )
11641anasss 630 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  m  e.  { y  e.  NN  |  y  ||  n } ) )  -> 
(Λ `  m )  e.  RR )
11746anasss 630 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  m  e.  { y  e.  NN  |  y  ||  n } ) )  -> 
(Λ `  ( n  /  m ) )  e.  RR )
118116, 117remulcld 9121 . . . . . . . . . . . . . . . . . . 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 9121 . . . . . . . . . . . . . . . . . 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 9119 . . . . . . . . . . . . . . . . 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 20978 . . . . . . . . . . . . . . . 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 708 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  x  e.  CC )
123 elfznn 11085 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( m  e.  ( 1 ... ( |_ `  x
) )  ->  m  e.  NN )
124123adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  m  e.  NN )
125124nnrpd 10652 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  m  e.  RR+ )
126125adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  m  e.  RR+ )
127126rpcnd 10655 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  m  e.  CC )
128 elfznn 11085 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( k  e.  ( 1 ... ( |_ `  (
x  /  m ) ) )  ->  k  e.  NN )
129128adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  k  e.  NN )
130129nncnd 10021 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  k  e.  CC )
131126rpne0d 10658 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  m  =/=  0 )
132129nnne0d 10049 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  k  =/=  0 )
133122, 127, 130, 131, 132divdiv1d 9826 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( (
x  /  m )  /  k )  =  ( x  /  (
m  x.  k ) ) )
134133eqcomd 2443 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( x  /  ( m  x.  k ) )  =  ( ( x  /  m )  /  k
) )
135134fveq2d 5735 . . . . . . . . . . . . . . . . . . . . 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 9800 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( (
m  x.  k )  /  m )  =  k )
137136fveq2d 5735 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  (Λ `  (
( m  x.  k
)  /  m ) )  =  (Λ `  k
) )
138137oveq2d 6100 . . . . . . . . . . . . . . . . . . . . 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 6102 . . . . . . . . . . . . . . . . . . . 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 708 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  x  e.  RR+ )
141140, 126rpdivcld 10670 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( x  /  m )  e.  RR+ )
142129nnrpd 10652 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  k  e.  RR+ )
143141, 142rpdivcld 10670 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( (
x  /  m )  /  k )  e.  RR+ )
14414ffvelrni 5872 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( x  /  m
)  /  k )  e.  RR+  ->  ( R `
 ( ( x  /  m )  / 
k ) )  e.  RR )
145143, 144syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( R `  ( ( x  /  m )  /  k
) )  e.  RR )
146145recnd 9119 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( R `  ( ( x  /  m )  /  k
) )  e.  CC )
147124, 40syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  m
)  e.  RR )
148147recnd 9119 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  m
)  e.  CC )
149148adantr 453 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  (Λ `  m
)  e.  CC )
150 vmacl 20906 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  e.  NN  ->  (Λ `  k )  e.  RR )
151129, 150syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  (Λ `  k
)  e.  RR )
152151recnd 9119 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  (Λ `  k
)  e.  CC )
153149, 152mulcld 9113 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( (Λ `  m )  x.  (Λ `  k ) )  e.  CC )
154146, 153mulcomd 9114 . . . . . . . . . . . . . . . . . . . 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 9116 . . . . . . . . . . . . . . . . . . . 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 2474 . . . . . . . . . . . . . . . . . . 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 12502 . . . . . . . . . . . . . . . . . 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 11317 . . . . . . . . . . . . . . . . . . 19  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1 ... ( |_ `  ( x  /  m
) ) )  e. 
Fin )
159151, 145remulcld 9121 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( (Λ `  k )  x.  ( R `  ( (
x  /  m )  /  k ) ) )  e.  RR )
160159recnd 9119 . . . . . . . . . . . . . . . . . . 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 12572 . . . . . . . . . . . . . . . . . 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 2473 . . . . . . . . . . . . . . . . 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 12502 . . . . . . . . . . . . . . . 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 2474 . . . . . . . . . . . . . . 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 6099 . . . . . . . . . . . . . 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 2474 . . . . . . . . . . . . 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 6100 . . . . . . . . . . . 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 12533 . . . . . . . . . . . . . . . 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 9121 . . . . . . . . . . . . . . 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 12533 . . . . . . . . . . . . . 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 9119 . . . . . . . . . . . . 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 9121 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  ( R `  ( x  /  n ) ) )  e.  RR )
173172, 51remulcld 9121 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  x.  ( R `  (
x  /  n ) ) )  x.  ( log `  n ) )  e.  RR )
17424, 173fsumrecl 12533 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) )  e.  RR )
175174recnd 9119 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) )  e.  CC )
17623, 171, 175subdid 9494 . . . . . . . . . . . 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 2470 . . . . . . . . . . 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 6100 . . . . . . . . . 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 9113 . . . . . . . . . . 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 9121 . . . . . . . . . . . 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 9119 . . . . . . . . . . 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 9446 . . . . . . . . . 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 2470 . . . . . . . . 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 10215 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  ( ( R `  x )  x.  ( log `  x
) ) )  =  ( ( ( R `
 x )  x.  ( log `  x
) )  +  ( ( R `  x
)  x.  ( log `  x ) ) ) )
185184oveq1d 6099 . . . . . . . . . . 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 9293 . . . . . . . . . . 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 2473 . . . . . . . . . 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 6099 . . . . . . . . 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 9120 . . . . . . . . . . 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 9119 . . . . . . . . . 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 9436 . . . . . . . . 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 2474 . . . . . . . 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 6099 . . . . . . 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 9416 . . . . . . . 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 9833 . . . . . . 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 2470 . . . . . 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 4298 . . . . 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 10680 . . . . . 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 9121 . . . . . . . 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 9470 . . . . . . 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 10680 . . . . . 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 21268 . . . . . . 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 11 . . . . . 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 21269 . . . . . . 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 ... ( |_ `  ( x  /  m
) ) ) ( (Λ `  k )  x.  ( R `  (
( x  /  m
)  /  k ) ) ) ) ) )  /  x ) )  e.  O ( 1 )
205204a1i 11 . . . . . 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 `
 (