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 24147

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 12186	. . . . 5 $/\$
2		inss2 3653	. . . . . . . . . 10
3		simpr 463	. . . . . . . . . 10 $/\$
4	2, 3	sseldi 3430	. . . . . . . . 9 $/\$
5		prmnn 14625	. . . . . . . . 9
6	4, 5	syl 17	. . . . . . . 8 $/\$
7	6	nnrpd 11339	. . . . . . 7 $/\$
8	7	relogcld 23572	. . . . . 6 $/\$
9	8	recnd 9669	. . . . 5 $/\$
10		fsumconst 13851	. . . . 5 $/\$
11	1, 9, 10	syl2anc 667	. . . 4 $/\$
12		simpl 459	. . . . . . . . . 10 $/\$
13		1red 9658	. . . . . . . . . . 11 $/\$
14	6	nnred 10624	. . . . . . . . . . 11 $/\$
15		prmuz2 14642	. . . . . . . . . . . . 13
16	4, 15	syl 17	. . . . . . . . . . . 12 $/\$
17		eluz2b2 11231	. . . . . . . . . . . . 13 $/\$
18	17	simprbi 466	. . . . . . . . . . . 12
19	16, 18	syl 17	. . . . . . . . . . 11 $/\$
20		inss1 3652	. . . . . . . . . . . . . 14
21	20, 3	sseldi 3430	. . . . . . . . . . . . 13 $/\$
22		0re 9643	. . . . . . . . . . . . . 14
23		elicc2 11699	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
24	22, 12, 23	sylancr 669	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
25	21, 24	mpbid 214	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
26	25	simp3d 1022	. . . . . . . . . . 11 $/\$
27	13, 14, 12, 19, 26	ltletrd 9795	. . . . . . . . . 10 $/\$
28	12, 27	rplogcld 23578	. . . . . . . . 9 $/\$
29	14, 19	rplogcld 23578	. . . . . . . . 9 $/\$
30	28, 29	rpdivcld 11358	. . . . . . . 8 $/\$
31	30	rpred 11341	. . . . . . 7 $/\$
32	30	rpge0d 11345	. . . . . . 7 $/\$
33		flge0nn0 12054	. . . . . . 7 $/\$
34	31, 32, 33	syl2anc 667	. . . . . 6 $/\$
35		hashfz1 12529	. . . . . 6
36	34, 35	syl 17	. . . . 5 $/\$
37	36	oveq1d 6305	. . . 4 $/\$
38	31	flcld 12034	. . . . . 6 $/\$
39	38	zcnd 11041	. . . . 5 $/\$
40	39, 9	mulcomd 9664	. . . 4 $/\$
41	11, 37, 40	3eqtrrd 2490	. . 3 $/\$
42	41	sumeq2dv 13769	. 2
43		chpval2 24146	. 2 ψ
44		simpl 459	. . . . . 6 $/\$
45		0red 9644	. . . . . . 7 $/\$
46		1red 9658	. . . . . . . 8 $/\$
47		0lt1 10136	. . . . . . . . 9
48	47	a1i 11	. . . . . . . 8 $/\$
49		elfzuz2 11804	. . . . . . . . 9
50		eluzle 11171	. . . . . . . . . . 11
51	50	adantl 468	. . . . . . . . . 10 $/\$
52		simpl 459	. . . . . . . . . . 11 $/\$
53		1z 10967	. . . . . . . . . . 11
54		flge 12041	. . . . . . . . . . 11 $/\$
55	52, 53, 54	sylancl 668	. . . . . . . . . 10 $/\$
56	51, 55	mpbird 236	. . . . . . . . 9 $/\$
57	49, 56	sylan2 477	. . . . . . . 8 $/\$
58	45, 46, 44, 48, 57	ltletrd 9795	. . . . . . 7 $/\$
59	45, 44, 58	ltled 9783	. . . . . 6 $/\$
60		elfznn 11828	. . . . . . . 8
61	60	adantl 468	. . . . . . 7 $/\$
62	61	nnrecred 10655	. . . . . 6 $/\$
63	44, 59, 62	recxpcld 23668	. . . . 5 $/\$
64		chtval 24037	. . . . 5
65	63, 64	syl 17	. . . 4 $/\$
66	65	sumeq2dv 13769	. . 3
67		ppifi 24032	. . . 4
68		fzfid 12186	. . . 4
69	2	sseli 3428	. . . . . . . 8
70		elfznn 11828	. . . . . . . 8
71	69, 70	anim12i 570	. . . . . . 7 $/\$ $/\$
72	71	a1i 11	. . . . . 6 $/\$ $/\$
73		0red 9644	. . . . . . . . 9 $/\$
74	2	a1i 11	. . . . . . . . . . . 12
75	74	sselda 3432	. . . . . . . . . . 11 $/\$
76	75, 5	syl 17	. . . . . . . . . 10 $/\$
77	76	nnred 10624	. . . . . . . . 9 $/\$
78	76	nngt0d 10653	. . . . . . . . 9 $/\$
79	73, 77, 12, 78, 26	ltletrd 9795	. . . . . . . 8 $/\$
80	79	ex 436	. . . . . . 7
81	80	adantrd 470	. . . . . 6 $/\$
82	72, 81	jcad 536	. . . . 5 $/\$ $/\$ $/\$
83		inss2 3653	. . . . . . . . 9
84	83	sseli 3428	. . . . . . . 8
85	60, 84	anim12ci 571	. . . . . . 7 $/\$ $/\$
86	85	a1i 11	. . . . . 6 $/\$ $/\$
87	58	ex 436	. . . . . . 7
88	87	adantrd 470	. . . . . 6 $/\$
89	86, 88	jcad 536	. . . . 5 $/\$ $/\$ $/\$
90		elin 3617	. . . . . . . . 9 $/\$
91		simprll 772	. . . . . . . . . . 11 $/\$ $/\$ $/\$
92	91	biantrud 510	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
93		0red 9644	. . . . . . . . . . 11 $/\$ $/\$ $/\$
94		simpl 459	. . . . . . . . . . 11 $/\$ $/\$ $/\$
95	91, 5	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
96	95	nnred 10624	. . . . . . . . . . 11 $/\$ $/\$ $/\$
97	95	nnnn0d 10925	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
98	97	nn0ge0d 10928	. . . . . . . . . . 11 $/\$ $/\$ $/\$
99		df-3an 987	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
100	23, 99	syl6bb 265	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
101	100	baibd 920	. . . . . . . . . . 11 $/\$ $/\$ $/\$
102	93, 94, 96, 98, 101	syl22anc 1269	. . . . . . . . . 10 $/\$ $/\$ $/\$
103	92, 102	bitr3d 259	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
104	90, 103	syl5bb 261	. . . . . . . 8 $/\$ $/\$ $/\$
105		simprr 766	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
106	94, 105	elrpd 11338	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
107	106	relogcld 23572	. . . . . . . . . . 11 $/\$ $/\$ $/\$
108	91, 15	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
109	108, 18	syl 17	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
110	96, 109	rplogcld 23578	. . . . . . . . . . 11 $/\$ $/\$ $/\$
111	107, 110	rerpdivcld 11369	. . . . . . . . . 10 $/\$ $/\$ $/\$
112		simprlr 773	. . . . . . . . . . 11 $/\$ $/\$ $/\$
113	112	nnzd 11039	. . . . . . . . . 10 $/\$ $/\$ $/\$
114		flge 12041	. . . . . . . . . 10 $/\$
115	111, 113, 114	syl2anc 667	. . . . . . . . 9 $/\$ $/\$ $/\$
116	112	nnnn0d 10925	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
117	95, 116	nnexpcld 12437	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
118	117	nnrpd 11339	. . . . . . . . . . 11 $/\$ $/\$ $/\$
119	118, 106	logled 23576	. . . . . . . . . 10 $/\$ $/\$ $/\$
120	95	nnrpd 11339	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
121		relogexp 23545	. . . . . . . . . . . 12 $/\$
122	120, 113, 121	syl2anc 667	. . . . . . . . . . 11 $/\$ $/\$ $/\$
123	122	breq1d 4412	. . . . . . . . . 10 $/\$ $/\$ $/\$
124	112	nnred 10624	. . . . . . . . . . 11 $/\$ $/\$ $/\$
125	124, 107, 110	lemuldivd 11387	. . . . . . . . . 10 $/\$ $/\$ $/\$
126	119, 123, 125	3bitrd 283	. . . . . . . . 9 $/\$ $/\$ $/\$
127		nnuz 11194	. . . . . . . . . . 11
128	112, 127	syl6eleq 2539	. . . . . . . . . 10 $/\$ $/\$ $/\$
129	111	flcld 12034	. . . . . . . . . 10 $/\$ $/\$ $/\$
130		elfz5 11792	. . . . . . . . . 10 $/\$
131	128, 129, 130	syl2anc 667	. . . . . . . . 9 $/\$ $/\$ $/\$
132	115, 126, 131	3bitr4rd 290	. . . . . . . 8 $/\$ $/\$ $/\$
133	104, 132	anbi12d 717	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
134	94	flcld 12034	. . . . . . . . . . 11 $/\$ $/\$ $/\$
135		elfz5 11792	. . . . . . . . . . 11 $/\$
136	128, 134, 135	syl2anc 667	. . . . . . . . . 10 $/\$ $/\$ $/\$
137		flge 12041	. . . . . . . . . . 11 $/\$
138	94, 113, 137	syl2anc 667	. . . . . . . . . 10 $/\$ $/\$ $/\$
139	136, 138	bitr4d 260	. . . . . . . . 9 $/\$ $/\$ $/\$
140		elin 3617	. . . . . . . . . 10 $/\$
141	91	biantrud 510	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
142	106	rpge0d 11345	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
143	112	nnrecred 10655	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
144	94, 142, 143	recxpcld 23668	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
145		elicc2 11699	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
146		df-3an 987	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
147	145, 146	syl6bb 265	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
148	147	baibd 920	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
149	93, 144, 96, 98, 148	syl22anc 1269	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
150	141, 149	bitr3d 259	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
151	94, 142, 143	cxpge0d 23669	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
152	112	nnrpd 11339	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
153	96, 98, 144, 151, 152	cxple2d 23672	. . . . . . . . . . 11 $/\$ $/\$ $/\$
154	95	nncnd 10625	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
155		cxpexp 23613	. . . . . . . . . . . . 13 $/\$
156	154, 116, 155	syl2anc 667	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
157	112	nncnd 10625	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
158	112	nnne0d 10654	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
159	157, 158	recid2d 10379	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
160	159	oveq2d 6306	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
161	106, 143, 157	cxpmuld 23679	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
162	94	recnd 9669	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
163	162	cxp1d 23651	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
164	160, 161, 163	3eqtr3d 2493	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
165	156, 164	breq12d 4415	. . . . . . . . . . 11 $/\$ $/\$ $/\$
166	150, 153, 165	3bitrd 283	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
167	140, 166	syl5bb 261	. . . . . . . . 9 $/\$ $/\$ $/\$
168	139, 167	anbi12d 717	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
169	117	nnred 10624	. . . . . . . . . . 11 $/\$ $/\$ $/\$
170		bernneq3 12400	. . . . . . . . . . . 12 $/\$
171	108, 116, 170	syl2anc 667	. . . . . . . . . . 11 $/\$ $/\$ $/\$
172	124, 169, 171	ltled 9783	. . . . . . . . . 10 $/\$ $/\$ $/\$
173		letr 9727	. . . . . . . . . . 11 $/\$ $/\$ $/\$
174	124, 169, 94, 173	syl3anc 1268	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
175	172, 174	mpand 681	. . . . . . . . 9 $/\$ $/\$ $/\$
176	175	pm4.71rd 641	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
177	154	exp1d 12411	. . . . . . . . . . 11 $/\$ $/\$ $/\$
178	95	nnge1d 10652	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
179	96, 178, 128	leexp2ad 12448	. . . . . . . . . . 11 $/\$ $/\$ $/\$
180	177, 179	eqbrtrrd 4425	. . . . . . . . . 10 $/\$ $/\$ $/\$
181		letr 9727	. . . . . . . . . . 11 $/\$ $/\$ $/\$
182	96, 169, 94, 181	syl3anc 1268	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
183	180, 182	mpand 681	. . . . . . . . 9 $/\$ $/\$ $/\$
184	183	pm4.71rd 641	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
185	168, 176, 184	3bitr2rd 286	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
186	133, 185	bitrd 257	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
187	186	ex 436	. . . . 5 $/\$ $/\$ $/\$ $/\$
188	82, 89, 187	pm5.21ndd 356	. . . 4 $/\$ $/\$
189	9	adantrr 723	. . . 4 $/\$ $/\$
190	67, 68, 1, 188, 189	fsumcom2 13835	. . 3
191	66, 190	eqtr4d 2488	. 2
192	42, 43, 191	3eqtr4d 2495	1 ψ

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 985

wceq 1444

wcel 1887

cin 3403

wss 3404 class class class wbr 4402

cfv 5582 (class class class)co 6290

cfn 7569

cc 9537

cr 9538

cc0 9539

c1 9540

cmul 9544

clt 9675

cle 9676

cdiv 10269

cn 10609

c2 10659

cn0 10869

cz 10937

cuz 11159

crp 11302

cicc 11638

cfz 11784

cfl 12026

cexp 12272

chash 12515

csu 13752

cprime 14622

clog 23504

ccxp 23505

ccht 24017 ψcchp 24019

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-inf2 8146 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616 ax-pre-sup 9617 ax-addf 9618 ax-mulf 9619

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-fal 1450 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-iin 4281 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-se 4794 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-isom 5591 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-of 6531 df-om 6693 df-1st 6793 df-2nd 6794 df-supp 6915 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-2o 7183 df-oadd 7186 df-er 7363 df-map 7474 df-pm 7475 df-ixp 7523 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-fsupp 7884 df-fi 7925 df-sup 7956 df-inf 7957 df-oi 8025 df-card 8373 df-cda 8598 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-div 10270 df-nn 10610 df-2 10668 df-3 10669 df-4 10670 df-5 10671 df-6 10672 df-7 10673 df-8 10674 df-9 10675 df-10 10676 df-n0 10870 df-z 10938 df-dec 11052 df-uz 11160 df-q 11265 df-rp 11303 df-xneg 11409 df-xadd 11410 df-xmul 11411 df-ioo 11639 df-ioc 11640 df-ico 11641 df-icc 11642 df-fz 11785 df-fzo 11916 df-fl 12028 df-mod 12097 df-seq 12214 df-exp 12273 df-fac 12460 df-bc 12488 df-hash 12516 df-shft 13130 df-cj 13162 df-re 13163 df-im 13164 df-sqrt 13298 df-abs 13299 df-limsup 13526 df-clim 13552 df-rlim 13553 df-sum 13753 df-ef 14121 df-sin 14123 df-cos 14124 df-pi 14126 df-dvds 14306 df-gcd 14469 df-prm 14623 df-pc 14787 df-struct 15123 df-ndx 15124 df-slot 15125 df-base 15126 df-sets 15127 df-ress 15128 df-plusg 15203 df-mulr 15204 df-starv 15205 df-sca 15206 df-vsca 15207 df-ip 15208 df-tset 15209 df-ple 15210 df-ds 15212 df-unif 15213 df-hom 15214 df-cco 15215 df-rest 15321 df-topn 15322 df-0g 15340 df-gsum 15341 df-topgen 15342 df-pt 15343 df-prds 15346 df-xrs 15400 df-qtop 15406 df-imas 15407 df-xps 15410 df-mre 15492 df-mrc 15493 df-acs 15495 df-mgm 16488 df-sgrp 16527 df-mnd 16537 df-submnd 16583 df-mulg 16676 df-cntz 16971 df-cmn 17432 df-psmet 18962 df-xmet 18963 df-met 18964 df-bl 18965 df-mopn 18966 df-fbas 18967 df-fg 18968 df-cnfld 18971 df-top 19921 df-bases 19922 df-topon 19923 df-topsp 19924 df-cld 20034 df-ntr 20035 df-cls 20036 df-nei 20114 df-lp 20152 df-perf 20153 df-cn 20243 df-cnp 20244 df-haus 20331 df-tx 20577 df-hmeo 20770 df-fil 20861 df-fm 20953 df-flim 20954 df-flf 20955 df-xms 21335 df-ms 21336 df-tms 21337 df-cncf 21910 df-limc 22821 df-dv 22822 df-log 23506 df-cxp 23507 df-cht 24023 df-vma 24024 df-chp 24025

This theorem is referenced by: (None)

W3C validator