chpchtsum - Metamath Proof Explorer

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

Theorem chpchtsum 23363

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 12059	. . . . 5 $/\$
2		inss2 3702	. . . . . . . . . 10
3		simpr 461	. . . . . . . . . 10 $/\$
4	2, 3	sseldi 3485	. . . . . . . . 9 $/\$
5		prmnn 14094	. . . . . . . . 9
6	4, 5	syl 16	. . . . . . . 8 $/\$
7	6	nnrpd 11261	. . . . . . 7 $/\$
8	7	relogcld 22877	. . . . . 6 $/\$
9	8	recnd 9622	. . . . 5 $/\$
10		fsumconst 13581	. . . . 5 $/\$
11	1, 9, 10	syl2anc 661	. . . 4 $/\$
12		simpl 457	. . . . . . . . . 10 $/\$
13		1red 9611	. . . . . . . . . . 11 $/\$
14	6	nnred 10554	. . . . . . . . . . 11 $/\$
15		prmuz2 14109	. . . . . . . . . . . . 13
16	4, 15	syl 16	. . . . . . . . . . . 12 $/\$
17		eluz2b2 11160	. . . . . . . . . . . . 13 $/\$
18	17	simprbi 464	. . . . . . . . . . . 12
19	16, 18	syl 16	. . . . . . . . . . 11 $/\$
20		inss1 3701	. . . . . . . . . . . . . 14
21	20, 3	sseldi 3485	. . . . . . . . . . . . 13 $/\$
22		0re 9596	. . . . . . . . . . . . . 14
23		elicc2 11595	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
24	22, 12, 23	sylancr 663	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
25	21, 24	mpbid 210	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
26	25	simp3d 1009	. . . . . . . . . . 11 $/\$
27	13, 14, 12, 19, 26	ltletrd 9742	. . . . . . . . . 10 $/\$
28	12, 27	rplogcld 22883	. . . . . . . . 9 $/\$
29	14, 19	rplogcld 22883	. . . . . . . . 9 $/\$
30	28, 29	rpdivcld 11279	. . . . . . . 8 $/\$
31	30	rpred 11262	. . . . . . 7 $/\$
32	30	rpge0d 11266	. . . . . . 7 $/\$
33		flge0nn0 11930	. . . . . . 7 $/\$
34	31, 32, 33	syl2anc 661	. . . . . 6 $/\$
35		hashfz1 12395	. . . . . 6
36	34, 35	syl 16	. . . . 5 $/\$
37	36	oveq1d 6293	. . . 4 $/\$
38	31	flcld 11911	. . . . . 6 $/\$
39	38	zcnd 10972	. . . . 5 $/\$
40	39, 9	mulcomd 9617	. . . 4 $/\$
41	11, 37, 40	3eqtrrd 2487	. . 3 $/\$
42	41	sumeq2dv 13501	. 2
43		chpval2 23362	. 2 ψ
44		simpl 457	. . . . . 6 $/\$
45		0red 9597	. . . . . . 7 $/\$
46		1red 9611	. . . . . . . 8 $/\$
47		0lt1 10078	. . . . . . . . 9
48	47	a1i 11	. . . . . . . 8 $/\$
49		elfzuz2 11697	. . . . . . . . 9
50		eluzle 11099	. . . . . . . . . . 11
51	50	adantl 466	. . . . . . . . . 10 $/\$
52		simpl 457	. . . . . . . . . . 11 $/\$
53		1z 10897	. . . . . . . . . . 11
54		flge 11918	. . . . . . . . . . 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 9742	. . . . . . 7 $/\$
59	45, 44, 58	ltled 9733	. . . . . 6 $/\$
60		elfznn 11720	. . . . . . . 8
61	60	adantl 466	. . . . . . 7 $/\$
62	61	nnrecred 10584	. . . . . 6 $/\$
63	44, 59, 62	recxpcld 22973	. . . . 5 $/\$
64		chtval 23253	. . . . 5
65	63, 64	syl 16	. . . 4 $/\$
66	65	sumeq2dv 13501	. . 3
67		ppifi 23248	. . . 4
68		fzfid 12059	. . . 4
69	2	sseli 3483	. . . . . . . 8
70		elfznn 11720	. . . . . . . 8
71	69, 70	anim12i 566	. . . . . . 7 $/\$ $/\$
72	71	a1i 11	. . . . . 6 $/\$ $/\$
73		0red 9597	. . . . . . . . 9 $/\$
74	2	a1i 11	. . . . . . . . . . . 12
75	74	sselda 3487	. . . . . . . . . . 11 $/\$
76	75, 5	syl 16	. . . . . . . . . 10 $/\$
77	76	nnred 10554	. . . . . . . . 9 $/\$
78	76	nngt0d 10582	. . . . . . . . 9 $/\$
79	73, 77, 12, 78, 26	ltletrd 9742	. . . . . . . 8 $/\$
80	79	ex 434	. . . . . . 7
81	80	adantrd 468	. . . . . 6 $/\$
82	72, 81	jcad 533	. . . . 5 $/\$ $/\$ $/\$
83		inss2 3702	. . . . . . . . 9
84	83	sseli 3483	. . . . . . . 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 3670	. . . . . . . . 9 $/\$
91		simprll 761	. . . . . . . . . . 11 $/\$ $/\$ $/\$
92	91	biantrud 507	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
93		0red 9597	. . . . . . . . . . 11 $/\$ $/\$ $/\$
94		simpl 457	. . . . . . . . . . 11 $/\$ $/\$ $/\$
95	91, 5	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
96	95	nnred 10554	. . . . . . . . . . 11 $/\$ $/\$ $/\$
97	95	nnnn0d 10855	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
98	97	nn0ge0d 10858	. . . . . . . . . . 11 $/\$ $/\$ $/\$
99		df-3an 974	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
100	23, 99	syl6bb 261	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
101	100	baibd 907	. . . . . . . . . . 11 $/\$ $/\$ $/\$
102	93, 94, 96, 98, 101	syl22anc 1228	. . . . . . . . . 10 $/\$ $/\$ $/\$
103	92, 102	bitr3d 255	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
104	90, 103	syl5bb 257	. . . . . . . 8 $/\$ $/\$ $/\$
105		simprr 756	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
106	94, 105	elrpd 11260	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
107	106	relogcld 22877	. . . . . . . . . . 11 $/\$ $/\$ $/\$
108	91, 15	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
109	108, 18	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
110	96, 109	rplogcld 22883	. . . . . . . . . . 11 $/\$ $/\$ $/\$
111	107, 110	rerpdivcld 11289	. . . . . . . . . 10 $/\$ $/\$ $/\$
112		simprlr 762	. . . . . . . . . . 11 $/\$ $/\$ $/\$
113	112	nnzd 10970	. . . . . . . . . 10 $/\$ $/\$ $/\$
114		flge 11918	. . . . . . . . . 10 $/\$
115	111, 113, 114	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$
116	112	nnnn0d 10855	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
117	95, 116	nnexpcld 12307	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
118	117	nnrpd 11261	. . . . . . . . . . 11 $/\$ $/\$ $/\$
119	118, 106	logled 22881	. . . . . . . . . 10 $/\$ $/\$ $/\$
120	95	nnrpd 11261	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
121		relogexp 22849	. . . . . . . . . . . 12 $/\$
122	120, 113, 121	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$
123	122	breq1d 4444	. . . . . . . . . 10 $/\$ $/\$ $/\$
124	112	nnred 10554	. . . . . . . . . . 11 $/\$ $/\$ $/\$
125	124, 107, 110	lemuldivd 11307	. . . . . . . . . 10 $/\$ $/\$ $/\$
126	119, 123, 125	3bitrd 279	. . . . . . . . 9 $/\$ $/\$ $/\$
127		nnuz 11122	. . . . . . . . . . 11
128	112, 127	syl6eleq 2539	. . . . . . . . . 10 $/\$ $/\$ $/\$
129	111	flcld 11911	. . . . . . . . . 10 $/\$ $/\$ $/\$
130		elfz5 11686	. . . . . . . . . 10 $/\$
131	128, 129, 130	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$
132	115, 126, 131	3bitr4rd 286	. . . . . . . 8 $/\$ $/\$ $/\$
133	104, 132	anbi12d 710	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
134	94	flcld 11911	. . . . . . . . . . 11 $/\$ $/\$ $/\$
135		elfz5 11686	. . . . . . . . . . 11 $/\$
136	128, 134, 135	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$
137		flge 11918	. . . . . . . . . . 11 $/\$
138	94, 113, 137	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$
139	136, 138	bitr4d 256	. . . . . . . . 9 $/\$ $/\$ $/\$
140		elin 3670	. . . . . . . . . 10 $/\$
141	91	biantrud 507	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
142	106	rpge0d 11266	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
143	112	nnrecred 10584	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
144	94, 142, 143	recxpcld 22973	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
145		elicc2 11595	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
146		df-3an 974	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
147	145, 146	syl6bb 261	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
148	147	baibd 907	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
149	93, 144, 96, 98, 148	syl22anc 1228	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
150	141, 149	bitr3d 255	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
151	94, 142, 143	cxpge0d 22974	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152	112	nnrpd 11261	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
153	96, 98, 144, 151, 152	cxple2d 22977	. . . . . . . . . . 11 $/\$ $/\$ $/\$
154	95	nncnd 10555	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
155		cxpexp 22918	. . . . . . . . . . . . 13 $/\$
156	154, 116, 155	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
157	112	nncnd 10555	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
158	112	nnne0d 10583	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
159	157, 158	recid2d 10319	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
160	159	oveq2d 6294	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
161	106, 143, 157	cxpmuld 22984	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
162	94	recnd 9622	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
163	162	cxp1d 22956	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
164	160, 161, 163	3eqtr3d 2490	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
165	156, 164	breq12d 4447	. . . . . . . . . . 11 $/\$ $/\$ $/\$
166	150, 153, 165	3bitrd 279	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
167	140, 166	syl5bb 257	. . . . . . . . 9 $/\$ $/\$ $/\$
168	139, 167	anbi12d 710	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
169	117	nnred 10554	. . . . . . . . . . 11 $/\$ $/\$ $/\$
170		bernneq3 12270	. . . . . . . . . . . 12 $/\$
171	108, 116, 170	syl2anc 661	. . . . . . . . . . 11 $/\$ $/\$ $/\$
172	124, 169, 171	ltled 9733	. . . . . . . . . 10 $/\$ $/\$ $/\$
173		letr 9678	. . . . . . . . . . 11 $/\$ $/\$ $/\$
174	124, 169, 94, 173	syl3anc 1227	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
175	172, 174	mpand 675	. . . . . . . . 9 $/\$ $/\$ $/\$
176	175	pm4.71rd 635	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
177	154	exp1d 12281	. . . . . . . . . . 11 $/\$ $/\$ $/\$
178	95	nnge1d 10581	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
179	96, 178, 128	leexp2ad 12318	. . . . . . . . . . 11 $/\$ $/\$ $/\$
180	177, 179	eqbrtrrd 4456	. . . . . . . . . 10 $/\$ $/\$ $/\$
181		letr 9678	. . . . . . . . . . 11 $/\$ $/\$ $/\$
182	96, 169, 94, 181	syl3anc 1227	. . . . . . . . . 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 13565	. . 3
191	66, 190	eqtr4d 2485	. 2
192	42, 43, 191	3eqtr4d 2492	1 ψ

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1381

wcel 1802

cin 3458

wss 3459 class class class wbr 4434

cfv 5575 (class class class)co 6278

cfn 7515

cc 9490

cr 9491

cc0 9492

c1 9493

cmul 9497

clt 9628

cle 9629

cdiv 10209

cn 10539

c2 10588

cn0 10798

cz 10867

cuz 11087

crp 11226

cicc 11538

cfz 11678

cfl 11903

cexp 12142

chash 12381

csu 13484

cprime 14091

clog 22811

ccxp 22812

ccht 23233 ψcchp 23235

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1603 ax-4 1616 ax-5 1689 ax-6 1732 ax-7 1774 ax-8 1804 ax-9 1806 ax-10 1821 ax-11 1826 ax-12 1838 ax-13 1983 ax-ext 2419 ax-rep 4545 ax-sep 4555 ax-nul 4563 ax-pow 4612 ax-pr 4673 ax-un 6574 ax-inf2 8058 ax-cnex 9548 ax-resscn 9549 ax-1cn 9550 ax-icn 9551 ax-addcl 9552 ax-addrcl 9553 ax-mulcl 9554 ax-mulrcl 9555 ax-mulcom 9556 ax-addass 9557 ax-mulass 9558 ax-distr 9559 ax-i2m1 9560 ax-1ne0 9561 ax-1rid 9562 ax-rnegex 9563 ax-rrecex 9564 ax-cnre 9565 ax-pre-lttri 9566 ax-pre-lttrn 9567 ax-pre-ltadd 9568 ax-pre-mulgt0 9569 ax-pre-sup 9570 ax-addf 9571 ax-mulf 9572

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 973 df-3an 974 df-tru 1384 df-fal 1387 df-ex 1598 df-nf 1602 df-sb 1725 df-eu 2270 df-mo 2271 df-clab 2427 df-cleq 2433 df-clel 2436 df-nfc 2591 df-ne 2638 df-nel 2639 df-ral 2796 df-rex 2797 df-reu 2798 df-rmo 2799 df-rab 2800 df-v 3095 df-sbc 3312 df-csb 3419 df-dif 3462 df-un 3464 df-in 3466 df-ss 3473 df-pss 3475 df-nul 3769 df-if 3924 df-pw 3996 df-sn 4012 df-pr 4014 df-tp 4016 df-op 4018 df-uni 4232 df-int 4269 df-iun 4314 df-iin 4315 df-br 4435 df-opab 4493 df-mpt 4494 df-tr 4528 df-eprel 4778 df-id 4782 df-po 4787 df-so 4788 df-fr 4825 df-se 4826 df-we 4827 df-ord 4868 df-on 4869 df-lim 4870 df-suc 4871 df-xp 4992 df-rel 4993 df-cnv 4994 df-co 4995 df-dm 4996 df-rn 4997 df-res 4998 df-ima 4999 df-iota 5538 df-fun 5577 df-fn 5578 df-f 5579 df-f1 5580 df-fo 5581 df-f1o 5582 df-fv 5583 df-isom 5584 df-riota 6239 df-ov 6281 df-oprab 6282 df-mpt2 6283 df-of 6522 df-om 6683 df-1st 6782 df-2nd 6783 df-supp 6901 df-recs 7041 df-rdg 7075 df-1o 7129 df-2o 7130 df-oadd 7133 df-er 7310 df-map 7421 df-pm 7422 df-ixp 7469 df-en 7516 df-dom 7517 df-sdom 7518 df-fin 7519 df-fsupp 7829 df-fi 7870 df-sup 7900 df-oi 7935 df-card 8320 df-cda 8548 df-pnf 9630 df-mnf 9631 df-xr 9632 df-ltxr 9633 df-le 9634 df-sub 9809 df-neg 9810 df-div 10210 df-nn 10540 df-2 10597 df-3 10598 df-4 10599 df-5 10600 df-6 10601 df-7 10602 df-8 10603 df-9 10604 df-10 10605 df-n0 10799 df-z 10868 df-dec 10982 df-uz 11088 df-q 11189 df-rp 11227 df-xneg 11324 df-xadd 11325 df-xmul 11326 df-ioo 11539 df-ioc 11540 df-ico 11541 df-icc 11542 df-fz 11679 df-fzo 11801 df-fl 11905 df-mod 11973 df-seq 12084 df-exp 12143 df-fac 12330 df-bc 12357 df-hash 12382 df-shft 12876 df-cj 12908 df-re 12909 df-im 12910 df-sqrt 13044 df-abs 13045 df-limsup 13270 df-clim 13287 df-rlim 13288 df-sum 13485 df-ef 13678 df-sin 13680 df-cos 13681 df-pi 13683 df-dvds 13861 df-gcd 14019 df-prm 14092 df-pc 14235 df-struct 14508 df-ndx 14509 df-slot 14510 df-base 14511 df-sets 14512 df-ress 14513 df-plusg 14584 df-mulr 14585 df-starv 14586 df-sca 14587 df-vsca 14588 df-ip 14589 df-tset 14590 df-ple 14591 df-ds 14593 df-unif 14594 df-hom 14595 df-cco 14596 df-rest 14694 df-topn 14695 df-0g 14713 df-gsum 14714 df-topgen 14715 df-pt 14716 df-prds 14719 df-xrs 14773 df-qtop 14778 df-imas 14779 df-xps 14781 df-mre 14857 df-mrc 14858 df-acs 14860 df-mgm 15743 df-sgrp 15782 df-mnd 15792 df-submnd 15838 df-mulg 15931 df-cntz 16226 df-cmn 16671 df-psmet 18282 df-xmet 18283 df-met 18284 df-bl 18285 df-mopn 18286 df-fbas 18287 df-fg 18288 df-cnfld 18292 df-top 19269 df-bases 19271 df-topon 19272 df-topsp 19273 df-cld 19390 df-ntr 19391 df-cls 19392 df-nei 19469 df-lp 19507 df-perf 19508 df-cn 19598 df-cnp 19599 df-haus 19686 df-tx 19933 df-hmeo 20126 df-fil 20217 df-fm 20309 df-flim 20310 df-flf 20311 df-xms 20693 df-ms 20694 df-tms 20695 df-cncf 21252 df-limc 22140 df-dv 22141 df-log 22813 df-cxp 22814 df-cht 23239 df-vma 23240 df-chp 23241

This theorem is referenced by: (None)

W3C validator