# 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 )`
` |-  ( ( 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 )`
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 )`
` |-  ( 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 ) ) ) )`
` |-  ( 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)`