simp only [mul_eq_mul_right_iff, abs_eq_zero, Real.log_eq_zero]
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
⊢ (fun x => |x ^ (-s.re - 1)| * |x.log|) x = (fun a => Complex.abs (↑a ^ (-s - 1)) * |a.log|) x
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)) ∨ x = 0 ∨ x = 1 ∨ x = -1