Metamath Proof Explorer

Theorem selberg4

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 , Lam ( i ) Lam ( j ) Lam ( k ) ; we eliminate one of the nested sums by using the definition of psi ( x ) = sum_ k <_ x , Lam ( k ) . This statement can thus equivalently be written psi ( x ) log ^ 2 ( x ) = 2 sum_ i j k <_ x , Lam ( i ) Lam ( j ) Lam ( k ) + O ( x log x ) . Equation 10.4.23 of Shapiro, p. 422. (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Assertion selberg4 
|- ( x e. ( 1 (,) +oo ) |-> ( ( ( ( psi ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) / x ) ) e. O(1)

Proof

Step Hyp Ref Expression
1 2re 
 |-  2 e. RR
2 1 a1i 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 e. RR )
3 elioore 
 |-  ( x e. ( 1 (,) +oo ) -> x e. RR )
4 3 adantl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR )
5 eliooord 
 |-  ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) )
6 5 adantl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 < x /\ x < +oo ) )
7 6 simpld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 < x )
8 4 7 rplogcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ )
9 2 8 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 / ( log ` x ) ) e. RR )
10 fzfid 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
11 elfznn 
 |-  ( m e. ( 1 ... ( |_ ` x ) ) -> m e. NN )
12 11 adantl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> m e. NN )
13 vmacl 
 |-  ( m e. NN -> ( Lam ` m ) e. RR )
14 12 13 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` m ) e. RR )
15 4 adantr 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR )
16 15 12 nndivred 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( x / m ) e. RR )
17 chpcl 
 |-  ( ( x / m ) e. RR -> ( psi ` ( x / m ) ) e. RR )
18 16 17 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( x / m ) ) e. RR )
19 14 18 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) e. RR )
20 12 nnrpd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> m e. RR+ )
21 20 relogcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` m ) e. RR )
22 19 21 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) e. RR )
23 10 22 fsumrecl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) e. RR )
24 9 23 remulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) ) e. RR )
25 10 19 fsumrecl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) e. RR )
26 24 25 resubcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) ) - sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) e. RR )
27 1rp 
 |-  1 e. RR+
28 27 a1i 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR+ )
29 1red 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR )
30 29 4 7 ltled 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 <_ x )
31 4 28 30 rpgecld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ )
32 26 31 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) ) - sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) / x ) e. RR )
33 32 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) ) - sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) / x ) e. CC )
34 chpcl 
 |-  ( x e. RR -> ( psi ` x ) e. RR )
35 4 34 syl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( psi ` x ) e. RR )
36 31 relogcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR )
37 35 36 remulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( psi ` x ) x. ( log ` x ) ) e. RR )
38 37 25 readdcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) e. RR )
39 38 31 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) / x ) e. RR )
40 39 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) / x ) e. CC )
41 2 36 remulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( log ` x ) ) e. RR )
42 41 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( log ` x ) ) e. CC )
43 33 40 42 addsubassd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) ) - sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) / x ) + ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) / x ) ) - ( 2 x. ( log ` x ) ) ) = ( ( ( ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) ) - sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) / x ) + ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) )
44 26 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) ) - sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) e. CC )
45 38 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) e. CC )
46 4 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. CC )
47 31 rpne0d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x =/= 0 )
48 44 45 46 47 divdird 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) ) - sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) + ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) ) / x ) = ( ( ( ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) ) - sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) / x ) + ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) / x ) ) )
49 24 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) ) e. CC )
50 25 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) e. CC )
51 37 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( psi ` x ) x. ( log ` x ) ) e. CC )
52 49 50 51 nppcan3d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) ) - sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) + ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) ) = ( ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) )
53 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` ( x / m ) ) ) -> n e. NN )
54 53 ad2antll 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( m e. ( 1 ... ( |_ ` x ) ) /\ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ) ) -> n e. NN )
55 vmacl 
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
56 54 55 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( m e. ( 1 ... ( |_ ` x ) ) /\ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ) ) -> ( Lam ` n ) e. RR )
57 14 adantrr 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( m e. ( 1 ... ( |_ ` x ) ) /\ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ) ) -> ( Lam ` m ) e. RR )
58 20 adantrr 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( m e. ( 1 ... ( |_ ` x ) ) /\ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ) ) -> m e. RR+ )
59 58 relogcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( m e. ( 1 ... ( |_ ` x ) ) /\ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ) ) -> ( log ` m ) e. RR )
60 57 59 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( m e. ( 1 ... ( |_ ` x ) ) /\ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ) ) -> ( ( Lam ` m ) x. ( log ` m ) ) e. RR )
61 56 60 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( m e. ( 1 ... ( |_ ` x ) ) /\ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ) ) -> ( ( Lam ` n ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) e. RR )
62 61 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ ( m e. ( 1 ... ( |_ ` x ) ) /\ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ) ) -> ( ( Lam ` n ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) e. CC )
63 4 62 fsumfldivdiag 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` n ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) )
64 14 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` m ) e. CC )
65 18 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( x / m ) ) e. CC )
66 21 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` m ) e. CC )
67 64 65 66 mul32d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) = ( ( ( Lam ` m ) x. ( log ` m ) ) x. ( psi ` ( x / m ) ) ) )
68 64 66 mulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` m ) x. ( log ` m ) ) e. CC )
69 68 65 mulcomd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` m ) x. ( log ` m ) ) x. ( psi ` ( x / m ) ) ) = ( ( psi ` ( x / m ) ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) )
70 chpval 
 |-  ( ( x / m ) e. RR -> ( psi ` ( x / m ) ) = sum_ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ( Lam ` n ) )
71 16 70 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( x / m ) ) = sum_ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ( Lam ` n ) )
72 71 oveq1d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( psi ` ( x / m ) ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ( Lam ` n ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) )
73 fzfid 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( x / m ) ) ) e. Fin )
74 56 anassrs 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> ( Lam ` n ) e. RR )
75 74 recnd 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> ( Lam ` n ) e. CC )
76 73 68 75 fsummulc1 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ( Lam ` n ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) = sum_ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` n ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) )
77 72 76 eqtrd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( psi ` ( x / m ) ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) = sum_ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` n ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) )
78 67 69 77 3eqtrd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) = sum_ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` n ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) )
79 78 sumeq2dv 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) = sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` n ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) )
80 fzfid 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( x / n ) ) ) e. Fin )
81 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
82 81 adantl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
83 82 55 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. RR )
84 83 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. CC )
85 elfznn 
 |-  ( m e. ( 1 ... ( |_ ` ( x / n ) ) ) -> m e. NN )
86 85 adantl 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. NN )
87 86 13 syl 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( Lam ` m ) e. RR )
88 86 nnrpd 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. RR+ )
89 88 relogcld 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( log ` m ) e. RR )
90 87 89 remulcld 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( Lam ` m ) x. ( log ` m ) ) e. RR )
91 90 recnd 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( Lam ` m ) x. ( log ` m ) ) e. CC )
92 80 84 91 fsummulc2 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) )
93 92 sumeq2dv 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) )
94 63 79 93 3eqtr4d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) )
95 94 oveq2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) ) = ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) )
96 95 oveq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) = ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) )
97 52 96 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) ) - sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) + ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) ) = ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) )
98 97 oveq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) ) - sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) + ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) ) / x ) = ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) / x ) )
99 48 98 eqtr3d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) ) - sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) / x ) + ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) / x ) ) = ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) / x ) )
100 99 oveq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) ) - sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) / x ) + ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) / x ) ) - ( 2 x. ( log ` x ) ) ) = ( ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) )
101 43 100 eqtr3d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) ) - sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) / x ) + ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) = ( ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) )
102 101 mpteq2dva 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) ) - sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) / x ) + ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) )
103 39 41 resubcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) e. RR )
104 selberg3lem2 
 |-  ( x e. ( 1 (,) +oo ) |-> ( ( ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) ) - sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) / x ) ) e. O(1)
105 104 a1i 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) ) - sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) / x ) ) e. O(1) )
106 31 ex 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) -> x e. RR+ ) )
107 106 ssrdv 
 |-  ( T. -> ( 1 (,) +oo ) C_ RR+ )
108 selberg2 
 |-  ( x e. RR+ |-> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)
109 108 a1i 
 |-  ( T. -> ( x e. RR+ |-> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1) )
110 107 109 o1res2 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1) )
111 32 103 105 110 o1add2 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( ( 2 / ( log ` x ) ) x. sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) ) - sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) / x ) + ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) ) e. O(1) )
112 102 111 eqeltrrd 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1) )
113 80 90 fsumrecl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) e. RR )
114 83 113 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) e. RR )
115 10 114 fsumrecl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) e. RR )
116 9 115 remulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) e. RR )
117 116 37 readdcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) e. RR )
118 117 31 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) / x ) e. RR )
119 118 41 resubcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) e. RR )
120 119 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) e. CC )
121 4 adantr 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR )
122 121 82 nndivred 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR )
123 122 adantr 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( x / n ) e. RR )
124 123 86 nndivred 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( x / n ) / m ) e. RR )
125 chpcl 
 |-  ( ( ( x / n ) / m ) e. RR -> ( psi ` ( ( x / n ) / m ) ) e. RR )
126 124 125 syl 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( psi ` ( ( x / n ) / m ) ) e. RR )
127 87 126 remulcld 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) e. RR )
128 80 127 fsumrecl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) e. RR )
129 83 128 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) e. RR )
130 10 129 fsumrecl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) e. RR )
131 9 130 remulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) e. RR )
132 37 131 resubcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( psi ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) e. RR )
133 132 31 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( psi ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) / x ) e. RR )
134 133 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( psi ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) / x ) e. CC )
135 116 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) e. CC )
136 131 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) e. CC )
137 51 135 136 pnncand 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) ) - ( ( ( psi ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) ) = ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) )
138 135 51 addcomd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) = ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) ) )
139 138 oveq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) - ( ( ( psi ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) ) = ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) ) - ( ( ( psi ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) ) )
140 87 recnd 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( Lam ` m ) e. CC )
141 89 recnd 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( log ` m ) e. CC )
142 126 recnd 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( psi ` ( ( x / n ) / m ) ) e. CC )
143 140 141 142 adddid 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) = ( ( ( Lam ` m ) x. ( log ` m ) ) + ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) )
144 143 sumeq2dv 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( ( Lam ` m ) x. ( log ` m ) ) + ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) )
145 127 recnd 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) e. CC )
146 80 91 145 fsumadd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( ( Lam ` m ) x. ( log ` m ) ) + ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) = ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) + sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) )
147 144 146 eqtrd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) = ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) + sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) )
148 147 oveq2d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) = ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) + sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) )
149 113 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) e. CC )
150 128 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) e. CC )
151 84 149 150 adddid 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) + sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) = ( ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) + ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) )
152 148 151 eqtrd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) = ( ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) + ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) )
153 152 sumeq2dv 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) + ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) )
154 114 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) e. CC )
155 129 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) e. CC )
156 10 154 155 fsumadd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) + ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) )
157 153 156 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) )
158 157 oveq2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) ) = ( ( 2 / ( log ` x ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) )
159 9 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 / ( log ` x ) ) e. CC )
160 115 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) e. CC )
161 130 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) e. CC )
162 159 160 161 adddid 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) = ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) )
163 158 162 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) ) = ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) )
164 137 139 163 3eqtr4d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) - ( ( ( psi ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) ) = ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) ) )
165 164 oveq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) - ( ( ( psi ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) ) / x ) = ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) ) / x ) )
166 117 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) e. CC )
167 51 136 subcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( psi ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) e. CC )
168 166 167 46 47 divsubdird 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) - ( ( ( psi ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) ) / x ) = ( ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) / x ) - ( ( ( ( psi ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) / x ) ) )
169 2cnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 e. CC )
170 89 126 readdcld 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) e. RR )
171 87 170 remulcld 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) e. RR )
172 80 171 fsumrecl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) e. RR )
173 83 172 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) e. RR )
174 10 173 fsumrecl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) e. RR )
175 174 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) e. CC )
176 169 175 mulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) ) e. CC )
177 36 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
178 8 rpne0d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) =/= 0 )
179 176 177 46 178 47 divdiv1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) ) / ( log ` x ) ) / x ) = ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) ) / ( ( log ` x ) x. x ) ) )
180 177 46 mulcomd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) x. x ) = ( x x. ( log ` x ) ) )
181 180 oveq2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) ) / ( ( log ` x ) x. x ) ) = ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) ) / ( x x. ( log ` x ) ) ) )
182 179 181 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) ) / ( log ` x ) ) / x ) = ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) ) / ( x x. ( log ` x ) ) ) )
183 169 175 177 178 div23d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) ) / ( log ` x ) ) = ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) ) )
184 183 oveq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) ) / ( log ` x ) ) / x ) = ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) ) / x ) )
185 31 8 rpmulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) e. RR+ )
186 185 rpcnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) e. CC )
187 185 rpne0d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) =/= 0 )
188 169 175 186 187 divassd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) ) / ( x x. ( log ` x ) ) ) = ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) )
189 182 184 188 3eqtr3d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) ) / x ) = ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) )
190 165 168 189 3eqtr3d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) / x ) - ( ( ( ( psi ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) / x ) ) = ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) )
191 190 oveq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) / x ) - ( ( ( ( psi ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) / x ) ) - ( 2 x. ( log ` x ) ) ) = ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) - ( 2 x. ( log ` x ) ) ) )
192 118 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) / x ) e. CC )
193 192 42 134 sub32d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) - ( ( ( ( psi ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) / x ) ) = ( ( ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) / x ) - ( ( ( ( psi ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) / x ) ) - ( 2 x. ( log ` x ) ) ) )
194 174 185 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) e. RR )
195 194 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) e. CC )
196 169 195 177 subdid 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( log ` x ) ) ) = ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) ) - ( 2 x. ( log ` x ) ) ) )
197 191 193 196 3eqtr4d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) - ( ( ( ( psi ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) / x ) ) = ( 2 x. ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( log ` x ) ) ) )
198 197 mpteq2dva 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) - ( ( ( ( psi ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) / x ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( 2 x. ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( log ` x ) ) ) ) )
199 194 36 resubcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( log ` x ) ) e. RR )
200 ioossre 
 |-  ( 1 (,) +oo ) C_ RR
201 2cnd 
 |-  ( T. -> 2 e. CC )
202 o1const 
 |-  ( ( ( 1 (,) +oo ) C_ RR /\ 2 e. CC ) -> ( x e. ( 1 (,) +oo ) |-> 2 ) e. O(1) )
203 200 201 202 sylancr 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> 2 ) e. O(1) )
204 selbergb 
 |-  E. c e. RR+ A. y e. ( 1 [,) +oo ) ( abs ` ( ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( y / i ) ) ) ) / y ) - ( 2 x. ( log ` y ) ) ) ) <_ c
205 simpl 
 |-  ( ( c e. RR+ /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( y / i ) ) ) ) / y ) - ( 2 x. ( log ` y ) ) ) ) <_ c ) -> c e. RR+ )
206 simpr 
 |-  ( ( c e. RR+ /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( y / i ) ) ) ) / y ) - ( 2 x. ( log ` y ) ) ) ) <_ c ) -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( y / i ) ) ) ) / y ) - ( 2 x. ( log ` y ) ) ) ) <_ c )
207 205 206 selberg4lem1 
 |-  ( ( c e. RR+ /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( y / i ) ) ) ) / y ) - ( 2 x. ( log ` y ) ) ) ) <_ c ) -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( log ` x ) ) ) e. O(1) )
208 207 rexlimiva 
 |-  ( E. c e. RR+ A. y e. ( 1 [,) +oo ) ( abs ` ( ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( y / i ) ) ) ) / y ) - ( 2 x. ( log ` y ) ) ) ) <_ c -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( log ` x ) ) ) e. O(1) )
209 204 208 mp1i 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( log ` x ) ) ) e. O(1) )
210 2 199 203 209 o1mul2 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( 2 x. ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( log ` m ) + ( psi ` ( ( x / n ) / m ) ) ) ) ) / ( x x. ( log ` x ) ) ) - ( log ` x ) ) ) ) e. O(1) )
211 198 210 eqeltrd 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) - ( ( ( ( psi ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) / x ) ) ) e. O(1) )
212 120 134 211 o1dif 
 |-  ( T. -> ( ( x e. ( 1 (,) +oo ) |-> ( ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1) <-> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( psi ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) / x ) ) e. O(1) ) )
213 112 212 mpbid 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( psi ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) / x ) ) e. O(1) )
214 213 mptru 
 |-  ( x e. ( 1 (,) +oo ) |-> ( ( ( ( psi ` x ) x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) / x ) ) e. O(1)