Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  selberg4 Unicode version

Theorem selberg4 21208
 Description: The Selberg symmetry formula for products of three primes, instead of two. The sum here can also be written in the symmetric form ΛΛΛ; we eliminate one of the nested sums by using the definition of ψ Λ. This statement can thus equivalently be written ψ ΛΛΛ . Equation 10.4.23 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)
Assertion
Ref Expression
selberg4 ψ Λ Λ ψ
Distinct variable group:   ,,

Proof of Theorem selberg4
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 2re 10025 . . . . . . . . . . . . 13
21a1i 11 . . . . . . . . . . . 12
3 elioore 10902 . . . . . . . . . . . . . 14
43adantl 453 . . . . . . . . . . . . 13
5 eliooord 10926 . . . . . . . . . . . . . . 15
65adantl 453 . . . . . . . . . . . . . 14
76simpld 446 . . . . . . . . . . . . 13
84, 7rplogcld 20477 . . . . . . . . . . . 12
92, 8rerpdivcld 10631 . . . . . . . . . . 11
10 fzfid 11267 . . . . . . . . . . . 12
11 elfznn 11036 . . . . . . . . . . . . . . . 16
1211adantl 453 . . . . . . . . . . . . . . 15
13 vmacl 20854 . . . . . . . . . . . . . . 15 Λ
1412, 13syl 16 . . . . . . . . . . . . . 14 Λ
154adantr 452 . . . . . . . . . . . . . . . 16
1615, 12nndivred 10004 . . . . . . . . . . . . . . 15
17 chpcl 20860 . . . . . . . . . . . . . . 15 ψ
1816, 17syl 16 . . . . . . . . . . . . . 14 ψ
1914, 18remulcld 9072 . . . . . . . . . . . . 13 Λ ψ
2012nnrpd 10603 . . . . . . . . . . . . . 14
2120relogcld 20471 . . . . . . . . . . . . 13
2219, 21remulcld 9072 . . . . . . . . . . . 12 Λ ψ
2310, 22fsumrecl 12483 . . . . . . . . . . 11 Λ ψ
249, 23remulcld 9072 . . . . . . . . . 10 Λ ψ
2510, 19fsumrecl 12483 . . . . . . . . . 10 Λ ψ
2624, 25resubcld 9421 . . . . . . . . 9 Λ ψ Λ ψ
27 1rp 10572 . . . . . . . . . . 11
2827a1i 11 . . . . . . . . . 10
2928rpred 10604 . . . . . . . . . . 11
3029, 4, 7ltled 9177 . . . . . . . . . 10
314, 28, 30rpgecld 10639 . . . . . . . . 9
3226, 31rerpdivcld 10631 . . . . . . . 8 Λ ψ Λ ψ
3332recnd 9070 . . . . . . 7 Λ ψ Λ ψ
34 chpcl 20860 . . . . . . . . . . . 12 ψ
354, 34syl 16 . . . . . . . . . . 11 ψ
3631relogcld 20471 . . . . . . . . . . 11
3735, 36remulcld 9072 . . . . . . . . . 10 ψ
3837, 25readdcld 9071 . . . . . . . . 9 ψ Λ ψ
3938, 31rerpdivcld 10631 . . . . . . . 8 ψ Λ ψ
4039recnd 9070 . . . . . . 7 ψ Λ ψ
412, 36remulcld 9072 . . . . . . . 8
4241recnd 9070 . . . . . . 7
4333, 40, 42addsubassd 9387 . . . . . 6 Λ ψ Λ ψ ψ Λ ψ Λ ψ Λ ψ ψ Λ ψ
4426recnd 9070 . . . . . . . . 9 Λ ψ Λ ψ
4538recnd 9070 . . . . . . . . 9 ψ Λ ψ
464recnd 9070 . . . . . . . . 9
4731rpne0d 10609 . . . . . . . . 9
4844, 45, 46, 47divdird 9784 . . . . . . . 8 Λ ψ Λ ψ ψ Λ ψ Λ ψ Λ ψ ψ Λ ψ
4924recnd 9070 . . . . . . . . . . 11 Λ ψ
5025recnd 9070 . . . . . . . . . . 11 Λ ψ
5137recnd 9070 . . . . . . . . . . 11 ψ
5249, 50, 51nppcan3d 9394 . . . . . . . . . 10 Λ ψ Λ ψ ψ Λ ψ Λ ψ ψ
53 elfznn 11036 . . . . . . . . . . . . . . . . . 18
5453ad2antll 710 . . . . . . . . . . . . . . . . 17
55 vmacl 20854 . . . . . . . . . . . . . . . . 17 Λ
5654, 55syl 16 . . . . . . . . . . . . . . . 16 Λ
5714adantrr 698 . . . . . . . . . . . . . . . . 17 Λ
5820adantrr 698 . . . . . . . . . . . . . . . . . 18
5958relogcld 20471 . . . . . . . . . . . . . . . . 17
6057, 59remulcld 9072 . . . . . . . . . . . . . . . 16 Λ
6156, 60remulcld 9072 . . . . . . . . . . . . . . 15 Λ Λ
6261recnd 9070 . . . . . . . . . . . . . 14 Λ Λ
634, 62fsumfldivdiag 20928 . . . . . . . . . . . . 13 Λ Λ Λ Λ
6414recnd 9070 . . . . . . . . . . . . . . . 16 Λ
6518recnd 9070 . . . . . . . . . . . . . . . 16 ψ
6621recnd 9070 . . . . . . . . . . . . . . . 16
6764, 65, 66mul32d 9232 . . . . . . . . . . . . . . 15 Λ ψ Λ ψ
6864, 66mulcld 9064 . . . . . . . . . . . . . . . 16 Λ
6968, 65mulcomd 9065 . . . . . . . . . . . . . . 15 Λ ψ ψ Λ
70 chpval 20858 . . . . . . . . . . . . . . . . . 18 ψ Λ
7116, 70syl 16 . . . . . . . . . . . . . . . . 17 ψ Λ
7271oveq1d 6055 . . . . . . . . . . . . . . . 16 ψ Λ Λ Λ
73 fzfid 11267 . . . . . . . . . . . . . . . . 17
7456anassrs 630 . . . . . . . . . . . . . . . . . 18 Λ
7574recnd 9070 . . . . . . . . . . . . . . . . 17 Λ
7673, 68, 75fsummulc1 12523 . . . . . . . . . . . . . . . 16 Λ Λ Λ Λ
7772, 76eqtrd 2436 . . . . . . . . . . . . . . 15 ψ Λ Λ Λ
7867, 69, 773eqtrd 2440 . . . . . . . . . . . . . 14 Λ ψ Λ Λ
7978sumeq2dv 12452 . . . . . . . . . . . . 13 Λ ψ Λ Λ
80 fzfid 11267 . . . . . . . . . . . . . . 15
81 elfznn 11036 . . . . . . . . . . . . . . . . . 18
8281adantl 453 . . . . . . . . . . . . . . . . 17
8382, 55syl 16 . . . . . . . . . . . . . . . 16 Λ
8483recnd 9070 . . . . . . . . . . . . . . 15 Λ
85 elfznn 11036 . . . . . . . . . . . . . . . . . . 19
8685adantl 453 . . . . . . . . . . . . . . . . . 18
8786, 13syl 16 . . . . . . . . . . . . . . . . 17 Λ
8886nnrpd 10603 . . . . . . . . . . . . . . . . . 18
8988relogcld 20471 . . . . . . . . . . . . . . . . 17
9087, 89remulcld 9072 . . . . . . . . . . . . . . . 16 Λ
9190recnd 9070 . . . . . . . . . . . . . . 15 Λ
9280, 84, 91fsummulc2 12522 . . . . . . . . . . . . . 14 Λ Λ Λ Λ
9392sumeq2dv 12452 . . . . . . . . . . . . 13 Λ Λ Λ Λ
9463, 79, 933eqtr4d 2446 . . . . . . . . . . . 12 Λ ψ Λ Λ
9594oveq2d 6056 . . . . . . . . . . 11 Λ ψ Λ Λ
9695oveq1d 6055 . . . . . . . . . 10 Λ ψ ψ Λ Λ ψ
9752, 96eqtrd 2436 . . . . . . . . 9 Λ ψ Λ ψ ψ Λ ψ Λ Λ ψ
9897oveq1d 6055 . . . . . . . 8 Λ ψ Λ ψ ψ Λ ψ Λ Λ ψ
9948, 98eqtr3d 2438 . . . . . . 7 Λ ψ Λ ψ ψ Λ ψ Λ Λ ψ
10099oveq1d 6055 . . . . . 6 Λ ψ Λ ψ ψ Λ ψ Λ Λ ψ
10143, 100eqtr3d 2438 . . . . 5 Λ ψ Λ ψ ψ Λ ψ Λ Λ ψ
102101mpteq2dva 4255 . . . 4 Λ ψ Λ ψ ψ Λ ψ Λ Λ ψ
10339, 41resubcld 9421 . . . . 5 ψ Λ ψ
104 selberg3lem2 21205 . . . . . 6 Λ ψ Λ ψ
105104a1i 11 . . . . 5 Λ ψ Λ ψ
10631ex 424 . . . . . . 7
107106ssrdv 3314 . . . . . 6
108 selberg2 21198 . . . . . . 7 ψ Λ ψ
109108a1i 11 . . . . . 6 ψ Λ ψ
110107, 109o1res2 12312 . . . . 5 ψ Λ ψ
11132, 103, 105, 110o1add2 12372 . . . 4 Λ ψ Λ ψ ψ Λ ψ
112102, 111eqeltrrd 2479 . . 3 Λ Λ ψ
11380, 90fsumrecl 12483 . . . . . . . . . . 11 Λ
11483, 113remulcld 9072 . . . . . . . . . 10 Λ Λ
11510, 114fsumrecl 12483 . . . . . . . . 9 Λ Λ
1169, 115remulcld 9072 . . . . . . . 8 Λ Λ
117116, 37readdcld 9071 . . . . . . 7 Λ Λ ψ
118117, 31rerpdivcld 10631 . . . . . 6 Λ Λ ψ
119118, 41resubcld 9421 . . . . 5 Λ Λ ψ
120119recnd 9070 . . . 4 Λ Λ ψ
1214adantr 452 . . . . . . . . . . . . . . . 16
122121, 82nndivred 10004 . . . . . . . . . . . . . . 15
123122adantr 452 . . . . . . . . . . . . . 14
124123, 86nndivred 10004 . . . . . . . . . . . . 13
125 chpcl 20860 . . . . . . . . . . . . 13 ψ
126124, 125syl 16 . . . . . . . . . . . 12 ψ
12787, 126remulcld 9072 . . . . . . . . . . 11 Λ ψ
12880, 127fsumrecl 12483 . . . . . . . . . 10 Λ ψ
12983, 128remulcld 9072 . . . . . . . . 9 Λ Λ ψ
13010, 129fsumrecl 12483 . . . . . . . 8 Λ Λ ψ
1319, 130remulcld 9072 . . . . . . 7 Λ Λ ψ
13237, 131resubcld 9421 . . . . . 6 ψ Λ Λ ψ
133132, 31rerpdivcld 10631 . . . . 5 ψ Λ Λ ψ
134133recnd 9070 . . . 4 ψ Λ Λ ψ
135116recnd 9070 . . . . . . . . . . . 12 Λ Λ
136131recnd 9070 . . . . . . . . . . . 12 Λ Λ ψ
13751, 135, 136pnncand 9406 . . . . . . . . . . 11 ψ Λ Λ ψ Λ Λ ψ Λ Λ Λ Λ ψ
138135, 51addcomd 9224 . . . . . . . . . . . 12 Λ Λ ψ ψ Λ Λ
139138oveq1d 6055 . . . . . . . . . . 11 Λ Λ ψ ψ Λ Λ ψ ψ Λ Λ ψ Λ Λ ψ
14087recnd 9070 . . . . . . . . . . . . . . . . . . . 20 Λ
14189recnd 9070 . . . . . . . . . . . . . . . . . . . 20
142126recnd 9070 . . . . . . . . . . . . . . . . . . . 20 ψ
143140, 141, 142adddid 9068 . . . . . . . . . . . . . . . . . . 19 Λ ψ Λ Λ ψ
144143sumeq2dv 12452 . . . . . . . . . . . . . . . . . 18 Λ ψ Λ Λ ψ
145127recnd 9070 . . . . . . . . . . . . . . . . . . 19 Λ ψ
14680, 91, 145fsumadd 12487 . . . . . . . . . . . . . . . . . 18 Λ Λ ψ Λ Λ ψ
147144, 146eqtrd 2436 . . . . . . . . . . . . . . . . 17 Λ ψ Λ Λ ψ
148147oveq2d 6056 . . . . . . . . . . . . . . . 16 Λ Λ ψ Λ Λ Λ ψ
149113recnd 9070 . . . . . . . . . . . . . . . . 17 Λ
150128recnd 9070 . . . . . . . . . . . . . . . . 17 Λ ψ
15184, 149, 150adddid 9068 . . . . . . . . . . . . . . . 16 Λ Λ Λ ψ Λ Λ Λ Λ ψ
152148, 151eqtrd 2436 . . . . . . . . . . . . . . 15 Λ Λ ψ Λ Λ Λ Λ ψ
153152sumeq2dv 12452 . . . . . . . . . . . . . 14 Λ Λ ψ Λ Λ Λ Λ ψ
154114recnd 9070 . . . . . . . . . . . . . . 15 Λ Λ
155129recnd 9070 . . . . . . . . . . . . . . 15 Λ Λ ψ
15610, 154, 155fsumadd 12487 . . . . . . . . . . . . . 14 Λ Λ Λ Λ ψ Λ Λ Λ Λ ψ
157153, 156eqtrd 2436 . . . . . . . . . . . . 13 Λ Λ ψ Λ Λ Λ Λ ψ
158157oveq2d 6056 . . . . . . . . . . . 12 Λ Λ ψ Λ Λ Λ Λ ψ
1599recnd 9070 . . . . . . . . . . . . 13
160115recnd 9070 . . . . . . . . . . . . 13 Λ Λ
161130recnd 9070 . . . . . . . . . . . . 13 Λ Λ ψ
162159, 160, 161adddid 9068 . . . . . . . . . . . 12 Λ Λ Λ Λ ψ Λ Λ Λ Λ ψ
163158, 162eqtrd 2436 . . . . . . . . . . 11 Λ Λ ψ Λ Λ Λ Λ ψ
164137, 139, 1633eqtr4d 2446 . . . . . . . . . 10 Λ Λ ψ ψ Λ Λ ψ Λ Λ ψ
165164oveq1d 6055 . . . . . . . . 9 Λ Λ ψ ψ Λ Λ ψ Λ Λ ψ
166117recnd 9070 . . . . . . . . . 10 Λ Λ ψ
16751, 136subcld 9367 . . . . . . . . . 10 ψ Λ Λ ψ
168166, 167, 46, 47divsubdird 9785 . . . . . . . . 9 Λ Λ ψ ψ Λ Λ ψ Λ Λ ψ ψ Λ Λ ψ
169 2cn 10026 . . . . . . . . . . . . . 14
170169a1i 11 . . . . . . . . . . . . 13
17189, 126readdcld 9071 . . . . . . . . . . . . . . . . . 18 ψ
17287, 171remulcld 9072 . . . . . . . . . . . . . . . . 17 Λ ψ
17380, 172fsumrecl 12483 . . . . . . . . . . . . . . . 16 Λ ψ
17483, 173remulcld 9072 . . . . . . . . . . . . . . 15 Λ Λ ψ
17510, 174fsumrecl 12483 . . . . . . . . . . . . . 14 Λ Λ ψ
176175recnd 9070 . . . . . . . . . . . . 13 Λ Λ ψ
177170, 176mulcld 9064 . . . . . . . . . . . 12 Λ Λ ψ
17836recnd 9070 . . . . . . . . . . . 12
1798rpne0d 10609 . . . . . . . . . . . 12
180177, 178, 46, 179, 47divdiv1d 9777 . . . . . . . . . . 11 Λ Λ ψ Λ Λ ψ
181178, 46mulcomd 9065 . . . . . . . . . . . 12
182181oveq2d 6056 . . . . . . . . . . 11 Λ Λ ψ Λ Λ ψ
183180, 182eqtrd 2436 . . . . . . . . . 10 Λ Λ ψ Λ Λ ψ
184170, 176, 178, 179div23d 9783 . . . . . . . . . . 11 Λ Λ ψ Λ Λ ψ
185184oveq1d 6055 . . . . . . . . . 10 Λ Λ ψ Λ Λ ψ
18631, 8rpmulcld 10620 . . . . . . . . . . . 12
187186rpcnd 10606 . . . . . . . . . . 11
188186rpne0d 10609 . . . . . . . . . . 11
189170, 176, 187, 188divassd 9781 . . . . . . . . . 10 Λ Λ ψ Λ Λ ψ
190183, 185, 1893eqtr3d 2444 . . . . . . . . 9 Λ Λ ψ Λ Λ ψ
191165, 168, 1903eqtr3d 2444 . . . . . . . 8 Λ Λ ψ ψ Λ Λ ψ Λ Λ ψ
192191oveq1d 6055 . . . . . . 7 Λ Λ ψ ψ Λ Λ ψ Λ Λ ψ
193118recnd 9070 . . . . . . . 8 Λ Λ ψ
194193, 42, 134sub32d 9399 . . . . . . 7 Λ Λ ψ ψ Λ Λ ψ