have : EqOn _ (fun (t : ℝ) ↦ -s * (t : ℂ) ^ (-(s + 1))) [[a, b]] :=
  fun x hx ↦ ZetaSum_aux1φderiv s_ne_zero <| xpos_of_uIcc ha hx
s : ℂ
s_ne_zero : s ≠ 0
a b : ℕ
ha : a ∈ Ioo 0 b
⊢ ContinuousOn (deriv fun t => 1 / ↑t ^ s) [[↑a, ↑b]]
s : ℂ
s_ne_zero : s ≠ 0
a b : ℕ
ha : a ∈ Ioo 0 b
this : EqOn (fun x => deriv (fun t => 1 / ↑t ^ s) x) (fun t => -s * ↑t ^ (-(s + 1))) [[↑a, ↑b]]
⊢ ContinuousOn (deriv fun t => 1 / ↑t ^ s) [[↑a, ↑b]]