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

Theorem prmreclem4 16848
Description: Lemma for prmrec 16851. Show by induction that the indexed (nondisjoint) union 𝑊𝑘 is at most the size of the prime reciprocal series. The key counting lemma is hashdvds 16704, 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 7412 . . . . . . 7 (𝑥 = 𝐾 → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...𝐾))
21iuneq1d 5023 . . . . . 6 (𝑥 = 𝐾 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘) = 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊𝑘))
32fveq2d 6892 . . . . 5 (𝑥 = 𝐾 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘)) = (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊𝑘)))
41sumeq1d 15643 . . . . . 6 (𝑥 = 𝐾 → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
54oveq2d 7420 . . . . 5 (𝑥 = 𝐾 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
63, 5breq12d 5160 . . . 4 (𝑥 = 𝐾 → ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
76imbi2d 341 . . 3 (𝑥 = 𝐾 → ((𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
8 oveq2 7412 . . . . . . 7 (𝑥 = 𝑗 → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...𝑗))
98iuneq1d 5023 . . . . . 6 (𝑥 = 𝑗 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘) = 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘))
109fveq2d 6892 . . . . 5 (𝑥 = 𝑗 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘)) = (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)))
118sumeq1d 15643 . . . . . 6 (𝑥 = 𝑗 → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
1211oveq2d 7420 . . . . 5 (𝑥 = 𝑗 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
1310, 12breq12d 5160 . . . 4 (𝑥 = 𝑗 → ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
1413imbi2d 341 . . 3 (𝑥 = 𝑗 → ((𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
15 oveq2 7412 . . . . . . 7 (𝑥 = (𝑗 + 1) → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...(𝑗 + 1)))
1615iuneq1d 5023 . . . . . 6 (𝑥 = (𝑗 + 1) → 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘) = 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘))
1716fveq2d 6892 . . . . 5 (𝑥 = (𝑗 + 1) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘)) = (♯‘ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘)))
1815sumeq1d 15643 . . . . . 6 (𝑥 = (𝑗 + 1) → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
1918oveq2d 7420 . . . . 5 (𝑥 = (𝑗 + 1) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
2017, 19breq12d 5160 . . . 4 (𝑥 = (𝑗 + 1) → ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (♯‘ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
2120imbi2d 341 . . 3 (𝑥 = (𝑗 + 1) → ((𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
22 oveq2 7412 . . . . . . 7 (𝑥 = 𝑁 → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...𝑁))
2322iuneq1d 5023 . . . . . 6 (𝑥 = 𝑁 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘) = 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))
2423fveq2d 6892 . . . . 5 (𝑥 = 𝑁 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘)) = (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
2522sumeq1d 15643 . . . . . 6 (𝑥 = 𝑁 → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
2625oveq2d 7420 . . . . 5 (𝑥 = 𝑁 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
2724, 26breq12d 5160 . . . 4 (𝑥 = 𝑁 → ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
2827imbi2d 341 . . 3 (𝑥 = 𝑁 → ((𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
29 0le0 12309 . . . . 5 0 ≤ 0
30 prmrec.3 . . . . . . 7 (𝜑𝑁 ∈ ℕ)
3130nncnd 12224 . . . . . 6 (𝜑𝑁 ∈ ℂ)
3231mul01d 11409 . . . . 5 (𝜑 → (𝑁 · 0) = 0)
3329, 32breqtrrid 5185 . . . 4 (𝜑 → 0 ≤ (𝑁 · 0))
34 prmrec.2 . . . . . . . . . . 11 (𝜑𝐾 ∈ ℕ)
3534nnred 12223 . . . . . . . . . 10 (𝜑𝐾 ∈ ℝ)
3635ltp1d 12140 . . . . . . . . 9 (𝜑𝐾 < (𝐾 + 1))
3734nnzd 12581 . . . . . . . . . . 11 (𝜑𝐾 ∈ ℤ)
3837peano2zd 12665 . . . . . . . . . 10 (𝜑 → (𝐾 + 1) ∈ ℤ)
39 fzn 13513 . . . . . . . . . 10 (((𝐾 + 1) ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐾 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝐾) = ∅))
4038, 37, 39syl2anc 585 . . . . . . . . 9 (𝜑 → (𝐾 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝐾) = ∅))
4136, 40mpbid 231 . . . . . . . 8 (𝜑 → ((𝐾 + 1)...𝐾) = ∅)
4241iuneq1d 5023 . . . . . . 7 (𝜑 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊𝑘) = 𝑘 ∈ ∅ (𝑊𝑘))
43 0iun 5065 . . . . . . 7 𝑘 ∈ ∅ (𝑊𝑘) = ∅
4442, 43eqtrdi 2789 . . . . . 6 (𝜑 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊𝑘) = ∅)
4544fveq2d 6892 . . . . 5 (𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊𝑘)) = (♯‘∅))
46 hash0 14323 . . . . 5 (♯‘∅) = 0
4745, 46eqtrdi 2789 . . . 4 (𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊𝑘)) = 0)
4841sumeq1d 15643 . . . . . 6 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
49 sum0 15663 . . . . . 6 Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0
5048, 49eqtrdi 2789 . . . . 5 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0)
5150oveq2d 7420 . . . 4 (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · 0))
5233, 47, 513brtr4d 5179 . . 3 (𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
53 fzfi 13933 . . . . . . . . . . 11 (1...𝑁) ∈ Fin
54 elfzuz 13493 . . . . . . . . . . . . . . 15 (𝑘 ∈ ((𝐾 + 1)...𝑗) → 𝑘 ∈ (ℤ‘(𝐾 + 1)))
5534peano2nnd 12225 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐾 + 1) ∈ ℕ)
56 eluznn 12898 . . . . . . . . . . . . . . . . 17 (((𝐾 + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ‘(𝐾 + 1))) → 𝑘 ∈ ℕ)
5755, 56sylan 581 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (ℤ‘(𝐾 + 1))) → 𝑘 ∈ ℕ)
58 eleq1 2822 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 = 𝑘 → (𝑝 ∈ ℙ ↔ 𝑘 ∈ ℙ))
59 breq1 5150 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 = 𝑘 → (𝑝𝑛𝑘𝑛))
6058, 59anbi12d 632 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = 𝑘 → ((𝑝 ∈ ℙ ∧ 𝑝𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘𝑛)))
6160rabbidv 3441 . . . . . . . . . . . . . . . . . . 19 (𝑝 = 𝑘 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)})
62 prmrec.7 . . . . . . . . . . . . . . . . . . 19 𝑊 = (𝑝 ∈ ℕ ↦ {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝𝑛)})
63 ovex 7437 . . . . . . . . . . . . . . . . . . . 20 (1...𝑁) ∈ V
6463rabex 5331 . . . . . . . . . . . . . . . . . . 19 {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)} ∈ V
6561, 62, 64fvmpt 6994 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ → (𝑊𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)})
6665adantl 483 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ ℕ) → (𝑊𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)})
67 ssrab2 4076 . . . . . . . . . . . . . . . . 17 {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)} ⊆ (1...𝑁)
6866, 67eqsstrdi 4035 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ℕ) → (𝑊𝑘) ⊆ (1...𝑁))
6957, 68syldan 592 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (ℤ‘(𝐾 + 1))) → (𝑊𝑘) ⊆ (1...𝑁))
7054, 69sylan2 594 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑗)) → (𝑊𝑘) ⊆ (1...𝑁))
7170ralrimiva 3147 . . . . . . . . . . . . 13 (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ⊆ (1...𝑁))
7271adantr 482 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝐾)) → ∀𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ⊆ (1...𝑁))
73 iunss 5047 . . . . . . . . . . . 12 ( 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ⊆ (1...𝑁) ↔ ∀𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ⊆ (1...𝑁))
7472, 73sylibr 233 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ⊆ (1...𝑁))
75 ssfi 9169 . . . . . . . . . . 11 (((1...𝑁) ∈ Fin ∧ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ⊆ (1...𝑁)) → 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ∈ Fin)
7653, 74, 75sylancr 588 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ∈ Fin)
77 hashcl 14312 . . . . . . . . . 10 ( 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ∈ Fin → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) ∈ ℕ0)
7876, 77syl 17 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) ∈ ℕ0)
7978nn0red 12529 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) ∈ ℝ)
8030nnred 12223 . . . . . . . . . 10 (𝜑𝑁 ∈ ℝ)
8180adantr 482 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑁 ∈ ℝ)
82 fzfid 13934 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((𝐾 + 1)...𝑗) ∈ Fin)
8355adantr 482 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝐾 + 1) ∈ ℕ)
8483, 54, 56syl2an 597 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑗)) → 𝑘 ∈ ℕ)
85 nnrecre 12250 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
86 0re 11212 . . . . . . . . . . . 12 0 ∈ ℝ
87 ifcl 4572 . . . . . . . . . . . 12 (((1 / 𝑘) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
8885, 86, 87sylancl 587 . . . . . . . . . . 11 (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
8984, 88syl 17 . . . . . . . . . 10 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑗)) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
9082, 89fsumrecl 15676 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
9181, 90remulcld 11240 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ∈ ℝ)
92 prmnn 16607 . . . . . . . . . . . 12 ((𝑗 + 1) ∈ ℙ → (𝑗 + 1) ∈ ℕ)
9392nnrecred 12259 . . . . . . . . . . 11 ((𝑗 + 1) ∈ ℙ → (1 / (𝑗 + 1)) ∈ ℝ)
9493adantl 483 . . . . . . . . . 10 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (1 / (𝑗 + 1)) ∈ ℝ)
95 0red 11213 . . . . . . . . . 10 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → 0 ∈ ℝ)
9694, 95ifclda 4562 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝐾)) → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) ∈ ℝ)
9781, 96remulcld 11240 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) ∈ ℝ)
9879, 91, 97leadd1d 11804 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ ((𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))))
99 eluzp1p1 12846 . . . . . . . . . . . . 13 (𝑗 ∈ (ℤ𝐾) → (𝑗 + 1) ∈ (ℤ‘(𝐾 + 1)))
10099adantl 483 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑗 + 1) ∈ (ℤ‘(𝐾 + 1)))
101 simpl 484 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝜑)
102 elfzuz 13493 . . . . . . . . . . . . 13 (𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1)) → 𝑘 ∈ (ℤ‘(𝐾 + 1)))
10388recnd 11238 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
10457, 103syl 17 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (ℤ‘(𝐾 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
105101, 102, 104syl2an 597 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
106 eleq1 2822 . . . . . . . . . . . . 13 (𝑘 = (𝑗 + 1) → (𝑘 ∈ ℙ ↔ (𝑗 + 1) ∈ ℙ))
107 oveq2 7412 . . . . . . . . . . . . 13 (𝑘 = (𝑗 + 1) → (1 / 𝑘) = (1 / (𝑗 + 1)))
108106, 107ifbieq1d 4551 . . . . . . . . . . . 12 (𝑘 = (𝑗 + 1) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))
109100, 105, 108fsumm1 15693 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = (Σ𝑘 ∈ ((𝐾 + 1)...((𝑗 + 1) − 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
110 eluzelz 12828 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (ℤ𝐾) → 𝑗 ∈ ℤ)
111110adantl 483 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑗 ∈ ℤ)
112111zcnd 12663 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑗 ∈ ℂ)
113 ax-1cn 11164 . . . . . . . . . . . . . . 15 1 ∈ ℂ
114 pncan 11462 . . . . . . . . . . . . . . 15 ((𝑗 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑗 + 1) − 1) = 𝑗)
115112, 113, 114sylancl 587 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((𝑗 + 1) − 1) = 𝑗)
116115oveq2d 7420 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((𝐾 + 1)...((𝑗 + 1) − 1)) = ((𝐾 + 1)...𝑗))
117116sumeq1d 15643 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...((𝑗 + 1) − 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
118117oveq1d 7419 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝐾)) → (Σ𝑘 ∈ ((𝐾 + 1)...((𝑗 + 1) − 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
119109, 118eqtrd 2773 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
120119oveq2d 7420 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
12131adantr 482 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑁 ∈ ℂ)
12290recnd 11238 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
12396recnd 11238 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝐾)) → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) ∈ ℂ)
124121, 122, 123adddid 11234 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑁 · (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) = ((𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
125120, 124eqtrd 2773 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = ((𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
126125breq2d 5159 . . . . . . 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)))))
12798, 126bitr4d 282 . . . . . 6 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
128102, 69sylan2 594 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))) → (𝑊𝑘) ⊆ (1...𝑁))
129128ralrimiva 3147 . . . . . . . . . . . . 13 (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘) ⊆ (1...𝑁))
130129adantr 482 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝐾)) → ∀𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘) ⊆ (1...𝑁))
131 iunss 5047 . . . . . . . . . . . 12 ( 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘) ⊆ (1...𝑁) ↔ ∀𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘) ⊆ (1...𝑁))
132130, 131sylibr 233 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘) ⊆ (1...𝑁))
133 ssfi 9169 . . . . . . . . . . 11 (((1...𝑁) ∈ Fin ∧ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘) ⊆ (1...𝑁)) → 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘) ∈ Fin)
13453, 132, 133sylancr 588 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘) ∈ Fin)
135 hashcl 14312 . . . . . . . . . 10 ( 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘) ∈ Fin → (♯‘ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘)) ∈ ℕ0)
136134, 135syl 17 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘)) ∈ ℕ0)
137136nn0red 12529 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘)) ∈ ℝ)
138 fveq2 6888 . . . . . . . . . . . . . 14 (𝑘 = (𝑗 + 1) → (𝑊𝑘) = (𝑊‘(𝑗 + 1)))
139138sseq1d 4012 . . . . . . . . . . . . 13 (𝑘 = (𝑗 + 1) → ((𝑊𝑘) ⊆ (1...𝑁) ↔ (𝑊‘(𝑗 + 1)) ⊆ (1...𝑁)))
14068ralrimiva 3147 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑘 ∈ ℕ (𝑊𝑘) ⊆ (1...𝑁))
141140adantr 482 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝐾)) → ∀𝑘 ∈ ℕ (𝑊𝑘) ⊆ (1...𝑁))
142 eluznn 12898 . . . . . . . . . . . . . . 15 ((𝐾 ∈ ℕ ∧ 𝑗 ∈ (ℤ𝐾)) → 𝑗 ∈ ℕ)
14334, 142sylan 581 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑗 ∈ ℕ)
144143peano2nnd 12225 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑗 + 1) ∈ ℕ)
145139, 141, 144rspcdva 3613 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑊‘(𝑗 + 1)) ⊆ (1...𝑁))
146 ssfi 9169 . . . . . . . . . . . 12 (((1...𝑁) ∈ Fin ∧ (𝑊‘(𝑗 + 1)) ⊆ (1...𝑁)) → (𝑊‘(𝑗 + 1)) ∈ Fin)
14753, 145, 146sylancr 588 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑊‘(𝑗 + 1)) ∈ Fin)
148 hashcl 14312 . . . . . . . . . . 11 ((𝑊‘(𝑗 + 1)) ∈ Fin → (♯‘(𝑊‘(𝑗 + 1))) ∈ ℕ0)
149147, 148syl 17 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘(𝑊‘(𝑗 + 1))) ∈ ℕ0)
150149nn0red 12529 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘(𝑊‘(𝑗 + 1))) ∈ ℝ)
15179, 150readdcld 11239 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))) ∈ ℝ)
15279, 97readdcld 11239 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ∈ ℝ)
15338adantr 482 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝐾 + 1) ∈ ℤ)
154 simpr 486 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑗 ∈ (ℤ𝐾))
15534nncnd 12224 . . . . . . . . . . . . . . . . 17 (𝜑𝐾 ∈ ℂ)
156155adantr 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝐾 ∈ ℂ)
157 pncan 11462 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐾 + 1) − 1) = 𝐾)
158156, 113, 157sylancl 587 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((𝐾 + 1) − 1) = 𝐾)
159158fveq2d 6892 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ𝐾)) → (ℤ‘((𝐾 + 1) − 1)) = (ℤ𝐾))
160154, 159eleqtrrd 2837 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑗 ∈ (ℤ‘((𝐾 + 1) − 1)))
161 fzsuc2 13555 . . . . . . . . . . . . 13 (((𝐾 + 1) ∈ ℤ ∧ 𝑗 ∈ (ℤ‘((𝐾 + 1) − 1))) → ((𝐾 + 1)...(𝑗 + 1)) = (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)}))
162153, 160, 161syl2anc 585 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((𝐾 + 1)...(𝑗 + 1)) = (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)}))
163162iuneq1d 5023 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘) = 𝑘 ∈ (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})(𝑊𝑘))
164 iunxun 5096 . . . . . . . . . . . 12 𝑘 ∈ (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})(𝑊𝑘) = ( 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ∪ 𝑘 ∈ {(𝑗 + 1)} (𝑊𝑘))
165 ovex 7437 . . . . . . . . . . . . . 14 (𝑗 + 1) ∈ V
166165, 138iunxsn 5093 . . . . . . . . . . . . 13 𝑘 ∈ {(𝑗 + 1)} (𝑊𝑘) = (𝑊‘(𝑗 + 1))
167166uneq2i 4159 . . . . . . . . . . . 12 ( 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ∪ 𝑘 ∈ {(𝑗 + 1)} (𝑊𝑘)) = ( 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ∪ (𝑊‘(𝑗 + 1)))
168164, 167eqtri 2761 . . . . . . . . . . 11 𝑘 ∈ (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})(𝑊𝑘) = ( 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ∪ (𝑊‘(𝑗 + 1)))
169163, 168eqtrdi 2789 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘) = ( 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ∪ (𝑊‘(𝑗 + 1))))
170169fveq2d 6892 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘)) = (♯‘( 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ∪ (𝑊‘(𝑗 + 1)))))
171 hashun2 14339 . . . . . . . . . 10 (( 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ∈ Fin ∧ (𝑊‘(𝑗 + 1)) ∈ Fin) → (♯‘( 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ∪ (𝑊‘(𝑗 + 1)))) ≤ ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))))
17276, 147, 171syl2anc 585 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘( 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘) ∪ (𝑊‘(𝑗 + 1)))) ≤ ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))))
173170, 172eqbrtrd 5169 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘)) ≤ ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))))
17481, 144nndivred 12262 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑁 / (𝑗 + 1)) ∈ ℝ)
175 flle 13760 . . . . . . . . . . . . . 14 ((𝑁 / (𝑗 + 1)) ∈ ℝ → (⌊‘(𝑁 / (𝑗 + 1))) ≤ (𝑁 / (𝑗 + 1)))
176174, 175syl 17 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝐾)) → (⌊‘(𝑁 / (𝑗 + 1))) ≤ (𝑁 / (𝑗 + 1)))
177 elfznn 13526 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ)
178177nncnd 12224 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ)
179178subid1d 11556 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (1...𝑁) → (𝑛 − 0) = 𝑛)
180179breq2d 5159 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (1...𝑁) → ((𝑗 + 1) ∥ (𝑛 − 0) ↔ (𝑗 + 1) ∥ 𝑛))
181180rabbiia 3437 . . . . . . . . . . . . . . 15 {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)} = {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}
182181fveq2i 6891 . . . . . . . . . . . . . 14 (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)}) = (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛})
183 1zzd 12589 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (ℤ𝐾)) → 1 ∈ ℤ)
18430nnnn0d 12528 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ ℕ0)
185 nn0uz 12860 . . . . . . . . . . . . . . . . . . 19 0 = (ℤ‘0)
186 1m1e0 12280 . . . . . . . . . . . . . . . . . . . 20 (1 − 1) = 0
187186fveq2i 6891 . . . . . . . . . . . . . . . . . . 19 (ℤ‘(1 − 1)) = (ℤ‘0)
188185, 187eqtr4i 2764 . . . . . . . . . . . . . . . . . 18 0 = (ℤ‘(1 − 1))
189184, 188eleqtrdi 2844 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ (ℤ‘(1 − 1)))
190189adantr 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (ℤ𝐾)) → 𝑁 ∈ (ℤ‘(1 − 1)))
191 0zd 12566 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (ℤ𝐾)) → 0 ∈ ℤ)
192144, 183, 190, 191hashdvds 16704 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)}) = ((⌊‘((𝑁 − 0) / (𝑗 + 1))) − (⌊‘(((1 − 1) − 0) / (𝑗 + 1)))))
193121subid1d 11556 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑁 − 0) = 𝑁)
194193fvoveq1d 7426 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (ℤ𝐾)) → (⌊‘((𝑁 − 0) / (𝑗 + 1))) = (⌊‘(𝑁 / (𝑗 + 1))))
195186oveq1i 7414 . . . . . . . . . . . . . . . . . . . . 21 ((1 − 1) − 0) = (0 − 0)
196 0m0e0 12328 . . . . . . . . . . . . . . . . . . . . 21 (0 − 0) = 0
197195, 196eqtri 2761 . . . . . . . . . . . . . . . . . . . 20 ((1 − 1) − 0) = 0
198197oveq1i 7414 . . . . . . . . . . . . . . . . . . 19 (((1 − 1) − 0) / (𝑗 + 1)) = (0 / (𝑗 + 1))
199144nncnd 12224 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑗 + 1) ∈ ℂ)
200144nnne0d 12258 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑗 + 1) ≠ 0)
201199, 200div0d 11985 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (ℤ𝐾)) → (0 / (𝑗 + 1)) = 0)
202198, 201eqtrid 2785 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (ℤ𝐾)) → (((1 − 1) − 0) / (𝑗 + 1)) = 0)
203202fveq2d 6892 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (ℤ𝐾)) → (⌊‘(((1 − 1) − 0) / (𝑗 + 1))) = (⌊‘0))
204 0z 12565 . . . . . . . . . . . . . . . . . 18 0 ∈ ℤ
205 flid 13769 . . . . . . . . . . . . . . . . . 18 (0 ∈ ℤ → (⌊‘0) = 0)
206204, 205ax-mp 5 . . . . . . . . . . . . . . . . 17 (⌊‘0) = 0
207203, 206eqtrdi 2789 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (ℤ𝐾)) → (⌊‘(((1 − 1) − 0) / (𝑗 + 1))) = 0)
208194, 207oveq12d 7422 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((⌊‘((𝑁 − 0) / (𝑗 + 1))) − (⌊‘(((1 − 1) − 0) / (𝑗 + 1)))) = ((⌊‘(𝑁 / (𝑗 + 1))) − 0))
209174flcld 13759 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (ℤ𝐾)) → (⌊‘(𝑁 / (𝑗 + 1))) ∈ ℤ)
210209zcnd 12663 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (ℤ𝐾)) → (⌊‘(𝑁 / (𝑗 + 1))) ∈ ℂ)
211210subid1d 11556 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((⌊‘(𝑁 / (𝑗 + 1))) − 0) = (⌊‘(𝑁 / (𝑗 + 1))))
212192, 208, 2113eqtrd 2777 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)}) = (⌊‘(𝑁 / (𝑗 + 1))))
213182, 212eqtr3id 2787 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) = (⌊‘(𝑁 / (𝑗 + 1))))
214121, 199, 200divrecd 11989 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑁 / (𝑗 + 1)) = (𝑁 · (1 / (𝑗 + 1))))
215214eqcomd 2739 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑁 · (1 / (𝑗 + 1))) = (𝑁 / (𝑗 + 1)))
216176, 213, 2153brtr4d 5179 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) ≤ (𝑁 · (1 / (𝑗 + 1))))
217216adantr 482 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) ≤ (𝑁 · (1 / (𝑗 + 1))))
218 eleq1 2822 . . . . . . . . . . . . . . . . . 18 (𝑝 = (𝑗 + 1) → (𝑝 ∈ ℙ ↔ (𝑗 + 1) ∈ ℙ))
219 breq1 5150 . . . . . . . . . . . . . . . . . 18 (𝑝 = (𝑗 + 1) → (𝑝𝑛 ↔ (𝑗 + 1) ∥ 𝑛))
220218, 219anbi12d 632 . . . . . . . . . . . . . . . . 17 (𝑝 = (𝑗 + 1) → ((𝑝 ∈ ℙ ∧ 𝑝𝑛) ↔ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)))
221220rabbidv 3441 . . . . . . . . . . . . . . . 16 (𝑝 = (𝑗 + 1) → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝𝑛)} = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)})
22263rabex 5331 . . . . . . . . . . . . . . . 16 {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)} ∈ V
223221, 62, 222fvmpt 6994 . . . . . . . . . . . . . . 15 ((𝑗 + 1) ∈ ℕ → (𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)})
224144, 223syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)})
225224adantr 482 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)})
226 simpr 486 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑗 + 1) ∈ ℙ)
227226biantrurd 534 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → ((𝑗 + 1) ∥ 𝑛 ↔ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)))
228227rabbidv 3441 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛} = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)})
229225, 228eqtr4d 2776 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛})
230229fveq2d 6892 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) = (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}))
231 iftrue 4533 . . . . . . . . . . . . 13 ((𝑗 + 1) ∈ ℙ → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) = (1 / (𝑗 + 1)))
232231adantl 483 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) = (1 / (𝑗 + 1)))
233232oveq2d 7420 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) = (𝑁 · (1 / (𝑗 + 1))))
234217, 230, 2333brtr4d 5179 . . . . . . . . . 10 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) ≤ (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
23529a1i 11 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → 0 ≤ 0)
236 simpl 484 . . . . . . . . . . . . . . . . 17 (((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛) → (𝑗 + 1) ∈ ℙ)
237236con3i 154 . . . . . . . . . . . . . . . 16 (¬ (𝑗 + 1) ∈ ℙ → ¬ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛))
238237ralrimivw 3151 . . . . . . . . . . . . . . 15 (¬ (𝑗 + 1) ∈ ℙ → ∀𝑛 ∈ (1...𝑁) ¬ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛))
239 rabeq0 4383 . . . . . . . . . . . . . . 15 ({𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)} = ∅ ↔ ∀𝑛 ∈ (1...𝑁) ¬ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛))
240238, 239sylibr 233 . . . . . . . . . . . . . 14 (¬ (𝑗 + 1) ∈ ℙ → {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)} = ∅)
241224, 240sylan9eq 2793 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (𝑊‘(𝑗 + 1)) = ∅)
242241fveq2d 6892 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) = (♯‘∅))
243242, 46eqtrdi 2789 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) = 0)
244 iffalse 4536 . . . . . . . . . . . . 13 (¬ (𝑗 + 1) ∈ ℙ → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) = 0)
245244oveq2d 7420 . . . . . . . . . . . 12 (¬ (𝑗 + 1) ∈ ℙ → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) = (𝑁 · 0))
24632adantr 482 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑁 · 0) = 0)
247245, 246sylan9eqr 2795 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) = 0)
248235, 243, 2473brtr4d 5179 . . . . . . . . . 10 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) ≤ (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
249234, 248pm2.61dan 812 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘(𝑊‘(𝑗 + 1))) ≤ (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
250150, 97, 79, 249leadd2dd 11825 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))) ≤ ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
251137, 151, 152, 173, 250letrd 11367 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ𝐾)) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘)) ≤ ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
252 fzfid 13934 . . . . . . . . . 10 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((𝐾 + 1)...(𝑗 + 1)) ∈ Fin)
25357, 88syl 17 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (ℤ‘(𝐾 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
254101, 102, 253syl2an 597 . . . . . . . . . 10 (((𝜑𝑗 ∈ (ℤ𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
255252, 254fsumrecl 15676 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
25681, 255remulcld 11240 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ∈ ℝ)
257 letr 11304 . . . . . . . 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))))
258137, 152, 256, 257syl3anc 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))))
259251, 258mpand 694 . . . . . 6 ((𝜑𝑗 ∈ (ℤ𝐾)) → (((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
260127, 259sylbid 239 . . . . 5 ((𝜑𝑗 ∈ (ℤ𝐾)) → ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
261260expcom 415 . . . 4 (𝑗 ∈ (ℤ𝐾) → (𝜑 → ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
262261a2d 29 . . 3 (𝑗 ∈ (ℤ𝐾) → ((𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) → (𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
2637, 14, 21, 28, 52, 262uzind4i 12890 . 2 (𝑁 ∈ (ℤ𝐾) → (𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
264263com12 32 1 (𝜑 → (𝑁 ∈ (ℤ𝐾) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  wral 3062  {crab 3433  cdif 3944  cun 3945  wss 3947  c0 4321  ifcif 4527  {csn 4627   ciun 4996   class class class wbr 5147  cmpt 5230  dom cdm 5675  cfv 6540  (class class class)co 7404  Fincfn 8935  cc 11104  cr 11105  0cc0 11106  1c1 11107   + caddc 11109   · cmul 11111   < clt 11244  cle 11245  cmin 11440   / cdiv 11867  cn 12208  2c2 12263  0cn0 12468  cz 12554  cuz 12818  ...cfz 13480  cfl 13751  seqcseq 13962  chash 14286  cli 15424  Σcsu 15628  cdvds 16193  cprime 16604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-om 7851  df-1st 7970  df-2nd 7971  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-oadd 8465  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-sup 9433  df-inf 9434  df-oi 9501  df-dju 9892  df-card 9930  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-n0 12469  df-xnn0 12541  df-z 12555  df-uz 12819  df-rp 12971  df-fz 13481  df-fzo 13624  df-fl 13753  df-seq 13963  df-exp 14024  df-hash 14287  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-clim 15428  df-sum 15629  df-dvds 16194  df-prm 16605
This theorem is referenced by:  prmreclem5  16849
  Copyright terms: Public domain W3C validator