have l5 (σ' : ℝ) (hσ' : 1 < σ') : Summable (nterm Λ σ') := by
  simpa only [← nterm_eq_norm_term] using (@ArithmeticFunction.LSeriesSummable_vonMangoldt σ' hσ').norm
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
l2 : ∀ (s : ℂ), 1 < s.re → (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
l3 : ContinuousOn (-deriv ζ₁ / ζ₁) {s | 1 ≤ s.re}
l4 : cheby fun n => ↑(Λ n)
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hnv : ∀ ⦃z : ℂ⦄, z ≠ 1 → 1 ≤ z.re → riemannZeta z ≠ 0
l1 : ∀ (n : ℕ), 0 ≤ Λ n
l2 : ∀ (s : ℂ), 1 < s.re → (-deriv ζ₁ / ζ₁) s = LSeries (fun n => ↑(Λ n)) s - 1 / (s - 1)
l3 : ContinuousOn (-deriv ζ₁ / ζ₁) {s | 1 ≤ s.re}
l4 : cheby fun n => ↑(Λ n)
l5 : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(Λ n)) σ')
⊢ Tendsto (fun N => cumsum (⇑Λ) N / ↑N) atTop (𝓝 1)