Proof of Existence and Uniqueness of the Square Root of a Sum of Two Squares

Let $a$ and $b$ be real numbers. By that definition the real numbers form an ordered field, so we may use the field axioms, the two order-compatibility conditions, and the fact that $\le$ is a total order. For a real number $x$ we write $x^{2}=x\cdot x$.

Step 1 (two field identities). For every real $x$ we have $x\cdot0=x\cdot(0+0)=x\cdot0+x\cdot0$ by the distributive law, and adding the additive inverse of $x\cdot0$ to both sides gives $x\cdot0=0$. Consequently, for all real $u,v$,

so $u\cdot(-v)=-(u\cdot v)$. Applying this twice, $(-x)\cdot(-x)=-\bigl((-x)\cdot x\bigr)=-\bigl(x\cdot(-x)\bigr)=-\bigl(-(x\cdot x)\bigr)=x\cdot x$.

Step 2 (squares are nonnegative). Let $x$ be real. Since $\le$ is a total order, $0\le x$ or $x\le0$. If $0\le x$, then $0\le x\cdot x$ by the second order-compatibility condition of Ordered Field. If $x\le0$, then adding $-x$ to both sides, which is permitted by the first order-compatibility condition, gives $0\le-x$, hence $0\le(-x)\cdot(-x)$, and this equals $x\cdot x$ by Step 1. In both cases $0\le x^{2}$.

Step 3 (the sum is nonnegative). By Step 2, $0\le a^{2}$ and $0\le b^{2}$. Adding $b^{2}$ to both sides of $0\le a^{2}$ gives $b^{2}\le a^{2}+b^{2}$. Since $0\le b^{2}$ and a total order is transitive, $0\le a^{2}+b^{2}$.

Step 4 (conclusion). Thus $a^{2}+b^{2}$ is a nonnegative real number, so by Existence and Uniqueness of the Nonnegative Square Root there is exactly one real number $r$ with $0\le r$ and $r^{2}=a^{2}+b^{2}$.