CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passverified 2026-08-06 (claude-sonnet-5)

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.

A monotone sequence converges if and only if it is bounded

Statement

Let $(x_k)$ be a monotone sequence of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences). Then $(x_k)$ converges if and only if it is bounded, that is if and only if there is $M \in \mathbb{R}$ with $|x_k| \le M$ for every $k \in \mathbb{N}$ .

The forward implication holds for every sequence and is Every convergent sequence is bounded. What monotonicity buys is the converse, which is false for sequences in general.

Facts & Assumptions

Given: A monotone sequence $(x_k)$ of reals, with range $S = \{x_k : k \in \mathbb{N}\}$ .

[L1]

Monotone means nondecreasing or nonincreasing (Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences).

[L2]

Monotone convergence: a nondecreasing sequence whose range is bounded above converges, to the supremum of its range; a nonincreasing sequence whose range is bounded below converges, to the infimum (A nondecreasing sequence bounded above converges to the supremum of its range, and a nonincreasing sequence bounded below to the infimum).

[L3]

Every convergent sequence of reals is bounded (Every convergent sequence is bounded).

[L4]

A sequence is bounded when some $M$ satisfies $|x_k| \le M$ for every $k$ ; its range is bounded above by $u$ when $x_k \le u$ for every $k$ , and bounded below by $\ell$ when $\ell \le x_k$ for every $k$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Lower bound, bounded below, bounded set).

[L5]

Absolute value: $|t| \le M$ exactly when $-M \le t \le M$ (Basic properties of the absolute value).

Proof

technique · direct

1.1

Suppose $(x_k)$ converges. Then it is bounded by [L3], and this direction uses neither the monotonicity hypothesis nor any case distinction.

givenL3

1.2

Suppose instead that $(x_k)$ is bounded, and fix $M$ with $|x_k| \le M$ for every $k$ ; then $-M \le x_k \le M$ for every $k$ , so the range $S$ is bounded above by $M$ and bounded below by $-M$ .

givenL4L5assume-hyp

2.1

If $(x_k)$ is nondecreasing then its range is bounded above by step 1.2, so $(x_k)$ converges, to $\sup S$ .

step 1.2L2assume-case nondec

2.2

If $(x_k)$ is nonincreasing then its range is bounded below by step 1.2, so $(x_k)$ converges, to $\inf S$ .

step 1.2L2assume-case noninc

3.1

A monotone sequence is nondecreasing or nonincreasing, so those two cases exhaust the hypothesis, and in both a bounded monotone sequence converges.

step 2.1step 2.2L1cases: nondecreasing or nonincreasingcases-exhaustive

4.1

Both directions are established: a monotone sequence converges if and only if it is bounded.

step 1.1step 3.1∎

Remarks

The limit is named, not merely asserted to exist. In the nondecreasing case it is $\sup S$ and in the nonincreasing case $\inf S$ , by A nondecreasing sequence bounded above converges to the supremum of its range, and a nonincreasing sequence bounded below to the infimum. The equivalence is stated without the value only because the value depends on which of the two cases holds.
This is the form in which the result is used. Bolzano-Weierstrass (Bolzano-Weierstrass: every bounded real sequence has a convergent subsequence) extracts a monotone subsequence of a bounded sequence and then needs exactly this corollary, since what is available about the subsequence is boundedness, inherited from the sequence, and not a bound on a particular side.
Monotonicity cannot be dropped. Without it the converse direction fails, by FALSE: every bounded sequence converges. The forward direction is not in the same position: it holds for every sequence, monotone or not, so there is no hypothesis to drop from it. What monotonicity adds there is sharpness rather than validity, and the sharpened form is recorded by A nondecreasing sequence that is not bounded above diverges to $+\infty$ : an unbounded nondecreasing sequence does not merely fail to converge, it diverges to $+\infty$ .

Depends on

Used by

Dependency tree · next 3 levels

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

Monotone convergence theorem (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 3 (Thm 3.14) (standard reference, not scraped)
T. Tao, Analysis I, 3rd ed., §6.3 (standard reference, not scraped)
J. Lebl, Basic Analysis I, Sequences and limits (Theorem 2.1.10) (standard reference, not scraped)