Proof of Coordinate Bounds Control the Euclidean Norm

For a real number $s$ write $s^{2}$ for $s\cdot s$. All finite sums below are the finite sums of families indexed by $[n]$, and $u^{n}:[n]\to\mathbb{R}$ denotes the constant family with value $1$ appearing in The Canonical Map from the Natural Numbers to a Field, so that $\iota(n)=\sum_{i=1}^{n}u^{n}_{i}$. Rearrangements of products use the commutativity and associativity of multiplication in the field $\mathbb{R}$ and the identity $a\cdot 1=a$.

Step 1: each coordinate square is at most $t^{2}$. Let $i\in[n]$. Statement 1 of Properties of the Absolute Value in an Ordered Field gives $0\le|x_i|$, and by hypothesis $|x_i|\le t$ with $0\le t$. Statement 2 of Monotonicity of Squaring on the Nonnegative Elements of an Ordered Field therefore gives $|x_i|^{2}\le t^{2}$. Statement 4 of Properties of the Absolute Value in an Ordered Field gives $|x_i|^{2}=|x_i|\,|x_i|=|x_i\,x_i|=|x_i^{2}|$, and statement 3 of the same result gives $x_i^{2}\le|x_i^{2}|$. By transitivity of $\le$,

Step 2: the sum of the coordinate squares. Let $a:[n]\to\mathbb{R}$ and $b:[n]\to\mathbb{R}$ be the families $a_i=x_i^{2}$ and $b_i=t^{2}$. Since $b_i=t^{2}\,u^{n}_{i}$, claim 3 of Properties of Finite Sums gives

Let $c:[n]\to\mathbb{R}$ be the family $c_i=b_i+(-1)a_i$. Statement 2 of Zero Products and Elementary Identities in a Field gives $(-1)a_i=-a_i$, so $c_i=b_i-a_i$, and Step 1 together with statement 3 of Elementary Arithmetic in an Ordered Field gives $0\le c_i$ for every $i\in[n]$. Claim 5 of Properties of Finite Sums then gives $0\le\sum_{i=1}^{n}c_i$. On the other hand claims 2 and 3 of the same result give

using statement 2 of Zero Products and Elementary Identities in a Field once more. Applying statement 3 of Elementary Arithmetic in an Ordered Field in the other direction we conclude

Step 3: comparison with the square of the asserted bound. Statement 2 of Properties of the Canonical Map from the Natural Numbers to an Ordered Field gives $1\le\iota(n)$ and statement 3 gives $0<\iota(n)$, hence $0\le\iota(n)$. Statement 5 of Elementary Arithmetic in an Ordered Field applied to $1\le\iota(n)$ and $0\le\iota(n)$ gives $\iota(n)\cdot 1\le\iota(n)\,\iota(n)$, that is, $\iota(n)\le\iota(n)^{2}$. By Nonnegativity of Squares in an Ordered Field we have $0\le t^{2}$, so statement 5 of Elementary Arithmetic in an Ordered Field gives $t^{2}\,\iota(n)\le t^{2}\,\iota(n)^{2}$. Since $t^{2}\,\iota(n)^{2}=(\iota(n)\,t)^{2}$, transitivity and Step 2 give

Step 4: conclusion. Statement 1 of Elementary Properties of the Euclidean Norm on $\mathbb{R}^n$ gives $0\le\lVert x\rVert$ and $\lVert x\rVert^{2}=\sum_{i=1}^{n}x_i^{2}$, so Step 3 gives $\lVert x\rVert^{2}\le(\iota(n)\,t)^{2}$. Moreover $0\le\iota(n)\,t$: indeed statement 5 of Elementary Arithmetic in an Ordered Field applied to $0\le t$ and $0\le\iota(n)$ gives $\iota(n)\cdot 0\le\iota(n)\,t$, and $\iota(n)\cdot 0=0$ by statement 1 of Zero Products and Elementary Identities in a Field. Both $\lVert x\rVert$ and $\iota(n)\,t$ being nonnegative, statement 2 of Monotonicity of Squaring on the Nonnegative Elements of an Ordered Field yields

as asserted.