# Positive Real has Real Square Root

## Theorem

Let $x \in \R_{>0}$ be a (strictly) positive real number.

Then:

$\exists y \in \R: x = y^2$

## Proof

Let $f: \R \to \R$ be defined as:

$\forall x \in \R: f \left({x}\right) = x^2$

We have that $f$ is the pointwise product of the identity mapping with itself.

$\exists q \in \R: f \left({q}\right) > x$

Then:

$0^2 = 0 \le x$

By the Intermediate Value Theorem:

$\exists y \in \R: 0 < y < q: y^2 = x$

$\blacksquare$