chpchtsum - Metamath Proof Explorer

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

Theorem chpchtsum 23222

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 12047	. . . . 5 $/\$
2		inss2 3719	. . . . . . . . . 10
3		simpr 461	. . . . . . . . . 10 $/\$
4	2, 3	sseldi 3502	. . . . . . . . 9 $/\$
5		prmnn 14075	. . . . . . . . 9
6	4, 5	syl 16	. . . . . . . 8 $/\$
7	6	nnrpd 11251	. . . . . . 7 $/\$
8	7	relogcld 22736	. . . . . 6 $/\$
9	8	recnd 9618	. . . . 5 $/\$
10		fsumconst 13564	. . . . 5 $/\$
11	1, 9, 10	syl2anc 661	. . . 4 $/\$
12		simpl 457	. . . . . . . . . 10 $/\$
13		1red 9607	. . . . . . . . . . 11 $/\$
14	6	nnred 10547	. . . . . . . . . . 11 $/\$
15		prmuz2 14090	. . . . . . . . . . . . 13
16	4, 15	syl 16	. . . . . . . . . . . 12 $/\$
17		eluz2b2 11150	. . . . . . . . . . . . 13 $/\$
18	17	simprbi 464	. . . . . . . . . . . 12
19	16, 18	syl 16	. . . . . . . . . . 11 $/\$
20		inss1 3718	. . . . . . . . . . . . . 14
21	20, 3	sseldi 3502	. . . . . . . . . . . . 13 $/\$
22		0re 9592	. . . . . . . . . . . . . 14
23		elicc2 11585	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
24	22, 12, 23	sylancr 663	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
25	21, 24	mpbid 210	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
26	25	simp3d 1010	. . . . . . . . . . 11 $/\$
27	13, 14, 12, 19, 26	ltletrd 9737	. . . . . . . . . 10 $/\$
28	12, 27	rplogcld 22742	. . . . . . . . 9 $/\$
29	14, 19	rplogcld 22742	. . . . . . . . 9 $/\$
30	28, 29	rpdivcld 11269	. . . . . . . 8 $/\$
31	30	rpred 11252	. . . . . . 7 $/\$
32	30	rpge0d 11256	. . . . . . 7 $/\$
33		flge0nn0 11918	. . . . . . 7 $/\$
34	31, 32, 33	syl2anc 661	. . . . . 6 $/\$
35		hashfz1 12383	. . . . . 6
36	34, 35	syl 16	. . . . 5 $/\$
37	36	oveq1d 6297	. . . 4 $/\$
38	31	flcld 11899	. . . . . 6 $/\$
39	38	zcnd 10963	. . . . 5 $/\$
40	39, 9	mulcomd 9613	. . . 4 $/\$
41	11, 37, 40	3eqtrrd 2513	. . 3 $/\$
42	41	sumeq2dv 13484	. 2
43		chpval2 23221	. 2 ψ
44		simpl 457	. . . . . 6 $/\$
45		0red 9593	. . . . . . 7 $/\$
46		1red 9607	. . . . . . . 8 $/\$
47		0lt1 10071	. . . . . . . . 9
48	47	a1i 11	. . . . . . . 8 $/\$
49		elfzuz2 11687	. . . . . . . . 9
50		eluzle 11090	. . . . . . . . . . 11
51	50	adantl 466	. . . . . . . . . 10 $/\$
52		simpl 457	. . . . . . . . . . 11 $/\$
53		1z 10890	. . . . . . . . . . 11
54		flge 11906	. . . . . . . . . . 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 9737	. . . . . . 7 $/\$
59	45, 44, 58	ltled 9728	. . . . . 6 $/\$
60		elfznn 11710	. . . . . . . 8
61	60	adantl 466	. . . . . . 7 $/\$
62	61	nnrecred 10577	. . . . . 6 $/\$
63	44, 59, 62	recxpcld 22832	. . . . 5 $/\$
64		chtval 23112	. . . . 5
65	63, 64	syl 16	. . . 4 $/\$
66	65	sumeq2dv 13484	. . 3
67		ppifi 23107	. . . 4
68		fzfid 12047	. . . 4
69	2	sseli 3500	. . . . . . . 8
70		elfznn 11710	. . . . . . . 8
71	69, 70	anim12i 566	. . . . . . 7 $/\$ $/\$
72	71	a1i 11	. . . . . 6 $/\$ $/\$
73		0red 9593	. . . . . . . . 9 $/\$
74	2	a1i 11	. . . . . . . . . . . 12
75	74	sselda 3504	. . . . . . . . . . 11 $/\$
76	75, 5	syl 16	. . . . . . . . . 10 $/\$
77	76	nnred 10547	. . . . . . . . 9 $/\$
78	76	nngt0d 10575	. . . . . . . . 9 $/\$
79	73, 77, 12, 78, 26	ltletrd 9737	. . . . . . . 8 $/\$
80	79	ex 434	. . . . . . 7
81	80	adantrd 468	. . . . . 6 $/\$
82	72, 81	jcad 533	. . . . 5 $/\$ $/\$ $/\$
83		inss2 3719	. . . . . . . . 9
84	83	sseli 3500	. . . . . . . 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 3687	. . . . . . . . 9 $/\$
91		simprll 761	. . . . . . . . . . 11 $/\$ $/\$ $/\$
92	91	biantrud 507	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
93		0red 9593	. . . . . . . . . . 11 $/\$ $/\$ $/\$
94		simpl 457	. . . . . . . . . . 11 $/\$ $/\$ $/\$
95	91, 5	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
96	95	nnred 10547	. . . . . . . . . . 11 $/\$ $/\$ $/\$
97	95	nnnn0d 10848	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
98	97	nn0ge0d 10851	. . . . . . . . . . 11 $/\$ $/\$ $/\$
99		df-3an 975	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
100	23, 99	syl6bb 261	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
101	100	baibd 907	. . . . . . . . . . 11 $/\$ $/\$ $/\$
102	93, 94, 96, 98, 101	syl22anc 1229	. . . . . . . . . 10 $/\$ $/\$ $/\$
103	92, 102	bitr3d 255	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
104	90, 103	syl5bb 257	. . . . . . . 8 $/\$ $/\$ $/\$
105		simprr 756	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
106	94, 105	elrpd 11250	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
107	106	relogcld 22736	. . . . . . . . . . 11 $/\$ $/\$ $/\$
108	91, 15	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
109	108, 18	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
110	96, 109	rplogcld 22742	. . . . . . . . . . 11 $/\$ $/\$ $/\$
111	107, 110	rerpdivcld 11279	. . . . . . . . . 10 $/\$ $/\$ $/\$
112		simprlr 762	. . . . . . . . . . 11 $/\$ $/\$ $/\$
113	112	nnzd 10961	. . . . . . . . . 10 $/\$ $/\$ $/\$
114		flge 11906	. . . . . . . . . 10 $/\$
115	111, 113, 114	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$
116	112	nnnn0d 10848	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
117	95, 116	nnexpcld 12295	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
118	117	nnrpd 11251	. . . . . . . . . . 11 $/\$ $/\$ $/\$
119	118, 106	logled 22740	. . . . . . . . . 10 $/\$ $/\$ $/\$
120	95	nnrpd 11251	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
121		relogexp 22708	. . . . . . . . . . . 12 $/\$
122	120, 113, 121	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$
123	122	breq1d 4457	. . . . . . . . . 10 $/\$ $/\$ $/\$
124	112	nnred 10547	. . . . . . . . . . 11 $/\$ $/\$ $/\$
125	124, 107, 110	lemuldivd 11297	. . . . . . . . . 10 $/\$ $/\$ $/\$
126	119, 123, 125	3bitrd 279	. . . . . . . . 9 $/\$ $/\$ $/\$
127		nnuz 11113	. . . . . . . . . . 11
128	112, 127	syl6eleq 2565	. . . . . . . . . 10 $/\$ $/\$ $/\$
129	111	flcld 11899	. . . . . . . . . 10 $/\$ $/\$ $/\$
130		elfz5 11676	. . . . . . . . . 10 $/\$
131	128, 129, 130	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$
132	115, 126, 131	3bitr4rd 286	. . . . . . . 8 $/\$ $/\$ $/\$
133	104, 132	anbi12d 710	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
134	94	flcld 11899	. . . . . . . . . . 11 $/\$ $/\$ $/\$
135		elfz5 11676	. . . . . . . . . . 11 $/\$
136	128, 134, 135	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$
137		flge 11906	. . . . . . . . . . 11 $/\$
138	94, 113, 137	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$
139	136, 138	bitr4d 256	. . . . . . . . 9 $/\$ $/\$ $/\$
140		elin 3687	. . . . . . . . . 10 $/\$
141	91	biantrud 507	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
142	106	rpge0d 11256	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
143	112	nnrecred 10577	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
144	94, 142, 143	recxpcld 22832	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
145		elicc2 11585	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
146		df-3an 975	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
147	145, 146	syl6bb 261	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
148	147	baibd 907	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
149	93, 144, 96, 98, 148	syl22anc 1229	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
150	141, 149	bitr3d 255	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
151	94, 142, 143	cxpge0d 22833	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152	112	nnrpd 11251	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
153	96, 98, 144, 151, 152	cxple2d 22836	. . . . . . . . . . 11 $/\$ $/\$ $/\$
154	95	nncnd 10548	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
155		cxpexp 22777	. . . . . . . . . . . . 13 $/\$
156	154, 116, 155	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
157	112	nncnd 10548	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
158	112	nnne0d 10576	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
159	157, 158	recid2d 10312	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
160	159	oveq2d 6298	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
161	106, 143, 157	cxpmuld 22843	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
162	94	recnd 9618	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
163	162	cxp1d 22815	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
164	160, 161, 163	3eqtr3d 2516	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
165	156, 164	breq12d 4460	. . . . . . . . . . 11 $/\$ $/\$ $/\$
166	150, 153, 165	3bitrd 279	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
167	140, 166	syl5bb 257	. . . . . . . . 9 $/\$ $/\$ $/\$
168	139, 167	anbi12d 710	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
169	117	nnred 10547	. . . . . . . . . . 11 $/\$ $/\$ $/\$
170		bernneq3 12258	. . . . . . . . . . . 12 $/\$
171	108, 116, 170	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$
172	124, 169, 171	ltled 9728	. . . . . . . . . 10 $/\$ $/\$ $/\$
173		letr 9674	. . . . . . . . . . 11 $/\$ $/\$ $/\$
174	124, 169, 94, 173	syl3anc 1228	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
175	172, 174	mpand 675	. . . . . . . . 9 $/\$ $/\$ $/\$
176	175	pm4.71rd 635	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
177	154	exp1d 12269	. . . . . . . . . . 11 $/\$ $/\$ $/\$
178	95	nnge1d 10574	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
179	96, 178, 128	leexp2ad 12306	. . . . . . . . . . 11 $/\$ $/\$ $/\$
180	177, 179	eqbrtrrd 4469	. . . . . . . . . 10 $/\$ $/\$ $/\$
181		letr 9674	. . . . . . . . . . 11 $/\$ $/\$ $/\$
182	96, 169, 94, 181	syl3anc 1228	. . . . . . . . . 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 13548	. . 3
191	66, 190	eqtr4d 2511	. 2
192	42, 43, 191	3eqtr4d 2518	1 ψ

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1379

wcel 1767

cin 3475

wss 3476 class class class wbr 4447

cfv 5586 (class class class)co 6282

cfn 7513

cc 9486

cr 9487

cc0 9488

c1 9489

cmul 9493

clt 9624

cle 9625

cdiv 10202

cn 10532

c2 10581

cn0 10791

cz 10860

cuz 11078

crp 11216

cicc 11528

cfz 11668

cfl 11891

cexp 12130

chash 12369

csu 13467

cprime 14072

clog 22670

ccxp 22671

ccht 23092 ψcchp 23094

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 6574 ax-inf2 8054 ax-cnex 9544 ax-resscn 9545 ax-1cn 9546 ax-icn 9547 ax-addcl 9548 ax-addrcl 9549 ax-mulcl 9550 ax-mulrcl 9551 ax-mulcom 9552 ax-addass 9553 ax-mulass 9554 ax-distr 9555 ax-i2m1 9556 ax-1ne0 9557 ax-1rid 9558 ax-rnegex 9559 ax-rrecex 9560 ax-cnre 9561 ax-pre-lttri 9562 ax-pre-lttrn 9563 ax-pre-ltadd 9564 ax-pre-mulgt0 9565 ax-pre-sup 9566 ax-addf 9567 ax-mulf 9568

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-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 5549 df-fun 5588 df-fn 5589 df-f 5590 df-f1 5591 df-fo 5592 df-f1o 5593 df-fv 5594 df-isom 5595 df-riota 6243 df-ov 6285 df-oprab 6286 df-mpt2 6287 df-of 6522 df-om 6679 df-1st 6781 df-2nd 6782 df-supp 6899 df-recs 7039 df-rdg 7073 df-1o 7127 df-2o 7128 df-oadd 7131 df-er 7308 df-map 7419 df-pm 7420 df-ixp 7467 df-en 7514 df-dom 7515 df-sdom 7516 df-fin 7517 df-fsupp 7826 df-fi 7867 df-sup 7897 df-oi 7931 df-card 8316 df-cda 8544 df-pnf 9626 df-mnf 9627 df-xr 9628 df-ltxr 9629 df-le 9630 df-sub 9803 df-neg 9804 df-div 10203 df-nn 10533 df-2 10590 df-3 10591 df-4 10592 df-5 10593 df-6 10594 df-7 10595 df-8 10596 df-9 10597 df-10 10598 df-n0 10792 df-z 10861 df-dec 10973 df-uz 11079 df-q 11179 df-rp 11217 df-xneg 11314 df-xadd 11315 df-xmul 11316 df-ioo 11529 df-ioc 11530 df-ico 11531 df-icc 11532 df-fz 11669 df-fzo 11789 df-fl 11893 df-mod 11961 df-seq 12072 df-exp 12131 df-fac 12318 df-bc 12345 df-hash 12370 df-shft 12859 df-cj 12891 df-re 12892 df-im 12893 df-sqrt 13027 df-abs 13028 df-limsup 13253 df-clim 13270 df-rlim 13271 df-sum 13468 df-ef 13661 df-sin 13663 df-cos 13664 df-pi 13666 df-dvds 13844 df-gcd 14000 df-prm 14073 df-pc 14216 df-struct 14488 df-ndx 14489 df-slot 14490 df-base 14491 df-sets 14492 df-ress 14493 df-plusg 14564 df-mulr 14565 df-starv 14566 df-sca 14567 df-vsca 14568 df-ip 14569 df-tset 14570 df-ple 14571 df-ds 14573 df-unif 14574 df-hom 14575 df-cco 14576 df-rest 14674 df-topn 14675 df-0g 14693 df-gsum 14694 df-topgen 14695 df-pt 14696 df-prds 14699 df-xrs 14753 df-qtop 14758 df-imas 14759 df-xps 14761 df-mre 14837 df-mrc 14838 df-acs 14840 df-mnd 15728 df-submnd 15778 df-mulg 15861 df-cntz 16150 df-cmn 16596 df-psmet 18182 df-xmet 18183 df-met 18184 df-bl 18185 df-mopn 18186 df-fbas 18187 df-fg 18188 df-cnfld 18192 df-top 19166 df-bases 19168 df-topon 19169 df-topsp 19170 df-cld 19286 df-ntr 19287 df-cls 19288 df-nei 19365 df-lp 19403 df-perf 19404 df-cn 19494 df-cnp 19495 df-haus 19582 df-tx 19798 df-hmeo 19991 df-fil 20082 df-fm 20174 df-flim 20175 df-flf 20176 df-xms 20558 df-ms 20559 df-tms 20560 df-cncf 21117 df-limc 22005 df-dv 22006 df-log 22672 df-cxp 22673 df-cht 23098 df-vma 23099 df-chp 23100

This theorem is referenced by: (None)

W3C validator