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

Theorem selberg34r 20826
Description: The sum of selberg3r 20824 and selberg4r 20825. (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 9902 . . . . . . . . . 10  |-  2  e.  RR
21a1i 10 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  2  e.  RR )
3 elioore 10775 . . . . . . . . . . . . 13  |-  ( x  e.  ( 1 (,) 
+oo )  ->  x  e.  RR )
43adantl 452 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  RR )
5 1rp 10447 . . . . . . . . . . . . 13  |-  1  e.  RR+
65a1i 10 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  RR+ )
76rpred 10479 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  RR )
8 eliooord 10799 . . . . . . . . . . . . . . 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 9054 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  <_  x )
124, 6, 11rpgecld 10514 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  RR+ )
13 pntrval.r . . . . . . . . . . . . 13  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
1413pntrf 20818 . . . . . . . . . . . 12  |-  R : RR+
--> RR
1514ffvelrni 5744 . . . . . . . . . . 11  |-  ( x  e.  RR+  ->  ( R `
 x )  e.  RR )
1612, 15syl 15 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( R `  x )  e.  RR )
1712relogcld 20079 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  RR )
1816, 17remulcld 8950 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( R `  x
)  x.  ( log `  x ) )  e.  RR )
192, 18remulcld 8950 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  ( ( R `  x )  x.  ( log `  x
) ) )  e.  RR )
2019recnd 8948 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  ( ( R `  x )  x.  ( log `  x
) ) )  e.  CC )
214, 10rplogcld 20085 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  RR+ )
222, 21rerpdivcld 10506 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  /  ( log `  x ) )  e.  RR )
2322recnd 8948 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  /  ( log `  x ) )  e.  CC )
24 fzfid 11124 . . . . . . . . . 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 10908 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
2726adantl 452 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
2827nnrpd 10478 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR+ )
2925, 28rpdivcld 10496 . . . . . . . . . . . 12  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
3014ffvelrni 5744 . . . . . . . . . . . 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 11124 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1 ... n )  e. 
Fin )
33 sgmss 20450 . . . . . . . . . . . . . . 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 7168 . . . . . . . . . . . . . 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 3334 . . . . . . . . . . . . . . . 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 3254 . . . . . . . . . . . . . . 15  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  {
y  e.  NN  | 
y  ||  n }
)  ->  m  e.  NN )
40 vmacl 20462 . . . . . . . . . . . . . . 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 20527 . . . . . . . . . . . . . . . . 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 3254 . . . . . . . . . . . . . . 15  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  {
y  e.  NN  | 
y  ||  n }
)  ->  ( n  /  m )  e.  NN )
45 vmacl 20462 . . . . . . . . . . . . . . 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 8950 . . . . . . . . . . . . 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 12298 . . . . . . . . . . . 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 20462 . . . . . . . . . . . . . 14  |-  ( n  e.  NN  ->  (Λ `  n )  e.  RR )
5027, 49syl 15 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n
)  e.  RR )
5128relogcld 20079 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  n )  e.  RR )
5250, 51remulcld 8950 . . . . . . . . . . . 12  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  ( log `  n ) )  e.  RR )
5348, 52resubcld 9298 . . . . . . . . . . 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 8950 . . . . . . . . . 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 12298 . . . . . . . . 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 8948 . . . . . . . 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 8942 . . . . . . 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 9244 . . . . . 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 8948 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  CC )
60 2cn 9903 . . . . . . 7  |-  2  e.  CC
6160a1i 10 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  2  e.  CC )
6212rpne0d 10484 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  =/=  0 )
63 2ne0 9916 . . . . . . 7  |-  2  =/=  0
6463a1i 10 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  2  =/=  0 )
6558, 59, 61, 62, 64divdiv32d 9648 . . . . 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 9623 . . . . . 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 9626 . . . . 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 9662 . . . . . . 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 8948 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( R `  x
)  x.  ( log `  x ) )  e.  CC )
7069, 61, 64divcan3d 9628 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  x.  (
( R `  x
)  x.  ( log `  x ) ) )  /  2 )  =  ( ( R `  x )  x.  ( log `  x ) ) )
7121rpcnd 10481 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  CC )
7221rpne0d 10484 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  =/=  0 )
7361, 71, 56, 72div32d 9646 . . . . . . . . . 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 5957 . . . . . . . . 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 10506 . . . . . . . . . . 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 8948 . . . . . . . . . 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 9628 . . . . . . . . 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 2390 . . . . . . . 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 5960 . . . . . . 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 2390 . . . . . 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 5957 . . . . 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 2398 . . . 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 4185 . . 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 8950 . . . . . 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 9298 . . . . 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 10506 . . . 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 8924 . . . . . 6  |-  1  e.  RR
8887a1i 10 . . . . 5  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  RR )
8988rehalfcld 10047 . . . 4  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  /  2 )  e.  RR )
9031recnd 8948 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  e.  CC )
9148recnd 8948 . . . . . . . . . . . . . . . . 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 8948 . . . . . . . . . . . . . . . . . 18  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n
)  e.  CC )
9351recnd 8948 . . . . . . . . . . . . . . . . . 18  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  n )  e.  CC )
9492, 93mulcld 8942 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  ( log `  n ) )  e.  CC )
9590, 91, 94subdid 9322 . . . . . . . . . . . . . . . 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 9108 . . . . . . . . . . . . . . . . . 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 8945 . . . . . . . . . . . . . . . . . 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 2393 . . . . . . . . . . . . . . . . 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 5958 . . . . . . . . . . . . . . . 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 2390 . . . . . . . . . . . . . . 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 12267 . . . . . . . . . . . . . 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 8942 . . . . . . . . . . . . . . 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 8942 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  ( R `  ( x  /  n ) ) )  e.  CC )
104103, 93mulcld 8942 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  x.  ( R `  (
x  /  n ) ) )  x.  ( log `  n ) )  e.  CC )
10524, 102, 104fsumsub 12341 . . . . . . . . . . . . . 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 8948 . . . . . . . . . . . . . . . . . 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 12337 . . . . . . . . . . . . . . . . 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 12267 . . . . . . . . . . . . . . . 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 5950 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  ( m  x.  k )  ->  (
x  /  n )  =  ( x  / 
( m  x.  k
) ) )
110109fveq2d 5609 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  ( m  x.  k )  ->  ( R `  ( x  /  n ) )  =  ( R `  (
x  /  ( m  x.  k ) ) ) )
111 oveq1 5949 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  ( m  x.  k )  ->  (
n  /  m )  =  ( ( m  x.  k )  /  m ) )
112111fveq2d 5609 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  ( m  x.  k )  ->  (Λ `  ( n  /  m
) )  =  (Λ `  ( ( m  x.  k )  /  m
) ) )
113112oveq2d 5958 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  ( m  x.  k )  ->  (
(Λ `  m )  x.  (Λ `  ( n  /  m ) ) )  =  ( (Λ `  m
)  x.  (Λ `  (
( m  x.  k
)  /  m ) ) ) )
114110, 113oveq12d 5960 . . . . . . . . . . . . . . . . 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 8950 . . . . . . . . . . . . . . . . . . 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 8950 . . . . . . . . . . . . . . . . . 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 8948 . . . . . . . . . . . . . . . . 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 20534 . . . . . . . . . . . . . . . 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 10908 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( m  e.  ( 1 ... ( |_ `  x
) )  ->  m  e.  NN )
124123adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  m  e.  NN )
125124nnrpd 10478 . . . . . . . . . . . . . . . . . . . . . . . . . 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 10481 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  m  e.  CC )
128 elfznn 10908 . . . . . . . . . . . . . . . . . . . . . . . . . 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 9849 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  k  e.  CC )
131126rpne0d 10484 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  m  =/=  0 )
132129nnne0d 9877 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  k  =/=  0 )
133122, 127, 130, 131, 132divdiv1d 9654 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( (
x  /  m )  /  k )  =  ( x  /  (
m  x.  k ) ) )
134133eqcomd 2363 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( x  /  ( m  x.  k ) )  =  ( ( x  /  m )  /  k
) )
135134fveq2d 5609 . . . . . . . . . . . . . . . . . . . . 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 9628 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( (
m  x.  k )  /  m )  =  k )
137136fveq2d 5609 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  (Λ `  (
( m  x.  k
)  /  m ) )  =  (Λ `  k
) )
138137oveq2d 5958 . . . . . . . . . . . . . . . . . . . . 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 5960 . . . . . . . . . . . . . . . . . . . 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 10496 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( x  /  m )  e.  RR+ )
142129nnrpd 10478 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  k  e.  RR+ )
143141, 142rpdivcld 10496 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( (
x  /  m )  /  k )  e.  RR+ )
14414ffvelrni 5744 . . . . . . . . . . . . . . . . . . . . . . 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 8948 . . . . . . . . . . . . . . . . . . . . 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 8948 . . . . . . . . . . . . . . . . . . . . . . 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 20462 . . . . . . . . . . . . . . . . . . . . . . . 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 8948 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  (Λ `  k
)  e.  CC )
153149, 152mulcld 8942 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( (Λ `  m )  x.  (Λ `  k ) )  e.  CC )
154146, 153mulcomd 8943 . . . . . . . . . . . . . . . . . . . 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 8945 . . . . . . . . . . . . . . . . . . . 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 2394 . . . . . . . . . . . . . . . . . . 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 12267 . . . . . . . . . . . . . . . . . 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 11124 . . . . . . . . . . . . . . . . . . 19  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1 ... ( |_ `  ( x  /  m
) ) )  e. 
Fin )
159151, 145remulcld 8950 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  k  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  ( (Λ `  k )  x.  ( R `  ( (
x  /  m )  /  k ) ) )  e.  RR )
160159recnd 8948 . . . . . . . . . . . . . . . . . . 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 12337 . . . . . . . . . . . . . . . . . 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 2393 . . . . . . . . . . . . . . . . 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 12267 . . . . . . . . . . . . . . . 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 2394 . . . . . . . . . . . . . . 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 5957 . . . . . . . . . . . . . 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 2394 . . . . . . . . . . . . 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 5958 . . . . . . . . . . . 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 12298 . . . . . . . . . . . . . . . 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 8950 . . . . . . . . . . . . . . 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 12298 . . . . . . . . . . . . . 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 8948 . . . . . . . . . . . . 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 8950 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  ( R `  ( x  /  n ) ) )  e.  RR )
173172, 51remulcld 8950 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  x.  ( R `  (
x  /  n ) ) )  x.  ( log `  n ) )  e.  RR )
17424, 173fsumrecl 12298 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) )  e.  RR )
175174recnd 8948 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  ( R `
 ( x  /  n ) ) )  x.  ( log `  n
) )  e.  CC )
17623, 171, 175subdid 9322 . . . . . . . . . . . 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 2390 . . . . . . . . . . 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 5958 . . . . . . . . . 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 8942 . . . . . . . . . . 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 8950 . . . . . . . . . . . 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 8948 . . . . . . . . . . 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 9274 . . . . . . . . . 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 2390 . . . . . . . . 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 10043 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  ( ( R `  x )  x.  ( log `  x
) ) )  =  ( ( ( R `
 x )  x.  ( log `  x
) )  +  ( ( R `  x
)  x.  ( log `  x ) ) ) )
185184oveq1d 5957 . . . . . . . . . . 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 9121 . . . . . . . . . . 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 2393 . . . . . . . . . 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 5957 . . . . . . . . 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 8949 . . . . . . . . . . 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 8948 . . . . . . . . . 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 9264 . . . . . . . . 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 2394 . . . . . . . 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 5957 . . . . . . 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 9244 . . . . . . . 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 9661 . . . . . . 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 2390 . . . . . 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 4185 . . . . 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 10506 . . . . . 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 8950 . . . . . . . 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 9298 . . . . . . 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 10506 . . . . . 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 20824 . . . . . . 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 20825 . . . . . . 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 10 . . . . . 6  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( ( ( R `  x )  x.  ( log `  x
) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ m  e.  (