Existence of square roots of nonnegative reals

Statement

Let $x$ be a real number with $x \ge 0$ . Then there is exactly one real number $y$ with $y \ge 0$ and $y^2 = x$ .

Remarks

Existence uses the completeness axiom: take $y = \sup \{t \ge 0 : t^2 \le x\}$ and show that $y^2 < x$ and $y^2 > x$ are both impossible. Uniqueness: if $y, z \ge 0$ and $y^2 = z^2$ , then $(y - z)(y + z) = 0$ , thus $y = z$ . In $\mathbb{Q}$ the existence fails: $2$ has no rational square root, by the irrationality of the square root of 2.

Reading path

To understand this page from the ground up, read these 5 pages in order. The foundations come first.

Show the path as a graph

Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.

no evidence level

Real numbers object
Set bounded above definition
Supremum definition
Completeness axiom statement
Existence of square roots of nonnegative reals statement

Where this leads

261 pages build on this one.

Tag	`068BZBXE0C`
URI	`m2://068BZBXE0C`
Kind	statement, theorem
Writing	W0 stub
MSC	26A09
Status	This copy of the site has no build data. Run `m2 status 068BZBXE0C`.
Uses	Completeness axiom

Existence of square roots of nonnegative reals

Statement

Remarks

Reading path

Where this leads

Further reading

What this page needs for W1

What links here

Used by