This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( θ ‘ 𝑁 ) − ( θ ‘ 𝑀 ) ) = Σ 𝑝 ∈ ( ( ( 𝑀 + 1 ) ... 𝑁 ) ∩ ℙ ) ( log ‘ 𝑝 ) )

Proof

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