Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16
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.

Inside its disc of convergence a complex power series is holomorphic and may be differentiated term by term

Statement

Let f(z)=∑n≥0cn(z−a)n have radius R. If ∣z−a∣<R, then f is complex differentiable at z and f′(z)=∑n≥1ncn(z−a)n−1. Consequently f is holomorphic on its open disc of convergence (Complex differentiability at a point, the complex derivative, holomorphic functions, and entire functions).

Facts & Assumptions

Given: A complex power series of radius R and a point z with ∣z−a∣<R.

Proof

technique · direct
1.1choosealgebra

Choose r with ∣z−a∣<r<R. For w near z, the finite identity wn−zn=(w−z)∑k<nwn−1−kzk follows by expanding and telescoping, so the difference quotient of each monomial tends to nzn−1.

2.1step 1.1L1

On ∣w−a∣,∣z−a∣≤r, the quotient in step 1.1 is bounded in modulus by nrn−1 after translating the centre to a. The series ∑n∣cn∣rn−1 converges by [L1], so its tails are uniformly small.

3.1step 1.1step 2.1

Split the difference quotient of f into a finite head and a tail. The finite head tends termwise to its derivative by step 1.1, while step 2.1 bounds the tail uniformly; hence the quotient tends to ∑n≥1ncn(z−a)n−1.

4.1step 3.1∎

Since z was arbitrary in the open disc, the derivative exists at every such point, which is holomorphy by Complex differentiability at a point, the complex derivative, holomorphic functions, and entire functions. If R=0 the disc is empty and the assertion is vacuous; the constant term differentiates to 0.

Depends on

Used by

Dependency tree · two levels

11 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