Proof of Cauchy-Schwarz Inequality for the Euclidean Dot Product

Throughout, $\le$ and $<$ are the order of the ordered field of real numbers, and for a real number $t$ we write $t^2$ for $t\,t$.

Step 1 (The identity matrix and its quadratic form). Let $I$ be the $n\times n$ identity matrix, the real matrix with entries $I_{ij}=1$ if $i=j$ and $I_{ij}=0$ otherwise ($i,j\in\{1,\dots,n\}$). For every $z=(z_1,\dots,z_n)\in\mathbb{R}^n$ and every $i$, the $i$-th component of the matrix-vector product $Iz$ is the finite sum $\sum_{j=1}^{n}I_{ij}z_j$; every summand with $j\ne i$ equals $0\cdot z_j=0$ and the summand with $j=i$ equals $1\cdot z_i=z_i$, so the sum evaluates to $z_i$. Hence $Iz=z$ for every $z\in\mathbb{R}^n$. The matrix $I$ is symmetric, since $I_{ij}=I_{ji}$ for all $i,j$ directly from the entry formula. Moreover, for every $z\in\mathbb{R}^n$,

the two identities hold by $Iz=z$ and by claim 1 of the elementary properties of the Euclidean norm, with the dot product; and the inequality follows since $0\le\lVert z\rVert$ (the same claim) and a nonnegative real has nonnegative square: for $r=0$ one has $r\,r=0$, while $0<r$ gives $0<r\,r$ by claim 5 of the elementary order arithmetic lemma. So $I$ is symmetric positive semidefinite.

Step 2 (Squared inequality). By claim 2 of the Cauchy-Schwarz inequality for a positive semidefinite quadratic form, applied with $B=I$,

which by Step 1 reads $(x\cdot y)^{2}\le\lVert x\rVert^{2}\,\lVert y\rVert^{2}$. Multiplication of real numbers is commutative and associative (axioms of the underlying field), so, regrouping the fourfold product, $\lVert x\rVert^{2}\lVert y\rVert^{2}=(\lVert x\rVert\lVert x\rVert)(\lVert y\rVert\lVert y\rVert)=(\lVert x\rVert\lVert y\rVert)(\lVert x\rVert\lVert y\rVert)=(\lVert x\rVert\,\lVert y\rVert)^{2}$. Set $b=\lVert x\rVert\,\lVert y\rVert$. Then

indeed $0\le\lVert x\rVert$ and $0\le\lVert y\rVert$ by claim 1 of the norm properties lemma; if both are strictly positive then $0<b$ by claim 5 of the elementary order arithmetic lemma, and otherwise one factor is $0$, so $b=0$.

Step 3 (From squares to absolute values). We first show: for all real $a,b$ with $0\le b$ and $a^{2}\le b^{2}$, it holds that $a\le b$. If $a\le 0$ then $a\le 0\le b$, and transitivity of the total order gives $a\le b$. Suppose instead $0<a$, and assume for contradiction that $b<a$. By claim 10 of the order arithmetic lemma (strict compatibility with multiplication, with the positive factor $a$), $b<a$ gives $ab<a\,a=a^{2}$. If $0<b$, the same claim with the positive factor $b$ gives $b\,b<b\,a$, and $b\,a=ab$ by commutativity, so $b^{2}<ab<a^{2}$ and hence $b^{2}<a^{2}$ by claim 2 of the same lemma (mixed transitivity). If $b=0$, then $b^{2}=0<a^{2}$ by claim 5 of the same lemma. In either case $b^{2}<a^{2}$; combined with $a^{2}\le b^{2}$, claim 2 of the same lemma yields $b^{2}<b^{2}$, which is false since $<$ requires the two sides to be distinct. Hence $a\le b$.

Applying this with $a=x\cdot y$ and the $b$ of Step 2 gives $x\cdot y\le b$. Applying it with $a=-(x\cdot y)$ --- noting $(-(x\cdot y))^{2}=(x\cdot y)^{2}$: in any field, distributivity and the uniqueness of additive inverses give $(-s)t=-(st)$ and $-(-w)=w$, whence $(-s)(-s)=-\big(s(-s)\big)=-\big(-(s\,s)\big)=s\,s$ --- gives $-(x\cdot y)\le b$, which by claim 4 of the order arithmetic lemma (sign reversal) and $-(-(x\cdot y))=x\cdot y$ is equivalent to $-b\le x\cdot y$. Thus $-b\le x\cdot y\le b$, and by the two-sided characterization of the absolute value, claim 6 of the properties of the absolute value,