selberg3r - Metamath Proof Explorer

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

Theorem selberg3r 23498

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 11558	. . . . . . . . . . . . 13
2	1	adantl 466	. . . . . . . . . . . 12 $/\$
3		1rp 11223	. . . . . . . . . . . . 13
4	3	a1i 11	. . . . . . . . . . . 12 $/\$
5		1red 9610	. . . . . . . . . . . . 13 $/\$
6		eliooord 11583	. . . . . . . . . . . . . . 15 $/\$
7	6	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$
8	7	simpld 459	. . . . . . . . . . . . 13 $/\$
9	5, 2, 8	ltled 9731	. . . . . . . . . . . 12 $/\$
10	2, 4, 9	rpgecld 11290	. . . . . . . . . . 11 $/\$
11	10	relogcld 22752	. . . . . . . . . 10 $/\$
12	11	recnd 9621	. . . . . . . . 9 $/\$
13	12	2timesd 10780	. . . . . . . 8 $/\$
14	13	oveq2d 6299	. . . . . . 7 $/\$ ψ Λ ψ ψ Λ ψ
15		chpcl 23142	. . . . . . . . . . . . 13 ψ
16	2, 15	syl 16	. . . . . . . . . . . 12 $/\$ ψ
17	16, 11	remulcld 9623	. . . . . . . . . . 11 $/\$ ψ
18		2re 10604	. . . . . . . . . . . . . 14
19	18	a1i 11	. . . . . . . . . . . . 13 $/\$
20	2, 8	rplogcld 22758	. . . . . . . . . . . . 13 $/\$
21	19, 20	rerpdivcld 11282	. . . . . . . . . . . 12 $/\$
22		fzfid 12050	. . . . . . . . . . . . 13 $/\$
23		elfznn 11713	. . . . . . . . . . . . . . . . 17
24	23	adantl 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$
25		vmacl 23136	. . . . . . . . . . . . . . . 16 Λ
26	24, 25	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ Λ
27	2	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
28	27, 24	nndivred 10583	. . . . . . . . . . . . . . . 16 $/\$ $/\$
29		chpcl 23142	. . . . . . . . . . . . . . . 16 ψ
30	28, 29	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ ψ
31	26, 30	remulcld 9623	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ ψ
32	24	nnrpd 11254	. . . . . . . . . . . . . . 15 $/\$ $/\$
33	32	relogcld 22752	. . . . . . . . . . . . . 14 $/\$ $/\$
34	31, 33	remulcld 9623	. . . . . . . . . . . . 13 $/\$ $/\$ Λ ψ
35	22, 34	fsumrecl 13518	. . . . . . . . . . . 12 $/\$ Λ ψ
36	21, 35	remulcld 9623	. . . . . . . . . . 11 $/\$ Λ ψ
37	17, 36	readdcld 9622	. . . . . . . . . 10 $/\$ ψ Λ ψ
38	37, 10	rerpdivcld 11282	. . . . . . . . 9 $/\$ ψ Λ ψ
39	38	recnd 9621	. . . . . . . 8 $/\$ ψ Λ ψ
40	39, 12, 12	subsub4d 9960	. . . . . . 7 $/\$ ψ Λ ψ ψ Λ ψ
41	14, 40	eqtr4d 2511	. . . . . 6 $/\$ ψ Λ ψ ψ Λ ψ
42	41	oveq1d 6298	. . . . 5 $/\$ ψ Λ ψ Λ ψ Λ ψ Λ
43	39, 12	subcld 9929	. . . . . 6 $/\$ ψ Λ ψ
44		2cn 10605	. . . . . . . . 9
45	44	a1i 11	. . . . . . . 8 $/\$
46	20	rpne0d 11260	. . . . . . . 8 $/\$
47	45, 12, 46	divcld 10319	. . . . . . 7 $/\$
48	26, 24	nndivred 10583	. . . . . . . . . 10 $/\$ $/\$ Λ
49	48, 33	remulcld 9623	. . . . . . . . 9 $/\$ $/\$ Λ
50	22, 49	fsumrecl 13518	. . . . . . . 8 $/\$ Λ
51	50	recnd 9621	. . . . . . 7 $/\$ Λ
52	47, 51	mulcld 9615	. . . . . 6 $/\$ Λ
53	43, 52, 12	nnncan2d 9964	. . . . 5 $/\$ ψ Λ ψ Λ ψ Λ ψ Λ
54		pntrval.r	. . . . . . . . . . . . 13 ψ
55	54	pntrf 23492	. . . . . . . . . . . 12
56	55	ffvelrni 6019	. . . . . . . . . . 11
57	10, 56	syl 16	. . . . . . . . . 10 $/\$
58	57	recnd 9621	. . . . . . . . 9 $/\$
59	58, 12	mulcld 9615	. . . . . . . 8 $/\$
60	36	recnd 9621	. . . . . . . 8 $/\$ Λ ψ
61	59, 60	addcld 9614	. . . . . . 7 $/\$ Λ ψ
62	2	recnd 9621	. . . . . . . 8 $/\$
63	62, 52	mulcld 9615	. . . . . . 7 $/\$ Λ
64	10	rpne0d 11260	. . . . . . 7 $/\$
65	61, 63, 62, 64	divsubdird 10358	. . . . . 6 $/\$ Λ ψ Λ Λ ψ Λ
66	59, 60, 63	addsubassd 9949	. . . . . . . 8 $/\$ Λ ψ Λ Λ ψ Λ
67	35	recnd 9621	. . . . . . . . . . 11 $/\$ Λ ψ
68	62, 51	mulcld 9615	. . . . . . . . . . 11 $/\$ Λ
69	47, 67, 68	subdid 10011	. . . . . . . . . 10 $/\$ Λ ψ Λ Λ ψ Λ
70	49	recnd 9621	. . . . . . . . . . . . . . 15 $/\$ $/\$ Λ
71	22, 62, 70	fsummulc2 13561	. . . . . . . . . . . . . 14 $/\$ Λ Λ
72	71	oveq2d 6299	. . . . . . . . . . . . 13 $/\$ Λ ψ Λ Λ ψ Λ
73	34	recnd 9621	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ ψ
74	62	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$
75	74, 70	mulcld 9615	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ
76	22, 73, 75	fsumsub 13565	. . . . . . . . . . . . 13 $/\$ Λ ψ Λ Λ ψ Λ
77	72, 76	eqtr4d 2511	. . . . . . . . . . . 12 $/\$ Λ ψ Λ Λ ψ Λ
78	26	recnd 9621	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Λ
79	30	recnd 9621	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ψ
80	33	recnd 9621	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
81	78, 79, 80	mul32d 9788	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Λ ψ Λ ψ
82	24	nncnd 10551	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
83	24	nnne0d 10579	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
84	78, 80, 82, 83	div23d 10356	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ Λ Λ
85	84	oveq2d 6299	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Λ Λ
86	78, 80	mulcld 9615	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ Λ
87	74, 86, 82, 83	div12d 10355	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Λ Λ
88	85, 87	eqtr3d 2510	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Λ Λ
89	81, 88	oveq12d 6301	. . . . . . . . . . . . . . 15 $/\$ $/\$ Λ ψ Λ Λ ψ Λ
90	10	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
91	90, 32	rpdivcld 11272	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
92	54	pntrval 23491	. . . . . . . . . . . . . . . . . 18 ψ
93	91, 92	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ψ
94	93	oveq2d 6299	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Λ Λ ψ
95	28	recnd 9621	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
96	86, 79, 95	subdid 10011	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Λ ψ Λ ψ Λ
97	94, 96	eqtrd 2508	. . . . . . . . . . . . . . 15 $/\$ $/\$ Λ Λ ψ Λ
98	89, 97	eqtr4d 2511	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ ψ Λ Λ
99	55	ffvelrni 6019	. . . . . . . . . . . . . . . . 17
100	91, 99	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
101	100	recnd 9621	. . . . . . . . . . . . . . 15 $/\$ $/\$
102	78, 101, 80	mul32d 9788	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ Λ
103	98, 102	eqtr4d 2511	. . . . . . . . . . . . 13 $/\$ $/\$ Λ ψ Λ Λ
104	103	sumeq2dv 13487	. . . . . . . . . . . 12 $/\$ Λ ψ Λ Λ
105	77, 104	eqtrd 2508	. . . . . . . . . . 11 $/\$ Λ ψ Λ Λ
106	105	oveq2d 6299	. . . . . . . . . 10 $/\$ Λ ψ Λ Λ
107	47, 62, 51	mul12d 9787	. . . . . . . . . . 11 $/\$ Λ Λ
108	107	oveq2d 6299	. . . . . . . . . 10 $/\$ Λ ψ Λ Λ ψ Λ
109	69, 106, 108	3eqtr3rd 2517	. . . . . . . . 9 $/\$ Λ ψ Λ Λ
110	109	oveq2d 6299	. . . . . . . 8 $/\$ Λ ψ Λ Λ
111	66, 110	eqtrd 2508	. . . . . . 7 $/\$ Λ ψ Λ Λ
112	111	oveq1d 6298	. . . . . 6 $/\$ Λ ψ Λ Λ
113	54	pntrval 23491	. . . . . . . . . . . . . 14 ψ
114	10, 113	syl 16	. . . . . . . . . . . . 13 $/\$ ψ
115	114	oveq1d 6298	. . . . . . . . . . . 12 $/\$ ψ
116	16	recnd 9621	. . . . . . . . . . . . 13 $/\$ ψ
117	116, 62, 12	subdird 10012	. . . . . . . . . . . 12 $/\$ ψ ψ
118	115, 117	eqtrd 2508	. . . . . . . . . . 11 $/\$ ψ
119	118	oveq1d 6298	. . . . . . . . . 10 $/\$ Λ ψ ψ Λ ψ
120	17	recnd 9621	. . . . . . . . . . 11 $/\$ ψ
121	62, 12	mulcld 9615	. . . . . . . . . . 11 $/\$
122	120, 60, 121	addsubd 9950	. . . . . . . . . 10 $/\$ ψ Λ ψ ψ Λ ψ
123	119, 122	eqtr4d 2511	. . . . . . . . 9 $/\$ Λ ψ ψ Λ ψ
124	123	oveq1d 6298	. . . . . . . 8 $/\$ Λ ψ ψ Λ ψ
125	37	recnd 9621	. . . . . . . . . 10 $/\$ ψ Λ ψ
126	125, 121, 62, 64	divsubdird 10358	. . . . . . . . 9 $/\$ ψ Λ ψ ψ Λ ψ
127	12, 62, 64	divcan3d 10324	. . . . . . . . . 10 $/\$
128	127	oveq2d 6299	. . . . . . . . 9 $/\$ ψ Λ ψ ψ Λ ψ
129	126, 128	eqtrd 2508	. . . . . . . 8 $/\$ ψ Λ ψ ψ Λ ψ
130	124, 129	eqtrd 2508	. . . . . . 7 $/\$ Λ ψ ψ Λ ψ
131	52, 62, 64	divcan3d 10324	. . . . . . 7 $/\$ Λ Λ
132	130, 131	oveq12d 6301	. . . . . 6 $/\$ Λ ψ Λ ψ Λ ψ Λ
133	65, 112, 132	3eqtr3rd 2517	. . . . 5 $/\$ ψ Λ ψ Λ Λ
134	42, 53, 133	3eqtrrd 2513	. . . 4 $/\$ Λ ψ Λ ψ Λ
135	134	mpteq2dva 4533	. . 3 Λ ψ Λ ψ Λ
136	19, 11	remulcld 9623	. . . . 5 $/\$
137	38, 136	resubcld 9986	. . . 4 $/\$ ψ Λ ψ
138	21, 50	remulcld 9623	. . . . 5 $/\$ Λ
139	138, 11	resubcld 9986	. . . 4 $/\$ Λ
140		selberg3 23488	. . . . 5 ψ Λ ψ
141	140	a1i 11	. . . 4 ψ Λ ψ
142	19	recnd 9621	. . . . . . . 8 $/\$
143	50, 20	rerpdivcld 11282	. . . . . . . . 9 $/\$ Λ
144	143	recnd 9621	. . . . . . . 8 $/\$ Λ
145	11	rehalfcld 10784	. . . . . . . . 9 $/\$
146	145	recnd 9621	. . . . . . . 8 $/\$
147	142, 144, 146	subdid 10011	. . . . . . 7 $/\$ Λ Λ
148	142, 12, 51, 46	div32d 10342	. . . . . . . . 9 $/\$ Λ Λ
149	148	eqcomd 2475	. . . . . . . 8 $/\$ Λ Λ
150		2ne0 10627	. . . . . . . . . 10
151	150	a1i 11	. . . . . . . . 9 $/\$
152	12, 142, 151	divcan2d 10321	. . . . . . . 8 $/\$
153	149, 152	oveq12d 6301	. . . . . . 7 $/\$ Λ Λ
154	147, 153	eqtrd 2508	. . . . . 6 $/\$ Λ Λ
155	154	mpteq2dva 4533	. . . . 5 Λ Λ
156	143, 145	resubcld 9986	. . . . . 6 $/\$ Λ
157		ioossre 11585	. . . . . . . 8
158		o1const 13404	. . . . . . . 8 $/\$
159	157, 44, 158	mp2an 672	. . . . . . 7
160	159	a1i 11	. . . . . 6
161		vmalogdivsum 23468	. . . . . . 7 Λ
162	161	a1i 11	. . . . . 6 Λ
163	19, 156, 160, 162	o1mul2 13409	. . . . 5 Λ
164	155, 163	eqeltrrd 2556	. . . 4 Λ
165	137, 139, 141, 164	o1sub2 13410	. . 3 ψ Λ ψ Λ
166	135, 165	eqeltrd 2555	. 2 Λ
167	166	trud 1388	1 Λ

Colors of variables: wff setvar class

Syntax hints: $/\$ wa 369

wceq 1379

wtru 1380

wcel 1767

wne 2662

wss 3476 class class class wbr 4447

cmpt 4505

cfv 5587 (class class class)co 6283

cc 9489

cr 9490

cc0 9491

c1 9492

caddc 9494

cmul 9496

cpnf 9624

clt 9627

cmin 9804

cdiv 10205

cn 10535

c2 10584

crp 11219

cioo 11528

cfz 11671

cfl 11894

co1 13271

csu 13470

clog 22686 Λcvma 23109 ψcchp 23110

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6575 ax-inf2 8057 ax-cnex 9547 ax-resscn 9548 ax-1cn 9549 ax-icn 9550 ax-addcl 9551 ax-addrcl 9552 ax-mulcl 9553 ax-mulrcl 9554 ax-mulcom 9555 ax-addass 9556 ax-mulass 9557 ax-distr 9558 ax-i2m1 9559 ax-1ne0 9560 ax-1rid 9561 ax-rnegex 9562 ax-rrecex 9563 ax-cnre 9564 ax-pre-lttri 9565 ax-pre-lttrn 9566 ax-pre-ltadd 9567 ax-pre-mulgt0 9568 ax-pre-sup 9569 ax-addf 9570 ax-mulf 9571

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-fal 1385 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-iin 4328 df-disj 4418 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-se 4839 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5550 df-fun 5589 df-fn 5590 df-f 5591 df-f1 5592 df-fo 5593 df-f1o 5594 df-fv 5595 df-isom 5596 df-riota 6244 df-ov 6286 df-oprab 6287 df-mpt2 6288 df-of 6523 df-om 6680 df-1st 6784 df-2nd 6785 df-supp 6902 df-recs 7042 df-rdg 7076 df-1o 7130 df-2o 7131 df-oadd 7134 df-er 7311 df-map 7422 df-pm 7423 df-ixp 7470 df-en 7517 df-dom 7518 df-sdom 7519 df-fin 7520 df-fsupp 7829 df-fi 7870 df-sup 7900 df-oi 7934 df-card 8319 df-cda 8547 df-pnf 9629 df-mnf 9630 df-xr 9631 df-ltxr 9632 df-le 9633 df-sub 9806 df-neg 9807 df-div 10206 df-nn 10536 df-2 10593 df-3 10594 df-4 10595 df-5 10596 df-6 10597 df-7 10598 df-8 10599 df-9 10600 df-10 10601 df-n0 10795 df-z 10864 df-dec 10976 df-uz 11082 df-q 11182 df-rp 11220 df-xneg 11317 df-xadd 11318 df-xmul 11319 df-ioo 11532 df-ioc 11533 df-ico 11534 df-icc 11535 df-fz 11672 df-fzo 11792 df-fl 11896 df-mod 11964 df-seq 12075 df-exp 12134 df-fac 12321 df-bc 12348 df-hash 12373 df-shft 12862 df-cj 12894 df-re 12895 df-im 12896 df-sqrt 13030 df-abs 13031 df-limsup 13256 df-clim 13273 df-rlim 13274 df-o1 13275 df-lo1 13276 df-sum 13471 df-ef 13664 df-e 13665 df-sin 13666 df-cos 13667 df-pi 13669 df-dvds 13847 df-gcd 14003 df-prm 14076 df-pc 14219 df-struct 14491 df-ndx 14492 df-slot 14493 df-base 14494 df-sets 14495 df-ress 14496 df-plusg 14567 df-mulr 14568 df-starv 14569 df-sca 14570 df-vsca 14571 df-ip 14572 df-tset 14573 df-ple 14574 df-ds 14576 df-unif 14577 df-hom 14578 df-cco 14579 df-rest 14677 df-topn 14678 df-0g 14696 df-gsum 14697 df-topgen 14698 df-pt 14699 df-prds 14702 df-xrs 14756 df-qtop 14761 df-imas 14762 df-xps 14764 df-mre 14840 df-mrc 14841 df-acs 14843 df-mnd 15731 df-submnd 15784 df-mulg 15867 df-cntz 16157 df-cmn 16603 df-psmet 18198 df-xmet 18199 df-met 18200 df-bl 18201 df-mopn 18202 df-fbas 18203 df-fg 18204 df-cnfld 18208 df-top 19182 df-bases 19184 df-topon 19185 df-topsp 19186 df-cld 19302 df-ntr 19303 df-cls 19304 df-nei 19381 df-lp 19419 df-perf 19420 df-cn 19510 df-cnp 19511 df-haus 19598 df-cmp 19669 df-tx 19814 df-hmeo 20007 df-fil 20098 df-fm 20190 df-flim 20191 df-flf 20192 df-xms 20574 df-ms 20575 df-tms 20576 df-cncf 21133 df-limc 22021 df-dv 22022 df-log 22688 df-cxp 22689 df-em 23066 df-cht 23114 df-vma 23115 df-chp 23116 df-ppi 23117 df-mu 23118

This theorem is referenced by: selberg34r 23500

W3C validator