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

∑(bk−bk+1) converges iff (bk) converges, with sum b0−lim⁡bk

Statement

Let (bk) be a sequence of reals and put ak:=bk−bk+1. Then the partial sums of ∑ak are

sn  =  ∑k<n(bk−bk+1)  =  b0−bn(n∈N),

and consequently ∑ak converges (Series, partial sums, convergence and the sum, divergence, and the tail series) if and only if (bk) converges (Limits and Cauchy sequences of reals), in which case

∑k=0∞(bk−bk+1)  =  b0−lim⁡kbk.

For a family from a general starting index m the same statement holds with b0 replaced by bm, being this statement applied to the shifted sequence j↦bj+m (Series, partial sums, convergence and the sum, divergence, and the tail series).

Facts & Assumptions

Given: A sequence (bk) of reals, the sequence ak:=bk−bk+1, and the partial sums sn=∑k<nak (Series, partial sums, convergence and the sum, divergence, and the tail series, Finite sums and finite products, by recursion).

[L1]

Telescoping of finite sums: ∑k<n(ck+1−ck)=cn−c0 for every sequence (ck) of reals and every n∈N (Laws of finite sums and finite products).

[L2]

Algebra of limits: if xn→x and yn→y then xn−yn→x−y (Algebra of limits: sums, scalar multiples, products and quotients).

[L3]

A constant sequence with value c converges to c (Limits and Cauchy sequences of reals).

Proof

technique · direct
1.1

Apply [L1] to the sequence ck:=−bk: it gives ∑k<n(−bk+1−(−bk))=−bn−(−b0), that is ∑k<n(bk−bk+1)=b0−bn.

L1algebra
2.1

So sn=b0−bn for every n∈N, and equivalently bn=b0−sn.

step 1.1algebra
3.1

Suppose (bk) converges, say bn→B; then sn=b0−bn→b0−B, so ∑ak converges with sum b0−B.

step 2.1L2L3
3.2

Suppose conversely that ∑ak converges, say sn→S; then bn=b0−sn→b0−S, so (bk) converges.

step 2.1L2L3
4.1

The two implications give the stated equivalence, and in the convergent case step 3.1 gives the sum b0−lim⁡kbk.

step 3.1step 3.2∎

Remarks

  • The first term of (bk) survives and the rest cancel. That is the whole content, and it is where an off-by-one error is easiest to make: the sum is b0−lim⁡bk and not b1−lim⁡bk, because the partial sum sn=∑k<n starts at k=0 (Series, partial sums, convergence and the sum, divergence, and the tail series). A series written from k=1 telescopes to b1−lim⁡bk instead.

  • No sign or monotonicity hypothesis is used. The lemma is an identity between finite sums followed by one limit rule, so it applies to sequences (bk) of any sign and is not restricted to the decreasing case in which telescoping series usually appear.

Depends on

Used by

Dependency tree · two levels

32 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