# Constructive intermediate value theorem

I have given real numbers $x_1,x_2,y_1,y_2$ such that $x_1 > x_2$ and $y_1 < y_2$. The the claim is that there exists some $\lambda \in (0,1)$ such that $\lambda (x_1 - x_2) + (1-\lambda)(y_1-y_2) = 0$. In order to proof this, one needs ( at least in my opinion) the intermediate value theorem. But the intermediate value theorem does not hold in constructive mathematics (that is without the law of excluded middle; or constructive mathematics acts in intuitionistic logic). For a proof of this c.f. this paper. Is there any constructive way to show the above equation?

• Anyway, the intermediate value theorem can be proved in a "constructive" way. (I put the "..." because I don't know a word about constructive mathematics). By bisecting iteratively, you construct a sequence that turns out to be Cauchy, and so it has a limit. – Giuseppe Negro Sep 18 at 10:19
• @GiuseppeNegro the "construction" is not "constructive" enough for this purpose; it uses "either the left or the right works, so pick one, and ..." but constructions of this kind (especially with an infinite number of such choices) are forbidden in that context – Richard Rast Sep 18 at 13:43
• @RichardRast: OK. On the other hand, if the function is differentiable, the Newton's method is available. That definitely is constructive. Am I right? This would provide a way of solving more general problems of the kind of this question – Giuseppe Negro Sep 18 at 13:56
• @GiuseppeNegro I'm not an expert on constructive mathematics, but according to Dr. Google, Cauchy's theorem has a constructive proof. If Newton's method is constructively proved to converge to a solution, that should be valid. But I think the conditions on it converging might be nontrivial and require additional "constructive metadata" (like an explicit neighborhood around the point in which blah blah blah) ... – Richard Rast Sep 18 at 14:05
• (cont.) but the accepted answer below is the intent of the discipline, to move away from general theorems that prove existence and toward constructions which (theoretically) give more information. Below we have the exact form of the answer, which in practice is often more useful than just knowing the answer exists. – Richard Rast Sep 18 at 14:08

Just solve the equation for $\lambda$. You get $\lambda =\frac {y_2-y_1}{x_1-x_2+y_2-y_1}$.
You can explicitly solve the equation; $$\lambda= \frac{y_2-y_1}{x_1-x_2-y_1+y_2}.$$