Metamath Proof Explorer

Theorem selberg

Description: Selberg's symmetry formula. The statement has many forms, and this one is equivalent to the statement that sum_ n <_ x , Lam ( n ) log n + sum_ m x. n <_ x , Lam ( m ) Lam ( n ) = 2 x log x + O ( x ) . Equation 10.4.10 of Shapiro, p. 419. (Contributed by Mario Carneiro, 23-May-2016)

Ref Expression
Assertion 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)

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( n = d -> ( Lam ` n ) = ( Lam ` d ) )
2 oveq2 
 |-  ( n = d -> ( x / n ) = ( x / d ) )
3 2 fveq2d 
 |-  ( n = d -> ( psi ` ( x / n ) ) = ( psi ` ( x / d ) ) )
4 1 3 oveq12d 
 |-  ( n = d -> ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) = ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) )
5 4 cbvsumv 
 |-  sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) = sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) )
6 fzfid 
 |-  ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( x / d ) ) ) e. Fin )
7 elfznn 
 |-  ( d e. ( 1 ... ( |_ ` x ) ) -> d e. NN )
8 7 adantl 
 |-  ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. NN )
9 vmacl 
 |-  ( d e. NN -> ( Lam ` d ) e. RR )
10 8 9 syl 
 |-  ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` d ) e. RR )
11 10 recnd 
 |-  ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` d ) e. CC )
12 elfznn 
 |-  ( m e. ( 1 ... ( |_ ` ( x / d ) ) ) -> m e. NN )
13 12 adantl 
 |-  ( ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> m e. NN )
14 vmacl 
 |-  ( m e. NN -> ( Lam ` m ) e. RR )
15 13 14 syl 
 |-  ( ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( Lam ` m ) e. RR )
16 15 recnd 
 |-  ( ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( Lam ` m ) e. CC )
17 6 11 16 fsummulc2 
 |-  ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` d ) x. sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( Lam ` m ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( Lam ` d ) x. ( Lam ` m ) ) )
18 7 nnrpd 
 |-  ( d e. ( 1 ... ( |_ ` x ) ) -> d e. RR+ )
19 rpdivcl 
 |-  ( ( x e. RR+ /\ d e. RR+ ) -> ( x / d ) e. RR+ )
20 18 19 sylan2 
 |-  ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( x / d ) e. RR+ )
21 20 rpred 
 |-  ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( x / d ) e. RR )
22 chpval 
 |-  ( ( x / d ) e. RR -> ( psi ` ( x / d ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( Lam ` m ) )
23 21 22 syl 
 |-  ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( x / d ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( Lam ` m ) )
24 23 oveq2d 
 |-  ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) = ( ( Lam ` d ) x. sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( Lam ` m ) ) )
25 13 nncnd 
 |-  ( ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> m e. CC )
26 7 ad2antlr 
 |-  ( ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> d e. NN )
27 26 nncnd 
 |-  ( ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> d e. CC )
28 26 nnne0d 
 |-  ( ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> d =/= 0 )
29 25 27 28 divcan3d 
 |-  ( ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( d x. m ) / d ) = m )
30 29 fveq2d 
 |-  ( ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( Lam ` ( ( d x. m ) / d ) ) = ( Lam ` m ) )
31 30 oveq2d 
 |-  ( ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( Lam ` d ) x. ( Lam ` ( ( d x. m ) / d ) ) ) = ( ( Lam ` d ) x. ( Lam ` m ) ) )
32 31 sumeq2dv 
 |-  ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( Lam ` d ) x. ( Lam ` ( ( d x. m ) / d ) ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( Lam ` d ) x. ( Lam ` m ) ) )
33 17 24 32 3eqtr4d 
 |-  ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( Lam ` d ) x. ( Lam ` ( ( d x. m ) / d ) ) ) )
34 33 sumeq2dv 
 |-  ( x e. RR+ -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` d ) x. ( psi ` ( x / d ) ) ) = sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( Lam ` d ) x. ( Lam ` ( ( d x. m ) / d ) ) ) )
35 5 34 syl5eq 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) = sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( Lam ` d ) x. ( Lam ` ( ( d x. m ) / d ) ) ) )
36 fvoveq1 
 |-  ( n = ( d x. m ) -> ( Lam ` ( n / d ) ) = ( Lam ` ( ( d x. m ) / d ) ) )
37 36 oveq2d 
 |-  ( n = ( d x. m ) -> ( ( Lam ` d ) x. ( Lam ` ( n / d ) ) ) = ( ( Lam ` d ) x. ( Lam ` ( ( d x. m ) / d ) ) ) )
38 rpre 
 |-  ( x e. RR+ -> x e. RR )
39 ssrab2 
 |-  { y e. NN | y || n } C_ NN
40 simprr 
 |-  ( ( x e. RR+ /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> d e. { y e. NN | y || n } )
41 39 40 sselid 
 |-  ( ( x e. RR+ /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> d e. NN )
42 41 anassrs 
 |-  ( ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ d e. { y e. NN | y || n } ) -> d e. NN )
43 42 9 syl 
 |-  ( ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ d e. { y e. NN | y || n } ) -> ( Lam ` d ) e. RR )
44 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
45 44 adantl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
46 dvdsdivcl 
 |-  ( ( n e. NN /\ d e. { y e. NN | y || n } ) -> ( n / d ) e. { y e. NN | y || n } )
47 45 46 sylan 
 |-  ( ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ d e. { y e. NN | y || n } ) -> ( n / d ) e. { y e. NN | y || n } )
48 39 47 sselid 
 |-  ( ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ d e. { y e. NN | y || n } ) -> ( n / d ) e. NN )
49 vmacl 
 |-  ( ( n / d ) e. NN -> ( Lam ` ( n / d ) ) e. RR )
50 48 49 syl 
 |-  ( ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ d e. { y e. NN | y || n } ) -> ( Lam ` ( n / d ) ) e. RR )
51 43 50 remulcld 
 |-  ( ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ d e. { y e. NN | y || n } ) -> ( ( Lam ` d ) x. ( Lam ` ( n / d ) ) ) e. RR )
52 51 recnd 
 |-  ( ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ d e. { y e. NN | y || n } ) -> ( ( Lam ` d ) x. ( Lam ` ( n / d ) ) ) e. CC )
53 52 anasss 
 |-  ( ( x e. RR+ /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> ( ( Lam ` d ) x. ( Lam ` ( n / d ) ) ) e. CC )
54 37 38 53 dvdsflsumcom 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ d e. { y e. NN | y || n } ( ( Lam ` d ) x. ( Lam ` ( n / d ) ) ) = sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( Lam ` d ) x. ( Lam ` ( ( d x. m ) / d ) ) ) )
55 35 54 eqtr4d 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ d e. { y e. NN | y || n } ( ( Lam ` d ) x. ( Lam ` ( n / d ) ) ) )
56 55 oveq1d 
 |-  ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ d e. { y e. NN | y || n } ( ( Lam ` d ) x. ( Lam ` ( n / d ) ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) ) )
57 fzfid 
 |-  ( x e. RR+ -> ( 1 ... ( |_ ` x ) ) e. Fin )
58 vmacl 
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
59 45 58 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. RR )
60 59 recnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. CC )
61 44 nnrpd 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. RR+ )
62 rpdivcl 
 |-  ( ( x e. RR+ /\ n e. RR+ ) -> ( x / n ) e. RR+ )
63 61 62 sylan2 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
64 63 rpred 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR )
65 chpcl 
 |-  ( ( x / n ) e. RR -> ( psi ` ( x / n ) ) e. RR )
66 64 65 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( x / n ) ) e. RR )
67 66 recnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( x / n ) ) e. CC )
68 60 67 mulcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) e. CC )
69 45 nnrpd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
70 relogcl 
 |-  ( n e. RR+ -> ( log ` n ) e. RR )
71 69 70 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. RR )
72 71 recnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. CC )
73 60 72 mulcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( log ` n ) ) e. CC )
74 57 68 73 fsumadd 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) + ( ( 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 ) ) ) )
75 fzfid 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... n ) e. Fin )
76 dvdsssfz1 
 |-  ( n e. NN -> { y e. NN | y || n } C_ ( 1 ... n ) )
77 45 76 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> { y e. NN | y || n } C_ ( 1 ... n ) )
78 75 77 ssfid 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> { y e. NN | y || n } e. Fin )
79 78 51 fsumrecl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ d e. { y e. NN | y || n } ( ( Lam ` d ) x. ( Lam ` ( n / d ) ) ) e. RR )
80 79 recnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ d e. { y e. NN | y || n } ( ( Lam ` d ) x. ( Lam ` ( n / d ) ) ) e. CC )
81 57 80 73 fsumadd 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( sum_ d e. { y e. NN | y || n } ( ( Lam ` d ) x. ( Lam ` ( n / d ) ) ) + ( ( Lam ` n ) x. ( log ` n ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ d e. { y e. NN | y || n } ( ( Lam ` d ) x. ( Lam ` ( n / d ) ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) ) )
82 56 74 81 3eqtr4d 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) + ( ( Lam ` n ) x. ( log ` n ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( sum_ d e. { y e. NN | y || n } ( ( Lam ` d ) x. ( Lam ` ( n / d ) ) ) + ( ( Lam ` n ) x. ( log ` n ) ) ) )
83 72 67 addcomd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` n ) + ( psi ` ( x / n ) ) ) = ( ( psi ` ( x / n ) ) + ( log ` n ) ) )
84 83 oveq2d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) = ( ( Lam ` n ) x. ( ( psi ` ( x / n ) ) + ( log ` n ) ) ) )
85 60 67 72 adddid 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( ( psi ` ( x / n ) ) + ( log ` n ) ) ) = ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) + ( ( Lam ` n ) x. ( log ` n ) ) ) )
86 84 85 eqtrd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) = ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) + ( ( Lam ` n ) x. ( log ` n ) ) ) )
87 86 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. ( psi ` ( x / n ) ) ) + ( ( Lam ` n ) x. ( log ` n ) ) ) )
88 logsqvma2 
 |-  ( n e. NN -> sum_ d e. { y e. NN | y || n } ( ( mmu ` d ) x. ( ( log ` ( n / d ) ) ^ 2 ) ) = ( sum_ d e. { y e. NN | y || n } ( ( Lam ` d ) x. ( Lam ` ( n / d ) ) ) + ( ( Lam ` n ) x. ( log ` n ) ) ) )
89 45 88 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ d e. { y e. NN | y || n } ( ( mmu ` d ) x. ( ( log ` ( n / d ) ) ^ 2 ) ) = ( sum_ d e. { y e. NN | y || n } ( ( Lam ` d ) x. ( Lam ` ( n / d ) ) ) + ( ( Lam ` n ) x. ( log ` n ) ) ) )
90 89 sumeq2dv 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ d e. { y e. NN | y || n } ( ( mmu ` d ) x. ( ( log ` ( n / d ) ) ^ 2 ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( sum_ d e. { y e. NN | y || n } ( ( Lam ` d ) x. ( Lam ` ( n / d ) ) ) + ( ( Lam ` n ) x. ( log ` n ) ) ) )
91 82 87 90 3eqtr4d 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ d e. { y e. NN | y || n } ( ( mmu ` d ) x. ( ( log ` ( n / d ) ) ^ 2 ) ) )
92 fvoveq1 
 |-  ( n = ( d x. m ) -> ( log ` ( n / d ) ) = ( log ` ( ( d x. m ) / d ) ) )
93 92 oveq1d 
 |-  ( n = ( d x. m ) -> ( ( log ` ( n / d ) ) ^ 2 ) = ( ( log ` ( ( d x. m ) / d ) ) ^ 2 ) )
94 93 oveq2d 
 |-  ( n = ( d x. m ) -> ( ( mmu ` d ) x. ( ( log ` ( n / d ) ) ^ 2 ) ) = ( ( mmu ` d ) x. ( ( log ` ( ( d x. m ) / d ) ) ^ 2 ) ) )
95 mucl 
 |-  ( d e. NN -> ( mmu ` d ) e. ZZ )
96 41 95 syl 
 |-  ( ( x e. RR+ /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> ( mmu ` d ) e. ZZ )
97 96 zcnd 
 |-  ( ( x e. RR+ /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> ( mmu ` d ) e. CC )
98 61 ad2antrl 
 |-  ( ( x e. RR+ /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> n e. RR+ )
99 41 nnrpd 
 |-  ( ( x e. RR+ /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> d e. RR+ )
100 98 99 rpdivcld 
 |-  ( ( x e. RR+ /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> ( n / d ) e. RR+ )
101 relogcl 
 |-  ( ( n / d ) e. RR+ -> ( log ` ( n / d ) ) e. RR )
102 101 recnd 
 |-  ( ( n / d ) e. RR+ -> ( log ` ( n / d ) ) e. CC )
103 100 102 syl 
 |-  ( ( x e. RR+ /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> ( log ` ( n / d ) ) e. CC )
104 103 sqcld 
 |-  ( ( x e. RR+ /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> ( ( log ` ( n / d ) ) ^ 2 ) e. CC )
105 97 104 mulcld 
 |-  ( ( x e. RR+ /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> ( ( mmu ` d ) x. ( ( log ` ( n / d ) ) ^ 2 ) ) e. CC )
106 94 38 105 dvdsflsumcom 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ d e. { y e. NN | y || n } ( ( mmu ` d ) x. ( ( log ` ( n / d ) ) ^ 2 ) ) = sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( mmu ` d ) x. ( ( log ` ( ( d x. m ) / d ) ) ^ 2 ) ) )
107 29 fveq2d 
 |-  ( ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( log ` ( ( d x. m ) / d ) ) = ( log ` m ) )
108 107 oveq1d 
 |-  ( ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( log ` ( ( d x. m ) / d ) ) ^ 2 ) = ( ( log ` m ) ^ 2 ) )
109 108 oveq2d 
 |-  ( ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( mmu ` d ) x. ( ( log ` ( ( d x. m ) / d ) ) ^ 2 ) ) = ( ( mmu ` d ) x. ( ( log ` m ) ^ 2 ) ) )
110 109 sumeq2dv 
 |-  ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( mmu ` d ) x. ( ( log ` ( ( d x. m ) / d ) ) ^ 2 ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( mmu ` d ) x. ( ( log ` m ) ^ 2 ) ) )
111 110 sumeq2dv 
 |-  ( x e. RR+ -> sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( mmu ` d ) x. ( ( log ` ( ( d x. m ) / d ) ) ^ 2 ) ) = sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( mmu ` d ) x. ( ( log ` m ) ^ 2 ) ) )
112 91 106 111 3eqtrd 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) = sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( mmu ` d ) x. ( ( log ` m ) ^ 2 ) ) )
113 112 oveq1d 
 |-  ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) = ( sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( mmu ` d ) x. ( ( log ` m ) ^ 2 ) ) / x ) )
114 113 oveq1d 
 |-  ( x e. RR+ -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) = ( ( sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( mmu ` d ) x. ( ( log ` m ) ^ 2 ) ) / x ) - ( 2 x. ( log ` x ) ) ) )
115 114 mpteq2ia 
 |-  ( 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_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( mmu ` d ) x. ( ( log ` m ) ^ 2 ) ) / x ) - ( 2 x. ( log ` x ) ) ) )
116 eqid 
 |-  ( ( ( ( log ` ( x / d ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / d ) ) ) ) ) / d ) = ( ( ( ( log ` ( x / d ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / d ) ) ) ) ) / d )
117 116 selberglem2 
 |-  ( x e. RR+ |-> ( ( sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( mmu ` d ) x. ( ( log ` m ) ^ 2 ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)
118 115 117 eqeltri 
 |-  ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)