ext k
case h.e'_3
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ (fun k => ∑ x ∈ Finset.Ico (N + 1) (k + 1), 1 / ↑x ^ s) = fun k => ∑ n ∈ Finset.Ico N k, f (n + 1)
case h.e'_3.h
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
k : ℕ
⊢ ∑ x ∈ Finset.Ico (N + 1) (k + 1), 1 / ↑x ^ s = ∑ n ∈ Finset.Ico N k, f (n + 1)