Rigorous proof of a unique solution using Banach's Fixed Point Theorem

Question

I would like to have feedback on the overall quality of the following proof.

Question: Prove that $x^5+7x-1=0$ has a unique solution in $[0,1]$.

Proof: Let $f(x)=\frac{1-x^5}{7}$ and note that any solution of $f(x)=x$ is in fact a solution of our polynomial equation. Since $[0,1]$ is closed in $\mathbb{R}$, which is complete, it follows that $[0,1]$ is also complete. Since our polynomial equation is algebraic we use the Euclidean metric, denoted by $d$. Together, $([0,1],d)$ is a complete metric space.

To satisfy Banach's fixed point theorem we require that $f$ is a contraction on $[0,1]$:

$d(f(x),f(y))=|f(x)-f(y)|=\frac{1}{7}|x^5-y^5|=\frac{1}{7}|x-y|\cdot|x^4+x^3y+x^2y^2+xy^3+y^4|\leq \frac{5}{7}|x-y|=\frac{5}{7}d(x,y)$

for all $x,y\in[0,1]$. Thus $f$ is a contraction on $[0,1]$. Therefore, by Banach's fixed point theorem, $f$ must have a unique fixed point in $[0,1]$ and so the polynomial equation must have a unique solution in $[0,1]$.

All suggestions for improvements are welcome!

Answer 1

A hostile reviewer could raise the following issues:

1. You do not explicitly define the function $p : [0,1] \rightarrow \mathbb{R}$ given by $p(x) = x^5 + 7x - 1$.
2. You do not explicitly list the domain and co-domain of the function $f$ given by $f(x) = \frac{1-x^5}{7}$.
3. You do not explicitly state that $p(x) = 0$ if and only if $f(x) = x$.
4. You do not explicitly state that $f$ maps $[0,1]$ into itself.
5. You would have chosen the Euclidian metric even when $f$ is not an algebraic function.
6. The metric should be identified when you first mention completeness.
7. Stictly speaking, $f$ does not satisfy Banach's fixed point theorem. The function $f$ satisfies the hypothesis of Banach's fixed point theorem.

The only really serious issue is point $4$. The function $g : [0,1] \rightarrow \mathbb{R}$ given by $g(x) =2$ is a contraction, but it has no fixed points. Nevertheless, it would serve you well to eliminate the remaining issues.

It is not necessary to apply this level of formalism in your daily work, but apply it when you need to remove any doubt about your ability to justify your reasoning.