# Existence of Positive Root of Positive Real Number/Negative Exponent

## Theorem

Let $x \in \R$ be a real number such that $x > 0$.

Let $n \in \Z$ be an integer such that $n < 0$.

Then there exists a $y \in \R: y \ge 0$ such that $y^n = x$.

## Proof

Let $m = -n$.

Then $m > 0$.

Let $g$ be the real function defined on $\left[{0 \,.\,.\, \to}\right)$ defined by:

- $g \paren y = y^m$

Since $x \ge 0$:

- $\dfrac 1 x \ge 0$

By Existence of Positive Root of Positive Real Number: Positive Exponent there is a $y > 0$ such that:

- $g \paren y = \dfrac 1 x$

It follows from the definition of power that:

\(\displaystyle f \paren y\) | \(=\) | \(\displaystyle \dfrac 1 {g \paren y}\) | |||||||||||

\(\displaystyle \) | \(=\) | \(\displaystyle \dfrac 1 {1 / x}\) | |||||||||||

\(\displaystyle \) | \(=\) | \(\displaystyle x\) |

$\blacksquare$