convert integrableOn_of_Zeta0_fun (s := σ + t * I) Npos (by simp [σpos]) using 1
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ IntegrableOn (fun a => (↑⌊a⌋ + 1 / 2 - ↑a) / ↑a ^ (↑σ + ↑t * I + 1)) (Ioi ↑N) volume
case h.e'_5
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ (fun a => (↑⌊a⌋ + 1 / 2 - ↑a) / ↑a ^ (↑σ + ↑t * I + 1)) = fun x => (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(↑σ + ↑t * I + 1))