intro n _
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ ∀ i ∈ Finset.range (N + 1), HasDerivAt (fun x => 1 / ↑i ^ x) (-1 / ↑i ^ s * ↑(↑i).log) s
N : ℕ
Npos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
n : ℕ
a✝ : n ∈ Finset.range (N + 1)
⊢ HasDerivAt (fun x => 1 / ↑n ^ x) (-1 / ↑n ^ s * ↑(↑n).log) s