ThmDex – An index of mathematical definitions, results, and conjectures.
Cauchy's theorem for a disc
Formulation 0
Let $D \subseteq \mathbb{C}$ be an D4995: Open complex disc such that
(i) $f : D \to \mathbb{C}$ is a D1392: Holomorphic function on $D$
(ii) $\gamma \subseteq C$ is an D5023: Oriented complex curve
(iii) $\gamma$ is a D5646: Closed complex curve
Then \begin{equation} \int_{\gamma} f(z) \, d z = 0 \end{equation}
Proofs
Proof 0
Let $D \subseteq \mathbb{C}$ be an D4995: Open complex disc such that
(i) $f : D \to \mathbb{C}$ is a D1392: Holomorphic function on $D$
(ii) $\gamma \subseteq C$ is an D5023: Oriented complex curve
(iii) $\gamma$ is a D5646: Closed complex curve
Result R3456: Holomorphic function on open disc has primitive on that disc shows that $f$ has a primitive $F : D \to \mathbb{C}$ on $D$. The claim is now a consequence of results
(i) R1522: Holomorphic function is continuous
(ii) R1564: Oriented complex curve integral of continuous function with a primitive on open set

$\square$