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.

Cauchy completeness plus the Archimedean property imply the monotone convergence property

Statement

Let $F$ be an Archimedean ordered field (Archimedean ordered field) with Cauchy completeness (CC). Then $F$ has the monotone convergence property (MCT) of The five completeness properties of an ordered field: least upper bound, monotone convergence, nested intervals, Bolzano-Weierstrass, and Cauchy completeness: every nondecreasing sequence in $F$ that is bounded above converges in $F$ .

The Archimedean hypothesis is not decoration. Without it the implication is false: $R ((t^{- 1}))$ has (CC) (Every Cauchy sequence in $R ((t^{- 1}))$ converges: $K$ is sequentially Cauchy complete) and fails (MCT), since (MCT) would force it to be Archimedean (The monotone convergence property alone forces the Archimedean property, so it carries no separate Archimedean hypothesis) and it is not ( $R ((t^{- 1}))$ is non-Archimedean, and the monomials $t^{- k}$ are cofinal below its positive elements).

Facts & Assumptions

Given: An Archimedean ordered field $F$ with (CC), and a nondecreasing sequence $(x_{k})$ in $F$ with $x_{k} \leq B$ for every $k$ and some $B \in F$ .

[L1]

The properties (MCT) and (CC) 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: $(x_{k})$ is nondecreasing when $x_{j} \leq x_{k}$ for all $j \leq k$ ; it is Cauchy in $F$ when for every $ε > 0$ in $F$ there is $N$ with $∣ x_{k} - x_{l} ∣ < ε$ for all $k, l \geq N$ ; convergence in $F$ is as fixed there (Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field).

[L3]

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

[L4]

Recursion theorem (The recursion theorem); well-ordering principle, every nonempty subset of $N$ has a least element (The well-ordering principle); induction principle (The principle of mathematical induction); the order on $N$ is total ( $\leq$ is a linear order on $N$ ).

[L5]

Absolute value: $∣ u ∣ = u$ whenever $u \geq 0$ (Basic properties of the absolute value).

[L6]

Order arithmetic: 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; for $c > 0$ one has $a < b$ if and only if $a c < b c$ (Sign rules for products and monotonicity of multiplication); a positive element is invertible with positive inverse (Inverses of positives are positive, and reciprocation reverses order); the order is total and transitive (Ordered field).

Proof

technique · contradiction

1.1

Suppose $(x_{k})$ is not Cauchy in $F$ : there is $ε > 0$ in $F$ such that for every $N \in N$ there are $k, l \geq N$ with $∣ x_{k} - x_{l} ∣ \geq ε$ .

L2assume-contra

2.1

For every $n \in N$ there is $k > n$ with $x_{k} - x_{n} \geq ε$ : apply step 1.1 with $N : = n + 1$ to get $k, l \geq n + 1$ with $∣ x_{k} - x_{l} ∣ \geq ε$ , name them so that $l \leq k$ , note that monotonicity gives $x_{l} \leq x_{k}$ and hence $∣ x_{k} - x_{l} ∣ = x_{k} - x_{l} \geq ε$ , and note that $n < l$ gives $x_{n} \leq x_{l}$ , so $x_{k} - x_{n} \geq x_{k} - x_{l} \geq ε$ with $k \geq n + 1 > n$ .

step 1.1L2L4L5L6

3.1

For each $n$ the set ${k \in N : k > n and x_{k} - x_{n} \geq ε}$ is therefore nonempty and has a least element, so $f (n) : = \min {k : k > n, x_{k} - x_{n} \geq ε}$ is a total function $N \to N$ ; the recursion theorem applied to $N$ , the element $0$ and $f$ gives indices $k_{0} = 0$ and $k_{j + 1} = f (k_{j})$ , with $k_{j} < k_{j + 1}$ and $x_{k_{j + 1}} - x_{k_{j}} \geq ε$ for every $j$ .

step 2.1L4

4.1

By induction on $j$ , $x_{k_{j}} - x_{k_{0}} \geq (j \cdot 1_{F}) ε$ for every $j$ : at $j = 0$ both sides are $0$ , and adding $x_{k_{j + 1}} - x_{k_{j}} \geq ε$ to the inductive inequality gives $x_{k_{j + 1}} - x_{k_{0}} \geq (j \cdot 1_{F}) ε + ε = ((j + 1) \cdot 1_{F}) ε$ .

step 3.1L3L4L6

5.1

Since $ε > 0$ is invertible with $ε^{- 1} > 0$ , the Archimedean property supplies $j \geq 1$ with $(B - x_{k_{0}}) ε^{- 1} < j \cdot 1_{F}$ , hence $B - x_{k_{0}} < (j \cdot 1_{F}) ε$ and $x_{k_{j}} \geq x_{k_{0}} + (j \cdot 1_{F}) ε > B$ , contradicting the hypothesis that $B$ bounds every term of $(x_{k})$ .

step 4.1L3L6

6.1

The assumption of step 1.1 is therefore untenable, so $(x_{k})$ is Cauchy in $F$ and (CC) makes it converge in $F$ ; as $(x_{k})$ was an arbitrary nondecreasing sequence bounded above, $F$ has (MCT).

step 5.1L1L2discharge-contradiction∎

Remarks

What the Archimedean property does here. It is used exactly once, in the final estimate, to say that a fixed positive $ε$ added to itself often enough exceeds a given element. In a non-Archimedean field the increments $ε$ of the recursion can be infinitesimal relative to $B - x_{k_{0}}$ , and the sequence $(x_{k_{j}})$ climbs forever without ever passing $B$ ; that is exactly how (CC) survives while (MCT) fails.
No choice is used: the recursion takes the least admissible index, supplied by The well-ordering principle, and it is The recursion theorem applied to a function defined outright.

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

41 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)
Monotone convergence theorem (Wikipedia) (standard reference, not scraped)
Cauchy sequence (Wikipedia) (standard reference, not scraped)
J. Lebl, Basic Analysis I, §2.4 (standard reference, not scraped)