Proof of The Squared Euclidean Norm is Smooth

Throughout, $\mathbb{R}^{n}$ is open in itself by claim 1 of Euclidean Space is Open in Itself, and $C^k$ Maps are Continuous; $\mathbb{N}$ denotes the natural numbers with successor map $S$ as in that definition, ordered by the relation of that definition, whose properties are those of Properties of the Order on the Natural Numbers. Smoothness is that of Smooth Map on a Euclidean Open Set.

For $i\in\mathbb{N}$ with $1\le i\le n$ let $\pi_{i}:\mathbb{R}^{n}\to\mathbb{R}$ be the $i$th coordinate function, $\pi_{i}(y)=y_{i}$. By claim 2 of Constants, Coordinate Functions, Sums and Products of $C^k$ Functions on a Euclidean Open Set, $\pi_{i}$ is smooth on $\mathbb{R}^{n}$, and by claim 3 there so is the pointwise product $\pi_{i}\pi_{i}$, whose value at $y$ is $y_{i}^{2}$.

For $m\in\mathbb{N}$ with $m\le n$ let $q_{m}:\mathbb{R}^{n}\to\mathbb{R}$ be given by

the finite sum formed from the family on the initial segment $[n]$ whose value at $k$ is $y_{k}^{2}$; by claim 1 of Properties of Finite Sums this value does not depend on which family extending the summands is used.

Let $A$ be the set of those $m\in\mathbb{N}$ for which either $m\le n$ fails, or $m\le n$ holds and $q_{m}$ is smooth on $\mathbb{R}^{n}$. We verify the two hypotheses of Principle of Induction for the Natural Numbers.

Base. By claim 4 of Properties of the Order on the Natural Numbers we have $1\le n$. By the recursion in claim 1 of Properties of Finite Sums, $q_{1}(y)=y_{1}^{2}$ for every $y\in\mathbb{R}^{n}$, so $q_{1}$ is the function $\pi_{1}\pi_{1}$ and is therefore smooth on $\mathbb{R}^{n}$. Hence $1\in A$.

Step. Let $m\in A$. If $S(m)\le n$ fails, then $S(m)\in A$ by definition of $A$. So suppose $S(m)\le n$. By claim 5 of Properties of the Order on the Natural Numbers we have $m<S(m)$, hence $m\le S(m)$ and then $m\le n$ by claim 1 of that lemma; since $m\in A$, the function $q_{m}$ is smooth on $\mathbb{R}^{n}$. By the recursion in claim 1 of Properties of Finite Sums,

so $q_{S(m)}$ is the pointwise sum $q_{m}+\pi_{S(m)}\pi_{S(m)}$, the coordinate function $\pi_{S(m)}$ being defined because $1\le S(m)\le n$ by claim 4 of Properties of the Order on the Natural Numbers. By claims 2 and 3 of Constants, Coordinate Functions, Sums and Products of $C^k$ Functions on a Euclidean Open Set, $q_{S(m)}$ is smooth on $\mathbb{R}^{n}$. Hence $S(m)\in A$.

By Principle of Induction for the Natural Numbers, $A=\mathbb{N}$. Since $n\le n$ by claim 1 of Properties of the Order on the Natural Numbers, it follows that $q_{n}$ is smooth on $\mathbb{R}^{n}$.

Finally, claim 1 of Elementary Properties of the Euclidean Norm on $\mathbb{R}^n$ gives $\lVert y\rVert^{2}=\sum_{i=1}^{n}y_{i}^{2}$ for every $y\in\mathbb{R}^{n}$, that is, $q=q_{n}$. Therefore $q$ is smooth on $\mathbb{R}^{n}$. $\blacksquare$