CorollaryStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26

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.

For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$

Statement

Let $F$ be a complete ordered field (Complete ordered field (least-upper-bound property)) and let $ε \in F$ with $ε > 0$ . Then there is a natural number $n \geq 1$ such that

$\frac{1}{n \cdot 1_{F}} < ε,$

where $n \cdot 1_{F}$ is the canonical natural of $F$ (Every complete ordered field is Archimedean) and $1 / (n \cdot 1_{F})$ is its multiplicative inverse (Field). As is standard we abbreviate $n \cdot 1_{F}$ to $n$ and write the conclusion $1 / n < ε$ .

This is the reciprocal form of the Archimedean property. Every complete ordered field is Archimedean on its own delivers only the assertion that the canonical naturals are cofinal, $x < n \cdot 1_{F}$ ; the form actually used in analysis, that the reciprocals of the naturals get below every positive bound, is the statement above, and it is recorded separately so that no proof has to reconstruct the inversion step in passing.

Facts & Assumptions

Given: A complete ordered field $F$ and an element $ε \in F$ with $ε > 0$ .

[L1]

Archimedean property: for every $x \in F$ there is a natural number $n \geq 1$ with $x < n \cdot 1_{F}$ (Every complete ordered field is Archimedean, Complete ordered field (least-upper-bound property)).

[L2]

Inverses and order: if $a > 0$ then $a^{- 1} > 0$ , and if $0 < a < b$ then $0 < b^{- 1} < a^{- 1}$ (Inverses of positives are positive, and reciprocation reverses order, Ordered field).

[L3]

Field arithmetic: an element $a$ with $a > 0$ is nonzero by trichotomy, hence has a multiplicative inverse $a^{- 1}$ , and $(a^{- 1})^{- 1} = a$ (Field, Ordered field).

Proof

technique · direct

1.1

Since $ε > 0$ , trichotomy gives $ε \neq 0$ , so $ε^{- 1}$ exists, and $ε^{- 1} > 0$ .

givenL2L3

2.1

Apply [L1] to $x = ε^{- 1}$ : fix a natural number $n \geq 1$ with $ε^{- 1} < n \cdot 1_{F}$ .

step 1.1L1choose

3.1

Chaining the two displayed inequalities gives $0 < ε^{- 1} < n \cdot 1_{F}$ ; in particular $n \cdot 1_{F} > 0$ , so $n \cdot 1_{F} \neq 0$ and $1 / (n \cdot 1_{F})$ is defined.

step 1.1step 2.1L3

4.1

Apply the second claim of [L2] with $a = ε^{- 1}$ and $b = n \cdot 1_{F}$ : $0 < (n \cdot 1_{F})^{- 1} < (ε^{- 1})^{- 1}$ .

step 3.1L2

5.1

By [L3], $(ε^{- 1})^{- 1} = ε$ , so the natural number $n \geq 1$ fixed in step 2.1 satisfies $1 / (n \cdot 1_{F}) < ε$ , which is the assertion.

step 4.1L3∎

Remarks

Monotonicity gives the eventual form for free. If $m \geq n \geq 1$ then $m \cdot 1_{F} \geq n \cdot 1_{F} > 0$ , because $k \mapsto k \cdot 1_{F}$ is strictly increasing on the naturals $\geq 1$ (Canonical naturals are positive and strictly increasing), and so $1 / (m \cdot 1_{F}) \leq 1 / (n \cdot 1_{F}) < ε$ by Inverses of positives are positive, and reciprocation reverses order again. So the corollary yields not merely one index but a threshold: every $m \geq n$ satisfies $1 / m < ε$ . That one extra line is what a convergence proof needs, and it is left to the caller rather than folded into the statement, because the caller usually has a threshold of its own to combine it with.
Completeness is used only through Every complete ordered field is Archimedean. Nothing here needs the least-upper-bound property directly. The corollary therefore holds verbatim in any Archimedean ordered field, in particular in $Q$ , and it fails in a non-Archimedean ordered field, where an infinitesimal $ε > 0$ is below every $1 / n$ by construction.
The equivalence is exact: the reciprocal form implies the cofinal form back again, since given $x > 0$ one applies it to $ε = 1 / x$ . The two are the same property written on the two sides of the inversion, and only the direction proved above is used in this library.

Depends on

Used by

…and 140 more results.

Dependency tree · next 3 levels

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

W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (Thm 1.20(a) and its corollaries) (standard reference, not scraped)
T. Tao, Analysis I, 3rd ed., §5.4 (Prop. 5.4.12, the Archimedean property) (standard reference, not scraped)
Archimedean property (Wikipedia) (standard reference, not scraped)
UTSA Mathematics: The Archimedean property (standard reference, not scraped)

For every ε>0ε>0 in a complete ordered field there is a natural n≥1n≥1 with 1/n<ε1/n<ε