∀ {k : ℕ},
  k ≠ 0 →
    ∀ {x : ℝ},
      x ∈ Set.Icc 0 1 →
        HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * Real.sin (2 * Real.pi * ↑n * x))
          ((-1) ^ (k + 1) * (2 * Real.pi) ^ (2 * k + 1) / 2 / ↑(2 * k + 1).factorial *
            Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))