have xpos : 0 < x := by linarith [mem_Ioi.mp hx]
case h
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
x : ℝ
hx : x ∈ Ioi ↑N
⊢ |x ^ (-s.re - 1)| = Complex.abs (↑x ^ (-s - 1))
case h
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
x : ℝ
hx : x ∈ Ioi ↑N
xpos : 0 < x
⊢ |x ^ (-s.re - 1)| = Complex.abs (↑x ^ (-s - 1))