# Uniqueness of Positive Root of Positive Real Number

## Theorem

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

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

Then there is at most one $y \in \R: y \ge 0$ such that $y^n = x$.

## Proof

Let the real function $f : \left[{0 \,.\,.\, \to}\right) \to \left[{0 \,.\,.\, \to}\right)$ be defined as:

- $f \left({y}\right) = y^n$

First let $n > 0$.

By Identity Mapping is Order Isomorphism, the identity function $I_\R$ on $\left[{0 \,.\,.\, \to}\right)$ is strictly increasing.

We have that:

- $f \left({y}\right) = \left({I_\R \left({y}\right) }\right)^n$

By Product of Positive Strictly Increasing Mappings is Strictly Increasing, $f$ is strictly increasing on $\left[{0 \,.\,.\, \to}\right)$.

From Strictly Monotone Mapping with Totally Ordered Domain is Injective:

- there is at most one $y \in \R: y \ge 0$ such that $y^n = x$.

$\Box$

Now let $n < 0$.

Let $m = -n$.

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

- $g \left({y}\right) = y^m$

From the definition of power:

- $g \left({y}\right) = \dfrac 1 {f \left({y}\right)}$

Hence $g \left({y}\right)$ is strictly decreasing.

From Strictly Monotone Mapping with Totally Ordered Domain is Injective:

- there is at most one $y \in \R: y \ge 0$ such that $y^n = x$.

$\blacksquare$