Metamath Proof Explorer


Theorem selberg3

Description: Introduce a log weighting on the summands of sum_ m x. n <_ x , Lam ( m ) Lam ( n ) , the core of selberg2 (written here as sum_ n <_ x , Lam ( n ) psi ( x / n ) ). Equation 10.6.7 of Shapiro, p. 422. (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Assertion selberg3 x1+∞ψxlogx+2logxn=1xΛnψxnlognx2logx𝑂1

Proof

Step Hyp Ref Expression
1 elioore x1+∞x
2 1 adantl x1+∞x
3 chpcl xψx
4 2 3 syl x1+∞ψx
5 1rp 1+
6 5 a1i x1+∞1+
7 1red x1+∞1
8 eliooord x1+∞1<xx<+∞
9 8 adantl x1+∞1<xx<+∞
10 9 simpld x1+∞1<x
11 7 2 10 ltled x1+∞1x
12 2 6 11 rpgecld x1+∞x+
13 12 relogcld x1+∞logx
14 4 13 remulcld x1+∞ψxlogx
15 14 recnd x1+∞ψxlogx
16 fzfid x1+∞1xFin
17 elfznn n1xn
18 17 adantl x1+∞n1xn
19 vmacl nΛn
20 18 19 syl x1+∞n1xΛn
21 2 adantr x1+∞n1xx
22 21 18 nndivred x1+∞n1xxn
23 chpcl xnψxn
24 22 23 syl x1+∞n1xψxn
25 20 24 remulcld x1+∞n1xΛnψxn
26 16 25 fsumrecl x1+∞n=1xΛnψxn
27 26 recnd x1+∞n=1xΛnψxn
28 2re 2
29 28 a1i x1+∞2
30 2 10 rplogcld x1+∞logx+
31 29 30 rerpdivcld x1+∞2logx
32 18 nnrpd x1+∞n1xn+
33 32 relogcld x1+∞n1xlogn
34 25 33 remulcld x1+∞n1xΛnψxnlogn
35 16 34 fsumrecl x1+∞n=1xΛnψxnlogn
36 31 35 remulcld x1+∞2logxn=1xΛnψxnlogn
37 36 26 resubcld x1+∞2logxn=1xΛnψxnlognn=1xΛnψxn
38 37 recnd x1+∞2logxn=1xΛnψxnlognn=1xΛnψxn
39 15 27 38 addassd x1+∞ψxlogx+n=1xΛnψxn+2logxn=1xΛnψxnlognn=1xΛnψxn=ψxlogx+n=1xΛnψxn+2logxn=1xΛnψxnlognn=1xΛnψxn
40 2cnd x1+∞2
41 13 recnd x1+∞logx
42 30 rpne0d x1+∞logx0
43 40 41 42 divcld x1+∞2logx
44 35 recnd x1+∞n=1xΛnψxnlogn
45 43 44 mulcld x1+∞2logxn=1xΛnψxnlogn
46 27 45 pncan3d x1+∞n=1xΛnψxn+2logxn=1xΛnψxnlogn-n=1xΛnψxn=2logxn=1xΛnψxnlogn
47 46 oveq2d x1+∞ψxlogx+n=1xΛnψxn+2logxn=1xΛnψxnlognn=1xΛnψxn=ψxlogx+2logxn=1xΛnψxnlogn
48 39 47 eqtr2d x1+∞ψxlogx+2logxn=1xΛnψxnlogn=ψxlogx+n=1xΛnψxn+2logxn=1xΛnψxnlognn=1xΛnψxn
49 48 oveq1d x1+∞ψxlogx+2logxn=1xΛnψxnlognx=ψxlogx+n=1xΛnψxn+2logxn=1xΛnψxnlognn=1xΛnψxnx
50 14 26 readdcld x1+∞ψxlogx+n=1xΛnψxn
51 50 recnd x1+∞ψxlogx+n=1xΛnψxn
52 2 recnd x1+∞x
53 12 rpne0d x1+∞x0
54 51 38 52 53 divdird x1+∞ψxlogx+n=1xΛnψxn+2logxn=1xΛnψxnlognn=1xΛnψxnx=ψxlogx+n=1xΛnψxnx+2logxn=1xΛnψxnlognn=1xΛnψxnx
55 49 54 eqtrd x1+∞ψxlogx+2logxn=1xΛnψxnlognx=ψxlogx+n=1xΛnψxnx+2logxn=1xΛnψxnlognn=1xΛnψxnx
56 55 oveq1d x1+∞ψxlogx+2logxn=1xΛnψxnlognx2logx=ψxlogx+n=1xΛnψxnx+2logxn=1xΛnψxnlognn=1xΛnψxnx-2logx
57 50 12 rerpdivcld x1+∞ψxlogx+n=1xΛnψxnx
58 57 recnd x1+∞ψxlogx+n=1xΛnψxnx
59 37 12 rerpdivcld x1+∞2logxn=1xΛnψxnlognn=1xΛnψxnx
60 59 recnd x1+∞2logxn=1xΛnψxnlognn=1xΛnψxnx
61 29 13 remulcld x1+∞2logx
62 61 recnd x1+∞2logx
63 58 60 62 addsubd x1+∞ψxlogx+n=1xΛnψxnx+2logxn=1xΛnψxnlognn=1xΛnψxnx-2logx=ψxlogx+n=1xΛnψxnx-2logx+2logxn=1xΛnψxnlognn=1xΛnψxnx
64 56 63 eqtrd x1+∞ψxlogx+2logxn=1xΛnψxnlognx2logx=ψxlogx+n=1xΛnψxnx-2logx+2logxn=1xΛnψxnlognn=1xΛnψxnx
65 64 mpteq2dva x1+∞ψxlogx+2logxn=1xΛnψxnlognx2logx=x1+∞ψxlogx+n=1xΛnψxnx-2logx+2logxn=1xΛnψxnlognn=1xΛnψxnx
66 57 61 resubcld x1+∞ψxlogx+n=1xΛnψxnx2logx
67 12 ex x1+∞x+
68 67 ssrdv 1+∞+
69 selberg2 x+ψxlogx+n=1xΛnψxnx2logx𝑂1
70 69 a1i x+ψxlogx+n=1xΛnψxnx2logx𝑂1
71 68 70 o1res2 x1+∞ψxlogx+n=1xΛnψxnx2logx𝑂1
72 selberg3lem2 x1+∞2logxn=1xΛnψxnlognn=1xΛnψxnx𝑂1
73 72 a1i x1+∞2logxn=1xΛnψxnlognn=1xΛnψxnx𝑂1
74 66 59 71 73 o1add2 x1+∞ψxlogx+n=1xΛnψxnx-2logx+2logxn=1xΛnψxnlognn=1xΛnψxnx𝑂1
75 65 74 eqeltrd x1+∞ψxlogx+2logxn=1xΛnψxnlognx2logx𝑂1
76 75 mptru x1+∞ψxlogx+2logxn=1xΛnψxnlognx2logx𝑂1