Metamath Proof Explorer

Theorem prmreclem4

Description: Lemma for prmrec . Show by induction that the indexed (nondisjoint) union Wk is at most the size of the prime reciprocal series. The key counting lemma is hashdvds , to show that the number of numbers in 1 ... N that divide k is at most N / k . (Contributed by Mario Carneiro, 6-Aug-2014)

Ref Expression
Hypotheses prmrec.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 1 / 𝑛 ) , 0 ) )
prmrec.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
prmrec.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
prmrec.4 ⊢ 𝑀 = { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑛 }
prmrec.5 ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ∈ dom ⇝ )
prmrec.6 ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) < ( 1 / 2 ) )
prmrec.7 ⊢ 𝑊 = ( 𝑝 ∈ ℕ ↦ { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛 ) } )
Assertion prmreclem4 ( 𝜑 → ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ) )

Proof

Step Hyp Ref Expression
1 prmrec.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 1 / 𝑛 ) , 0 ) )
2 prmrec.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
3 prmrec.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 prmrec.4 ⊢ 𝑀 = { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑛 }
5 prmrec.5 ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ∈ dom ⇝ )
6 prmrec.6 ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) < ( 1 / 2 ) )
7 prmrec.7 ⊢ 𝑊 = ( 𝑝 ∈ ℕ ↦ { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛 ) } )
8 oveq2 ⊢ ( 𝑥 = 𝐾 → ( ( 𝐾 + 1 ) ... 𝑥 ) = ( ( 𝐾 + 1 ) ... 𝐾 ) )
9 8 iuneq1d ⊢ ( 𝑥 = 𝐾 → ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) ( 𝑊 ‘ 𝑘 ) = ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝐾 ) ( 𝑊 ‘ 𝑘 ) )
10 9 fveq2d ⊢ ( 𝑥 = 𝐾 → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) ( 𝑊 ‘ 𝑘 ) ) = ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝐾 ) ( 𝑊 ‘ 𝑘 ) ) )
11 8 sumeq1d ⊢ ( 𝑥 = 𝐾 → Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) = Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝐾 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) )
12 11 oveq2d ⊢ ( 𝑥 = 𝐾 → ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) = ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝐾 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) )
13 10 12 breq12d ⊢ ( 𝑥 = 𝐾 → ( ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ↔ ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝐾 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝐾 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ) )
14 13 imbi2d ⊢ ( 𝑥 = 𝐾 → ( ( 𝜑 → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ) ↔ ( 𝜑 → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝐾 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝐾 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ) ) )
15 oveq2 ⊢ ( 𝑥 = 𝑗 → ( ( 𝐾 + 1 ) ... 𝑥 ) = ( ( 𝐾 + 1 ) ... 𝑗 ) )
16 15 iuneq1d ⊢ ( 𝑥 = 𝑗 → ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) ( 𝑊 ‘ 𝑘 ) = ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) )
17 16 fveq2d ⊢ ( 𝑥 = 𝑗 → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) ( 𝑊 ‘ 𝑘 ) ) = ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ) )
18 15 sumeq1d ⊢ ( 𝑥 = 𝑗 → Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) = Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) )
19 18 oveq2d ⊢ ( 𝑥 = 𝑗 → ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) = ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) )
20 17 19 breq12d ⊢ ( 𝑥 = 𝑗 → ( ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ↔ ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ) )
21 20 imbi2d ⊢ ( 𝑥 = 𝑗 → ( ( 𝜑 → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ) ↔ ( 𝜑 → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ) ) )
22 oveq2 ⊢ ( 𝑥 = ( 𝑗 + 1 ) → ( ( 𝐾 + 1 ) ... 𝑥 ) = ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) )
23 22 iuneq1d ⊢ ( 𝑥 = ( 𝑗 + 1 ) → ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) ( 𝑊 ‘ 𝑘 ) = ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ( 𝑊 ‘ 𝑘 ) )
24 23 fveq2d ⊢ ( 𝑥 = ( 𝑗 + 1 ) → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) ( 𝑊 ‘ 𝑘 ) ) = ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ( 𝑊 ‘ 𝑘 ) ) )
25 22 sumeq1d ⊢ ( 𝑥 = ( 𝑗 + 1 ) → Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) = Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) )
26 25 oveq2d ⊢ ( 𝑥 = ( 𝑗 + 1 ) → ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) = ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) )
27 24 26 breq12d ⊢ ( 𝑥 = ( 𝑗 + 1 ) → ( ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ↔ ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ) )
28 27 imbi2d ⊢ ( 𝑥 = ( 𝑗 + 1 ) → ( ( 𝜑 → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ) ↔ ( 𝜑 → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ) ) )
29 oveq2 ⊢ ( 𝑥 = 𝑁 → ( ( 𝐾 + 1 ) ... 𝑥 ) = ( ( 𝐾 + 1 ) ... 𝑁 ) )
30 29 iuneq1d ⊢ ( 𝑥 = 𝑁 → ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) ( 𝑊 ‘ 𝑘 ) = ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) )
31 30 fveq2d ⊢ ( 𝑥 = 𝑁 → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) ( 𝑊 ‘ 𝑘 ) ) = ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) )
32 29 sumeq1d ⊢ ( 𝑥 = 𝑁 → Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) = Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) )
33 32 oveq2d ⊢ ( 𝑥 = 𝑁 → ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) = ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) )
34 31 33 breq12d ⊢ ( 𝑥 = 𝑁 → ( ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ↔ ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ) )
35 34 imbi2d ⊢ ( 𝑥 = 𝑁 → ( ( 𝜑 → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑥 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ) ↔ ( 𝜑 → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ) ) )
36 0le0 ⊢ 0 ≤ 0
37 3 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
38 37 mul01d ⊢ ( 𝜑 → ( 𝑁 · 0 ) = 0 )
39 36 38 breqtrrid ⊢ ( 𝜑 → 0 ≤ ( 𝑁 · 0 ) )
40 2 nnred ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
41 40 ltp1d ⊢ ( 𝜑 → 𝐾 < ( 𝐾 + 1 ) )
42 2 nnzd ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
43 42 peano2zd ⊢ ( 𝜑 → ( 𝐾 + 1 ) ∈ ℤ )
44 fzn ⊢ ( ( ( 𝐾 + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐾 < ( 𝐾 + 1 ) ↔ ( ( 𝐾 + 1 ) ... 𝐾 ) = ∅ ) )
45 43 42 44 syl2anc ⊢ ( 𝜑 → ( 𝐾 < ( 𝐾 + 1 ) ↔ ( ( 𝐾 + 1 ) ... 𝐾 ) = ∅ ) )
46 41 45 mpbid ⊢ ( 𝜑 → ( ( 𝐾 + 1 ) ... 𝐾 ) = ∅ )
47 46 iuneq1d ⊢ ( 𝜑 → ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝐾 ) ( 𝑊 ‘ 𝑘 ) = ∪ 𝑘 ∈ ∅ ( 𝑊 ‘ 𝑘 ) )
48 0iun ⊢ ∪ 𝑘 ∈ ∅ ( 𝑊 ‘ 𝑘 ) = ∅
49 47 48 eqtrdi ⊢ ( 𝜑 → ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝐾 ) ( 𝑊 ‘ 𝑘 ) = ∅ )
50 49 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝐾 ) ( 𝑊 ‘ 𝑘 ) ) = ( ♯ ‘ ∅ ) )
51 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
52 50 51 eqtrdi ⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝐾 ) ( 𝑊 ‘ 𝑘 ) ) = 0 )
53 46 sumeq1d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝐾 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) = Σ 𝑘 ∈ ∅ if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) )
54 sum0 ⊢ Σ 𝑘 ∈ ∅ if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) = 0
55 53 54 eqtrdi ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝐾 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) = 0 )
56 55 oveq2d ⊢ ( 𝜑 → ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝐾 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) = ( 𝑁 · 0 ) )
57 39 52 56 3brtr4d ⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝐾 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝐾 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) )
58 fzfi ⊢ ( 1 ... 𝑁 ) ∈ Fin
59 elfzuz ⊢ ( 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) )
60 2 peano2nnd ⊢ ( 𝜑 → ( 𝐾 + 1 ) ∈ ℕ )
61 eluznn ⊢ ( ( ( 𝐾 + 1 ) ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ) → 𝑘 ∈ ℕ )
62 60 61 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ) → 𝑘 ∈ ℕ )
63 eleq1 ⊢ ( 𝑝 = 𝑘 → ( 𝑝 ∈ ℙ ↔ 𝑘 ∈ ℙ ) )
64 breq1 ⊢ ( 𝑝 = 𝑘 → ( 𝑝 ∥ 𝑛 ↔ 𝑘 ∥ 𝑛 ) )
65 63 64 anbi12d ⊢ ( 𝑝 = 𝑘 → ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛 ) ↔ ( 𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛 ) ) )
66 65 rabbidv ⊢ ( 𝑝 = 𝑘 → { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛 ) } = { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛 ) } )
67 ovex ⊢ ( 1 ... 𝑁 ) ∈ V
68 67 rabex ⊢ { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛 ) } ∈ V
69 66 7 68 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( 𝑊 ‘ 𝑘 ) = { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛 ) } )
70 69 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑊 ‘ 𝑘 ) = { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛 ) } )
71 ssrab2 ⊢ { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛 ) } ⊆ ( 1 ... 𝑁 )
72 70 71 eqsstrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑊 ‘ 𝑘 ) ⊆ ( 1 ... 𝑁 ) )
73 62 72 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ) → ( 𝑊 ‘ 𝑘 ) ⊆ ( 1 ... 𝑁 ) )
74 59 73 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ) → ( 𝑊 ‘ 𝑘 ) ⊆ ( 1 ... 𝑁 ) )
75 74 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ⊆ ( 1 ... 𝑁 ) )
76 75 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ∀ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ⊆ ( 1 ... 𝑁 ) )
77 iunss ⊢ ( ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ⊆ ( 1 ... 𝑁 ) ↔ ∀ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ⊆ ( 1 ... 𝑁 ) )
78 76 77 sylibr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ⊆ ( 1 ... 𝑁 ) )
79 ssfi ⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ⊆ ( 1 ... 𝑁 ) ) → ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ∈ Fin )
80 58 78 79 sylancr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ∈ Fin )
81 hashcl ⊢ ( ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ∈ Fin → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ) ∈ ℕ0 )
82 80 81 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ) ∈ ℕ0 )
83 82 nn0red ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ) ∈ ℝ )
84 3 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
85 84 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑁 ∈ ℝ )
86 fzfid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( 𝐾 + 1 ) ... 𝑗 ) ∈ Fin )
87 60 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝐾 + 1 ) ∈ ℕ )
88 87 59 61 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ) → 𝑘 ∈ ℕ )
89 nnrecre ⊢ ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℝ )
90 0re ⊢ 0 ∈ ℝ
91 ifcl ⊢ ( ( ( 1 / 𝑘 ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ∈ ℝ )
92 89 90 91 sylancl ⊢ ( 𝑘 ∈ ℕ → if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ∈ ℝ )
93 88 92 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ) → if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ∈ ℝ )
94 86 93 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ∈ ℝ )
95 85 94 remulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ∈ ℝ )
96 prmnn ⊢ ( ( 𝑗 + 1 ) ∈ ℙ → ( 𝑗 + 1 ) ∈ ℕ )
97 96 nnrecred ⊢ ( ( 𝑗 + 1 ) ∈ ℙ → ( 1 / ( 𝑗 + 1 ) ) ∈ ℝ )
98 97 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑗 + 1 ) ∈ ℙ ) → ( 1 / ( 𝑗 + 1 ) ) ∈ ℝ )
99 0red ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ¬ ( 𝑗 + 1 ) ∈ ℙ ) → 0 ∈ ℝ )
100 98 99 ifclda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) ∈ ℝ )
101 85 100 remulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑁 · if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) ) ∈ ℝ )
102 83 95 101 leadd1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ↔ ( ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ) + ( 𝑁 · if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) ) ) ≤ ( ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) + ( 𝑁 · if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) ) ) ) )
103 eluzp1p1 ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) → ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) )
104 103 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) )
105 simpl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝜑 )
106 elfzuz ⊢ ( 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) )
107 92 recnd ⊢ ( 𝑘 ∈ ℕ → if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ∈ ℂ )
108 62 107 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ) → if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ∈ ℂ )
109 105 106 108 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ) → if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ∈ ℂ )
110 eleq1 ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝑘 ∈ ℙ ↔ ( 𝑗 + 1 ) ∈ ℙ ) )
111 oveq2 ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 1 / 𝑘 ) = ( 1 / ( 𝑗 + 1 ) ) )
112 110 111 ifbieq1d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) = if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) )
113 104 109 112 fsumm1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) = ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( ( 𝑗 + 1 ) − 1 ) ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) + if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) ) )
114 eluzelz ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝑗 ∈ ℤ )
115 114 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑗 ∈ ℤ )
116 115 zcnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑗 ∈ ℂ )
117 ax-1cn ⊢ 1 ∈ ℂ
118 pncan ⊢ ( ( 𝑗 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑗 + 1 ) − 1 ) = 𝑗 )
119 116 117 118 sylancl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( 𝑗 + 1 ) − 1 ) = 𝑗 )
120 119 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( 𝐾 + 1 ) ... ( ( 𝑗 + 1 ) − 1 ) ) = ( ( 𝐾 + 1 ) ... 𝑗 ) )
121 120 sumeq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( ( 𝑗 + 1 ) − 1 ) ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) = Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) )
122 121 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( ( 𝑗 + 1 ) − 1 ) ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) + if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) ) = ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) + if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) ) )
123 113 122 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) = ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) + if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) ) )
124 123 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) = ( 𝑁 · ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) + if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) ) ) )
125 37 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑁 ∈ ℂ )
126 94 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ∈ ℂ )
127 100 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) ∈ ℂ )
128 125 126 127 adddid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑁 · ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) + if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) ) ) = ( ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) + ( 𝑁 · if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) ) ) )
129 124 128 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) = ( ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) + ( 𝑁 · if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) ) ) )
130 129 breq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 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 ) ) ) ) )
131 102 130 bitr4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ↔ ( ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ) + ( 𝑁 · if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ) )
132 106 73 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ) → ( 𝑊 ‘ 𝑘 ) ⊆ ( 1 ... 𝑁 ) )
133 132 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ( 𝑊 ‘ 𝑘 ) ⊆ ( 1 ... 𝑁 ) )
134 133 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ∀ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ( 𝑊 ‘ 𝑘 ) ⊆ ( 1 ... 𝑁 ) )
135 iunss ⊢ ( ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ( 𝑊 ‘ 𝑘 ) ⊆ ( 1 ... 𝑁 ) ↔ ∀ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ( 𝑊 ‘ 𝑘 ) ⊆ ( 1 ... 𝑁 ) )
136 134 135 sylibr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ( 𝑊 ‘ 𝑘 ) ⊆ ( 1 ... 𝑁 ) )
137 ssfi ⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ( 𝑊 ‘ 𝑘 ) ⊆ ( 1 ... 𝑁 ) ) → ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ( 𝑊 ‘ 𝑘 ) ∈ Fin )
138 58 136 137 sylancr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ( 𝑊 ‘ 𝑘 ) ∈ Fin )
139 hashcl ⊢ ( ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ( 𝑊 ‘ 𝑘 ) ∈ Fin → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ( 𝑊 ‘ 𝑘 ) ) ∈ ℕ0 )
140 138 139 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ( 𝑊 ‘ 𝑘 ) ) ∈ ℕ0 )
141 140 nn0red ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ( 𝑊 ‘ 𝑘 ) ) ∈ ℝ )
142 fveq2 ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝑊 ‘ 𝑘 ) = ( 𝑊 ‘ ( 𝑗 + 1 ) ) )
143 142 sseq1d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( ( 𝑊 ‘ 𝑘 ) ⊆ ( 1 ... 𝑁 ) ↔ ( 𝑊 ‘ ( 𝑗 + 1 ) ) ⊆ ( 1 ... 𝑁 ) ) )
144 72 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( 𝑊 ‘ 𝑘 ) ⊆ ( 1 ... 𝑁 ) )
145 144 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ∀ 𝑘 ∈ ℕ ( 𝑊 ‘ 𝑘 ) ⊆ ( 1 ... 𝑁 ) )
146 eluznn ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑗 ∈ ℕ )
147 2 146 sylan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑗 ∈ ℕ )
148 147 peano2nnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑗 + 1 ) ∈ ℕ )
149 143 145 148 rspcdva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑊 ‘ ( 𝑗 + 1 ) ) ⊆ ( 1 ... 𝑁 ) )
150 ssfi ⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ ( 𝑊 ‘ ( 𝑗 + 1 ) ) ⊆ ( 1 ... 𝑁 ) ) → ( 𝑊 ‘ ( 𝑗 + 1 ) ) ∈ Fin )
151 58 149 150 sylancr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑊 ‘ ( 𝑗 + 1 ) ) ∈ Fin )
152 hashcl ⊢ ( ( 𝑊 ‘ ( 𝑗 + 1 ) ) ∈ Fin → ( ♯ ‘ ( 𝑊 ‘ ( 𝑗 + 1 ) ) ) ∈ ℕ0 )
153 151 152 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ♯ ‘ ( 𝑊 ‘ ( 𝑗 + 1 ) ) ) ∈ ℕ0 )
154 153 nn0red ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ♯ ‘ ( 𝑊 ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ )
155 83 154 readdcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ) + ( ♯ ‘ ( 𝑊 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ℝ )
156 83 101 readdcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ) + ( 𝑁 · if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) ) ) ∈ ℝ )
157 43 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝐾 + 1 ) ∈ ℤ )
158 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) )
159 2 nncnd ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
160 159 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝐾 ∈ ℂ )
161 pncan ⊢ ( ( 𝐾 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐾 + 1 ) − 1 ) = 𝐾 )
162 160 117 161 sylancl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( 𝐾 + 1 ) − 1 ) = 𝐾 )
163 162 fveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ℤ≥ ‘ ( ( 𝐾 + 1 ) − 1 ) ) = ( ℤ≥ ‘ 𝐾 ) )
164 158 163 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑗 ∈ ( ℤ≥ ‘ ( ( 𝐾 + 1 ) − 1 ) ) )
165 fzsuc2 ⊢ ( ( ( 𝐾 + 1 ) ∈ ℤ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( ( 𝐾 + 1 ) − 1 ) ) ) → ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) = ( ( ( 𝐾 + 1 ) ... 𝑗 ) ∪ { ( 𝑗 + 1 ) } ) )
166 157 164 165 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) = ( ( ( 𝐾 + 1 ) ... 𝑗 ) ∪ { ( 𝑗 + 1 ) } ) )
167 166 iuneq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ( 𝑊 ‘ 𝑘 ) = ∪ 𝑘 ∈ ( ( ( 𝐾 + 1 ) ... 𝑗 ) ∪ { ( 𝑗 + 1 ) } ) ( 𝑊 ‘ 𝑘 ) )
168 iunxun ⊢ ∪ 𝑘 ∈ ( ( ( 𝐾 + 1 ) ... 𝑗 ) ∪ { ( 𝑗 + 1 ) } ) ( 𝑊 ‘ 𝑘 ) = ( ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ∪ ∪ 𝑘 ∈ { ( 𝑗 + 1 ) } ( 𝑊 ‘ 𝑘 ) )
169 ovex ⊢ ( 𝑗 + 1 ) ∈ V
170 169 142 iunxsn ⊢ ∪ 𝑘 ∈ { ( 𝑗 + 1 ) } ( 𝑊 ‘ 𝑘 ) = ( 𝑊 ‘ ( 𝑗 + 1 ) )
171 170 uneq2i ⊢ ( ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ∪ ∪ 𝑘 ∈ { ( 𝑗 + 1 ) } ( 𝑊 ‘ 𝑘 ) ) = ( ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ∪ ( 𝑊 ‘ ( 𝑗 + 1 ) ) )
172 168 171 eqtri ⊢ ∪ 𝑘 ∈ ( ( ( 𝐾 + 1 ) ... 𝑗 ) ∪ { ( 𝑗 + 1 ) } ) ( 𝑊 ‘ 𝑘 ) = ( ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ∪ ( 𝑊 ‘ ( 𝑗 + 1 ) ) )
173 167 172 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ( 𝑊 ‘ 𝑘 ) = ( ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ∪ ( 𝑊 ‘ ( 𝑗 + 1 ) ) ) )
174 173 fveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ( 𝑊 ‘ 𝑘 ) ) = ( ♯ ‘ ( ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ∪ ( 𝑊 ‘ ( 𝑗 + 1 ) ) ) ) )
175 hashun2 ⊢ ( ( ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ∈ Fin ∧ ( 𝑊 ‘ ( 𝑗 + 1 ) ) ∈ Fin ) → ( ♯ ‘ ( ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ∪ ( 𝑊 ‘ ( 𝑗 + 1 ) ) ) ) ≤ ( ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ) + ( ♯ ‘ ( 𝑊 ‘ ( 𝑗 + 1 ) ) ) ) )
176 80 151 175 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ♯ ‘ ( ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ∪ ( 𝑊 ‘ ( 𝑗 + 1 ) ) ) ) ≤ ( ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ) + ( ♯ ‘ ( 𝑊 ‘ ( 𝑗 + 1 ) ) ) ) )
177 174 176 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ) + ( ♯ ‘ ( 𝑊 ‘ ( 𝑗 + 1 ) ) ) ) )
178 85 148 nndivred ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑁 / ( 𝑗 + 1 ) ) ∈ ℝ )
179 flle ⊢ ( ( 𝑁 / ( 𝑗 + 1 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝑁 / ( 𝑗 + 1 ) ) ) ≤ ( 𝑁 / ( 𝑗 + 1 ) ) )
180 178 179 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ⌊ ‘ ( 𝑁 / ( 𝑗 + 1 ) ) ) ≤ ( 𝑁 / ( 𝑗 + 1 ) ) )
181 elfznn ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → 𝑛 ∈ ℕ )
182 181 nncnd ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → 𝑛 ∈ ℂ )
183 182 subid1d ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( 𝑛 − 0 ) = 𝑛 )
184 183 breq2d ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ( 𝑗 + 1 ) ∥ ( 𝑛 − 0 ) ↔ ( 𝑗 + 1 ) ∥ 𝑛 ) )
185 184 rabbiia ⊢ { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑗 + 1 ) ∥ ( 𝑛 − 0 ) } = { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑗 + 1 ) ∥ 𝑛 }
186 185 fveq2i ⊢ ( ♯ ‘ { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑗 + 1 ) ∥ ( 𝑛 − 0 ) } ) = ( ♯ ‘ { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑗 + 1 ) ∥ 𝑛 } )
187 1zzd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 1 ∈ ℤ )
188 3 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
189 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
190 1m1e0 ⊢ ( 1 − 1 ) = 0
191 190 fveq2i ⊢ ( ℤ≥ ‘ ( 1 − 1 ) ) = ( ℤ≥ ‘ 0 )
192 189 191 eqtr4i ⊢ ℕ0 = ( ℤ≥ ‘ ( 1 − 1 ) )
193 188 192 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( 1 − 1 ) ) )
194 193 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( 1 − 1 ) ) )
195 0zd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 0 ∈ ℤ )
196 148 187 194 195 hashdvds ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ♯ ‘ { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑗 + 1 ) ∥ ( 𝑛 − 0 ) } ) = ( ( ⌊ ‘ ( ( 𝑁 − 0 ) / ( 𝑗 + 1 ) ) ) − ( ⌊ ‘ ( ( ( 1 − 1 ) − 0 ) / ( 𝑗 + 1 ) ) ) ) )
197 125 subid1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑁 − 0 ) = 𝑁 )
198 197 fvoveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ⌊ ‘ ( ( 𝑁 − 0 ) / ( 𝑗 + 1 ) ) ) = ( ⌊ ‘ ( 𝑁 / ( 𝑗 + 1 ) ) ) )
199 190 oveq1i ⊢ ( ( 1 − 1 ) − 0 ) = ( 0 − 0 )
200 0m0e0 ⊢ ( 0 − 0 ) = 0
201 199 200 eqtri ⊢ ( ( 1 − 1 ) − 0 ) = 0
202 201 oveq1i ⊢ ( ( ( 1 − 1 ) − 0 ) / ( 𝑗 + 1 ) ) = ( 0 / ( 𝑗 + 1 ) )
203 148 nncnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑗 + 1 ) ∈ ℂ )
204 148 nnne0d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑗 + 1 ) ≠ 0 )
205 203 204 div0d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 0 / ( 𝑗 + 1 ) ) = 0 )
206 202 205 syl5eq ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( ( 1 − 1 ) − 0 ) / ( 𝑗 + 1 ) ) = 0 )
207 206 fveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ⌊ ‘ ( ( ( 1 − 1 ) − 0 ) / ( 𝑗 + 1 ) ) ) = ( ⌊ ‘ 0 ) )
208 0z ⊢ 0 ∈ ℤ
209 flid ⊢ ( 0 ∈ ℤ → ( ⌊ ‘ 0 ) = 0 )
210 208 209 ax-mp ⊢ ( ⌊ ‘ 0 ) = 0
211 207 210 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ⌊ ‘ ( ( ( 1 − 1 ) − 0 ) / ( 𝑗 + 1 ) ) ) = 0 )
212 198 211 oveq12d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( ⌊ ‘ ( ( 𝑁 − 0 ) / ( 𝑗 + 1 ) ) ) − ( ⌊ ‘ ( ( ( 1 − 1 ) − 0 ) / ( 𝑗 + 1 ) ) ) ) = ( ( ⌊ ‘ ( 𝑁 / ( 𝑗 + 1 ) ) ) − 0 ) )
213 178 flcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ⌊ ‘ ( 𝑁 / ( 𝑗 + 1 ) ) ) ∈ ℤ )
214 213 zcnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ⌊ ‘ ( 𝑁 / ( 𝑗 + 1 ) ) ) ∈ ℂ )
215 214 subid1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( ⌊ ‘ ( 𝑁 / ( 𝑗 + 1 ) ) ) − 0 ) = ( ⌊ ‘ ( 𝑁 / ( 𝑗 + 1 ) ) ) )
216 196 212 215 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ♯ ‘ { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑗 + 1 ) ∥ ( 𝑛 − 0 ) } ) = ( ⌊ ‘ ( 𝑁 / ( 𝑗 + 1 ) ) ) )
217 186 216 eqtr3id ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ♯ ‘ { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑗 + 1 ) ∥ 𝑛 } ) = ( ⌊ ‘ ( 𝑁 / ( 𝑗 + 1 ) ) ) )
218 125 203 204 divrecd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑁 / ( 𝑗 + 1 ) ) = ( 𝑁 · ( 1 / ( 𝑗 + 1 ) ) ) )
219 218 eqcomd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑁 · ( 1 / ( 𝑗 + 1 ) ) ) = ( 𝑁 / ( 𝑗 + 1 ) ) )
220 180 217 219 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ♯ ‘ { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑗 + 1 ) ∥ 𝑛 } ) ≤ ( 𝑁 · ( 1 / ( 𝑗 + 1 ) ) ) )
221 220 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑗 + 1 ) ∈ ℙ ) → ( ♯ ‘ { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑗 + 1 ) ∥ 𝑛 } ) ≤ ( 𝑁 · ( 1 / ( 𝑗 + 1 ) ) ) )
222 eleq1 ⊢ ( 𝑝 = ( 𝑗 + 1 ) → ( 𝑝 ∈ ℙ ↔ ( 𝑗 + 1 ) ∈ ℙ ) )
223 breq1 ⊢ ( 𝑝 = ( 𝑗 + 1 ) → ( 𝑝 ∥ 𝑛 ↔ ( 𝑗 + 1 ) ∥ 𝑛 ) )
224 222 223 anbi12d ⊢ ( 𝑝 = ( 𝑗 + 1 ) → ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛 ) ↔ ( ( 𝑗 + 1 ) ∈ ℙ ∧ ( 𝑗 + 1 ) ∥ 𝑛 ) ) )
225 224 rabbidv ⊢ ( 𝑝 = ( 𝑗 + 1 ) → { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛 ) } = { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( ( 𝑗 + 1 ) ∈ ℙ ∧ ( 𝑗 + 1 ) ∥ 𝑛 ) } )
226 67 rabex ⊢ { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( ( 𝑗 + 1 ) ∈ ℙ ∧ ( 𝑗 + 1 ) ∥ 𝑛 ) } ∈ V
227 225 7 226 fvmpt ⊢ ( ( 𝑗 + 1 ) ∈ ℕ → ( 𝑊 ‘ ( 𝑗 + 1 ) ) = { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( ( 𝑗 + 1 ) ∈ ℙ ∧ ( 𝑗 + 1 ) ∥ 𝑛 ) } )
228 148 227 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑊 ‘ ( 𝑗 + 1 ) ) = { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( ( 𝑗 + 1 ) ∈ ℙ ∧ ( 𝑗 + 1 ) ∥ 𝑛 ) } )
229 228 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑗 + 1 ) ∈ ℙ ) → ( 𝑊 ‘ ( 𝑗 + 1 ) ) = { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( ( 𝑗 + 1 ) ∈ ℙ ∧ ( 𝑗 + 1 ) ∥ 𝑛 ) } )
230 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑗 + 1 ) ∈ ℙ ) → ( 𝑗 + 1 ) ∈ ℙ )
231 230 biantrurd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑗 + 1 ) ∈ ℙ ) → ( ( 𝑗 + 1 ) ∥ 𝑛 ↔ ( ( 𝑗 + 1 ) ∈ ℙ ∧ ( 𝑗 + 1 ) ∥ 𝑛 ) ) )
232 231 rabbidv ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑗 + 1 ) ∈ ℙ ) → { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑗 + 1 ) ∥ 𝑛 } = { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( ( 𝑗 + 1 ) ∈ ℙ ∧ ( 𝑗 + 1 ) ∥ 𝑛 ) } )
233 229 232 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑗 + 1 ) ∈ ℙ ) → ( 𝑊 ‘ ( 𝑗 + 1 ) ) = { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑗 + 1 ) ∥ 𝑛 } )
234 233 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑗 + 1 ) ∈ ℙ ) → ( ♯ ‘ ( 𝑊 ‘ ( 𝑗 + 1 ) ) ) = ( ♯ ‘ { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( 𝑗 + 1 ) ∥ 𝑛 } ) )
235 iftrue ⊢ ( ( 𝑗 + 1 ) ∈ ℙ → if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) = ( 1 / ( 𝑗 + 1 ) ) )
236 235 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑗 + 1 ) ∈ ℙ ) → if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) = ( 1 / ( 𝑗 + 1 ) ) )
237 236 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑗 + 1 ) ∈ ℙ ) → ( 𝑁 · if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) ) = ( 𝑁 · ( 1 / ( 𝑗 + 1 ) ) ) )
238 221 234 237 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝑗 + 1 ) ∈ ℙ ) → ( ♯ ‘ ( 𝑊 ‘ ( 𝑗 + 1 ) ) ) ≤ ( 𝑁 · if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) ) )
239 36 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ¬ ( 𝑗 + 1 ) ∈ ℙ ) → 0 ≤ 0 )
240 simpl ⊢ ( ( ( 𝑗 + 1 ) ∈ ℙ ∧ ( 𝑗 + 1 ) ∥ 𝑛 ) → ( 𝑗 + 1 ) ∈ ℙ )
241 240 con3i ⊢ ( ¬ ( 𝑗 + 1 ) ∈ ℙ → ¬ ( ( 𝑗 + 1 ) ∈ ℙ ∧ ( 𝑗 + 1 ) ∥ 𝑛 ) )
242 241 ralrimivw ⊢ ( ¬ ( 𝑗 + 1 ) ∈ ℙ → ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ¬ ( ( 𝑗 + 1 ) ∈ ℙ ∧ ( 𝑗 + 1 ) ∥ 𝑛 ) )
243 rabeq0 ⊢ ( { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( ( 𝑗 + 1 ) ∈ ℙ ∧ ( 𝑗 + 1 ) ∥ 𝑛 ) } = ∅ ↔ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ¬ ( ( 𝑗 + 1 ) ∈ ℙ ∧ ( 𝑗 + 1 ) ∥ 𝑛 ) )
244 242 243 sylibr ⊢ ( ¬ ( 𝑗 + 1 ) ∈ ℙ → { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ( ( 𝑗 + 1 ) ∈ ℙ ∧ ( 𝑗 + 1 ) ∥ 𝑛 ) } = ∅ )
245 228 244 sylan9eq ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ¬ ( 𝑗 + 1 ) ∈ ℙ ) → ( 𝑊 ‘ ( 𝑗 + 1 ) ) = ∅ )
246 245 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ¬ ( 𝑗 + 1 ) ∈ ℙ ) → ( ♯ ‘ ( 𝑊 ‘ ( 𝑗 + 1 ) ) ) = ( ♯ ‘ ∅ ) )
247 246 51 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ¬ ( 𝑗 + 1 ) ∈ ℙ ) → ( ♯ ‘ ( 𝑊 ‘ ( 𝑗 + 1 ) ) ) = 0 )
248 iffalse ⊢ ( ¬ ( 𝑗 + 1 ) ∈ ℙ → if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) = 0 )
249 248 oveq2d ⊢ ( ¬ ( 𝑗 + 1 ) ∈ ℙ → ( 𝑁 · if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) ) = ( 𝑁 · 0 ) )
250 38 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑁 · 0 ) = 0 )
251 249 250 sylan9eqr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ¬ ( 𝑗 + 1 ) ∈ ℙ ) → ( 𝑁 · if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) ) = 0 )
252 239 247 251 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ¬ ( 𝑗 + 1 ) ∈ ℙ ) → ( ♯ ‘ ( 𝑊 ‘ ( 𝑗 + 1 ) ) ) ≤ ( 𝑁 · if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) ) )
253 238 252 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ♯ ‘ ( 𝑊 ‘ ( 𝑗 + 1 ) ) ) ≤ ( 𝑁 · if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) ) )
254 154 101 83 253 leadd2dd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ) + ( ♯ ‘ ( 𝑊 ‘ ( 𝑗 + 1 ) ) ) ) ≤ ( ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ) + ( 𝑁 · if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) ) ) )
255 141 155 156 177 254 letrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ) + ( 𝑁 · if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) ) ) )
256 fzfid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ∈ Fin )
257 62 92 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ) → if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ∈ ℝ )
258 105 106 257 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ) → if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ∈ ℝ )
259 256 258 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ∈ ℝ )
260 85 259 remulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ∈ ℝ )
261 letr ⊢ ( ( ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 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 ) ) ) )
262 141 156 260 261 syl3anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 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 ) ) ) )
263 255 262 mpand ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ) + ( 𝑁 · if ( ( 𝑗 + 1 ) ∈ ℙ , ( 1 / ( 𝑗 + 1 ) ) , 0 ) ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ) )
264 131 263 sylbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ) )
265 264 expcom ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) → ( 𝜑 → ( ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ) ) )
266 265 a2d ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝐾 ) → ( ( 𝜑 → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑗 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ) → ( 𝜑 → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... ( 𝑗 + 1 ) ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ) ) )
267 14 21 28 35 57 266 uzind4i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → ( 𝜑 → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ) )
268 267 com12 ⊢ ( 𝜑 → ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → ( ♯ ‘ ∪ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( 𝑊 ‘ 𝑘 ) ) ≤ ( 𝑁 · Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) if ( 𝑘 ∈ ℙ , ( 1 / 𝑘 ) , 0 ) ) ) )