chpchtsum - Metamath Proof Explorer

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

Theorem chpchtsum 20956

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 11267	. . . . 5 $/\$
2		inss2 3522	. . . . . . . . . 10
3		simpr 448	. . . . . . . . . 10 $/\$
4	2, 3	sseldi 3306	. . . . . . . . 9 $/\$
5		prmnn 13037	. . . . . . . . 9
6	4, 5	syl 16	. . . . . . . 8 $/\$
7	6	nnrpd 10603	. . . . . . 7 $/\$
8	7	relogcld 20471	. . . . . 6 $/\$
9	8	recnd 9070	. . . . 5 $/\$
10		fsumconst 12528	. . . . 5 $/\$
11	1, 9, 10	syl2anc 643	. . . 4 $/\$
12		simpl 444	. . . . . . . . . 10 $/\$
13		1re 9046	. . . . . . . . . . . 12
14	13	a1i 11	. . . . . . . . . . 11 $/\$
15	6	nnred 9971	. . . . . . . . . . 11 $/\$
16		prmuz2 13052	. . . . . . . . . . . . 13
17	4, 16	syl 16	. . . . . . . . . . . 12 $/\$
18		eluz2b2 10504	. . . . . . . . . . . . 13 $/\$
19	18	simprbi 451	. . . . . . . . . . . 12
20	17, 19	syl 16	. . . . . . . . . . 11 $/\$
21		inss1 3521	. . . . . . . . . . . . . 14
22	21, 3	sseldi 3306	. . . . . . . . . . . . 13 $/\$
23		0re 9047	. . . . . . . . . . . . . 14
24		elicc2 10931	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
25	23, 12, 24	sylancr 645	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
26	22, 25	mpbid 202	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
27	26	simp3d 971	. . . . . . . . . . 11 $/\$
28	14, 15, 12, 20, 27	ltletrd 9186	. . . . . . . . . 10 $/\$
29	12, 28	rplogcld 20477	. . . . . . . . 9 $/\$
30	15, 20	rplogcld 20477	. . . . . . . . 9 $/\$
31	29, 30	rpdivcld 10621	. . . . . . . 8 $/\$
32	31	rpred 10604	. . . . . . 7 $/\$
33	31	rpge0d 10608	. . . . . . 7 $/\$
34		flge0nn0 11180	. . . . . . 7 $/\$
35	32, 33, 34	syl2anc 643	. . . . . 6 $/\$
36		hashfz1 11585	. . . . . 6
37	35, 36	syl 16	. . . . 5 $/\$
38	37	oveq1d 6055	. . . 4 $/\$
39	32	flcld 11162	. . . . . 6 $/\$
40	39	zcnd 10332	. . . . 5 $/\$
41	40, 9	mulcomd 9065	. . . 4 $/\$
42	11, 38, 41	3eqtrrd 2441	. . 3 $/\$
43	42	sumeq2dv 12452	. 2
44		chpval2 20955	. 2 ψ
45		simpl 444	. . . . . 6 $/\$
46	23	a1i 11	. . . . . . 7 $/\$
47	13	a1i 11	. . . . . . . 8 $/\$
48		0lt1 9506	. . . . . . . . 9
49	48	a1i 11	. . . . . . . 8 $/\$
50		elfzuz2 11018	. . . . . . . . 9
51		eluzle 10454	. . . . . . . . . . 11
52	51	adantl 453	. . . . . . . . . 10 $/\$
53		simpl 444	. . . . . . . . . . 11 $/\$
54		1z 10267	. . . . . . . . . . 11
55		flge 11169	. . . . . . . . . . 11 $/\$
56	53, 54, 55	sylancl 644	. . . . . . . . . 10 $/\$
57	52, 56	mpbird 224	. . . . . . . . 9 $/\$
58	50, 57	sylan2 461	. . . . . . . 8 $/\$
59	46, 47, 45, 49, 58	ltletrd 9186	. . . . . . 7 $/\$
60	46, 45, 59	ltled 9177	. . . . . 6 $/\$
61		elfznn 11036	. . . . . . . 8
62	61	adantl 453	. . . . . . 7 $/\$
63	62	nnrecred 10001	. . . . . 6 $/\$
64	45, 60, 63	recxpcld 20567	. . . . 5 $/\$
65		chtval 20846	. . . . 5
66	64, 65	syl 16	. . . 4 $/\$
67	66	sumeq2dv 12452	. . 3
68		ppifi 20841	. . . 4
69		fzfid 11267	. . . 4
70	2	sseli 3304	. . . . . . . 8
71		elfznn 11036	. . . . . . . 8
72	70, 71	anim12i 550	. . . . . . 7 $/\$ $/\$
73	72	a1i 11	. . . . . 6 $/\$ $/\$
74	23	a1i 11	. . . . . . . . 9 $/\$
75	2	a1i 11	. . . . . . . . . . . 12
76	75	sselda 3308	. . . . . . . . . . 11 $/\$
77	76, 5	syl 16	. . . . . . . . . 10 $/\$
78	77	nnred 9971	. . . . . . . . 9 $/\$
79	77	nngt0d 9999	. . . . . . . . 9 $/\$
80	74, 78, 12, 79, 27	ltletrd 9186	. . . . . . . 8 $/\$
81	80	ex 424	. . . . . . 7
82	81	adantrd 455	. . . . . 6 $/\$
83	73, 82	jcad 520	. . . . 5 $/\$ $/\$ $/\$
84		inss2 3522	. . . . . . . . 9
85	84	sseli 3304	. . . . . . . 8
86	61, 85	anim12ci 551	. . . . . . 7 $/\$ $/\$
87	86	a1i 11	. . . . . 6 $/\$ $/\$
88	59	ex 424	. . . . . . 7
89	88	adantrd 455	. . . . . 6 $/\$
90	87, 89	jcad 520	. . . . 5 $/\$ $/\$ $/\$
91		elin 3490	. . . . . . . . 9 $/\$
92		simprll 739	. . . . . . . . . . 11 $/\$ $/\$ $/\$
93	92	biantrud 494	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
94	23	a1i 11	. . . . . . . . . . 11 $/\$ $/\$ $/\$
95		simpl 444	. . . . . . . . . . 11 $/\$ $/\$ $/\$
96	92, 5	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
97	96	nnred 9971	. . . . . . . . . . 11 $/\$ $/\$ $/\$
98	96	nnnn0d 10230	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
99	98	nn0ge0d 10233	. . . . . . . . . . 11 $/\$ $/\$ $/\$
100		df-3an 938	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
101	24, 100	syl6bb 253	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
102	101	baibd 876	. . . . . . . . . . 11 $/\$ $/\$ $/\$
103	94, 95, 97, 99, 102	syl22anc 1185	. . . . . . . . . 10 $/\$ $/\$ $/\$
104	93, 103	bitr3d 247	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
105	91, 104	syl5bb 249	. . . . . . . 8 $/\$ $/\$ $/\$
106		simprr 734	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
107	95, 106	elrpd 10602	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
108	107	relogcld 20471	. . . . . . . . . . 11 $/\$ $/\$ $/\$
109	92, 16	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
110	109, 19	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
111	97, 110	rplogcld 20477	. . . . . . . . . . 11 $/\$ $/\$ $/\$
112	108, 111	rerpdivcld 10631	. . . . . . . . . 10 $/\$ $/\$ $/\$
113		simprlr 740	. . . . . . . . . . 11 $/\$ $/\$ $/\$
114	113	nnzd 10330	. . . . . . . . . 10 $/\$ $/\$ $/\$
115		flge 11169	. . . . . . . . . 10 $/\$
116	112, 114, 115	syl2anc 643	. . . . . . . . 9 $/\$ $/\$ $/\$
117	113	nnnn0d 10230	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
118	96, 117	nnexpcld 11499	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
119	118	nnrpd 10603	. . . . . . . . . . 11 $/\$ $/\$ $/\$
120	119, 107	logled 20475	. . . . . . . . . 10 $/\$ $/\$ $/\$
121	96	nnrpd 10603	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
122		relogexp 20443	. . . . . . . . . . . 12 $/\$
123	121, 114, 122	syl2anc 643	. . . . . . . . . . 11 $/\$ $/\$ $/\$
124	123	breq1d 4182	. . . . . . . . . 10 $/\$ $/\$ $/\$
125	113	nnred 9971	. . . . . . . . . . 11 $/\$ $/\$ $/\$
126	125, 108, 111	lemuldivd 10649	. . . . . . . . . 10 $/\$ $/\$ $/\$
127	120, 124, 126	3bitrd 271	. . . . . . . . 9 $/\$ $/\$ $/\$
128		nnuz 10477	. . . . . . . . . . 11
129	113, 128	syl6eleq 2494	. . . . . . . . . 10 $/\$ $/\$ $/\$
130	112	flcld 11162	. . . . . . . . . 10 $/\$ $/\$ $/\$
131		elfz5 11007	. . . . . . . . . 10 $/\$
132	129, 130, 131	syl2anc 643	. . . . . . . . 9 $/\$ $/\$ $/\$
133	116, 127, 132	3bitr4rd 278	. . . . . . . 8 $/\$ $/\$ $/\$
134	105, 133	anbi12d 692	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
135	95	flcld 11162	. . . . . . . . . . 11 $/\$ $/\$ $/\$
136		elfz5 11007	. . . . . . . . . . 11 $/\$
137	129, 135, 136	syl2anc 643	. . . . . . . . . 10 $/\$ $/\$ $/\$
138		flge 11169	. . . . . . . . . . 11 $/\$
139	95, 114, 138	syl2anc 643	. . . . . . . . . 10 $/\$ $/\$ $/\$
140	137, 139	bitr4d 248	. . . . . . . . 9 $/\$ $/\$ $/\$
141		elin 3490	. . . . . . . . . 10 $/\$
142	92	biantrud 494	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
143	107	rpge0d 10608	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
144	113	nnrecred 10001	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
145	95, 143, 144	recxpcld 20567	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
146		elicc2 10931	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
147		df-3an 938	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
148	146, 147	syl6bb 253	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
149	148	baibd 876	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
150	94, 145, 97, 99, 149	syl22anc 1185	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
151	142, 150	bitr3d 247	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
152	95, 143, 144	cxpge0d 20568	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
153	113	nnrpd 10603	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
154	97, 99, 145, 152, 153	cxple2d 20571	. . . . . . . . . . 11 $/\$ $/\$ $/\$
155	96	nncnd 9972	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
156		cxpexp 20512	. . . . . . . . . . . . 13 $/\$
157	155, 117, 156	syl2anc 643	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
158	113	nncnd 9972	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
159	113	nnne0d 10000	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
160	158, 159	recid2d 9742	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
161	160	oveq2d 6056	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
162	107, 144, 158	cxpmuld 20578	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
163	95	recnd 9070	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
164	163	cxp1d 20550	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
165	161, 162, 164	3eqtr3d 2444	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
166	157, 165	breq12d 4185	. . . . . . . . . . 11 $/\$ $/\$ $/\$
167	151, 154, 166	3bitrd 271	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
168	141, 167	syl5bb 249	. . . . . . . . 9 $/\$ $/\$ $/\$
169	140, 168	anbi12d 692	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
170	118	nnred 9971	. . . . . . . . . . 11 $/\$ $/\$ $/\$
171		bernneq3 11462	. . . . . . . . . . . 12 $/\$
172	109, 117, 171	syl2anc 643	. . . . . . . . . . 11 $/\$ $/\$ $/\$
173	125, 170, 172	ltled 9177	. . . . . . . . . 10 $/\$ $/\$ $/\$
174		letr 9123	. . . . . . . . . . 11 $/\$ $/\$ $/\$
175	125, 170, 95, 174	syl3anc 1184	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
176	173, 175	mpand 657	. . . . . . . . 9 $/\$ $/\$ $/\$
177	176	pm4.71rd 617	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
178	155	exp1d 11473	. . . . . . . . . . 11 $/\$ $/\$ $/\$
179	96	nnge1d 9998	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
180	97, 179, 129	leexp2ad 11510	. . . . . . . . . . 11 $/\$ $/\$ $/\$
181	178, 180	eqbrtrrd 4194	. . . . . . . . . 10 $/\$ $/\$ $/\$
182		letr 9123	. . . . . . . . . . 11 $/\$ $/\$ $/\$
183	97, 170, 95, 182	syl3anc 1184	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
184	181, 183	mpand 657	. . . . . . . . 9 $/\$ $/\$ $/\$
185	184	pm4.71rd 617	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
186	169, 177, 185	3bitr2rd 274	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
187	134, 186	bitrd 245	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
188	187	ex 424	. . . . 5 $/\$ $/\$ $/\$ $/\$
189	83, 90, 188	pm5.21ndd 344	. . . 4 $/\$ $/\$
190	9	adantrr 698	. . . 4 $/\$ $/\$
191	68, 69, 1, 189, 190	fsumcom2 12513	. . 3
192	67, 191	eqtr4d 2439	. 2
193	43, 44, 192	3eqtr4d 2446	1 ψ

Colors of variables: wff set class

Syntax hints:

wi 4

wb 177 $/\$ wa 359 $/\$ w3a 936

wceq 1649

wcel 1721

cin 3279

wss 3280 class class class wbr 4172

cfv 5413 (class class class)co 6040

cfn 7068

cc 8944

cr 8945

cc0 8946

c1 8947

cmul 8951

clt 9076

cle 9077

cdiv 9633

cn 9956

c2 10005

cn0 10177

cz 10238

cuz 10444

crp 10568

cicc 10875

cfz 10999

cfl 11156

cexp 11337

chash 11573

csu 12434

cprime 13034

clog 20405

ccxp 20406

ccht 20826 ψcchp 20828

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-inf2 7552 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024 ax-addf 9025 ax-mulf 9026

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-iin 4056 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-se 4502 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-of 6264 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-2o 6684 df-oadd 6687 df-er 6864 df-map 6979 df-pm 6980 df-ixp 7023 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-fi 7374 df-sup 7404 df-oi 7435 df-card 7782 df-cda 8004 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-2 10014 df-3 10015 df-4 10016 df-5 10017 df-6 10018 df-7 10019 df-8 10020 df-9 10021 df-10 10022 df-n0 10178 df-z 10239 df-dec 10339 df-uz 10445 df-q 10531 df-rp 10569 df-xneg 10666 df-xadd 10667 df-xmul 10668 df-ioo 10876 df-ioc 10877 df-ico 10878 df-icc 10879 df-fz 11000 df-fzo 11091 df-fl 11157 df-mod 11206 df-seq 11279 df-exp 11338 df-fac 11522 df-bc 11549 df-hash 11574 df-shft 11837 df-cj 11859 df-re 11860 df-im 11861 df-sqr 11995 df-abs 11996 df-limsup 12220 df-clim 12237 df-rlim 12238 df-sum 12435 df-ef 12625 df-sin 12627 df-cos 12628 df-pi 12630 df-dvds 12808 df-gcd 12962 df-prm 13035 df-pc 13166 df-struct 13426 df-ndx 13427 df-slot 13428 df-base 13429 df-sets 13430 df-ress 13431 df-plusg 13497 df-mulr 13498 df-starv 13499 df-sca 13500 df-vsca 13501 df-tset 13503 df-ple 13504 df-ds 13506 df-unif 13507 df-hom 13508 df-cco 13509 df-rest 13605 df-topn 13606 df-topgen 13622 df-pt 13623 df-prds 13626 df-xrs 13681 df-0g 13682 df-gsum 13683 df-qtop 13688 df-imas 13689 df-xps 13691 df-mre 13766 df-mrc 13767 df-acs 13769 df-mnd 14645 df-submnd 14694 df-mulg 14770 df-cntz 15071 df-cmn 15369 df-psmet 16649 df-xmet 16650 df-met 16651 df-bl 16652 df-mopn 16653 df-fbas 16654 df-fg 16655 df-cnfld 16659 df-top 16918 df-bases 16920 df-topon 16921 df-topsp 16922 df-cld 17038 df-ntr 17039 df-cls 17040 df-nei 17117 df-lp 17155 df-perf 17156 df-cn 17245 df-cnp 17246 df-haus 17333 df-tx 17547 df-hmeo 17740 df-fil 17831 df-fm 17923 df-flim 17924 df-flf 17925 df-xms 18303 df-ms 18304 df-tms 18305 df-cncf 18861 df-limc 19706 df-dv 19707 df-log 20407 df-cxp 20408 df-cht 20832 df-vma 20833 df-chp 20834

W3C validator