Alphabeta Math
CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck 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≥1 with 1/n<ε

Statement

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

1n⋅1F<ε,

where n⋅1F is the canonical natural of F (Every complete ordered field is Archimedean) and 1/(n⋅1F) is its multiplicative inverse (Field). As is standard we abbreviate n⋅1F 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⋅1F; 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 ε∈F with ε>0.

[L1]

Archimedean property: for every x∈F there is a natural number n≥1 with x<n⋅1F (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 ε≠0, so ε−1 exists, and ε−1>0.

givenL2L3
2.1

Apply [L1] to x=ε−1: fix a natural number n≥1 with ε−1<n⋅1F.

step 1.1L1choose
3.1

Chaining the two displayed inequalities gives 0<ε−1<n⋅1F; in particular n⋅1F>0, so n⋅1F≠0 and 1/(n⋅1F) is defined.

step 1.1step 2.1L3
4.1

Apply the second claim of [L2] with a=ε−1 and b=n⋅1F: 0<(n⋅1F)−1<(ε−1)−1.

step 3.1L2
5.1

By [L3], (ε−1)−1=ε, so the natural number n≥1 fixed in step 2.1 satisfies 1/(n⋅1F)<ε, which is the assertion.

step 4.1L3∎

Remarks

  • Monotonicity gives the eventual form for free. If m≥n≥1 then m⋅1F≥n⋅1F>0, because k↦k⋅1F is strictly increasing on the naturals ≥1 (Canonical naturals are positive and strictly increasing), and so 1/(m⋅1F)≤1/(n⋅1F)<ε by Inverses of positives are positive, and reciprocation reverses order again. So the corollary yields not merely one index but a threshold: every m≥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 220 more results.

Dependency tree · two levels

8 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