chpchtsum - Metamath Proof Explorer

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

Theorem chpchtsum 22442

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 11778	. . . . 5 $/\$
2		inss2 3559	. . . . . . . . . 10
3		simpr 458	. . . . . . . . . 10 $/\$
4	2, 3	sseldi 3342	. . . . . . . . 9 $/\$
5		prmnn 13748	. . . . . . . . 9
6	4, 5	syl 16	. . . . . . . 8 $/\$
7	6	nnrpd 11013	. . . . . . 7 $/\$
8	7	relogcld 21956	. . . . . 6 $/\$
9	8	recnd 9399	. . . . 5 $/\$
10		fsumconst 13239	. . . . 5 $/\$
11	1, 9, 10	syl2anc 654	. . . 4 $/\$
12		simpl 454	. . . . . . . . . 10 $/\$
13		1red 9388	. . . . . . . . . . 11 $/\$
14	6	nnred 10324	. . . . . . . . . . 11 $/\$
15		prmuz2 13763	. . . . . . . . . . . . 13
16	4, 15	syl 16	. . . . . . . . . . . 12 $/\$
17		eluz2b2 10914	. . . . . . . . . . . . 13 $/\$
18	17	simprbi 461	. . . . . . . . . . . 12
19	16, 18	syl 16	. . . . . . . . . . 11 $/\$
20		inss1 3558	. . . . . . . . . . . . . 14
21	20, 3	sseldi 3342	. . . . . . . . . . . . 13 $/\$
22		0re 9373	. . . . . . . . . . . . . 14
23		elicc2 11347	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
24	22, 12, 23	sylancr 656	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
25	21, 24	mpbid 210	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
26	25	simp3d 995	. . . . . . . . . . 11 $/\$
27	13, 14, 12, 19, 26	ltletrd 9518	. . . . . . . . . 10 $/\$
28	12, 27	rplogcld 21962	. . . . . . . . 9 $/\$
29	14, 19	rplogcld 21962	. . . . . . . . 9 $/\$
30	28, 29	rpdivcld 11031	. . . . . . . 8 $/\$
31	30	rpred 11014	. . . . . . 7 $/\$
32	30	rpge0d 11018	. . . . . . 7 $/\$
33		flge0nn0 11649	. . . . . . 7 $/\$
34	31, 32, 33	syl2anc 654	. . . . . 6 $/\$
35		hashfz1 12100	. . . . . 6
36	34, 35	syl 16	. . . . 5 $/\$
37	36	oveq1d 6095	. . . 4 $/\$
38	31	flcld 11631	. . . . . 6 $/\$
39	38	zcnd 10735	. . . . 5 $/\$
40	39, 9	mulcomd 9394	. . . 4 $/\$
41	11, 37, 40	3eqtrrd 2470	. . 3 $/\$
42	41	sumeq2dv 13163	. 2
43		chpval2 22441	. 2 ψ
44		simpl 454	. . . . . 6 $/\$
45		0red 9374	. . . . . . 7 $/\$
46		1red 9388	. . . . . . . 8 $/\$
47		0lt1 9849	. . . . . . . . 9
48	47	a1i 11	. . . . . . . 8 $/\$
49		elfzuz2 11442	. . . . . . . . 9
50		eluzle 10860	. . . . . . . . . . 11
51	50	adantl 463	. . . . . . . . . 10 $/\$
52		simpl 454	. . . . . . . . . . 11 $/\$
53		1z 10663	. . . . . . . . . . 11
54		flge 11638	. . . . . . . . . . 11 $/\$
55	52, 53, 54	sylancl 655	. . . . . . . . . 10 $/\$
56	51, 55	mpbird 232	. . . . . . . . 9 $/\$
57	49, 56	sylan2 471	. . . . . . . 8 $/\$
58	45, 46, 44, 48, 57	ltletrd 9518	. . . . . . 7 $/\$
59	45, 44, 58	ltled 9509	. . . . . 6 $/\$
60		elfznn 11464	. . . . . . . 8
61	60	adantl 463	. . . . . . 7 $/\$
62	61	nnrecred 10354	. . . . . 6 $/\$
63	44, 59, 62	recxpcld 22052	. . . . 5 $/\$
64		chtval 22332	. . . . 5
65	63, 64	syl 16	. . . 4 $/\$
66	65	sumeq2dv 13163	. . 3
67		ppifi 22327	. . . 4
68		fzfid 11778	. . . 4
69	2	sseli 3340	. . . . . . . 8
70		elfznn 11464	. . . . . . . 8
71	69, 70	anim12i 561	. . . . . . 7 $/\$ $/\$
72	71	a1i 11	. . . . . 6 $/\$ $/\$
73		0red 9374	. . . . . . . . 9 $/\$
74	2	a1i 11	. . . . . . . . . . . 12
75	74	sselda 3344	. . . . . . . . . . 11 $/\$
76	75, 5	syl 16	. . . . . . . . . 10 $/\$
77	76	nnred 10324	. . . . . . . . 9 $/\$
78	76	nngt0d 10352	. . . . . . . . 9 $/\$
79	73, 77, 12, 78, 26	ltletrd 9518	. . . . . . . 8 $/\$
80	79	ex 434	. . . . . . 7
81	80	adantrd 465	. . . . . 6 $/\$
82	72, 81	jcad 530	. . . . 5 $/\$ $/\$ $/\$
83		inss2 3559	. . . . . . . . 9
84	83	sseli 3340	. . . . . . . 8
85	60, 84	anim12ci 562	. . . . . . 7 $/\$ $/\$
86	85	a1i 11	. . . . . 6 $/\$ $/\$
87	58	ex 434	. . . . . . 7
88	87	adantrd 465	. . . . . 6 $/\$
89	86, 88	jcad 530	. . . . 5 $/\$ $/\$ $/\$
90		elin 3527	. . . . . . . . 9 $/\$
91		simprll 754	. . . . . . . . . . 11 $/\$ $/\$ $/\$
92	91	biantrud 504	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
93		0red 9374	. . . . . . . . . . 11 $/\$ $/\$ $/\$
94		simpl 454	. . . . . . . . . . 11 $/\$ $/\$ $/\$
95	91, 5	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
96	95	nnred 10324	. . . . . . . . . . 11 $/\$ $/\$ $/\$
97	95	nnnn0d 10623	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
98	97	nn0ge0d 10626	. . . . . . . . . . 11 $/\$ $/\$ $/\$
99		df-3an 960	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
100	23, 99	syl6bb 261	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
101	100	baibd 893	. . . . . . . . . . 11 $/\$ $/\$ $/\$
102	93, 94, 96, 98, 101	syl22anc 1212	. . . . . . . . . 10 $/\$ $/\$ $/\$
103	92, 102	bitr3d 255	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
104	90, 103	syl5bb 257	. . . . . . . 8 $/\$ $/\$ $/\$
105		simprr 749	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
106	94, 105	elrpd 11012	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
107	106	relogcld 21956	. . . . . . . . . . 11 $/\$ $/\$ $/\$
108	91, 15	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
109	108, 18	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
110	96, 109	rplogcld 21962	. . . . . . . . . . 11 $/\$ $/\$ $/\$
111	107, 110	rerpdivcld 11041	. . . . . . . . . 10 $/\$ $/\$ $/\$
112		simprlr 755	. . . . . . . . . . 11 $/\$ $/\$ $/\$
113	112	nnzd 10733	. . . . . . . . . 10 $/\$ $/\$ $/\$
114		flge 11638	. . . . . . . . . 10 $/\$
115	111, 113, 114	syl2anc 654	. . . . . . . . 9 $/\$ $/\$ $/\$
116	112	nnnn0d 10623	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
117	95, 116	nnexpcld 12012	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
118	117	nnrpd 11013	. . . . . . . . . . 11 $/\$ $/\$ $/\$
119	118, 106	logled 21960	. . . . . . . . . 10 $/\$ $/\$ $/\$
120	95	nnrpd 11013	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
121		relogexp 21928	. . . . . . . . . . . 12 $/\$
122	120, 113, 121	syl2anc 654	. . . . . . . . . . 11 $/\$ $/\$ $/\$
123	122	breq1d 4290	. . . . . . . . . 10 $/\$ $/\$ $/\$
124	112	nnred 10324	. . . . . . . . . . 11 $/\$ $/\$ $/\$
125	124, 107, 110	lemuldivd 11059	. . . . . . . . . 10 $/\$ $/\$ $/\$
126	119, 123, 125	3bitrd 279	. . . . . . . . 9 $/\$ $/\$ $/\$
127		nnuz 10883	. . . . . . . . . . 11
128	112, 127	syl6eleq 2523	. . . . . . . . . 10 $/\$ $/\$ $/\$
129	111	flcld 11631	. . . . . . . . . 10 $/\$ $/\$ $/\$
130		elfz5 11431	. . . . . . . . . 10 $/\$
131	128, 129, 130	syl2anc 654	. . . . . . . . 9 $/\$ $/\$ $/\$
132	115, 126, 131	3bitr4rd 286	. . . . . . . 8 $/\$ $/\$ $/\$
133	104, 132	anbi12d 703	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
134	94	flcld 11631	. . . . . . . . . . 11 $/\$ $/\$ $/\$
135		elfz5 11431	. . . . . . . . . . 11 $/\$
136	128, 134, 135	syl2anc 654	. . . . . . . . . 10 $/\$ $/\$ $/\$
137		flge 11638	. . . . . . . . . . 11 $/\$
138	94, 113, 137	syl2anc 654	. . . . . . . . . 10 $/\$ $/\$ $/\$
139	136, 138	bitr4d 256	. . . . . . . . 9 $/\$ $/\$ $/\$
140		elin 3527	. . . . . . . . . 10 $/\$
141	91	biantrud 504	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
142	106	rpge0d 11018	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
143	112	nnrecred 10354	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
144	94, 142, 143	recxpcld 22052	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
145		elicc2 11347	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
146		df-3an 960	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
147	145, 146	syl6bb 261	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
148	147	baibd 893	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
149	93, 144, 96, 98, 148	syl22anc 1212	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
150	141, 149	bitr3d 255	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
151	94, 142, 143	cxpge0d 22053	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152	112	nnrpd 11013	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
153	96, 98, 144, 151, 152	cxple2d 22056	. . . . . . . . . . 11 $/\$ $/\$ $/\$
154	95	nncnd 10325	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
155		cxpexp 21997	. . . . . . . . . . . . 13 $/\$
156	154, 116, 155	syl2anc 654	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
157	112	nncnd 10325	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
158	112	nnne0d 10353	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
159	157, 158	recid2d 10090	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
160	159	oveq2d 6096	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
161	106, 143, 157	cxpmuld 22063	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
162	94	recnd 9399	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
163	162	cxp1d 22035	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
164	160, 161, 163	3eqtr3d 2473	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
165	156, 164	breq12d 4293	. . . . . . . . . . 11 $/\$ $/\$ $/\$
166	150, 153, 165	3bitrd 279	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
167	140, 166	syl5bb 257	. . . . . . . . 9 $/\$ $/\$ $/\$
168	139, 167	anbi12d 703	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
169	117	nnred 10324	. . . . . . . . . . 11 $/\$ $/\$ $/\$
170		bernneq3 11975	. . . . . . . . . . . 12 $/\$
171	108, 116, 170	syl2anc 654	. . . . . . . . . . 11 $/\$ $/\$ $/\$
172	124, 169, 171	ltled 9509	. . . . . . . . . 10 $/\$ $/\$ $/\$
173		letr 9455	. . . . . . . . . . 11 $/\$ $/\$ $/\$
174	124, 169, 94, 173	syl3anc 1211	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
175	172, 174	mpand 668	. . . . . . . . 9 $/\$ $/\$ $/\$
176	175	pm4.71rd 628	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
177	154	exp1d 11986	. . . . . . . . . . 11 $/\$ $/\$ $/\$
178	95	nnge1d 10351	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
179	96, 178, 128	leexp2ad 12023	. . . . . . . . . . 11 $/\$ $/\$ $/\$
180	177, 179	eqbrtrrd 4302	. . . . . . . . . 10 $/\$ $/\$ $/\$
181		letr 9455	. . . . . . . . . . 11 $/\$ $/\$ $/\$
182	96, 169, 94, 181	syl3anc 1211	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
183	180, 182	mpand 668	. . . . . . . . 9 $/\$ $/\$ $/\$
184	183	pm4.71rd 628	. . . . . . . 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 709	. . . 4 $/\$ $/\$
190	67, 68, 1, 188, 189	fsumcom2 13224	. . 3
191	66, 190	eqtr4d 2468	. 2
192	42, 43, 191	3eqtr4d 2475	1 ψ

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1362

wcel 1755

cin 3315

wss 3316 class class class wbr 4280

cfv 5406 (class class class)co 6080

cfn 7298

cc 9267

cr 9268

cc0 9269

c1 9270

cmul 9274

clt 9405

cle 9406

cdiv 9980

cn 10309

c2 10358

cn0 10566

cz 10633

cuz 10848

crp 10978

cicc 11290

cfz 11423

cfl 11623

cexp 11848

chash 12086

csu 13146

cprime 13745

clog 21890

ccxp 21891

ccht 22312 ψcchp 22314

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1594 ax-4 1605 ax-5 1669 ax-6 1707 ax-7 1727 ax-8 1757 ax-9 1759 ax-10 1774 ax-11 1779 ax-12 1791 ax-13 1942 ax-ext 2414 ax-rep 4391 ax-sep 4401 ax-nul 4409 ax-pow 4458 ax-pr 4519 ax-un 6361 ax-inf2 7835 ax-cnex 9325 ax-resscn 9326 ax-1cn 9327 ax-icn 9328 ax-addcl 9329 ax-addrcl 9330 ax-mulcl 9331 ax-mulrcl 9332 ax-mulcom 9333 ax-addass 9334 ax-mulass 9335 ax-distr 9336 ax-i2m1 9337 ax-1ne0 9338 ax-1rid 9339 ax-rnegex 9340 ax-rrecex 9341 ax-cnre 9342 ax-pre-lttri 9343 ax-pre-lttrn 9344 ax-pre-ltadd 9345 ax-pre-mulgt0 9346 ax-pre-sup 9347 ax-addf 9348 ax-mulf 9349

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 959 df-3an 960 df-tru 1365 df-fal 1368 df-ex 1590 df-nf 1593 df-sb 1700 df-eu 2258 df-mo 2259 df-clab 2420 df-cleq 2426 df-clel 2429 df-nfc 2558 df-ne 2598 df-nel 2599 df-ral 2710 df-rex 2711 df-reu 2712 df-rmo 2713 df-rab 2714 df-v 2964 df-sbc 3176 df-csb 3277 df-dif 3319 df-un 3321 df-in 3323 df-ss 3330 df-pss 3332 df-nul 3626 df-if 3780 df-pw 3850 df-sn 3866 df-pr 3868 df-tp 3870 df-op 3872 df-uni 4080 df-int 4117 df-iun 4161 df-iin 4162 df-br 4281 df-opab 4339 df-mpt 4340 df-tr 4374 df-eprel 4619 df-id 4623 df-po 4628 df-so 4629 df-fr 4666 df-se 4667 df-we 4668 df-ord 4709 df-on 4710 df-lim 4711 df-suc 4712 df-xp 4833 df-rel 4834 df-cnv 4835 df-co 4836 df-dm 4837 df-rn 4838 df-res 4839 df-ima 4840 df-iota 5369 df-fun 5408 df-fn 5409 df-f 5410 df-f1 5411 df-fo 5412 df-f1o 5413 df-fv 5414 df-isom 5415 df-riota 6039 df-ov 6083 df-oprab 6084 df-mpt2 6085 df-of 6309 df-om 6466 df-1st 6566 df-2nd 6567 df-supp 6680 df-recs 6818 df-rdg 6852 df-1o 6908 df-2o 6909 df-oadd 6912 df-er 7089 df-map 7204 df-pm 7205 df-ixp 7252 df-en 7299 df-dom 7300 df-sdom 7301 df-fin 7302 df-fsupp 7609 df-fi 7649 df-sup 7679 df-oi 7712 df-card 8097 df-cda 8325 df-pnf 9407 df-mnf 9408 df-xr 9409 df-ltxr 9410 df-le 9411 df-sub 9584 df-neg 9585 df-div 9981 df-nn 10310 df-2 10367 df-3 10368 df-4 10369 df-5 10370 df-6 10371 df-7 10372 df-8 10373 df-9 10374 df-10 10375 df-n0 10567 df-z 10634 df-dec 10743 df-uz 10849 df-q 10941 df-rp 10979 df-xneg 11076 df-xadd 11077 df-xmul 11078 df-ioo 11291 df-ioc 11292 df-ico 11293 df-icc 11294 df-fz 11424 df-fzo 11532 df-fl 11625 df-mod 11692 df-seq 11790 df-exp 11849 df-fac 12035 df-bc 12062 df-hash 12087 df-shft 12539 df-cj 12571 df-re 12572 df-im 12573 df-sqr 12707 df-abs 12708 df-limsup 12932 df-clim 12949 df-rlim 12950 df-sum 13147 df-ef 13335 df-sin 13337 df-cos 13338 df-pi 13340 df-dvds 13518 df-gcd 13673 df-prm 13746 df-pc 13886 df-struct 14158 df-ndx 14159 df-slot 14160 df-base 14161 df-sets 14162 df-ress 14163 df-plusg 14233 df-mulr 14234 df-starv 14235 df-sca 14236 df-vsca 14237 df-ip 14238 df-tset 14239 df-ple 14240 df-ds 14242 df-unif 14243 df-hom 14244 df-cco 14245 df-rest 14343 df-topn 14344 df-0g 14362 df-gsum 14363 df-topgen 14364 df-pt 14365 df-prds 14368 df-xrs 14422 df-qtop 14427 df-imas 14428 df-xps 14430 df-mre 14506 df-mrc 14507 df-acs 14509 df-mnd 15397 df-submnd 15447 df-mulg 15527 df-cntz 15814 df-cmn 16258 df-psmet 17652 df-xmet 17653 df-met 17654 df-bl 17655 df-mopn 17656 df-fbas 17657 df-fg 17658 df-cnfld 17662 df-top 18344 df-bases 18346 df-topon 18347 df-topsp 18348 df-cld 18464 df-ntr 18465 df-cls 18466 df-nei 18543 df-lp 18581 df-perf 18582 df-cn 18672 df-cnp 18673 df-haus 18760 df-tx 18976 df-hmeo 19169 df-fil 19260 df-fm 19352 df-flim 19353 df-flf 19354 df-xms 19736 df-ms 19737 df-tms 19738 df-cncf 20295 df-limc 21182 df-dv 21183 df-log 21892 df-cxp 21893 df-cht 22318 df-vma 22319 df-chp 22320

This theorem is referenced by: (None)

W3C validator