selberg3r - Metamath Proof Explorer

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

Theorem selberg3r 23880

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 11584	. . . . . . . . . . . . 13
2	1	adantl 466	. . . . . . . . . . . 12 $/\$
3		1rp 11249	. . . . . . . . . . . . 13
4	3	a1i 11	. . . . . . . . . . . 12 $/\$
5		1red 9628	. . . . . . . . . . . . 13 $/\$
6		eliooord 11609	. . . . . . . . . . . . . . 15 $/\$
7	6	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$
8	7	simpld 459	. . . . . . . . . . . . 13 $/\$
9	5, 2, 8	ltled 9750	. . . . . . . . . . . 12 $/\$
10	2, 4, 9	rpgecld 11316	. . . . . . . . . . 11 $/\$
11	10	relogcld 23134	. . . . . . . . . 10 $/\$
12	11	recnd 9639	. . . . . . . . 9 $/\$
13	12	2timesd 10802	. . . . . . . 8 $/\$
14	13	oveq2d 6312	. . . . . . 7 $/\$ ψ Λ ψ ψ Λ ψ
15		chpcl 23524	. . . . . . . . . . . . 13 ψ
16	2, 15	syl 16	. . . . . . . . . . . 12 $/\$ ψ
17	16, 11	remulcld 9641	. . . . . . . . . . 11 $/\$ ψ
18		2re 10626	. . . . . . . . . . . . . 14
19	18	a1i 11	. . . . . . . . . . . . 13 $/\$
20	2, 8	rplogcld 23140	. . . . . . . . . . . . 13 $/\$
21	19, 20	rerpdivcld 11308	. . . . . . . . . . . 12 $/\$
22		fzfid 12086	. . . . . . . . . . . . 13 $/\$
23		elfznn 11739	. . . . . . . . . . . . . . . . 17
24	23	adantl 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$
25		vmacl 23518	. . . . . . . . . . . . . . . 16 Λ
26	24, 25	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ Λ
27	2	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
28	27, 24	nndivred 10605	. . . . . . . . . . . . . . . 16 $/\$ $/\$
29		chpcl 23524	. . . . . . . . . . . . . . . 16 ψ
30	28, 29	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ ψ
31	26, 30	remulcld 9641	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ ψ
32	24	nnrpd 11280	. . . . . . . . . . . . . . 15 $/\$ $/\$
33	32	relogcld 23134	. . . . . . . . . . . . . 14 $/\$ $/\$
34	31, 33	remulcld 9641	. . . . . . . . . . . . 13 $/\$ $/\$ Λ ψ
35	22, 34	fsumrecl 13568	. . . . . . . . . . . 12 $/\$ Λ ψ
36	21, 35	remulcld 9641	. . . . . . . . . . 11 $/\$ Λ ψ
37	17, 36	readdcld 9640	. . . . . . . . . 10 $/\$ ψ Λ ψ
38	37, 10	rerpdivcld 11308	. . . . . . . . 9 $/\$ ψ Λ ψ
39	38	recnd 9639	. . . . . . . 8 $/\$ ψ Λ ψ
40	39, 12, 12	subsub4d 9981	. . . . . . 7 $/\$ ψ Λ ψ ψ Λ ψ
41	14, 40	eqtr4d 2501	. . . . . 6 $/\$ ψ Λ ψ ψ Λ ψ
42	41	oveq1d 6311	. . . . 5 $/\$ ψ Λ ψ Λ ψ Λ ψ Λ
43	39, 12	subcld 9950	. . . . . 6 $/\$ ψ Λ ψ
44		2cn 10627	. . . . . . . . 9
45	44	a1i 11	. . . . . . . 8 $/\$
46	20	rpne0d 11286	. . . . . . . 8 $/\$
47	45, 12, 46	divcld 10341	. . . . . . 7 $/\$
48	26, 24	nndivred 10605	. . . . . . . . . 10 $/\$ $/\$ Λ
49	48, 33	remulcld 9641	. . . . . . . . 9 $/\$ $/\$ Λ
50	22, 49	fsumrecl 13568	. . . . . . . 8 $/\$ Λ
51	50	recnd 9639	. . . . . . 7 $/\$ Λ
52	47, 51	mulcld 9633	. . . . . 6 $/\$ Λ
53	43, 52, 12	nnncan2d 9985	. . . . 5 $/\$ ψ Λ ψ Λ ψ Λ ψ Λ
54		pntrval.r	. . . . . . . . . . . . 13 ψ
55	54	pntrf 23874	. . . . . . . . . . . 12
56	55	ffvelrni 6031	. . . . . . . . . . 11
57	10, 56	syl 16	. . . . . . . . . 10 $/\$
58	57	recnd 9639	. . . . . . . . 9 $/\$
59	58, 12	mulcld 9633	. . . . . . . 8 $/\$
60	36	recnd 9639	. . . . . . . 8 $/\$ Λ ψ
61	59, 60	addcld 9632	. . . . . . 7 $/\$ Λ ψ
62	2	recnd 9639	. . . . . . . 8 $/\$
63	62, 52	mulcld 9633	. . . . . . 7 $/\$ Λ
64	10	rpne0d 11286	. . . . . . 7 $/\$
65	61, 63, 62, 64	divsubdird 10380	. . . . . 6 $/\$ Λ ψ Λ Λ ψ Λ
66	59, 60, 63	addsubassd 9970	. . . . . . . 8 $/\$ Λ ψ Λ Λ ψ Λ
67	35	recnd 9639	. . . . . . . . . . 11 $/\$ Λ ψ
68	62, 51	mulcld 9633	. . . . . . . . . . 11 $/\$ Λ
69	47, 67, 68	subdid 10033	. . . . . . . . . 10 $/\$ Λ ψ Λ Λ ψ Λ
70	49	recnd 9639	. . . . . . . . . . . . . . 15 $/\$ $/\$ Λ
71	22, 62, 70	fsummulc2 13611	. . . . . . . . . . . . . 14 $/\$ Λ Λ
72	71	oveq2d 6312	. . . . . . . . . . . . 13 $/\$ Λ ψ Λ Λ ψ Λ
73	34	recnd 9639	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ ψ
74	62	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$
75	74, 70	mulcld 9633	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ
76	22, 73, 75	fsumsub 13615	. . . . . . . . . . . . 13 $/\$ Λ ψ Λ Λ ψ Λ
77	72, 76	eqtr4d 2501	. . . . . . . . . . . 12 $/\$ Λ ψ Λ Λ ψ Λ
78	26	recnd 9639	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Λ
79	30	recnd 9639	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ψ
80	33	recnd 9639	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
81	78, 79, 80	mul32d 9807	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Λ ψ Λ ψ
82	24	nncnd 10572	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
83	24	nnne0d 10601	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
84	78, 80, 82, 83	div23d 10378	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ Λ Λ
85	84	oveq2d 6312	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Λ Λ
86	78, 80	mulcld 9633	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ Λ
87	74, 86, 82, 83	div12d 10377	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Λ Λ
88	85, 87	eqtr3d 2500	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Λ Λ
89	81, 88	oveq12d 6314	. . . . . . . . . . . . . . 15 $/\$ $/\$ Λ ψ Λ Λ ψ Λ
90	10	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
91	90, 32	rpdivcld 11298	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
92	54	pntrval 23873	. . . . . . . . . . . . . . . . . 18 ψ
93	91, 92	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ψ
94	93	oveq2d 6312	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Λ Λ ψ
95	28	recnd 9639	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
96	86, 79, 95	subdid 10033	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Λ ψ Λ ψ Λ
97	94, 96	eqtrd 2498	. . . . . . . . . . . . . . 15 $/\$ $/\$ Λ Λ ψ Λ
98	89, 97	eqtr4d 2501	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ ψ Λ Λ
99	55	ffvelrni 6031	. . . . . . . . . . . . . . . . 17
100	91, 99	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
101	100	recnd 9639	. . . . . . . . . . . . . . 15 $/\$ $/\$
102	78, 101, 80	mul32d 9807	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ Λ
103	98, 102	eqtr4d 2501	. . . . . . . . . . . . 13 $/\$ $/\$ Λ ψ Λ Λ
104	103	sumeq2dv 13537	. . . . . . . . . . . 12 $/\$ Λ ψ Λ Λ
105	77, 104	eqtrd 2498	. . . . . . . . . . 11 $/\$ Λ ψ Λ Λ
106	105	oveq2d 6312	. . . . . . . . . 10 $/\$ Λ ψ Λ Λ
107	47, 62, 51	mul12d 9806	. . . . . . . . . . 11 $/\$ Λ Λ
108	107	oveq2d 6312	. . . . . . . . . 10 $/\$ Λ ψ Λ Λ ψ Λ
109	69, 106, 108	3eqtr3rd 2507	. . . . . . . . 9 $/\$ Λ ψ Λ Λ
110	109	oveq2d 6312	. . . . . . . 8 $/\$ Λ ψ Λ Λ
111	66, 110	eqtrd 2498	. . . . . . 7 $/\$ Λ ψ Λ Λ
112	111	oveq1d 6311	. . . . . 6 $/\$ Λ ψ Λ Λ
113	54	pntrval 23873	. . . . . . . . . . . . . 14 ψ
114	10, 113	syl 16	. . . . . . . . . . . . 13 $/\$ ψ
115	114	oveq1d 6311	. . . . . . . . . . . 12 $/\$ ψ
116	16	recnd 9639	. . . . . . . . . . . . 13 $/\$ ψ
117	116, 62, 12	subdird 10034	. . . . . . . . . . . 12 $/\$ ψ ψ
118	115, 117	eqtrd 2498	. . . . . . . . . . 11 $/\$ ψ
119	118	oveq1d 6311	. . . . . . . . . 10 $/\$ Λ ψ ψ Λ ψ
120	17	recnd 9639	. . . . . . . . . . 11 $/\$ ψ
121	62, 12	mulcld 9633	. . . . . . . . . . 11 $/\$
122	120, 60, 121	addsubd 9971	. . . . . . . . . 10 $/\$ ψ Λ ψ ψ Λ ψ
123	119, 122	eqtr4d 2501	. . . . . . . . 9 $/\$ Λ ψ ψ Λ ψ
124	123	oveq1d 6311	. . . . . . . 8 $/\$ Λ ψ ψ Λ ψ
125	37	recnd 9639	. . . . . . . . . 10 $/\$ ψ Λ ψ
126	125, 121, 62, 64	divsubdird 10380	. . . . . . . . 9 $/\$ ψ Λ ψ ψ Λ ψ
127	12, 62, 64	divcan3d 10346	. . . . . . . . . 10 $/\$
128	127	oveq2d 6312	. . . . . . . . 9 $/\$ ψ Λ ψ ψ Λ ψ
129	126, 128	eqtrd 2498	. . . . . . . 8 $/\$ ψ Λ ψ ψ Λ ψ
130	124, 129	eqtrd 2498	. . . . . . 7 $/\$ Λ ψ ψ Λ ψ
131	52, 62, 64	divcan3d 10346	. . . . . . 7 $/\$ Λ Λ
132	130, 131	oveq12d 6314	. . . . . 6 $/\$ Λ ψ Λ ψ Λ ψ Λ
133	65, 112, 132	3eqtr3rd 2507	. . . . 5 $/\$ ψ Λ ψ Λ Λ
134	42, 53, 133	3eqtrrd 2503	. . . 4 $/\$ Λ ψ Λ ψ Λ
135	134	mpteq2dva 4543	. . 3 Λ ψ Λ ψ Λ
136	19, 11	remulcld 9641	. . . . 5 $/\$
137	38, 136	resubcld 10008	. . . 4 $/\$ ψ Λ ψ
138	21, 50	remulcld 9641	. . . . 5 $/\$ Λ
139	138, 11	resubcld 10008	. . . 4 $/\$ Λ
140		selberg3 23870	. . . . 5 ψ Λ ψ
141	140	a1i 11	. . . 4 ψ Λ ψ
142	19	recnd 9639	. . . . . . . 8 $/\$
143	50, 20	rerpdivcld 11308	. . . . . . . . 9 $/\$ Λ
144	143	recnd 9639	. . . . . . . 8 $/\$ Λ
145	11	rehalfcld 10806	. . . . . . . . 9 $/\$
146	145	recnd 9639	. . . . . . . 8 $/\$
147	142, 144, 146	subdid 10033	. . . . . . 7 $/\$ Λ Λ
148	142, 12, 51, 46	div32d 10364	. . . . . . . . 9 $/\$ Λ Λ
149	148	eqcomd 2465	. . . . . . . 8 $/\$ Λ Λ
150		2ne0 10649	. . . . . . . . . 10
151	150	a1i 11	. . . . . . . . 9 $/\$
152	12, 142, 151	divcan2d 10343	. . . . . . . 8 $/\$
153	149, 152	oveq12d 6314	. . . . . . 7 $/\$ Λ Λ
154	147, 153	eqtrd 2498	. . . . . 6 $/\$ Λ Λ
155	154	mpteq2dva 4543	. . . . 5 Λ Λ
156	143, 145	resubcld 10008	. . . . . 6 $/\$ Λ
157		ioossre 11611	. . . . . . . 8
158		o1const 13454	. . . . . . . 8 $/\$
159	157, 44, 158	mp2an 672	. . . . . . 7
160	159	a1i 11	. . . . . 6
161		vmalogdivsum 23850	. . . . . . 7 Λ
162	161	a1i 11	. . . . . 6 Λ
163	19, 156, 160, 162	o1mul2 13459	. . . . 5 Λ
164	155, 163	eqeltrrd 2546	. . . 4 Λ
165	137, 139, 141, 164	o1sub2 13460	. . 3 ψ Λ ψ Λ
166	135, 165	eqeltrd 2545	. 2 Λ
167	166	trud 1404	1 Λ

Colors of variables: wff setvar class

Syntax hints: $/\$ wa 369

wceq 1395

wtru 1396

wcel 1819

wne 2652

wss 3471 class class class wbr 4456

cmpt 4515

cfv 5594 (class class class)co 6296

cc 9507

cr 9508

cc0 9509

c1 9510

caddc 9512

cmul 9514

cpnf 9642

clt 9645

cmin 9824

cdiv 10227

cn 10556

c2 10606

crp 11245

cioo 11554

cfz 11697

cfl 11930

co1 13321

csu 13520

clog 23068 Λcvma 23491 ψcchp 23492

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-inf2 8075 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-pre-sup 9587 ax-addf 9588 ax-mulf 9589

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-fal 1401 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-iin 4335 df-disj 4428 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-se 4848 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-isom 5603 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-of 6539 df-om 6700 df-1st 6799 df-2nd 6800 df-supp 6918 df-recs 7060 df-rdg 7094 df-1o 7148 df-2o 7149 df-oadd 7152 df-er 7329 df-map 7440 df-pm 7441 df-ixp 7489 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-fsupp 7848 df-fi 7889 df-sup 7919 df-oi 7953 df-card 8337 df-cda 8565 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-div 10228 df-nn 10557 df-2 10615 df-3 10616 df-4 10617 df-5 10618 df-6 10619 df-7 10620 df-8 10621 df-9 10622 df-10 10623 df-n0 10817 df-z 10886 df-dec 11001 df-uz 11107 df-q 11208 df-rp 11246 df-xneg 11343 df-xadd 11344 df-xmul 11345 df-ioo 11558 df-ioc 11559 df-ico 11560 df-icc 11561 df-fz 11698 df-fzo 11822 df-fl 11932 df-mod 12000 df-seq 12111 df-exp 12170 df-fac 12357 df-bc 12384 df-hash 12409 df-shft 12912 df-cj 12944 df-re 12945 df-im 12946 df-sqrt 13080 df-abs 13081 df-limsup 13306 df-clim 13323 df-rlim 13324 df-o1 13325 df-lo1 13326 df-sum 13521 df-ef 13815 df-e 13816 df-sin 13817 df-cos 13818 df-pi 13820 df-dvds 13999 df-gcd 14157 df-prm 14230 df-pc 14373 df-struct 14646 df-ndx 14647 df-slot 14648 df-base 14649 df-sets 14650 df-ress 14651 df-plusg 14725 df-mulr 14726 df-starv 14727 df-sca 14728 df-vsca 14729 df-ip 14730 df-tset 14731 df-ple 14732 df-ds 14734 df-unif 14735 df-hom 14736 df-cco 14737 df-rest 14840 df-topn 14841 df-0g 14859 df-gsum 14860 df-topgen 14861 df-pt 14862 df-prds 14865 df-xrs 14919 df-qtop 14924 df-imas 14925 df-xps 14927 df-mre 15003 df-mrc 15004 df-acs 15006 df-mgm 15999 df-sgrp 16038 df-mnd 16048 df-submnd 16094 df-mulg 16187 df-cntz 16482 df-cmn 16927 df-psmet 18538 df-xmet 18539 df-met 18540 df-bl 18541 df-mopn 18542 df-fbas 18543 df-fg 18544 df-cnfld 18548 df-top 19526 df-bases 19528 df-topon 19529 df-topsp 19530 df-cld 19647 df-ntr 19648 df-cls 19649 df-nei 19726 df-lp 19764 df-perf 19765 df-cn 19855 df-cnp 19856 df-haus 19943 df-cmp 20014 df-tx 20189 df-hmeo 20382 df-fil 20473 df-fm 20565 df-flim 20566 df-flf 20567 df-xms 20949 df-ms 20950 df-tms 20951 df-cncf 21508 df-limc 22396 df-dv 22397 df-log 23070 df-cxp 23071 df-em 23448 df-cht 23496 df-vma 23497 df-chp 23498 df-ppi 23499 df-mu 23500

This theorem is referenced by: selberg34r 23882

W3C validator