Metamath Proof Explorer

Theorem selberg4r

Description: Selberg's symmetry formula, using the residual of the second Chebyshev function. Equation 10.6.11 of Shapiro, p. 430. (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Hypothesis pntrval.r 
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
Assertion selberg4r 
|- ( x e. ( 1 (,) +oo ) |-> ( ( ( ( R ` 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. ( R ` ( ( x / n ) / m ) ) ) ) ) ) / x ) ) e. O(1)

Proof

Step Hyp Ref Expression
1 pntrval.r 
 |-  R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
2 elioore 
 |-  ( x e. ( 1 (,) +oo ) -> x e. RR )
3 2 adantl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR )
4 1rp 
 |-  1 e. RR+
5 4 a1i 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR+ )
6 1red 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR )
7 eliooord 
 |-  ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) )
8 7 adantl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 < x /\ x < +oo ) )
9 8 simpld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 < x )
10 6 3 9 ltled 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 <_ x )
11 3 5 10 rpgecld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ )
12 1 pntrval 
 |-  ( x e. RR+ -> ( R ` x ) = ( ( psi ` x ) - x ) )
13 11 12 syl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` x ) = ( ( psi ` x ) - x ) )
14 13 oveq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( R ` x ) x. ( log ` x ) ) = ( ( ( psi ` x ) - x ) x. ( log ` x ) ) )
15 chpcl 
 |-  ( x e. RR -> ( psi ` x ) e. RR )
16 3 15 syl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( psi ` x ) e. RR )
17 16 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( psi ` x ) e. CC )
18 3 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. CC )
19 11 relogcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR )
20 19 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
21 17 18 20 subdird 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( psi ` x ) - x ) x. ( log ` x ) ) = ( ( ( psi ` x ) x. ( log ` x ) ) - ( x x. ( log ` x ) ) ) )
22 14 21 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( R ` x ) x. ( log ` x ) ) = ( ( ( psi ` x ) x. ( log ` x ) ) - ( x x. ( log ` x ) ) ) )
23 11 ad2antrr 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> x e. RR+ )
24 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
25 24 adantl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
26 25 nnrpd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
27 26 adantr 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> n e. RR+ )
28 23 27 rpdivcld 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( x / n ) e. RR+ )
29 elfznn 
 |-  ( m e. ( 1 ... ( |_ ` ( x / n ) ) ) -> m e. NN )
30 29 adantl 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. NN )
31 30 nnrpd 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. RR+ )
32 28 31 rpdivcld 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( x / n ) / m ) e. RR+ )
33 1 pntrval 
 |-  ( ( ( x / n ) / m ) e. RR+ -> ( R ` ( ( x / n ) / m ) ) = ( ( psi ` ( ( x / n ) / m ) ) - ( ( x / n ) / m ) ) )
34 32 33 syl 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( R ` ( ( x / n ) / m ) ) = ( ( psi ` ( ( x / n ) / m ) ) - ( ( x / n ) / m ) ) )
35 34 oveq2d 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( Lam ` m ) x. ( R ` ( ( x / n ) / m ) ) ) = ( ( Lam ` m ) x. ( ( psi ` ( ( x / n ) / m ) ) - ( ( x / n ) / m ) ) ) )
36 vmacl 
 |-  ( m e. NN -> ( Lam ` m ) e. RR )
37 30 36 syl 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( Lam ` m ) e. RR )
38 37 recnd 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( Lam ` m ) e. CC )
39 3 adantr 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR )
40 39 25 nndivred 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR )
41 40 adantr 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( x / n ) e. RR )
42 41 30 nndivred 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( x / n ) / m ) e. RR )
43 chpcl 
 |-  ( ( ( x / n ) / m ) e. RR -> ( psi ` ( ( x / n ) / m ) ) e. RR )
44 42 43 syl 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( psi ` ( ( x / n ) / m ) ) e. RR )
45 44 recnd 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( psi ` ( ( x / n ) / m ) ) e. CC )
46 42 recnd 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( x / n ) / m ) e. CC )
47 38 45 46 subdid 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( Lam ` m ) x. ( ( psi ` ( ( x / n ) / m ) ) - ( ( x / n ) / m ) ) ) = ( ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) - ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) )
48 35 47 eqtrd 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( Lam ` m ) x. ( R ` ( ( x / n ) / m ) ) ) = ( ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) - ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) )
49 48 sumeq2dv 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( R ` ( ( x / n ) / m ) ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) - ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) )
50 fzfid 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( x / n ) ) ) e. Fin )
51 37 44 remulcld 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) e. RR )
52 51 recnd 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) e. CC )
53 38 46 mulcld 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( Lam ` m ) x. ( ( x / n ) / m ) ) e. CC )
54 50 52 53 fsumsub 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) - ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) = ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) )
55 49 54 eqtrd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( R ` ( ( x / n ) / m ) ) ) = ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) )
56 55 oveq2d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( R ` ( ( x / n ) / m ) ) ) ) = ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( psi ` ( ( x / n ) / m ) ) ) - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) ) )
57 vmacl 
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
58 25 57 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. RR )
59 58 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. CC )
60 50 51 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 )
61 60 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 )
62 50 53 fsumcl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) e. CC )
63 59 61 62 subdid 
 |-  ( ( ( 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 ) ) ) - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) ) = ( ( ( Lam ` n ) x. 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. ( ( x / n ) / m ) ) ) ) )
64 56 63 eqtrd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( R ` ( ( x / n ) / m ) ) ) ) = ( ( ( Lam ` n ) x. 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. ( ( x / n ) / m ) ) ) ) )
65 64 sumeq2dv 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( R ` ( ( x / n ) / m ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. 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. ( ( x / n ) / m ) ) ) ) )
66 fzfid 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
67 58 60 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 )
68 67 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 )
69 59 62 mulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) e. CC )
70 66 68 69 fsumsub 
 |-  ( ( 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 ) ) ) ) - ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 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. ( ( x / n ) / m ) ) ) ) )
71 65 70 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( R ` ( ( x / n ) / m ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 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. ( ( x / n ) / m ) ) ) ) )
72 71 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. ( R ` ( ( x / n ) / 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 ) ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) ) ) )
73 2re 
 |-  2 e. RR
74 73 a1i 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 e. RR )
75 3 9 rplogcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ )
76 74 75 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 / ( log ` x ) ) e. RR )
77 76 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 / ( log ` x ) ) e. CC )
78 66 67 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 )
79 78 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 )
80 66 69 fsumcl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) e. CC )
81 77 79 80 subdid 
 |-  ( ( 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 ) ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / 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 ) ) ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) ) ) )
82 72 81 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. ( R ` ( ( x / n ) / 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 ) ) ) ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) ) ) )
83 22 82 oveq12d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( R ` 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. ( R ` ( ( x / n ) / m ) ) ) ) ) ) = ( ( ( ( psi ` x ) x. ( log ` x ) ) - ( 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. ( ( x / n ) / m ) ) ) ) ) ) )
84 16 19 remulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( psi ` x ) x. ( log ` x ) ) e. RR )
85 84 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( psi ` x ) x. ( log ` x ) ) e. CC )
86 18 20 mulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) e. CC )
87 76 78 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 )
88 87 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 )
89 77 80 mulcld 
 |-  ( ( 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. ( ( x / n ) / m ) ) ) ) e. CC )
90 85 86 88 89 sub4d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( psi ` x ) x. ( log ` x ) ) - ( 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. ( ( 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. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) - ( ( 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. ( ( x / n ) / m ) ) ) ) ) ) )
91 83 90 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( R ` 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. ( R ` ( ( 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. ( psi ` ( ( x / n ) / m ) ) ) ) ) ) - ( ( 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. ( ( x / n ) / m ) ) ) ) ) ) )
92 91 oveq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( R ` 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. ( R ` ( ( x / n ) / m ) ) ) ) ) ) / 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. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) ) ) ) / x ) )
93 84 87 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 )
94 93 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 ) ) ) ) ) ) e. CC )
95 3 19 remulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) e. RR )
96 37 42 remulcld 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( Lam ` m ) x. ( ( x / n ) / m ) ) e. RR )
97 50 96 fsumrecl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) e. RR )
98 58 97 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) e. RR )
99 66 98 fsumrecl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) e. RR )
100 76 99 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. ( ( x / n ) / m ) ) ) ) e. RR )
101 95 100 resubcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 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. ( ( x / n ) / m ) ) ) ) ) e. RR )
102 101 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 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. ( ( x / n ) / m ) ) ) ) ) e. CC )
103 11 rpne0d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x =/= 0 )
104 94 102 18 103 divsubdird 
 |-  ( ( 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 x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) ) ) ) / 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 x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) ) ) / x ) ) )
105 95 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) e. CC )
106 99 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) e. CC )
107 77 106 mulcld 
 |-  ( ( 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. ( ( x / n ) / m ) ) ) ) e. CC )
108 105 107 18 103 divsubdird 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 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. ( ( x / n ) / m ) ) ) ) ) / x ) = ( ( ( x x. ( log ` x ) ) / x ) - ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) ) / x ) ) )
109 20 18 103 divcan3d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( x x. ( log ` x ) ) / x ) = ( log ` x ) )
110 77 106 18 103 divassd 
 |-  ( ( 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. ( ( 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. ( ( x / n ) / m ) ) ) / x ) ) )
111 98 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) e. CC )
112 66 18 111 103 fsumdivc 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) / x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) / x ) )
113 41 recnd 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( x / n ) e. CC )
114 30 nncnd 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. CC )
115 30 nnne0d 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m =/= 0 )
116 113 38 114 115 div12d 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( x / n ) x. ( ( Lam ` m ) / m ) ) = ( ( Lam ` m ) x. ( ( x / n ) / m ) ) )
117 18 adantr 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. CC )
118 117 adantr 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> x e. CC )
119 25 nncnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
120 119 adantr 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> n e. CC )
121 37 30 nndivred 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( Lam ` m ) / m ) e. RR )
122 121 recnd 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( Lam ` m ) / m ) e. CC )
123 25 nnne0d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n =/= 0 )
124 123 adantr 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> n =/= 0 )
125 118 120 122 124 div32d 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( x / n ) x. ( ( Lam ` m ) / m ) ) = ( x x. ( ( ( Lam ` m ) / m ) / n ) ) )
126 116 125 eqtr3d 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( Lam ` m ) x. ( ( x / n ) / m ) ) = ( x x. ( ( ( Lam ` m ) / m ) / n ) ) )
127 126 oveq1d 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( ( Lam ` m ) x. ( ( x / n ) / m ) ) / x ) = ( ( x x. ( ( ( Lam ` m ) / m ) / n ) ) / x ) )
128 25 adantr 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> n e. NN )
129 121 128 nndivred 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( ( Lam ` m ) / m ) / n ) e. RR )
130 129 recnd 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( ( Lam ` m ) / m ) / n ) e. CC )
131 103 adantr 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x =/= 0 )
132 131 adantr 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> x =/= 0 )
133 130 118 132 divcan3d 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( x x. ( ( ( Lam ` m ) / m ) / n ) ) / x ) = ( ( ( Lam ` m ) / m ) / n ) )
134 127 133 eqtrd 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( ( Lam ` m ) x. ( ( x / n ) / m ) ) / x ) = ( ( ( Lam ` m ) / m ) / n ) )
135 134 sumeq2dv 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( ( Lam ` m ) x. ( ( x / n ) / m ) ) / x ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( ( Lam ` m ) / m ) / n ) )
136 96 recnd 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( Lam ` m ) x. ( ( x / n ) / m ) ) e. CC )
137 50 117 136 131 fsumdivc 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) / x ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( ( Lam ` m ) x. ( ( x / n ) / m ) ) / x ) )
138 50 119 122 123 fsumdivc 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) / n ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( ( Lam ` m ) / m ) / n ) )
139 135 137 138 3eqtr4d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) / x ) = ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) / n ) )
140 139 oveq2d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) / x ) ) = ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) / n ) ) )
141 97 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) e. CC )
142 59 141 117 131 divassd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) / x ) = ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) / x ) ) )
143 50 121 fsumrecl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) e. RR )
144 143 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) e. CC )
145 59 119 144 123 div32d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) = ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) / n ) ) )
146 140 142 145 3eqtr4d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) / x ) = ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) )
147 146 sumeq2dv 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) / x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) )
148 112 147 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) / x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) )
149 148 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. ( ( x / n ) / m ) ) ) / x ) ) = ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) ) )
150 110 149 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. ( ( x / n ) / m ) ) ) ) / x ) = ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) ) )
151 109 150 oveq12d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( x x. ( log ` x ) ) / x ) - ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) ) / x ) ) = ( ( log ` x ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) ) ) )
152 108 151 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 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. ( ( x / n ) / m ) ) ) ) ) / x ) = ( ( log ` x ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) ) ) )
153 152 oveq2d 
 |-  ( ( 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 ) - ( ( ( 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. ( ( x / n ) / m ) ) ) ) ) / 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 ) - ( ( log ` x ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) ) ) ) )
154 94 18 103 divcld 
 |-  ( ( 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 )
155 58 25 nndivred 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. RR )
156 155 143 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) e. RR )
157 66 156 fsumrecl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) e. RR )
158 76 157 remulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) ) e. RR )
159 158 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) ) e. CC )
160 154 20 159 subsub2d 
 |-  ( ( 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 ) - ( ( log ` x ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / 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 ) ) ) ) ) ) / x ) + ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) ) - ( log ` x ) ) ) )
161 153 160 eqtrd 
 |-  ( ( 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 ) - ( ( ( 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. ( ( x / n ) / m ) ) ) ) ) / 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 ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) ) - ( log ` x ) ) ) )
162 104 161 eqtrd 
 |-  ( ( 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 x. ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( ( x / n ) / m ) ) ) ) ) ) / 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 ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) ) - ( log ` x ) ) ) )
163 92 162 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( R ` 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. ( R ` ( ( x / n ) / m ) ) ) ) ) ) / 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 ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) ) - ( log ` x ) ) ) )
164 163 mpteq2dva 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( R ` 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. ( R ` ( ( x / n ) / m ) ) ) ) ) ) / x ) ) = ( 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 ) + ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) ) - ( log ` x ) ) ) ) )
165 93 11 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 )
166 158 19 resubcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) ) - ( log ` x ) ) e. RR )
167 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)
168 167 a1i 
 |-  ( 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) )
169 2cnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 e. CC )
170 157 75 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) e. RR )
171 170 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) e. CC )
172 19 rehalfcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / 2 ) e. RR )
173 172 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / 2 ) e. CC )
174 169 171 173 subdid 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) = ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) ) - ( 2 x. ( ( log ` x ) / 2 ) ) ) )
175 157 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) e. CC )
176 75 rpne0d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) =/= 0 )
177 169 20 175 176 div32d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) ) = ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) ) )
178 177 eqcomd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) ) = ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) ) )
179 2ne0 
 |-  2 =/= 0
180 179 a1i 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 =/= 0 )
181 20 169 180 divcan2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( ( log ` x ) / 2 ) ) = ( log ` x ) )
182 178 181 oveq12d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) ) - ( 2 x. ( ( log ` x ) / 2 ) ) ) = ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) ) - ( log ` x ) ) )
183 174 182 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) = ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) ) - ( log ` x ) ) )
184 183 mpteq2dva 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( 2 x. ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) ) - ( log ` x ) ) ) )
185 170 172 resubcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) e. RR )
186 ioossre 
 |-  ( 1 (,) +oo ) C_ RR
187 2cnd 
 |-  ( T. -> 2 e. CC )
188 o1const 
 |-  ( ( ( 1 (,) +oo ) C_ RR /\ 2 e. CC ) -> ( x e. ( 1 (,) +oo ) |-> 2 ) e. O(1) )
189 186 187 188 sylancr 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> 2 ) e. O(1) )
190 2vmadivsum 
 |-  ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1)
191 190 a1i 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1) )
192 74 185 189 191 o1mul2 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( 2 x. ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) ) e. O(1) )
193 184 192 eqeltrrd 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) ) - ( log ` x ) ) ) e. O(1) )
194 165 166 168 193 o1add2 
 |-  ( 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 ) + ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) ) - ( log ` x ) ) ) ) e. O(1) )
195 164 194 eqeltrd 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( R ` 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. ( R ` ( ( x / n ) / m ) ) ) ) ) ) / x ) ) e. O(1) )
196 195 mptru 
 |-  ( x e. ( 1 (,) +oo ) |-> ( ( ( ( R ` 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. ( R ` ( ( x / n ) / m ) ) ) ) ) ) / x ) ) e. O(1)