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 e. ( ZZ>= ` M ) -> ( ( theta ` N ) - ( theta ` M ) ) = sum_ p e. ( ( ( M + 1 ) ... N ) i^i Prime ) ( log ` p ) )

Proof

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