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

Theorem selberg4 21247
Description: The Selberg symmetry formula for products of three primes, instead of two. The sum here can also be written in the symmetric form  sum_ i j k  <_  x , Λ ( i )Λ ( j )Λ ( k ); we eliminate one of the nested sums by using the definition of ψ ( x )  =  sum_ k  <_  x , Λ ( k ). This statement can thus equivalently be written ψ
( x ) log
^ 2 ( x )  =  2 sum_ i
j k  <_  x , Λ ( i )Λ (
j )Λ ( k )  +  O ( x log x ). Equation 10.4.23 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)
Assertion
Ref Expression
selberg4  |-  ( x  e.  ( 1 (,) 
+oo )  |->  ( ( ( (ψ `  x
)  x.  ( log `  x ) )  -  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) )  /  x
) )  e.  O
( 1 )
Distinct variable group:    m, n, x

Proof of Theorem selberg4
Dummy variables  i 
c  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 2re 10061 . . . . . . . . . . . . 13  |-  2  e.  RR
21a1i 11 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  2  e.  RR )
3 elioore 10938 . . . . . . . . . . . . . 14  |-  ( x  e.  ( 1 (,) 
+oo )  ->  x  e.  RR )
43adantl 453 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  RR )
5 eliooord 10962 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( 1 (,) 
+oo )  ->  (
1  <  x  /\  x  <  +oo ) )
65adantl 453 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  <  x  /\  x  <  +oo ) )
76simpld 446 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  <  x )
84, 7rplogcld 20516 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  RR+ )
92, 8rerpdivcld 10667 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  /  ( log `  x ) )  e.  RR )
10 fzfid 11304 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1 ... ( |_ `  x ) )  e. 
Fin )
11 elfznn 11072 . . . . . . . . . . . . . . . 16  |-  ( m  e.  ( 1 ... ( |_ `  x
) )  ->  m  e.  NN )
1211adantl 453 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  m  e.  NN )
13 vmacl 20893 . . . . . . . . . . . . . . 15  |-  ( m  e.  NN  ->  (Λ `  m )  e.  RR )
1412, 13syl 16 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  m
)  e.  RR )
154adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR )
1615, 12nndivred 10040 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  m )  e.  RR )
17 chpcl 20899 . . . . . . . . . . . . . . 15  |-  ( ( x  /  m )  e.  RR  ->  (ψ `  ( x  /  m
) )  e.  RR )
1816, 17syl 16 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  m ) )  e.  RR )
1914, 18remulcld 9108 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  m )  x.  (ψ `  ( x  /  m
) ) )  e.  RR )
2012nnrpd 10639 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  m  e.  RR+ )
2120relogcld 20510 . . . . . . . . . . . . 13  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  m )  e.  RR )
2219, 21remulcld 9108 . . . . . . . . . . . 12  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  m )  x.  (ψ `  ( x  /  m ) ) )  x.  ( log `  m
) )  e.  RR )
2310, 22fsumrecl 12520 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  m
)  x.  (ψ `  ( x  /  m
) ) )  x.  ( log `  m
) )  e.  RR )
249, 23remulcld 9108 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ m  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  m
)  x.  (ψ `  ( x  /  m
) ) )  x.  ( log `  m
) ) )  e.  RR )
2510, 19fsumrecl 12520 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  m
)  x.  (ψ `  ( x  /  m
) ) )  e.  RR )
2624, 25resubcld 9457 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( 2  / 
( log `  x
) )  x.  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) )  x.  ( log `  m
) ) )  -  sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) ) )  e.  RR )
27 1rp 10608 . . . . . . . . . . 11  |-  1  e.  RR+
2827a1i 11 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  RR+ )
2928rpred 10640 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  RR )
3029, 4, 7ltled 9213 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  <_  x )
314, 28, 30rpgecld 10675 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  RR+ )
3226, 31rerpdivcld 10667 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( 2  /  ( log `  x
) )  x.  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) )  x.  ( log `  m
) ) )  -  sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) ) )  /  x )  e.  RR )
3332recnd 9106 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( 2  /  ( log `  x
) )  x.  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) )  x.  ( log `  m
) ) )  -  sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) ) )  /  x )  e.  CC )
34 chpcl 20899 . . . . . . . . . . . 12  |-  ( x  e.  RR  ->  (ψ `  x )  e.  RR )
354, 34syl 16 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (ψ `  x )  e.  RR )
3631relogcld 20510 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  RR )
3735, 36remulcld 9108 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  x )  x.  ( log `  x
) )  e.  RR )
3837, 25readdcld 9107 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( (ψ `  x
)  x.  ( log `  x ) )  + 
sum_ m  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) ) )  e.  RR )
3938, 31rerpdivcld 10667 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( (ψ `  x )  x.  ( log `  x ) )  +  sum_ m  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  m
)  x.  (ψ `  ( x  /  m
) ) ) )  /  x )  e.  RR )
4039recnd 9106 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( (ψ `  x )  x.  ( log `  x ) )  +  sum_ m  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  m
)  x.  (ψ `  ( x  /  m
) ) ) )  /  x )  e.  CC )
412, 36remulcld 9108 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  ( log `  x ) )  e.  RR )
4241recnd 9106 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  ( log `  x ) )  e.  CC )
4333, 40, 42addsubassd 9423 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( ( ( 2  /  ( log `  x ) )  x.  sum_ m  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  m
)  x.  (ψ `  ( x  /  m
) ) )  x.  ( log `  m
) ) )  -  sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) ) )  /  x )  +  ( ( ( (ψ `  x )  x.  ( log `  x
) )  +  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m
) ) ) )  /  x ) )  -  ( 2  x.  ( log `  x
) ) )  =  ( ( ( ( ( 2  /  ( log `  x ) )  x.  sum_ m  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  m
)  x.  (ψ `  ( x  /  m
) ) )  x.  ( log `  m
) ) )  -  sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) ) )  /  x )  +  ( ( ( ( (ψ `  x
)  x.  ( log `  x ) )  + 
sum_ m  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) ) )  /  x )  -  ( 2  x.  ( log `  x
) ) ) ) )
4426recnd 9106 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( 2  / 
( log `  x
) )  x.  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) )  x.  ( log `  m
) ) )  -  sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) ) )  e.  CC )
4538recnd 9106 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( (ψ `  x
)  x.  ( log `  x ) )  + 
sum_ m  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) ) )  e.  CC )
464recnd 9106 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  CC )
4731rpne0d 10645 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  =/=  0 )
4844, 45, 46, 47divdird 9820 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( ( 2  /  ( log `  x ) )  x. 
sum_ m  e.  (
1 ... ( |_ `  x ) ) ( ( (Λ `  m
)  x.  (ψ `  ( x  /  m
) ) )  x.  ( log `  m
) ) )  -  sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) ) )  +  ( ( (ψ `  x )  x.  ( log `  x
) )  +  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m
) ) ) ) )  /  x )  =  ( ( ( ( ( 2  / 
( log `  x
) )  x.  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) )  x.  ( log `  m
) ) )  -  sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) ) )  /  x )  +  ( ( ( (ψ `  x )  x.  ( log `  x
) )  +  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m
) ) ) )  /  x ) ) )
4924recnd 9106 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ m  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  m
)  x.  (ψ `  ( x  /  m
) ) )  x.  ( log `  m
) ) )  e.  CC )
5025recnd 9106 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  m
)  x.  (ψ `  ( x  /  m
) ) )  e.  CC )
5137recnd 9106 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  x )  x.  ( log `  x
) )  e.  CC )
5249, 50, 51nppcan3d 9430 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( 2  /  ( log `  x
) )  x.  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) )  x.  ( log `  m
) ) )  -  sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) ) )  +  ( ( (ψ `  x )  x.  ( log `  x
) )  +  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m
) ) ) ) )  =  ( ( ( 2  /  ( log `  x ) )  x.  sum_ m  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  m
)  x.  (ψ `  ( x  /  m
) ) )  x.  ( log `  m
) ) )  +  ( (ψ `  x
)  x.  ( log `  x ) ) ) )
53 elfznn 11072 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  ( 1 ... ( |_ `  (
x  /  m ) ) )  ->  n  e.  NN )
5453ad2antll 710 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
m  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  ( 1 ... ( |_ `  ( x  /  m
) ) ) ) )  ->  n  e.  NN )
55 vmacl 20893 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  NN  ->  (Λ `  n )  e.  RR )
5654, 55syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
m  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  ( 1 ... ( |_ `  ( x  /  m
) ) ) ) )  ->  (Λ `  n
)  e.  RR )
5714adantrr 698 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
m  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  ( 1 ... ( |_ `  ( x  /  m
) ) ) ) )  ->  (Λ `  m
)  e.  RR )
5820adantrr 698 . . . . . . . . . . . . . . . . . 18  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
m  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  ( 1 ... ( |_ `  ( x  /  m
) ) ) ) )  ->  m  e.  RR+ )
5958relogcld 20510 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
m  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  ( 1 ... ( |_ `  ( x  /  m
) ) ) ) )  ->  ( log `  m )  e.  RR )
6057, 59remulcld 9108 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
m  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  ( 1 ... ( |_ `  ( x  /  m
) ) ) ) )  ->  ( (Λ `  m )  x.  ( log `  m ) )  e.  RR )
6156, 60remulcld 9108 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
m  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  ( 1 ... ( |_ `  ( x  /  m
) ) ) ) )  ->  ( (Λ `  n )  x.  (
(Λ `  m )  x.  ( log `  m
) ) )  e.  RR )
6261recnd 9106 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
m  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  ( 1 ... ( |_ `  ( x  /  m
) ) ) ) )  ->  ( (Λ `  n )  x.  (
(Λ `  m )  x.  ( log `  m
) ) )  e.  CC )
634, 62fsumfldivdiag 20967 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  x ) )
sum_ n  e.  (
1 ... ( |_ `  ( x  /  m
) ) ) ( (Λ `  n )  x.  ( (Λ `  m
)  x.  ( log `  m ) ) )  =  sum_ n  e.  ( 1 ... ( |_
`  x ) )
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  n )  x.  ( (Λ `  m
)  x.  ( log `  m ) ) ) )
6414recnd 9106 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  m
)  e.  CC )
6518recnd 9106 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  m ) )  e.  CC )
6621recnd 9106 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  m )  e.  CC )
6764, 65, 66mul32d 9268 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  m )  x.  (ψ `  ( x  /  m ) ) )  x.  ( log `  m
) )  =  ( ( (Λ `  m
)  x.  ( log `  m ) )  x.  (ψ `  ( x  /  m ) ) ) )
6864, 66mulcld 9100 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  m )  x.  ( log `  m ) )  e.  CC )
6968, 65mulcomd 9101 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  m )  x.  ( log `  m
) )  x.  (ψ `  ( x  /  m
) ) )  =  ( (ψ `  (
x  /  m ) )  x.  ( (Λ `  m )  x.  ( log `  m ) ) ) )
70 chpval 20897 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  /  m )  e.  RR  ->  (ψ `  ( x  /  m
) )  =  sum_ n  e.  ( 1 ... ( |_ `  (
x  /  m ) ) ) (Λ `  n
) )
7116, 70syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  m ) )  =  sum_ n  e.  ( 1 ... ( |_ `  ( x  /  m ) ) ) (Λ `  n )
)
7271oveq1d 6088 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  m
) )  x.  (
(Λ `  m )  x.  ( log `  m
) ) )  =  ( sum_ n  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) (Λ `  n )  x.  ( (Λ `  m
)  x.  ( log `  m ) ) ) )
73 fzfid 11304 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1 ... ( |_ `  ( x  /  m
) ) )  e. 
Fin )
7456anassrs 630 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  n  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  (Λ `  n
)  e.  RR )
7574recnd 9106 . . . . . . . . . . . . . . . . 17  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  n  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  (Λ `  n
)  e.  CC )
7673, 68, 75fsummulc1 12560 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  (
x  /  m ) ) ) (Λ `  n
)  x.  ( (Λ `  m )  x.  ( log `  m ) ) )  =  sum_ n  e.  ( 1 ... ( |_ `  ( x  /  m ) ) ) ( (Λ `  n
)  x.  ( (Λ `  m )  x.  ( log `  m ) ) ) )
7772, 76eqtrd 2467 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  m
) )  x.  (
(Λ `  m )  x.  ( log `  m
) ) )  = 
sum_ n  e.  (
1 ... ( |_ `  ( x  /  m
) ) ) ( (Λ `  n )  x.  ( (Λ `  m
)  x.  ( log `  m ) ) ) )
7867, 69, 773eqtrd 2471 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  m )  x.  (ψ `  ( x  /  m ) ) )  x.  ( log `  m
) )  =  sum_ n  e.  ( 1 ... ( |_ `  (
x  /  m ) ) ) ( (Λ `  n )  x.  (
(Λ `  m )  x.  ( log `  m
) ) ) )
7978sumeq2dv 12489 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  m
)  x.  (ψ `  ( x  /  m
) ) )  x.  ( log `  m
) )  =  sum_ m  e.  ( 1 ... ( |_ `  x
) ) sum_ n  e.  ( 1 ... ( |_ `  ( x  /  m ) ) ) ( (Λ `  n
)  x.  ( (Λ `  m )  x.  ( log `  m ) ) ) )
80 fzfid 11304 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1 ... ( |_ `  ( x  /  n
) ) )  e. 
Fin )
81 elfznn 11072 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
8281adantl 453 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
8382, 55syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n
)  e.  RR )
8483recnd 9106 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n
)  e.  CC )
85 elfznn 11072 . . . . . . . . . . . . . . . . . . 19  |-  ( m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) )  ->  m  e.  NN )
8685adantl 453 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  m  e.  NN )
8786, 13syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  (Λ `  m
)  e.  RR )
8886nnrpd 10639 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  m  e.  RR+ )
8988relogcld 20510 . . . . . . . . . . . . . . . . 17  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( log `  m )  e.  RR )
9087, 89remulcld 9108 . . . . . . . . . . . . . . . 16  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( (Λ `  m )  x.  ( log `  m ) )  e.  RR )
9190recnd 9106 . . . . . . . . . . . . . . 15  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( (Λ `  m )  x.  ( log `  m ) )  e.  CC )
9280, 84, 91fsummulc2 12559 . . . . . . . . . . . . . 14  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) ) )  =  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  n
)  x.  ( (Λ `  m )  x.  ( log `  m ) ) ) )
9392sumeq2dv 12489 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) )  =  sum_ n  e.  ( 1 ... ( |_
`  x ) )
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  n )  x.  ( (Λ `  m
)  x.  ( log `  m ) ) ) )
9463, 79, 933eqtr4d 2477 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  m
)  x.  (ψ `  ( x  /  m
) ) )  x.  ( log `  m
) )  =  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) ) ) )
9594oveq2d 6089 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ m  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  m
)  x.  (ψ `  ( x  /  m
) ) )  x.  ( log `  m
) ) )  =  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) ) ) ) )
9695oveq1d 6088 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( 2  / 
( log `  x
) )  x.  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) )  x.  ( log `  m
) ) )  +  ( (ψ `  x
)  x.  ( log `  x ) ) )  =  ( ( ( 2  /  ( log `  x ) )  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) ) )  +  ( (ψ `  x )  x.  ( log `  x ) ) ) )
9752, 96eqtrd 2467 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( 2  /  ( log `  x
) )  x.  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) )  x.  ( log `  m
) ) )  -  sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) ) )  +  ( ( (ψ `  x )  x.  ( log `  x
) )  +  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m
) ) ) ) )  =  ( ( ( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) ) )  +  ( (ψ `  x )  x.  ( log `  x ) ) ) )
9897oveq1d 6088 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( ( 2  /  ( log `  x ) )  x. 
sum_ m  e.  (
1 ... ( |_ `  x ) ) ( ( (Λ `  m
)  x.  (ψ `  ( x  /  m
) ) )  x.  ( log `  m
) ) )  -  sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) ) )  +  ( ( (ψ `  x )  x.  ( log `  x
) )  +  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m
) ) ) ) )  /  x )  =  ( ( ( ( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) ) )  +  ( (ψ `  x )  x.  ( log `  x ) ) )  /  x ) )
9948, 98eqtr3d 2469 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( ( 2  /  ( log `  x ) )  x. 
sum_ m  e.  (
1 ... ( |_ `  x ) ) ( ( (Λ `  m
)  x.  (ψ `  ( x  /  m
) ) )  x.  ( log `  m
) ) )  -  sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) ) )  /  x )  +  ( ( ( (ψ `  x )  x.  ( log `  x
) )  +  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m
) ) ) )  /  x ) )  =  ( ( ( ( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) ) )  +  ( (ψ `  x )  x.  ( log `  x ) ) )  /  x ) )
10099oveq1d 6088 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( ( ( 2  /  ( log `  x ) )  x.  sum_ m  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  m
)  x.  (ψ `  ( x  /  m
) ) )  x.  ( log `  m
) ) )  -  sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) ) )  /  x )  +  ( ( ( (ψ `  x )  x.  ( log `  x
) )  +  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m
) ) ) )  /  x ) )  -  ( 2  x.  ( log `  x
) ) )  =  ( ( ( ( ( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) ) )  +  ( (ψ `  x )  x.  ( log `  x ) ) )  /  x )  -  ( 2  x.  ( log `  x
) ) ) )
10143, 100eqtr3d 2469 . . . . 5  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( ( 2  /  ( log `  x ) )  x. 
sum_ m  e.  (
1 ... ( |_ `  x ) ) ( ( (Λ `  m
)  x.  (ψ `  ( x  /  m
) ) )  x.  ( log `  m
) ) )  -  sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) ) )  /  x )  +  ( ( ( ( (ψ `  x
)  x.  ( log `  x ) )  + 
sum_ m  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) ) )  /  x )  -  ( 2  x.  ( log `  x
) ) ) )  =  ( ( ( ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) ) ) )  +  ( (ψ `  x )  x.  ( log `  x
) ) )  /  x )  -  (
2  x.  ( log `  x ) ) ) )
102101mpteq2dva 4287 . . . 4  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( ( ( ( 2  /  ( log `  x ) )  x.  sum_ m  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  m
)  x.  (ψ `  ( x  /  m
) ) )  x.  ( log `  m
) ) )  -  sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) ) )  /  x )  +  ( ( ( ( (ψ `  x
)  x.  ( log `  x ) )  + 
sum_ m  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) ) )  /  x )  -  ( 2  x.  ( log `  x
) ) ) ) )  =  ( x  e.  ( 1 (,) 
+oo )  |->  ( ( ( ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) ) ) )  +  ( (ψ `  x )  x.  ( log `  x
) ) )  /  x )  -  (
2  x.  ( log `  x ) ) ) ) )
10339, 41resubcld 9457 . . . . 5  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( (ψ `  x )  x.  ( log `  x ) )  +  sum_ m  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  m
)  x.  (ψ `  ( x  /  m
) ) ) )  /  x )  -  ( 2  x.  ( log `  x ) ) )  e.  RR )
104 selberg3lem2 21244 . . . . . 6  |-  ( x  e.  ( 1 (,) 
+oo )  |->  ( ( ( ( 2  / 
( log `  x
) )  x.  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) )  x.  ( log `  m
) ) )  -  sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) ) )  /  x ) )  e.  O ( 1 )
105104a1i 11 . . . . 5  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( ( ( 2  /  ( log `  x ) )  x. 
sum_ m  e.  (
1 ... ( |_ `  x ) ) ( ( (Λ `  m
)  x.  (ψ `  ( x  /  m
) ) )  x.  ( log `  m
) ) )  -  sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) ) )  /  x ) )  e.  O ( 1 ) )
10631ex 424 . . . . . . 7  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  ->  x  e.  RR+ )
)
107106ssrdv 3346 . . . . . 6  |-  (  T. 
->  ( 1 (,)  +oo )  C_  RR+ )
108 selberg2 21237 . . . . . . 7  |-  ( x  e.  RR+  |->  ( ( ( ( (ψ `  x )  x.  ( log `  x ) )  +  sum_ m  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  m
)  x.  (ψ `  ( x  /  m
) ) ) )  /  x )  -  ( 2  x.  ( log `  x ) ) ) )  e.  O
( 1 )
109108a1i 11 . . . . . 6  |-  (  T. 
->  ( x  e.  RR+  |->  ( ( ( ( (ψ `  x )  x.  ( log `  x
) )  +  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m
) ) ) )  /  x )  -  ( 2  x.  ( log `  x ) ) ) )  e.  O
( 1 ) )
110107, 109o1res2 12349 . . . . 5  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( ( ( (ψ `  x )  x.  ( log `  x
) )  +  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m
) ) ) )  /  x )  -  ( 2  x.  ( log `  x ) ) ) )  e.  O
( 1 ) )
11132, 103, 105, 110o1add2 12409 . . . 4  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( ( ( ( 2  /  ( log `  x ) )  x.  sum_ m  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  m
)  x.  (ψ `  ( x  /  m
) ) )  x.  ( log `  m
) ) )  -  sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) ) )  /  x )  +  ( ( ( ( (ψ `  x
)  x.  ( log `  x ) )  + 
sum_ m  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) ) )  /  x )  -  ( 2  x.  ( log `  x
) ) ) ) )  e.  O ( 1 ) )
112102, 111eqeltrrd 2510 . . 3  |-  (  T. 
->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( ( ( ( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) ) )  +  ( (ψ `  x )  x.  ( log `  x ) ) )  /  x )  -  ( 2  x.  ( log `  x
) ) ) )  e.  O ( 1 ) )
11380, 90fsumrecl 12520 . . . . . . . . . . 11  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) )  e.  RR )
11483, 113remulcld 9108 . . . . . . . . . 10  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) ) )  e.  RR )
11510, 114fsumrecl 12520 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) )  e.  RR )
1169, 115remulcld 9108 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) ) )  e.  RR )
117116, 37readdcld 9107 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) ) ) )  +  ( (ψ `  x )  x.  ( log `  x
) ) )  e.  RR )
118117, 31rerpdivcld 10667 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) ) ) )  +  ( (ψ `  x )  x.  ( log `  x
) ) )  /  x )  e.  RR )
119118, 41resubcld 9457 . . . . 5  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( ( 2  /  ( log `  x ) )  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) ) )  +  ( (ψ `  x )  x.  ( log `  x ) ) )  /  x )  -  ( 2  x.  ( log `  x
) ) )  e.  RR )
120119recnd 9106 . . . 4  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( ( 2  /  ( log `  x ) )  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) ) )  +  ( (ψ `  x )  x.  ( log `  x ) ) )  /  x )  -  ( 2  x.  ( log `  x
) ) )  e.  CC )
1214adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR )
122121, 82nndivred 10040 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR )
123122adantr 452 . . . . . . . . . . . . . 14  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( x  /  n )  e.  RR )
124123, 86nndivred 10040 . . . . . . . . . . . . 13  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( (
x  /  n )  /  m )  e.  RR )
125 chpcl 20899 . . . . . . . . . . . . 13  |-  ( ( ( x  /  n
)  /  m )  e.  RR  ->  (ψ `  ( ( x  /  n )  /  m
) )  e.  RR )
126124, 125syl 16 . . . . . . . . . . . 12  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  (ψ `  (
( x  /  n
)  /  m ) )  e.  RR )
12787, 126remulcld 9108 . . . . . . . . . . 11  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( (Λ `  m )  x.  (ψ `  ( ( x  /  n )  /  m
) ) )  e.  RR )
12880, 127fsumrecl 12520 . . . . . . . . . 10  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  (ψ `  ( ( x  /  n )  /  m
) ) )  e.  RR )
12983, 128remulcld 9108 . . . . . . . . 9  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) )  e.  RR )
13010, 129fsumrecl 12520 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) )  e.  RR )
1319, 130remulcld 9108 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) )  e.  RR )
13237, 131resubcld 9457 . . . . . 6  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( (ψ `  x
)  x.  ( log `  x ) )  -  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) )  e.  RR )
133132, 31rerpdivcld 10667 . . . . 5  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( (ψ `  x )  x.  ( log `  x ) )  -  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) )  /  x
)  e.  RR )
134133recnd 9106 . . . 4  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( (ψ `  x )  x.  ( log `  x ) )  -  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) )  /  x
)  e.  CC )
135116recnd 9106 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) ) )  e.  CC )
136131recnd 9106 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) )  e.  CC )
13751, 135, 136pnncand 9442 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( (ψ `  x )  x.  ( log `  x ) )  +  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) ) ) ) )  -  ( ( (ψ `  x )  x.  ( log `  x ) )  -  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) ) )  =  ( ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) ) ) )  +  ( ( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) ) )
138135, 51addcomd 9260 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) ) ) )  +  ( (ψ `  x )  x.  ( log `  x
) ) )  =  ( ( (ψ `  x )  x.  ( log `  x ) )  +  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) ) ) ) ) )
139138oveq1d 6088 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) ) ) )  +  ( (ψ `  x )  x.  ( log `  x
) ) )  -  ( ( (ψ `  x )  x.  ( log `  x ) )  -  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) ) )  =  ( ( ( (ψ `  x )  x.  ( log `  x ) )  +  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) ) ) ) )  -  ( ( (ψ `  x )  x.  ( log `  x ) )  -  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) ) ) )
14087recnd 9106 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  (Λ `  m
)  e.  CC )
14189recnd 9106 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( log `  m )  e.  CC )
142126recnd 9106 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  (ψ `  (
( x  /  n
)  /  m ) )  e.  CC )
143140, 141, 142adddid 9104 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  =  ( ( (Λ `  m )  x.  ( log `  m ) )  +  ( (Λ `  m
)  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) )
144143sumeq2dv 12489 . . . . . . . . . . . . . . . . . 18  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  = 
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( ( (Λ `  m
)  x.  ( log `  m ) )  +  ( (Λ `  m
)  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) )
145127recnd 9106 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( (Λ `  m )  x.  (ψ `  ( ( x  /  n )  /  m
) ) )  e.  CC )
14680, 91, 145fsumadd 12524 . . . . . . . . . . . . . . . . . 18  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( ( (Λ `  m
)  x.  ( log `  m ) )  +  ( (Λ `  m
)  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) )  =  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) )  + 
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  (ψ `  ( (
x  /  n )  /  m ) ) ) ) )
147144, 146eqtrd 2467 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  =  ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) )  + 
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  (ψ `  ( (
x  /  n )  /  m ) ) ) ) )
148147oveq2d 6089 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) ) )  =  ( (Λ `  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( log `  m
) )  +  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) )
149113recnd 9106 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) )  e.  CC )
150128recnd 9106 . . . . . . . . . . . . . . . . 17  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  (ψ `  ( ( x  /  n )  /  m
) ) )  e.  CC )
15184, 149, 150adddid 9104 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( log `  m
) )  +  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) )  =  ( ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) )  +  ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) )
152148, 151eqtrd 2467 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) ) )  =  ( ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) )  +  ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) )
153152sumeq2dv 12489 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  =  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) )  +  ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) )
154114recnd 9106 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) ) )  e.  CC )
155129recnd 9106 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) )  e.  CC )
15610, 154, 155fsumadd 12524 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) )  +  ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) )  =  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) ) )  +  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) )
157153, 156eqtrd 2467 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  =  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) )  +  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) )
158157oveq2d 6089 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) ) )  =  ( ( 2  /  ( log `  x ) )  x.  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) )  +  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) ) )
1599recnd 9106 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  /  ( log `  x ) )  e.  CC )
160115recnd 9106 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) )  e.  CC )
161130recnd 9106 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) )  e.  CC )
162159, 160, 161adddid 9104 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) )  +  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) )  =  ( ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) ) ) )  +  ( ( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) ) )
163158, 162eqtrd 2467 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) ) )  =  ( ( ( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) ) )  +  ( ( 2  /  ( log `  x ) )  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) ) )
164137, 139, 1633eqtr4d 2477 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) ) ) )  +  ( (ψ `  x )  x.  ( log `  x
) ) )  -  ( ( (ψ `  x )  x.  ( log `  x ) )  -  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) ) )  =  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) ) )
165164oveq1d 6088 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( ( 2  /  ( log `  x ) )  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) ) )  +  ( (ψ `  x )  x.  ( log `  x ) ) )  -  ( ( (ψ `  x )  x.  ( log `  x
) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) ) )  /  x )  =  ( ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) )  /  x
) )
166117recnd 9106 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) ) ) )  +  ( (ψ `  x )  x.  ( log `  x
) ) )  e.  CC )
16751, 136subcld 9403 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( (ψ `  x
)  x.  ( log `  x ) )  -  ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) )  e.  CC )
168166, 167, 46, 47divsubdird 9821 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( ( 2  /  ( log `  x ) )  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) ) )  +  ( (ψ `  x )  x.  ( log `  x ) ) )  -  ( ( (ψ `  x )  x.  ( log `  x
) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) ) )  /  x )  =  ( ( ( ( ( 2  /  ( log `  x ) )  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) ) )  +  ( (ψ `  x )  x.  ( log `  x ) ) )  /  x )  -  ( ( ( (ψ `  x )  x.  ( log `  x
) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) )  /  x
) ) )
169 2cn 10062 . . . . . . . . . . . . . 14  |-  2  e.  CC
170169a1i 11 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  2  e.  CC )
17189, 126readdcld 9107 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( ( log `  m )  +  (ψ `  ( (
x  /  n )  /  m ) ) )  e.  RR )
17287, 171remulcld 9108 . . . . . . . . . . . . . . . . 17  |-  ( ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  e.  RR )
17380, 172fsumrecl 12520 . . . . . . . . . . . . . . . 16  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  e.  RR )
17483, 173remulcld 9108 . . . . . . . . . . . . . . 15  |-  ( ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) ) )  e.  RR )
17510, 174fsumrecl 12520 . . . . . . . . . . . . . 14  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  e.  RR )
176175recnd 9106 . . . . . . . . . . . . 13  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  e.  CC )
177170, 176mulcld 9100 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) ) )  e.  CC )
17836recnd 9106 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  CC )
1798rpne0d 10645 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  =/=  0 )
180177, 178, 46, 179, 47divdiv1d 9813 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( 2  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) ) )  /  ( log `  x ) )  /  x )  =  ( ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) )  /  (
( log `  x
)  x.  x ) ) )
181178, 46mulcomd 9101 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( log `  x
)  x.  x )  =  ( x  x.  ( log `  x
) ) )
182181oveq2d 6089 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) )  /  (
( log `  x
)  x.  x ) )  =  ( ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) ) )  /  ( x  x.  ( log `  x
) ) ) )
183180, 182eqtrd 2467 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( 2  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) ) )  /  ( log `  x ) )  /  x )  =  ( ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) )  /  (
x  x.  ( log `  x ) ) ) )
184170, 176, 178, 179div23d 9819 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) )  /  ( log `  x ) )  =  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) ) )
185184oveq1d 6088 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( 2  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) ) )  /  ( log `  x ) )  /  x )  =  ( ( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) )  /  x
) )
18631, 8rpmulcld 10656 . . . . . . . . . . . 12  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  x.  ( log `  x ) )  e.  RR+ )
187186rpcnd 10642 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  x.  ( log `  x ) )  e.  CC )
188186rpne0d 10645 . . . . . . . . . . 11  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  x.  ( log `  x ) )  =/=  0 )
189170, 176, 187, 188divassd 9817 . . . . . . . . . 10  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) )  /  (
x  x.  ( log `  x ) ) )  =  ( 2  x.  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  ( x  x.  ( log `  x
) ) ) ) )
190183, 185, 1893eqtr3d 2475 . . . . . . . . 9  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) )  /  x
)  =  ( 2  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  ( x  x.  ( log `  x
) ) ) ) )
191165, 168, 1903eqtr3d 2475 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( ( 2  /  ( log `  x ) )  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) ) )  +  ( (ψ `  x )  x.  ( log `  x ) ) )  /  x )  -  ( ( ( (ψ `  x )  x.  ( log `  x
) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) )  /  x
) )  =  ( 2  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) ) )  /  ( x  x.  ( log `  x
) ) ) ) )
192191oveq1d 6088 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( ( ( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) ) )  +  ( (ψ `  x )  x.  ( log `  x ) ) )  /  x )  -  ( ( ( (ψ `  x )  x.  ( log `  x
) )  -  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) )  /  x
) )  -  (
2  x.  ( log `  x ) ) )  =  ( ( 2  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  ( x  x.  ( log `  x
) ) ) )  -  ( 2  x.  ( log `  x
) ) ) )
193118recnd 9106 . . . . . . . 8  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) ) ) )  +  ( (ψ `  x )  x.  ( log `  x
) ) )  /  x )  e.  CC )
194193, 42, 134sub32d 9435 . . . . . . 7  |-  ( (  T.  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( ( ( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) ) )  +  ( (ψ `  x )  x.  ( log `  x ) ) )  /  x )  -  ( 2  x.  ( log `  x
) ) )  -  ( ( ( (ψ `  x )  x.  ( log `  x ) )  -  ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (ψ `  ( ( x  /  n )  /  m
) ) ) ) ) )  /  x
) )  =  ( ( ( ( ( ( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... (