exact MeasureTheory.intervalIntegral_tendsto_integral_Ioi (a := N)
  (b := (fun (n : ℕ) ↦ (n : ℝ))) (integrableOn_of_Zeta0_fun N_pos <| by positivity) tendsto_coe_atTop
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ Tendsto (fun k => ∫ (x : ℝ) in ↑N..↑k, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))) atTop
    (𝓝 (∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))))
no goals