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 ${⊢}\left({x}\in {ℝ}^{+}⟼\left(\frac{\sum _{{n}=1}^{⌊{x}⌋}\Lambda \left({n}\right)\left(\mathrm{log}{n}+\psi \left(\frac{{x}}{{n}}\right)\right)}{{x}}\right)-2\mathrm{log}{x}\right)\in 𝑂\left(1\right)$

Proof

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