selberg3r - Metamath Proof Explorer

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

Theorem selberg3r 22703

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 11318	. . . . . . . . . . . . 13
2	1	adantl 463	. . . . . . . . . . . 12 $/\$
3		1rp 10983	. . . . . . . . . . . . 13
4	3	a1i 11	. . . . . . . . . . . 12 $/\$
5		1red 9389	. . . . . . . . . . . . 13 $/\$
6		eliooord 11343	. . . . . . . . . . . . . . 15 $/\$
7	6	adantl 463	. . . . . . . . . . . . . 14 $/\$ $/\$
8	7	simpld 456	. . . . . . . . . . . . 13 $/\$
9	5, 2, 8	ltled 9510	. . . . . . . . . . . 12 $/\$
10	2, 4, 9	rpgecld 11050	. . . . . . . . . . 11 $/\$
11	10	relogcld 21957	. . . . . . . . . 10 $/\$
12	11	recnd 9400	. . . . . . . . 9 $/\$
13	12	2timesd 10555	. . . . . . . 8 $/\$
14	13	oveq2d 6096	. . . . . . 7 $/\$ ψ Λ ψ ψ Λ ψ
15		chpcl 22347	. . . . . . . . . . . . 13 ψ
16	2, 15	syl 16	. . . . . . . . . . . 12 $/\$ ψ
17	16, 11	remulcld 9402	. . . . . . . . . . 11 $/\$ ψ
18		2re 10379	. . . . . . . . . . . . . 14
19	18	a1i 11	. . . . . . . . . . . . 13 $/\$
20	2, 8	rplogcld 21963	. . . . . . . . . . . . 13 $/\$
21	19, 20	rerpdivcld 11042	. . . . . . . . . . . 12 $/\$
22		fzfid 11779	. . . . . . . . . . . . 13 $/\$
23		elfznn 11465	. . . . . . . . . . . . . . . . 17
24	23	adantl 463	. . . . . . . . . . . . . . . 16 $/\$ $/\$
25		vmacl 22341	. . . . . . . . . . . . . . . 16 Λ
26	24, 25	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ Λ
27	2	adantr 462	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
28	27, 24	nndivred 10358	. . . . . . . . . . . . . . . 16 $/\$ $/\$
29		chpcl 22347	. . . . . . . . . . . . . . . 16 ψ
30	28, 29	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ ψ
31	26, 30	remulcld 9402	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ ψ
32	24	nnrpd 11014	. . . . . . . . . . . . . . 15 $/\$ $/\$
33	32	relogcld 21957	. . . . . . . . . . . . . 14 $/\$ $/\$
34	31, 33	remulcld 9402	. . . . . . . . . . . . 13 $/\$ $/\$ Λ ψ
35	22, 34	fsumrecl 13195	. . . . . . . . . . . 12 $/\$ Λ ψ
36	21, 35	remulcld 9402	. . . . . . . . . . 11 $/\$ Λ ψ
37	17, 36	readdcld 9401	. . . . . . . . . 10 $/\$ ψ Λ ψ
38	37, 10	rerpdivcld 11042	. . . . . . . . 9 $/\$ ψ Λ ψ
39	38	recnd 9400	. . . . . . . 8 $/\$ ψ Λ ψ
40	39, 12, 12	subsub4d 9738	. . . . . . 7 $/\$ ψ Λ ψ ψ Λ ψ
41	14, 40	eqtr4d 2468	. . . . . 6 $/\$ ψ Λ ψ ψ Λ ψ
42	41	oveq1d 6095	. . . . 5 $/\$ ψ Λ ψ Λ ψ Λ ψ Λ
43	39, 12	subcld 9707	. . . . . 6 $/\$ ψ Λ ψ
44		2cn 10380	. . . . . . . . 9
45	44	a1i 11	. . . . . . . 8 $/\$
46	20	rpne0d 11020	. . . . . . . 8 $/\$
47	45, 12, 46	divcld 10095	. . . . . . 7 $/\$
48	26, 24	nndivred 10358	. . . . . . . . . 10 $/\$ $/\$ Λ
49	48, 33	remulcld 9402	. . . . . . . . 9 $/\$ $/\$ Λ
50	22, 49	fsumrecl 13195	. . . . . . . 8 $/\$ Λ
51	50	recnd 9400	. . . . . . 7 $/\$ Λ
52	47, 51	mulcld 9394	. . . . . 6 $/\$ Λ
53	43, 52, 12	nnncan2d 9742	. . . . 5 $/\$ ψ Λ ψ Λ ψ Λ ψ Λ
54		pntrval.r	. . . . . . . . . . . . 13 ψ
55	54	pntrf 22697	. . . . . . . . . . . 12
56	55	ffvelrni 5830	. . . . . . . . . . 11
57	10, 56	syl 16	. . . . . . . . . 10 $/\$
58	57	recnd 9400	. . . . . . . . 9 $/\$
59	58, 12	mulcld 9394	. . . . . . . 8 $/\$
60	36	recnd 9400	. . . . . . . 8 $/\$ Λ ψ
61	59, 60	addcld 9393	. . . . . . 7 $/\$ Λ ψ
62	2	recnd 9400	. . . . . . . 8 $/\$
63	62, 52	mulcld 9394	. . . . . . 7 $/\$ Λ
64	10	rpne0d 11020	. . . . . . 7 $/\$
65	61, 63, 62, 64	divsubdird 10134	. . . . . 6 $/\$ Λ ψ Λ Λ ψ Λ
66	59, 60, 63	addsubassd 9727	. . . . . . . 8 $/\$ Λ ψ Λ Λ ψ Λ
67	35	recnd 9400	. . . . . . . . . . 11 $/\$ Λ ψ
68	62, 51	mulcld 9394	. . . . . . . . . . 11 $/\$ Λ
69	47, 67, 68	subdid 9788	. . . . . . . . . 10 $/\$ Λ ψ Λ Λ ψ Λ
70	49	recnd 9400	. . . . . . . . . . . . . . 15 $/\$ $/\$ Λ
71	22, 62, 70	fsummulc2 13234	. . . . . . . . . . . . . 14 $/\$ Λ Λ
72	71	oveq2d 6096	. . . . . . . . . . . . 13 $/\$ Λ ψ Λ Λ ψ Λ
73	34	recnd 9400	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ ψ
74	62	adantr 462	. . . . . . . . . . . . . . 15 $/\$ $/\$
75	74, 70	mulcld 9394	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ
76	22, 73, 75	fsumsub 13238	. . . . . . . . . . . . 13 $/\$ Λ ψ Λ Λ ψ Λ
77	72, 76	eqtr4d 2468	. . . . . . . . . . . 12 $/\$ Λ ψ Λ Λ ψ Λ
78	26	recnd 9400	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Λ
79	30	recnd 9400	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ψ
80	33	recnd 9400	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
81	78, 79, 80	mul32d 9567	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Λ ψ Λ ψ
82	24	nncnd 10326	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
83	24	nnne0d 10354	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
84	78, 80, 82, 83	div23d 10132	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ Λ Λ
85	84	oveq2d 6096	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Λ Λ
86	78, 80	mulcld 9394	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ Λ
87	74, 86, 82, 83	div12d 10131	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Λ Λ
88	85, 87	eqtr3d 2467	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Λ Λ
89	81, 88	oveq12d 6098	. . . . . . . . . . . . . . 15 $/\$ $/\$ Λ ψ Λ Λ ψ Λ
90	10	adantr 462	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
91	90, 32	rpdivcld 11032	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
92	54	pntrval 22696	. . . . . . . . . . . . . . . . . 18 ψ
93	91, 92	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ψ
94	93	oveq2d 6096	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Λ Λ ψ
95	28	recnd 9400	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
96	86, 79, 95	subdid 9788	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Λ ψ Λ ψ Λ
97	94, 96	eqtrd 2465	. . . . . . . . . . . . . . 15 $/\$ $/\$ Λ Λ ψ Λ
98	89, 97	eqtr4d 2468	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ ψ Λ Λ
99	55	ffvelrni 5830	. . . . . . . . . . . . . . . . 17
100	91, 99	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
101	100	recnd 9400	. . . . . . . . . . . . . . 15 $/\$ $/\$
102	78, 101, 80	mul32d 9567	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ Λ
103	98, 102	eqtr4d 2468	. . . . . . . . . . . . 13 $/\$ $/\$ Λ ψ Λ Λ
104	103	sumeq2dv 13164	. . . . . . . . . . . 12 $/\$ Λ ψ Λ Λ
105	77, 104	eqtrd 2465	. . . . . . . . . . 11 $/\$ Λ ψ Λ Λ
106	105	oveq2d 6096	. . . . . . . . . 10 $/\$ Λ ψ Λ Λ
107	47, 62, 51	mul12d 9566	. . . . . . . . . . 11 $/\$ Λ Λ
108	107	oveq2d 6096	. . . . . . . . . 10 $/\$ Λ ψ Λ Λ ψ Λ
109	69, 106, 108	3eqtr3rd 2474	. . . . . . . . 9 $/\$ Λ ψ Λ Λ
110	109	oveq2d 6096	. . . . . . . 8 $/\$ Λ ψ Λ Λ
111	66, 110	eqtrd 2465	. . . . . . 7 $/\$ Λ ψ Λ Λ
112	111	oveq1d 6095	. . . . . 6 $/\$ Λ ψ Λ Λ
113	54	pntrval 22696	. . . . . . . . . . . . . 14 ψ
114	10, 113	syl 16	. . . . . . . . . . . . 13 $/\$ ψ
115	114	oveq1d 6095	. . . . . . . . . . . 12 $/\$ ψ
116	16	recnd 9400	. . . . . . . . . . . . 13 $/\$ ψ
117	116, 62, 12	subdird 9789	. . . . . . . . . . . 12 $/\$ ψ ψ
118	115, 117	eqtrd 2465	. . . . . . . . . . 11 $/\$ ψ
119	118	oveq1d 6095	. . . . . . . . . 10 $/\$ Λ ψ ψ Λ ψ
120	17	recnd 9400	. . . . . . . . . . 11 $/\$ ψ
121	62, 12	mulcld 9394	. . . . . . . . . . 11 $/\$
122	120, 60, 121	addsubd 9728	. . . . . . . . . 10 $/\$ ψ Λ ψ ψ Λ ψ
123	119, 122	eqtr4d 2468	. . . . . . . . 9 $/\$ Λ ψ ψ Λ ψ
124	123	oveq1d 6095	. . . . . . . 8 $/\$ Λ ψ ψ Λ ψ
125	37	recnd 9400	. . . . . . . . . 10 $/\$ ψ Λ ψ
126	125, 121, 62, 64	divsubdird 10134	. . . . . . . . 9 $/\$ ψ Λ ψ ψ Λ ψ
127	12, 62, 64	divcan3d 10100	. . . . . . . . . 10 $/\$
128	127	oveq2d 6096	. . . . . . . . 9 $/\$ ψ Λ ψ ψ Λ ψ
129	126, 128	eqtrd 2465	. . . . . . . 8 $/\$ ψ Λ ψ ψ Λ ψ
130	124, 129	eqtrd 2465	. . . . . . 7 $/\$ Λ ψ ψ Λ ψ
131	52, 62, 64	divcan3d 10100	. . . . . . 7 $/\$ Λ Λ
132	130, 131	oveq12d 6098	. . . . . 6 $/\$ Λ ψ Λ ψ Λ ψ Λ
133	65, 112, 132	3eqtr3rd 2474	. . . . 5 $/\$ ψ Λ ψ Λ Λ
134	42, 53, 133	3eqtrrd 2470	. . . 4 $/\$ Λ ψ Λ ψ Λ
135	134	mpteq2dva 4366	. . 3 Λ ψ Λ ψ Λ
136	19, 11	remulcld 9402	. . . . 5 $/\$
137	38, 136	resubcld 9764	. . . 4 $/\$ ψ Λ ψ
138	21, 50	remulcld 9402	. . . . 5 $/\$ Λ
139	138, 11	resubcld 9764	. . . 4 $/\$ Λ
140		selberg3 22693	. . . . 5 ψ Λ ψ
141	140	a1i 11	. . . 4 ψ Λ ψ
142	19	recnd 9400	. . . . . . . 8 $/\$
143	50, 20	rerpdivcld 11042	. . . . . . . . 9 $/\$ Λ
144	143	recnd 9400	. . . . . . . 8 $/\$ Λ
145	11	rehalfcld 10559	. . . . . . . . 9 $/\$
146	145	recnd 9400	. . . . . . . 8 $/\$
147	142, 144, 146	subdid 9788	. . . . . . 7 $/\$ Λ Λ
148	142, 12, 51, 46	div32d 10118	. . . . . . . . 9 $/\$ Λ Λ
149	148	eqcomd 2438	. . . . . . . 8 $/\$ Λ Λ
150		2ne0 10402	. . . . . . . . . 10
151	150	a1i 11	. . . . . . . . 9 $/\$
152	12, 142, 151	divcan2d 10097	. . . . . . . 8 $/\$
153	149, 152	oveq12d 6098	. . . . . . 7 $/\$ Λ Λ
154	147, 153	eqtrd 2465	. . . . . 6 $/\$ Λ Λ
155	154	mpteq2dva 4366	. . . . 5 Λ Λ
156	143, 145	resubcld 9764	. . . . . 6 $/\$ Λ
157		ioossre 11345	. . . . . . . 8
158		o1const 13081	. . . . . . . 8 $/\$
159	157, 44, 158	mp2an 665	. . . . . . 7
160	159	a1i 11	. . . . . 6
161		vmalogdivsum 22673	. . . . . . 7 Λ
162	161	a1i 11	. . . . . 6 Λ
163	19, 156, 160, 162	o1mul2 13086	. . . . 5 Λ
164	155, 163	eqeltrrd 2508	. . . 4 Λ
165	137, 139, 141, 164	o1sub2 13087	. . 3 ψ Λ ψ Λ
166	135, 165	eqeltrd 2507	. 2 Λ
167	166	trud 1371	1 Λ

Colors of variables: wff setvar class

Syntax hints: $/\$ wa 369

wceq 1362

wtru 1363

wcel 1755

wne 2596

wss 3316 class class class wbr 4280

cmpt 4338

cfv 5406 (class class class)co 6080

cc 9268

cr 9269

cc0 9270

c1 9271

caddc 9273

cmul 9275

cpnf 9403

clt 9406

cmin 9583

cdiv 9981

cn 10310

c2 10359

crp 10979

cioo 11288

cfz 11424

cfl 11624

co1 12948

csu 13147

clog 21891 Λcvma 22314 ψcchp 22315

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1594 ax-4 1605 ax-5 1669 ax-6 1707 ax-7 1727 ax-8 1757 ax-9 1759 ax-10 1774 ax-11 1779 ax-12 1791 ax-13 1942 ax-ext 2414 ax-rep 4391 ax-sep 4401 ax-nul 4409 ax-pow 4458 ax-pr 4519 ax-un 6361 ax-inf2 7835 ax-cnex 9326 ax-resscn 9327 ax-1cn 9328 ax-icn 9329 ax-addcl 9330 ax-addrcl 9331 ax-mulcl 9332 ax-mulrcl 9333 ax-mulcom 9334 ax-addass 9335 ax-mulass 9336 ax-distr 9337 ax-i2m1 9338 ax-1ne0 9339 ax-1rid 9340 ax-rnegex 9341 ax-rrecex 9342 ax-cnre 9343 ax-pre-lttri 9344 ax-pre-lttrn 9345 ax-pre-ltadd 9346 ax-pre-mulgt0 9347 ax-pre-sup 9348 ax-addf 9349 ax-mulf 9350

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 959 df-3an 960 df-tru 1365 df-fal 1368 df-ex 1590 df-nf 1593 df-sb 1700 df-eu 2258 df-mo 2259 df-clab 2420 df-cleq 2426 df-clel 2429 df-nfc 2558 df-ne 2598 df-nel 2599 df-ral 2710 df-rex 2711 df-reu 2712 df-rmo 2713 df-rab 2714 df-v 2964 df-sbc 3176 df-csb 3277 df-dif 3319 df-un 3321 df-in 3323 df-ss 3330 df-pss 3332 df-nul 3626 df-if 3780 df-pw 3850 df-sn 3866 df-pr 3868 df-tp 3870 df-op 3872 df-uni 4080 df-int 4117 df-iun 4161 df-iin 4162 df-disj 4251 df-br 4281 df-opab 4339 df-mpt 4340 df-tr 4374 df-eprel 4619 df-id 4623 df-po 4628 df-so 4629 df-fr 4666 df-se 4667 df-we 4668 df-ord 4709 df-on 4710 df-lim 4711 df-suc 4712 df-xp 4833 df-rel 4834 df-cnv 4835 df-co 4836 df-dm 4837 df-rn 4838 df-res 4839 df-ima 4840 df-iota 5369 df-fun 5408 df-fn 5409 df-f 5410 df-f1 5411 df-fo 5412 df-f1o 5413 df-fv 5414 df-isom 5415 df-riota 6039 df-ov 6083 df-oprab 6084 df-mpt2 6085 df-of 6309 df-om 6466 df-1st 6566 df-2nd 6567 df-supp 6680 df-recs 6818 df-rdg 6852 df-1o 6908 df-2o 6909 df-oadd 6912 df-er 7089 df-map 7204 df-pm 7205 df-ixp 7252 df-en 7299 df-dom 7300 df-sdom 7301 df-fin 7302 df-fsupp 7609 df-fi 7649 df-sup 7679 df-oi 7712 df-card 8097 df-cda 8325 df-pnf 9408 df-mnf 9409 df-xr 9410 df-ltxr 9411 df-le 9412 df-sub 9585 df-neg 9586 df-div 9982 df-nn 10311 df-2 10368 df-3 10369 df-4 10370 df-5 10371 df-6 10372 df-7 10373 df-8 10374 df-9 10375 df-10 10376 df-n0 10568 df-z 10635 df-dec 10744 df-uz 10850 df-q 10942 df-rp 10980 df-xneg 11077 df-xadd 11078 df-xmul 11079 df-ioo 11292 df-ioc 11293 df-ico 11294 df-icc 11295 df-fz 11425 df-fzo 11533 df-fl 11626 df-mod 11693 df-seq 11791 df-exp 11850 df-fac 12036 df-bc 12063 df-hash 12088 df-shft 12540 df-cj 12572 df-re 12573 df-im 12574 df-sqr 12708 df-abs 12709 df-limsup 12933 df-clim 12950 df-rlim 12951 df-o1 12952 df-lo1 12953 df-sum 13148 df-ef 13336 df-e 13337 df-sin 13338 df-cos 13339 df-pi 13341 df-dvds 13519 df-gcd 13674 df-prm 13747 df-pc 13887 df-struct 14159 df-ndx 14160 df-slot 14161 df-base 14162 df-sets 14163 df-ress 14164 df-plusg 14234 df-mulr 14235 df-starv 14236 df-sca 14237 df-vsca 14238 df-ip 14239 df-tset 14240 df-ple 14241 df-ds 14243 df-unif 14244 df-hom 14245 df-cco 14246 df-rest 14344 df-topn 14345 df-0g 14363 df-gsum 14364 df-topgen 14365 df-pt 14366 df-prds 14369 df-xrs 14423 df-qtop 14428 df-imas 14429 df-xps 14431 df-mre 14507 df-mrc 14508 df-acs 14510 df-mnd 15398 df-submnd 15448 df-mulg 15528 df-cntz 15815 df-cmn 16259 df-psmet 17653 df-xmet 17654 df-met 17655 df-bl 17656 df-mopn 17657 df-fbas 17658 df-fg 17659 df-cnfld 17663 df-top 18345 df-bases 18347 df-topon 18348 df-topsp 18349 df-cld 18465 df-ntr 18466 df-cls 18467 df-nei 18544 df-lp 18582 df-perf 18583 df-cn 18673 df-cnp 18674 df-haus 18761 df-cmp 18832 df-tx 18977 df-hmeo 19170 df-fil 19261 df-fm 19353 df-flim 19354 df-flf 19355 df-xms 19737 df-ms 19738 df-tms 19739 df-cncf 20296 df-limc 21183 df-dv 21184 df-log 21893 df-cxp 21894 df-em 22271 df-cht 22319 df-vma 22320 df-chp 22321 df-ppi 22322 df-mu 22323

This theorem is referenced by: selberg34r 22705

W3C validator