Proof of The Cauchy-Schwarz Inequality on $\mathbb{R}^n$

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

Write $a=x\cdot x$, $b=x\cdot y$ and $c=y\cdot y$, real numbers by The Dot Product on $\mathbb{R}^n$ §dot-product and Iterated Operations and Operations over Finite Sets Take Values in the Underlying Set §segment-sums. By The Dot Product on $\mathbb{R}^n$ Is Symmetric, Bilinear and Positive Definite §nonnegative, $a\ge0$ and $c\ge0$. By The Euclidean Norm on $\mathbb{R}^n$ §norm and The k-th Root and the Square Root of a Nonnegative Real Number §square-root, $\lVert x\rVert=\sqrt{a}$ and $\lVert y\rVert=\sqrt{c}$ are the unique nonnegative real numbers whose squares are $a$ and $c$, uniqueness being given by Existence and Uniqueness of Nonnegative k-th Roots of Nonnegative Real Numbers §root. We use that $u^{2}=u^{1+1}=u^{1}u^{1}=u\,u$ for $u\in\mathbb{R}$, by $2=1+1$ (Arithmetic and Order of the Natural Numbers §digits), Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §exponents and Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §product. Since $b$ is real, $|b|$ is its absolute value, by Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces §complex-plane.

Step 1: $b\,b\le a\,c$. Suppose first $c=0$. Then $y=0$, the origin, by The Dot Product on $\mathbb{R}^n$ Is Symmetric, Bilinear and Positive Definite §definite, and $0y=0$ by Rules for Pointwise Operations on Real-Valued Maps: a Commutative Ring, Scalar Multiples and Evaluation §constant-multiple with $I=[n]$, the origin being the constant map $0$ of Pointwise Operations on Real-Valued Maps §constants by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §origin; so $y=0y$ and, by The Dot Product on $\mathbb{R}^n$ Is Symmetric, Bilinear and Positive Definite §second and Rules of Arithmetic and Order in an Ordered Field §zero,

$$b=x\cdot(0y)=0\,(x\cdot y)=0 .$$

Hence $b\,b=0=a\cdot0=a\,c$ by Rules of Arithmetic and Order in an Ordered Field §zero and commutativity, and $b\,b\le a\,c$.

Suppose now $c\neq0$; then $c>0$, as $c\ge0$, and $c^{-1}$ exists by Negatives, Differences, Reciprocals and Quotients §reciprocal. Let $t=b\,c^{-1}$, which lies in $\mathbb{R}$ by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima §quotient, so that $t\,c=b\,(c^{-1}c)=b\cdot1=b$. The vector $v=x-ty$ lies in $\mathbb{R}^{n}$ by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §operations. By The Dot Product on $\mathbb{R}^n$ Is Symmetric, Bilinear and Positive Definite §second and The Dot Product on $\mathbb{R}^n$ Is Symmetric, Bilinear and Positive Definite §symmetric,

$$x\cdot v=x\cdot x-x\cdot(ty)=a-t\,(x\cdot y)=a-t\,b,\qquad y\cdot v=y\cdot x-y\cdot(ty)=b-t\,(y\cdot y)=b-t\,c=b-b=0,$$

and then, by The Dot Product on $\mathbb{R}^n$ Is Symmetric, Bilinear and Positive Definite §first,

$$v\cdot v=(x-ty)\cdot v=x\cdot v-(ty)\cdot v=(a-t\,b)-t\,(y\cdot v)=(a-t\,b)-t\cdot0=a-t\,b,$$

using Rules of Arithmetic and Order in an Ordered Field §zero and $-0=0$ ($-0=0$ since $0+0=0$, by Negatives, Differences, Reciprocals and Quotients §negative). By The Dot Product on $\mathbb{R}^n$ Is Symmetric, Bilinear and Positive Definite §nonnegative, $0\le v\cdot v=a-t\,b$, so $t\,b\le a$ by Rules of Arithmetic and Order in an Ordered Field §order-sum. As $c>0$, Rules of Arithmetic and Order in an Ordered Field §order-product gives $(t\,b)\,c\le a\,c$, and $(t\,b)\,c=b\,(t\,c)=b\,b$ by associativity and commutativity. So $b\,b\le a\,c$.

Step 2: square roots. By Step 1 and the identity $u^{2}=u\,u$, $b^{2}\le a\,c$; moreover $b^{2}=b\,b\ge0$ by Rules of Arithmetic and Order in an Ordered Field §squares, so $a\,c\ge0$ as well. Hence, by Properties of k-th Roots: Inverse to Powers, Absolute Values, Products, Monotonicity, Subadditivity, Differences and Limits §abs, Properties of k-th Roots: Inverse to Powers, Absolute Values, Products, Monotonicity, Subadditivity, Differences and Limits §monotone (with $k=2$, both $b^{2}$ and $a\,c$ being nonnegative) and Properties of k-th Roots: Inverse to Powers, Absolute Values, Products, Monotonicity, Subadditivity, Differences and Limits §product (with $k=2$, $a,c\ge0$),

$$|x\cdot y|=|b|=\sqrt{b^{2}}\le\sqrt{a\,c}=\sqrt{a}\,\sqrt{c}=\lVert x\rVert\,\lVert y\rVert .$$