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

The monotone convergence property plus the Archimedean property imply the least-upper-bound property

Statement

Let $F$ be an Archimedean ordered field (Archimedean ordered field) with 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. Then $F$ has the least-upper-bound property (LUB), that is, $F$ is a complete ordered field (Complete ordered field (least-upper-bound property)).

The Archimedean hypothesis is stated for symmetry with the other implications on this page and is in fact redundant here: (MCT) implies it on its own (The monotone convergence property alone forces the Archimedean property, so it carries no separate Archimedean hypothesis).

The supremum is produced by bisection between an upper bound and a non-upper bound, and it is identified as a limit of both bracketing sequences.

Facts & Assumptions

Given: An Archimedean ordered field $F$ with (MCT), a nonempty $S \subseteq F$ bounded above by some $B \in F$ , and an element $s_0 \in S$ .

[L1]

The properties (MCT) and (LUB), and least upper bounds: $u$ is an upper bound of $S$ when $s \le u$ for all $s \in S$ , and a least upper bound when moreover $u \le v$ for every upper bound $v$ ; (LUB) says every nonempty subset bounded above has one (The five completeness properties of an ordered field: least upper bound, monotone convergence, nested intervals, Bolzano-Weierstrass, and Cauchy completeness, Complete ordered field (least-upper-bound property), Upper bound, least upper bound, and strict upper bound).

[L2]

Sequences in an ordered field: nondecreasing, nonincreasing, bounded above, and convergence in $F$ (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 \ge 1$ with $z < n \cdot 1_F$ (Archimedean ordered field); the canonical naturals are positive for $n \ge 1$ and satisfy $n \cdot 1_F \le m \cdot 1_F$ for $n \le m$ (Canonical naturals are positive and strictly increasing).

[L4]

Recursion theorem (The recursion theorem), induction principle (The principle of mathematical induction), and totality of the order on $\mathbb{N}$ ( $\le$ is a linear order on $\mathbb{N}$ ).

[L5]

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

[L6]

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 (Ordered field).

[L7]

Absolute value: $|u| \ge 0$ , $|u| = |-u|$ , $|u| = u$ for $u \ge 0$ (Basic properties of the absolute value); and $|u + v| \le |u| + |v|$ (The triangle inequality).

[L8]

Limits in an ordered field preserve non-strict inequalities (clause 2 of Sequence basics in an arbitrary ordered field: limits are unique, limits preserve non-strict inequalities, convergent sequences are Cauchy, Cauchy sequences are bounded, and a Cauchy sequence with a convergent subsequence converges).

Proof

technique · constructive

1.1

Put $u_0 := B$ and $l_0 := s_0 - 1_F$ ; then $u_0$ is an upper bound of $S$ , $l_0$ is not one because $s_0 \in S$ and $l_0 < s_0$ , and $l_0 < s_0 \le u_0$ .

L1L6construct

1.2

Writing $m(l,u) := (l + u)\,(2 \cdot 1_F)^{-1}$ , define $f : F \times F \to F \times F$ by $f(l,u) := (l, m(l,u))$ when $m(l,u)$ is an upper bound of $S$ and $f(l,u) := (m(l,u), u)$ otherwise; the recursion theorem applied to $F \times F$ , the element $(l_0, u_0)$ and $f$ gives a unique $g : \mathbb{N} \to F \times F$ with $g(0) = (l_0,u_0)$ and $g(n+1) = f(g(n))$ , and we write $g(n) = (l_n, u_n)$ .

L4L6construct

1.3

A constant sequence in $F$ converges to its value, since $|a - a| = 0 < \varepsilon$ for every $\varepsilon > 0$ .

L2L7

2.1

By induction on $n$ : $u_n$ is an upper bound of $S$ ; $l_n$ is not an upper bound of $S$ ; $l_n \le l_{n+1} \le u_{n+1} \le u_n$ ; and $u_n - l_n = (u_0 - l_0)\,((2 \cdot 1_F)^n)^{-1}$ . The base case is step 1.1 together with $(2 \cdot 1_F)^0 = 1_F$ ; for the step, $m := m(l_n,u_n)$ satisfies $l_n \le m \le u_n$ and $m - l_n = u_n - m = (u_n - l_n)(2 \cdot 1_F)^{-1}$ , and whichever of the two clauses of $f$ applies, the retained pair again brackets $S$ in the stated sense with half the previous length.

step 1.1step 1.2L1L5L6

3.1

The lengths tend to $0$ in $F$ : given $\varepsilon > 0$ , the element $(u_0 - l_0)\varepsilon^{-1}$ is positive, so [L3] supplies $n \ge 1$ with $(u_0-l_0)\varepsilon^{-1} < n \cdot 1_F$ , and for every $p \ge n$ Bernoulli at $x = 1_F$ gives $(2 \cdot 1_F)^p \ge 1_F + p \cdot 1_F > p \cdot 1_F \ge n \cdot 1_F > (u_0-l_0)\varepsilon^{-1} > 0$ , whence $u_p - l_p = (u_0-l_0)((2 \cdot 1_F)^p)^{-1} < \varepsilon$ .

step 2.1L3L5L6

3.2

The sequence $(-u_n)$ is nondecreasing and is bounded above by $-l_0$ , since $l_0 \le l_n \le u_n$ for every $n$ ; so (MCT) gives $w \in F$ with $-u_n \to w$ , and putting $c := -w$ one has $|u_n - c| = |{-}((-u_n) - w)| = |(-u_n) - w|$ , so $u_n \to c$ in $F$ .

step 2.1L1L2L6L7

4.1

$l_n \to c$ in $F$ : given $\varepsilon > 0$ , step 3.1 supplies $N_1$ with $u_n - l_n < \varepsilon/2$ for $n \ge N_1$ and step 3.2 supplies $N_2$ with $|u_n - c| < \varepsilon/2$ for $n \ge N_2$ , and for $n$ beyond both, $|l_n - c| \le |l_n - u_n| + |u_n - c| = (u_n - l_n) + |u_n - c| < \varepsilon$ .

step 3.1step 3.2L2L4L6L7

4.2

$c$ is an upper bound of $S$ : for $s \in S$ one has $s \le u_n$ for every $n$ by step 2.1, and the constant sequence with value $s$ converges to $s$ while $u_n \to c$ , so $s \le c$ by [L8].

step 1.3step 2.1step 3.2L1L8

5.1

$c$ is the least upper bound: let $v$ be any upper bound of $S$ ; for each $n$ the element $l_n$ is not an upper bound, so some $s \in S$ has $l_n < s \le v$ and hence $l_n \le v$ ; since $l_n \to c$ and the constant sequence with value $v$ converges to $v$ , [L8] gives $c \le v$ .

step 1.3step 2.1step 4.1L1L6L8

6.1

So $c = \sup S$ exists in $F$ ; as $S$ was an arbitrary nonempty subset bounded above, $F$ has (LUB) and is a complete ordered field.

step 4.2step 5.1L1discharge-construct∎

Remarks

Both bracketing sequences are needed. The upper endpoints give the upper-bound half of the conclusion and the lower endpoints give minimality; the shrinking lengths are what force the two to have the same limit, and that is the only place the Archimedean property is used.
Nonincreasing sequences are handled by reflection, as announced in The five completeness properties of an ordered field: least upper bound, monotone convergence, nested intervals, Bolzano-Weierstrass, and Cauchy completeness: (MCT) is stated only for nondecreasing sequences, and step 3.2 applies it to $(-u_n)$ rather than assuming a second form of the property.
No choice is used. The bisection rule keeps the left half exactly when the midpoint is an upper bound of $S$ , which is a definite condition, so $f$ is a function and The recursion theorem applies.

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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 99 results over 24 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

J. F. Hall, Completeness of Ordered Fields (standard reference, not scraped)
Least-upper-bound property (Wikipedia) (standard reference, not scraped)
Monotone convergence theorem (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 and Ch. 3 (standard reference, not scraped)