---
tag: E9F3A0A60C
kind: proof
name: Proof of the existence of square roots of nonnegative reals
msc: [26A09]
proves: 068BZBXE0C
uses: [0AXWET80YW, 0BTMQ04556, 0B5H2V4JW8, 0QSPNASE50]
methods: [0J0XBKG64S]
sources:
  - url: https://proofwiki.org/wiki/Existence_of_Square_Roots_of_Positive_Real_Number
---

## Proof

We take the supremum of the numbers whose square is at most $x$, and rule out the two strict inequalities by contradiction.

1. Let $x$ be a real number with $x \ge 0$. All computations take place in the [[ordered field|0QSPNASE50]] $\R$.
2. Lemma. If $0 \le a < b$, then $a^2 < b^2$. Indeed, $b^2 - a^2 = (b - a)(b + a)$, with $b - a > 0$ and $b + a \ge b > 0$. A product of two positive numbers is positive.
3. Uniqueness. Let $y, z \ge 0$ with $y^2 = z^2 = x$. If $y < z$, the lemma gives $y^2 < z^2$, which is false. In the same way $z < y$ is false. So $y = z$.
4. Existence. Let $S = \set{t \in \R : t \ge 0 \text{ and } t^2 \le x}$. Then $0 \in S$, so $S$ is nonempty.
5. The set $S$ is [[bounded above|0B5H2V4JW8]] by $x + 1$. If $t > x + 1 \ge 0$, the lemma gives $t^2 > (x + 1)^2 = x^2 + 2x + 1 > x$, so $t \notin S$.
6. By the [[completeness axiom|0AXWET80YW]], $S$ has a [[supremum|0BTMQ04556]] $y$. Since $0 \in S$, $y \ge 0$.
7. Suppose $y^2 < x$. Let $\delta = x - y^2 > 0$ and $h = \min(1, \delta/(2y + 1))$. Then $0 < h \le 1$, so $h^2 \le h$.
8. Then $(y + h)^2 = y^2 + 2 y h + h^2 \le y^2 + h (2y + 1) \le y^2 + \delta = x$.
9. So $y + h \in S$, and $y + h > y$. This contradicts that $y$ is an upper bound of $S$.
10. Suppose $y^2 > x$. Then $y \ne 0$, since $0^2 = 0 \le x$. So $y > 0$.
11. Let $\delta = y^2 - x > 0$ and $h = \min(y/2, \delta/(2y))$. Then $h > 0$ and $y - h \ge y/2 > 0$.
12. Then $(y - h)^2 = y^2 - 2 y h + h^2 \ge y^2 - 2 y h \ge y^2 - \delta = x$.
13. Let $t \in S$. If $t > y - h$, then the lemma gives $(y - h)^2 < t^2 \le x$, against step 12. So $t \le y - h$.
14. Thus $y - h$ is an upper bound of $S$ smaller than $y$. This contradicts that $y$ is the least upper bound.
15. By steps 9 and 14, neither $y^2 < x$ nor $y^2 > x$. Since the order is total, $y^2 = x$, and $y \ge 0$.

## Idea

The supremum $y$ of the numbers with square at most $x$ is the candidate. If $y^2$ were too small, a slightly larger number would still be in the set. If $y^2$ were too large, a slightly smaller number would still be an upper bound.