# Metamath Proof Explorer

## 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 {ℤ}_{\ge {M}}\to \theta \left({N}\right)-\theta \left({M}\right)=\sum _{{p}\in \left({M}+1\dots {N}\right)\cap ℙ}\mathrm{log}{p}$

### Proof

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