If $f$ has a vanishing (first or higher) derivative at every point, $f$ is a polynomial

There's a problem from calculus I remember: $$\forall x\ \exists n.\ f^{(n)}(x) = 0 \iff \exists n\ \forall x.\ f^{(n)}(x) = 0\,.$$

Function $f \in C^\infty(\mathbb{R})$, and the notation $f^{(n)}$ means differentiation.

Right side is just curious statement that $f$ is a polynomial. Of course $(\Leftarrow)$ is just trivial, however, $(\Rightarrow)$ is far from obvious. Have anybody seen this, maybe somebody knows where it comes from? What about the proof of $(\Rightarrow)$?


Here are some reference about the problem:

  • this thread at Math Overflow;
  • Robert Israel's solution.