Alphabeta Math
LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck passverified 2026-08-05 (gpt-5.6-sol-codex-subscription)
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.

Every convergent sequence is bounded

Statement

Let (xk) be a sequence of reals converging to x∈R (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals). Then (xk) is bounded: there is M∈R with ∣xk∣≤M for every k∈N.

Facts & Assumptions

[L1]

Convergence: for every rational ε>0 there is K∈N with ∣xk−x∣<ε for all k≥K (Limits and Cauchy sequences of reals); and 1 is a rational >0, since Q is an ordered field (The rationals form a totally ordered field) and 0<1 in every ordered field (The multiplicative identity is positive).

[L2]

Triangle inequality: ∣a+b∣≤∣a∣+∣b∣ in R (The triangle inequality, Complete ordered field (least-upper-bound property)).

[L3]

Absolute value: ∣u∣≥0 for every real u (Basic properties of the absolute value).

[L4]

Finite maxima: for every n∈N and all reals a0,…,an the set {a0,…,an} has a maximum (Every nonempty finite set of reals has a maximum and a minimum); a maximum lies in the set and dominates every element of it (Maximum and minimum of a set).

[L5]

Order arithmetic in R: transitivity of ≤ and of <; both mixed forms, u<v≤w⇒u<w and u≤v<w⇒u<w, and the implication u<v⇒u≤v, all immediate from the reading of u≤v as "u<v or u=v" (Complete ordered field (least-upper-bound property), Ordered field); and translation invariance, a<b⇒a+c<b+c (Order is preserved by adding a constant and by adding inequalities).

[L6]

The order on N is total, so every index k satisfies k<K or k≥K (≤ is a linear order on N).

Proof

technique · direct
1.1

Apply convergence with the rational ε=1: fix K∈N such that ∣xk−x∣<1 for all k≥K.

L1
2.1

For every k≥K we have ∣xk∣=∣(xk−x)+x∣≤∣xk−x∣+∣x∣, while adding ∣x∣ to both sides of ∣xk−x∣<1 gives ∣xk−x∣+∣x∣<1+∣x∣=∣x∣+1; composing the non-strict inequality with the strict one yields ∣xk∣<∣x∣+1.

step 1.1L2L5
2.2

Define M:=max⁡{ ∣x0∣,∣x1∣,…,∣xK−1∣,∣x∣+1 }, the maximum of the finite list obtained by appending ∣x∣+1 to the first K values ∣x0∣,…,∣xK−1∣; the list is nonempty because its last entry is always present (when K=0 the list is the single entry ∣x∣+1), so the maximum exists by [L4].

step 1.1L4choose
3.1

For every k<K the value ∣xk∣ is one of the entries of that list, hence ∣xk∣≤M.

step 2.2L4
3.2

For every k≥K we have ∣xk∣<∣x∣+1≤M, since ∣x∣+1 is an entry of the list, hence ∣xk∣≤M.

step 2.1step 2.2L4L5
4.1

Every index satisfies k<K or k≥K, and in both cases ∣xk∣≤M; therefore (xk) is bounded.

step 3.1step 3.2L3L6∎

Remarks

Depends on

Used by

Dependency tree · two levels

35 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