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

Theorem selberg4 24478
 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 10701 . . . . . . . . . . . . 13
21a1i 11 . . . . . . . . . . . 12
3 elioore 11691 . . . . . . . . . . . . . 14
43adantl 473 . . . . . . . . . . . . 13
5 eliooord 11719 . . . . . . . . . . . . . . 15
65adantl 473 . . . . . . . . . . . . . 14
76simpld 466 . . . . . . . . . . . . 13
84, 7rplogcld 23657 . . . . . . . . . . . 12
92, 8rerpdivcld 11392 . . . . . . . . . . 11
10 fzfid 12224 . . . . . . . . . . . 12
11 elfznn 11854 . . . . . . . . . . . . . . . 16
1211adantl 473 . . . . . . . . . . . . . . 15
13 vmacl 24124 . . . . . . . . . . . . . . 15 Λ
1412, 13syl 17 . . . . . . . . . . . . . 14 Λ
154adantr 472 . . . . . . . . . . . . . . . 16
1615, 12nndivred 10680 . . . . . . . . . . . . . . 15
17 chpcl 24130 . . . . . . . . . . . . . . 15 ψ
1816, 17syl 17 . . . . . . . . . . . . . 14 ψ
1914, 18remulcld 9689 . . . . . . . . . . . . 13 Λ ψ
2012nnrpd 11362 . . . . . . . . . . . . . 14
2120relogcld 23651 . . . . . . . . . . . . 13
2219, 21remulcld 9689 . . . . . . . . . . . 12 Λ ψ
2310, 22fsumrecl 13877 . . . . . . . . . . 11 Λ ψ
249, 23remulcld 9689 . . . . . . . . . 10 Λ ψ
2510, 19fsumrecl 13877 . . . . . . . . . 10 Λ ψ
2624, 25resubcld 10068 . . . . . . . . 9 Λ ψ Λ ψ
27 1rp 11329 . . . . . . . . . . 11
2827a1i 11 . . . . . . . . . 10
29 1red 9676 . . . . . . . . . . 11
3029, 4, 7ltled 9800 . . . . . . . . . 10
314, 28, 30rpgecld 11400 . . . . . . . . 9
3226, 31rerpdivcld 11392 . . . . . . . 8 Λ ψ Λ ψ
3332recnd 9687 . . . . . . 7 Λ ψ Λ ψ
34 chpcl 24130 . . . . . . . . . . . 12 ψ
354, 34syl 17 . . . . . . . . . . 11 ψ
3631relogcld 23651 . . . . . . . . . . 11
3735, 36remulcld 9689 . . . . . . . . . 10 ψ
3837, 25readdcld 9688 . . . . . . . . 9 ψ Λ ψ
3938, 31rerpdivcld 11392 . . . . . . . 8 ψ Λ ψ
4039recnd 9687 . . . . . . 7 ψ Λ ψ
412, 36remulcld 9689 . . . . . . . 8
4241recnd 9687 . . . . . . 7
4333, 40, 42addsubassd 10025 . . . . . 6 Λ ψ Λ ψ ψ Λ ψ Λ ψ Λ ψ ψ Λ ψ
4426recnd 9687 . . . . . . . . 9 Λ ψ Λ ψ
4538recnd 9687 . . . . . . . . 9 ψ Λ ψ
464recnd 9687 . . . . . . . . 9
4731rpne0d 11369 . . . . . . . . 9
4844, 45, 46, 47divdird 10443 . . . . . . . 8 Λ ψ Λ ψ ψ Λ ψ Λ ψ Λ ψ ψ Λ ψ
4924recnd 9687 . . . . . . . . . . 11 Λ ψ
5025recnd 9687 . . . . . . . . . . 11 Λ ψ
5137recnd 9687 . . . . . . . . . . 11 ψ
5249, 50, 51nppcan3d 10032 . . . . . . . . . 10 Λ ψ Λ ψ ψ Λ ψ Λ ψ ψ
53 elfznn 11854 . . . . . . . . . . . . . . . . . 18
5453ad2antll 743 . . . . . . . . . . . . . . . . 17
55 vmacl 24124 . . . . . . . . . . . . . . . . 17 Λ
5654, 55syl 17 . . . . . . . . . . . . . . . 16 Λ
5714adantrr 731 . . . . . . . . . . . . . . . . 17 Λ
5820adantrr 731 . . . . . . . . . . . . . . . . . 18
5958relogcld 23651 . . . . . . . . . . . . . . . . 17
6057, 59remulcld 9689 . . . . . . . . . . . . . . . 16 Λ
6156, 60remulcld 9689 . . . . . . . . . . . . . . 15 Λ Λ
6261recnd 9687 . . . . . . . . . . . . . 14 Λ Λ
634, 62fsumfldivdiag 24198 . . . . . . . . . . . . 13 Λ Λ Λ Λ
6414recnd 9687 . . . . . . . . . . . . . . . 16 Λ
6518recnd 9687 . . . . . . . . . . . . . . . 16 ψ
6621recnd 9687 . . . . . . . . . . . . . . . 16
6764, 65, 66mul32d 9861 . . . . . . . . . . . . . . 15 Λ ψ Λ ψ
6864, 66mulcld 9681 . . . . . . . . . . . . . . . 16 Λ
6968, 65mulcomd 9682 . . . . . . . . . . . . . . 15 Λ ψ ψ Λ
70 chpval 24128 . . . . . . . . . . . . . . . . . 18 ψ Λ
7116, 70syl 17 . . . . . . . . . . . . . . . . 17 ψ Λ
7271oveq1d 6323 . . . . . . . . . . . . . . . 16 ψ Λ Λ Λ
73 fzfid 12224 . . . . . . . . . . . . . . . . 17
7456anassrs 660 . . . . . . . . . . . . . . . . . 18 Λ
7574recnd 9687 . . . . . . . . . . . . . . . . 17 Λ
7673, 68, 75fsummulc1 13923 . . . . . . . . . . . . . . . 16 Λ Λ Λ Λ
7772, 76eqtrd 2505 . . . . . . . . . . . . . . 15 ψ Λ Λ Λ
7867, 69, 773eqtrd 2509 . . . . . . . . . . . . . 14 Λ ψ Λ Λ
7978sumeq2dv 13846 . . . . . . . . . . . . 13 Λ ψ Λ Λ
80 fzfid 12224 . . . . . . . . . . . . . . 15
81 elfznn 11854 . . . . . . . . . . . . . . . . . 18
8281adantl 473 . . . . . . . . . . . . . . . . 17
8382, 55syl 17 . . . . . . . . . . . . . . . 16 Λ
8483recnd 9687 . . . . . . . . . . . . . . 15 Λ
85 elfznn 11854 . . . . . . . . . . . . . . . . . . 19
8685adantl 473 . . . . . . . . . . . . . . . . . 18
8786, 13syl 17 . . . . . . . . . . . . . . . . 17 Λ
8886nnrpd 11362 . . . . . . . . . . . . . . . . . 18
8988relogcld 23651 . . . . . . . . . . . . . . . . 17
9087, 89remulcld 9689 . . . . . . . . . . . . . . . 16 Λ
9190recnd 9687 . . . . . . . . . . . . . . 15 Λ
9280, 84, 91fsummulc2 13922 . . . . . . . . . . . . . 14 Λ Λ Λ Λ
9392sumeq2dv 13846 . . . . . . . . . . . . 13 Λ Λ Λ Λ
9463, 79, 933eqtr4d 2515 . . . . . . . . . . . 12 Λ ψ Λ Λ
9594oveq2d 6324 . . . . . . . . . . 11 Λ ψ Λ Λ
9695oveq1d 6323 . . . . . . . . . 10 Λ ψ ψ Λ Λ ψ
9752, 96eqtrd 2505 . . . . . . . . 9 Λ ψ Λ ψ ψ Λ ψ Λ Λ ψ
9897oveq1d 6323 . . . . . . . 8 Λ ψ Λ ψ ψ Λ ψ Λ Λ ψ
9948, 98eqtr3d 2507 . . . . . . 7 Λ ψ Λ ψ ψ Λ ψ Λ Λ ψ
10099oveq1d 6323 . . . . . 6 Λ ψ Λ ψ ψ Λ ψ Λ Λ ψ
10143, 100eqtr3d 2507 . . . . 5 Λ ψ Λ ψ ψ Λ ψ Λ Λ ψ
102101mpteq2dva 4482 . . . 4 Λ ψ Λ ψ ψ Λ ψ Λ Λ ψ
10339, 41resubcld 10068 . . . . 5 ψ Λ ψ
104 selberg3lem2 24475 . . . . . 6 Λ ψ Λ ψ
105104a1i 11 . . . . 5 Λ ψ Λ ψ
10631ex 441 . . . . . . 7
107106ssrdv 3424 . . . . . 6
108 selberg2 24468 . . . . . . 7 ψ Λ ψ
109108a1i 11 . . . . . 6 ψ Λ ψ
110107, 109o1res2 13704 . . . . 5 ψ Λ ψ
11132, 103, 105, 110o1add2 13764 . . . 4 Λ ψ Λ ψ ψ Λ ψ
112102, 111eqeltrrd 2550 . . 3 Λ Λ ψ
11380, 90fsumrecl 13877 . . . . . . . . . . 11 Λ
11483, 113remulcld 9689 . . . . . . . . . 10 Λ Λ
11510, 114fsumrecl 13877 . . . . . . . . 9 Λ Λ
1169, 115remulcld 9689 . . . . . . . 8 Λ Λ
117116, 37readdcld 9688 . . . . . . 7 Λ Λ ψ
118117, 31rerpdivcld 11392 . . . . . 6 Λ Λ ψ
119118, 41resubcld 10068 . . . . 5 Λ Λ ψ
120119recnd 9687 . . . 4 Λ Λ ψ
1214adantr 472 . . . . . . . . . . . . . . . 16
122121, 82nndivred 10680 . . . . . . . . . . . . . . 15
123122adantr 472 . . . . . . . . . . . . . 14
124123, 86nndivred 10680 . . . . . . . . . . . . 13
125 chpcl 24130 . . . . . . . . . . . . 13 ψ
126124, 125syl 17 . . . . . . . . . . . 12 ψ
12787, 126remulcld 9689 . . . . . . . . . . 11 Λ ψ
12880, 127fsumrecl 13877 . . . . . . . . . 10 Λ ψ
12983, 128remulcld 9689 . . . . . . . . 9 Λ Λ ψ
13010, 129fsumrecl 13877 . . . . . . . 8 Λ Λ ψ
1319, 130remulcld 9689 . . . . . . 7 Λ Λ ψ
13237, 131resubcld 10068 . . . . . 6 ψ Λ Λ ψ
133132, 31rerpdivcld 11392 . . . . 5 ψ Λ Λ ψ
134133recnd 9687 . . . 4 ψ Λ Λ ψ
135116recnd 9687 . . . . . . . . . . . 12 Λ Λ
136131recnd 9687 . . . . . . . . . . . 12 Λ Λ ψ
13751, 135, 136pnncand 10044 . . . . . . . . . . 11 ψ Λ Λ ψ Λ Λ ψ Λ Λ Λ Λ ψ
138135, 51addcomd 9853 . . . . . . . . . . . 12 Λ Λ ψ ψ Λ Λ
139138oveq1d 6323 . . . . . . . . . . 11 Λ Λ ψ ψ Λ Λ ψ ψ Λ Λ ψ Λ Λ ψ
14087recnd 9687 . . . . . . . . . . . . . . . . . . . 20 Λ
14189recnd 9687 . . . . . . . . . . . . . . . . . . . 20
142126recnd 9687 . . . . . . . . . . . . . . . . . . . 20 ψ
143140, 141, 142adddid 9685 . . . . . . . . . . . . . . . . . . 19 Λ ψ Λ Λ ψ
144143sumeq2dv 13846 . . . . . . . . . . . . . . . . . 18 Λ ψ Λ Λ ψ
145127recnd 9687 . . . . . . . . . . . . . . . . . . 19 Λ ψ
14680, 91, 145fsumadd 13882 . . . . . . . . . . . . . . . . . 18 Λ Λ ψ Λ Λ ψ
147144, 146eqtrd 2505 . . . . . . . . . . . . . . . . 17 Λ ψ Λ Λ ψ
148147oveq2d 6324 . . . . . . . . . . . . . . . 16 Λ Λ ψ Λ Λ Λ ψ
149113recnd 9687 . . . . . . . . . . . . . . . . 17 Λ
150128recnd 9687 . . . . . . . . . . . . . . . . 17 Λ ψ
15184, 149, 150adddid 9685 . . . . . . . . . . . . . . . 16 Λ Λ Λ ψ Λ Λ Λ Λ ψ
152148, 151eqtrd 2505 . . . . . . . . . . . . . . 15 Λ Λ ψ Λ Λ Λ Λ ψ
153152sumeq2dv 13846 . . . . . . . . . . . . . 14 Λ Λ ψ Λ Λ Λ Λ ψ
154114recnd 9687 . . . . . . . . . . . . . . 15 Λ Λ
155129recnd 9687 . . . . . . . . . . . . . . 15 Λ Λ ψ
15610, 154, 155fsumadd 13882 . . . . . . . . . . . . . 14 Λ Λ Λ Λ ψ Λ Λ Λ Λ ψ
157153, 156eqtrd 2505 . . . . . . . . . . . . 13 Λ Λ ψ Λ Λ Λ Λ ψ
158157oveq2d 6324 . . . . . . . . . . . 12 Λ Λ ψ Λ Λ Λ Λ ψ
1599recnd 9687 . . . . . . . . . . . . 13
160115recnd 9687 . . . . . . . . . . . . 13 Λ Λ
161130recnd 9687 . . . . . . . . . . . . 13 Λ Λ ψ
162159, 160, 161adddid 9685 . . . . . . . . . . . 12 Λ Λ Λ Λ ψ Λ Λ Λ Λ ψ
163158, 162eqtrd 2505 . . . . . . . . . . 11 Λ Λ ψ Λ Λ Λ Λ ψ
164137, 139, 1633eqtr4d 2515 . . . . . . . . . 10 Λ Λ ψ ψ Λ Λ ψ Λ Λ ψ
165164oveq1d 6323 . . . . . . . . 9 Λ Λ ψ ψ Λ Λ ψ Λ Λ ψ
166117recnd 9687 . . . . . . . . . 10 Λ Λ ψ
16751, 136subcld 10005 . . . . . . . . . 10 ψ Λ Λ ψ
168166, 167, 46, 47divsubdird 10444 . . . . . . . . 9 Λ Λ ψ ψ Λ Λ ψ Λ Λ ψ ψ Λ Λ ψ
169 2cnd 10704 . . . . . . . . . . . . 13
17089, 126readdcld 9688 . . . . . . . . . . . . . . . . . 18 ψ
17187, 170remulcld 9689 . . . . . . . . . . . . . . . . 17 Λ ψ
17280, 171fsumrecl 13877 . . . . . . . . . . . . . . . 16 Λ ψ
17383, 172remulcld 9689 . . . . . . . . . . . . . . 15 Λ Λ ψ
17410, 173fsumrecl 13877 . . . . . . . . . . . . . 14 Λ Λ ψ
175174recnd 9687 . . . . . . . . . . . . 13 Λ Λ ψ
176169, 175mulcld 9681 . . . . . . . . . . . 12 Λ Λ ψ
17736recnd 9687 . . . . . . . . . . . 12
1788rpne0d 11369 . . . . . . . . . . . 12
179176, 177, 46, 178, 47divdiv1d 10436 . . . . . . . . . . 11 Λ Λ ψ Λ Λ ψ
180177, 46mulcomd 9682 . . . . . . . . . . . 12
181180oveq2d 6324 . . . . . . . . . . 11 Λ Λ ψ Λ Λ ψ
182179, 181eqtrd 2505 . . . . . . . . . 10 Λ Λ ψ Λ Λ ψ
183169, 175, 177, 178div23d 10442 . . . . . . . . . . 11 Λ Λ ψ Λ Λ ψ
184183oveq1d 6323 . . . . . . . . . 10 Λ Λ ψ Λ Λ ψ
18531, 8rpmulcld 11380 . . . . . . . . . . . 12
186185rpcnd 11366 . . . . . . . . . . 11
187185rpne0d 11369 . . . . . . . . . . 11
188169, 175, 186, 187divassd 10440 . . . . . . . . . 10 Λ Λ ψ Λ Λ ψ
189182, 184, 1883eqtr3d 2513 . . . . . . . . 9 Λ Λ ψ Λ Λ ψ
190165, 168, 1893eqtr3d 2513 . . . . . . . 8 Λ Λ ψ ψ Λ Λ ψ Λ Λ ψ
191190oveq1d 6323 . . . . . . 7 Λ Λ ψ ψ Λ Λ ψ Λ Λ ψ
192118recnd 9687 . . . . . . . 8 Λ Λ ψ
193192, 42, 134sub32d 10037 . . . . . . 7 Λ Λ ψ ψ Λ Λ ψ Λ