Proof of Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square

Each result cited is universally quantified over the data in its own statement.

Throughout, $\mathbb{R}$ is an ordered field, so the rules of arithmetic and order of Rules of Arithmetic and Order in an Ordered Field, carried by Commutative Rings, Fields and Ordered Fields: Standard Notation §ordered-fields, are used without further citation. For $a\in\mathbb{R}$ we have $a^{2}=a\,a$, since $2=1+1$ by Arithmetic and Order of the Natural Numbers §digits, $a^{1+1}=a^{1}a^{1}$ by Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §exponents and $a^{1}=a$ by Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §product; moreover $2=1+1$ in $\mathbb{R}$ by Commutative Rings, Fields and Ordered Fields: Standard Notation §numerals and Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima §two, so $b+b=2b$ for $b\in\mathbb{R}$, and $2>0$ since $0<1+1$. Also $|a|^{2}=|a^{2}|=a^{2}$ for every $a\in\mathbb{R}$, where $|a|\in\mathbb{R}$ by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima §absolute-value: the first equality is Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §sign, and the second holds by Absolute Value in an Ordered Field §absolute-value because $a^{2}=a\,a\ge0$.

For $u,v\in\mathbb{R}^{n}$ and $t\in\mathbb{R}$, the elements $u+v$, $u-v$, $-u$ and $tu$ lie in $\mathbb{R}^{n}=\mathbb{R}^{[n]}$ by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §operations and Pointwise Operations on Real-Valued Maps §operations, and their components are given by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §operations. Two elements of $\mathbb{R}^{n}$ with the same components are equal by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §equality; the origin $0$ has every component $0$ by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §origin and Pointwise Operations on Real-Valued Maps §constants. In particular, comparing components, for $u,v\in\mathbb{R}^{n}$:

$$u-0=u,\qquad u-(u+v)=-v,\qquad (u-v)+v=u,\qquad v-u=-(u-v),\qquad -u=(-1)u,$$

since, for each $k\in[n]$, $u_{k}-0=u_{k}$, $u_{k}-(u_{k}+v_{k})=-v_{k}$, $(u_{k}-v_{k})+v_{k}=u_{k}$, $v_{k}-u_{k}=-(u_{k}-v_{k})$ and $(-1)u_{k}=-u_{k}$.

Clause square. By The Dot Product on $\mathbb{R}^n$ Is Symmetric, Bilinear and Positive Definite §nonnegative, $x\cdot x=\sum_{k=1}^{n}x_{k}^{2}\ge0$. By The Euclidean Norm on $\mathbb{R}^n$ §norm, The k-th Root and the Square Root of a Nonnegative Real Number §square-root and The k-th Root and the Square Root of a Nonnegative Real Number §root, $\lVert x\rVert=\sqrt{x\cdot x}$ is the real number $y\ge0$ with $y^{2}=x\cdot x$, and by Existence and Uniqueness of Nonnegative k-th Roots of Nonnegative Real Numbers §root there is exactly one such $y$. Hence $\lVert x\rVert\ge0$, $\lVert x\rVert^{2}=x\cdot x=\sum_{k=1}^{n}x_{k}^{2}$, and $\lVert x\rVert$ is the only nonnegative real number whose square is $x\cdot x$. We refer to the last statement as uniqueness: for $u\in\mathbb{R}^{n}$ and $r\in\mathbb{R}$, if $r\ge0$ and $r^{2}=u\cdot u$, then $r=\lVert u\rVert$.

Clause vanishing. If $\lVert x\rVert=0$, then $x\cdot x=\lVert x\rVert^{2}=0^{2}=0$, by the clause square and Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §product. Conversely, if $x\cdot x=0$, then $0\ge0$ and $0^{2}=0=x\cdot x$, so $\lVert x\rVert=0$ by uniqueness. Thus $\lVert x\rVert=0$ if and only if $x\cdot x=0$, which holds if and only if $x=0$ by The Dot Product on $\mathbb{R}^n$ Is Symmetric, Bilinear and Positive Definite §definite.

Clause homogeneity. By The Dot Product on $\mathbb{R}^n$ Is Symmetric, Bilinear and Positive Definite §first (with $z=tx$) and The Dot Product on $\mathbb{R}^n$ Is Symmetric, Bilinear and Positive Definite §second (with $z=x$),

$$(tx)\cdot(tx)=t\,\bigl(x\cdot(tx)\bigr)=t\,\bigl(t\,(x\cdot x)\bigr)=t^{2}\,(x\cdot x).$$

Let $r=|t|\,\lVert x\rVert$; then $r\ge0$ as a product of nonnegative reals ($|t|\in\mathbb{R}$ by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima §absolute-value and $|t|\ge0$, and $\lVert x\rVert\ge0$ by the clause square). By Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §product and the preliminary remarks, $r^{2}=|t|^{2}\,\lVert x\rVert^{2}=t^{2}\,(x\cdot x)=(tx)\cdot(tx)$. By uniqueness applied to $u=tx$, $\lVert tx\rVert=r=|t|\,\lVert x\rVert$. Since $-x=(-1)x$ and $|-1|=|1|=1$, with $-1\in\mathbb{R}$ by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima §negative, this gives $\lVert -x\rVert=\lVert x\rVert$.

Clause distance. By The Euclidean Distance on $\mathbb{R}^n$ §distance, $d_{E}(x,y)=\lVert x-y\rVert$. By the clause square applied to $x-y$, and since $(x-y)_{k}=x_{k}-y_{k}$ for every $k\in[n]$,

$$d_{E}(x,y)^{2}=\lVert x-y\rVert^{2}=\sum_{k=1}^{n}(x-y)_{k}^{2}=\sum_{k=1}^{n}(x_{k}-y_{k})^{2}.$$

Further $d_{E}(x,0)=\lVert x-0\rVert=\lVert x\rVert$, and $d_{E}(x,x+y)=\lVert x-(x+y)\rVert=\lVert -y\rVert=\lVert y\rVert$ by the clause homogeneity.

Clause expansion. By the clause square applied to $x+y$, then The Dot Product on $\mathbb{R}^n$ Is Symmetric, Bilinear and Positive Definite §first (with $z=x+y$), The Dot Product on $\mathbb{R}^n$ Is Symmetric, Bilinear and Positive Definite §second (with $z=x$ and with $z=y$) and The Dot Product on $\mathbb{R}^n$ Is Symmetric, Bilinear and Positive Definite §symmetric,

$$\lVert x+y\rVert^{2}=(x+y)\cdot(x+y)=x\cdot(x+y)+y\cdot(x+y)=x\cdot x+x\cdot y+y\cdot x+y\cdot y=\lVert x\rVert^{2}+2\,(x\cdot y)+\lVert y\rVert^{2},$$

using $x\cdot y+y\cdot x=x\cdot y+x\cdot y=2\,(x\cdot y)$ and the clause square for $x$ and $y$. If $x\cdot y=0$, then $2\,(x\cdot y)=0$ and $\lVert x+y\rVert^{2}=\lVert x\rVert^{2}+\lVert y\rVert^{2}$.

Clause triangle. By Rules of Arithmetic and Order in an Ordered Field §absolute-value and The Cauchy-Schwarz Inequality on $\mathbb{R}^n$ §cauchy-schwarz, $x\cdot y\le|x\cdot y|\le\lVert x\rVert\,\lVert y\rVert$, and as $2>0$, $2\,(x\cdot y)\le2\,\lVert x\rVert\,\lVert y\rVert$. Hence, by the clause expansion and The Square and the Fourth Power of a Sum §square (in the commutative ring $\mathbb{R}$),

$$\lVert x+y\rVert^{2}=\lVert x\rVert^{2}+2\,(x\cdot y)+\lVert y\rVert^{2}\le\lVert x\rVert^{2}+2\,\lVert x\rVert\,\lVert y\rVert+\lVert y\rVert^{2}=\bigl(\lVert x\rVert+\lVert y\rVert\bigr)^{2}.$$

Both $\lVert x+y\rVert$ and $\lVert x\rVert+\lVert y\rVert$ are nonnegative by the clause square, so Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §monotone-iff (with exponent $2\ge1$) gives $\lVert x+y\rVert\le\lVert x\rVert+\lVert y\rVert$.

Clause reverse-triangle. Since $x=(x-y)+y$, the clause triangle gives $\lVert x\rVert\le\lVert x-y\rVert+\lVert y\rVert$, that is $\lVert x\rVert-\lVert y\rVert\le\lVert x-y\rVert$. Likewise $y=(y-x)+x$ gives $\lVert y\rVert-\lVert x\rVert\le\lVert y-x\rVert$, and $\lVert y-x\rVert=\lVert-(x-y)\rVert=\lVert x-y\rVert$ by the clause homogeneity. So $-\lVert x-y\rVert\le\lVert x\rVert-\lVert y\rVert\le\lVert x-y\rVert$, and Rules of Arithmetic and Order in an Ordered Field §absolute-value gives $\bigl|\lVert x\rVert-\lVert y\rVert\bigr|\le\lVert x-y\rVert$.

Clause coordinate. Let $k\in[n]$. By the preliminary remarks, The Dot Product on $\mathbb{R}^n$ Is Symmetric, Bilinear and Positive Definite §coordinate-square and the clause square, $|x_{k}|^{2}=x_{k}^{2}\le x\cdot x=\lVert x\rVert^{2}$; as $|x_{k}|\ge0$ and $\lVert x\rVert\ge0$, Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §monotone-iff (exponent $2$) gives $|x_{k}|\le\lVert x\rVert$.

For the second inequality let $S=\sum_{j=1}^{n}|x_{j}|$. The maps $j\mapsto|x_{j}|$, $j\mapsto S\,|x_{j}|$ and $j\mapsto|x_{j}|\,|x_{j}|$ to which the finite-sum lemmas are applied below, and the constant map $j\mapsto s$ of the last paragraph, are maps from $[n]$ to $\mathbb{R}$ by Sets and Maps: Ordinary Notation §maps, their values lying in $\mathbb{R}$ by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima §absolute-value (for $S\,|x_{j}|$ with $S\in\mathbb{R}$, which holds by Iterated Operations and Operations over Finite Sets Take Values in the Underlying Set §segment-sums applied to $j\mapsto|x_{j}|$) and their defining conditions being predicative by Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field §value-substitution, Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field §operation-substitution and Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field §absolute-value-formula. Since $|x_{j}|\ge0$ for every $j\in[n]$, Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality §nonnegative gives $S\ge0$ and $|x_{j}|\le S$ for every $j\in[n]$. For each $j\in[n]$ we have $|x_{j}|\,|x_{j}|\le S\,|x_{j}|$: if $|x_{j}|=0$ both sides are $0$, and otherwise $|x_{j}|>0$ and this follows from $|x_{j}|\le S$ by Rules of Arithmetic and Order in an Ordered Field §order-product. Hence, by Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality §distributive (with $c=S$), Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality §comparison, the preliminary remarks and the clause square,

$$S^{2}=S\sum_{j=1}^{n}|x_{j}|=\sum_{j=1}^{n}S\,|x_{j}|\ge\sum_{j=1}^{n}|x_{j}|\,|x_{j}|=\sum_{j=1}^{n}x_{j}^{2}=\lVert x\rVert^{2},$$

the equality $|x_{j}|\,|x_{j}|=|x_{j}|^{2}=x_{j}^{2}$ holding termwise. As $S\ge0$ and $\lVert x\rVert\ge0$, Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §monotone-iff (exponent $2$) gives $\lVert x\rVert\le S$.

Finally let $s\in\mathbb{R}$ with $|x_{k}|\le s$ for every $k\in[n]$. By Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality §comparison and Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality §constant, $\sum_{j=1}^{n}|x_{j}|\le\sum_{j=1}^{n}s=n\,s$, so $\lVert x\rVert\le n\,s$ by the bound just proved.