MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prmreclem4 Structured version   Visualization version   GIF version

Theorem prmreclem4 15904
Description: Lemma for prmrec 15907. Show by induction that the indexed (nondisjoint) union 𝑊𝑘 is at most the size of the prime reciprocal series. The key counting lemma is hashdvds 15761, to show that the number of numbers in 1...𝑁 that divide 𝑘 is at most 𝑁 / 𝑘. (Contributed by Mario Carneiro, 6-Aug-2014.)
Hypotheses
Ref Expression
prmrec.1 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0))
prmrec.2 (𝜑𝐾 ∈ ℕ)
prmrec.3 (𝜑𝑁 ∈ ℕ)
prmrec.4 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛}
prmrec.5 (𝜑 → seq1( + , 𝐹) ∈ dom ⇝ )
prmrec.6 (𝜑 → Σ𝑘 ∈ (ℤ‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2))
prmrec.7 𝑊 = (𝑝 ∈ ℕ ↦ {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝𝑛)})
Assertion
Ref Expression
prmreclem4 (𝜑 → (𝑁 ∈ (ℤ𝐾) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
Distinct variable groups:   𝑘,𝑛,𝑝,𝐹   𝑘,𝐾,𝑛,𝑝   𝑘,𝑀,𝑛,𝑝   𝜑,𝑘,𝑛,𝑝   𝑘,𝑊   𝑘,𝑁,𝑛,𝑝
Allowed substitution hints:   𝑊(𝑛,𝑝)

Proof of Theorem prmreclem4
Dummy variables 𝑗 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 6850 . . . . . . 7 (𝑥 = 𝐾 → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...𝐾))
21iuneq1d 4701 . . . . . 6 (𝑥 = 𝐾 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘) = 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊𝑘))
32fveq2d 6379 . . . . 5 (𝑥 = 𝐾 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘)) = (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊𝑘)))
41sumeq1d 14718 . . . . . 6 (𝑥 = 𝐾 → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
54oveq2d 6858 . . . . 5 (𝑥 = 𝐾 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
63, 5breq12d 4822 . . . 4 (𝑥 = 𝐾 → ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
76imbi2d 331 . . 3 (𝑥 = 𝐾 → ((𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
8 oveq2 6850 . . . . . . 7 (𝑥 = 𝑗 → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...𝑗))
98iuneq1d 4701 . . . . . 6 (𝑥 = 𝑗 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘) = 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘))
109fveq2d 6379 . . . . 5 (𝑥 = 𝑗 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘)) = (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)))
118sumeq1d 14718 . . . . . 6 (𝑥 = 𝑗 → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
1211oveq2d 6858 . . . . 5 (𝑥 = 𝑗 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
1310, 12breq12d 4822 . . . 4 (𝑥 = 𝑗 → ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
1413imbi2d 331 . . 3 (𝑥 = 𝑗 → ((𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
15 oveq2 6850 . . . . . . 7 (𝑥 = (𝑗 + 1) → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...(𝑗 + 1)))
1615iuneq1d 4701 . . . . . 6 (𝑥 = (𝑗 + 1) → 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘) = 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘))
1716fveq2d 6379 . . . . 5 (𝑥 = (𝑗 + 1) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘)) = (♯‘ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘)))
1815sumeq1d 14718 . . . . . 6 (𝑥 = (𝑗 + 1) → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
1918oveq2d 6858 . . . . 5 (𝑥 = (𝑗 + 1) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
2017, 19breq12d 4822 . . . 4 (𝑥 = (𝑗 + 1) → ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (♯‘ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
2120imbi2d 331 . . 3 (𝑥 = (𝑗 + 1) → ((𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
22 oveq2 6850 . . . . . . 7 (𝑥 = 𝑁 → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...𝑁))
2322iuneq1d 4701 . . . . . 6 (𝑥 = 𝑁 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘) = 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))
2423fveq2d 6379 . . . . 5 (𝑥 = 𝑁 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘)) = (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
2522sumeq1d 14718 . . . . . 6 (𝑥 = 𝑁 → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
2625oveq2d 6858 . . . . 5 (𝑥 = 𝑁 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
2724, 26breq12d 4822 . . . 4 (𝑥 = 𝑁 → ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
2827imbi2d 331 . . 3 (𝑥 = 𝑁 → ((𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
29 0le0 11380 . . . . . 6 0 ≤ 0
30 prmrec.3 . . . . . . . 8 (𝜑𝑁 ∈ ℕ)
3130nncnd 11292 . . . . . . 7 (𝜑𝑁 ∈ ℂ)
3231mul01d 10489 . . . . . 6 (𝜑 → (𝑁 · 0) = 0)
3329, 32syl5breqr 4847 . . . . 5 (𝜑 → 0 ≤ (𝑁 · 0))
34 prmrec.2 . . . . . . . . . . . 12 (𝜑𝐾 ∈ ℕ)
3534nnred 11291 . . . . . . . . . . 11 (𝜑𝐾 ∈ ℝ)
3635ltp1d 11208 . . . . . . . . . 10 (𝜑𝐾 < (𝐾 + 1))
3734nnzd 11728 . . . . . . . . . . . 12 (𝜑𝐾 ∈ ℤ)
3837peano2zd 11732 . . . . . . . . . . 11 (𝜑 → (𝐾 + 1) ∈ ℤ)
39 fzn 12564 . . . . . . . . . . 11 (((𝐾 + 1) ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐾 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝐾) = ∅))
4038, 37, 39syl2anc 579 . . . . . . . . . 10 (𝜑 → (𝐾 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝐾) = ∅))
4136, 40mpbid 223 . . . . . . . . 9 (𝜑 → ((𝐾 + 1)...𝐾) = ∅)
4241iuneq1d 4701 . . . . . . . 8 (𝜑 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊𝑘) = 𝑘 ∈ ∅ (𝑊𝑘))
43 0iun 4733 . . . . . . . 8 𝑘 ∈ ∅ (𝑊𝑘) = ∅
4442, 43syl6eq 2815 . . . . . . 7 (𝜑 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊𝑘) = ∅)
4544fveq2d 6379 . . . . . 6 (𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊𝑘)) = (♯‘∅))
46 hash0 13360 . . . . . 6 (♯‘∅) = 0
4745, 46syl6eq 2815 . . . . 5 (𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊𝑘)) = 0)
4841sumeq1d 14718 . . . . . . 7 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
49 sum0 14739 . . . . . . 7 Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0
5048, 49syl6eq 2815 . . . . . 6 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0)
5150oveq2d 6858 . . . . 5 (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · 0))
5233, 47, 513brtr4d 4841 . . . 4 (𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
5352a1i 11 . . 3 (𝐾 ∈ ℤ → (𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
54 fzfi 12979 . . . . . . . . . . 11 (1...𝑁) ∈ Fin
55 elfzuz 12545 . . . . . . . . . . . . . . 15 (𝑘 ∈ ((𝐾 + 1)...𝑗) → 𝑘 ∈ (ℤ‘(𝐾 + 1)))
5634peano2nnd 11293 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐾 + 1) ∈ ℕ)
57 eluznn 11959 . . . . . . . . . . . . . . . . 17 (((𝐾 + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ‘(𝐾 + 1))) → 𝑘 ∈ ℕ)
5856, 57sylan 575 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (ℤ‘(𝐾 + 1))) → 𝑘 ∈ ℕ)
59 eleq1 2832 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 = 𝑘 → (𝑝 ∈ ℙ ↔ 𝑘 ∈ ℙ))
60 breq1 4812 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 = 𝑘 → (𝑝𝑛𝑘𝑛))
6159, 60anbi12d 624 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = 𝑘 → ((𝑝 ∈ ℙ ∧ 𝑝𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘𝑛)))
6261rabbidv 3338 . . . . . . . . . . . . . . . . . . 19 (𝑝 = 𝑘 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)})
63 prmrec.7 . . . . . . . . . . . . . . . . . . 19 𝑊 = (𝑝 ∈ ℕ ↦ {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝𝑛)})
64 ovex 6874 . . . . . . . . . . . . . . . . . . . 20 (1...𝑁) ∈ V
6564rabex 4973 . . . . . . . . . . . . . . . . . . 19 {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)} ∈ V
6662, 63, 65fvmpt 6471 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ → (𝑊𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)})
6766adantl 473 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → (𝑊𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)})
68 ssrab2 3847 . . . . . . . . . . . . . . . . 17 {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)} ⊆ (1...𝑁)
6967, 68syl6eqss 3815 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (𝑊𝑘) ⊆ (1...𝑁))
7058, 69syldan 585 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (ℤ‘(𝐾 + 1))) → (𝑊𝑘) ⊆ (1...𝑁))
7155, 70sylan2 586 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑗)) → (𝑊𝑘) ⊆ (1...𝑁))
7271ralrimiva 3113 . . . . . . . . . . . . 13 (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ⊆ (1...𝑁))
7372adantr 472 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝐾)) → ∀𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ⊆ (1...𝑁))
74 iunss 4717 . . . . . . . . . . . 12 ( 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ⊆ (1...𝑁) ↔ ∀𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ⊆ (1...𝑁))
7573, 74sylibr 225 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ⊆ (1...𝑁))
76 ssfi 8387 . . . . . . . . . . 11 (((1...𝑁) ∈ Fin ∧ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ⊆ (1...𝑁)) → 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ∈ Fin)
7754, 75, 76sylancr 581 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ∈ Fin)
78 hashcl 13349 . . . . . . . . . 10 ( 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ∈ Fin → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) ∈ ℕ0)
7977, 78syl 17 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) ∈ ℕ0)
8079nn0red 11599 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) ∈ ℝ)
8130nnred 11291 . . . . . . . . . 10 (𝜑𝑁 ∈ ℝ)
8281adantr 472 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑁 ∈ ℝ)
83 fzfid 12980 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((𝐾 + 1)...𝑗) ∈ Fin)
8456adantr 472 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝐾 + 1) ∈ ℕ)
8584, 55, 57syl2an 589 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑗)) → 𝑘 ∈ ℕ)
86 nnrecre 11314 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
87 0re 10295 . . . . . . . . . . . 12 0 ∈ ℝ
88 ifcl 4287 . . . . . . . . . . . 12 (((1 / 𝑘) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
8986, 87, 88sylancl 580 . . . . . . . . . . 11 (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
9085, 89syl 17 . . . . . . . . . 10 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑗)) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
9183, 90fsumrecl 14752 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
9282, 91remulcld 10324 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ∈ ℝ)
93 prmnn 15670 . . . . . . . . . . . 12 ((𝑗 + 1) ∈ ℙ → (𝑗 + 1) ∈ ℕ)
94 nnrecre 11314 . . . . . . . . . . . 12 ((𝑗 + 1) ∈ ℕ → (1 / (𝑗 + 1)) ∈ ℝ)
9593, 94syl 17 . . . . . . . . . . 11 ((𝑗 + 1) ∈ ℙ → (1 / (𝑗 + 1)) ∈ ℝ)
9695adantl 473 . . . . . . . . . 10 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (1 / (𝑗 + 1)) ∈ ℝ)
97 0red 10297 . . . . . . . . . 10 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → 0 ∈ ℝ)
9896, 97ifclda 4277 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝐾)) → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) ∈ ℝ)
9982, 98remulcld 10324 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) ∈ ℝ)
10080, 92, 99leadd1d 10875 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ ((𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))))
101 eluzp1p1 11912 . . . . . . . . . . . . 13 (𝑗 ∈ (ℤ𝐾) → (𝑗 + 1) ∈ (ℤ‘(𝐾 + 1)))
102101adantl 473 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑗 + 1) ∈ (ℤ‘(𝐾 + 1)))
103 simpl 474 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝜑)
104 elfzuz 12545 . . . . . . . . . . . . 13 (𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1)) → 𝑘 ∈ (ℤ‘(𝐾 + 1)))
10589recnd 10322 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
10658, 105syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (ℤ‘(𝐾 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
107103, 104, 106syl2an 589 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
108 eleq1 2832 . . . . . . . . . . . . 13 (𝑘 = (𝑗 + 1) → (𝑘 ∈ ℙ ↔ (𝑗 + 1) ∈ ℙ))
109 oveq2 6850 . . . . . . . . . . . . 13 (𝑘 = (𝑗 + 1) → (1 / 𝑘) = (1 / (𝑗 + 1)))
110108, 109ifbieq1d 4266 . . . . . . . . . . . 12 (𝑘 = (𝑗 + 1) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))
111102, 107, 110fsumm1 14767 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = (Σ𝑘 ∈ ((𝐾 + 1)...((𝑗 + 1) − 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
112 eluzelz 11896 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (ℤ𝐾) → 𝑗 ∈ ℤ)
113112adantl 473 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑗 ∈ ℤ)
114113zcnd 11730 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑗 ∈ ℂ)
115 ax-1cn 10247 . . . . . . . . . . . . . . 15 1 ∈ ℂ
116 pncan 10541 . . . . . . . . . . . . . . 15 ((𝑗 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑗 + 1) − 1) = 𝑗)
117114, 115, 116sylancl 580 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((𝑗 + 1) − 1) = 𝑗)
118117oveq2d 6858 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((𝐾 + 1)...((𝑗 + 1) − 1)) = ((𝐾 + 1)...𝑗))
119118sumeq1d 14718 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...((𝑗 + 1) − 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
120119oveq1d 6857 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝐾)) → (Σ𝑘 ∈ ((𝐾 + 1)...((𝑗 + 1) − 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
121111, 120eqtrd 2799 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
122121oveq2d 6858 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
12331adantr 472 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑁 ∈ ℂ)
12491recnd 10322 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
12598recnd 10322 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝐾)) → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) ∈ ℂ)
126123, 124, 125adddid 10318 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑁 · (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) = ((𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
127122, 126eqtrd 2799 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = ((𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
128127breq2d 4821 . . . . . . 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)))))
129100, 128bitr4d 273 . . . . . 6 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
130104, 70sylan2 586 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))) → (𝑊𝑘) ⊆ (1...𝑁))
131130ralrimiva 3113 . . . . . . . . . . . . 13 (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘) ⊆ (1...𝑁))
132131adantr 472 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝐾)) → ∀𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘) ⊆ (1...𝑁))
133 iunss 4717 . . . . . . . . . . . 12 ( 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘) ⊆ (1...𝑁) ↔ ∀𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘) ⊆ (1...𝑁))
134132, 133sylibr 225 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘) ⊆ (1...𝑁))
135 ssfi 8387 . . . . . . . . . . 11 (((1...𝑁) ∈ Fin ∧ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘) ⊆ (1...𝑁)) → 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘) ∈ Fin)
13654, 134, 135sylancr 581 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘) ∈ Fin)
137 hashcl 13349 . . . . . . . . . 10 ( 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘) ∈ Fin → (♯‘ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘)) ∈ ℕ0)
138136, 137syl 17 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘)) ∈ ℕ0)
139138nn0red 11599 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘)) ∈ ℝ)
140 fveq2 6375 . . . . . . . . . . . . . 14 (𝑘 = (𝑗 + 1) → (𝑊𝑘) = (𝑊‘(𝑗 + 1)))
141140sseq1d 3792 . . . . . . . . . . . . 13 (𝑘 = (𝑗 + 1) → ((𝑊𝑘) ⊆ (1...𝑁) ↔ (𝑊‘(𝑗 + 1)) ⊆ (1...𝑁)))
14269ralrimiva 3113 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑘 ∈ ℕ (𝑊𝑘) ⊆ (1...𝑁))
143142adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝐾)) → ∀𝑘 ∈ ℕ (𝑊𝑘) ⊆ (1...𝑁))
144 eluznn 11959 . . . . . . . . . . . . . . 15 ((𝐾 ∈ ℕ ∧ 𝑗 ∈ (ℤ𝐾)) → 𝑗 ∈ ℕ)
14534, 144sylan 575 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑗 ∈ ℕ)
146145peano2nnd 11293 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑗 + 1) ∈ ℕ)
147141, 143, 146rspcdva 3467 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑊‘(𝑗 + 1)) ⊆ (1...𝑁))
148 ssfi 8387 . . . . . . . . . . . 12 (((1...𝑁) ∈ Fin ∧ (𝑊‘(𝑗 + 1)) ⊆ (1...𝑁)) → (𝑊‘(𝑗 + 1)) ∈ Fin)
14954, 147, 148sylancr 581 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑊‘(𝑗 + 1)) ∈ Fin)
150 hashcl 13349 . . . . . . . . . . 11 ((𝑊‘(𝑗 + 1)) ∈ Fin → (♯‘(𝑊‘(𝑗 + 1))) ∈ ℕ0)
151149, 150syl 17 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘(𝑊‘(𝑗 + 1))) ∈ ℕ0)
152151nn0red 11599 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘(𝑊‘(𝑗 + 1))) ∈ ℝ)
15380, 152readdcld 10323 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))) ∈ ℝ)
15480, 99readdcld 10323 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ∈ ℝ)
15538adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝐾 + 1) ∈ ℤ)
156 simpr 477 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑗 ∈ (ℤ𝐾))
15734nncnd 11292 . . . . . . . . . . . . . . . . 17 (𝜑𝐾 ∈ ℂ)
158157adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝐾 ∈ ℂ)
159 pncan 10541 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐾 + 1) − 1) = 𝐾)
160158, 115, 159sylancl 580 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((𝐾 + 1) − 1) = 𝐾)
161160fveq2d 6379 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ𝐾)) → (ℤ‘((𝐾 + 1) − 1)) = (ℤ𝐾))
162156, 161eleqtrrd 2847 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑗 ∈ (ℤ‘((𝐾 + 1) − 1)))
163 fzsuc2 12605 . . . . . . . . . . . . 13 (((𝐾 + 1) ∈ ℤ ∧ 𝑗 ∈ (ℤ‘((𝐾 + 1) − 1))) → ((𝐾 + 1)...(𝑗 + 1)) = (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)}))
164155, 162, 163syl2anc 579 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((𝐾 + 1)...(𝑗 + 1)) = (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)}))
165164iuneq1d 4701 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘) = 𝑘 ∈ (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})(𝑊𝑘))
166 iunxun 4762 . . . . . . . . . . . 12 𝑘 ∈ (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})(𝑊𝑘) = ( 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ∪ 𝑘 ∈ {(𝑗 + 1)} (𝑊𝑘))
167 ovex 6874 . . . . . . . . . . . . . 14 (𝑗 + 1) ∈ V
168167, 140iunxsn 4759 . . . . . . . . . . . . 13 𝑘 ∈ {(𝑗 + 1)} (𝑊𝑘) = (𝑊‘(𝑗 + 1))
169168uneq2i 3926 . . . . . . . . . . . 12 ( 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ∪ 𝑘 ∈ {(𝑗 + 1)} (𝑊𝑘)) = ( 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ∪ (𝑊‘(𝑗 + 1)))
170166, 169eqtri 2787 . . . . . . . . . . 11 𝑘 ∈ (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})(𝑊𝑘) = ( 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ∪ (𝑊‘(𝑗 + 1)))
171165, 170syl6eq 2815 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘) = ( 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ∪ (𝑊‘(𝑗 + 1))))
172171fveq2d 6379 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘)) = (♯‘( 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ∪ (𝑊‘(𝑗 + 1)))))
173 hashun2 13374 . . . . . . . . . 10 (( 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ∈ Fin ∧ (𝑊‘(𝑗 + 1)) ∈ Fin) → (♯‘( 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ∪ (𝑊‘(𝑗 + 1)))) ≤ ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))))
17477, 149, 173syl2anc 579 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘( 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ∪ (𝑊‘(𝑗 + 1)))) ≤ ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))))
175172, 174eqbrtrd 4831 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘)) ≤ ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))))
17682, 146nndivred 11326 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑁 / (𝑗 + 1)) ∈ ℝ)
177 flle 12808 . . . . . . . . . . . . . 14 ((𝑁 / (𝑗 + 1)) ∈ ℝ → (⌊‘(𝑁 / (𝑗 + 1))) ≤ (𝑁 / (𝑗 + 1)))
178176, 177syl 17 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝐾)) → (⌊‘(𝑁 / (𝑗 + 1))) ≤ (𝑁 / (𝑗 + 1)))
179 elfznn 12577 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ)
180179nncnd 11292 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ)
181180subid1d 10635 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (1...𝑁) → (𝑛 − 0) = 𝑛)
182181breq2d 4821 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (1...𝑁) → ((𝑗 + 1) ∥ (𝑛 − 0) ↔ (𝑗 + 1) ∥ 𝑛))
183182rabbiia 3333 . . . . . . . . . . . . . . 15 {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)} = {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}
184183fveq2i 6378 . . . . . . . . . . . . . 14 (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)}) = (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛})
185 1zzd 11655 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (ℤ𝐾)) → 1 ∈ ℤ)
18630nnnn0d 11598 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ ℕ0)
187 nn0uz 11922 . . . . . . . . . . . . . . . . . . 19 0 = (ℤ‘0)
188 1m1e0 11344 . . . . . . . . . . . . . . . . . . . 20 (1 − 1) = 0
189188fveq2i 6378 . . . . . . . . . . . . . . . . . . 19 (ℤ‘(1 − 1)) = (ℤ‘0)
190187, 189eqtr4i 2790 . . . . . . . . . . . . . . . . . 18 0 = (ℤ‘(1 − 1))
191186, 190syl6eleq 2854 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ (ℤ‘(1 − 1)))
192191adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑁 ∈ (ℤ‘(1 − 1)))
193 0zd 11636 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (ℤ𝐾)) → 0 ∈ ℤ)
194146, 185, 192, 193hashdvds 15761 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)}) = ((⌊‘((𝑁 − 0) / (𝑗 + 1))) − (⌊‘(((1 − 1) − 0) / (𝑗 + 1)))))
195123subid1d 10635 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑁 − 0) = 𝑁)
196195fvoveq1d 6864 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (ℤ𝐾)) → (⌊‘((𝑁 − 0) / (𝑗 + 1))) = (⌊‘(𝑁 / (𝑗 + 1))))
197188oveq1i 6852 . . . . . . . . . . . . . . . . . . . . 21 ((1 − 1) − 0) = (0 − 0)
198 0m0e0 11399 . . . . . . . . . . . . . . . . . . . . 21 (0 − 0) = 0
199197, 198eqtri 2787 . . . . . . . . . . . . . . . . . . . 20 ((1 − 1) − 0) = 0
200199oveq1i 6852 . . . . . . . . . . . . . . . . . . 19 (((1 − 1) − 0) / (𝑗 + 1)) = (0 / (𝑗 + 1))
201146nncnd 11292 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑗 + 1) ∈ ℂ)
202146nnne0d 11322 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑗 + 1) ≠ 0)
203201, 202div0d 11054 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (ℤ𝐾)) → (0 / (𝑗 + 1)) = 0)
204200, 203syl5eq 2811 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (ℤ𝐾)) → (((1 − 1) − 0) / (𝑗 + 1)) = 0)
205204fveq2d 6379 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (ℤ𝐾)) → (⌊‘(((1 − 1) − 0) / (𝑗 + 1))) = (⌊‘0))
206 0z 11635 . . . . . . . . . . . . . . . . . 18 0 ∈ ℤ
207 flid 12817 . . . . . . . . . . . . . . . . . 18 (0 ∈ ℤ → (⌊‘0) = 0)
208206, 207ax-mp 5 . . . . . . . . . . . . . . . . 17 (⌊‘0) = 0
209205, 208syl6eq 2815 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (ℤ𝐾)) → (⌊‘(((1 − 1) − 0) / (𝑗 + 1))) = 0)
210196, 209oveq12d 6860 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((⌊‘((𝑁 − 0) / (𝑗 + 1))) − (⌊‘(((1 − 1) − 0) / (𝑗 + 1)))) = ((⌊‘(𝑁 / (𝑗 + 1))) − 0))
211176flcld 12807 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (ℤ𝐾)) → (⌊‘(𝑁 / (𝑗 + 1))) ∈ ℤ)
212211zcnd 11730 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (ℤ𝐾)) → (⌊‘(𝑁 / (𝑗 + 1))) ∈ ℂ)
213212subid1d 10635 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((⌊‘(𝑁 / (𝑗 + 1))) − 0) = (⌊‘(𝑁 / (𝑗 + 1))))
214194, 210, 2133eqtrd 2803 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)}) = (⌊‘(𝑁 / (𝑗 + 1))))
215184, 214syl5eqr 2813 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) = (⌊‘(𝑁 / (𝑗 + 1))))
216123, 201, 202divrecd 11058 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑁 / (𝑗 + 1)) = (𝑁 · (1 / (𝑗 + 1))))
217216eqcomd 2771 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑁 · (1 / (𝑗 + 1))) = (𝑁 / (𝑗 + 1)))
218178, 215, 2173brtr4d 4841 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) ≤ (𝑁 · (1 / (𝑗 + 1))))
219218adantr 472 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) ≤ (𝑁 · (1 / (𝑗 + 1))))
220 eleq1 2832 . . . . . . . . . . . . . . . . . 18 (𝑝 = (𝑗 + 1) → (𝑝 ∈ ℙ ↔ (𝑗 + 1) ∈ ℙ))
221 breq1 4812 . . . . . . . . . . . . . . . . . 18 (𝑝 = (𝑗 + 1) → (𝑝𝑛 ↔ (𝑗 + 1) ∥ 𝑛))
222220, 221anbi12d 624 . . . . . . . . . . . . . . . . 17 (𝑝 = (𝑗 + 1) → ((𝑝 ∈ ℙ ∧ 𝑝𝑛) ↔ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)))
223222rabbidv 3338 . . . . . . . . . . . . . . . 16 (𝑝 = (𝑗 + 1) → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝𝑛)} = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)})
22464rabex 4973 . . . . . . . . . . . . . . . 16 {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)} ∈ V
225223, 63, 224fvmpt 6471 . . . . . . . . . . . . . . 15 ((𝑗 + 1) ∈ ℕ → (𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)})
226146, 225syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)})
227226adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)})
228 simpr 477 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑗 + 1) ∈ ℙ)
229228biantrurd 528 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → ((𝑗 + 1) ∥ 𝑛 ↔ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)))
230229rabbidv 3338 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛} = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)})
231227, 230eqtr4d 2802 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛})
232231fveq2d 6379 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) = (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}))
233 iftrue 4249 . . . . . . . . . . . . 13 ((𝑗 + 1) ∈ ℙ → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) = (1 / (𝑗 + 1)))
234233adantl 473 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) = (1 / (𝑗 + 1)))
235234oveq2d 6858 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) = (𝑁 · (1 / (𝑗 + 1))))
236219, 232, 2353brtr4d 4841 . . . . . . . . . 10 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) ≤ (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
23729a1i 11 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → 0 ≤ 0)
238 simpl 474 . . . . . . . . . . . . . . . . 17 (((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛) → (𝑗 + 1) ∈ ℙ)
239238con3i 151 . . . . . . . . . . . . . . . 16 (¬ (𝑗 + 1) ∈ ℙ → ¬ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛))
240239ralrimivw 3114 . . . . . . . . . . . . . . 15 (¬ (𝑗 + 1) ∈ ℙ → ∀𝑛 ∈ (1...𝑁) ¬ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛))
241 rabeq0 4121 . . . . . . . . . . . . . . 15 ({𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)} = ∅ ↔ ∀𝑛 ∈ (1...𝑁) ¬ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛))
242240, 241sylibr 225 . . . . . . . . . . . . . 14 (¬ (𝑗 + 1) ∈ ℙ → {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)} = ∅)
243226, 242sylan9eq 2819 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (𝑊‘(𝑗 + 1)) = ∅)
244243fveq2d 6379 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) = (♯‘∅))
245244, 46syl6eq 2815 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) = 0)
246 iffalse 4252 . . . . . . . . . . . . 13 (¬ (𝑗 + 1) ∈ ℙ → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) = 0)
247246oveq2d 6858 . . . . . . . . . . . 12 (¬ (𝑗 + 1) ∈ ℙ → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) = (𝑁 · 0))
24832adantr 472 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑁 · 0) = 0)
249247, 248sylan9eqr 2821 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) = 0)
250237, 245, 2493brtr4d 4841 . . . . . . . . . 10 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) ≤ (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
251236, 250pm2.61dan 847 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘(𝑊‘(𝑗 + 1))) ≤ (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
252152, 99, 80, 251leadd2dd 10896 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))) ≤ ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
253139, 153, 154, 175, 252letrd 10448 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘)) ≤ ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
254 fzfid 12980 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((𝐾 + 1)...(𝑗 + 1)) ∈ Fin)
25558, 89syl 17 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ℤ‘(𝐾 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
256103, 104, 255syl2an 589 . . . . . . . . . 10 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
257254, 256fsumrecl 14752 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
25882, 257remulcld 10324 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ∈ ℝ)
259 letr 10385 . . . . . . . 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))))
260139, 154, 258, 259syl3anc 1490 . . . . . . 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))))
261253, 260mpand 686 . . . . . 6 ((𝜑𝑗 ∈ (ℤ𝐾)) → (((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
262129, 261sylbid 231 . . . . 5 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
263262expcom 402 . . . 4 (𝑗 ∈ (ℤ𝐾) → (𝜑 → ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
264263a2d 29 . . 3 (𝑗 ∈ (ℤ𝐾) → ((𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) → (𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
2657, 14, 21, 28, 53, 264uzind4 11946 . 2 (𝑁 ∈ (ℤ𝐾) → (𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
266265com12 32 1 (𝜑 → (𝑁 ∈ (ℤ𝐾) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  wral 3055  {crab 3059  cdif 3729  cun 3730  wss 3732  c0 4079  ifcif 4243  {csn 4334   ciun 4676   class class class wbr 4809  cmpt 4888  dom cdm 5277  cfv 6068  (class class class)co 6842  Fincfn 8160  cc 10187  cr 10188  0cc0 10189  1c1 10190   + caddc 10192   · cmul 10194   < clt 10328  cle 10329  cmin 10520   / cdiv 10938  cn 11274  2c2 11327  0cn0 11538  cz 11624  cuz 11886  ...cfz 12533  cfl 12799  seqcseq 13008  chash 13321  cli 14502  Σcsu 14703  cdvds 15267  cprime 15667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-inf2 8753  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-isom 6077  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-oadd 7768  df-er 7947  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-sup 8555  df-inf 8556  df-oi 8622  df-card 9016  df-cda 9243  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-n0 11539  df-xnn0 11611  df-z 11625  df-uz 11887  df-rp 12029  df-fz 12534  df-fzo 12674  df-fl 12801  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14126  df-re 14127  df-im 14128  df-sqrt 14262  df-abs 14263  df-clim 14506  df-sum 14704  df-dvds 15268  df-prm 15668
This theorem is referenced by:  prmreclem5  15905
  Copyright terms: Public domain W3C validator