chpchtsum - Metamath Proof Explorer

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

Theorem chpchtsum 24007

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 12172	. . . . 5 $/\$
2		inss2 3680	. . . . . . . . . 10
3		simpr 462	. . . . . . . . . 10 $/\$
4	2, 3	sseldi 3459	. . . . . . . . 9 $/\$
5		prmnn 14585	. . . . . . . . 9
6	4, 5	syl 17	. . . . . . . 8 $/\$
7	6	nnrpd 11328	. . . . . . 7 $/\$
8	7	relogcld 23434	. . . . . 6 $/\$
9	8	recnd 9658	. . . . 5 $/\$
10		fsumconst 13818	. . . . 5 $/\$
11	1, 9, 10	syl2anc 665	. . . 4 $/\$
12		simpl 458	. . . . . . . . . 10 $/\$
13		1red 9647	. . . . . . . . . . 11 $/\$
14	6	nnred 10613	. . . . . . . . . . 11 $/\$
15		prmuz2 14602	. . . . . . . . . . . . 13
16	4, 15	syl 17	. . . . . . . . . . . 12 $/\$
17		eluz2b2 11220	. . . . . . . . . . . . 13 $/\$
18	17	simprbi 465	. . . . . . . . . . . 12
19	16, 18	syl 17	. . . . . . . . . . 11 $/\$
20		inss1 3679	. . . . . . . . . . . . . 14
21	20, 3	sseldi 3459	. . . . . . . . . . . . 13 $/\$
22		0re 9632	. . . . . . . . . . . . . 14
23		elicc2 11688	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
24	22, 12, 23	sylancr 667	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
25	21, 24	mpbid 213	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
26	25	simp3d 1019	. . . . . . . . . . 11 $/\$
27	13, 14, 12, 19, 26	ltletrd 9784	. . . . . . . . . 10 $/\$
28	12, 27	rplogcld 23440	. . . . . . . . 9 $/\$
29	14, 19	rplogcld 23440	. . . . . . . . 9 $/\$
30	28, 29	rpdivcld 11347	. . . . . . . 8 $/\$
31	30	rpred 11330	. . . . . . 7 $/\$
32	30	rpge0d 11334	. . . . . . 7 $/\$
33		flge0nn0 12040	. . . . . . 7 $/\$
34	31, 32, 33	syl2anc 665	. . . . . 6 $/\$
35		hashfz1 12515	. . . . . 6
36	34, 35	syl 17	. . . . 5 $/\$
37	36	oveq1d 6311	. . . 4 $/\$
38	31	flcld 12020	. . . . . 6 $/\$
39	38	zcnd 11030	. . . . 5 $/\$
40	39, 9	mulcomd 9653	. . . 4 $/\$
41	11, 37, 40	3eqtrrd 2466	. . 3 $/\$
42	41	sumeq2dv 13736	. 2
43		chpval2 24006	. 2 ψ
44		simpl 458	. . . . . 6 $/\$
45		0red 9633	. . . . . . 7 $/\$
46		1red 9647	. . . . . . . 8 $/\$
47		0lt1 10125	. . . . . . . . 9
48	47	a1i 11	. . . . . . . 8 $/\$
49		elfzuz2 11791	. . . . . . . . 9
50		eluzle 11160	. . . . . . . . . . 11
51	50	adantl 467	. . . . . . . . . 10 $/\$
52		simpl 458	. . . . . . . . . . 11 $/\$
53		1z 10956	. . . . . . . . . . 11
54		flge 12027	. . . . . . . . . . 11 $/\$
55	52, 53, 54	sylancl 666	. . . . . . . . . 10 $/\$
56	51, 55	mpbird 235	. . . . . . . . 9 $/\$
57	49, 56	sylan2 476	. . . . . . . 8 $/\$
58	45, 46, 44, 48, 57	ltletrd 9784	. . . . . . 7 $/\$
59	45, 44, 58	ltled 9772	. . . . . 6 $/\$
60		elfznn 11815	. . . . . . . 8
61	60	adantl 467	. . . . . . 7 $/\$
62	61	nnrecred 10644	. . . . . 6 $/\$
63	44, 59, 62	recxpcld 23530	. . . . 5 $/\$
64		chtval 23897	. . . . 5
65	63, 64	syl 17	. . . 4 $/\$
66	65	sumeq2dv 13736	. . 3
67		ppifi 23892	. . . 4
68		fzfid 12172	. . . 4
69	2	sseli 3457	. . . . . . . 8
70		elfznn 11815	. . . . . . . 8
71	69, 70	anim12i 568	. . . . . . 7 $/\$ $/\$
72	71	a1i 11	. . . . . 6 $/\$ $/\$
73		0red 9633	. . . . . . . . 9 $/\$
74	2	a1i 11	. . . . . . . . . . . 12
75	74	sselda 3461	. . . . . . . . . . 11 $/\$
76	75, 5	syl 17	. . . . . . . . . 10 $/\$
77	76	nnred 10613	. . . . . . . . 9 $/\$
78	76	nngt0d 10642	. . . . . . . . 9 $/\$
79	73, 77, 12, 78, 26	ltletrd 9784	. . . . . . . 8 $/\$
80	79	ex 435	. . . . . . 7
81	80	adantrd 469	. . . . . 6 $/\$
82	72, 81	jcad 535	. . . . 5 $/\$ $/\$ $/\$
83		inss2 3680	. . . . . . . . 9
84	83	sseli 3457	. . . . . . . 8
85	60, 84	anim12ci 569	. . . . . . 7 $/\$ $/\$
86	85	a1i 11	. . . . . 6 $/\$ $/\$
87	58	ex 435	. . . . . . 7
88	87	adantrd 469	. . . . . 6 $/\$
89	86, 88	jcad 535	. . . . 5 $/\$ $/\$ $/\$
90		elin 3646	. . . . . . . . 9 $/\$
91		simprll 770	. . . . . . . . . . 11 $/\$ $/\$ $/\$
92	91	biantrud 509	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
93		0red 9633	. . . . . . . . . . 11 $/\$ $/\$ $/\$
94		simpl 458	. . . . . . . . . . 11 $/\$ $/\$ $/\$
95	91, 5	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
96	95	nnred 10613	. . . . . . . . . . 11 $/\$ $/\$ $/\$
97	95	nnnn0d 10914	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
98	97	nn0ge0d 10917	. . . . . . . . . . 11 $/\$ $/\$ $/\$
99		df-3an 984	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
100	23, 99	syl6bb 264	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
101	100	baibd 917	. . . . . . . . . . 11 $/\$ $/\$ $/\$
102	93, 94, 96, 98, 101	syl22anc 1265	. . . . . . . . . 10 $/\$ $/\$ $/\$
103	92, 102	bitr3d 258	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
104	90, 103	syl5bb 260	. . . . . . . 8 $/\$ $/\$ $/\$
105		simprr 764	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
106	94, 105	elrpd 11327	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
107	106	relogcld 23434	. . . . . . . . . . 11 $/\$ $/\$ $/\$
108	91, 15	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
109	108, 18	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
110	96, 109	rplogcld 23440	. . . . . . . . . . 11 $/\$ $/\$ $/\$
111	107, 110	rerpdivcld 11358	. . . . . . . . . 10 $/\$ $/\$ $/\$
112		simprlr 771	. . . . . . . . . . 11 $/\$ $/\$ $/\$
113	112	nnzd 11028	. . . . . . . . . 10 $/\$ $/\$ $/\$
114		flge 12027	. . . . . . . . . 10 $/\$
115	111, 113, 114	syl2anc 665	. . . . . . . . 9 $/\$ $/\$ $/\$
116	112	nnnn0d 10914	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
117	95, 116	nnexpcld 12423	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
118	117	nnrpd 11328	. . . . . . . . . . 11 $/\$ $/\$ $/\$
119	118, 106	logled 23438	. . . . . . . . . 10 $/\$ $/\$ $/\$
120	95	nnrpd 11328	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
121		relogexp 23407	. . . . . . . . . . . 12 $/\$
122	120, 113, 121	syl2anc 665	. . . . . . . . . . 11 $/\$ $/\$ $/\$
123	122	breq1d 4427	. . . . . . . . . 10 $/\$ $/\$ $/\$
124	112	nnred 10613	. . . . . . . . . . 11 $/\$ $/\$ $/\$
125	124, 107, 110	lemuldivd 11376	. . . . . . . . . 10 $/\$ $/\$ $/\$
126	119, 123, 125	3bitrd 282	. . . . . . . . 9 $/\$ $/\$ $/\$
127		nnuz 11183	. . . . . . . . . . 11
128	112, 127	syl6eleq 2518	. . . . . . . . . 10 $/\$ $/\$ $/\$
129	111	flcld 12020	. . . . . . . . . 10 $/\$ $/\$ $/\$
130		elfz5 11779	. . . . . . . . . 10 $/\$
131	128, 129, 130	syl2anc 665	. . . . . . . . 9 $/\$ $/\$ $/\$
132	115, 126, 131	3bitr4rd 289	. . . . . . . 8 $/\$ $/\$ $/\$
133	104, 132	anbi12d 715	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
134	94	flcld 12020	. . . . . . . . . . 11 $/\$ $/\$ $/\$
135		elfz5 11779	. . . . . . . . . . 11 $/\$
136	128, 134, 135	syl2anc 665	. . . . . . . . . 10 $/\$ $/\$ $/\$
137		flge 12027	. . . . . . . . . . 11 $/\$
138	94, 113, 137	syl2anc 665	. . . . . . . . . 10 $/\$ $/\$ $/\$
139	136, 138	bitr4d 259	. . . . . . . . 9 $/\$ $/\$ $/\$
140		elin 3646	. . . . . . . . . 10 $/\$
141	91	biantrud 509	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
142	106	rpge0d 11334	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
143	112	nnrecred 10644	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
144	94, 142, 143	recxpcld 23530	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
145		elicc2 11688	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
146		df-3an 984	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
147	145, 146	syl6bb 264	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
148	147	baibd 917	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
149	93, 144, 96, 98, 148	syl22anc 1265	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
150	141, 149	bitr3d 258	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
151	94, 142, 143	cxpge0d 23531	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152	112	nnrpd 11328	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
153	96, 98, 144, 151, 152	cxple2d 23534	. . . . . . . . . . 11 $/\$ $/\$ $/\$
154	95	nncnd 10614	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
155		cxpexp 23475	. . . . . . . . . . . . 13 $/\$
156	154, 116, 155	syl2anc 665	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
157	112	nncnd 10614	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
158	112	nnne0d 10643	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
159	157, 158	recid2d 10368	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
160	159	oveq2d 6312	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
161	106, 143, 157	cxpmuld 23541	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
162	94	recnd 9658	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
163	162	cxp1d 23513	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
164	160, 161, 163	3eqtr3d 2469	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
165	156, 164	breq12d 4430	. . . . . . . . . . 11 $/\$ $/\$ $/\$
166	150, 153, 165	3bitrd 282	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
167	140, 166	syl5bb 260	. . . . . . . . 9 $/\$ $/\$ $/\$
168	139, 167	anbi12d 715	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
169	117	nnred 10613	. . . . . . . . . . 11 $/\$ $/\$ $/\$
170		bernneq3 12386	. . . . . . . . . . . 12 $/\$
171	108, 116, 170	syl2anc 665	. . . . . . . . . . 11 $/\$ $/\$ $/\$
172	124, 169, 171	ltled 9772	. . . . . . . . . 10 $/\$ $/\$ $/\$
173		letr 9716	. . . . . . . . . . 11 $/\$ $/\$ $/\$
174	124, 169, 94, 173	syl3anc 1264	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
175	172, 174	mpand 679	. . . . . . . . 9 $/\$ $/\$ $/\$
176	175	pm4.71rd 639	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
177	154	exp1d 12397	. . . . . . . . . . 11 $/\$ $/\$ $/\$
178	95	nnge1d 10641	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
179	96, 178, 128	leexp2ad 12434	. . . . . . . . . . 11 $/\$ $/\$ $/\$
180	177, 179	eqbrtrrd 4439	. . . . . . . . . 10 $/\$ $/\$ $/\$
181		letr 9716	. . . . . . . . . . 11 $/\$ $/\$ $/\$
182	96, 169, 94, 181	syl3anc 1264	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
183	180, 182	mpand 679	. . . . . . . . 9 $/\$ $/\$ $/\$
184	183	pm4.71rd 639	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
185	168, 176, 184	3bitr2rd 285	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
186	133, 185	bitrd 256	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
187	186	ex 435	. . . . 5 $/\$ $/\$ $/\$ $/\$
188	82, 89, 187	pm5.21ndd 355	. . . 4 $/\$ $/\$
189	9	adantrr 721	. . . 4 $/\$ $/\$
190	67, 68, 1, 188, 189	fsumcom2 13802	. . 3
191	66, 190	eqtr4d 2464	. 2
192	42, 43, 191	3eqtr4d 2471	1 ψ

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 187 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wcel 1867

cin 3432

wss 3433 class class class wbr 4417

cfv 5592 (class class class)co 6296

cfn 7568

cc 9526

cr 9527

cc0 9528

c1 9529

cmul 9533

clt 9664

cle 9665

cdiv 10258

cn 10598

c2 10648

cn0 10858

cz 10926

cuz 11148

crp 11291

cicc 11627

cfz 11771

cfl 12012

cexp 12258

chash 12501

csu 13719

cprime 14582

clog 23366

ccxp 23367

ccht 23877 ψcchp 23879

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1838 ax-8 1869 ax-9 1871 ax-10 1886 ax-11 1891 ax-12 1904 ax-13 2052 ax-ext 2398 ax-rep 4529 ax-sep 4539 ax-nul 4547 ax-pow 4594 ax-pr 4652 ax-un 6588 ax-inf2 8137 ax-cnex 9584 ax-resscn 9585 ax-1cn 9586 ax-icn 9587 ax-addcl 9588 ax-addrcl 9589 ax-mulcl 9590 ax-mulrcl 9591 ax-mulcom 9592 ax-addass 9593 ax-mulass 9594 ax-distr 9595 ax-i2m1 9596 ax-1ne0 9597 ax-1rid 9598 ax-rnegex 9599 ax-rrecex 9600 ax-cnre 9601 ax-pre-lttri 9602 ax-pre-lttrn 9603 ax-pre-ltadd 9604 ax-pre-mulgt0 9605 ax-pre-sup 9606 ax-addf 9607 ax-mulf 9608

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-fal 1443 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2267 df-mo 2268 df-clab 2406 df-cleq 2412 df-clel 2415 df-nfc 2570 df-ne 2618 df-nel 2619 df-ral 2778 df-rex 2779 df-reu 2780 df-rmo 2781 df-rab 2782 df-v 3080 df-sbc 3297 df-csb 3393 df-dif 3436 df-un 3438 df-in 3440 df-ss 3447 df-pss 3449 df-nul 3759 df-if 3907 df-pw 3978 df-sn 3994 df-pr 3996 df-tp 3998 df-op 4000 df-uni 4214 df-int 4250 df-iun 4295 df-iin 4296 df-br 4418 df-opab 4476 df-mpt 4477 df-tr 4512 df-eprel 4756 df-id 4760 df-po 4766 df-so 4767 df-fr 4804 df-se 4805 df-we 4806 df-xp 4851 df-rel 4852 df-cnv 4853 df-co 4854 df-dm 4855 df-rn 4856 df-res 4857 df-ima 4858 df-pred 5390 df-ord 5436 df-on 5437 df-lim 5438 df-suc 5439 df-iota 5556 df-fun 5594 df-fn 5595 df-f 5596 df-f1 5597 df-fo 5598 df-f1o 5599 df-fv 5600 df-isom 5601 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-of 6536 df-om 6698 df-1st 6798 df-2nd 6799 df-supp 6917 df-wrecs 7027 df-recs 7089 df-rdg 7127 df-1o 7181 df-2o 7182 df-oadd 7185 df-er 7362 df-map 7473 df-pm 7474 df-ixp 7522 df-en 7569 df-dom 7570 df-sdom 7571 df-fin 7572 df-fsupp 7881 df-fi 7922 df-sup 7953 df-inf 7954 df-oi 8016 df-card 8363 df-cda 8587 df-pnf 9666 df-mnf 9667 df-xr 9668 df-ltxr 9669 df-le 9670 df-sub 9851 df-neg 9852 df-div 10259 df-nn 10599 df-2 10657 df-3 10658 df-4 10659 df-5 10660 df-6 10661 df-7 10662 df-8 10663 df-9 10664 df-10 10665 df-n0 10859 df-z 10927 df-dec 11041 df-uz 11149 df-q 11254 df-rp 11292 df-xneg 11398 df-xadd 11399 df-xmul 11400 df-ioo 11628 df-ioc 11629 df-ico 11630 df-icc 11631 df-fz 11772 df-fzo 11903 df-fl 12014 df-mod 12083 df-seq 12200 df-exp 12259 df-fac 12446 df-bc 12474 df-hash 12502 df-shft 13098 df-cj 13130 df-re 13131 df-im 13132 df-sqrt 13266 df-abs 13267 df-limsup 13493 df-clim 13519 df-rlim 13520 df-sum 13720 df-ef 14088 df-sin 14090 df-cos 14091 df-pi 14093 df-dvds 14273 df-gcd 14432 df-prm 14583 df-pc 14739 df-struct 15075 df-ndx 15076 df-slot 15077 df-base 15078 df-sets 15079 df-ress 15080 df-plusg 15155 df-mulr 15156 df-starv 15157 df-sca 15158 df-vsca 15159 df-ip 15160 df-tset 15161 df-ple 15162 df-ds 15164 df-unif 15165 df-hom 15166 df-cco 15167 df-rest 15273 df-topn 15274 df-0g 15292 df-gsum 15293 df-topgen 15294 df-pt 15295 df-prds 15298 df-xrs 15352 df-qtop 15357 df-imas 15358 df-xps 15360 df-mre 15436 df-mrc 15437 df-acs 15439 df-mgm 16432 df-sgrp 16471 df-mnd 16481 df-submnd 16527 df-mulg 16620 df-cntz 16915 df-cmn 17360 df-psmet 18890 df-xmet 18891 df-met 18892 df-bl 18893 df-mopn 18894 df-fbas 18895 df-fg 18896 df-cnfld 18899 df-top 19845 df-bases 19846 df-topon 19847 df-topsp 19848 df-cld 19958 df-ntr 19959 df-cls 19960 df-nei 20038 df-lp 20076 df-perf 20077 df-cn 20167 df-cnp 20168 df-haus 20255 df-tx 20501 df-hmeo 20694 df-fil 20785 df-fm 20877 df-flim 20878 df-flf 20879 df-xms 21259 df-ms 21260 df-tms 21261 df-cncf 21799 df-limc 22695 df-dv 22696 df-log 23368 df-cxp 23369 df-cht 23883 df-vma 23884 df-chp 23885

This theorem is referenced by: (None)

W3C validator