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 alone forces the Archimedean property, so it carries no separate Archimedean hypothesis

Statement

Let $F$ be an 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$ is Archimedean (Archimedean ordered field).

So (MCT), like (BW) and like (LUB), carries the Archimedean property on its own, and the hypothesis attached to (CC) in Cauchy completeness plus the Archimedean property imply the monotone convergence property need not be attached here. This is what lets Which of the five completeness properties carry the Archimedean property on their own, and which must be handed it sort the five properties into those that do and those that do not.

Facts & Assumptions

Given: An ordered field $F$ with (MCT).

[L1]

The property (MCT): every nondecreasing sequence in $F$ that is bounded above converges in $F$ (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: a sequence is a function $\mathbb{N} \to F$ ; it is nondecreasing when $x_j \le x_k$ for all $j \le k$ ; convergence and Cauchyness in $F$ are as fixed there (Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field).

[L3]

Archimedean property: $F$ is Archimedean when for every $x \in F$ there is a natural $n$ with $x < n \cdot 1_F$ , where $0 \cdot 1_F = 0$ and $(n+1)\cdot 1_F = n \cdot 1_F + 1_F$ (Archimedean ordered field).

[L4]

Canonical naturals: $n \cdot 1_F > 0$ for $n \ge 1$ and $n \mapsto n \cdot 1_F$ is strictly increasing on $\{1,2,3,\dots\}$ (Canonical naturals are positive and strictly increasing).

[L5]

A sequence converging in $F$ is Cauchy in $F$ (clause 3 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).

[L6]

Order arithmetic: $0 < 1_F$ (The multiplicative identity is positive); the order is total, so the failure of $x < y$ is $y \le x$ ; adding a constant preserves the order (Order is preserved by adding a constant and by adding inequalities, Ordered field); and $|u| = u$ whenever $u \ge 0$ (Basic properties of the absolute value). Here Order is preserved by adding a constant and by adding inequalities states the STRICT forms and only those; the nonstrict forms used below are those together with the equality cases, which trichotomy settles, the order being total (Ordered field).

Proof

technique · contradiction

1.1

Suppose $F$ has (MCT) and is not Archimedean; then there is $x \in F$ with $n \cdot 1_F \le x$ for every $n \in \mathbb{N}$ .

L3L6assume-contra

1.2

Let $(y_k)$ be the sequence $y_k := k \cdot 1_F$ in $F$ , so $y_0 = 0$ and $y_{k+1} = y_k + 1_F$ ; it is nondecreasing, since $0 = y_0 < y_n$ for $n \ge 1$ and $j \mapsto j \cdot 1_F$ is strictly increasing on the positive naturals.

L2L3L4

2.1

$(y_k)$ is bounded above by $x$ , so (MCT) makes it converge in $F$ to some $L$ .

step 1.1step 1.2L1L2

3.1

Being convergent, $(y_k)$ is Cauchy in $F$ , so, $1_F$ being positive, there is $N \in \mathbb{N}$ with $|y_k - y_l| < 1_F$ for all $k, l \ge N$ .

step 2.1L2L5L6

4.1

But $y_{N+1} - y_N = 1_F > 0$ , so $|y_{N+1} - y_N| = 1_F$ , which is not $< 1_F$ ; this contradicts step 3.1.

step 1.2step 3.1L6

5.1

The assumption of step 1.1 is therefore untenable, and an ordered field with (MCT) is Archimedean.

step 4.1discharge-contradiction∎

Remarks

Why this item exists. Without it, the natural reading of the equivalence theorem would attach an Archimedean hypothesis to (MCT) as well, and Which of the five completeness properties carry the Archimedean property on their own, and which must be handed it would answer its own question wrongly. With it the answer is clean: (LUB), (BW) and (MCT) each imply the Archimedean property, while (NIP) and (CC) do not (FALSE: the nested interval property alone implies the least-upper-bound property, FALSE: an ordered field in which every Cauchy sequence converges has the least-upper-bound property).
The witness is the same sequence as in Bolzano-Weierstrass alone forces the Archimedean property, so it needs no separate Archimedean hypothesis, the canonical naturals, but the two arguments use different failures of it. There the sequence is bounded and has no convergent subsequence; here it is nondecreasing and bounded above and has no limit. Neither argument implies the other, because neither (BW) nor (MCT) is assumed in the other's proof.
The gap of exactly $1_F$ between consecutive terms is what does the work, and it is available in every ordered field: $1_F > 0$ by The multiplicative identity is positive, and no smallness of $1_F$ relative to $x$ is possible, since the Cauchy condition is tested at the threshold $1_F$ itself.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 70 results over 13 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)
Archimedean property (Wikipedia) (standard reference, not scraped)
Monotone convergence theorem (Wikipedia) (standard reference, not scraped)
J. Lebl, Basic Analysis I, §1.2 and §2.4 (standard reference, not scraped)