∀ {R : Type u_1} [inst : NormedCommRing R] {f : ℕ → R} [CompleteSpace R],
  Summable f →
    f 0 = 0 →
      ∀ {ε : ℝ},
        0 < ε →
          ∃ N, ∀ (s : Finset ℕ), N.primesBelow ≤ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(Nat.factoredNumbers s)), f ↑m‖ < ε