let f := fun (n : ℕ) ↦ 1 / (n : ℂ) ^ s
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ioc N k, 1 / ↑n ^ s) atTop (𝓝 (∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s))
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ioc N k, 1 / ↑n ^ s) atTop (𝓝 (∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s))