LemmaStatement: AI-adaptedProof: AI-generatedprecheck 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.

Nested intervals plus the Archimedean property imply Bolzano-Weierstrass, by repeated bisection

Statement

Let $F$ be an ordered field that is Archimedean (Archimedean ordered field) and has the nested interval property (NIP) of The five completeness properties of an ordered field: least upper bound, monotone convergence, nested intervals, Bolzano-Weierstrass, and Cauchy completeness. Then $F$ has the Bolzano-Weierstrass property (BW): every bounded sequence in $F$ has a subsequence converging in $F$ .

Say that a set $E \subseteq N$ is cofinal when for every $K \in N$ there is $k \geq K$ with $k \in E$ . The construction below bisects a bracketing interval, keeping at each stage a half that the sequence visits cofinally often, and reads the limit off (NIP).

Facts & Assumptions

Given: An Archimedean ordered field $F$ with (NIP), and a bounded sequence $(x_{k})$ in $F$ , so that $∣ x_{k} ∣ \leq M_{0}$ for every $k$ and some $M_{0} \in F$ .

[L1]

The properties (NIP) and (BW) of The five completeness properties of an ordered field: least upper bound, monotone convergence, nested intervals, Bolzano-Weierstrass, and Cauchy completeness.

[L2]

Sequences in an ordered field: boundedness, $[a, b]_{F} = {x \in F : a \leq x \leq b}$ for $a \leq b$ , nesting, lengths tending to $0$ in $F$ , convergence in $F$ , and subsequences along a strictly increasing index map (Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field).

[L3]

Archimedean property: for every $x \in F$ there is a natural number $n$ with $x < n \cdot 1_{F}$ (Archimedean ordered field); and the canonical naturals satisfy $n \cdot 1_{F} > 0$ for $n \geq 1$ and $n \cdot 1_{F} \leq m \cdot 1_{F}$ whenever $n \leq m$ (Canonical naturals are positive and strictly increasing).

[L4]

Recursion theorem (The recursion theorem).

[L5]

Well-ordering principle: every nonempty subset of $N$ has a least element (The well-ordering principle).

[L6]

Consecutive comparisons suffice for strict increase: if $n_{j} < n_{j + 1}$ for every $j$ then $n$ is strictly increasing (A strictly increasing index map satisfies $n_{k} \geq k$ ).

[L7]

Powers and Bernoulli: $a^{0} = 1$ and $a^{n + 1} = a^{n} a$ (Integer powers $a^{m}$ ); and $(1_{F} + x)^{n} \geq 1_{F} + n \cdot x$ for $x \geq - 1_{F}$ (Bernoulli's inequality $(1 + x)^{n} \geq 1 + n x$ ).

[L8]

Order arithmetic: $0 < 1_{F}$ (The multiplicative identity is positive); adding a constant preserves the strict order and strict inequalities add (Order is preserved by adding a constant and by adding inequalities), the nonstrict forms following with the equality cases; $a > 0$ gives $a^{- 1} > 0$ , and $0 < a < b$ gives $0 < b^{- 1} < a^{- 1}$ (Inverses of positives are positive, and reciprocation reverses order); the order is total and transitive and sums and products of positives are positive (Ordered field).

[L9]

Absolute value: $∣ u ∣ \geq 0$ , and $∣ u ∣$ equals $u$ or $- u$ , so $∣ u ∣ \leq c$ whenever both $u \leq c$ and $- u \leq c$ (Basic properties of the absolute value).

[L10]

Induction principle (The principle of mathematical induction) and totality of the order on $N$ ( $\leq$ is a linear order on $N$ ).

Proof

technique · constructive

1.1

Since $M_{0} \geq ∣ x_{0} ∣ \geq 0$ , the element $M : = M_{0} + 1_{F}$ satisfies $M > 0$ and $∣ x_{k} ∣ \leq M_{0} < M$ for every $k$ , so $- M \leq x_{k} \leq M$ and $x_{k} \in [- M, M]_{F}$ for every $k$ .

L2L8L9construct

1.2

Writing $m (a, b) : = (a + b) \cdot (2 \cdot 1_{F})^{- 1}$ , define $f : F \times F \to F \times F$ by $f (a, b) : = (a, m (a, b))$ when $a \leq b$ and the set of $k$ with $x_{k} \in [a, m (a, b)]_{F}$ is cofinal, and $f (a, b) : = (m (a, b), b)$ otherwise; the recursion theorem applied to $F \times F$ , the element $(- M, M)$ and $f$ gives a unique $g : N \to F \times F$ with $g (0) = (- M, M)$ and $g (n + 1) = f (g (n))$ , and we write $g (n) = (a_{n}, b_{n})$ and $I_{n} : = [a_{n}, b_{n}]_{F}$ .

L4L8construct

2.1

By induction on $n$ , all of the following hold: $a_{n} \leq b_{n}$ ; $b_{n} - a_{n} = 2 M \cdot ((2 \cdot 1_{F})^{n})^{- 1}$ ; $I_{n + 1} \subseteq I_{n}$ ; and the set $E_{n} : = {k : x_{k} \in I_{n}}$ is cofinal. For $n = 0$ this is step 1.1 together with $b_{0} - a_{0} = 2 M$ and $(2 \cdot 1_{F})^{0} = 1_{F}$ . For the step, put $m : = m (a_{n}, b_{n})$ , so that $a_{n} \leq m \leq b_{n}$ and $m - a_{n} = b_{n} - m = (b_{n} - a_{n}) \cdot (2 \cdot 1_{F})^{- 1}$ ; if the first clause of $f$ applies then $I_{n + 1} = [a_{n}, m]_{F}$ has the four properties by construction, and otherwise there is $K$ with $x_{k} \notin [a_{n}, m]_{F}$ for all $k \geq K$ , so every $k \geq K$ in the cofinal set $E_{n}$ has $m < x_{k} \leq b_{n}$ and hence lies in ${k : x_{k} \in [m, b_{n}]_{F}}$ , which is therefore cofinal as well.

step 1.1step 1.2L2L7L8L9L10

3.1

The lengths $b_{n} - a_{n}$ tend to $0$ in $F$ : given $ε > 0$ , the element $2 M ε^{- 1}$ is positive, so [L3] supplies $n \geq 1$ with $2 M ε^{- 1} < n \cdot 1_{F}$ , and then for every $p \geq n$ Bernoulli at $x = 1_{F}$ gives $(2 \cdot 1_{F})^{p} \geq 1_{F} + p \cdot 1_{F} > p \cdot 1_{F} \geq n \cdot 1_{F} > 2 M ε^{- 1} > 0$ , whence $((2 \cdot 1_{F})^{p})^{- 1} < ε (2 M)^{- 1}$ and $b_{p} - a_{p} = 2 M \cdot ((2 \cdot 1_{F})^{p})^{- 1} < ε$ .

step 2.1L3L7L8

3.2

Since each $E_{j}$ is cofinal, for every $j$ and every $n$ the set ${k \in N : k > n and x_{k} \in I_{j + 1}}$ is nonempty and so has a least element; the recursion theorem applied to $N \times N$ , the element $(0, 0)$ and the map sending $(j, n)$ to $(j + 1, \min {k : k > n, x_{k} \in I_{j + 1}})$ therefore yields indices $n_{0} = 0$ and $n_{j + 1} = \min {k : k > n_{j}, x_{k} \in I_{j + 1}}$ .

step 2.1L4L5construct

4.1

The sequence $(I_{n})$ is nested with lengths tending to $0$ , so (NIP) supplies an element $c$ lying in $I_{n}$ for every $n$ .

step 2.1step 3.1L1L2

4.2

Since $n_{j} < n_{j + 1}$ for every $j$ , the map $j \mapsto n_{j}$ is strictly increasing and $(x_{n_{j}})$ is a subsequence of $(x_{k})$ ; moreover $x_{n_{j}} \in I_{j}$ for every $j$ , the case $j = 0$ being $x_{0} \in I_{0}$ from step 1.1.

step 3.2L2L6

5.1

For every $j$ , both $x_{n_{j}}$ and $c$ lie in $I_{j}$ , so $x_{n_{j}} - c \leq b_{j} - a_{j}$ and $c - x_{n_{j}} \leq b_{j} - a_{j}$ , whence $∣ x_{n_{j}} - c ∣ \leq b_{j} - a_{j}$ .

step 4.1step 4.2L2L8L9

6.1

Given $ε > 0$ in $F$ , step 3.1 supplies $J$ with $b_{j} - a_{j} < ε$ for all $j \geq J$ , so $∣ x_{n_{j}} - c ∣ < ε$ for all $j \geq J$ ; hence $x_{n_{j}} \to c$ in $F$ .

step 3.1step 5.1L2L8

7.1

An arbitrary bounded sequence in $F$ has therefore been given a subsequence converging in $F$ , so $F$ has (BW).

step 6.1L1discharge-construct∎

Remarks

No choice is used. Both recursions are applications of The recursion theorem to functions defined outright: the bisection rule keeps the left half exactly when that half is visited cofinally often, and the index $n_{j + 1}$ is the least admissible one, supplied by The well-ordering principle rather than chosen.
Where each hypothesis enters. (NIP) is used once, at step 4.1. The Archimedean property is used once, at step 3.1, and only to know that the halved lengths get below every positive element of $F$ . Without it the bisection still runs and still produces nested intervals, but their lengths need not tend to $0$ in $F$ , and (NIP) as stated would not apply.
The bracketing interval is widened by $1_{F}$ in step 1.1 so that $M > 0$ even when the sequence is identically $0$ ; the argument of step 3.1 divides by $2 M$ and would otherwise have to treat that case separately.

Depends on

Used by

For an ordered field the five completeness properties are equivalent, provided the Archimedean property is assumed alongside nested intervals and Cauchy completeness Theorem

Dependency tree · two levels

53 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

J. F. Hall, Completeness of Ordered Fields (standard reference, not scraped)
Bolzano-Weierstrass theorem (Wikipedia) (standard reference, not scraped)
Nested intervals (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 3 (standard reference, not scraped)