simp_rw [mul_assoc]
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ IntegrableOn (fun x => (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)) * -↑x.log) (Ioi ↑N) volume
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ IntegrableOn (fun x => (↑⌊x⌋ + 1 / 2 - ↑x) * (↑x ^ (-(s + 1)) * -↑x.log)) (Ioi ↑N) volume