Theorem: riemannZeta0_apply (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
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)))
Tactic:
simp_rw [riemannZeta0, div_cpow_eq_cpow_neg]
State after:
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)))

State before:
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)))
Tactic:
ring
State after:
no goals