selberg3r - Metamath Proof Explorer

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

Theorem selberg3r 22798

Description: Selberg's symmetry formula, using the residual of the second Chebyshev function. Equation 10.6.8 of [Shapiro], p. 429. (Contributed by Mario Carneiro, 30-May-2016.)

**Hypothesis**
Ref	Expression
pntrval.r	ψ

**Assertion**
Ref	Expression
selberg3r	Λ

Distinct variable groups:

Allowed substitution hint:

(

)

**Proof of Theorem selberg3r**
Step	Hyp	Ref	Expression
1		elioore 11322	. . . . . . . . . . . . 13
2	1	adantl 466	. . . . . . . . . . . 12 $/\$
3		1rp 10987	. . . . . . . . . . . . 13
4	3	a1i 11	. . . . . . . . . . . 12 $/\$
5		1red 9393	. . . . . . . . . . . . 13 $/\$
6		eliooord 11347	. . . . . . . . . . . . . . 15 $/\$
7	6	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$
8	7	simpld 459	. . . . . . . . . . . . 13 $/\$
9	5, 2, 8	ltled 9514	. . . . . . . . . . . 12 $/\$
10	2, 4, 9	rpgecld 11054	. . . . . . . . . . 11 $/\$
11	10	relogcld 22052	. . . . . . . . . 10 $/\$
12	11	recnd 9404	. . . . . . . . 9 $/\$
13	12	2timesd 10559	. . . . . . . 8 $/\$
14	13	oveq2d 6102	. . . . . . 7 $/\$ ψ Λ ψ ψ Λ ψ
15		chpcl 22442	. . . . . . . . . . . . 13 ψ
16	2, 15	syl 16	. . . . . . . . . . . 12 $/\$ ψ
17	16, 11	remulcld 9406	. . . . . . . . . . 11 $/\$ ψ
18		2re 10383	. . . . . . . . . . . . . 14
19	18	a1i 11	. . . . . . . . . . . . 13 $/\$
20	2, 8	rplogcld 22058	. . . . . . . . . . . . 13 $/\$
21	19, 20	rerpdivcld 11046	. . . . . . . . . . . 12 $/\$
22		fzfid 11787	. . . . . . . . . . . . 13 $/\$
23		elfznn 11470	. . . . . . . . . . . . . . . . 17
24	23	adantl 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$
25		vmacl 22436	. . . . . . . . . . . . . . . 16 Λ
26	24, 25	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ Λ
27	2	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
28	27, 24	nndivred 10362	. . . . . . . . . . . . . . . 16 $/\$ $/\$
29		chpcl 22442	. . . . . . . . . . . . . . . 16 ψ
30	28, 29	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ ψ
31	26, 30	remulcld 9406	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ ψ
32	24	nnrpd 11018	. . . . . . . . . . . . . . 15 $/\$ $/\$
33	32	relogcld 22052	. . . . . . . . . . . . . 14 $/\$ $/\$
34	31, 33	remulcld 9406	. . . . . . . . . . . . 13 $/\$ $/\$ Λ ψ
35	22, 34	fsumrecl 13203	. . . . . . . . . . . 12 $/\$ Λ ψ
36	21, 35	remulcld 9406	. . . . . . . . . . 11 $/\$ Λ ψ
37	17, 36	readdcld 9405	. . . . . . . . . 10 $/\$ ψ Λ ψ
38	37, 10	rerpdivcld 11046	. . . . . . . . 9 $/\$ ψ Λ ψ
39	38	recnd 9404	. . . . . . . 8 $/\$ ψ Λ ψ
40	39, 12, 12	subsub4d 9742	. . . . . . 7 $/\$ ψ Λ ψ ψ Λ ψ
41	14, 40	eqtr4d 2473	. . . . . 6 $/\$ ψ Λ ψ ψ Λ ψ
42	41	oveq1d 6101	. . . . 5 $/\$ ψ Λ ψ Λ ψ Λ ψ Λ
43	39, 12	subcld 9711	. . . . . 6 $/\$ ψ Λ ψ
44		2cn 10384	. . . . . . . . 9
45	44	a1i 11	. . . . . . . 8 $/\$
46	20	rpne0d 11024	. . . . . . . 8 $/\$
47	45, 12, 46	divcld 10099	. . . . . . 7 $/\$
48	26, 24	nndivred 10362	. . . . . . . . . 10 $/\$ $/\$ Λ
49	48, 33	remulcld 9406	. . . . . . . . 9 $/\$ $/\$ Λ
50	22, 49	fsumrecl 13203	. . . . . . . 8 $/\$ Λ
51	50	recnd 9404	. . . . . . 7 $/\$ Λ
52	47, 51	mulcld 9398	. . . . . 6 $/\$ Λ
53	43, 52, 12	nnncan2d 9746	. . . . 5 $/\$ ψ Λ ψ Λ ψ Λ ψ Λ
54		pntrval.r	. . . . . . . . . . . . 13 ψ
55	54	pntrf 22792	. . . . . . . . . . . 12
56	55	ffvelrni 5837	. . . . . . . . . . 11
57	10, 56	syl 16	. . . . . . . . . 10 $/\$
58	57	recnd 9404	. . . . . . . . 9 $/\$
59	58, 12	mulcld 9398	. . . . . . . 8 $/\$
60	36	recnd 9404	. . . . . . . 8 $/\$ Λ ψ
61	59, 60	addcld 9397	. . . . . . 7 $/\$ Λ ψ
62	2	recnd 9404	. . . . . . . 8 $/\$
63	62, 52	mulcld 9398	. . . . . . 7 $/\$ Λ
64	10	rpne0d 11024	. . . . . . 7 $/\$
65	61, 63, 62, 64	divsubdird 10138	. . . . . 6 $/\$ Λ ψ Λ Λ ψ Λ
66	59, 60, 63	addsubassd 9731	. . . . . . . 8 $/\$ Λ ψ Λ Λ ψ Λ
67	35	recnd 9404	. . . . . . . . . . 11 $/\$ Λ ψ
68	62, 51	mulcld 9398	. . . . . . . . . . 11 $/\$ Λ
69	47, 67, 68	subdid 9792	. . . . . . . . . 10 $/\$ Λ ψ Λ Λ ψ Λ
70	49	recnd 9404	. . . . . . . . . . . . . . 15 $/\$ $/\$ Λ
71	22, 62, 70	fsummulc2 13243	. . . . . . . . . . . . . 14 $/\$ Λ Λ
72	71	oveq2d 6102	. . . . . . . . . . . . 13 $/\$ Λ ψ Λ Λ ψ Λ
73	34	recnd 9404	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ ψ
74	62	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$
75	74, 70	mulcld 9398	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ
76	22, 73, 75	fsumsub 13247	. . . . . . . . . . . . 13 $/\$ Λ ψ Λ Λ ψ Λ
77	72, 76	eqtr4d 2473	. . . . . . . . . . . 12 $/\$ Λ ψ Λ Λ ψ Λ
78	26	recnd 9404	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Λ
79	30	recnd 9404	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ψ
80	33	recnd 9404	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
81	78, 79, 80	mul32d 9571	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Λ ψ Λ ψ
82	24	nncnd 10330	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
83	24	nnne0d 10358	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
84	78, 80, 82, 83	div23d 10136	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ Λ Λ
85	84	oveq2d 6102	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Λ Λ
86	78, 80	mulcld 9398	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ Λ
87	74, 86, 82, 83	div12d 10135	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Λ Λ
88	85, 87	eqtr3d 2472	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Λ Λ
89	81, 88	oveq12d 6104	. . . . . . . . . . . . . . 15 $/\$ $/\$ Λ ψ Λ Λ ψ Λ
90	10	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
91	90, 32	rpdivcld 11036	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
92	54	pntrval 22791	. . . . . . . . . . . . . . . . . 18 ψ
93	91, 92	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ψ
94	93	oveq2d 6102	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Λ Λ ψ
95	28	recnd 9404	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
96	86, 79, 95	subdid 9792	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Λ ψ Λ ψ Λ
97	94, 96	eqtrd 2470	. . . . . . . . . . . . . . 15 $/\$ $/\$ Λ Λ ψ Λ
98	89, 97	eqtr4d 2473	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ ψ Λ Λ
99	55	ffvelrni 5837	. . . . . . . . . . . . . . . . 17
100	91, 99	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
101	100	recnd 9404	. . . . . . . . . . . . . . 15 $/\$ $/\$
102	78, 101, 80	mul32d 9571	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ Λ
103	98, 102	eqtr4d 2473	. . . . . . . . . . . . 13 $/\$ $/\$ Λ ψ Λ Λ
104	103	sumeq2dv 13172	. . . . . . . . . . . 12 $/\$ Λ ψ Λ Λ
105	77, 104	eqtrd 2470	. . . . . . . . . . 11 $/\$ Λ ψ Λ Λ
106	105	oveq2d 6102	. . . . . . . . . 10 $/\$ Λ ψ Λ Λ
107	47, 62, 51	mul12d 9570	. . . . . . . . . . 11 $/\$ Λ Λ
108	107	oveq2d 6102	. . . . . . . . . 10 $/\$ Λ ψ Λ Λ ψ Λ
109	69, 106, 108	3eqtr3rd 2479	. . . . . . . . 9 $/\$ Λ ψ Λ Λ
110	109	oveq2d 6102	. . . . . . . 8 $/\$ Λ ψ Λ Λ
111	66, 110	eqtrd 2470	. . . . . . 7 $/\$ Λ ψ Λ Λ
112	111	oveq1d 6101	. . . . . 6 $/\$ Λ ψ Λ Λ
113	54	pntrval 22791	. . . . . . . . . . . . . 14 ψ
114	10, 113	syl 16	. . . . . . . . . . . . 13 $/\$ ψ
115	114	oveq1d 6101	. . . . . . . . . . . 12 $/\$ ψ
116	16	recnd 9404	. . . . . . . . . . . . 13 $/\$ ψ
117	116, 62, 12	subdird 9793	. . . . . . . . . . . 12 $/\$ ψ ψ
118	115, 117	eqtrd 2470	. . . . . . . . . . 11 $/\$ ψ
119	118	oveq1d 6101	. . . . . . . . . 10 $/\$ Λ ψ ψ Λ ψ
120	17	recnd 9404	. . . . . . . . . . 11 $/\$ ψ
121	62, 12	mulcld 9398	. . . . . . . . . . 11 $/\$
122	120, 60, 121	addsubd 9732	. . . . . . . . . 10 $/\$ ψ Λ ψ ψ Λ ψ
123	119, 122	eqtr4d 2473	. . . . . . . . 9 $/\$ Λ ψ ψ Λ ψ
124	123	oveq1d 6101	. . . . . . . 8 $/\$ Λ ψ ψ Λ ψ
125	37	recnd 9404	. . . . . . . . . 10 $/\$ ψ Λ ψ
126	125, 121, 62, 64	divsubdird 10138	. . . . . . . . 9 $/\$ ψ Λ ψ ψ Λ ψ
127	12, 62, 64	divcan3d 10104	. . . . . . . . . 10 $/\$
128	127	oveq2d 6102	. . . . . . . . 9 $/\$ ψ Λ ψ ψ Λ ψ
129	126, 128	eqtrd 2470	. . . . . . . 8 $/\$ ψ Λ ψ ψ Λ ψ
130	124, 129	eqtrd 2470	. . . . . . 7 $/\$ Λ ψ ψ Λ ψ
131	52, 62, 64	divcan3d 10104	. . . . . . 7 $/\$ Λ Λ
132	130, 131	oveq12d 6104	. . . . . 6 $/\$ Λ ψ Λ ψ Λ ψ Λ
133	65, 112, 132	3eqtr3rd 2479	. . . . 5 $/\$ ψ Λ ψ Λ Λ
134	42, 53, 133	3eqtrrd 2475	. . . 4 $/\$ Λ ψ Λ ψ Λ
135	134	mpteq2dva 4373	. . 3 Λ ψ Λ ψ Λ
136	19, 11	remulcld 9406	. . . . 5 $/\$
137	38, 136	resubcld 9768	. . . 4 $/\$ ψ Λ ψ
138	21, 50	remulcld 9406	. . . . 5 $/\$ Λ
139	138, 11	resubcld 9768	. . . 4 $/\$ Λ
140		selberg3 22788	. . . . 5 ψ Λ ψ
141	140	a1i 11	. . . 4 ψ Λ ψ
142	19	recnd 9404	. . . . . . . 8 $/\$
143	50, 20	rerpdivcld 11046	. . . . . . . . 9 $/\$ Λ
144	143	recnd 9404	. . . . . . . 8 $/\$ Λ
145	11	rehalfcld 10563	. . . . . . . . 9 $/\$
146	145	recnd 9404	. . . . . . . 8 $/\$
147	142, 144, 146	subdid 9792	. . . . . . 7 $/\$ Λ Λ
148	142, 12, 51, 46	div32d 10122	. . . . . . . . 9 $/\$ Λ Λ
149	148	eqcomd 2443	. . . . . . . 8 $/\$ Λ Λ
150		2ne0 10406	. . . . . . . . . 10
151	150	a1i 11	. . . . . . . . 9 $/\$
152	12, 142, 151	divcan2d 10101	. . . . . . . 8 $/\$
153	149, 152	oveq12d 6104	. . . . . . 7 $/\$ Λ Λ
154	147, 153	eqtrd 2470	. . . . . 6 $/\$ Λ Λ
155	154	mpteq2dva 4373	. . . . 5 Λ Λ
156	143, 145	resubcld 9768	. . . . . 6 $/\$ Λ
157		ioossre 11349	. . . . . . . 8
158		o1const 13089	. . . . . . . 8 $/\$
159	157, 44, 158	mp2an 672	. . . . . . 7
160	159	a1i 11	. . . . . 6
161		vmalogdivsum 22768	. . . . . . 7 Λ
162	161	a1i 11	. . . . . 6 Λ
163	19, 156, 160, 162	o1mul2 13094	. . . . 5 Λ
164	155, 163	eqeltrrd 2513	. . . 4 Λ
165	137, 139, 141, 164	o1sub2 13095	. . 3 ψ Λ ψ Λ
166	135, 165	eqeltrd 2512	. 2 Λ
167	166	trud 1378	1 Λ

Colors of variables: wff setvar class

Syntax hints: $/\$ wa 369

wceq 1369

wtru 1370

wcel 1756

wne 2601

wss 3323 class class class wbr 4287

cmpt 4345

cfv 5413 (class class class)co 6086

cc 9272

cr 9273

cc0 9274

c1 9275

caddc 9277

cmul 9279

cpnf 9407

clt 9410

cmin 9587

cdiv 9985

cn 10314

c2 10363

crp 10983

cioo 11292

cfz 11429

cfl 11632

co1 12956

csu 13155

clog 21986 Λcvma 22409 ψcchp 22410

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2419 ax-rep 4398 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367 ax-inf2 7839 ax-cnex 9330 ax-resscn 9331 ax-1cn 9332 ax-icn 9333 ax-addcl 9334 ax-addrcl 9335 ax-mulcl 9336 ax-mulrcl 9337 ax-mulcom 9338 ax-addass 9339 ax-mulass 9340 ax-distr 9341 ax-i2m1 9342 ax-1ne0 9343 ax-1rid 9344 ax-rnegex 9345 ax-rrecex 9346 ax-cnre 9347 ax-pre-lttri 9348 ax-pre-lttrn 9349 ax-pre-ltadd 9350 ax-pre-mulgt0 9351 ax-pre-sup 9352 ax-addf 9353 ax-mulf 9354

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-fal 1375 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-nel 2604 df-ral 2715 df-rex 2716 df-reu 2717 df-rmo 2718 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-pss 3339 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-tp 3877 df-op 3879 df-uni 4087 df-int 4124 df-iun 4168 df-iin 4169 df-disj 4258 df-br 4288 df-opab 4346 df-mpt 4347 df-tr 4381 df-eprel 4627 df-id 4631 df-po 4636 df-so 4637 df-fr 4674 df-se 4675 df-we 4676 df-ord 4717 df-on 4718 df-lim 4719 df-suc 4720 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-riota 6047 df-ov 6089 df-oprab 6090 df-mpt2 6091 df-of 6315 df-om 6472 df-1st 6572 df-2nd 6573 df-supp 6686 df-recs 6824 df-rdg 6858 df-1o 6912 df-2o 6913 df-oadd 6916 df-er 7093 df-map 7208 df-pm 7209 df-ixp 7256 df-en 7303 df-dom 7304 df-sdom 7305 df-fin 7306 df-fsupp 7613 df-fi 7653 df-sup 7683 df-oi 7716 df-card 8101 df-cda 8329 df-pnf 9412 df-mnf 9413 df-xr 9414 df-ltxr 9415 df-le 9416 df-sub 9589 df-neg 9590 df-div 9986 df-nn 10315 df-2 10372 df-3 10373 df-4 10374 df-5 10375 df-6 10376 df-7 10377 df-8 10378 df-9 10379 df-10 10380 df-n0 10572 df-z 10639 df-dec 10748 df-uz 10854 df-q 10946 df-rp 10984 df-xneg 11081 df-xadd 11082 df-xmul 11083 df-ioo 11296 df-ioc 11297 df-ico 11298 df-icc 11299 df-fz 11430 df-fzo 11541 df-fl 11634 df-mod 11701 df-seq 11799 df-exp 11858 df-fac 12044 df-bc 12071 df-hash 12096 df-shft 12548 df-cj 12580 df-re 12581 df-im 12582 df-sqr 12716 df-abs 12717 df-limsup 12941 df-clim 12958 df-rlim 12959 df-o1 12960 df-lo1 12961 df-sum 13156 df-ef 13345 df-e 13346 df-sin 13347 df-cos 13348 df-pi 13350 df-dvds 13528 df-gcd 13683 df-prm 13756 df-pc 13896 df-struct 14168 df-ndx 14169 df-slot 14170 df-base 14171 df-sets 14172 df-ress 14173 df-plusg 14243 df-mulr 14244 df-starv 14245 df-sca 14246 df-vsca 14247 df-ip 14248 df-tset 14249 df-ple 14250 df-ds 14252 df-unif 14253 df-hom 14254 df-cco 14255 df-rest 14353 df-topn 14354 df-0g 14372 df-gsum 14373 df-topgen 14374 df-pt 14375 df-prds 14378 df-xrs 14432 df-qtop 14437 df-imas 14438 df-xps 14440 df-mre 14516 df-mrc 14517 df-acs 14519 df-mnd 15407 df-submnd 15457 df-mulg 15539 df-cntz 15826 df-cmn 16270 df-psmet 17789 df-xmet 17790 df-met 17791 df-bl 17792 df-mopn 17793 df-fbas 17794 df-fg 17795 df-cnfld 17799 df-top 18483 df-bases 18485 df-topon 18486 df-topsp 18487 df-cld 18603 df-ntr 18604 df-cls 18605 df-nei 18682 df-lp 18720 df-perf 18721 df-cn 18811 df-cnp 18812 df-haus 18899 df-cmp 18970 df-tx 19115 df-hmeo 19308 df-fil 19399 df-fm 19491 df-flim 19492 df-flf 19493 df-xms 19875 df-ms 19876 df-tms 19877 df-cncf 20434 df-limc 21321 df-dv 21322 df-log 21988 df-cxp 21989 df-em 22366 df-cht 22414 df-vma 22415 df-chp 22416 df-ppi 22417 df-mu 22418

This theorem is referenced by: selberg34r 22800

W3C validator