Uniqueness of Positive Root of Positive Real Number

This article is complete as far as it goes, but it could do with expansion. In particular: this result holds in any ordered field, or at least any totally ordered field. Possibly even in ordered division rings? You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding this information. 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 {{Expand}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.

Theorem

Positive Exponent

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$.

Negative Exponent

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$.