Metamath Proof Explorer

Theorem selberg3r

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

Ref Expression
Hypothesis pntrval.r 
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
Assertion selberg3r 
|- ( x e. ( 1 (,) +oo ) |-> ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / 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 11 relogcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR )
13 12 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
14 13 2timesd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( log ` x ) ) = ( ( log ` x ) + ( log ` x ) ) )
15 14 oveq2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) = ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) - ( ( log ` x ) + ( log ` x ) ) ) )
16 chpcl 
 |-  ( x e. RR -> ( psi ` x ) e. RR )
17 3 16 syl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( psi ` x ) e. RR )
18 17 12 remulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( psi ` x ) x. ( log ` x ) ) e. RR )
19 2re 
 |-  2 e. RR
20 19 a1i 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 e. RR )
21 3 9 rplogcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ )
22 20 21 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 / ( log ` x ) ) e. RR )
23 fzfid 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
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 vmacl 
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
27 25 26 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. RR )
28 3 adantr 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR )
29 28 25 nndivred 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR )
30 chpcl 
 |-  ( ( x / n ) e. RR -> ( psi ` ( x / n ) ) e. RR )
31 29 30 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( x / n ) ) e. RR )
32 27 31 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) e. RR )
33 25 nnrpd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
34 33 relogcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. RR )
35 32 34 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) e. RR )
36 23 35 fsumrecl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) e. RR )
37 22 36 remulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) e. RR )
38 18 37 readdcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) e. RR )
39 38 11 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) e. RR )
40 39 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) e. CC )
41 40 13 13 subsub4d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) - ( log ` x ) ) - ( log ` x ) ) = ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) - ( ( log ` x ) + ( log ` x ) ) ) )
42 15 41 eqtr4d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) = ( ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) - ( log ` x ) ) - ( log ` x ) ) )
43 42 oveq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) - ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) - ( log ` x ) ) ) = ( ( ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) - ( log ` x ) ) - ( log ` x ) ) - ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) - ( log ` x ) ) ) )
44 40 13 subcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) - ( log ` x ) ) e. CC )
45 2cn 
 |-  2 e. CC
46 45 a1i 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 e. CC )
47 21 rpne0d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) =/= 0 )
48 46 13 47 divcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 / ( log ` x ) ) e. CC )
49 27 25 nndivred 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. RR )
50 49 34 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) e. RR )
51 23 50 fsumrecl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) e. RR )
52 51 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) e. CC )
53 48 52 mulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) e. CC )
54 44 53 13 nnncan2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) - ( log ` x ) ) - ( log ` x ) ) - ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) - ( log ` x ) ) ) = ( ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) - ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) )
55 1 pntrf 
 |-  R : RR+ --> RR
56 55 ffvelcdmi 
 |-  ( x e. RR+ -> ( R ` x ) e. RR )
57 11 56 syl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` x ) e. RR )
58 57 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` x ) e. CC )
59 58 13 mulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( R ` x ) x. ( log ` x ) ) e. CC )
60 37 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) e. CC )
61 59 60 addcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) e. CC )
62 3 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. CC )
63 62 53 mulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) e. CC )
64 11 rpne0d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x =/= 0 )
65 61 63 62 64 divsubdird 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) - ( x x. ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) ) / x ) = ( ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) - ( ( x x. ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) / x ) ) )
66 59 60 63 addsubassd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) - ( x x. ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) ) = ( ( ( R ` x ) x. ( log ` x ) ) + ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( x x. ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) ) ) )
67 36 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) e. CC )
68 62 52 mulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) e. CC )
69 48 67 68 subdid 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) - ( x x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) ) = ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( ( 2 / ( log ` x ) ) x. ( x x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) ) )
70 50 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) e. CC )
71 23 62 70 fsummulc2 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( x x. ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) )
72 71 oveq2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) - ( x x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( x x. ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) )
73 35 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) e. CC )
74 62 adantr 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. CC )
75 74 70 mulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x x. ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) e. CC )
76 23 73 75 fsumsub 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) - ( x x. ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( x x. ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) )
77 72 76 eqtr4d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) - ( x x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) - ( x x. ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) )
78 27 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. CC )
79 31 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( x / n ) ) e. CC )
80 34 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. CC )
81 78 79 80 mul32d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) = ( ( ( Lam ` n ) x. ( log ` n ) ) x. ( psi ` ( x / n ) ) ) )
82 25 nncnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
83 25 nnne0d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n =/= 0 )
84 78 80 82 83 div23d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) x. ( log ` n ) ) / n ) = ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) )
85 84 oveq2d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x x. ( ( ( Lam ` n ) x. ( log ` n ) ) / n ) ) = ( x x. ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) )
86 78 80 mulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( log ` n ) ) e. CC )
87 74 86 82 83 div12d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x x. ( ( ( Lam ` n ) x. ( log ` n ) ) / n ) ) = ( ( ( Lam ` n ) x. ( log ` n ) ) x. ( x / n ) ) )
88 85 87 eqtr3d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x x. ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) = ( ( ( Lam ` n ) x. ( log ` n ) ) x. ( x / n ) ) )
89 81 88 oveq12d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) - ( x x. ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) = ( ( ( ( Lam ` n ) x. ( log ` n ) ) x. ( psi ` ( x / n ) ) ) - ( ( ( Lam ` n ) x. ( log ` n ) ) x. ( x / n ) ) ) )
90 11 adantr 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR+ )
91 90 33 rpdivcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
92 1 pntrval 
 |-  ( ( x / n ) e. RR+ -> ( R ` ( x / n ) ) = ( ( psi ` ( x / n ) ) - ( x / n ) ) )
93 91 92 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) = ( ( psi ` ( x / n ) ) - ( x / n ) ) )
94 93 oveq2d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) x. ( log ` n ) ) x. ( R ` ( x / n ) ) ) = ( ( ( Lam ` n ) x. ( log ` n ) ) x. ( ( psi ` ( x / n ) ) - ( x / n ) ) ) )
95 29 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. CC )
96 86 79 95 subdid 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) x. ( log ` n ) ) x. ( ( psi ` ( x / n ) ) - ( x / n ) ) ) = ( ( ( ( Lam ` n ) x. ( log ` n ) ) x. ( psi ` ( x / n ) ) ) - ( ( ( Lam ` n ) x. ( log ` n ) ) x. ( x / n ) ) ) )
97 94 96 eqtrd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) x. ( log ` n ) ) x. ( R ` ( x / n ) ) ) = ( ( ( ( Lam ` n ) x. ( log ` n ) ) x. ( psi ` ( x / n ) ) ) - ( ( ( Lam ` n ) x. ( log ` n ) ) x. ( x / n ) ) ) )
98 89 97 eqtr4d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) - ( x x. ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) = ( ( ( Lam ` n ) x. ( log ` n ) ) x. ( R ` ( x / n ) ) ) )
99 55 ffvelcdmi 
 |-  ( ( x / n ) e. RR+ -> ( R ` ( x / n ) ) e. RR )
100 91 99 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. RR )
101 100 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. CC )
102 78 101 80 mul32d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) = ( ( ( Lam ` n ) x. ( log ` n ) ) x. ( R ` ( x / n ) ) ) )
103 98 102 eqtr4d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) - ( x x. ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) = ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) )
104 103 sumeq2dv 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) - ( x x. ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) )
105 77 104 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) - ( x x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) )
106 105 oveq2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) - ( x x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) ) = ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) )
107 48 62 52 mul12d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. ( x x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) = ( x x. ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) )
108 107 oveq2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( ( 2 / ( log ` x ) ) x. ( x x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) ) = ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( x x. ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) ) )
109 69 106 108 3eqtr3rd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( x x. ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) ) = ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) )
110 109 oveq2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( R ` x ) x. ( log ` x ) ) + ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( x x. ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) ) ) = ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) )
111 66 110 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) - ( x x. ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) ) = ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) )
112 111 oveq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) - ( x x. ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) ) / x ) = ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) )
113 1 pntrval 
 |-  ( x e. RR+ -> ( R ` x ) = ( ( psi ` x ) - x ) )
114 11 113 syl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` x ) = ( ( psi ` x ) - x ) )
115 114 oveq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( R ` x ) x. ( log ` x ) ) = ( ( ( psi ` x ) - x ) x. ( log ` x ) ) )
116 17 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( psi ` x ) e. CC )
117 116 62 13 subdird 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( psi ` x ) - x ) x. ( log ` x ) ) = ( ( ( psi ` x ) x. ( log ` x ) ) - ( x x. ( log ` x ) ) ) )
118 115 117 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( R ` x ) x. ( log ` x ) ) = ( ( ( psi ` x ) x. ( log ` x ) ) - ( x x. ( log ` x ) ) ) )
119 118 oveq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) = ( ( ( ( psi ` x ) x. ( log ` x ) ) - ( x x. ( log ` x ) ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) )
120 18 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( psi ` x ) x. ( log ` x ) ) e. CC )
121 62 13 mulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) e. CC )
122 120 60 121 addsubd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) - ( x x. ( log ` x ) ) ) = ( ( ( ( psi ` x ) x. ( log ` x ) ) - ( x x. ( log ` x ) ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) )
123 119 122 eqtr4d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) = ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) - ( x x. ( log ` x ) ) ) )
124 123 oveq1d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) = ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) - ( x x. ( log ` x ) ) ) / x ) )
125 38 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) e. CC )
126 125 121 62 64 divsubdird 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) - ( x x. ( log ` x ) ) ) / x ) = ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) - ( ( x x. ( log ` x ) ) / x ) ) )
127 13 62 64 divcan3d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( x x. ( log ` x ) ) / x ) = ( log ` x ) )
128 127 oveq2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) - ( ( x x. ( log ` x ) ) / x ) ) = ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) - ( log ` x ) ) )
129 126 128 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) - ( x x. ( log ` x ) ) ) / x ) = ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) - ( log ` x ) ) )
130 124 129 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) = ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) - ( log ` x ) ) )
131 53 62 64 divcan3d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( x x. ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) / x ) = ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) )
132 130 131 oveq12d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) - ( ( x x. ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) / x ) ) = ( ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) - ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) )
133 65 112 132 3eqtr3rd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) - ( log ` x ) ) - ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) ) = ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) )
134 43 54 133 3eqtrrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) = ( ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) - ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) - ( log ` x ) ) ) )
135 134 mpteq2dva 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) - ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) - ( log ` x ) ) ) ) )
136 20 12 remulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( log ` x ) ) e. RR )
137 39 136 resubcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) e. RR )
138 22 51 remulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) e. RR )
139 138 12 resubcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) - ( log ` x ) ) e. RR )
140 selberg3 
 |-  ( x e. ( 1 (,) +oo ) |-> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)
141 140 a1i 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1) )
142 20 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 e. CC )
143 51 21 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) e. RR )
144 143 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) e. CC )
145 12 rehalfcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / 2 ) e. RR )
146 145 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) / 2 ) e. CC )
147 142 144 146 subdid 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) = ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) ) - ( 2 x. ( ( log ` x ) / 2 ) ) ) )
148 142 13 52 47 div32d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) = ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) ) )
149 148 eqcomd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) ) = ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) )
150 2ne0 
 |-  2 =/= 0
151 150 a1i 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 2 =/= 0 )
152 13 142 151 divcan2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( ( log ` x ) / 2 ) ) = ( log ` x ) )
153 149 152 oveq12d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) ) - ( 2 x. ( ( log ` x ) / 2 ) ) ) = ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) - ( log ` x ) ) )
154 147 153 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) = ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) - ( log ` x ) ) )
155 154 mpteq2dva 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( 2 x. ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) - ( log ` x ) ) ) )
156 143 145 resubcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) e. RR )
157 ioossre 
 |-  ( 1 (,) +oo ) C_ RR
158 o1const 
 |-  ( ( ( 1 (,) +oo ) C_ RR /\ 2 e. CC ) -> ( x e. ( 1 (,) +oo ) |-> 2 ) e. O(1) )
159 157 45 158 mp2an 
 |-  ( x e. ( 1 (,) +oo ) |-> 2 ) e. O(1)
160 159 a1i 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> 2 ) e. O(1) )
161 vmalogdivsum 
 |-  ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1)
162 161 a1i 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1) )
163 20 156 160 162 o1mul2 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( 2 x. ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) ) e. O(1) )
164 155 163 eqeltrrd 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) - ( log ` x ) ) ) e. O(1) )
165 137 139 141 164 o1sub2 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) - ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( log ` n ) ) ) - ( log ` x ) ) ) ) e. O(1) )
166 135 165 eqeltrd 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) ) e. O(1) )
167 166 mptru 
 |-  ( x e. ( 1 (,) +oo ) |-> ( ( ( ( R ` x ) x. ( log ` x ) ) + ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( R ` ( x / n ) ) ) x. ( log ` n ) ) ) ) / x ) ) e. O(1)