selberg3r - Metamath Proof Explorer

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

Theorem selberg3r 24486

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 11691	. . . . . . . . . . . . 13
2	1	adantl 473	. . . . . . . . . . . 12 $/\$
3		1rp 11329	. . . . . . . . . . . . 13
4	3	a1i 11	. . . . . . . . . . . 12 $/\$
5		1red 9676	. . . . . . . . . . . . 13 $/\$
6		eliooord 11719	. . . . . . . . . . . . . . 15 $/\$
7	6	adantl 473	. . . . . . . . . . . . . 14 $/\$ $/\$
8	7	simpld 466	. . . . . . . . . . . . 13 $/\$
9	5, 2, 8	ltled 9800	. . . . . . . . . . . 12 $/\$
10	2, 4, 9	rpgecld 11400	. . . . . . . . . . 11 $/\$
11	10	relogcld 23651	. . . . . . . . . 10 $/\$
12	11	recnd 9687	. . . . . . . . 9 $/\$
13	12	2timesd 10878	. . . . . . . 8 $/\$
14	13	oveq2d 6324	. . . . . . 7 $/\$ ψ Λ ψ ψ Λ ψ
15		chpcl 24130	. . . . . . . . . . . . 13 ψ
16	2, 15	syl 17	. . . . . . . . . . . 12 $/\$ ψ
17	16, 11	remulcld 9689	. . . . . . . . . . 11 $/\$ ψ
18		2re 10701	. . . . . . . . . . . . . 14
19	18	a1i 11	. . . . . . . . . . . . 13 $/\$
20	2, 8	rplogcld 23657	. . . . . . . . . . . . 13 $/\$
21	19, 20	rerpdivcld 11392	. . . . . . . . . . . 12 $/\$
22		fzfid 12224	. . . . . . . . . . . . 13 $/\$
23		elfznn 11854	. . . . . . . . . . . . . . . . 17
24	23	adantl 473	. . . . . . . . . . . . . . . 16 $/\$ $/\$
25		vmacl 24124	. . . . . . . . . . . . . . . 16 Λ
26	24, 25	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ Λ
27	2	adantr 472	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
28	27, 24	nndivred 10680	. . . . . . . . . . . . . . . 16 $/\$ $/\$
29		chpcl 24130	. . . . . . . . . . . . . . . 16 ψ
30	28, 29	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ ψ
31	26, 30	remulcld 9689	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ ψ
32	24	nnrpd 11362	. . . . . . . . . . . . . . 15 $/\$ $/\$
33	32	relogcld 23651	. . . . . . . . . . . . . 14 $/\$ $/\$
34	31, 33	remulcld 9689	. . . . . . . . . . . . 13 $/\$ $/\$ Λ ψ
35	22, 34	fsumrecl 13877	. . . . . . . . . . . 12 $/\$ Λ ψ
36	21, 35	remulcld 9689	. . . . . . . . . . 11 $/\$ Λ ψ
37	17, 36	readdcld 9688	. . . . . . . . . 10 $/\$ ψ Λ ψ
38	37, 10	rerpdivcld 11392	. . . . . . . . 9 $/\$ ψ Λ ψ
39	38	recnd 9687	. . . . . . . 8 $/\$ ψ Λ ψ
40	39, 12, 12	subsub4d 10036	. . . . . . 7 $/\$ ψ Λ ψ ψ Λ ψ
41	14, 40	eqtr4d 2508	. . . . . 6 $/\$ ψ Λ ψ ψ Λ ψ
42	41	oveq1d 6323	. . . . 5 $/\$ ψ Λ ψ Λ ψ Λ ψ Λ
43	39, 12	subcld 10005	. . . . . 6 $/\$ ψ Λ ψ
44		2cn 10702	. . . . . . . . 9
45	44	a1i 11	. . . . . . . 8 $/\$
46	20	rpne0d 11369	. . . . . . . 8 $/\$
47	45, 12, 46	divcld 10405	. . . . . . 7 $/\$
48	26, 24	nndivred 10680	. . . . . . . . . 10 $/\$ $/\$ Λ
49	48, 33	remulcld 9689	. . . . . . . . 9 $/\$ $/\$ Λ
50	22, 49	fsumrecl 13877	. . . . . . . 8 $/\$ Λ
51	50	recnd 9687	. . . . . . 7 $/\$ Λ
52	47, 51	mulcld 9681	. . . . . 6 $/\$ Λ
53	43, 52, 12	nnncan2d 10040	. . . . 5 $/\$ ψ Λ ψ Λ ψ Λ ψ Λ
54		pntrval.r	. . . . . . . . . . . . 13 ψ
55	54	pntrf 24480	. . . . . . . . . . . 12
56	55	ffvelrni 6036	. . . . . . . . . . 11
57	10, 56	syl 17	. . . . . . . . . 10 $/\$
58	57	recnd 9687	. . . . . . . . 9 $/\$
59	58, 12	mulcld 9681	. . . . . . . 8 $/\$
60	36	recnd 9687	. . . . . . . 8 $/\$ Λ ψ
61	59, 60	addcld 9680	. . . . . . 7 $/\$ Λ ψ
62	2	recnd 9687	. . . . . . . 8 $/\$
63	62, 52	mulcld 9681	. . . . . . 7 $/\$ Λ
64	10	rpne0d 11369	. . . . . . 7 $/\$
65	61, 63, 62, 64	divsubdird 10444	. . . . . 6 $/\$ Λ ψ Λ Λ ψ Λ
66	59, 60, 63	addsubassd 10025	. . . . . . . 8 $/\$ Λ ψ Λ Λ ψ Λ
67	35	recnd 9687	. . . . . . . . . . 11 $/\$ Λ ψ
68	62, 51	mulcld 9681	. . . . . . . . . . 11 $/\$ Λ
69	47, 67, 68	subdid 10095	. . . . . . . . . 10 $/\$ Λ ψ Λ Λ ψ Λ
70	49	recnd 9687	. . . . . . . . . . . . . . 15 $/\$ $/\$ Λ
71	22, 62, 70	fsummulc2 13922	. . . . . . . . . . . . . 14 $/\$ Λ Λ
72	71	oveq2d 6324	. . . . . . . . . . . . 13 $/\$ Λ ψ Λ Λ ψ Λ
73	34	recnd 9687	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ ψ
74	62	adantr 472	. . . . . . . . . . . . . . 15 $/\$ $/\$
75	74, 70	mulcld 9681	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ
76	22, 73, 75	fsumsub 13926	. . . . . . . . . . . . 13 $/\$ Λ ψ Λ Λ ψ Λ
77	72, 76	eqtr4d 2508	. . . . . . . . . . . 12 $/\$ Λ ψ Λ Λ ψ Λ
78	26	recnd 9687	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Λ
79	30	recnd 9687	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ψ
80	33	recnd 9687	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
81	78, 79, 80	mul32d 9861	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Λ ψ Λ ψ
82	24	nncnd 10647	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
83	24	nnne0d 10676	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
84	78, 80, 82, 83	div23d 10442	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ Λ Λ
85	84	oveq2d 6324	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Λ Λ
86	78, 80	mulcld 9681	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ Λ
87	74, 86, 82, 83	div12d 10441	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Λ Λ
88	85, 87	eqtr3d 2507	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Λ Λ
89	81, 88	oveq12d 6326	. . . . . . . . . . . . . . 15 $/\$ $/\$ Λ ψ Λ Λ ψ Λ
90	10	adantr 472	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
91	90, 32	rpdivcld 11381	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
92	54	pntrval 24479	. . . . . . . . . . . . . . . . . 18 ψ
93	91, 92	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ψ
94	93	oveq2d 6324	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Λ Λ ψ
95	28	recnd 9687	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
96	86, 79, 95	subdid 10095	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Λ ψ Λ ψ Λ
97	94, 96	eqtrd 2505	. . . . . . . . . . . . . . 15 $/\$ $/\$ Λ Λ ψ Λ
98	89, 97	eqtr4d 2508	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ ψ Λ Λ
99	55	ffvelrni 6036	. . . . . . . . . . . . . . . . 17
100	91, 99	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
101	100	recnd 9687	. . . . . . . . . . . . . . 15 $/\$ $/\$
102	78, 101, 80	mul32d 9861	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ Λ
103	98, 102	eqtr4d 2508	. . . . . . . . . . . . 13 $/\$ $/\$ Λ ψ Λ Λ
104	103	sumeq2dv 13846	. . . . . . . . . . . 12 $/\$ Λ ψ Λ Λ
105	77, 104	eqtrd 2505	. . . . . . . . . . 11 $/\$ Λ ψ Λ Λ
106	105	oveq2d 6324	. . . . . . . . . 10 $/\$ Λ ψ Λ Λ
107	47, 62, 51	mul12d 9860	. . . . . . . . . . 11 $/\$ Λ Λ
108	107	oveq2d 6324	. . . . . . . . . 10 $/\$ Λ ψ Λ Λ ψ Λ
109	69, 106, 108	3eqtr3rd 2514	. . . . . . . . 9 $/\$ Λ ψ Λ Λ
110	109	oveq2d 6324	. . . . . . . 8 $/\$ Λ ψ Λ Λ
111	66, 110	eqtrd 2505	. . . . . . 7 $/\$ Λ ψ Λ Λ
112	111	oveq1d 6323	. . . . . 6 $/\$ Λ ψ Λ Λ
113	54	pntrval 24479	. . . . . . . . . . . . . 14 ψ
114	10, 113	syl 17	. . . . . . . . . . . . 13 $/\$ ψ
115	114	oveq1d 6323	. . . . . . . . . . . 12 $/\$ ψ
116	16	recnd 9687	. . . . . . . . . . . . 13 $/\$ ψ
117	116, 62, 12	subdird 10096	. . . . . . . . . . . 12 $/\$ ψ ψ
118	115, 117	eqtrd 2505	. . . . . . . . . . 11 $/\$ ψ
119	118	oveq1d 6323	. . . . . . . . . 10 $/\$ Λ ψ ψ Λ ψ
120	17	recnd 9687	. . . . . . . . . . 11 $/\$ ψ
121	62, 12	mulcld 9681	. . . . . . . . . . 11 $/\$
122	120, 60, 121	addsubd 10026	. . . . . . . . . 10 $/\$ ψ Λ ψ ψ Λ ψ
123	119, 122	eqtr4d 2508	. . . . . . . . 9 $/\$ Λ ψ ψ Λ ψ
124	123	oveq1d 6323	. . . . . . . 8 $/\$ Λ ψ ψ Λ ψ
125	37	recnd 9687	. . . . . . . . . 10 $/\$ ψ Λ ψ
126	125, 121, 62, 64	divsubdird 10444	. . . . . . . . 9 $/\$ ψ Λ ψ ψ Λ ψ
127	12, 62, 64	divcan3d 10410	. . . . . . . . . 10 $/\$
128	127	oveq2d 6324	. . . . . . . . 9 $/\$ ψ Λ ψ ψ Λ ψ
129	126, 128	eqtrd 2505	. . . . . . . 8 $/\$ ψ Λ ψ ψ Λ ψ
130	124, 129	eqtrd 2505	. . . . . . 7 $/\$ Λ ψ ψ Λ ψ
131	52, 62, 64	divcan3d 10410	. . . . . . 7 $/\$ Λ Λ
132	130, 131	oveq12d 6326	. . . . . 6 $/\$ Λ ψ Λ ψ Λ ψ Λ
133	65, 112, 132	3eqtr3rd 2514	. . . . 5 $/\$ ψ Λ ψ Λ Λ
134	42, 53, 133	3eqtrrd 2510	. . . 4 $/\$ Λ ψ Λ ψ Λ
135	134	mpteq2dva 4482	. . 3 Λ ψ Λ ψ Λ
136	19, 11	remulcld 9689	. . . . 5 $/\$
137	38, 136	resubcld 10068	. . . 4 $/\$ ψ Λ ψ
138	21, 50	remulcld 9689	. . . . 5 $/\$ Λ
139	138, 11	resubcld 10068	. . . 4 $/\$ Λ
140		selberg3 24476	. . . . 5 ψ Λ ψ
141	140	a1i 11	. . . 4 ψ Λ ψ
142	19	recnd 9687	. . . . . . . 8 $/\$
143	50, 20	rerpdivcld 11392	. . . . . . . . 9 $/\$ Λ
144	143	recnd 9687	. . . . . . . 8 $/\$ Λ
145	11	rehalfcld 10882	. . . . . . . . 9 $/\$
146	145	recnd 9687	. . . . . . . 8 $/\$
147	142, 144, 146	subdid 10095	. . . . . . 7 $/\$ Λ Λ
148	142, 12, 51, 46	div32d 10428	. . . . . . . . 9 $/\$ Λ Λ
149	148	eqcomd 2477	. . . . . . . 8 $/\$ Λ Λ
150		2ne0 10724	. . . . . . . . . 10
151	150	a1i 11	. . . . . . . . 9 $/\$
152	12, 142, 151	divcan2d 10407	. . . . . . . 8 $/\$
153	149, 152	oveq12d 6326	. . . . . . 7 $/\$ Λ Λ
154	147, 153	eqtrd 2505	. . . . . 6 $/\$ Λ Λ
155	154	mpteq2dva 4482	. . . . 5 Λ Λ
156	143, 145	resubcld 10068	. . . . . 6 $/\$ Λ
157		ioossre 11721	. . . . . . . 8
158		o1const 13760	. . . . . . . 8 $/\$
159	157, 44, 158	mp2an 686	. . . . . . 7
160	159	a1i 11	. . . . . 6
161		vmalogdivsum 24456	. . . . . . 7 Λ
162	161	a1i 11	. . . . . 6 Λ
163	19, 156, 160, 162	o1mul2 13765	. . . . 5 Λ
164	155, 163	eqeltrrd 2550	. . . 4 Λ
165	137, 139, 141, 164	o1sub2 13766	. . 3 ψ Λ ψ Λ
166	135, 165	eqeltrd 2549	. 2 Λ
167	166	trud 1461	1 Λ

Colors of variables: wff setvar class

Syntax hints: $/\$ wa 376

wceq 1452

wtru 1453

wcel 1904

wne 2641

wss 3390 class class class wbr 4395

cmpt 4454

cfv 5589 (class class class)co 6308

cc 9555

cr 9556

cc0 9557

c1 9558

caddc 9560

cmul 9562

cpnf 9690

clt 9693

cmin 9880

cdiv 10291

cn 10631

c2 10681

crp 11325

cioo 11660

cfz 11810

cfl 12059

co1 13627

csu 13829

clog 23583 Λcvma 24097 ψcchp 24098

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-inf2 8164 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635 ax-addf 9636 ax-mulf 9637

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-fal 1458 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-iin 4272 df-disj 4367 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-of 6550 df-om 6712 df-1st 6812 df-2nd 6813 df-supp 6934 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-2o 7201 df-oadd 7204 df-er 7381 df-map 7492 df-pm 7493 df-ixp 7541 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-fsupp 7902 df-fi 7943 df-sup 7974 df-inf 7975 df-oi 8043 df-card 8391 df-cda 8616 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-4 10692 df-5 10693 df-6 10694 df-7 10695 df-8 10696 df-9 10697 df-10 10698 df-n0 10894 df-z 10962 df-dec 11075 df-uz 11183 df-q 11288 df-rp 11326 df-xneg 11432 df-xadd 11433 df-xmul 11434 df-ioo 11664 df-ioc 11665 df-ico 11666 df-icc 11667 df-fz 11811 df-fzo 11943 df-fl 12061 df-mod 12130 df-seq 12252 df-exp 12311 df-fac 12498 df-bc 12526 df-hash 12554 df-shft 13207 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 df-limsup 13603 df-clim 13629 df-rlim 13630 df-o1 13631 df-lo1 13632 df-sum 13830 df-ef 14198 df-e 14199 df-sin 14200 df-cos 14201 df-pi 14203 df-dvds 14383 df-gcd 14548 df-prm 14702 df-pc 14866 df-struct 15201 df-ndx 15202 df-slot 15203 df-base 15204 df-sets 15205 df-ress 15206 df-plusg 15281 df-mulr 15282 df-starv 15283 df-sca 15284 df-vsca 15285 df-ip 15286 df-tset 15287 df-ple 15288 df-ds 15290 df-unif 15291 df-hom 15292 df-cco 15293 df-rest 15399 df-topn 15400 df-0g 15418 df-gsum 15419 df-topgen 15420 df-pt 15421 df-prds 15424 df-xrs 15478 df-qtop 15484 df-imas 15485 df-xps 15488 df-mre 15570 df-mrc 15571 df-acs 15573 df-mgm 16566 df-sgrp 16605 df-mnd 16615 df-submnd 16661 df-mulg 16754 df-cntz 17049 df-cmn 17510 df-psmet 19039 df-xmet 19040 df-met 19041 df-bl 19042 df-mopn 19043 df-fbas 19044 df-fg 19045 df-cnfld 19048 df-top 19998 df-bases 19999 df-topon 20000 df-topsp 20001 df-cld 20111 df-ntr 20112 df-cls 20113 df-nei 20191 df-lp 20229 df-perf 20230 df-cn 20320 df-cnp 20321 df-haus 20408 df-cmp 20479 df-tx 20654 df-hmeo 20847 df-fil 20939 df-fm 21031 df-flim 21032 df-flf 21033 df-xms 21413 df-ms 21414 df-tms 21415 df-cncf 21988 df-limc 22900 df-dv 22901 df-log 23585 df-cxp 23586 df-em 23997 df-cht 24102 df-vma 24103 df-chp 24104 df-ppi 24105 df-mu 24106

This theorem is referenced by: selberg34r 24488

W3C validator