simp_rw [riemannZeta0, div_cpow_eq_cpow_neg]
N : ℕ
s : ℂ
⊢ ζ₀ N s =
    ∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ s +
      (-↑N ^ (1 - s) / (1 - s) + -↑N ^ (-s) / 2 + s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)))
N : ℕ
s : ℂ
⊢ ∑ x ∈ Finset.range (N + 1), 1 * ↑x ^ (-s) + -↑N ^ (1 - s) / (1 - s) + -↑N ^ (-s) / 2 +
      s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)) =
    ∑ x ∈ Finset.range (N + 1), 1 * ↑x ^ (-s) +
      (-↑N ^ (1 - s) / (1 - s) + -↑N ^ (-s) / 2 + s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)))