chpchtsum - Metamath Proof Explorer

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

Theorem chpchtsum 23692

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 12065	. . . . 5 $/\$
2		inss2 3705	. . . . . . . . . 10
3		simpr 459	. . . . . . . . . 10 $/\$
4	2, 3	sseldi 3487	. . . . . . . . 9 $/\$
5		prmnn 14304	. . . . . . . . 9
6	4, 5	syl 16	. . . . . . . 8 $/\$
7	6	nnrpd 11257	. . . . . . 7 $/\$
8	7	relogcld 23176	. . . . . 6 $/\$
9	8	recnd 9611	. . . . 5 $/\$
10		fsumconst 13687	. . . . 5 $/\$
11	1, 9, 10	syl2anc 659	. . . 4 $/\$
12		simpl 455	. . . . . . . . . 10 $/\$
13		1red 9600	. . . . . . . . . . 11 $/\$
14	6	nnred 10546	. . . . . . . . . . 11 $/\$
15		prmuz2 14319	. . . . . . . . . . . . 13
16	4, 15	syl 16	. . . . . . . . . . . 12 $/\$
17		eluz2b2 11155	. . . . . . . . . . . . 13 $/\$
18	17	simprbi 462	. . . . . . . . . . . 12
19	16, 18	syl 16	. . . . . . . . . . 11 $/\$
20		inss1 3704	. . . . . . . . . . . . . 14
21	20, 3	sseldi 3487	. . . . . . . . . . . . 13 $/\$
22		0re 9585	. . . . . . . . . . . . . 14
23		elicc2 11592	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
24	22, 12, 23	sylancr 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
25	21, 24	mpbid 210	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
26	25	simp3d 1008	. . . . . . . . . . 11 $/\$
27	13, 14, 12, 19, 26	ltletrd 9731	. . . . . . . . . 10 $/\$
28	12, 27	rplogcld 23182	. . . . . . . . 9 $/\$
29	14, 19	rplogcld 23182	. . . . . . . . 9 $/\$
30	28, 29	rpdivcld 11276	. . . . . . . 8 $/\$
31	30	rpred 11259	. . . . . . 7 $/\$
32	30	rpge0d 11263	. . . . . . 7 $/\$
33		flge0nn0 11936	. . . . . . 7 $/\$
34	31, 32, 33	syl2anc 659	. . . . . 6 $/\$
35		hashfz1 12401	. . . . . 6
36	34, 35	syl 16	. . . . 5 $/\$
37	36	oveq1d 6285	. . . 4 $/\$
38	31	flcld 11916	. . . . . 6 $/\$
39	38	zcnd 10966	. . . . 5 $/\$
40	39, 9	mulcomd 9606	. . . 4 $/\$
41	11, 37, 40	3eqtrrd 2500	. . 3 $/\$
42	41	sumeq2dv 13607	. 2
43		chpval2 23691	. 2 ψ
44		simpl 455	. . . . . 6 $/\$
45		0red 9586	. . . . . . 7 $/\$
46		1red 9600	. . . . . . . 8 $/\$
47		0lt1 10071	. . . . . . . . 9
48	47	a1i 11	. . . . . . . 8 $/\$
49		elfzuz2 11694	. . . . . . . . 9
50		eluzle 11094	. . . . . . . . . . 11
51	50	adantl 464	. . . . . . . . . 10 $/\$
52		simpl 455	. . . . . . . . . . 11 $/\$
53		1z 10890	. . . . . . . . . . 11
54		flge 11923	. . . . . . . . . . 11 $/\$
55	52, 53, 54	sylancl 660	. . . . . . . . . 10 $/\$
56	51, 55	mpbird 232	. . . . . . . . 9 $/\$
57	49, 56	sylan2 472	. . . . . . . 8 $/\$
58	45, 46, 44, 48, 57	ltletrd 9731	. . . . . . 7 $/\$
59	45, 44, 58	ltled 9722	. . . . . 6 $/\$
60		elfznn 11717	. . . . . . . 8
61	60	adantl 464	. . . . . . 7 $/\$
62	61	nnrecred 10577	. . . . . 6 $/\$
63	44, 59, 62	recxpcld 23272	. . . . 5 $/\$
64		chtval 23582	. . . . 5
65	63, 64	syl 16	. . . 4 $/\$
66	65	sumeq2dv 13607	. . 3
67		ppifi 23577	. . . 4
68		fzfid 12065	. . . 4
69	2	sseli 3485	. . . . . . . 8
70		elfznn 11717	. . . . . . . 8
71	69, 70	anim12i 564	. . . . . . 7 $/\$ $/\$
72	71	a1i 11	. . . . . 6 $/\$ $/\$
73		0red 9586	. . . . . . . . 9 $/\$
74	2	a1i 11	. . . . . . . . . . . 12
75	74	sselda 3489	. . . . . . . . . . 11 $/\$
76	75, 5	syl 16	. . . . . . . . . 10 $/\$
77	76	nnred 10546	. . . . . . . . 9 $/\$
78	76	nngt0d 10575	. . . . . . . . 9 $/\$
79	73, 77, 12, 78, 26	ltletrd 9731	. . . . . . . 8 $/\$
80	79	ex 432	. . . . . . 7
81	80	adantrd 466	. . . . . 6 $/\$
82	72, 81	jcad 531	. . . . 5 $/\$ $/\$ $/\$
83		inss2 3705	. . . . . . . . 9
84	83	sseli 3485	. . . . . . . 8
85	60, 84	anim12ci 565	. . . . . . 7 $/\$ $/\$
86	85	a1i 11	. . . . . 6 $/\$ $/\$
87	58	ex 432	. . . . . . 7
88	87	adantrd 466	. . . . . 6 $/\$
89	86, 88	jcad 531	. . . . 5 $/\$ $/\$ $/\$
90		elin 3673	. . . . . . . . 9 $/\$
91		simprll 761	. . . . . . . . . . 11 $/\$ $/\$ $/\$
92	91	biantrud 505	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
93		0red 9586	. . . . . . . . . . 11 $/\$ $/\$ $/\$
94		simpl 455	. . . . . . . . . . 11 $/\$ $/\$ $/\$
95	91, 5	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
96	95	nnred 10546	. . . . . . . . . . 11 $/\$ $/\$ $/\$
97	95	nnnn0d 10848	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
98	97	nn0ge0d 10851	. . . . . . . . . . 11 $/\$ $/\$ $/\$
99		df-3an 973	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
100	23, 99	syl6bb 261	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
101	100	baibd 907	. . . . . . . . . . 11 $/\$ $/\$ $/\$
102	93, 94, 96, 98, 101	syl22anc 1227	. . . . . . . . . 10 $/\$ $/\$ $/\$
103	92, 102	bitr3d 255	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
104	90, 103	syl5bb 257	. . . . . . . 8 $/\$ $/\$ $/\$
105		simprr 755	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
106	94, 105	elrpd 11256	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
107	106	relogcld 23176	. . . . . . . . . . 11 $/\$ $/\$ $/\$
108	91, 15	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
109	108, 18	syl 16	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
110	96, 109	rplogcld 23182	. . . . . . . . . . 11 $/\$ $/\$ $/\$
111	107, 110	rerpdivcld 11286	. . . . . . . . . 10 $/\$ $/\$ $/\$
112		simprlr 762	. . . . . . . . . . 11 $/\$ $/\$ $/\$
113	112	nnzd 10964	. . . . . . . . . 10 $/\$ $/\$ $/\$
114		flge 11923	. . . . . . . . . 10 $/\$
115	111, 113, 114	syl2anc 659	. . . . . . . . 9 $/\$ $/\$ $/\$
116	112	nnnn0d 10848	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
117	95, 116	nnexpcld 12313	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
118	117	nnrpd 11257	. . . . . . . . . . 11 $/\$ $/\$ $/\$
119	118, 106	logled 23180	. . . . . . . . . 10 $/\$ $/\$ $/\$
120	95	nnrpd 11257	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
121		relogexp 23149	. . . . . . . . . . . 12 $/\$
122	120, 113, 121	syl2anc 659	. . . . . . . . . . 11 $/\$ $/\$ $/\$
123	122	breq1d 4449	. . . . . . . . . 10 $/\$ $/\$ $/\$
124	112	nnred 10546	. . . . . . . . . . 11 $/\$ $/\$ $/\$
125	124, 107, 110	lemuldivd 11304	. . . . . . . . . 10 $/\$ $/\$ $/\$
126	119, 123, 125	3bitrd 279	. . . . . . . . 9 $/\$ $/\$ $/\$
127		nnuz 11117	. . . . . . . . . . 11
128	112, 127	syl6eleq 2552	. . . . . . . . . 10 $/\$ $/\$ $/\$
129	111	flcld 11916	. . . . . . . . . 10 $/\$ $/\$ $/\$
130		elfz5 11683	. . . . . . . . . 10 $/\$
131	128, 129, 130	syl2anc 659	. . . . . . . . 9 $/\$ $/\$ $/\$
132	115, 126, 131	3bitr4rd 286	. . . . . . . 8 $/\$ $/\$ $/\$
133	104, 132	anbi12d 708	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
134	94	flcld 11916	. . . . . . . . . . 11 $/\$ $/\$ $/\$
135		elfz5 11683	. . . . . . . . . . 11 $/\$
136	128, 134, 135	syl2anc 659	. . . . . . . . . 10 $/\$ $/\$ $/\$
137		flge 11923	. . . . . . . . . . 11 $/\$
138	94, 113, 137	syl2anc 659	. . . . . . . . . 10 $/\$ $/\$ $/\$
139	136, 138	bitr4d 256	. . . . . . . . 9 $/\$ $/\$ $/\$
140		elin 3673	. . . . . . . . . 10 $/\$
141	91	biantrud 505	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
142	106	rpge0d 11263	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
143	112	nnrecred 10577	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
144	94, 142, 143	recxpcld 23272	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
145		elicc2 11592	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
146		df-3an 973	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
147	145, 146	syl6bb 261	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
148	147	baibd 907	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
149	93, 144, 96, 98, 148	syl22anc 1227	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
150	141, 149	bitr3d 255	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
151	94, 142, 143	cxpge0d 23273	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152	112	nnrpd 11257	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
153	96, 98, 144, 151, 152	cxple2d 23276	. . . . . . . . . . 11 $/\$ $/\$ $/\$
154	95	nncnd 10547	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
155		cxpexp 23217	. . . . . . . . . . . . 13 $/\$
156	154, 116, 155	syl2anc 659	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
157	112	nncnd 10547	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
158	112	nnne0d 10576	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
159	157, 158	recid2d 10312	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
160	159	oveq2d 6286	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
161	106, 143, 157	cxpmuld 23283	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
162	94	recnd 9611	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
163	162	cxp1d 23255	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
164	160, 161, 163	3eqtr3d 2503	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
165	156, 164	breq12d 4452	. . . . . . . . . . 11 $/\$ $/\$ $/\$
166	150, 153, 165	3bitrd 279	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
167	140, 166	syl5bb 257	. . . . . . . . 9 $/\$ $/\$ $/\$
168	139, 167	anbi12d 708	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
169	117	nnred 10546	. . . . . . . . . . 11 $/\$ $/\$ $/\$
170		bernneq3 12276	. . . . . . . . . . . 12 $/\$
171	108, 116, 170	syl2anc 659	. . . . . . . . . . 11 $/\$ $/\$ $/\$
172	124, 169, 171	ltled 9722	. . . . . . . . . 10 $/\$ $/\$ $/\$
173		letr 9667	. . . . . . . . . . 11 $/\$ $/\$ $/\$
174	124, 169, 94, 173	syl3anc 1226	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
175	172, 174	mpand 673	. . . . . . . . 9 $/\$ $/\$ $/\$
176	175	pm4.71rd 633	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
177	154	exp1d 12287	. . . . . . . . . . 11 $/\$ $/\$ $/\$
178	95	nnge1d 10574	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
179	96, 178, 128	leexp2ad 12324	. . . . . . . . . . 11 $/\$ $/\$ $/\$
180	177, 179	eqbrtrrd 4461	. . . . . . . . . 10 $/\$ $/\$ $/\$
181		letr 9667	. . . . . . . . . . 11 $/\$ $/\$ $/\$
182	96, 169, 94, 181	syl3anc 1226	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
183	180, 182	mpand 673	. . . . . . . . 9 $/\$ $/\$ $/\$
184	183	pm4.71rd 633	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
185	168, 176, 184	3bitr2rd 282	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
186	133, 185	bitrd 253	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
187	186	ex 432	. . . . 5 $/\$ $/\$ $/\$ $/\$
188	82, 89, 187	pm5.21ndd 352	. . . 4 $/\$ $/\$
189	9	adantrr 714	. . . 4 $/\$ $/\$
190	67, 68, 1, 188, 189	fsumcom2 13671	. . 3
191	66, 190	eqtr4d 2498	. 2
192	42, 43, 191	3eqtr4d 2505	1 ψ

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 971

wceq 1398

wcel 1823

cin 3460

wss 3461 class class class wbr 4439

cfv 5570 (class class class)co 6270

cfn 7509

cc 9479

cr 9480

cc0 9481

c1 9482

cmul 9486

clt 9617

cle 9618

cdiv 10202

cn 10531

c2 10581

cn0 10791

cz 10860

cuz 11082

crp 11221

cicc 11535

cfz 11675

cfl 11908

cexp 12148

chash 12387

csu 13590

cprime 14301

clog 23108

ccxp 23109

ccht 23562 ψcchp 23564

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1623 ax-4 1636 ax-5 1709 ax-6 1752 ax-7 1795 ax-8 1825 ax-9 1827 ax-10 1842 ax-11 1847 ax-12 1859 ax-13 2004 ax-ext 2432 ax-rep 4550 ax-sep 4560 ax-nul 4568 ax-pow 4615 ax-pr 4676 ax-un 6565 ax-inf2 8049 ax-cnex 9537 ax-resscn 9538 ax-1cn 9539 ax-icn 9540 ax-addcl 9541 ax-addrcl 9542 ax-mulcl 9543 ax-mulrcl 9544 ax-mulcom 9545 ax-addass 9546 ax-mulass 9547 ax-distr 9548 ax-i2m1 9549 ax-1ne0 9550 ax-1rid 9551 ax-rnegex 9552 ax-rrecex 9553 ax-cnre 9554 ax-pre-lttri 9555 ax-pre-lttrn 9556 ax-pre-ltadd 9557 ax-pre-mulgt0 9558 ax-pre-sup 9559 ax-addf 9560 ax-mulf 9561

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1401 df-fal 1404 df-ex 1618 df-nf 1622 df-sb 1745 df-eu 2288 df-mo 2289 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2651 df-nel 2652 df-ral 2809 df-rex 2810 df-reu 2811 df-rmo 2812 df-rab 2813 df-v 3108 df-sbc 3325 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3784 df-if 3930 df-pw 4001 df-sn 4017 df-pr 4019 df-tp 4021 df-op 4023 df-uni 4236 df-int 4272 df-iun 4317 df-iin 4318 df-br 4440 df-opab 4498 df-mpt 4499 df-tr 4533 df-eprel 4780 df-id 4784 df-po 4789 df-so 4790 df-fr 4827 df-se 4828 df-we 4829 df-ord 4870 df-on 4871 df-lim 4872 df-suc 4873 df-xp 4994 df-rel 4995 df-cnv 4996 df-co 4997 df-dm 4998 df-rn 4999 df-res 5000 df-ima 5001 df-iota 5534 df-fun 5572 df-fn 5573 df-f 5574 df-f1 5575 df-fo 5576 df-f1o 5577 df-fv 5578 df-isom 5579 df-riota 6232 df-ov 6273 df-oprab 6274 df-mpt2 6275 df-of 6513 df-om 6674 df-1st 6773 df-2nd 6774 df-supp 6892 df-recs 7034 df-rdg 7068 df-1o 7122 df-2o 7123 df-oadd 7126 df-er 7303 df-map 7414 df-pm 7415 df-ixp 7463 df-en 7510 df-dom 7511 df-sdom 7512 df-fin 7513 df-fsupp 7822 df-fi 7863 df-sup 7893 df-oi 7927 df-card 8311 df-cda 8539 df-pnf 9619 df-mnf 9620 df-xr 9621 df-ltxr 9622 df-le 9623 df-sub 9798 df-neg 9799 df-div 10203 df-nn 10532 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 10977 df-uz 11083 df-q 11184 df-rp 11222 df-xneg 11321 df-xadd 11322 df-xmul 11323 df-ioo 11536 df-ioc 11537 df-ico 11538 df-icc 11539 df-fz 11676 df-fzo 11800 df-fl 11910 df-mod 11979 df-seq 12090 df-exp 12149 df-fac 12336 df-bc 12363 df-hash 12388 df-shft 12982 df-cj 13014 df-re 13015 df-im 13016 df-sqrt 13150 df-abs 13151 df-limsup 13376 df-clim 13393 df-rlim 13394 df-sum 13591 df-ef 13885 df-sin 13887 df-cos 13888 df-pi 13890 df-dvds 14071 df-gcd 14229 df-prm 14302 df-pc 14445 df-struct 14718 df-ndx 14719 df-slot 14720 df-base 14721 df-sets 14722 df-ress 14723 df-plusg 14797 df-mulr 14798 df-starv 14799 df-sca 14800 df-vsca 14801 df-ip 14802 df-tset 14803 df-ple 14804 df-ds 14806 df-unif 14807 df-hom 14808 df-cco 14809 df-rest 14912 df-topn 14913 df-0g 14931 df-gsum 14932 df-topgen 14933 df-pt 14934 df-prds 14937 df-xrs 14991 df-qtop 14996 df-imas 14997 df-xps 14999 df-mre 15075 df-mrc 15076 df-acs 15078 df-mgm 16071 df-sgrp 16110 df-mnd 16120 df-submnd 16166 df-mulg 16259 df-cntz 16554 df-cmn 16999 df-psmet 18606 df-xmet 18607 df-met 18608 df-bl 18609 df-mopn 18610 df-fbas 18611 df-fg 18612 df-cnfld 18616 df-top 19566 df-bases 19568 df-topon 19569 df-topsp 19570 df-cld 19687 df-ntr 19688 df-cls 19689 df-nei 19766 df-lp 19804 df-perf 19805 df-cn 19895 df-cnp 19896 df-haus 19983 df-tx 20229 df-hmeo 20422 df-fil 20513 df-fm 20605 df-flim 20606 df-flf 20607 df-xms 20989 df-ms 20990 df-tms 20991 df-cncf 21548 df-limc 22436 df-dv 22437 df-log 23110 df-cxp 23111 df-cht 23568 df-vma 23569 df-chp 23570

This theorem is referenced by: (None)

W3C validator