chpchtsum - Metamath Proof Explorer

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

Theorem chpchtsum 22563

Description: The second Chebyshev function is the sum of the theta function at arguments quickly approaching zero. (This is usually stated as an infinite sum, but after a certain point, the terms are all zero, and it is easier for us to use an explicit finite sum.) (Contributed by Mario Carneiro, 7-Apr-2016.)

**Assertion**
Ref	Expression
chpchtsum	ψ

Distinct variable group:

Proof of Theorem chpchtsum Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fzfid 11800	. . . . 5 $/\$
2		inss2 3576	. . . . . . . . . 10
3		simpr 461	. . . . . . . . . 10 $/\$
4	2, 3	sseldi 3359	. . . . . . . . 9 $/\$
5		prmnn 13771	. . . . . . . . 9
6	4, 5	syl 16	. . . . . . . 8 $/\$
7	6	nnrpd 11031	. . . . . . 7 $/\$
8	7	relogcld 22077	. . . . . 6 $/\$
9	8	recnd 9417	. . . . 5 $/\$
10		fsumconst 13262	. . . . 5 $/\$
11	1, 9, 10	syl2anc 661	. . . 4 $/\$
12		simpl 457	. . . . . . . . . 10 $/\$
13		1red 9406	. . . . . . . . . . 11 $/\$
14	6	nnred 10342	. . . . . . . . . . 11 $/\$
15		prmuz2 13786	. . . . . . . . . . . . 13
16	4, 15	syl 16	. . . . . . . . . . . 12 $/\$
17		eluz2b2 10932	. . . . . . . . . . . . 13 $/\$
18	17	simprbi 464	. . . . . . . . . . . 12
19	16, 18	syl 16	. . . . . . . . . . 11 $/\$
20		inss1 3575	. . . . . . . . . . . . . 14
21	20, 3	sseldi 3359	. . . . . . . . . . . . 13 $/\$
22		0re 9391	. . . . . . . . . . . . . 14
23		elicc2 11365	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
24	22, 12, 23	sylancr 663	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
25	21, 24	mpbid 210	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
26	25	simp3d 1002	. . . . . . . . . . 11 $/\$
27	13, 14, 12, 19, 26	ltletrd 9536	. . . . . . . . . 10 $/\$
28	12, 27	rplogcld 22083	. . . . . . . . 9 $/\$
29	14, 19	rplogcld 22083	. . . . . . . . 9 $/\$
30	28, 29	rpdivcld 11049	. . . . . . . 8 $/\$
31	30	rpred 11032	. . . . . . 7 $/\$
32	30	rpge0d 11036	. . . . . . 7 $/\$
33		flge0nn0 11671	. . . . . . 7 $/\$
34	31, 32, 33	syl2anc 661	. . . . . 6 $/\$
35		hashfz1 12122	. . . . . 6
36	34, 35	syl 16	. . . . 5 $/\$
37	36	oveq1d 6111	. . . 4 $/\$
38	31	flcld 11653	. . . . . 6 $/\$
39	38	zcnd 10753	. . . . 5 $/\$
40	39, 9	mulcomd 9412	. . . 4 $/\$
41	11, 37, 40	3eqtrrd 2480	. . 3 $/\$
42	41	sumeq2dv 13185	. 2
43		chpval2 22562	. 2 ψ
44		simpl 457	. . . . . 6 $/\$
45		0red 9392	. . . . . . 7 $/\$
46		1red 9406	. . . . . . . 8 $/\$
47		0lt1 9867	. . . . . . . . 9
48	47	a1i 11	. . . . . . . 8 $/\$
49		elfzuz2 11461	. . . . . . . . 9
50		eluzle 10878	. . . . . . . . . . 11
51	50	adantl 466	. . . . . . . . . 10 $/\$
52		simpl 457	. . . . . . . . . . 11 $/\$
53		1z 10681	. . . . . . . . . . 11
54		flge 11660	. . . . . . . . . . 11 $/\$
55	52, 53, 54	sylancl 662	. . . . . . . . . 10 $/\$
56	51, 55	mpbird 232	. . . . . . . . 9 $/\$
57	49, 56	sylan2 474	. . . . . . . 8 $/\$
58	45, 46, 44, 48, 57	ltletrd 9536	. . . . . . 7 $/\$
59	45, 44, 58	ltled 9527	. . . . . 6 $/\$
60		elfznn 11483	. . . . . . . 8
61	60	adantl 466	. . . . . . 7 $/\$
62	61	nnrecred 10372	. . . . . 6 $/\$
63	44, 59, 62	recxpcld 22173	. . . . 5 $/\$
64		chtval 22453	. . . . 5
65	63, 64	syl 16	. . . 4 $/\$
66	65	sumeq2dv 13185	. . 3
67		ppifi 22448	. . . 4
68		fzfid 11800	. . . 4
69	2	sseli 3357	. . . . . . . 8
70		elfznn 11483	. . . . . . . 8
71	69, 70	anim12i 566	. . . . . . 7 $/\$ $/\$
72	71	a1i 11	. . . . . 6 $/\$ $/\$
73		0red 9392	. . . . . . . . 9 $/\$
74	2	a1i 11	. . . . . . . . . . . 12
75	74	sselda 3361	. . . . . . . . . . 11 $/\$
76	75, 5	syl 16	. . . . . . . . . 10 $/\$
77	76	nnred 10342	. . . . . . . . 9 $/\$
78	76	nngt0d 10370	. . . . . . . . 9 $/\$
79	73, 77, 12, 78, 26	ltletrd 9536	. . . . . . . 8 $/\$
80	79	ex 434	. . . . . . 7
81	80	adantrd 468	. . . . . 6 $/\$
82	72, 81	jcad 533	. . . . 5 $/\$ $/\$ $/\$
83		inss2 3576	. . . . . . . . 9
84	83	sseli 3357	. . . . . . . 8
85	60, 84	anim12ci 567	. . . . . . 7 $/\$ $/\$
86	85	a1i 11	. . . . . 6 $/\$ $/\$
87	58	ex 434	. . . . . . 7
88	87	adantrd 468	. . . . . 6 $/\$
89	86, 88	jcad 533	. . . . 5 $/\$ $/\$ $/\$
90		elin 3544	. . . . . . . . 9 $/\$
91		simprll 761	. . . . . . . . . . 11 $/\$ $/\$ $/\$
92	91	biantrud 507	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
93		0red 9392	. . . . . . . . . . 11 $/\$ $/\$ $/\$
94		simpl 457	. . . . . . . . . . 11 $/\$ $/\$ $/\$
95	91, 5	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
96	95	nnred 10342	. . . . . . . . . . 11 $/\$ $/\$ $/\$
97	95	nnnn0d 10641	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
98	97	nn0ge0d 10644	. . . . . . . . . . 11 $/\$ $/\$ $/\$
99		df-3an 967	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
100	23, 99	syl6bb 261	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
101	100	baibd 900	. . . . . . . . . . 11 $/\$ $/\$ $/\$
102	93, 94, 96, 98, 101	syl22anc 1219	. . . . . . . . . 10 $/\$ $/\$ $/\$
103	92, 102	bitr3d 255	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
104	90, 103	syl5bb 257	. . . . . . . 8 $/\$ $/\$ $/\$
105		simprr 756	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
106	94, 105	elrpd 11030	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
107	106	relogcld 22077	. . . . . . . . . . 11 $/\$ $/\$ $/\$
108	91, 15	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
109	108, 18	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
110	96, 109	rplogcld 22083	. . . . . . . . . . 11 $/\$ $/\$ $/\$
111	107, 110	rerpdivcld 11059	. . . . . . . . . 10 $/\$ $/\$ $/\$
112		simprlr 762	. . . . . . . . . . 11 $/\$ $/\$ $/\$
113	112	nnzd 10751	. . . . . . . . . 10 $/\$ $/\$ $/\$
114		flge 11660	. . . . . . . . . 10 $/\$
115	111, 113, 114	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$
116	112	nnnn0d 10641	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
117	95, 116	nnexpcld 12034	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
118	117	nnrpd 11031	. . . . . . . . . . 11 $/\$ $/\$ $/\$
119	118, 106	logled 22081	. . . . . . . . . 10 $/\$ $/\$ $/\$
120	95	nnrpd 11031	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
121		relogexp 22049	. . . . . . . . . . . 12 $/\$
122	120, 113, 121	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$
123	122	breq1d 4307	. . . . . . . . . 10 $/\$ $/\$ $/\$
124	112	nnred 10342	. . . . . . . . . . 11 $/\$ $/\$ $/\$
125	124, 107, 110	lemuldivd 11077	. . . . . . . . . 10 $/\$ $/\$ $/\$
126	119, 123, 125	3bitrd 279	. . . . . . . . 9 $/\$ $/\$ $/\$
127		nnuz 10901	. . . . . . . . . . 11
128	112, 127	syl6eleq 2533	. . . . . . . . . 10 $/\$ $/\$ $/\$
129	111	flcld 11653	. . . . . . . . . 10 $/\$ $/\$ $/\$
130		elfz5 11450	. . . . . . . . . 10 $/\$
131	128, 129, 130	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$
132	115, 126, 131	3bitr4rd 286	. . . . . . . 8 $/\$ $/\$ $/\$
133	104, 132	anbi12d 710	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
134	94	flcld 11653	. . . . . . . . . . 11 $/\$ $/\$ $/\$
135		elfz5 11450	. . . . . . . . . . 11 $/\$
136	128, 134, 135	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$
137		flge 11660	. . . . . . . . . . 11 $/\$
138	94, 113, 137	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$
139	136, 138	bitr4d 256	. . . . . . . . 9 $/\$ $/\$ $/\$
140		elin 3544	. . . . . . . . . 10 $/\$
141	91	biantrud 507	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
142	106	rpge0d 11036	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
143	112	nnrecred 10372	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
144	94, 142, 143	recxpcld 22173	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
145		elicc2 11365	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
146		df-3an 967	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
147	145, 146	syl6bb 261	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
148	147	baibd 900	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
149	93, 144, 96, 98, 148	syl22anc 1219	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
150	141, 149	bitr3d 255	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
151	94, 142, 143	cxpge0d 22174	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152	112	nnrpd 11031	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
153	96, 98, 144, 151, 152	cxple2d 22177	. . . . . . . . . . 11 $/\$ $/\$ $/\$
154	95	nncnd 10343	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
155		cxpexp 22118	. . . . . . . . . . . . 13 $/\$
156	154, 116, 155	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
157	112	nncnd 10343	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
158	112	nnne0d 10371	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
159	157, 158	recid2d 10108	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
160	159	oveq2d 6112	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
161	106, 143, 157	cxpmuld 22184	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
162	94	recnd 9417	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
163	162	cxp1d 22156	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
164	160, 161, 163	3eqtr3d 2483	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
165	156, 164	breq12d 4310	. . . . . . . . . . 11 $/\$ $/\$ $/\$
166	150, 153, 165	3bitrd 279	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
167	140, 166	syl5bb 257	. . . . . . . . 9 $/\$ $/\$ $/\$
168	139, 167	anbi12d 710	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
169	117	nnred 10342	. . . . . . . . . . 11 $/\$ $/\$ $/\$
170		bernneq3 11997	. . . . . . . . . . . 12 $/\$
171	108, 116, 170	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$
172	124, 169, 171	ltled 9527	. . . . . . . . . 10 $/\$ $/\$ $/\$
173		letr 9473	. . . . . . . . . . 11 $/\$ $/\$ $/\$
174	124, 169, 94, 173	syl3anc 1218	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
175	172, 174	mpand 675	. . . . . . . . 9 $/\$ $/\$ $/\$
176	175	pm4.71rd 635	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
177	154	exp1d 12008	. . . . . . . . . . 11 $/\$ $/\$ $/\$
178	95	nnge1d 10369	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
179	96, 178, 128	leexp2ad 12045	. . . . . . . . . . 11 $/\$ $/\$ $/\$
180	177, 179	eqbrtrrd 4319	. . . . . . . . . 10 $/\$ $/\$ $/\$
181		letr 9473	. . . . . . . . . . 11 $/\$ $/\$ $/\$
182	96, 169, 94, 181	syl3anc 1218	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
183	180, 182	mpand 675	. . . . . . . . 9 $/\$ $/\$ $/\$
184	183	pm4.71rd 635	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
185	168, 176, 184	3bitr2rd 282	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
186	133, 185	bitrd 253	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
187	186	ex 434	. . . . 5 $/\$ $/\$ $/\$ $/\$
188	82, 89, 187	pm5.21ndd 354	. . . 4 $/\$ $/\$
189	9	adantrr 716	. . . 4 $/\$ $/\$
190	67, 68, 1, 188, 189	fsumcom2 13246	. . 3
191	66, 190	eqtr4d 2478	. 2
192	42, 43, 191	3eqtr4d 2485	1 ψ

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 965

wceq 1369

wcel 1756

cin 3332

wss 3333 class class class wbr 4297

cfv 5423 (class class class)co 6096

cfn 7315

cc 9285

cr 9286

cc0 9287

c1 9288

cmul 9292

clt 9423

cle 9424

cdiv 9998

cn 10327

c2 10376

cn0 10584

cz 10651

cuz 10866

crp 10996

cicc 11308

cfz 11442

cfl 11645

cexp 11870

chash 12108

csu 13168

cprime 13768

clog 22011

ccxp 22012

ccht 22433 ψcchp 22435

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4408 ax-sep 4418 ax-nul 4426 ax-pow 4475 ax-pr 4536 ax-un 6377 ax-inf2 7852 ax-cnex 9343 ax-resscn 9344 ax-1cn 9345 ax-icn 9346 ax-addcl 9347 ax-addrcl 9348 ax-mulcl 9349 ax-mulrcl 9350 ax-mulcom 9351 ax-addass 9352 ax-mulass 9353 ax-distr 9354 ax-i2m1 9355 ax-1ne0 9356 ax-1rid 9357 ax-rnegex 9358 ax-rrecex 9359 ax-cnre 9360 ax-pre-lttri 9361 ax-pre-lttrn 9362 ax-pre-ltadd 9363 ax-pre-mulgt0 9364 ax-pre-sup 9365 ax-addf 9366 ax-mulf 9367

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-fal 1375 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2573 df-ne 2613 df-nel 2614 df-ral 2725 df-rex 2726 df-reu 2727 df-rmo 2728 df-rab 2729 df-v 2979 df-sbc 3192 df-csb 3294 df-dif 3336 df-un 3338 df-in 3340 df-ss 3347 df-pss 3349 df-nul 3643 df-if 3797 df-pw 3867 df-sn 3883 df-pr 3885 df-tp 3887 df-op 3889 df-uni 4097 df-int 4134 df-iun 4178 df-iin 4179 df-br 4298 df-opab 4356 df-mpt 4357 df-tr 4391 df-eprel 4637 df-id 4641 df-po 4646 df-so 4647 df-fr 4684 df-se 4685 df-we 4686 df-ord 4727 df-on 4728 df-lim 4729 df-suc 4730 df-xp 4851 df-rel 4852 df-cnv 4853 df-co 4854 df-dm 4855 df-rn 4856 df-res 4857 df-ima 4858 df-iota 5386 df-fun 5425 df-fn 5426 df-f 5427 df-f1 5428 df-fo 5429 df-f1o 5430 df-fv 5431 df-isom 5432 df-riota 6057 df-ov 6099 df-oprab 6100 df-mpt2 6101 df-of 6325 df-om 6482 df-1st 6582 df-2nd 6583 df-supp 6696 df-recs 6837 df-rdg 6871 df-1o 6925 df-2o 6926 df-oadd 6929 df-er 7106 df-map 7221 df-pm 7222 df-ixp 7269 df-en 7316 df-dom 7317 df-sdom 7318 df-fin 7319 df-fsupp 7626 df-fi 7666 df-sup 7696 df-oi 7729 df-card 8114 df-cda 8342 df-pnf 9425 df-mnf 9426 df-xr 9427 df-ltxr 9428 df-le 9429 df-sub 9602 df-neg 9603 df-div 9999 df-nn 10328 df-2 10385 df-3 10386 df-4 10387 df-5 10388 df-6 10389 df-7 10390 df-8 10391 df-9 10392 df-10 10393 df-n0 10585 df-z 10652 df-dec 10761 df-uz 10867 df-q 10959 df-rp 10997 df-xneg 11094 df-xadd 11095 df-xmul 11096 df-ioo 11309 df-ioc 11310 df-ico 11311 df-icc 11312 df-fz 11443 df-fzo 11554 df-fl 11647 df-mod 11714 df-seq 11812 df-exp 11871 df-fac 12057 df-bc 12084 df-hash 12109 df-shft 12561 df-cj 12593 df-re 12594 df-im 12595 df-sqr 12729 df-abs 12730 df-limsup 12954 df-clim 12971 df-rlim 12972 df-sum 13169 df-ef 13358 df-sin 13360 df-cos 13361 df-pi 13363 df-dvds 13541 df-gcd 13696 df-prm 13769 df-pc 13909 df-struct 14181 df-ndx 14182 df-slot 14183 df-base 14184 df-sets 14185 df-ress 14186 df-plusg 14256 df-mulr 14257 df-starv 14258 df-sca 14259 df-vsca 14260 df-ip 14261 df-tset 14262 df-ple 14263 df-ds 14265 df-unif 14266 df-hom 14267 df-cco 14268 df-rest 14366 df-topn 14367 df-0g 14385 df-gsum 14386 df-topgen 14387 df-pt 14388 df-prds 14391 df-xrs 14445 df-qtop 14450 df-imas 14451 df-xps 14453 df-mre 14529 df-mrc 14530 df-acs 14532 df-mnd 15420 df-submnd 15470 df-mulg 15553 df-cntz 15840 df-cmn 16284 df-psmet 17814 df-xmet 17815 df-met 17816 df-bl 17817 df-mopn 17818 df-fbas 17819 df-fg 17820 df-cnfld 17824 df-top 18508 df-bases 18510 df-topon 18511 df-topsp 18512 df-cld 18628 df-ntr 18629 df-cls 18630 df-nei 18707 df-lp 18745 df-perf 18746 df-cn 18836 df-cnp 18837 df-haus 18924 df-tx 19140 df-hmeo 19333 df-fil 19424 df-fm 19516 df-flim 19517 df-flf 19518 df-xms 19900 df-ms 19901 df-tms 19902 df-cncf 20459 df-limc 21346 df-dv 21347 df-log 22013 df-cxp 22014 df-cht 22439 df-vma 22440 df-chp 22441

This theorem is referenced by: (None)

W3C validator