Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27
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 series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum

Statement

Let (ak) be a sequence of reals with ak≥0 for every k∈N, let sn=∑k<nak be its partial sums and let S={ sn:n∈N } be the range of (sn) (Series, partial sums, convergence and the sum, divergence, and the tail series). Then:

  1. (sn) is nondecreasing (Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences) and sn≥0 for every n;
  2. ∑ak converges if and only if S is bounded above (Lower bound, bounded below, bounded set), and in that case ∑k=0∞ak  =  sup⁡S, so in particular sn≤∑k=0∞ak for every n;
  3. if S is not bounded above then sn→+∞ (Divergence to +∞ and to −∞) and ∑ak diverges.

This is the theorem that makes the nonnegative theory work: for terms of one sign, convergence is a boundedness question and no candidate limit is ever needed. Every comparison test on this page is an application of it.

Facts & Assumptions

Given: A sequence (ak) of reals with ak≥0 for every k, its partial sums sn=∑k<nak, and the range S={sn:n∈N} (Series, partial sums, convergence and the sum, divergence, and the tail series, Finite sums and finite products, by recursion, Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L1]

The recursion clause of the finite sum: sn+1=sn+an (Finite sums and finite products, by recursion).

[L2]

Consecutive comparisons suffice for monotonicity: (xk) is nondecreasing if and only if xk≤xk+1 for every k; and a nondecreasing sequence is bounded below by its first term (Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences).

[L3]

Monotonicity of finite sums: if ak≥0 for all k<n then ∑k<nak≥0 (Laws of finite sums and finite products).

[L4]

A monotone sequence converges if and only if it is bounded, that is if and only if there is M with ∣xk∣≤M for every k (A monotone sequence converges if and only if it is bounded, Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L6]

A nondecreasing sequence whose range is not bounded above diverges to +∞ (A nondecreasing sequence that is not bounded above diverges to +∞, Divergence to +∞ and to −∞).

Proof

technique · direct
1.1givenL1L2

For every n, sn+1−sn=an≥0, so sn≤sn+1 and (sn) is nondecreasing.

1.2givenL3

For every n, sn=∑k<nak≥0, all terms being nonnegative.

2.1step 1.1step 1.2

Claim 1 is steps 1.1 and 1.2 together.

2.2step 1.2L4

Since sn≥0 we have ∣sn∣=sn, so (sn) is bounded in the sense of [L4] if and only if S is bounded above.

3.1step 1.1step 2.2L4

By [L4] applied to the monotone sequence (sn), the series converges if and only if (sn) is bounded, hence if and only if S is bounded above.

4.1step 1.1step 3.1L5

If S is bounded above then (sn) converges to sup⁡S, so ∑ak converges with sum sup⁡S; and since sup⁡S is an upper bound of S, sn≤sup⁡S for every n.

4.2step 1.1step 3.1L6

If S is not bounded above then sn→+∞, and by step 3.1 the series diverges.

5.1step 3.1step 4.1step 4.2∎

The equivalence and the identification of the sum as the supremum together make claim 2, and the divergence statement is claim 3.

Remarks

Depends on

Dependency tree · 2 levels

Sources