Proof of Elementary Properties of the Euclidean Norm on $\mathbb{R}^n$

Notation is as in the statement. Points of Euclidean space $\mathbb{R}^n$ are ordered $n$-tuples of real numbers, two points being equal exactly when their corresponding coordinates are equal; for a point $z$ we write $z_i$ for its $i$-th coordinate. The real numbers form an ordered field, and in particular a field; its axioms of associativity, commutativity, distributivity, identities and inverses are used below without further comment.

Step 0 (Squares). Apply Nonnegativity of Squares in an Ordered Field to the ordered field of real numbers: for every real number $t$ we have $t^{2}=|t|^{2}$ by claim 1 there, and $0\le t^{2}$ by claim 2. Both are used repeatedly below.

Step 1 (The distance as a square root). Let $u=(u_1,\dots,u_n)$ and $v=(v_1,\dots,v_n)$ be points of $\mathbb{R}^n$. By Step 0 every summand $(u_i-v_i)^{2}$ is nonnegative, so claim 5 of Properties of Finite Sums gives

By the definition of the Euclidean distance, $d_E(u,v)$ is the nonnegative square root of this sum, so by Existence and Uniqueness of the Nonnegative Square Root it is the unique real number $r$ with $0\le r$ and $r^{2}=\sum_{i=1}^{n}(u_i-v_i)^{2}$.

Step 2 (Claim 1). By Step 0 every summand $x_i^{2}$ is nonnegative, so claim 5 of Properties of Finite Sums gives $0\le\sum_{i=1}^{n}x_i^{2}$, where the finite sum is formed in the field of real numbers. By the definition of the Euclidean norm, $\lVert x\rVert$ is the nonnegative square root of that sum, so by Existence and Uniqueness of the Nonnegative Square Root it is the unique real number $r$ with $0\le r$ and $r^{2}=\sum_{i=1}^{n}x_i^{2}$. In particular $0\le\lVert x\rVert$ and $\lVert x\rVert^{2}=\sum_{i=1}^{n}x_i^{2}$. Finally, by the definition of the dot product,

since $x_i^{2}$ abbreviates $x_i x_i$. This proves claim 1. The point $x$ was arbitrary, so claim 1 is available below for any point of $\mathbb{R}^n$.

Step 3 (Claim 2). By the definition of the difference of points, the $i$-th coordinate of $x-y$ is $x_i-y_i$. Applying claim 1 to the point $x-y$ shows that $\lVert x-y\rVert$ is the unique nonnegative real number whose square is $\sum_{i=1}^{n}(x_i-y_i)^{2}$, while Step 1 shows that $d_E(x,y)$ is the unique such number. Hence $d_E(x,y)=\lVert x-y\rVert$.

Taking $y=0_{\mathbb{R}^n}$ here gives $d_E(x,0_{\mathbb{R}^n})=\lVert x-0_{\mathbb{R}^n}\rVert$. Every coordinate of the origin equals $0$ and $x_i-0=x_i$ by claim 4 of Additive Cancellation and Elementary Additive Identities in a Field, so $x-0_{\mathbb{R}^n}=x$ and therefore $d_E(x,0_{\mathbb{R}^n})=\lVert x\rVert$.

For the third assertion, by the definition of the sum of points the $i$-th coordinate of $x+h$ is $x_i+h_i$, so the $i$-th coordinate of $(x+h)-x$ is

using commutativity and associativity of addition, the additive inverse axiom, and the additive identity axiom. Hence $(x+h)-x=h$, and the first assertion applied to the pair $x+h$, $x$ gives $d_E(x+h,x)=\lVert h\rVert$. By Euclidean Distance is a Metric on $\mathbb{R}^n$ the function $d_E$ is a metric on $\mathbb{R}^n$, so it is symmetric, and therefore $d_E(x,x+h)=d_E(x+h,x)=\lVert h\rVert$.

Step 4 (Claim 3). By Euclidean Distance is a Metric on $\mathbb{R}^n$ the function $d_E$ is a metric on $\mathbb{R}^n$, so by condition 2 of that definition $d_E(x,0_{\mathbb{R}^n})=0$ holds if and only if $x=0_{\mathbb{R}^n}$. Since $\lVert x\rVert=d_E(x,0_{\mathbb{R}^n})$ by the second assertion of claim 2, this is exactly claim 3.

Step 5 (Claim 4). Let $j$ be a natural number with $1\le j\le n$. By Step 0 every summand $x_i^{2}$ is nonnegative, so claim 6 of Properties of Finite Sums and claim 1 give

By Step 0 again $x_j^{2}=|x_j|^{2}$, so $|x_j|^{2}\le\lVert x\rVert^{2}$. Since $0\le|x_j|$ by claim 1 of Properties of the Absolute Value in an Ordered Field and $0\le\lVert x\rVert$ by claim 1, the weak form (claim 2) of Monotonicity of Squaring on the Nonnegative Elements of an Ordered Field yields $|x_j|\le\lVert x\rVert$.

Step 6 (Claim 5). By the definition of the scalar multiple the $i$-th coordinate of $\lambda x$ is $\lambda x_i$, and by commutativity and associativity of multiplication

Hence, by claim 3 of Properties of Finite Sums and claim 1,

Put $r=|\lambda|\,\lVert x\rVert$. Applying claim 5 of Elementary Arithmetic in an Ordered Field to the inequality $0\le\lVert x\rVert$ with the nonnegative multiplier $|\lambda|$ gives $|\lambda|\cdot0\le|\lambda|\,\lVert x\rVert$, and $|\lambda|\cdot0=0$ by claim 1 of Zero Products and Elementary Identities in a Field, so $0\le r$. Moreover, using commutativity and associativity of multiplication and then Step 0,

Claim 1, applied to the point $\lambda x$, characterises $\lVert\lambda x\rVert$ as the unique nonnegative real number whose square is $\sum_{i=1}^{n}(\lambda x_i)^{2}$. Hence $\lVert\lambda x\rVert=r=|\lambda|\,\lVert x\rVert$.

Step 7 (Claim 6). By Euclidean Distance is a Metric on $\mathbb{R}^n$ the function $d_E$ is a metric on $\mathbb{R}^n$, so it is symmetric and satisfies the triangle inequality

for all points $a,b,c$ of $\mathbb{R}^n$. Taking $a=x+y$, $b=y$ and $c=0_{\mathbb{R}^n}$, and using the second assertion of claim 2 twice, we get

By Euclidean Space $\mathbb{R}^n$ is a Real Vector Space the space $\mathbb{R}^n$ with these operations is a vector space, so its addition is commutative by condition 2 of that definition; hence $x+y=y+x$ and, by symmetry of $d_E$,

the last equality by the third assertion of claim 2, applied with $y$ as the base point and $x$ as the increment. Combining the two displays gives $\lVert x+y\rVert\le\lVert x\rVert+\lVert y\rVert$. $\blacksquare$