| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑥 = 𝐾 → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...𝐾)) | 
| 2 | 1 | iuneq1d 5018 | . . . . . 6
⊢ (𝑥 = 𝐾 → ∪
𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘) = ∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) | 
| 3 | 2 | fveq2d 6909 | . . . . 5
⊢ (𝑥 = 𝐾 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) = (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘))) | 
| 4 | 1 | sumeq1d 15737 | . . . . . 6
⊢ (𝑥 = 𝐾 → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) | 
| 5 | 4 | oveq2d 7448 | . . . . 5
⊢ (𝑥 = 𝐾 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) | 
| 6 | 3, 5 | breq12d 5155 | . . . 4
⊢ (𝑥 = 𝐾 → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) | 
| 7 | 6 | imbi2d 340 | . . 3
⊢ (𝑥 = 𝐾 → ((𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))) | 
| 8 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑥 = 𝑗 → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...𝑗)) | 
| 9 | 8 | iuneq1d 5018 | . . . . . 6
⊢ (𝑥 = 𝑗 → ∪
𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘) = ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) | 
| 10 | 9 | fveq2d 6909 | . . . . 5
⊢ (𝑥 = 𝑗 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) = (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘))) | 
| 11 | 8 | sumeq1d 15737 | . . . . . 6
⊢ (𝑥 = 𝑗 → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) | 
| 12 | 11 | oveq2d 7448 | . . . . 5
⊢ (𝑥 = 𝑗 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) | 
| 13 | 10, 12 | breq12d 5155 | . . . 4
⊢ (𝑥 = 𝑗 → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) | 
| 14 | 13 | imbi2d 340 | . . 3
⊢ (𝑥 = 𝑗 → ((𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))) | 
| 15 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑥 = (𝑗 + 1) → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...(𝑗 + 1))) | 
| 16 | 15 | iuneq1d 5018 | . . . . . 6
⊢ (𝑥 = (𝑗 + 1) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘) = ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) | 
| 17 | 16 | fveq2d 6909 | . . . . 5
⊢ (𝑥 = (𝑗 + 1) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) = (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘))) | 
| 18 | 15 | sumeq1d 15737 | . . . . . 6
⊢ (𝑥 = (𝑗 + 1) → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) | 
| 19 | 18 | oveq2d 7448 | . . . . 5
⊢ (𝑥 = (𝑗 + 1) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) | 
| 20 | 17, 19 | breq12d 5155 | . . . 4
⊢ (𝑥 = (𝑗 + 1) → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) | 
| 21 | 20 | imbi2d 340 | . . 3
⊢ (𝑥 = (𝑗 + 1) → ((𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))) | 
| 22 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑥 = 𝑁 → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...𝑁)) | 
| 23 | 22 | iuneq1d 5018 | . . . . . 6
⊢ (𝑥 = 𝑁 → ∪
𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘) = ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) | 
| 24 | 23 | fveq2d 6909 | . . . . 5
⊢ (𝑥 = 𝑁 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) = (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) | 
| 25 | 22 | sumeq1d 15737 | . . . . . 6
⊢ (𝑥 = 𝑁 → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) | 
| 26 | 25 | oveq2d 7448 | . . . . 5
⊢ (𝑥 = 𝑁 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) | 
| 27 | 24, 26 | breq12d 5155 | . . . 4
⊢ (𝑥 = 𝑁 → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) | 
| 28 | 27 | imbi2d 340 | . . 3
⊢ (𝑥 = 𝑁 → ((𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))) | 
| 29 |  | 0le0 12368 | . . . . 5
⊢ 0 ≤
0 | 
| 30 |  | prmrec.3 | . . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 31 | 30 | nncnd 12283 | . . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℂ) | 
| 32 | 31 | mul01d 11461 | . . . . 5
⊢ (𝜑 → (𝑁 · 0) = 0) | 
| 33 | 29, 32 | breqtrrid 5180 | . . . 4
⊢ (𝜑 → 0 ≤ (𝑁 · 0)) | 
| 34 |  | prmrec.2 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ ℕ) | 
| 35 | 34 | nnred 12282 | . . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ ℝ) | 
| 36 | 35 | ltp1d 12199 | . . . . . . . . 9
⊢ (𝜑 → 𝐾 < (𝐾 + 1)) | 
| 37 | 34 | nnzd 12642 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ ℤ) | 
| 38 | 37 | peano2zd 12727 | . . . . . . . . . 10
⊢ (𝜑 → (𝐾 + 1) ∈ ℤ) | 
| 39 |  | fzn 13581 | . . . . . . . . . 10
⊢ (((𝐾 + 1) ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐾 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝐾) = ∅)) | 
| 40 | 38, 37, 39 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (𝐾 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝐾) = ∅)) | 
| 41 | 36, 40 | mpbid 232 | . . . . . . . 8
⊢ (𝜑 → ((𝐾 + 1)...𝐾) = ∅) | 
| 42 | 41 | iuneq1d 5018 | . . . . . . 7
⊢ (𝜑 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘) = ∪ 𝑘 ∈ ∅ (𝑊‘𝑘)) | 
| 43 |  | 0iun 5062 | . . . . . . 7
⊢ ∪ 𝑘 ∈ ∅ (𝑊‘𝑘) = ∅ | 
| 44 | 42, 43 | eqtrdi 2792 | . . . . . 6
⊢ (𝜑 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘) = ∅) | 
| 45 | 44 | fveq2d 6909 | . . . . 5
⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) =
(♯‘∅)) | 
| 46 |  | hash0 14407 | . . . . 5
⊢
(♯‘∅) = 0 | 
| 47 | 45, 46 | eqtrdi 2792 | . . . 4
⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) = 0) | 
| 48 | 41 | sumeq1d 15737 | . . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) | 
| 49 |  | sum0 15758 | . . . . . 6
⊢
Σ𝑘 ∈
∅ if(𝑘 ∈
ℙ, (1 / 𝑘), 0) =
0 | 
| 50 | 48, 49 | eqtrdi 2792 | . . . . 5
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0) | 
| 51 | 50 | oveq2d 7448 | . . . 4
⊢ (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · 0)) | 
| 52 | 33, 47, 51 | 3brtr4d 5174 | . . 3
⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) | 
| 53 |  | fzfi 14014 | . . . . . . . . . . 11
⊢
(1...𝑁) ∈
Fin | 
| 54 |  | elfzuz 13561 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ((𝐾 + 1)...𝑗) → 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) | 
| 55 | 34 | peano2nnd 12284 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐾 + 1) ∈ ℕ) | 
| 56 |  | eluznn 12961 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐾 + 1) ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘(𝐾 + 1))) → 𝑘 ∈ ℕ) | 
| 57 | 55, 56 | sylan 580 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → 𝑘 ∈
ℕ) | 
| 58 |  | eleq1 2828 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 = 𝑘 → (𝑝 ∈ ℙ ↔ 𝑘 ∈ ℙ)) | 
| 59 |  | breq1 5145 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 = 𝑘 → (𝑝 ∥ 𝑛 ↔ 𝑘 ∥ 𝑛)) | 
| 60 | 58, 59 | anbi12d 632 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 = 𝑘 → ((𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛))) | 
| 61 | 60 | rabbidv 3443 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 = 𝑘 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)}) | 
| 62 |  | prmrec.7 | . . . . . . . . . . . . . . . . . . 19
⊢ 𝑊 = (𝑝 ∈ ℕ ↦ {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)}) | 
| 63 |  | ovex 7465 | . . . . . . . . . . . . . . . . . . . 20
⊢
(1...𝑁) ∈
V | 
| 64 | 63 | rabex 5338 | . . . . . . . . . . . . . . . . . . 19
⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ∈ V | 
| 65 | 61, 62, 64 | fvmpt 7015 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)}) | 
| 66 | 65 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)}) | 
| 67 |  | ssrab2 4079 | . . . . . . . . . . . . . . . . 17
⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ⊆ (1...𝑁) | 
| 68 | 66, 67 | eqsstrdi 4027 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑊‘𝑘) ⊆ (1...𝑁)) | 
| 69 | 57, 68 | syldan 591 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → (𝑊‘𝑘) ⊆ (1...𝑁)) | 
| 70 | 54, 69 | sylan2 593 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑗)) → (𝑊‘𝑘) ⊆ (1...𝑁)) | 
| 71 | 70 | ralrimiva 3145 | . . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁)) | 
| 72 | 71 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ∀𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁)) | 
| 73 |  | iunss 5044 | . . . . . . . . . . . 12
⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁) ↔ ∀𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁)) | 
| 74 | 72, 73 | sylibr 234 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁)) | 
| 75 |  | ssfi 9214 | . . . . . . . . . . 11
⊢
(((1...𝑁) ∈ Fin
∧ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁)) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∈ Fin) | 
| 76 | 53, 74, 75 | sylancr 587 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∈ Fin) | 
| 77 |  | hashcl 14396 | . . . . . . . . . 10
⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∈ Fin → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ∈
ℕ0) | 
| 78 | 76, 77 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) →
(♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ∈
ℕ0) | 
| 79 | 78 | nn0red 12590 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) →
(♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ∈ ℝ) | 
| 80 | 30 | nnred 12282 | . . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 81 | 80 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝑁 ∈ ℝ) | 
| 82 |  | fzfid 14015 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ((𝐾 + 1)...𝑗) ∈ Fin) | 
| 83 | 55 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝐾 + 1) ∈ ℕ) | 
| 84 | 83, 54, 56 | syl2an 596 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑗)) → 𝑘 ∈ ℕ) | 
| 85 |  | nnrecre 12309 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ) | 
| 86 |  | 0re 11264 | . . . . . . . . . . . 12
⊢ 0 ∈
ℝ | 
| 87 |  | ifcl 4570 | . . . . . . . . . . . 12
⊢ (((1 /
𝑘) ∈ ℝ ∧ 0
∈ ℝ) → if(𝑘
∈ ℙ, (1 / 𝑘), 0)
∈ ℝ) | 
| 88 | 85, 86, 87 | sylancl 586 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈
ℝ) | 
| 89 | 84, 88 | syl 17 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑗)) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ) | 
| 90 | 82, 89 | fsumrecl 15771 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ) | 
| 91 | 81, 90 | remulcld 11292 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ∈ ℝ) | 
| 92 |  | prmnn 16712 | . . . . . . . . . . . 12
⊢ ((𝑗 + 1) ∈ ℙ →
(𝑗 + 1) ∈
ℕ) | 
| 93 | 92 | nnrecred 12318 | . . . . . . . . . . 11
⊢ ((𝑗 + 1) ∈ ℙ → (1 /
(𝑗 + 1)) ∈
ℝ) | 
| 94 | 93 | adantl 481 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (1 / (𝑗 + 1)) ∈
ℝ) | 
| 95 |  | 0red 11265 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → 0
∈ ℝ) | 
| 96 | 94, 95 | ifclda 4560 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) ∈
ℝ) | 
| 97 | 81, 96 | remulcld 11292 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) ∈
ℝ) | 
| 98 | 79, 91, 97 | leadd1d 11858 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) →
((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ ((𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))) | 
| 99 |  | eluzp1p1 12907 | . . . . . . . . . . . . 13
⊢ (𝑗 ∈
(ℤ≥‘𝐾) → (𝑗 + 1) ∈
(ℤ≥‘(𝐾 + 1))) | 
| 100 | 99 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑗 + 1) ∈
(ℤ≥‘(𝐾 + 1))) | 
| 101 |  | simpl 482 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝜑) | 
| 102 |  | elfzuz 13561 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1)) → 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) | 
| 103 | 88 | recnd 11290 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈
ℂ) | 
| 104 | 57, 103 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈
ℂ) | 
| 105 | 101, 102,
104 | syl2an 596 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ) | 
| 106 |  | eleq1 2828 | . . . . . . . . . . . . 13
⊢ (𝑘 = (𝑗 + 1) → (𝑘 ∈ ℙ ↔ (𝑗 + 1) ∈ ℙ)) | 
| 107 |  | oveq2 7440 | . . . . . . . . . . . . 13
⊢ (𝑘 = (𝑗 + 1) → (1 / 𝑘) = (1 / (𝑗 + 1))) | 
| 108 | 106, 107 | ifbieq1d 4549 | . . . . . . . . . . . 12
⊢ (𝑘 = (𝑗 + 1) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) | 
| 109 | 100, 105,
108 | fsumm1 15788 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = (Σ𝑘 ∈ ((𝐾 + 1)...((𝑗 + 1) − 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) | 
| 110 |  | eluzelz 12889 | . . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈
(ℤ≥‘𝐾) → 𝑗 ∈ ℤ) | 
| 111 | 110 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝑗 ∈ ℤ) | 
| 112 | 111 | zcnd 12725 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝑗 ∈ ℂ) | 
| 113 |  | ax-1cn 11214 | . . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ | 
| 114 |  | pncan 11515 | . . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑗 + 1)
− 1) = 𝑗) | 
| 115 | 112, 113,
114 | sylancl 586 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ((𝑗 + 1) − 1) = 𝑗) | 
| 116 | 115 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ((𝐾 + 1)...((𝑗 + 1) − 1)) = ((𝐾 + 1)...𝑗)) | 
| 117 | 116 | sumeq1d 15737 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...((𝑗 + 1) − 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) | 
| 118 | 117 | oveq1d 7447 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (Σ𝑘 ∈ ((𝐾 + 1)...((𝑗 + 1) − 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) | 
| 119 | 109, 118 | eqtrd 2776 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) | 
| 120 | 119 | oveq2d 7448 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))) | 
| 121 | 31 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝑁 ∈ ℂ) | 
| 122 | 90 | recnd 11290 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ) | 
| 123 | 96 | recnd 11290 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) ∈
ℂ) | 
| 124 | 121, 122,
123 | adddid 11286 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑁 · (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) = ((𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))) | 
| 125 | 120, 124 | eqtrd 2776 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = ((𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))) | 
| 126 | 125 | breq2d 5154 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) →
(((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ ((𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))) | 
| 127 | 98, 126 | bitr4d 282 | . . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) →
((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) | 
| 128 | 102, 69 | sylan2 593 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))) → (𝑊‘𝑘) ⊆ (1...𝑁)) | 
| 129 | 128 | ralrimiva 3145 | . . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁)) | 
| 130 | 129 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ∀𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁)) | 
| 131 |  | iunss 5044 | . . . . . . . . . . . 12
⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁) ↔ ∀𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁)) | 
| 132 | 130, 131 | sylibr 234 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁)) | 
| 133 |  | ssfi 9214 | . . . . . . . . . . 11
⊢
(((1...𝑁) ∈ Fin
∧ ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ∈ Fin) | 
| 134 | 53, 132, 133 | sylancr 587 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ∈ Fin) | 
| 135 |  | hashcl 14396 | . . . . . . . . . 10
⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ∈ Fin → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ∈
ℕ0) | 
| 136 | 134, 135 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) →
(♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ∈
ℕ0) | 
| 137 | 136 | nn0red 12590 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) →
(♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ∈ ℝ) | 
| 138 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑗 + 1) → (𝑊‘𝑘) = (𝑊‘(𝑗 + 1))) | 
| 139 | 138 | sseq1d 4014 | . . . . . . . . . . . . 13
⊢ (𝑘 = (𝑗 + 1) → ((𝑊‘𝑘) ⊆ (1...𝑁) ↔ (𝑊‘(𝑗 + 1)) ⊆ (1...𝑁))) | 
| 140 | 68 | ralrimiva 3145 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑊‘𝑘) ⊆ (1...𝑁)) | 
| 141 | 140 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ∀𝑘 ∈ ℕ (𝑊‘𝑘) ⊆ (1...𝑁)) | 
| 142 |  | eluznn 12961 | . . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝐾)) → 𝑗 ∈ ℕ) | 
| 143 | 34, 142 | sylan 580 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝑗 ∈ ℕ) | 
| 144 | 143 | peano2nnd 12284 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑗 + 1) ∈ ℕ) | 
| 145 | 139, 141,
144 | rspcdva 3622 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑊‘(𝑗 + 1)) ⊆ (1...𝑁)) | 
| 146 |  | ssfi 9214 | . . . . . . . . . . . 12
⊢
(((1...𝑁) ∈ Fin
∧ (𝑊‘(𝑗 + 1)) ⊆ (1...𝑁)) → (𝑊‘(𝑗 + 1)) ∈ Fin) | 
| 147 | 53, 145, 146 | sylancr 587 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑊‘(𝑗 + 1)) ∈ Fin) | 
| 148 |  | hashcl 14396 | . . . . . . . . . . 11
⊢ ((𝑊‘(𝑗 + 1)) ∈ Fin →
(♯‘(𝑊‘(𝑗 + 1))) ∈
ℕ0) | 
| 149 | 147, 148 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (♯‘(𝑊‘(𝑗 + 1))) ∈
ℕ0) | 
| 150 | 149 | nn0red 12590 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (♯‘(𝑊‘(𝑗 + 1))) ∈ ℝ) | 
| 151 | 79, 150 | readdcld 11291 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) →
((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))) ∈ ℝ) | 
| 152 | 79, 97 | readdcld 11291 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) →
((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ∈
ℝ) | 
| 153 | 38 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝐾 + 1) ∈ ℤ) | 
| 154 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝑗 ∈ (ℤ≥‘𝐾)) | 
| 155 | 34 | nncnd 12283 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐾 ∈ ℂ) | 
| 156 | 155 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝐾 ∈ ℂ) | 
| 157 |  | pncan 11515 | . . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐾 + 1)
− 1) = 𝐾) | 
| 158 | 156, 113,
157 | sylancl 586 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ((𝐾 + 1) − 1) = 𝐾) | 
| 159 | 158 | fveq2d 6909 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) →
(ℤ≥‘((𝐾 + 1) − 1)) =
(ℤ≥‘𝐾)) | 
| 160 | 154, 159 | eleqtrrd 2843 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝑗 ∈ (ℤ≥‘((𝐾 + 1) −
1))) | 
| 161 |  | fzsuc2 13623 | . . . . . . . . . . . . 13
⊢ (((𝐾 + 1) ∈ ℤ ∧ 𝑗 ∈
(ℤ≥‘((𝐾 + 1) − 1))) → ((𝐾 + 1)...(𝑗 + 1)) = (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})) | 
| 162 | 153, 160,
161 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ((𝐾 + 1)...(𝑗 + 1)) = (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})) | 
| 163 | 162 | iuneq1d 5018 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) = ∪ 𝑘 ∈ (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})(𝑊‘𝑘)) | 
| 164 |  | iunxun 5093 | . . . . . . . . . . . 12
⊢ ∪ 𝑘 ∈ (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})(𝑊‘𝑘) = (∪
𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ ∪
𝑘 ∈ {(𝑗 + 1)} (𝑊‘𝑘)) | 
| 165 |  | ovex 7465 | . . . . . . . . . . . . . 14
⊢ (𝑗 + 1) ∈ V | 
| 166 | 165, 138 | iunxsn 5090 | . . . . . . . . . . . . 13
⊢ ∪ 𝑘 ∈ {(𝑗 + 1)} (𝑊‘𝑘) = (𝑊‘(𝑗 + 1)) | 
| 167 | 166 | uneq2i 4164 | . . . . . . . . . . . 12
⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ ∪
𝑘 ∈ {(𝑗 + 1)} (𝑊‘𝑘)) = (∪
𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1))) | 
| 168 | 164, 167 | eqtri 2764 | . . . . . . . . . . 11
⊢ ∪ 𝑘 ∈ (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})(𝑊‘𝑘) = (∪
𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1))) | 
| 169 | 163, 168 | eqtrdi 2792 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) = (∪
𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1)))) | 
| 170 | 169 | fveq2d 6909 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) →
(♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) = (♯‘(∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1))))) | 
| 171 |  | hashun2 14423 | . . . . . . . . . 10
⊢
((∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∈ Fin ∧ (𝑊‘(𝑗 + 1)) ∈ Fin) →
(♯‘(∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1)))) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (♯‘(𝑊‘(𝑗 + 1))))) | 
| 172 | 76, 147, 171 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) →
(♯‘(∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1)))) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (♯‘(𝑊‘(𝑗 + 1))))) | 
| 173 | 170, 172 | eqbrtrd 5164 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) →
(♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (♯‘(𝑊‘(𝑗 + 1))))) | 
| 174 | 81, 144 | nndivred 12321 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑁 / (𝑗 + 1)) ∈ ℝ) | 
| 175 |  | flle 13840 | . . . . . . . . . . . . . 14
⊢ ((𝑁 / (𝑗 + 1)) ∈ ℝ →
(⌊‘(𝑁 / (𝑗 + 1))) ≤ (𝑁 / (𝑗 + 1))) | 
| 176 | 174, 175 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (⌊‘(𝑁 / (𝑗 + 1))) ≤ (𝑁 / (𝑗 + 1))) | 
| 177 |  | elfznn 13594 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ) | 
| 178 | 177 | nncnd 12283 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ) | 
| 179 | 178 | subid1d 11610 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (1...𝑁) → (𝑛 − 0) = 𝑛) | 
| 180 | 179 | breq2d 5154 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (1...𝑁) → ((𝑗 + 1) ∥ (𝑛 − 0) ↔ (𝑗 + 1) ∥ 𝑛)) | 
| 181 | 180 | rabbiia 3439 | . . . . . . . . . . . . . . 15
⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)} = {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛} | 
| 182 | 181 | fveq2i 6908 | . . . . . . . . . . . . . 14
⊢
(♯‘{𝑛
∈ (1...𝑁) ∣
(𝑗 + 1) ∥ (𝑛 − 0)}) =
(♯‘{𝑛 ∈
(1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) | 
| 183 |  | 1zzd 12650 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 1 ∈
ℤ) | 
| 184 | 30 | nnnn0d 12589 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 185 |  | nn0uz 12921 | . . . . . . . . . . . . . . . . . . 19
⊢
ℕ0 = (ℤ≥‘0) | 
| 186 |  | 1m1e0 12339 | . . . . . . . . . . . . . . . . . . . 20
⊢ (1
− 1) = 0 | 
| 187 | 186 | fveq2i 6908 | . . . . . . . . . . . . . . . . . . 19
⊢
(ℤ≥‘(1 − 1)) =
(ℤ≥‘0) | 
| 188 | 185, 187 | eqtr4i 2767 | . . . . . . . . . . . . . . . . . 18
⊢
ℕ0 = (ℤ≥‘(1 −
1)) | 
| 189 | 184, 188 | eleqtrdi 2850 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(1
− 1))) | 
| 190 | 189 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝑁 ∈ (ℤ≥‘(1
− 1))) | 
| 191 |  | 0zd 12627 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 0 ∈
ℤ) | 
| 192 | 144, 183,
190, 191 | hashdvds 16813 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)}) = ((⌊‘((𝑁 − 0) / (𝑗 + 1))) −
(⌊‘(((1 − 1) − 0) / (𝑗 + 1))))) | 
| 193 | 121 | subid1d 11610 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑁 − 0) = 𝑁) | 
| 194 | 193 | fvoveq1d 7454 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (⌊‘((𝑁 − 0) / (𝑗 + 1))) = (⌊‘(𝑁 / (𝑗 + 1)))) | 
| 195 | 186 | oveq1i 7442 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((1
− 1) − 0) = (0 − 0) | 
| 196 |  | 0m0e0 12387 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (0
− 0) = 0 | 
| 197 | 195, 196 | eqtri 2764 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((1
− 1) − 0) = 0 | 
| 198 | 197 | oveq1i 7442 | . . . . . . . . . . . . . . . . . . 19
⊢ (((1
− 1) − 0) / (𝑗
+ 1)) = (0 / (𝑗 +
1)) | 
| 199 | 144 | nncnd 12283 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑗 + 1) ∈ ℂ) | 
| 200 | 144 | nnne0d 12317 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑗 + 1) ≠ 0) | 
| 201 | 199, 200 | div0d 12043 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (0 / (𝑗 + 1)) = 0) | 
| 202 | 198, 201 | eqtrid 2788 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (((1 − 1)
− 0) / (𝑗 + 1)) =
0) | 
| 203 | 202 | fveq2d 6909 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (⌊‘(((1
− 1) − 0) / (𝑗
+ 1))) = (⌊‘0)) | 
| 204 |  | 0z 12626 | . . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℤ | 
| 205 |  | flid 13849 | . . . . . . . . . . . . . . . . . 18
⊢ (0 ∈
ℤ → (⌊‘0) = 0) | 
| 206 | 204, 205 | ax-mp 5 | . . . . . . . . . . . . . . . . 17
⊢
(⌊‘0) = 0 | 
| 207 | 203, 206 | eqtrdi 2792 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (⌊‘(((1
− 1) − 0) / (𝑗
+ 1))) = 0) | 
| 208 | 194, 207 | oveq12d 7450 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) →
((⌊‘((𝑁 −
0) / (𝑗 + 1))) −
(⌊‘(((1 − 1) − 0) / (𝑗 + 1)))) = ((⌊‘(𝑁 / (𝑗 + 1))) − 0)) | 
| 209 | 174 | flcld 13839 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (⌊‘(𝑁 / (𝑗 + 1))) ∈ ℤ) | 
| 210 | 209 | zcnd 12725 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (⌊‘(𝑁 / (𝑗 + 1))) ∈ ℂ) | 
| 211 | 210 | subid1d 11610 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ((⌊‘(𝑁 / (𝑗 + 1))) − 0) = (⌊‘(𝑁 / (𝑗 + 1)))) | 
| 212 | 192, 208,
211 | 3eqtrd 2780 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)}) = (⌊‘(𝑁 / (𝑗 + 1)))) | 
| 213 | 182, 212 | eqtr3id 2790 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) = (⌊‘(𝑁 / (𝑗 + 1)))) | 
| 214 | 121, 199,
200 | divrecd 12047 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑁 / (𝑗 + 1)) = (𝑁 · (1 / (𝑗 + 1)))) | 
| 215 | 214 | eqcomd 2742 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑁 · (1 / (𝑗 + 1))) = (𝑁 / (𝑗 + 1))) | 
| 216 | 176, 213,
215 | 3brtr4d 5174 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) ≤ (𝑁 · (1 / (𝑗 + 1)))) | 
| 217 | 216 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) →
(♯‘{𝑛 ∈
(1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) ≤ (𝑁 · (1 / (𝑗 + 1)))) | 
| 218 |  | eleq1 2828 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑝 = (𝑗 + 1) → (𝑝 ∈ ℙ ↔ (𝑗 + 1) ∈ ℙ)) | 
| 219 |  | breq1 5145 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑝 = (𝑗 + 1) → (𝑝 ∥ 𝑛 ↔ (𝑗 + 1) ∥ 𝑛)) | 
| 220 | 218, 219 | anbi12d 632 | . . . . . . . . . . . . . . . . 17
⊢ (𝑝 = (𝑗 + 1) → ((𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛) ↔ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛))) | 
| 221 | 220 | rabbidv 3443 | . . . . . . . . . . . . . . . 16
⊢ (𝑝 = (𝑗 + 1) → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)} = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)}) | 
| 222 | 63 | rabex 5338 | . . . . . . . . . . . . . . . 16
⊢ {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)} ∈ V | 
| 223 | 221, 62, 222 | fvmpt 7015 | . . . . . . . . . . . . . . 15
⊢ ((𝑗 + 1) ∈ ℕ →
(𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)}) | 
| 224 | 144, 223 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)}) | 
| 225 | 224 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)}) | 
| 226 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑗 + 1) ∈
ℙ) | 
| 227 | 226 | biantrurd 532 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → ((𝑗 + 1) ∥ 𝑛 ↔ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛))) | 
| 228 | 227 | rabbidv 3443 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛} = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)}) | 
| 229 | 225, 228 | eqtr4d 2779 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) | 
| 230 | 229 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) →
(♯‘(𝑊‘(𝑗 + 1))) = (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛})) | 
| 231 |  | iftrue 4530 | . . . . . . . . . . . . 13
⊢ ((𝑗 + 1) ∈ ℙ →
if((𝑗 + 1) ∈ ℙ,
(1 / (𝑗 + 1)), 0) = (1 /
(𝑗 + 1))) | 
| 232 | 231 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → if((𝑗 + 1) ∈ ℙ, (1 /
(𝑗 + 1)), 0) = (1 / (𝑗 + 1))) | 
| 233 | 232 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) = (𝑁 · (1 / (𝑗 + 1)))) | 
| 234 | 217, 230,
233 | 3brtr4d 5174 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) →
(♯‘(𝑊‘(𝑗 + 1))) ≤ (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) | 
| 235 | 29 | a1i 11 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → 0
≤ 0) | 
| 236 |  | simpl 482 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑗 + 1) ∈ ℙ ∧
(𝑗 + 1) ∥ 𝑛) → (𝑗 + 1) ∈ ℙ) | 
| 237 | 236 | con3i 154 | . . . . . . . . . . . . . . . 16
⊢ (¬
(𝑗 + 1) ∈ ℙ
→ ¬ ((𝑗 + 1)
∈ ℙ ∧ (𝑗 +
1) ∥ 𝑛)) | 
| 238 | 237 | ralrimivw 3149 | . . . . . . . . . . . . . . 15
⊢ (¬
(𝑗 + 1) ∈ ℙ
→ ∀𝑛 ∈
(1...𝑁) ¬ ((𝑗 + 1) ∈ ℙ ∧
(𝑗 + 1) ∥ 𝑛)) | 
| 239 |  | rabeq0 4387 | . . . . . . . . . . . . . . 15
⊢ ({𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)} = ∅ ↔ ∀𝑛 ∈ (1...𝑁) ¬ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)) | 
| 240 | 238, 239 | sylibr 234 | . . . . . . . . . . . . . 14
⊢ (¬
(𝑗 + 1) ∈ ℙ
→ {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)} = ∅) | 
| 241 | 224, 240 | sylan9eq 2796 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) →
(𝑊‘(𝑗 + 1)) =
∅) | 
| 242 | 241 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) →
(♯‘(𝑊‘(𝑗 + 1))) =
(♯‘∅)) | 
| 243 | 242, 46 | eqtrdi 2792 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) →
(♯‘(𝑊‘(𝑗 + 1))) = 0) | 
| 244 |  | iffalse 4533 | . . . . . . . . . . . . 13
⊢ (¬
(𝑗 + 1) ∈ ℙ
→ if((𝑗 + 1) ∈
ℙ, (1 / (𝑗 + 1)), 0)
= 0) | 
| 245 | 244 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (¬
(𝑗 + 1) ∈ ℙ
→ (𝑁 ·
if((𝑗 + 1) ∈ ℙ,
(1 / (𝑗 + 1)), 0)) = (𝑁 · 0)) | 
| 246 | 32 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑁 · 0) = 0) | 
| 247 | 245, 246 | sylan9eqr 2798 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) →
(𝑁 · if((𝑗 + 1) ∈ ℙ, (1 /
(𝑗 + 1)), 0)) =
0) | 
| 248 | 235, 243,
247 | 3brtr4d 5174 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) →
(♯‘(𝑊‘(𝑗 + 1))) ≤ (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) | 
| 249 | 234, 248 | pm2.61dan 812 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (♯‘(𝑊‘(𝑗 + 1))) ≤ (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) | 
| 250 | 150, 97, 79, 249 | leadd2dd 11879 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) →
((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))) | 
| 251 | 137, 151,
152, 173, 250 | letrd 11419 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) →
(♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))) | 
| 252 |  | fzfid 14015 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ((𝐾 + 1)...(𝑗 + 1)) ∈ Fin) | 
| 253 | 57, 88 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈
ℝ) | 
| 254 | 101, 102,
253 | syl2an 596 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ) | 
| 255 | 252, 254 | fsumrecl 15771 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ) | 
| 256 | 81, 255 | remulcld 11292 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ∈ ℝ) | 
| 257 |  | letr 11356 | . . . . . . . 8
⊢
(((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ∈ ℝ ∧
((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ∈ ℝ
∧ (𝑁 ·
Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ∈ ℝ) →
(((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ∧
((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) | 
| 258 | 137, 152,
256, 257 | syl3anc 1372 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) →
(((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ∧
((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) | 
| 259 | 251, 258 | mpand 695 | . . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) →
(((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) | 
| 260 | 127, 259 | sylbid 240 | . . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) →
((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) | 
| 261 | 260 | expcom 413 | . . . 4
⊢ (𝑗 ∈
(ℤ≥‘𝐾) → (𝜑 → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))) | 
| 262 | 261 | a2d 29 | . . 3
⊢ (𝑗 ∈
(ℤ≥‘𝐾) → ((𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) → (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))) | 
| 263 | 7, 14, 21, 28, 52, 262 | uzind4i 12953 | . 2
⊢ (𝑁 ∈
(ℤ≥‘𝐾) → (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) | 
| 264 | 263 | com12 32 | 1
⊢ (𝜑 → (𝑁 ∈ (ℤ≥‘𝐾) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) |