LemmaStatement: AI-adaptedProof: AI-generatedSession-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.

A nondecreasing sequence that is not bounded above diverges to $+\infty$

Statement

Let $(x_k)$ be a nondecreasing sequence of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences, Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences) whose range $S = \{x_k : k \in \mathbb{N}\}$ is not bounded above (Lower bound, bounded below, bounded set). Then $(x_k)$ diverges to $+\infty$ (Divergence to $+\infty$ and to $-\infty$ ): for every $M \in \mathbb{R}$ there is $K \in \mathbb{N}$ with $x_k > M$ for all $k \ge K$ .

Read together with the monotone convergence theorem this says that a nondecreasing sequence has exactly two possible behaviours, with nothing in between: it converges to the supremum of its range, or it runs away to $+\infty$ .

Facts & Assumptions

Given: A nondecreasing sequence $(x_k)$ of reals whose range $S = \{x_k : k \in \mathbb{N}\}$ is not bounded above.

[L1]

Monotonicity: $x_j \le x_k$ whenever $j \le k$ (Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences).

[L2]

Bounded above: $S$ is bounded above exactly when some $M \in \mathbb{R}$ satisfies $s \le M$ for every $s \in S$ (Lower bound, bounded below, bounded set).

[L3]

Trichotomy: for reals $s$ and $M$ , exactly one of $s < M$ , $s = M$ , $s > M$ holds, so the failure of $s \le M$ is $s > M$ (Complete ordered field (least-upper-bound property), Ordered field).

[L4]

Divergence to $+\infty$ : $x_k \to +\infty$ when for every $M \in \mathbb{R}$ there is $K \in \mathbb{N}$ such that $x_k > M$ for all $k \ge K$ (Divergence to $+\infty$ and to $-\infty$ ).

[L5]

Every element of $S$ is a term of the sequence, and conversely (Sequences of reals: bounded, eventually, frequently, tails, subsequences).

Proof

technique · direct

1.1

Let $M \in \mathbb{R}$ be arbitrary. Since $S$ is not bounded above, $M$ is not an upper bound of $S$ , so some $s \in S$ fails $s \le M$ .

givenL2

2.1

By trichotomy that $s$ satisfies $s > M$ , and being an element of $S$ it is a term: fix $K \in \mathbb{N}$ with $s = x_K$ , so $x_K > M$ .

step 1.1L3L5choose

3.1

For every $k \ge K$ monotonicity gives $x_K \le x_k$ , hence $x_k \ge x_K > M$ and so $x_k > M$ .

step 2.1L1

4.1

For every real $M$ an index $K$ has been produced with $x_k > M$ for all $k \ge K$ , which is exactly divergence to $+\infty$ .

step 3.1L4∎

Remarks

Only "not bounded above" is used, not unboundedness of the sequence. For a nondecreasing sequence the two coincide, since such a sequence is bounded below by $x_0$ (Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences), so a nondecreasing sequence is unbounded exactly when its range is not bounded above. The hypothesis is stated in the one-sided form because that is the form the proof consumes.
The dual statement holds with the same proof: a nonincreasing sequence whose range is not bounded below diverges to $-\infty$ . Reflecting through the origin turns one into the other.
$+\infty$ is not a limit. Divergence to $+\infty$ and to $-\infty$ is deliberately not a case of Limits and Cauchy sequences of reals: a sequence diverging to $+\infty$ is unbounded, hence not convergent (Every convergent sequence is bounded), and the arrow in $x_k \to +\infty$ is an abbreviation for the displayed quantifier statement and never an equation.
The companion statement is A nondecreasing sequence bounded above converges to the supremum of its range, and a nonincreasing sequence bounded below to the infimum: between them, a nondecreasing sequence converges to the supremum of its range or diverges to $+\infty$ , with no third possibility.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 50 results over 11 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 and Def. 3.15) (standard reference, not scraped)
J. Lebl, Basic Analysis I, §2.2 (standard reference, not scraped)

A nondecreasing sequence that is not bounded above diverges to +∞+\infty+∞