Existence of Positive Root of Positive Real Number/Negative Exponent

This article needs to be linked to other articles. In particular: to results used, in particular so as to clarify the scope of the domain in $\dfrac 1 x > 0$. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding these links. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{MissingLinks}} from the code.

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 $\hointr 0 \to$ defined by:

$\map g 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:

$\map g y = \dfrac 1 x$

It follows from the definition of power that:

\(\ds \map f y\)

\(=\)

\(\ds \dfrac 1 {\map g y}\)

\(\ds \)

\(=\)

\(\ds \dfrac 1 {1 / x}\)

\(\ds \)

\(=\)

\(\ds x\)

$\blacksquare$