exact continuousOn_id.rpow_const fun x hx ↦ Or.inl (ne_of_gt <| ZetaSum_aux1_1' apos hx)
case refine_1
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ ContinuousOn (fun u => u ^ (s.re + 1)) (Icc a b)
no goals