The intermediate value theorem gives a second proof that every nonnegative real has an $n$-th root, applied to $x^n$ on a closed bounded interval

Let $a\in \mathbb{R}$ with $a\ge 0$ and let $n\in \mathbb{N}$ with $n\ge 1$. Put $M:=a+1$ and consider

$f:[0,M]\to \mathbb{R},f(x):=x^n$

(Integer powers $a^m$, Intervals of $\mathbb{R}$: the nine order-convex forms, nondegeneracy, and length). Then $f$ is continuous on $[0,M]$, $f(0)=0\le a\le M^n=f(M)$, and the intermediate value theorem (Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a,b]$ takes every value between $f(a)$ and $f(b)$) supplies $c\in [0,M]$ with

$c^n=a\mathrm{.}$

Moreover $c$ is the only nonnegative real with this property, so $c=a^{1\mathrm{/}n}$ in the notation of Existence and uniqueness of $n$-th roots: a unique $a^{1\mathrm{/}n}\ge 0$ with $(a^{1\mathrm{/}n}{)}^n=a$.

This is a second proof of an existing theorem, not a new one. Existence and uniqueness of $n$-th roots: a unique $a^{1\mathrm{/}n}\ge 0$ with $(a^{1\mathrm{/}n}{)}^n=a$ already proves existence and uniqueness of $n$-th roots, by an argument that runs directly from the least-upper-bound property and the factorisation of $b^n-a^n$; it is the item the rest of the library cites, and no second identifier is minted for the same statement. What is recorded here is that the intermediate value theorem gives the existence half in three lines once continuity of $x\mapsto x^n$ is available, which is the standard modern route and the reason the theorem is usually met in this form.

No circularity. Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a,b]$ takes every value between $f(a)$ and $f(b)$ rests on A nested sequence of nonempty closed bounded intervals has nonempty intersection, and the intersection is a single point exactly when the lengths tend to $0$, on the algebra of continuous functions and on the sequential criterion, none of which uses $n$-th roots; and the uniqueness half below is Monotonicity of $x\mapsto x^n$ and of $n\mapsto a^n$, which is pure ordered-field arithmetic. So this argument could have been the library's definition of $a^{1\mathrm{/}n}$; it is not, only because the roots were needed at order $16$, long before continuity existed.

• Why $M=a+1$ and not $M=a$. For $0\le a<1$ the value $a^n$ is at most $a$, so $[0,a]$ need not reach $a$ at its right endpoint; adding $1$ makes $M\ge 1$, and then $M^n\ge M>a$ by Monotonicity of $x\mapsto x^n$ and of $n\mapsto a^n$. Taking $M:=\max \{1,a\}$ works equally well and is the usual textbook choice; $a+1$ avoids naming a maximum.

• The same argument through the image. The image of an interval under a continuous real function is order-convex, hence an interval, and the image of a closed bounded interval is a closed bounded interval says $f[[0,M]]$ is a closed bounded interval containing $f(0)=0$ and $f(M)=M^n$, hence containing $a$; that is the intermediate value theorem repackaged, and it is the form in which the statement generalises to other continuous increasing functions.

• What this does not give. The argument produces a root but no way to compute it, and no rate: it is a pure existence proof, exactly like the bisection that underlies Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a,b]$ takes every value between $f(a)$ and $f(b)$. The companion example A worked fixed point on $[1,2]$ for the map $x\mapsto (x+2\mathrm{/}x)\mathrm{/}2$, from the one-dimensional fixed point theorem identifies the same number, for $n=2$ and $a=2$, as the fixed point of $x\mapsto (x+2\mathrm{/}x)\mathrm{/}2$ on $[1,2]$.