IVT (Classical) Let $f:\left[a,b\right]\to\mathbb{R}$ be continuous. If $f\left(a\right)<0$ and $f\left(b\right)>0$, then there exists $c\in\left(a,b\right)$ such that $f\left(c\right)=0$.
In intuitionistic logic, there's no proof of the classical form of the Intermediate Value Theorem. However, there is an approximate form which can be proved in intuitionistic logic.
IVT (Approximate) Let $f:\left[a,b\right]\to\mathbb{R}$ be continuous. If $f\left(a\right)<0$ and $f\left(b\right)>0$, then, for any $\varepsilon>0$, there exists $c\in\left(a,b\right)$ such that $|f\left(c\right)|<\varepsilon$.
While IVT (Classical) and IVT (Approximate) are not equivalent in intuitionistic logic, they are in classical logic. Below is my attempt at a proof of this equivalence.
Proposition. IVT (Classical) is equivalent to IVT (Approximate) in classical logic.
Proof.
Let $f:\left[a,b\right]\to\mathbb{R}$ be continuous such that $f\left(a\right)<0$ and $f\left(b\right)>0$.
For any $\varepsilon>0$, the classical form immediately determines a $c\in\left(a,b\right)$ such that $|f\left(c\right)|=0<\varepsilon$.
On the other hand, suppose that, for all $\varepsilon>0$, we have that there exists $x\in\left(a,b\right)$ such that $|f\left(x\right)|<\varepsilon$. Then, we may define a sequence $\left(c_{N}\right)_{N\geq1}$ such that $|f\left(c_{N}\right)|<1/N$. Then, $|f\left(c_{N}\right)|\to0$ as $N\to0$.
Since $\left(c_{N}\right)_{N\geq1}$ is bounded below and above by $a$ and $b$, respectively, there is a convergent subsequence (Bolzano-Weierstrass). Since we may evaluate $f$ along a convergent subsequence, we may, without loss in generality, assume $c_{N}\to c\in\left(a,b\right)$.
Therefore, $|f\left(c_{N}\right)|\to|f\left(c\right)|$, and so we have a $c\in\left(a,b\right)$ such that $f\left(c\right)=0$, as required.
QED
Is my proof correct?