chpchtsum - Metamath Proof Explorer

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

Theorem chpchtsum 24226

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 12224	. . . . 5 $/\$
2		inss2 3644	. . . . . . . . . 10
3		simpr 468	. . . . . . . . . 10 $/\$
4	2, 3	sseldi 3416	. . . . . . . . 9 $/\$
5		prmnn 14704	. . . . . . . . 9
6	4, 5	syl 17	. . . . . . . 8 $/\$
7	6	nnrpd 11362	. . . . . . 7 $/\$
8	7	relogcld 23651	. . . . . 6 $/\$
9	8	recnd 9687	. . . . 5 $/\$
10		fsumconst 13928	. . . . 5 $/\$
11	1, 9, 10	syl2anc 673	. . . 4 $/\$
12		simpl 464	. . . . . . . . . 10 $/\$
13		1red 9676	. . . . . . . . . . 11 $/\$
14	6	nnred 10646	. . . . . . . . . . 11 $/\$
15		prmuz2 14721	. . . . . . . . . . . . 13
16	4, 15	syl 17	. . . . . . . . . . . 12 $/\$
17		eluz2b2 11254	. . . . . . . . . . . . 13 $/\$
18	17	simprbi 471	. . . . . . . . . . . 12
19	16, 18	syl 17	. . . . . . . . . . 11 $/\$
20		inss1 3643	. . . . . . . . . . . . . 14
21	20, 3	sseldi 3416	. . . . . . . . . . . . 13 $/\$
22		0re 9661	. . . . . . . . . . . . . 14
23		elicc2 11724	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
24	22, 12, 23	sylancr 676	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
25	21, 24	mpbid 215	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
26	25	simp3d 1044	. . . . . . . . . . 11 $/\$
27	13, 14, 12, 19, 26	ltletrd 9812	. . . . . . . . . 10 $/\$
28	12, 27	rplogcld 23657	. . . . . . . . 9 $/\$
29	14, 19	rplogcld 23657	. . . . . . . . 9 $/\$
30	28, 29	rpdivcld 11381	. . . . . . . 8 $/\$
31	30	rpred 11364	. . . . . . 7 $/\$
32	30	rpge0d 11368	. . . . . . 7 $/\$
33		flge0nn0 12087	. . . . . . 7 $/\$
34	31, 32, 33	syl2anc 673	. . . . . 6 $/\$
35		hashfz1 12567	. . . . . 6
36	34, 35	syl 17	. . . . 5 $/\$
37	36	oveq1d 6323	. . . 4 $/\$
38	31	flcld 12067	. . . . . 6 $/\$
39	38	zcnd 11064	. . . . 5 $/\$
40	39, 9	mulcomd 9682	. . . 4 $/\$
41	11, 37, 40	3eqtrrd 2510	. . 3 $/\$
42	41	sumeq2dv 13846	. 2
43		chpval2 24225	. 2 ψ
44		simpl 464	. . . . . 6 $/\$
45		0red 9662	. . . . . . 7 $/\$
46		1red 9676	. . . . . . . 8 $/\$
47		0lt1 10157	. . . . . . . . 9
48	47	a1i 11	. . . . . . . 8 $/\$
49		elfzuz2 11830	. . . . . . . . 9
50		eluzle 11195	. . . . . . . . . . 11
51	50	adantl 473	. . . . . . . . . 10 $/\$
52		simpl 464	. . . . . . . . . . 11 $/\$
53		1z 10991	. . . . . . . . . . 11
54		flge 12074	. . . . . . . . . . 11 $/\$
55	52, 53, 54	sylancl 675	. . . . . . . . . 10 $/\$
56	51, 55	mpbird 240	. . . . . . . . 9 $/\$
57	49, 56	sylan2 482	. . . . . . . 8 $/\$
58	45, 46, 44, 48, 57	ltletrd 9812	. . . . . . 7 $/\$
59	45, 44, 58	ltled 9800	. . . . . 6 $/\$
60		elfznn 11854	. . . . . . . 8
61	60	adantl 473	. . . . . . 7 $/\$
62	61	nnrecred 10677	. . . . . 6 $/\$
63	44, 59, 62	recxpcld 23747	. . . . 5 $/\$
64		chtval 24116	. . . . 5
65	63, 64	syl 17	. . . 4 $/\$
66	65	sumeq2dv 13846	. . 3
67		ppifi 24111	. . . 4
68		fzfid 12224	. . . 4
69	2	sseli 3414	. . . . . . . 8
70		elfznn 11854	. . . . . . . 8
71	69, 70	anim12i 576	. . . . . . 7 $/\$ $/\$
72	71	a1i 11	. . . . . 6 $/\$ $/\$
73		0red 9662	. . . . . . . . 9 $/\$
74	2	a1i 11	. . . . . . . . . . . 12
75	74	sselda 3418	. . . . . . . . . . 11 $/\$
76	75, 5	syl 17	. . . . . . . . . 10 $/\$
77	76	nnred 10646	. . . . . . . . 9 $/\$
78	76	nngt0d 10675	. . . . . . . . 9 $/\$
79	73, 77, 12, 78, 26	ltletrd 9812	. . . . . . . 8 $/\$
80	79	ex 441	. . . . . . 7
81	80	adantrd 475	. . . . . 6 $/\$
82	72, 81	jcad 542	. . . . 5 $/\$ $/\$ $/\$
83		inss2 3644	. . . . . . . . 9
84	83	sseli 3414	. . . . . . . 8
85	60, 84	anim12ci 577	. . . . . . 7 $/\$ $/\$
86	85	a1i 11	. . . . . 6 $/\$ $/\$
87	58	ex 441	. . . . . . 7
88	87	adantrd 475	. . . . . 6 $/\$
89	86, 88	jcad 542	. . . . 5 $/\$ $/\$ $/\$
90		elin 3608	. . . . . . . . 9 $/\$
91		simprll 780	. . . . . . . . . . 11 $/\$ $/\$ $/\$
92	91	biantrud 515	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
93		0red 9662	. . . . . . . . . . 11 $/\$ $/\$ $/\$
94		simpl 464	. . . . . . . . . . 11 $/\$ $/\$ $/\$
95	91, 5	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
96	95	nnred 10646	. . . . . . . . . . 11 $/\$ $/\$ $/\$
97	95	nnnn0d 10949	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
98	97	nn0ge0d 10952	. . . . . . . . . . 11 $/\$ $/\$ $/\$
99		df-3an 1009	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
100	23, 99	syl6bb 269	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
101	100	baibd 923	. . . . . . . . . . 11 $/\$ $/\$ $/\$
102	93, 94, 96, 98, 101	syl22anc 1293	. . . . . . . . . 10 $/\$ $/\$ $/\$
103	92, 102	bitr3d 263	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
104	90, 103	syl5bb 265	. . . . . . . 8 $/\$ $/\$ $/\$
105		simprr 774	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
106	94, 105	elrpd 11361	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
107	106	relogcld 23651	. . . . . . . . . . 11 $/\$ $/\$ $/\$
108	91, 15	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
109	108, 18	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
110	96, 109	rplogcld 23657	. . . . . . . . . . 11 $/\$ $/\$ $/\$
111	107, 110	rerpdivcld 11392	. . . . . . . . . 10 $/\$ $/\$ $/\$
112		simprlr 781	. . . . . . . . . . 11 $/\$ $/\$ $/\$
113	112	nnzd 11062	. . . . . . . . . 10 $/\$ $/\$ $/\$
114		flge 12074	. . . . . . . . . 10 $/\$
115	111, 113, 114	syl2anc 673	. . . . . . . . 9 $/\$ $/\$ $/\$
116	112	nnnn0d 10949	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
117	95, 116	nnexpcld 12475	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
118	117	nnrpd 11362	. . . . . . . . . . 11 $/\$ $/\$ $/\$
119	118, 106	logled 23655	. . . . . . . . . 10 $/\$ $/\$ $/\$
120	95	nnrpd 11362	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
121		relogexp 23624	. . . . . . . . . . . 12 $/\$
122	120, 113, 121	syl2anc 673	. . . . . . . . . . 11 $/\$ $/\$ $/\$
123	122	breq1d 4405	. . . . . . . . . 10 $/\$ $/\$ $/\$
124	112	nnred 10646	. . . . . . . . . . 11 $/\$ $/\$ $/\$
125	124, 107, 110	lemuldivd 11410	. . . . . . . . . 10 $/\$ $/\$ $/\$
126	119, 123, 125	3bitrd 287	. . . . . . . . 9 $/\$ $/\$ $/\$
127		nnuz 11218	. . . . . . . . . . 11
128	112, 127	syl6eleq 2559	. . . . . . . . . 10 $/\$ $/\$ $/\$
129	111	flcld 12067	. . . . . . . . . 10 $/\$ $/\$ $/\$
130		elfz5 11818	. . . . . . . . . 10 $/\$
131	128, 129, 130	syl2anc 673	. . . . . . . . 9 $/\$ $/\$ $/\$
132	115, 126, 131	3bitr4rd 294	. . . . . . . 8 $/\$ $/\$ $/\$
133	104, 132	anbi12d 725	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
134	94	flcld 12067	. . . . . . . . . . 11 $/\$ $/\$ $/\$
135		elfz5 11818	. . . . . . . . . . 11 $/\$
136	128, 134, 135	syl2anc 673	. . . . . . . . . 10 $/\$ $/\$ $/\$
137		flge 12074	. . . . . . . . . . 11 $/\$
138	94, 113, 137	syl2anc 673	. . . . . . . . . 10 $/\$ $/\$ $/\$
139	136, 138	bitr4d 264	. . . . . . . . 9 $/\$ $/\$ $/\$
140		elin 3608	. . . . . . . . . 10 $/\$
141	91	biantrud 515	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
142	106	rpge0d 11368	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
143	112	nnrecred 10677	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
144	94, 142, 143	recxpcld 23747	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
145		elicc2 11724	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
146		df-3an 1009	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
147	145, 146	syl6bb 269	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
148	147	baibd 923	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
149	93, 144, 96, 98, 148	syl22anc 1293	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
150	141, 149	bitr3d 263	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
151	94, 142, 143	cxpge0d 23748	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152	112	nnrpd 11362	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
153	96, 98, 144, 151, 152	cxple2d 23751	. . . . . . . . . . 11 $/\$ $/\$ $/\$
154	95	nncnd 10647	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
155		cxpexp 23692	. . . . . . . . . . . . 13 $/\$
156	154, 116, 155	syl2anc 673	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
157	112	nncnd 10647	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
158	112	nnne0d 10676	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
159	157, 158	recid2d 10401	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
160	159	oveq2d 6324	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
161	106, 143, 157	cxpmuld 23758	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
162	94	recnd 9687	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
163	162	cxp1d 23730	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
164	160, 161, 163	3eqtr3d 2513	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
165	156, 164	breq12d 4408	. . . . . . . . . . 11 $/\$ $/\$ $/\$
166	150, 153, 165	3bitrd 287	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
167	140, 166	syl5bb 265	. . . . . . . . 9 $/\$ $/\$ $/\$
168	139, 167	anbi12d 725	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
169	117	nnred 10646	. . . . . . . . . . 11 $/\$ $/\$ $/\$
170		bernneq3 12438	. . . . . . . . . . . 12 $/\$
171	108, 116, 170	syl2anc 673	. . . . . . . . . . 11 $/\$ $/\$ $/\$
172	124, 169, 171	ltled 9800	. . . . . . . . . 10 $/\$ $/\$ $/\$
173		letr 9745	. . . . . . . . . . 11 $/\$ $/\$ $/\$
174	124, 169, 94, 173	syl3anc 1292	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
175	172, 174	mpand 689	. . . . . . . . 9 $/\$ $/\$ $/\$
176	175	pm4.71rd 647	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
177	154	exp1d 12449	. . . . . . . . . . 11 $/\$ $/\$ $/\$
178	95	nnge1d 10674	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
179	96, 178, 128	leexp2ad 12486	. . . . . . . . . . 11 $/\$ $/\$ $/\$
180	177, 179	eqbrtrrd 4418	. . . . . . . . . 10 $/\$ $/\$ $/\$
181		letr 9745	. . . . . . . . . . 11 $/\$ $/\$ $/\$
182	96, 169, 94, 181	syl3anc 1292	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
183	180, 182	mpand 689	. . . . . . . . 9 $/\$ $/\$ $/\$
184	183	pm4.71rd 647	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
185	168, 176, 184	3bitr2rd 290	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
186	133, 185	bitrd 261	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
187	186	ex 441	. . . . 5 $/\$ $/\$ $/\$ $/\$
188	82, 89, 187	pm5.21ndd 361	. . . 4 $/\$ $/\$
189	9	adantrr 731	. . . 4 $/\$ $/\$
190	67, 68, 1, 188, 189	fsumcom2 13912	. . 3
191	66, 190	eqtr4d 2508	. 2
192	42, 43, 191	3eqtr4d 2515	1 ψ

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wcel 1904

cin 3389

wss 3390 class class class wbr 4395

cfv 5589 (class class class)co 6308

cfn 7587

cc 9555

cr 9556

cc0 9557

c1 9558

cmul 9562

clt 9693

cle 9694

cdiv 10291

cn 10631

c2 10681

cn0 10893

cz 10961

cuz 11182

crp 11325

cicc 11663

cfz 11810

cfl 12059

cexp 12310

chash 12553

csu 13829

cprime 14701

clog 23583

ccxp 23584

ccht 24096 ψcchp 24098

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-inf2 8164 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635 ax-addf 9636 ax-mulf 9637

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-fal 1458 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-iin 4272 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-of 6550 df-om 6712 df-1st 6812 df-2nd 6813 df-supp 6934 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-2o 7201 df-oadd 7204 df-er 7381 df-map 7492 df-pm 7493 df-ixp 7541 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-fsupp 7902 df-fi 7943 df-sup 7974 df-inf 7975 df-oi 8043 df-card 8391 df-cda 8616 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-4 10692 df-5 10693 df-6 10694 df-7 10695 df-8 10696 df-9 10697 df-10 10698 df-n0 10894 df-z 10962 df-dec 11075 df-uz 11183 df-q 11288 df-rp 11326 df-xneg 11432 df-xadd 11433 df-xmul 11434 df-ioo 11664 df-ioc 11665 df-ico 11666 df-icc 11667 df-fz 11811 df-fzo 11943 df-fl 12061 df-mod 12130 df-seq 12252 df-exp 12311 df-fac 12498 df-bc 12526 df-hash 12554 df-shft 13207 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 df-limsup 13603 df-clim 13629 df-rlim 13630 df-sum 13830 df-ef 14198 df-sin 14200 df-cos 14201 df-pi 14203 df-dvds 14383 df-gcd 14548 df-prm 14702 df-pc 14866 df-struct 15201 df-ndx 15202 df-slot 15203 df-base 15204 df-sets 15205 df-ress 15206 df-plusg 15281 df-mulr 15282 df-starv 15283 df-sca 15284 df-vsca 15285 df-ip 15286 df-tset 15287 df-ple 15288 df-ds 15290 df-unif 15291 df-hom 15292 df-cco 15293 df-rest 15399 df-topn 15400 df-0g 15418 df-gsum 15419 df-topgen 15420 df-pt 15421 df-prds 15424 df-xrs 15478 df-qtop 15484 df-imas 15485 df-xps 15488 df-mre 15570 df-mrc 15571 df-acs 15573 df-mgm 16566 df-sgrp 16605 df-mnd 16615 df-submnd 16661 df-mulg 16754 df-cntz 17049 df-cmn 17510 df-psmet 19039 df-xmet 19040 df-met 19041 df-bl 19042 df-mopn 19043 df-fbas 19044 df-fg 19045 df-cnfld 19048 df-top 19998 df-bases 19999 df-topon 20000 df-topsp 20001 df-cld 20111 df-ntr 20112 df-cls 20113 df-nei 20191 df-lp 20229 df-perf 20230 df-cn 20320 df-cnp 20321 df-haus 20408 df-tx 20654 df-hmeo 20847 df-fil 20939 df-fm 21031 df-flim 21032 df-flf 21033 df-xms 21413 df-ms 21414 df-tms 21415 df-cncf 21988 df-limc 22900 df-dv 22901 df-log 23585 df-cxp 23586 df-cht 24102 df-vma 24103 df-chp 24104

This theorem is referenced by: (None)

W3C validator