Uniqueness of roots

Stream: new members

[Sammy Webb]

Hello, I am wondering if anyone can tell me if I have misstated a theorem I am trying to prove.

The theorem is as follows:

Let $x>0$ and $k\in\mathbb{N}$. Then there is a unique $y>0$ such that $y^{k}=x$.

Proof

Let $S=\{s \geq 0 \; | \; s^{k}<x\}$. Then $S$ is nonempty (since $0 \in S$) and bounded above since $\max \{x, 1\}$ is an upper bound for $S$. Therefore

$$y=\text{LUB}(S)=\text{LUB}(\{s \geq0 \; | \; s^{k}<x\})$$

exists by the Completeness Axiom. We claim that $y^{k}=x$.

Since $y$ is the least upper bound of $S$, this means that for all $n\in\mathbb{N}$, $y-\frac{1}{n}$ is not an upper bound, i.e.\ there is $y_{n}\in S$ such that

$$y-\frac{1}{n}<y_{n}\leq y.$$

Now $y - \frac{1}{n} \to y$ (by Example) and the rules for
limits), and the constant sequence $y, y, \ldots$ converges to $y$ too, so
by the squeeze theorem, $y_n \to y$.

By Proposition power-lim, $y_n^k \to y^k$. But
$y_n\in S$, so $y_{n}^{k}<x$ for all $n$, so
Proposition~\ref{p:x_n<y_n} gives

$$y^{k} \leq x.$$

Now we will show the reverse inequality, i.e.\ that $x\leq y^{k}$, and this will imply $y^k=x$. Since $y=\text{LUB}(S)$, $y$ is an upper bound for $S$, and so for all $n$, $y+\frac{1}{n}\not\in S$. By the definition of $S$, this means

$$\left(y+\frac{1}{n}\right)^{k}\geq x.$$

Again, Propositions~\ref{p:power-lim} and~\ref{p:x_n<y_n}, together with the fact that $y + \frac{1}{n}\rightarrow y$, imply that

$$y^{k} \geq x.$$

Thus, $y^k=x$.

Finally, if $0 < w < z$ then $w^k < z^k$ (see Proposition 4.3) and so there is a {\em unique} $y >0$ such that $y^k = x$.

I have stated it as follows:

theorem theorem_6_6 {x:ℝ} (k:ℕ) (hx: 0 < x) (hk:1 ≤ k): ∃! y, 0 < y → y^k = x := by

Should this implication be an and statement?

However, while I am able to prove the existence I am struggling with the uniqueness.

[Kevin Buzzard]

Uniqueness isn't true the way you've written it, because any y which isn't >0 will also work. Yes it should be an "and" statement in the conclusion

[Sammy Webb]

Thank you I will try that.

[Kevin Buzzard]

I made the same error of logic in my initial definition of a scheme, and Commelin pointed it out to me.