selberg3r - Metamath Proof Explorer

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

Theorem selberg3r 22954

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 11444	. . . . . . . . . . . . 13
2	1	adantl 466	. . . . . . . . . . . 12 $/\$
3		1rp 11109	. . . . . . . . . . . . 13
4	3	a1i 11	. . . . . . . . . . . 12 $/\$
5		1red 9515	. . . . . . . . . . . . 13 $/\$
6		eliooord 11469	. . . . . . . . . . . . . . 15 $/\$
7	6	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$
8	7	simpld 459	. . . . . . . . . . . . 13 $/\$
9	5, 2, 8	ltled 9636	. . . . . . . . . . . 12 $/\$
10	2, 4, 9	rpgecld 11176	. . . . . . . . . . 11 $/\$
11	10	relogcld 22208	. . . . . . . . . 10 $/\$
12	11	recnd 9526	. . . . . . . . 9 $/\$
13	12	2timesd 10681	. . . . . . . 8 $/\$
14	13	oveq2d 6219	. . . . . . 7 $/\$ ψ Λ ψ ψ Λ ψ
15		chpcl 22598	. . . . . . . . . . . . 13 ψ
16	2, 15	syl 16	. . . . . . . . . . . 12 $/\$ ψ
17	16, 11	remulcld 9528	. . . . . . . . . . 11 $/\$ ψ
18		2re 10505	. . . . . . . . . . . . . 14
19	18	a1i 11	. . . . . . . . . . . . 13 $/\$
20	2, 8	rplogcld 22214	. . . . . . . . . . . . 13 $/\$
21	19, 20	rerpdivcld 11168	. . . . . . . . . . . 12 $/\$
22		fzfid 11915	. . . . . . . . . . . . 13 $/\$
23		elfznn 11598	. . . . . . . . . . . . . . . . 17
24	23	adantl 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$
25		vmacl 22592	. . . . . . . . . . . . . . . 16 Λ
26	24, 25	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ Λ
27	2	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
28	27, 24	nndivred 10484	. . . . . . . . . . . . . . . 16 $/\$ $/\$
29		chpcl 22598	. . . . . . . . . . . . . . . 16 ψ
30	28, 29	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ ψ
31	26, 30	remulcld 9528	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ ψ
32	24	nnrpd 11140	. . . . . . . . . . . . . . 15 $/\$ $/\$
33	32	relogcld 22208	. . . . . . . . . . . . . 14 $/\$ $/\$
34	31, 33	remulcld 9528	. . . . . . . . . . . . 13 $/\$ $/\$ Λ ψ
35	22, 34	fsumrecl 13332	. . . . . . . . . . . 12 $/\$ Λ ψ
36	21, 35	remulcld 9528	. . . . . . . . . . 11 $/\$ Λ ψ
37	17, 36	readdcld 9527	. . . . . . . . . 10 $/\$ ψ Λ ψ
38	37, 10	rerpdivcld 11168	. . . . . . . . 9 $/\$ ψ Λ ψ
39	38	recnd 9526	. . . . . . . 8 $/\$ ψ Λ ψ
40	39, 12, 12	subsub4d 9864	. . . . . . 7 $/\$ ψ Λ ψ ψ Λ ψ
41	14, 40	eqtr4d 2498	. . . . . 6 $/\$ ψ Λ ψ ψ Λ ψ
42	41	oveq1d 6218	. . . . 5 $/\$ ψ Λ ψ Λ ψ Λ ψ Λ
43	39, 12	subcld 9833	. . . . . 6 $/\$ ψ Λ ψ
44		2cn 10506	. . . . . . . . 9
45	44	a1i 11	. . . . . . . 8 $/\$
46	20	rpne0d 11146	. . . . . . . 8 $/\$
47	45, 12, 46	divcld 10221	. . . . . . 7 $/\$
48	26, 24	nndivred 10484	. . . . . . . . . 10 $/\$ $/\$ Λ
49	48, 33	remulcld 9528	. . . . . . . . 9 $/\$ $/\$ Λ
50	22, 49	fsumrecl 13332	. . . . . . . 8 $/\$ Λ
51	50	recnd 9526	. . . . . . 7 $/\$ Λ
52	47, 51	mulcld 9520	. . . . . 6 $/\$ Λ
53	43, 52, 12	nnncan2d 9868	. . . . 5 $/\$ ψ Λ ψ Λ ψ Λ ψ Λ
54		pntrval.r	. . . . . . . . . . . . 13 ψ
55	54	pntrf 22948	. . . . . . . . . . . 12
56	55	ffvelrni 5954	. . . . . . . . . . 11
57	10, 56	syl 16	. . . . . . . . . 10 $/\$
58	57	recnd 9526	. . . . . . . . 9 $/\$
59	58, 12	mulcld 9520	. . . . . . . 8 $/\$
60	36	recnd 9526	. . . . . . . 8 $/\$ Λ ψ
61	59, 60	addcld 9519	. . . . . . 7 $/\$ Λ ψ
62	2	recnd 9526	. . . . . . . 8 $/\$
63	62, 52	mulcld 9520	. . . . . . 7 $/\$ Λ
64	10	rpne0d 11146	. . . . . . 7 $/\$
65	61, 63, 62, 64	divsubdird 10260	. . . . . 6 $/\$ Λ ψ Λ Λ ψ Λ
66	59, 60, 63	addsubassd 9853	. . . . . . . 8 $/\$ Λ ψ Λ Λ ψ Λ
67	35	recnd 9526	. . . . . . . . . . 11 $/\$ Λ ψ
68	62, 51	mulcld 9520	. . . . . . . . . . 11 $/\$ Λ
69	47, 67, 68	subdid 9914	. . . . . . . . . 10 $/\$ Λ ψ Λ Λ ψ Λ
70	49	recnd 9526	. . . . . . . . . . . . . . 15 $/\$ $/\$ Λ
71	22, 62, 70	fsummulc2 13372	. . . . . . . . . . . . . 14 $/\$ Λ Λ
72	71	oveq2d 6219	. . . . . . . . . . . . 13 $/\$ Λ ψ Λ Λ ψ Λ
73	34	recnd 9526	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ ψ
74	62	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$
75	74, 70	mulcld 9520	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ
76	22, 73, 75	fsumsub 13376	. . . . . . . . . . . . 13 $/\$ Λ ψ Λ Λ ψ Λ
77	72, 76	eqtr4d 2498	. . . . . . . . . . . 12 $/\$ Λ ψ Λ Λ ψ Λ
78	26	recnd 9526	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Λ
79	30	recnd 9526	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ψ
80	33	recnd 9526	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
81	78, 79, 80	mul32d 9693	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Λ ψ Λ ψ
82	24	nncnd 10452	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
83	24	nnne0d 10480	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
84	78, 80, 82, 83	div23d 10258	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ Λ Λ
85	84	oveq2d 6219	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Λ Λ
86	78, 80	mulcld 9520	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ Λ
87	74, 86, 82, 83	div12d 10257	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Λ Λ
88	85, 87	eqtr3d 2497	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Λ Λ
89	81, 88	oveq12d 6221	. . . . . . . . . . . . . . 15 $/\$ $/\$ Λ ψ Λ Λ ψ Λ
90	10	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
91	90, 32	rpdivcld 11158	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
92	54	pntrval 22947	. . . . . . . . . . . . . . . . . 18 ψ
93	91, 92	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ψ
94	93	oveq2d 6219	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Λ Λ ψ
95	28	recnd 9526	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
96	86, 79, 95	subdid 9914	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Λ ψ Λ ψ Λ
97	94, 96	eqtrd 2495	. . . . . . . . . . . . . . 15 $/\$ $/\$ Λ Λ ψ Λ
98	89, 97	eqtr4d 2498	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ ψ Λ Λ
99	55	ffvelrni 5954	. . . . . . . . . . . . . . . . 17
100	91, 99	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$
101	100	recnd 9526	. . . . . . . . . . . . . . 15 $/\$ $/\$
102	78, 101, 80	mul32d 9693	. . . . . . . . . . . . . 14 $/\$ $/\$ Λ Λ
103	98, 102	eqtr4d 2498	. . . . . . . . . . . . 13 $/\$ $/\$ Λ ψ Λ Λ
104	103	sumeq2dv 13301	. . . . . . . . . . . 12 $/\$ Λ ψ Λ Λ
105	77, 104	eqtrd 2495	. . . . . . . . . . 11 $/\$ Λ ψ Λ Λ
106	105	oveq2d 6219	. . . . . . . . . 10 $/\$ Λ ψ Λ Λ
107	47, 62, 51	mul12d 9692	. . . . . . . . . . 11 $/\$ Λ Λ
108	107	oveq2d 6219	. . . . . . . . . 10 $/\$ Λ ψ Λ Λ ψ Λ
109	69, 106, 108	3eqtr3rd 2504	. . . . . . . . 9 $/\$ Λ ψ Λ Λ
110	109	oveq2d 6219	. . . . . . . 8 $/\$ Λ ψ Λ Λ
111	66, 110	eqtrd 2495	. . . . . . 7 $/\$ Λ ψ Λ Λ
112	111	oveq1d 6218	. . . . . 6 $/\$ Λ ψ Λ Λ
113	54	pntrval 22947	. . . . . . . . . . . . . 14 ψ
114	10, 113	syl 16	. . . . . . . . . . . . 13 $/\$ ψ
115	114	oveq1d 6218	. . . . . . . . . . . 12 $/\$ ψ
116	16	recnd 9526	. . . . . . . . . . . . 13 $/\$ ψ
117	116, 62, 12	subdird 9915	. . . . . . . . . . . 12 $/\$ ψ ψ
118	115, 117	eqtrd 2495	. . . . . . . . . . 11 $/\$ ψ
119	118	oveq1d 6218	. . . . . . . . . 10 $/\$ Λ ψ ψ Λ ψ
120	17	recnd 9526	. . . . . . . . . . 11 $/\$ ψ
121	62, 12	mulcld 9520	. . . . . . . . . . 11 $/\$
122	120, 60, 121	addsubd 9854	. . . . . . . . . 10 $/\$ ψ Λ ψ ψ Λ ψ
123	119, 122	eqtr4d 2498	. . . . . . . . 9 $/\$ Λ ψ ψ Λ ψ
124	123	oveq1d 6218	. . . . . . . 8 $/\$ Λ ψ ψ Λ ψ
125	37	recnd 9526	. . . . . . . . . 10 $/\$ ψ Λ ψ
126	125, 121, 62, 64	divsubdird 10260	. . . . . . . . 9 $/\$ ψ Λ ψ ψ Λ ψ
127	12, 62, 64	divcan3d 10226	. . . . . . . . . 10 $/\$
128	127	oveq2d 6219	. . . . . . . . 9 $/\$ ψ Λ ψ ψ Λ ψ
129	126, 128	eqtrd 2495	. . . . . . . 8 $/\$ ψ Λ ψ ψ Λ ψ
130	124, 129	eqtrd 2495	. . . . . . 7 $/\$ Λ ψ ψ Λ ψ
131	52, 62, 64	divcan3d 10226	. . . . . . 7 $/\$ Λ Λ
132	130, 131	oveq12d 6221	. . . . . 6 $/\$ Λ ψ Λ ψ Λ ψ Λ
133	65, 112, 132	3eqtr3rd 2504	. . . . 5 $/\$ ψ Λ ψ Λ Λ
134	42, 53, 133	3eqtrrd 2500	. . . 4 $/\$ Λ ψ Λ ψ Λ
135	134	mpteq2dva 4489	. . 3 Λ ψ Λ ψ Λ
136	19, 11	remulcld 9528	. . . . 5 $/\$
137	38, 136	resubcld 9890	. . . 4 $/\$ ψ Λ ψ
138	21, 50	remulcld 9528	. . . . 5 $/\$ Λ
139	138, 11	resubcld 9890	. . . 4 $/\$ Λ
140		selberg3 22944	. . . . 5 ψ Λ ψ
141	140	a1i 11	. . . 4 ψ Λ ψ
142	19	recnd 9526	. . . . . . . 8 $/\$
143	50, 20	rerpdivcld 11168	. . . . . . . . 9 $/\$ Λ
144	143	recnd 9526	. . . . . . . 8 $/\$ Λ
145	11	rehalfcld 10685	. . . . . . . . 9 $/\$
146	145	recnd 9526	. . . . . . . 8 $/\$
147	142, 144, 146	subdid 9914	. . . . . . 7 $/\$ Λ Λ
148	142, 12, 51, 46	div32d 10244	. . . . . . . . 9 $/\$ Λ Λ
149	148	eqcomd 2462	. . . . . . . 8 $/\$ Λ Λ
150		2ne0 10528	. . . . . . . . . 10
151	150	a1i 11	. . . . . . . . 9 $/\$
152	12, 142, 151	divcan2d 10223	. . . . . . . 8 $/\$
153	149, 152	oveq12d 6221	. . . . . . 7 $/\$ Λ Λ
154	147, 153	eqtrd 2495	. . . . . 6 $/\$ Λ Λ
155	154	mpteq2dva 4489	. . . . 5 Λ Λ
156	143, 145	resubcld 9890	. . . . . 6 $/\$ Λ
157		ioossre 11471	. . . . . . . 8
158		o1const 13218	. . . . . . . 8 $/\$
159	157, 44, 158	mp2an 672	. . . . . . 7
160	159	a1i 11	. . . . . 6
161		vmalogdivsum 22924	. . . . . . 7 Λ
162	161	a1i 11	. . . . . 6 Λ
163	19, 156, 160, 162	o1mul2 13223	. . . . 5 Λ
164	155, 163	eqeltrrd 2543	. . . 4 Λ
165	137, 139, 141, 164	o1sub2 13224	. . 3 ψ Λ ψ Λ
166	135, 165	eqeltrd 2542	. 2 Λ
167	166	trud 1379	1 Λ

Colors of variables: wff setvar class

Syntax hints: $/\$ wa 369

wceq 1370

wtru 1371

wcel 1758

wne 2648

wss 3439 class class class wbr 4403

cmpt 4461

cfv 5529 (class class class)co 6203

cc 9394

cr 9395

cc0 9396

c1 9397

caddc 9399

cmul 9401

cpnf 9529

clt 9532

cmin 9709

cdiv 10107

cn 10436

c2 10485

crp 11105

cioo 11414

cfz 11557

cfl 11760

co1 13085

csu 13284

clog 22142 Λcvma 22565 ψcchp 22566

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-rep 4514 ax-sep 4524 ax-nul 4532 ax-pow 4581 ax-pr 4642 ax-un 6485 ax-inf2 7961 ax-cnex 9452 ax-resscn 9453 ax-1cn 9454 ax-icn 9455 ax-addcl 9456 ax-addrcl 9457 ax-mulcl 9458 ax-mulrcl 9459 ax-mulcom 9460 ax-addass 9461 ax-mulass 9462 ax-distr 9463 ax-i2m1 9464 ax-1ne0 9465 ax-1rid 9466 ax-rnegex 9467 ax-rrecex 9468 ax-cnre 9469 ax-pre-lttri 9470 ax-pre-lttrn 9471 ax-pre-ltadd 9472 ax-pre-mulgt0 9473 ax-pre-sup 9474 ax-addf 9475 ax-mulf 9476

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-fal 1376 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2650 df-nel 2651 df-ral 2804 df-rex 2805 df-reu 2806 df-rmo 2807 df-rab 2808 df-v 3080 df-sbc 3295 df-csb 3399 df-dif 3442 df-un 3444 df-in 3446 df-ss 3453 df-pss 3455 df-nul 3749 df-if 3903 df-pw 3973 df-sn 3989 df-pr 3991 df-tp 3993 df-op 3995 df-uni 4203 df-int 4240 df-iun 4284 df-iin 4285 df-disj 4374 df-br 4404 df-opab 4462 df-mpt 4463 df-tr 4497 df-eprel 4743 df-id 4747 df-po 4752 df-so 4753 df-fr 4790 df-se 4791 df-we 4792 df-ord 4833 df-on 4834 df-lim 4835 df-suc 4836 df-xp 4957 df-rel 4958 df-cnv 4959 df-co 4960 df-dm 4961 df-rn 4962 df-res 4963 df-ima 4964 df-iota 5492 df-fun 5531 df-fn 5532 df-f 5533 df-f1 5534 df-fo 5535 df-f1o 5536 df-fv 5537 df-isom 5538 df-riota 6164 df-ov 6206 df-oprab 6207 df-mpt2 6208 df-of 6433 df-om 6590 df-1st 6690 df-2nd 6691 df-supp 6804 df-recs 6945 df-rdg 6979 df-1o 7033 df-2o 7034 df-oadd 7037 df-er 7214 df-map 7329 df-pm 7330 df-ixp 7377 df-en 7424 df-dom 7425 df-sdom 7426 df-fin 7427 df-fsupp 7735 df-fi 7775 df-sup 7805 df-oi 7838 df-card 8223 df-cda 8451 df-pnf 9534 df-mnf 9535 df-xr 9536 df-ltxr 9537 df-le 9538 df-sub 9711 df-neg 9712 df-div 10108 df-nn 10437 df-2 10494 df-3 10495 df-4 10496 df-5 10497 df-6 10498 df-7 10499 df-8 10500 df-9 10501 df-10 10502 df-n0 10694 df-z 10761 df-dec 10870 df-uz 10976 df-q 11068 df-rp 11106 df-xneg 11203 df-xadd 11204 df-xmul 11205 df-ioo 11418 df-ioc 11419 df-ico 11420 df-icc 11421 df-fz 11558 df-fzo 11669 df-fl 11762 df-mod 11829 df-seq 11927 df-exp 11986 df-fac 12172 df-bc 12199 df-hash 12224 df-shft 12677 df-cj 12709 df-re 12710 df-im 12711 df-sqr 12845 df-abs 12846 df-limsup 13070 df-clim 13087 df-rlim 13088 df-o1 13089 df-lo1 13090 df-sum 13285 df-ef 13474 df-e 13475 df-sin 13476 df-cos 13477 df-pi 13479 df-dvds 13657 df-gcd 13812 df-prm 13885 df-pc 14025 df-struct 14297 df-ndx 14298 df-slot 14299 df-base 14300 df-sets 14301 df-ress 14302 df-plusg 14373 df-mulr 14374 df-starv 14375 df-sca 14376 df-vsca 14377 df-ip 14378 df-tset 14379 df-ple 14380 df-ds 14382 df-unif 14383 df-hom 14384 df-cco 14385 df-rest 14483 df-topn 14484 df-0g 14502 df-gsum 14503 df-topgen 14504 df-pt 14505 df-prds 14508 df-xrs 14562 df-qtop 14567 df-imas 14568 df-xps 14570 df-mre 14646 df-mrc 14647 df-acs 14649 df-mnd 15537 df-submnd 15587 df-mulg 15670 df-cntz 15957 df-cmn 16403 df-psmet 17937 df-xmet 17938 df-met 17939 df-bl 17940 df-mopn 17941 df-fbas 17942 df-fg 17943 df-cnfld 17947 df-top 18638 df-bases 18640 df-topon 18641 df-topsp 18642 df-cld 18758 df-ntr 18759 df-cls 18760 df-nei 18837 df-lp 18875 df-perf 18876 df-cn 18966 df-cnp 18967 df-haus 19054 df-cmp 19125 df-tx 19270 df-hmeo 19463 df-fil 19554 df-fm 19646 df-flim 19647 df-flf 19648 df-xms 20030 df-ms 20031 df-tms 20032 df-cncf 20589 df-limc 21477 df-dv 21478 df-log 22144 df-cxp 22145 df-em 22522 df-cht 22570 df-vma 22571 df-chp 22572 df-ppi 22573 df-mu 22574

This theorem is referenced by: selberg34r 22956

W3C validator