TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

On a positively oriented circle about a, the integral of (z-a)^m is zero for every integer m except -1, and is 2 pi i for m=-1

Statement

Let $a \in C$ , $r > 0$ , and $γ (t) = a + r \exp (i t)$ for $0 \leq t \leq 2 π$ . For every integer $m$ , $\int_{γ} (z - a)^{m} d z = {\begin{cases} 2 π i, & m = - 1, \\ 0, & m \neq - 1. \end{cases}$

Facts & Assumptions

Given: The positively oriented circle $γ$ and an integer $m$ .

[L1]

On a piecewise- $C^{1}$ contour, the Riemann–Stieltjes integral agrees with $\int f (γ (t)) γ^{'} (t) d t$ (For piecewise-C1 contours the Riemann–Stieltjes integral agrees with the parametric complex integral and the published real line integrals).

[L2]

Negative integer powers are defined exactly for nonzero complex bases (Integer powers in the complex field).

[L3]

The complex exponential is entire with derivative itself and satisfies $\exp (z + w) = \exp z \exp w$ (The complex exponential is entire and its complex derivative is itself, $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential).

[L4]

For real $x, y$ , $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ and $∣ \exp (x + i y) ∣ = e^{x}$ ; in particular $e^{i π} + 1 = 0$ ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ ).

[L5]

If a real function $G$ is differentiable on $[a, b]$ and $G^{'}$ is integrable, then $\int_{a}^{b} G^{'} = G (b) - G (a)$ (The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ ).

[L6]

Derivatives and integrals of $R^{2}$ -valued functions are defined componentwise (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral).

Proof

technique · cases

1.1

Since $r > 0$ , $γ (t) - a \neq 0$ , so all integer powers in [L2] are defined. By [L1] and [L3], the integrand becomes $i r^{m + 1} \exp (i (m + 1) t)$ .

L1L2L3algebra

2.1

If $m = - 1$ , the expression in step 1.1 is the constant $i$ , whose integral from $0$ to $2 π$ is $2 π i$ .

assume-case exceptionalstep 1.1algebra

2.2

If $m \neq - 1$ , an antiderivative is $r^{m + 1} \exp (i (m + 1) t) / (m + 1)$ by [L3]. Apply the real theorem [L5] to its two components using [L6]; the complex integral is the endpoint difference $r^{m + 1} (\exp (2 π i (m + 1)) - 1) / (m + 1)$ . Write $k : = m + 1$ , a nonzero integer. For $k > 0$ the addition law in [L3] gives $\exp (2 π i k) = \exp (i π)^{2 k}$ , and $\exp (i π) = - 1$ by [L4], so $\exp (2 π i k) = (- 1)^{2 k} = 1$ ; for $k < 0$ the addition law gives $\exp (2 π i k) \exp (- 2 π i k) = \exp (0) = 1$ with $\exp (- 2 π i k) = 1$ by the previous case, so again $\exp (2 π i k) = 1$ . The endpoint difference is therefore $0$ .

assume-case regularstep 1.1L3L4L5L6algebra

3.1

The integer cases $m = - 1$ and $m \neq - 1$ are exhaustive, proving the formula.

step 2.1step 2.2cases-exhaustive∎

Depends on

Used by

Dependency tree · next 3 levels

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

A. Weber, Lecture Notes in Complex Analysis, Example 1.7.1 (standard reference, not scraped)