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.

Bolzano-Weierstrass alone forces the Archimedean property, so it needs no separate Archimedean hypothesis

Statement

Let $F$ be an ordered field with the Bolzano-Weierstrass property (BW) 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).

Consequently (BW) needs no Archimedean hypothesis attached to it, in contrast with the nested interval property and with Cauchy completeness, which do (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).

Facts & Assumptions

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

[L1]

The property (BW): every bounded sequence in $F$ has a subsequence converging 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 $N \to F$ ; it is bounded when $∣ x_{k} ∣ \leq M$ for every $k$ and some $M \in F$ ; a subsequence is taken along a strictly increasing $n : N \to N$ ; 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 number $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 \geq 1$ , the map $n \mapsto n \cdot 1_{F}$ is strictly increasing on ${1, 2, 3, \dots}$ , and $(m + n) \cdot 1_{F} = m \cdot 1_{F} + n \cdot 1_{F}$ (Canonical naturals are positive and strictly increasing).

[L5]

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

[L6]

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).

[L7]

Order arithmetic: $0 < 1_{F}$ (The multiplicative identity is positive); the order is total, so the failure of $x < y$ is $y \leq x$ ; adding a constant preserves the order (Order is preserved by adding a constant and by adding inequalities, Ordered field). 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).

[L8]

Discreteness of $N$ : $m < p$ if and only if $m + 1 \leq p$ (Discreteness: $σ (n)$ is the immediate successor).

Proof

technique · contradiction

1.1

Suppose $F$ has (BW) and is not Archimedean; then there is $x \in F$ such that $x < n \cdot 1_{F}$ fails for every natural $n$ , that is, $n \cdot 1_{F} \leq x$ for every $n \in N$ .

L3L7assume-contra

1.2

Let $(y_{k})$ be the sequence in $F$ given by $y_{k} : = k \cdot 1_{F}$ , so that $y_{0} = 0$ , $y_{k + 1} = y_{k} + 1_{F}$ , and $y_{k} \geq 0$ for every $k$ .

L2L3L4

2.1

$(y_{k})$ is bounded: $∣ y_{k} ∣ = y_{k} \leq x$ for every $k$ .

step 1.1step 1.2L2L5

3.1

By (BW) there is a strictly increasing $n : N \to N$ and an $L \in F$ with $y_{n_{j}} \to L$ in $F$ .

step 2.1L1L2

4.1

The subsequence $(y_{n_{j}})$ is therefore Cauchy in $F$ , so, $1_{F}$ being positive, there is $J \in N$ with $∣ y_{n_{j}} - y_{n_{i}} ∣ < 1_{F}$ for all $i, j \geq J$ .

step 3.1L2L6L7

5.1

But $n_{J} < n_{J + 1}$ gives $n_{J} + 1 \leq n_{J + 1}$ and hence $y_{n_{J + 1}} \geq y_{n_{J} + 1} = y_{n_{J}} + 1_{F}$ , so $y_{n_{J + 1}} - y_{n_{J}} \geq 1_{F} > 0$ and $∣ y_{n_{J + 1}} - y_{n_{J}} ∣ \geq 1_{F}$ , contradicting step 4.1.

step 1.2step 4.1L4L5L7L8

6.1

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

step 5.1discharge-contradiction∎

Remarks

The witness sequence is the obstruction itself. In a non-Archimedean field the canonical naturals are bounded, so they form a bounded sequence; and no subsequence of them can converge, because consecutive terms of any subsequence stay at distance at least $1_{F}$ . That is the whole argument, and it shows that (BW) fails in every non-Archimedean ordered field, for instance in $R (t)$ (Not every ordered field is Archimedean) and in $R ((t^{- 1}))$ ( $R ((t^{- 1}))$ is non-Archimedean, and the monomials $t^{- k}$ are cofinal below its positive elements).
Note which direction is being used: the sequence is bounded and has no convergent subsequence, so (BW) is contradicted. Nothing here says that $(y_{k})$ fails to be Cauchy for some other reason; it is Cauchy along no subsequence at all.

Depends on

Used by

Dependency tree · two levels

36 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)
Archimedean property (Wikipedia) (standard reference, not scraped)
Bolzano-Weierstrass theorem (Wikipedia) (standard reference, not scraped)
J. Lebl, Basic Analysis I, §1.2 and §2.3 (standard reference, not scraped)