Proof of The Cauchy-Schwarz Inequality in a Real Inner Product Space

Let $x,y\in E$. We use the notation and claims of Elementary Identities in a Real Inner Product Space.

If $y=0_{E}$, then $\langle x,y\rangle=0$ and $|y|=0$ by Elementary Identities in a Real Inner Product Space (ii), so both sides of the asserted inequality equal $0$ (using $|0|=0$, claim 1 of Properties of the Absolute Value in an Ordered Field), and there is nothing to prove.

Suppose $y\ne 0_{E}$. Then $0<|y|$ by Elementary Identities in a Real Inner Product Space (iii), hence $0<|y|^{2}$ by claim 5 of Elementary Order Arithmetic in an Ordered Field, and $|y|^{2}$ has a multiplicative inverse. Put $t=\langle x,y\rangle\,(|y|^{2})^{-1}\in\mathbb{R}$. By Elementary Identities in a Real Inner Product Space (v), Elementary Identities in a Real Inner Product Space (i) and Elementary Identities in a Real Inner Product Space (iv),

$$0\le|x-ty|^{2}=|x|^{2}-2\langle x,ty\rangle+|ty|^{2}=|x|^{2}-2t\langle x,y\rangle+t^{2}|y|^{2},$$

the first inequality being condition (d) of Real Inner Product Spaces (i), since $|x-ty|^{2}=\langle x-ty,x-ty\rangle$. With the chosen $t$ we have $t\langle x,y\rangle=\langle x,y\rangle^{2}(|y|^{2})^{-1}$ and $t^{2}|y|^{2}=\langle x,y\rangle^{2}(|y|^{2})^{-1}$, so the display reads

$$0\le|x|^{2}-\langle x,y\rangle^{2}\,(|y|^{2})^{-1}.$$

Multiplying by the positive number $|y|^{2}$ (claim 5 of Elementary Arithmetic in an Ordered Field) and rearranging by the translation rule (claim 3 of Elementary Arithmetic in an Ordered Field) gives $\langle x,y\rangle^{2}\le|x|^{2}|y|^{2}=(|x|\,|y|)^{2}$. Now $|\langle x,y\rangle|^{2}=\langle x,y\rangle^{2}$ because $|\langle x,y\rangle|$ equals $\langle x,y\rangle$ or $-\langle x,y\rangle$ (claim 1 of Properties of the Absolute Value in an Ordered Field), and both $|\langle x,y\rangle|$ and $|x|\,|y|$ are nonnegative (the same claim; and $0=|x|\cdot 0\le|x|\,|y|$ by claim 5 of Elementary Arithmetic in an Ordered Field). Therefore $|\langle x,y\rangle|\le|x|\,|y|$ by claim 2 of Monotonicity of Squaring on the Nonnegative Elements of an Ordered Field.