TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced — the exact statement appears in a cited source; only wording and notation differ.
AI-adapted — a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated — a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a,b]$ takes every value between $f(a)$ and $f(b)$

Statement

Let $a, b \in \mathbb{R}$ with $a \le b$ , let $f : [a,b] \to \mathbb{R}$ be continuous on the closed bounded interval $[a,b]$ (Intervals of $\mathbb{R}$ : the nine order-convex forms, nondegeneracy, and length, Continuity of $f : A \to \mathbb{R}$ at a point of $A$ and on $A$ : the $\varepsilon$ - $\delta$ condition, its agreement with $\lim_{x \to c} f(x) = f(c)$ at a limit point, and continuity at an isolated point), and let $y \in \mathbb{R}$ satisfy

$f(a) \le y \le f(b) \qquad \text{or} \qquad f(b) \le y \le f(a) .$

Then there is $c \in [a,b]$ with $f(c) = y$ .

The construction is canonical, so no choice principle is used. The bisection below tests the left half first and takes the right half only when the left one has been ruled out, so the passage from one interval to the next is a function of that interval, and The recursion theorem applies with nothing selected. This is the same discipline the library uses wherever a sequence is built one term at a time.

Completeness of $\mathbb{R}$ is what does the work. The bisection produces a nested sequence of closed bounded intervals whose lengths tend to $0$ , and it is A nested sequence of nonempty closed bounded intervals has nonempty intersection, and the intersection is a single point exactly when the lengths tend to $0$ — hence the least-upper-bound property — that supplies the point. Over an ordered field that is not complete the theorem fails; the witness for that, stated for an arbitrary ordered field and worked over $\mathbb{Q}$ , is On a closed interval of $\mathbb{Q}$ there is a continuous unbounded function, a bounded one with no maximum, and one without the intermediate value property, which states its own $\varepsilon$ - $\delta$ continuity inline and is not an instance of this page's definition.

Facts & Assumptions

Given: Reals $a \le b$ , a function $f : [a,b] \to \mathbb{R}$ continuous on $[a,b]$ , and a real $y$ with $f(a) \le y \le f(b)$ or $f(b) \le y \le f(a)$ .

[L1]

Scalar multiples of continuous functions are continuous, so $(-1)f$ is continuous on $[a,b]$ (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function, Continuity of $f : A \to \mathbb{R}$ at a point of $A$ and on $A$ : the $\varepsilon$ - $\delta$ condition, its agreement with $\lim_{x \to c} f(x) = f(c)$ at a limit point, and continuity at an isolated point).

[L2]

Recursion: for a set $X$ , an element $x_0 \in X$ and a function $F : X \to X$ there is a unique $g : \mathbb{N} \to X$ with $g(0) = x_0$ and $g(k+1) = F(g(k))$ for every $k$ (The recursion theorem).

[L3]

Nested intervals: if $I_k = [a_k,b_k]$ with $a_k \le b_k$ and $I_{k+1} \subseteq I_k$ for every $k \in \mathbb{N}$ , then $\bigcap_{k} I_k$ is nonempty, and it is a single point exactly when the lengths $b_k - a_k$ tend to $0$ (A nested sequence of nonempty closed bounded intervals has nonempty intersection, and the intersection is a single point exactly when the lengths tend to $0$ , Intervals of $\mathbb{R}$ : the nine order-convex forms, nondegeneracy, and length, Limits and Cauchy sequences of reals).

[L4]

Null geometric sequences: $|r| < 1$ implies $r^{k} \to 0$ ; and a constant multiple of a null sequence is null, while a constant sequence converges to that constant (For $|r| < 1$ the sequence $r^k$ is null, and for $|r| > 1$ the sequence $|r|^k$ diverges to $+\infty$ , Algebra of limits: sums, scalar multiples, products and quotients, Integer powers $a^m$ , Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L5]

Powers: $(2^{-1})^{k} = (2^{k})^{-1}$ for every $k \in \mathbb{N}$ (Laws of integer exponents, Integer powers $a^m$ ).

[L6]

Sequential criterion, the choice-free direction: if $f$ is continuous at $c$ and $x_k \in [a,b]$ with $x_k \to c$ , then $f(x_k) \to f(c)$ ( $f$ is continuous at $c \in A$ if and only if $f(x_k) \to f(c)$ for every sequence in $A$ converging to $c$ , the converse direction costing countable choice, Continuity of $f : A \to \mathbb{R}$ at a point of $A$ and on $A$ : the $\varepsilon$ - $\delta$ condition, its agreement with $\lim_{x \to c} f(x) = f(c)$ at a limit point, and continuity at an isolated point).

[L7]

Limits preserve non-strict inequalities (Limits preserve non-strict inequalities).

[L8]

Order and field arithmetic in $\mathbb{R}$ : trichotomy and totality, so exactly one of $f(m) \ge y$ and $f(m) < y$ holds; halving and the ordered-field identities (Ordered field, Complete ordered field (least-upper-bound property)); and $|t| \le s$ whenever $-s \le t \le s$ (Basic properties of the absolute value).

Proof

technique · constructive

1.1

Reduction. It is enough to prove the theorem under the hypothesis $f(a) \le y \le f(b)$ . Indeed, in the remaining case $f(b) \le y \le f(a)$ , put $h := (-1)f$ and $z := -y$ ; then $h$ is continuous on $[a,b]$ by [L1] and $h(a) = -f(a) \le -y = z \le -f(b) = h(b)$ , so a point $c \in [a,b]$ with $h(c) = z$ is a point with $f(c) = y$ .

L1L8suffices: assume f(a) le y le f(b)

1.2

The bisection map. Assume $f(a) \le y \le f(b)$ and put $X \;:=\; \bigl\{\, (u,v) \in \mathbb{R} \times \mathbb{R} \ : \ a \le u \le v \le b,\ f(u) \le y \le f(v) \,\bigr\},$ so $(a,b) \in X$ . For $(u,v) \in X$ write $m := (u+v)/2$ , which satisfies $a \le u \le m \le v \le b$ and so lies in $[a,b]$ , and define $F(u,v) \;:=\; \begin{cases} (u,\ m) & \text{if } f(m) \ge y,\\ (m,\ v) & \text{if } f(m) < y. \end{cases}$ By trichotomy exactly one clause applies, so $F$ is a function on $X$ ; and $F(u,v) \in X$ in both clauses, since in the first $f(u) \le y \le f(m)$ and in the second $f(m) \le y \le f(v)$ . The left half is tested first and the right half is taken only when the left is excluded, so nothing is selected.

L8construct

2.1

The nested sequence. By [L2] applied to $X$ , the element $(a,b)$ and the map $F$ , there is a unique $g : \mathbb{N} \to X$ with $g(0) = (a,b)$ and $g(k+1) = F(g(k))$ . Write $g(k) = (a_k,b_k)$ and $I_k := [a_k,b_k]$ . Then for every $k$ : $a \le a_k \le b_k \le b$ and $f(a_k) \le y \le f(b_k)$ , because $g(k) \in X$ ; and $I_{k+1} \subseteq I_k$ , since in either clause of the definition of $F$ the new endpoints lie in $[a_k,b_k]$ and the new interval is $[a_k,m_k]$ or $[m_k,b_k]$ with $m_k = (a_k+b_k)/2$ .

step 1.2L2L8

3.1

The lengths. In both clauses the new length is $m_k - a_k = (b_k - a_k)/2$ or $b_k - m_k = (b_k - a_k)/2$ , so $b_{k+1} - a_{k+1} = (b_k - a_k)/2$ ; with $b_0 - a_0 = b - a$ an induction on $k$ gives $b_k - a_k = (b-a)\,(2^{-1})^{k}$ for every $k \in \mathbb{N}$ , that is $(b-a)/2^{k}$ by [L5]. Since $|2^{-1}| < 1$ , [L4] gives $(2^{-1})^{k} \to 0$ and hence $b_k - a_k \to 0$ .

step 2.1L4L5L8

4.1

The point. By [L3] applied to the nested family $(I_k)$ , whose lengths tend to $0$ by step 3.1, the intersection $\bigcap_k I_k$ is a single point; call it $c$ . Then $c \in I_0 = [a,b]$ and $a_k \le c \le b_k$ for every $k$ .

step 2.1step 3.1L3construct

5.1

The endpoints converge to $c$ . Let a rational $\varepsilon > 0$ be given. By step 3.1 there is $K$ with $b_k - a_k < \varepsilon$ for all $k \ge K$ . For such $k$ , from $a_k \le c \le b_k$ we get $-(b_k - a_k) \le a_k - c \le 0$ and $0 \le b_k - c \le b_k - a_k$ , so $|a_k - c| \le b_k - a_k < \varepsilon$ and $|b_k - c| \le b_k - a_k < \varepsilon$ by [L8]. Hence $a_k \to c$ and $b_k \to c$ .

step 3.1step 4.1L8

6.1

Passing to the limit. The point $c$ lies in $[a,b]$ , so $f$ is continuous at $c$ , and [L6] applied to the two sequences of step 5.1 gives $f(a_k) \to f(c)$ and $f(b_k) \to f(c)$ .

step 4.1step 5.1L6

7.1

By step 2.1, $f(a_k) \le y$ for every $k$ ; the constant sequence with value $y$ converges to $y$ by [L4], so [L7] gives $f(c) \le y$ . Likewise $y \le f(b_k)$ for every $k$ gives $y \le f(c)$ . Hence $f(c) = y$ .

step 2.1step 6.1L4L7L8

8.1

A point $c \in [a,b]$ with $f(c) = y$ has therefore been constructed, under the reduction of step 1.1 and hence in both cases of the hypothesis.

step 1.1step 4.1step 7.1discharge-construct: c is the unique point of the nested intersection∎

Remarks

Why the left half is tested first. The bisection has to choose one of two halves at every stage, and if the rule were "choose a half in which the sign change persists" the construction would be a dependent choice, not a recursion. Testing $f(m) \ge y$ and taking the left half in that case makes the successor a function of its predecessor, so The recursion theorem applies verbatim. The same device is used in Every nonempty perfect subset of $\mathbb{R}$ is uncountable and in the bisection proof of Heine-Borel.
What the theorem does not say. It does not say that $c$ is unique, and it does not say that the set of solutions is an interval; $f$ may take the value $y$ on a complicated set. It also does not say that a function with the intermediate value property is continuous — that converse is false, and the witness for it needs machinery that is not available at this point in the reading order.
Only the choice-free direction of the sequential criterion is used. Step 6.1 turns a convergent sequence into a convergent image sequence, which is the implication proved in ZF ( $f$ is continuous at $c \in A$ if and only if $f(x_k) \to f(c)$ for every sequence in $A$ converging to $c$ , the converse direction costing countable choice); the converse, which spends countable choice, is never invoked here.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 118 results over 30 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Intermediate value theorem (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 4 (Thm 4.23) (standard reference, not scraped)
J. Lebl, Basic Analysis I, §3.3 (standard reference, not scraped)
E. Zakon, Mathematical Analysis, §4.9: The Intermediate Value Property (standard reference, not scraped)

Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on [a,b][a,b][a,b] takes every value between f(a)f(a)f(a) and f(b)f(b)f(b)