# Uniqueness of Positive Root of Positive Real Number/Positive 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 is at most one $y \in \R: y \ge 0$ such that $y^n = x$.

## Proof 1

Let the real function $f: \hointr 0 \to \to \hointr 0 \to$ be defined as:

$\map f y = y^n$

First let $n > 0$.

By Identity Mapping is Order Isomorphism, the identity function $I_\R$ on $\hointr 0 \to$ is strictly increasing.

We have that:

$\map f y = \paren {\map {I_\R} y}^n$

By Product of Positive Strictly Increasing Mappings is Strictly Increasing, $f$ is strictly increasing on $\hointr 0 \to$.

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

$\blacksquare$

## Proof 2

We have that:

$0 < y_1 < y_2 \implies y_1^n < y_2^n$

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

$\blacksquare$