LemmaStatement: Literature-sourcedProof: Literature-sourcedSession-authored (Fable 5 assisted)precheck 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 $(x_k)$ be a sequence of reals converging to $x \in \mathbb{R}$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals). Then $(x_k)$ is bounded: there is $M \in \mathbb{R}$ with $|x_k| \le M$ for every $k \in \mathbb{N}$ .

Facts & Assumptions

Given: A sequence $(x_k)$ of reals converging to a real $x$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Limits and Cauchy sequences of reals).

[L1]

Convergence: for every rational $\varepsilon > 0$ there is $K \in \mathbb{N}$ with $|x_k - x| < \varepsilon$ for all $k \ge K$ (Limits and Cauchy sequences of reals); and $1$ is a rational $> 0$ , since $\mathbb{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| \le |a| + |b|$ in $\mathbb{R}$ (The triangle inequality, Complete ordered field (least-upper-bound property)).

[L3]

Absolute value: $|u| \ge 0$ for every real $u$ (Basic properties of the absolute value).

[L4]

Finite maxima: for every $n \in \mathbb{N}$ and all reals $a_0, \dots, a_n$ the set $\{a_0, \dots, a_n\}$ 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 $\mathbb{R}$ : transitivity of $\le$ and of $<$ ; both mixed forms, $u < v \le w \Rightarrow u < w$ and $u \le v < w \Rightarrow u < w$ , and the implication $u < v \Rightarrow u \le v$ , all immediate from the reading of $u \le v$ as " $u < v$ or $u = v$ " (Complete ordered field (least-upper-bound property), Ordered field); and translation invariance, $a < b \Rightarrow a + c < b + c$ (Order is preserved by adding a constant and by adding inequalities).

[L6]

The order on $\mathbb{N}$ is total, so every index $k$ satisfies $k < K$ or $k \ge K$ ( $\le$ is a linear order on $\mathbb{N}$ ).

Proof

technique · direct

1.1

Apply convergence with the rational $\varepsilon = 1$ : fix $K \in \mathbb{N}$ such that $|x_k - x| < 1$ for all $k \ge K$ .

2.1

For every $k \ge K$ we have $|x_k| = |(x_k - x) + x| \le |x_k - x| + |x|$ , while adding $|x|$ to both sides of $|x_k - x| < 1$ gives $|x_k - x| + |x| < 1 + |x| = |x| + 1$ ; composing the non-strict inequality with the strict one yields $|x_k| < |x| + 1$ .

step 1.1L2L5

2.2

Define $M := \max\{\, |x_0|, |x_1|, \dots, |x_{K-1}|, |x| + 1 \,\}$ , the maximum of the finite list obtained by appending $|x| + 1$ to the first $K$ values $|x_0|, \dots, |x_{K-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 $|x_k|$ is one of the entries of that list, hence $|x_k| \le M$ .

step 2.2L4

3.2

For every $k \ge K$ we have $|x_k| < |x| + 1 \le M$ , since $|x| + 1$ is an entry of the list, hence $|x_k| \le M$ .

step 2.1step 2.2L4L5

4.1

Every index satisfies $k < K$ or $k \ge K$ , and in both cases $|x_k| \le M$ ; therefore $(x_k)$ is bounded.

step 3.1step 3.2L3L6∎

Remarks

This is where Every nonempty finite set of reals has a maximum and a minimum does its main work on this page: the first $K$ terms are bounded because a nonempty finite set of reals has a maximum, and that fact is proved once, by induction, rather than re-derived here. It is not the only consumer, and no claim of uniqueness is made: A null sequence times a bounded sequence is null and Conventions for sequences: indexing, eventually, $\lim$ , and rational $\varepsilon$ cite the same lemma, each for a maximum of finitely many reals.
The converse is false. A bounded sequence need not converge (FALSE: every bounded sequence converges). What is true in that direction is the Bolzano-Weierstrass theorem, which requires a passage to a subsequence; it is not available at this point in the reading order, being the subject of the next page of this track, Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness, where it is proved.
Boundedness is exactly what makes A null sequence times a bounded sequence is null applicable to a convergent factor, and that is how boundedness enters the product rule of Algebra of limits: sums, scalar multiples, products and quotients.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 63 results over 26 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. K. Hunter, An Introduction to Real Analysis, Ch. 3 (standard reference, not scraped)
Limit of a sequence (Wikipedia) (standard reference, not scraped)
T. Tao, Analysis I, 3rd ed., §6.1 (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 3 (standard reference, not scraped)