ThmDex – An index of mathematical definitions, results, and conjectures.
Oriented complex curve integral of continuous function with a primitive on open set
Formulation 0
Let $U \subseteq \mathbb{C}$ be a D5008: Standard open complex set such that
(i) $f : U \to \mathbb{C}$ is a D5635: Standard-continuous complex function on $U$
(ii) $F : U \to \mathbb{C}$ is a D5005: Complex function primitive for $f$ on $U$
(iii) $\gamma \subseteq U$ is an D5023: Oriented complex curve
(iv) $\gamma$ is a D5646: Closed complex curve
Then \begin{equation} \int_{\gamma} f(z) \, d z = 0 \end{equation}
Proofs
Proof 0
Let $U \subseteq \mathbb{C}$ be a D5008: Standard open complex set such that
(i) $f : U \to \mathbb{C}$ is a D5635: Standard-continuous complex function on $U$
(ii) $F : U \to \mathbb{C}$ is a D5005: Complex function primitive for $f$ on $U$
(iii) $\gamma \subseteq U$ is an D5023: Oriented complex curve
(iv) $\gamma$ is a D5646: Closed complex curve
Applying R1558: Second fundamental theorem of complex integral calculus yields immediately \begin{equation} \int_{\gamma} f(z) \, d z = F(z_0) - F(z_0) = 0 \end{equation} $\square$