Proof of Polynomial Functions on the Real Line are Smooth

Throughout, $S$ is the successor map of Natural Numbers and $[N]$ is the initial segment determined by $N$; real-valued functions are treated as maps into $\mathbb{R}^{1}$ according to the scalar convention of clause 3 of C^k Maps on a Euclidean Open Set.

Claim 1. By Open Subset of Euclidean Space, a subset of $\mathbb{R}^{1}$ is open when each of its points admits a positive radius $r$ such that every point of $\mathbb{R}^{1}$ within that radius of it again lies in the subset. For the subset $\mathbb{R}^{1}$ itself take $r=1$, which is positive by claim 6 of Elementary Order Arithmetic in an Ordered Field; the required containment holds because every point of $\mathbb{R}^{1}$ lies in $\mathbb{R}^{1}$. Hence $\mathbb{R}^{1}$ is open in $\mathbb{R}^{1}$.

Claim 2. Let $U$ be an open subset of $\mathbb{R}^{1}$. Under the identification of $\mathbb{R}$ with $\mathbb{R}^{1}$, the first coordinate function $\pi_{1}:U\to\mathbb{R}$, $\pi_{1}(x)=x_{1}$, of claim 2 of Constants, Coordinate Functions, Sums and Products of $C^k$ Functions on a Euclidean Open Set is the map $x\mapsto x$ on $U$; by that claim it is smooth on $U$, as is every constant function on $U$.

Step A (powers). We show that for every $n\in\mathbb{N}$ the function $U\to\mathbb{R}$, $x\mapsto x^{n}$, with the natural number power of $\mathbb{R}$, is smooth on $U$. Let $E$ be the set of $n\in\mathbb{N}$ for which this holds. By claim 1 of Properties of Natural Number Powers in a Field, $x^{1}=x$, so the function in question for $n=1$ is $\pi_{1}$ and $1\in E$. If $n\in E$, then by the same claim $x^{S(n)}=x^{n}x$, so the function for $S(n)$ is the pointwise product of the functions for $n$ and for $1$, hence smooth on $U$ by claim 3 of Constants, Coordinate Functions, Sums and Products of $C^k$ Functions on a Euclidean Open Set; thus $S(n)\in E$. By Principle of Induction for the Natural Numbers, $E=\mathbb{N}$.

Step B (polynomial functions). Let $E'$ be the set of those $N\in\mathbb{N}$ with the following property: for every $c_{0}\in\mathbb{R}$ and every map $c:[N]\to\mathbb{R}$, the function $U\to\mathbb{R}$ given by $x\mapsto c_{0}+\sum_{k=1}^{N}c_{k}x^{k}$, with the finite sum of $\mathbb{R}$, is smooth on $U$.

For $N=1$, claim 1 of Properties of Finite Sums and claim 1 of Properties of Natural Number Powers in a Field give $c_{0}+\sum_{k=1}^{1}c_{k}x^{k}=c_{0}+c_{1}x$, the pointwise sum of a constant function and a scalar multiple of $\pi_{1}$, which is smooth on $U$ by claims 2 and 3 of Constants, Coordinate Functions, Sums and Products of $C^k$ Functions on a Euclidean Open Set. Hence $1\in E'$.

Let $N\in E'$, let $c_{0}\in\mathbb{R}$ and let $c:[S(N)]\to\mathbb{R}$. By the restriction and recursion parts of claim 1 of Properties of Finite Sums and associativity of addition,

the inner sum being formed from the restriction of $c$ to $[N]$. The first summand is smooth on $U$ because $N\in E'$, and the second is a scalar multiple of the function of Step A for the exponent $S(N)$, hence smooth on $U$ by claim 3 of Constants, Coordinate Functions, Sums and Products of $C^k$ Functions on a Euclidean Open Set; by that claim again their pointwise sum is smooth on $U$. Hence $S(N)\in E'$, and by Principle of Induction for the Natural Numbers, $E'=\mathbb{N}$.

By Polynomial Function on a Field the polynomial function $p$ has coefficients $(N,c_{0},c)$ for some $N\in\mathbb{N}$, so the restriction of $p$ to $U$ is exactly the function treated in Step B and is smooth on $U$.

Taking $U=\mathbb{R}^{1}$, which is legitimate by claim 1, shows that $p$ is smooth on $\mathbb{R}^{1}$; by Smooth Map on a Euclidean Open Set this means that $p$ is of class $C^{k}$ on $\mathbb{R}^{1}$ for every natural number $k$.