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 M θ N θ M = p M + 1 N log p

Proof

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