Nested-bracket proof of the intermediate value theorem (source code)

= Nested-bracket proof of the intermediate value theorem

For a short proof outline, endpoint values give the non-strict cases immediately. If $y$ is strictly between $f(a)$ and $f(b)$, apply the <bisection method> to the <continuous function> $g(x)=f(x)-y$. A <midpoint> with $g=0$ finishes the proof. Otherwise retain <nested intervals> $[a_k,b_k]$ with strictly opposite signs and widths $(b-a)2^{-k}$. The <nested interval theorem>, using <completeness of the real numbers>, gives a common point $c$ to which both endpoint <sequences> converge. After reversing the sign of $g$ if necessary, $g(a_k)<0<g(b_k)$. <Continuity> makes both endpoint value <sequences> converge to $g(c)$, forcing $g(c)\leq0$ and $g(c)\geq0$, hence $f(c)=y$. The original endpoint values differ from $y$, so $c\in(a,b)$. This proof explains why a jump can defeat the construction: shrinking a candidate <closed interval> cannot supply the missing <continuity>.