Proof of Theorem chtdif
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eluzelre 12890 | . . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℝ) | 
| 2 |  | chtval 27154 | . . . . 5
⊢ (𝑁 ∈ ℝ →
(θ‘𝑁) =
Σ𝑝 ∈ ((0[,]𝑁) ∩ ℙ)(log‘𝑝)) | 
| 3 | 1, 2 | syl 17 | . . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (θ‘𝑁) = Σ𝑝 ∈ ((0[,]𝑁) ∩ ℙ)(log‘𝑝)) | 
| 4 |  | eluzel2 12884 | . . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) | 
| 5 |  | 2z 12651 | . . . . . . . . . 10
⊢ 2 ∈
ℤ | 
| 6 |  | ifcl 4570 | . . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 2 ∈
ℤ) → if(𝑀 ≤
2, 𝑀, 2) ∈
ℤ) | 
| 7 | 4, 5, 6 | sylancl 586 | . . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → if(𝑀 ≤ 2, 𝑀, 2) ∈ ℤ) | 
| 8 | 5 | a1i 11 | . . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 2 ∈ ℤ) | 
| 9 | 4 | zred 12724 | . . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℝ) | 
| 10 |  | 2re 12341 | . . . . . . . . . 10
⊢ 2 ∈
ℝ | 
| 11 |  | min2 13233 | . . . . . . . . . 10
⊢ ((𝑀 ∈ ℝ ∧ 2 ∈
ℝ) → if(𝑀 ≤
2, 𝑀, 2) ≤
2) | 
| 12 | 9, 10, 11 | sylancl 586 | . . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → if(𝑀 ≤ 2, 𝑀, 2) ≤ 2) | 
| 13 |  | eluz2 12885 | . . . . . . . . 9
⊢ (2 ∈
(ℤ≥‘if(𝑀 ≤ 2, 𝑀, 2)) ↔ (if(𝑀 ≤ 2, 𝑀, 2) ∈ ℤ ∧ 2 ∈ ℤ
∧ if(𝑀 ≤ 2, 𝑀, 2) ≤ 2)) | 
| 14 | 7, 8, 12, 13 | syl3anbrc 1343 | . . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 2 ∈
(ℤ≥‘if(𝑀 ≤ 2, 𝑀, 2))) | 
| 15 |  | ppisval2 27149 | . . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 2 ∈
(ℤ≥‘if(𝑀 ≤ 2, 𝑀, 2))) → ((0[,]𝑁) ∩ ℙ) = ((if(𝑀 ≤ 2, 𝑀, 2)...(⌊‘𝑁)) ∩ ℙ)) | 
| 16 | 1, 14, 15 | syl2anc 584 | . . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((0[,]𝑁) ∩ ℙ) = ((if(𝑀 ≤ 2, 𝑀, 2)...(⌊‘𝑁)) ∩ ℙ)) | 
| 17 |  | eluzelz 12889 | . . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) | 
| 18 |  | flid 13849 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℤ →
(⌊‘𝑁) = 𝑁) | 
| 19 | 17, 18 | syl 17 | . . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (⌊‘𝑁) = 𝑁) | 
| 20 | 19 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (if(𝑀 ≤ 2, 𝑀, 2)...(⌊‘𝑁)) = (if(𝑀 ≤ 2, 𝑀, 2)...𝑁)) | 
| 21 | 20 | ineq1d 4218 | . . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((if(𝑀 ≤ 2, 𝑀, 2)...(⌊‘𝑁)) ∩ ℙ) = ((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ)) | 
| 22 | 16, 21 | eqtrd 2776 | . . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((0[,]𝑁) ∩ ℙ) = ((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ)) | 
| 23 | 22 | sumeq1d 15737 | . . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → Σ𝑝 ∈ ((0[,]𝑁) ∩ ℙ)(log‘𝑝) = Σ𝑝 ∈ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ)(log‘𝑝)) | 
| 24 | 9 | ltp1d 12199 | . . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 < (𝑀 + 1)) | 
| 25 |  | fzdisj 13592 | . . . . . . . . 9
⊢ (𝑀 < (𝑀 + 1) → ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅) | 
| 26 | 24, 25 | syl 17 | . . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅) | 
| 27 | 26 | ineq1d 4218 | . . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ((𝑀 + 1)...𝑁)) ∩ ℙ) = (∅ ∩
ℙ)) | 
| 28 |  | inindir 4235 | . . . . . . 7
⊢
(((if(𝑀 ≤ 2,
𝑀, 2)...𝑀) ∩ ((𝑀 + 1)...𝑁)) ∩ ℙ) = (((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ∩ (((𝑀 + 1)...𝑁) ∩ ℙ)) | 
| 29 |  | 0in 4396 | . . . . . . 7
⊢ (∅
∩ ℙ) = ∅ | 
| 30 | 27, 28, 29 | 3eqtr3g 2799 | . . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ∩ (((𝑀 + 1)...𝑁) ∩ ℙ)) =
∅) | 
| 31 |  | min1 13232 | . . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℝ ∧ 2 ∈
ℝ) → if(𝑀 ≤
2, 𝑀, 2) ≤ 𝑀) | 
| 32 | 9, 10, 31 | sylancl 586 | . . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → if(𝑀 ≤ 2, 𝑀, 2) ≤ 𝑀) | 
| 33 |  | eluz2 12885 | . . . . . . . . . . 11
⊢ (𝑀 ∈
(ℤ≥‘if(𝑀 ≤ 2, 𝑀, 2)) ↔ (if(𝑀 ≤ 2, 𝑀, 2) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ if(𝑀 ≤ 2, 𝑀, 2) ≤ 𝑀)) | 
| 34 | 7, 4, 32, 33 | syl3anbrc 1343 | . . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈
(ℤ≥‘if(𝑀 ≤ 2, 𝑀, 2))) | 
| 35 |  | id 22 | . . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (ℤ≥‘𝑀)) | 
| 36 |  | elfzuzb 13559 | . . . . . . . . . 10
⊢ (𝑀 ∈ (if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ↔ (𝑀 ∈
(ℤ≥‘if(𝑀 ≤ 2, 𝑀, 2)) ∧ 𝑁 ∈ (ℤ≥‘𝑀))) | 
| 37 | 34, 35, 36 | sylanbrc 583 | . . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (if(𝑀 ≤ 2, 𝑀, 2)...𝑁)) | 
| 38 |  | fzsplit 13591 | . . . . . . . . 9
⊢ (𝑀 ∈ (if(𝑀 ≤ 2, 𝑀, 2)...𝑁) → (if(𝑀 ≤ 2, 𝑀, 2)...𝑁) = ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∪ ((𝑀 + 1)...𝑁))) | 
| 39 | 37, 38 | syl 17 | . . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (if(𝑀 ≤ 2, 𝑀, 2)...𝑁) = ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∪ ((𝑀 + 1)...𝑁))) | 
| 40 | 39 | ineq1d 4218 | . . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ) = (((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∪ ((𝑀 + 1)...𝑁)) ∩ ℙ)) | 
| 41 |  | indir 4285 | . . . . . . 7
⊢
(((if(𝑀 ≤ 2,
𝑀, 2)...𝑀) ∪ ((𝑀 + 1)...𝑁)) ∩ ℙ) = (((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ∪ (((𝑀 + 1)...𝑁) ∩ ℙ)) | 
| 42 | 40, 41 | eqtrdi 2792 | . . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ) = (((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ∪ (((𝑀 + 1)...𝑁) ∩ ℙ))) | 
| 43 |  | fzfid 14015 | . . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∈ Fin) | 
| 44 |  | inss1 4236 | . . . . . . 7
⊢
((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ) ⊆ (if(𝑀 ≤ 2, 𝑀, 2)...𝑁) | 
| 45 |  | ssfi 9214 | . . . . . . 7
⊢
(((if(𝑀 ≤ 2,
𝑀, 2)...𝑁) ∈ Fin ∧ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ) ⊆ (if(𝑀 ≤ 2, 𝑀, 2)...𝑁)) → ((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ) ∈
Fin) | 
| 46 | 43, 44, 45 | sylancl 586 | . . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ) ∈
Fin) | 
| 47 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑝 ∈ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ)) → 𝑝 ∈ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ)) | 
| 48 | 47 | elin2d 4204 | . . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑝 ∈ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ)) → 𝑝 ∈ ℙ) | 
| 49 |  | prmnn 16712 | . . . . . . . . . 10
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) | 
| 50 | 48, 49 | syl 17 | . . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑝 ∈ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ)) → 𝑝 ∈ ℕ) | 
| 51 | 50 | nnrpd 13076 | . . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑝 ∈ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ)) → 𝑝 ∈ ℝ+) | 
| 52 | 51 | relogcld 26666 | . . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑝 ∈ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ)) → (log‘𝑝) ∈
ℝ) | 
| 53 | 52 | recnd 11290 | . . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑝 ∈ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ)) → (log‘𝑝) ∈
ℂ) | 
| 54 | 30, 42, 46, 53 | fsumsplit 15778 | . . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → Σ𝑝 ∈ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ)(log‘𝑝) = (Σ𝑝 ∈ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)(log‘𝑝) + Σ𝑝 ∈ (((𝑀 + 1)...𝑁) ∩ ℙ)(log‘𝑝))) | 
| 55 | 23, 54 | eqtrd 2776 | . . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → Σ𝑝 ∈ ((0[,]𝑁) ∩ ℙ)(log‘𝑝) = (Σ𝑝 ∈ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)(log‘𝑝) + Σ𝑝 ∈ (((𝑀 + 1)...𝑁) ∩ ℙ)(log‘𝑝))) | 
| 56 | 3, 55 | eqtrd 2776 | . . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (θ‘𝑁) = (Σ𝑝 ∈ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)(log‘𝑝) + Σ𝑝 ∈ (((𝑀 + 1)...𝑁) ∩ ℙ)(log‘𝑝))) | 
| 57 |  | chtval 27154 | . . . . 5
⊢ (𝑀 ∈ ℝ →
(θ‘𝑀) =
Σ𝑝 ∈ ((0[,]𝑀) ∩ ℙ)(log‘𝑝)) | 
| 58 | 9, 57 | syl 17 | . . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (θ‘𝑀) = Σ𝑝 ∈ ((0[,]𝑀) ∩ ℙ)(log‘𝑝)) | 
| 59 |  | ppisval2 27149 | . . . . . . 7
⊢ ((𝑀 ∈ ℝ ∧ 2 ∈
(ℤ≥‘if(𝑀 ≤ 2, 𝑀, 2))) → ((0[,]𝑀) ∩ ℙ) = ((if(𝑀 ≤ 2, 𝑀, 2)...(⌊‘𝑀)) ∩ ℙ)) | 
| 60 | 9, 14, 59 | syl2anc 584 | . . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((0[,]𝑀) ∩ ℙ) = ((if(𝑀 ≤ 2, 𝑀, 2)...(⌊‘𝑀)) ∩ ℙ)) | 
| 61 |  | flid 13849 | . . . . . . . . 9
⊢ (𝑀 ∈ ℤ →
(⌊‘𝑀) = 𝑀) | 
| 62 | 4, 61 | syl 17 | . . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (⌊‘𝑀) = 𝑀) | 
| 63 | 62 | oveq2d 7448 | . . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (if(𝑀 ≤ 2, 𝑀, 2)...(⌊‘𝑀)) = (if(𝑀 ≤ 2, 𝑀, 2)...𝑀)) | 
| 64 | 63 | ineq1d 4218 | . . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((if(𝑀 ≤ 2, 𝑀, 2)...(⌊‘𝑀)) ∩ ℙ) = ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)) | 
| 65 | 60, 64 | eqtrd 2776 | . . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((0[,]𝑀) ∩ ℙ) = ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)) | 
| 66 | 65 | sumeq1d 15737 | . . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → Σ𝑝 ∈ ((0[,]𝑀) ∩ ℙ)(log‘𝑝) = Σ𝑝 ∈ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)(log‘𝑝)) | 
| 67 | 58, 66 | eqtrd 2776 | . . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (θ‘𝑀) = Σ𝑝 ∈ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)(log‘𝑝)) | 
| 68 | 56, 67 | oveq12d 7450 | . 2
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((θ‘𝑁) − (θ‘𝑀)) = ((Σ𝑝 ∈ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)(log‘𝑝) + Σ𝑝 ∈ (((𝑀 + 1)...𝑁) ∩ ℙ)(log‘𝑝)) − Σ𝑝 ∈ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)(log‘𝑝))) | 
| 69 |  | fzfi 14014 | . . . . . 6
⊢ (if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∈ Fin | 
| 70 |  | inss1 4236 | . . . . . 6
⊢
((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ⊆ (if(𝑀 ≤ 2, 𝑀, 2)...𝑀) | 
| 71 |  | ssfi 9214 | . . . . . 6
⊢
(((if(𝑀 ≤ 2,
𝑀, 2)...𝑀) ∈ Fin ∧ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ⊆ (if(𝑀 ≤ 2, 𝑀, 2)...𝑀)) → ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ∈
Fin) | 
| 72 | 69, 70, 71 | mp2an 692 | . . . . 5
⊢
((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ∈ Fin | 
| 73 | 72 | a1i 11 | . . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ∈
Fin) | 
| 74 |  | ssun1 4177 | . . . . . . 7
⊢
((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ⊆ (((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ∪ (((𝑀 + 1)...𝑁) ∩ ℙ)) | 
| 75 | 74, 42 | sseqtrrid 4026 | . . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ⊆ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ)) | 
| 76 | 75 | sselda 3982 | . . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑝 ∈ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)) → 𝑝 ∈ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ)) | 
| 77 | 76, 53 | syldan 591 | . . . 4
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑝 ∈ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)) → (log‘𝑝) ∈
ℂ) | 
| 78 | 73, 77 | fsumcl 15770 | . . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → Σ𝑝 ∈ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)(log‘𝑝) ∈
ℂ) | 
| 79 |  | fzfi 14014 | . . . . . 6
⊢ ((𝑀 + 1)...𝑁) ∈ Fin | 
| 80 |  | inss1 4236 | . . . . . 6
⊢ (((𝑀 + 1)...𝑁) ∩ ℙ) ⊆ ((𝑀 + 1)...𝑁) | 
| 81 |  | ssfi 9214 | . . . . . 6
⊢ ((((𝑀 + 1)...𝑁) ∈ Fin ∧ (((𝑀 + 1)...𝑁) ∩ ℙ) ⊆ ((𝑀 + 1)...𝑁)) → (((𝑀 + 1)...𝑁) ∩ ℙ) ∈
Fin) | 
| 82 | 79, 80, 81 | mp2an 692 | . . . . 5
⊢ (((𝑀 + 1)...𝑁) ∩ ℙ) ∈ Fin | 
| 83 | 82 | a1i 11 | . . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (((𝑀 + 1)...𝑁) ∩ ℙ) ∈
Fin) | 
| 84 |  | ssun2 4178 | . . . . . . 7
⊢ (((𝑀 + 1)...𝑁) ∩ ℙ) ⊆ (((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ) ∪ (((𝑀 + 1)...𝑁) ∩ ℙ)) | 
| 85 | 84, 42 | sseqtrrid 4026 | . . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (((𝑀 + 1)...𝑁) ∩ ℙ) ⊆ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ)) | 
| 86 | 85 | sselda 3982 | . . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑝 ∈ (((𝑀 + 1)...𝑁) ∩ ℙ)) → 𝑝 ∈ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑁) ∩ ℙ)) | 
| 87 | 86, 53 | syldan 591 | . . . 4
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑝 ∈ (((𝑀 + 1)...𝑁) ∩ ℙ)) → (log‘𝑝) ∈
ℂ) | 
| 88 | 83, 87 | fsumcl 15770 | . . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → Σ𝑝 ∈ (((𝑀 + 1)...𝑁) ∩ ℙ)(log‘𝑝) ∈
ℂ) | 
| 89 | 78, 88 | pncan2d 11623 | . 2
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((Σ𝑝 ∈ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)(log‘𝑝) + Σ𝑝 ∈ (((𝑀 + 1)...𝑁) ∩ ℙ)(log‘𝑝)) − Σ𝑝 ∈ ((if(𝑀 ≤ 2, 𝑀, 2)...𝑀) ∩ ℙ)(log‘𝑝)) = Σ𝑝 ∈ (((𝑀 + 1)...𝑁) ∩ ℙ)(log‘𝑝)) | 
| 90 | 68, 89 | eqtrd 2776 | 1
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((θ‘𝑁) − (θ‘𝑀)) = Σ𝑝 ∈ (((𝑀 + 1)...𝑁) ∩ ℙ)(log‘𝑝)) |