Metamath Proof Explorer

Theorem selberg2

Description: Selberg's symmetry formula, using the second Chebyshev function. Equation 10.4.14 of Shapiro, p. 420. (Contributed by Mario Carneiro, 23-May-2016)

Ref Expression
Assertion selberg2 
|- ( x e. RR+ |-> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)

Proof

Step Hyp Ref Expression
1 reex 
 |-  RR e. _V
2 rpssre 
 |-  RR+ C_ RR
3 1 2 ssexi 
 |-  RR+ e. _V
4 3 a1i 
 |-  ( T. -> RR+ e. _V )
5 ovexd 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) e. _V )
6 ovexd 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) e. _V )
7 eqidd 
 |-  ( T. -> ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) = ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) )
8 eqidd 
 |-  ( T. -> ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) ) = ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) ) )
9 4 5 6 7 8 offval2 
 |-  ( T. -> ( ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) oF - ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) ) ) = ( x e. RR+ |-> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) ) ) )
10 9 mptru 
 |-  ( ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) oF - ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) ) ) = ( x e. RR+ |-> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) ) )
11 fzfid 
 |-  ( x e. RR+ -> ( 1 ... ( |_ ` x ) ) e. Fin )
12 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
13 12 adantl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
14 vmacl 
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
15 13 14 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. RR )
16 15 recnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. CC )
17 13 nnrpd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
18 relogcl 
 |-  ( n e. RR+ -> ( log ` n ) e. RR )
19 17 18 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. RR )
20 19 recnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. CC )
21 rpre 
 |-  ( x e. RR+ -> x e. RR )
22 nndivre 
 |-  ( ( x e. RR /\ n e. NN ) -> ( x / n ) e. RR )
23 21 12 22 syl2an 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR )
24 chpcl 
 |-  ( ( x / n ) e. RR -> ( psi ` ( x / n ) ) e. RR )
25 23 24 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( x / n ) ) e. RR )
26 25 recnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( x / n ) ) e. CC )
27 20 26 addcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` n ) + ( psi ` ( x / n ) ) ) e. CC )
28 16 27 mulcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) e. CC )
29 11 28 fsumcl 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) e. CC )
30 rpcn 
 |-  ( x e. RR+ -> x e. CC )
31 rpne0 
 |-  ( x e. RR+ -> x =/= 0 )
32 29 30 31 divcld 
 |-  ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) e. CC )
33 2cn 
 |-  2 e. CC
34 relogcl 
 |-  ( x e. RR+ -> ( log ` x ) e. RR )
35 34 recnd 
 |-  ( x e. RR+ -> ( log ` x ) e. CC )
36 mulcl 
 |-  ( ( 2 e. CC /\ ( log ` x ) e. CC ) -> ( 2 x. ( log ` x ) ) e. CC )
37 33 35 36 sylancr 
 |-  ( x e. RR+ -> ( 2 x. ( log ` x ) ) e. CC )
38 16 20 mulcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( log ` n ) ) e. CC )
39 11 38 fsumcl 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) e. CC )
40 chpcl 
 |-  ( x e. RR -> ( psi ` x ) e. RR )
41 21 40 syl 
 |-  ( x e. RR+ -> ( psi ` x ) e. RR )
42 41 recnd 
 |-  ( x e. RR+ -> ( psi ` x ) e. CC )
43 42 35 mulcld 
 |-  ( x e. RR+ -> ( ( psi ` x ) x. ( log ` x ) ) e. CC )
44 39 43 subcld 
 |-  ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) e. CC )
45 44 30 31 divcld 
 |-  ( x e. RR+ -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) e. CC )
46 32 37 45 sub32d 
 |-  ( x e. RR+ -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) ) = ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) ) - ( 2 x. ( log ` x ) ) ) )
47 rpcnne0 
 |-  ( x e. RR+ -> ( x e. CC /\ x =/= 0 ) )
48 divsubdir 
 |-  ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) e. CC /\ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) e. CC /\ ( x e. CC /\ x =/= 0 ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) ) / x ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) ) )
49 29 44 47 48 syl3anc 
 |-  ( x e. RR+ -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) ) / x ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) ) )
50 16 20 26 adddid 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) = ( ( ( Lam ` n ) x. ( log ` n ) ) + ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) )
51 50 sumeq2dv 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( log ` n ) ) + ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) )
52 16 26 mulcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) e. CC )
53 11 38 52 fsumadd 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( log ` n ) ) + ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) )
54 51 53 eqtrd 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) )
55 54 oveq1d 
 |-  ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) ) )
56 11 52 fsumcl 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) e. CC )
57 39 56 43 pnncand 
 |-  ( x e. RR+ -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) )
58 56 43 addcomd 
 |-  ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) + ( ( psi ` x ) x. ( log ` x ) ) ) = ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) )
59 55 57 58 3eqtrd 
 |-  ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) ) = ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) )
60 59 oveq1d 
 |-  ( x e. RR+ -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) ) / x ) = ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) )
61 49 60 eqtr3d 
 |-  ( x e. RR+ -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) ) = ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) )
62 61 oveq1d 
 |-  ( x e. RR+ -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) ) - ( 2 x. ( log ` x ) ) ) = ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) )
63 46 62 eqtrd 
 |-  ( x e. RR+ -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) ) = ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) )
64 63 mpteq2ia 
 |-  ( x e. RR+ |-> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) ) ) = ( x e. RR+ |-> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) )
65 10 64 eqtri 
 |-  ( ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) oF - ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) ) ) = ( x e. RR+ |-> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) )
66 selberg 
 |-  ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)
67 selberg2lem 
 |-  ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) ) e. O(1)
68 o1sub 
 |-  ( ( ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1) /\ ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) ) e. O(1) ) -> ( ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) oF - ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) ) ) e. O(1) )
69 66 67 68 mp2an 
 |-  ( ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) oF - ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) ) ) e. O(1)
70 65 69 eqeltrri 
 |-  ( x e. RR+ |-> ( ( ( ( ( psi ` x ) x. ( log ` x ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)