rw [← Finset.sum_filter]
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
⊢ (∑ i ∈ Finset.range n, if IsPrimePow i then (↑i).log else 0) ≤
    ∑ _i ∈ Finset.filter IsPrimePow (Finset.range n), (↑n).log
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hC : ∀ (N : ℕ), ↑(Finset.filter IsPrimePow (Finset.range N)).card ≤ C * (↑N / (↑N).log)
hC_nonneg : 0 ≤ C
n : ℕ
⊢ ∑ a ∈ Finset.filter (fun i => IsPrimePow i) (Finset.range n), (↑a).log ≤
    ∑ _i ∈ Finset.filter IsPrimePow (Finset.range n), (↑n).log