Theorem chtdif

Description: The difference of the Chebyshev function at two points sums the logarithms of the primes in an interval. (Contributed by Mario Carneiro, 22-Sep-2014)

	Ref	Expression
Assertion	chtdif	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \theta \left(N\right)-\theta \left(M\right)=\sum _{p\in \left(M+1\dots N\right)\cap \mathbb{P}}\log p$$

Proof

Step	Hyp	Ref	Expression
1		eluzelre	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in ℝ$$
2		chtval	$$⊢N\in ℝ\to \theta \left(N\right)=\sum _{p\in \left[0,N\right]\cap \mathbb{P}}\log p$$
3	1 2	syl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \theta \left(N\right)=\sum _{p\in \left[0,N\right]\cap \mathbb{P}}\log p$$
4		eluzel2	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in \mathbb{Z}$$
5		2z	$$⊢2\in \mathbb{Z}$$
6		ifcl	$$⊢\left(M\in \mathbb{Z}\wedge 2\in \mathbb{Z}\right)\to if\left(M\le 2,M,2\right)\in \mathbb{Z}$$
7	4 5 6	sylancl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to if\left(M\le 2,M,2\right)\in \mathbb{Z}$$
8	5	a1i	$$⊢N\in {\mathbb{Z}}_{\ge M}\to 2\in \mathbb{Z}$$
9	4	zred	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in ℝ$$
10		2re	$$⊢2\in ℝ$$
11		min2	$$⊢\left(M\in ℝ\wedge 2\in ℝ\right)\to if\left(M\le 2,M,2\right)\le 2$$
12	9 10 11	sylancl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to if\left(M\le 2,M,2\right)\le 2$$
13		eluz2	$$⊢2\in {\mathbb{Z}}_{\ge if\left(M\le 2,M,2\right)}\leftrightarrow \left(if\left(M\le 2,M,2\right)\in \mathbb{Z}\wedge 2\in \mathbb{Z}\wedge if\left(M\le 2,M,2\right)\le 2\right)$$
14	7 8 12 13	syl3anbrc	$$⊢N\in {\mathbb{Z}}_{\ge M}\to 2\in {\mathbb{Z}}_{\ge if\left(M\le 2,M,2\right)}$$
15		ppisval2	$$⊢\left(N\in ℝ\wedge 2\in {\mathbb{Z}}_{\ge if\left(M\le 2,M,2\right)}\right)\to \left[0,N\right]\cap \mathbb{P}=\left(if\left(M\le 2,M,2\right)\dots ⌊N⌋\right)\cap \mathbb{P}$$
16	1 14 15	syl2anc	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left[0,N\right]\cap \mathbb{P}=\left(if\left(M\le 2,M,2\right)\dots ⌊N⌋\right)\cap \mathbb{P}$$
17		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in \mathbb{Z}$$
18		flid	$$⊢N\in \mathbb{Z}\to ⌊N⌋=N$$
19	17 18	syl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to ⌊N⌋=N$$
20	19	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(if\left(M\le 2,M,2\right)\dots ⌊N⌋\right)=\left(if\left(M\le 2,M,2\right)\dots N\right)$$
21	20	ineq1d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(if\left(M\le 2,M,2\right)\dots ⌊N⌋\right)\cap \mathbb{P}=\left(if\left(M\le 2,M,2\right)\dots N\right)\cap \mathbb{P}$$
22	16 21	eqtrd	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left[0,N\right]\cap \mathbb{P}=\left(if\left(M\le 2,M,2\right)\dots N\right)\cap \mathbb{P}$$
23	22	sumeq1d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \sum _{p\in \left[0,N\right]\cap \mathbb{P}}\log p=\sum _{p\in \left(if\left(M\le 2,M,2\right)\dots N\right)\cap \mathbb{P}}\log p$$
24	9	ltp1d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M<M+1$$
25		fzdisj	$$⊢M<M+1\to \left(if\left(M\le 2,M,2\right)\dots M\right)\cap \left(M+1\dots N\right)=\varnothing$$
26	24 25	syl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(if\left(M\le 2,M,2\right)\dots M\right)\cap \left(M+1\dots N\right)=\varnothing$$
27	26	ineq1d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \left(M+1\dots N\right)\right)\cap \mathbb{P}=\varnothing \cap \mathbb{P}$$
28		inindir	$$⊢\left(\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \left(M+1\dots N\right)\right)\cap \mathbb{P}=\left(\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right)\cap \left(\left(M+1\dots N\right)\cap \mathbb{P}\right)$$
29		0in	$$⊢\varnothing \cap \mathbb{P}=\varnothing$$
30	27 28 29	3eqtr3g	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right)\cap \left(\left(M+1\dots N\right)\cap \mathbb{P}\right)=\varnothing$$
31		min1	$$⊢\left(M\in ℝ\wedge 2\in ℝ\right)\to if\left(M\le 2,M,2\right)\le M$$
32	9 10 31	sylancl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to if\left(M\le 2,M,2\right)\le M$$
33		eluz2	$$⊢M\in {\mathbb{Z}}_{\ge if\left(M\le 2,M,2\right)}\leftrightarrow \left(if\left(M\le 2,M,2\right)\in \mathbb{Z}\wedge M\in \mathbb{Z}\wedge if\left(M\le 2,M,2\right)\le M\right)$$
34	7 4 32 33	syl3anbrc	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in {\mathbb{Z}}_{\ge if\left(M\le 2,M,2\right)}$$
35		id	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in {\mathbb{Z}}_{\ge M}$$
36		elfzuzb	$$⊢M\in \left(if\left(M\le 2,M,2\right)\dots N\right)\leftrightarrow \left(M\in {\mathbb{Z}}_{\ge if\left(M\le 2,M,2\right)}\wedge N\in {\mathbb{Z}}_{\ge M}\right)$$
37	34 35 36	sylanbrc	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in \left(if\left(M\le 2,M,2\right)\dots N\right)$$
38		fzsplit	$$⊢M\in \left(if\left(M\le 2,M,2\right)\dots N\right)\to \left(if\left(M\le 2,M,2\right)\dots N\right)=\left(if\left(M\le 2,M,2\right)\dots M\right)\cup \left(M+1\dots N\right)$$
39	37 38	syl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(if\left(M\le 2,M,2\right)\dots N\right)=\left(if\left(M\le 2,M,2\right)\dots M\right)\cup \left(M+1\dots N\right)$$
40	39	ineq1d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(if\left(M\le 2,M,2\right)\dots N\right)\cap \mathbb{P}=\left(\left(if\left(M\le 2,M,2\right)\dots M\right)\cup \left(M+1\dots N\right)\right)\cap \mathbb{P}$$
41		indir	$$⊢\left(\left(if\left(M\le 2,M,2\right)\dots M\right)\cup \left(M+1\dots N\right)\right)\cap \mathbb{P}=\left(\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right)\cup \left(\left(M+1\dots N\right)\cap \mathbb{P}\right)$$
42	40 41	eqtrdi	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(if\left(M\le 2,M,2\right)\dots N\right)\cap \mathbb{P}=\left(\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right)\cup \left(\left(M+1\dots N\right)\cap \mathbb{P}\right)$$
43		fzfid	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(if\left(M\le 2,M,2\right)\dots N\right)\in \mathrm{Fin}$$
44		inss1	$$⊢\left(if\left(M\le 2,M,2\right)\dots N\right)\cap \mathbb{P}\subseteq \left(if\left(M\le 2,M,2\right)\dots N\right)$$
45		ssfi	$$⊢\left(\left(if\left(M\le 2,M,2\right)\dots N\right)\in \mathrm{Fin}\wedge \left(if\left(M\le 2,M,2\right)\dots N\right)\cap \mathbb{P}\subseteq \left(if\left(M\le 2,M,2\right)\dots N\right)\right)\to \left(if\left(M\le 2,M,2\right)\dots N\right)\cap \mathbb{P}\in \mathrm{Fin}$$
46	43 44 45	sylancl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(if\left(M\le 2,M,2\right)\dots N\right)\cap \mathbb{P}\in \mathrm{Fin}$$
47		simpr	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge p\in \left(\left(if\left(M\le 2,M,2\right)\dots N\right)\cap \mathbb{P}\right)\right)\to p\in \left(\left(if\left(M\le 2,M,2\right)\dots N\right)\cap \mathbb{P}\right)$$
48	47	elin2d	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge p\in \left(\left(if\left(M\le 2,M,2\right)\dots N\right)\cap \mathbb{P}\right)\right)\to p\in \mathbb{P}$$
49		prmnn	$$⊢p\in \mathbb{P}\to p\in \mathbb{N}$$
50	48 49	syl	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge p\in \left(\left(if\left(M\le 2,M,2\right)\dots N\right)\cap \mathbb{P}\right)\right)\to p\in \mathbb{N}$$
51	50	nnrpd	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge p\in \left(\left(if\left(M\le 2,M,2\right)\dots N\right)\cap \mathbb{P}\right)\right)\to p\in {ℝ}^{+}$$
52	51	relogcld	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge p\in \left(\left(if\left(M\le 2,M,2\right)\dots N\right)\cap \mathbb{P}\right)\right)\to \log p\in ℝ$$
53	52	recnd	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge p\in \left(\left(if\left(M\le 2,M,2\right)\dots N\right)\cap \mathbb{P}\right)\right)\to \log p\in ℂ$$
54	30 42 46 53	fsumsplit	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \sum _{p\in \left(if\left(M\le 2,M,2\right)\dots N\right)\cap \mathbb{P}}\log p=\sum _{p\in \left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}}\log p+\sum _{p\in \left(M+1\dots N\right)\cap \mathbb{P}}\log p$$
55	23 54	eqtrd	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \sum _{p\in \left[0,N\right]\cap \mathbb{P}}\log p=\sum _{p\in \left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}}\log p+\sum _{p\in \left(M+1\dots N\right)\cap \mathbb{P}}\log p$$
56	3 55	eqtrd	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \theta \left(N\right)=\sum _{p\in \left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}}\log p+\sum _{p\in \left(M+1\dots N\right)\cap \mathbb{P}}\log p$$
57		chtval	$$⊢M\in ℝ\to \theta \left(M\right)=\sum _{p\in \left[0,M\right]\cap \mathbb{P}}\log p$$
58	9 57	syl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \theta \left(M\right)=\sum _{p\in \left[0,M\right]\cap \mathbb{P}}\log p$$
59		ppisval2	$$⊢\left(M\in ℝ\wedge 2\in {\mathbb{Z}}_{\ge if\left(M\le 2,M,2\right)}\right)\to \left[0,M\right]\cap \mathbb{P}=\left(if\left(M\le 2,M,2\right)\dots ⌊M⌋\right)\cap \mathbb{P}$$
60	9 14 59	syl2anc	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left[0,M\right]\cap \mathbb{P}=\left(if\left(M\le 2,M,2\right)\dots ⌊M⌋\right)\cap \mathbb{P}$$
61		flid	$$⊢M\in \mathbb{Z}\to ⌊M⌋=M$$
62	4 61	syl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to ⌊M⌋=M$$
63	62	oveq2d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(if\left(M\le 2,M,2\right)\dots ⌊M⌋\right)=\left(if\left(M\le 2,M,2\right)\dots M\right)$$
64	63	ineq1d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(if\left(M\le 2,M,2\right)\dots ⌊M⌋\right)\cap \mathbb{P}=\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}$$
65	60 64	eqtrd	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left[0,M\right]\cap \mathbb{P}=\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}$$
66	65	sumeq1d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \sum _{p\in \left[0,M\right]\cap \mathbb{P}}\log p=\sum _{p\in \left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}}\log p$$
67	58 66	eqtrd	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \theta \left(M\right)=\sum _{p\in \left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}}\log p$$
68	56 67	oveq12d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \theta \left(N\right)-\theta \left(M\right)=\sum _{p\in \left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}}\log p+\sum _{p\in \left(M+1\dots N\right)\cap \mathbb{P}}\log p-\sum _{p\in \left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}}\log p$$
69		fzfi	$$⊢\left(if\left(M\le 2,M,2\right)\dots M\right)\in \mathrm{Fin}$$
70		inss1	$$⊢\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\subseteq \left(if\left(M\le 2,M,2\right)\dots M\right)$$
71		ssfi	$$⊢\left(\left(if\left(M\le 2,M,2\right)\dots M\right)\in \mathrm{Fin}\wedge \left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\subseteq \left(if\left(M\le 2,M,2\right)\dots M\right)\right)\to \left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\in \mathrm{Fin}$$
72	69 70 71	mp2an	$$⊢\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\in \mathrm{Fin}$$
73	72	a1i	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\in \mathrm{Fin}$$
74		ssun1	$$⊢\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\subseteq \left(\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right)\cup \left(\left(M+1\dots N\right)\cap \mathbb{P}\right)$$
75	74 42	sseqtrrid	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\subseteq \left(if\left(M\le 2,M,2\right)\dots N\right)\cap \mathbb{P}$$
76	75	sselda	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge p\in \left(\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right)\right)\to p\in \left(\left(if\left(M\le 2,M,2\right)\dots N\right)\cap \mathbb{P}\right)$$
77	76 53	syldan	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge p\in \left(\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right)\right)\to \log p\in ℂ$$
78	73 77	fsumcl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \sum _{p\in \left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}}\log p\in ℂ$$
79		fzfi	$$⊢\left(M+1\dots N\right)\in \mathrm{Fin}$$
80		inss1	$$⊢\left(M+1\dots N\right)\cap \mathbb{P}\subseteq \left(M+1\dots N\right)$$
81		ssfi	$$⊢\left(\left(M+1\dots N\right)\in \mathrm{Fin}\wedge \left(M+1\dots N\right)\cap \mathbb{P}\subseteq \left(M+1\dots N\right)\right)\to \left(M+1\dots N\right)\cap \mathbb{P}\in \mathrm{Fin}$$
82	79 80 81	mp2an	$$⊢\left(M+1\dots N\right)\cap \mathbb{P}\in \mathrm{Fin}$$
83	82	a1i	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(M+1\dots N\right)\cap \mathbb{P}\in \mathrm{Fin}$$
84		ssun2	$$⊢\left(M+1\dots N\right)\cap \mathbb{P}\subseteq \left(\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right)\cup \left(\left(M+1\dots N\right)\cap \mathbb{P}\right)$$
85	84 42	sseqtrrid	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(M+1\dots N\right)\cap \mathbb{P}\subseteq \left(if\left(M\le 2,M,2\right)\dots N\right)\cap \mathbb{P}$$
86	85	sselda	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge p\in \left(\left(M+1\dots N\right)\cap \mathbb{P}\right)\right)\to p\in \left(\left(if\left(M\le 2,M,2\right)\dots N\right)\cap \mathbb{P}\right)$$
87	86 53	syldan	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge p\in \left(\left(M+1\dots N\right)\cap \mathbb{P}\right)\right)\to \log p\in ℂ$$
88	83 87	fsumcl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \sum _{p\in \left(M+1\dots N\right)\cap \mathbb{P}}\log p\in ℂ$$
89	78 88	pncan2d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \sum _{p\in \left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}}\log p+\sum _{p\in \left(M+1\dots N\right)\cap \mathbb{P}}\log p-\sum _{p\in \left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}}\log p=\sum _{p\in \left(M+1\dots N\right)\cap \mathbb{P}}\log p$$
90	68 89	eqtrd	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \theta \left(N\right)-\theta \left(M\right)=\sum _{p\in \left(M+1\dots N\right)\cap \mathbb{P}}\log p$$