Theorem: Zero Staircase Integral Condition for Primitive

Let $f: D \to \C$ be a continuous complex function, where $D$ is an open and connected domain.
Let $z_0 \in D$.
Suppose that $\ds \oint_C \map f z \rd z = 0$ for all closed staircase contours $C$ in $D$.
Then $f$ has a primitive $F: D \to \C$ defined by:
:$\ds \map F w = \int_{C_w} \map f z \rd z$
where $C_w$ is any staircase contour in $D$ with start point $z_0$ and end point $w$.

Proof:
From Connected Domain is Connected by Staircase Contours, it follows that there exists a staircase contour $C_w$ in $D$ with start point $z_0$ and end point $w$.
If $C_w'$ is another staircase contour with the same endpoints as $C_w$, then $C_w' \cup \paren {-C_w}$ is a closed staircase contour where $-C_w$ is the reversed contour of $C_w$ and $\cup$ is concatenation of contours.
Then the definition of $F$ is independent of the choice of contour, as:
{{begin-eqn}}
{{eqn | l = \int_{C_w} \map f z \rd z
      | r = \int_{C_w} \map f z \rd z + \oint_{C_w' \cup \paren {-C_w} } \map f z \rd z
      | c = {{hypothesis}}
}}
{{eqn | r = \int_{C_w} \map f z \rd z + \int_{C_w'} \map f z \rd z + \int_{-C_w} \map f z \rd z
      | c = Contour Integral of Concatenation of Contours
}}
{{eqn | r = \int_{C_w} \map f z \rd z + \int_{C_w'} \map f z \rd z - \int_{C_w} \map f z \rd z
      | c = Contour Integral along Reversed Contour
}}
{{eqn | r = \int_{C_w'} \map f z \rd z
}}
{{end-eqn}}
We now show that $F$ is the primitive of $f$.
Let $\epsilon \in \R_{>0}$.
By definition of continuity, there exists $r \in \R_{>0}$ such that the open ball $\map {B_r} w \subseteq D$, and for all $z \in \map {B_r} w$:
:$\cmod {\map f z - \map f w} < \dfrac \epsilon 2$
Let $h = x + i y \in \C \setminus \set 0$ with $x, y \in \R$ such that $\cmod h < r$.
Let $\LL$ be the staircase contour that goes in a horizontal line from $w$ to $w + x$, and continues in a vertical line from $w + x$ to $w + h$.
As $w + x, w + h \in \map {B_r} w$, it follows from Open Ball is Convex Set that $\LL$ is a contour in $\map {B_r} w$.
Then $C_w \cup \LL$ is a staircase contour from $z_0$ to $w + h$, so:
{{begin-eqn}}
{{eqn | l = \map F {w + h} - \map F w
      | r = \int_{C_w \cup \LL} \map f z \rd z - \int_{C_w} \map f z \rd z
}}
{{eqn | r = \int_\LL \map f z \rd z
      | c = Contour Integral of Concatenation of Contours
}}
{{end-eqn}}
From Derivative of Complex Polynomial, it follows that $\dfrac \d {\d z} \map f w z = \map f w$, so:
{{begin-eqn}}
{{eqn | l = \int_\LL \map f w \rd z
      | r = \map f w \paren {w + h} - \map f w w
      | c = Fundamental Theorem of Calculus for Contour Integrals
}}
{{eqn | r = h \map f w
}}
{{end-eqn}}
We can now show that $\map {F'} w = \map f w$, as:
{{begin-eqn}}
{{eqn | l = \cmod {\dfrac {\map F {w + h} - \map F w} h - \map f w}
      | r = \cmod {\dfrac 1 h \int_\LL \map f z \rd z - \dfrac 1 h h \map f w}
      | c = {{apriori}}
}}
{{eqn | r = \cmod {\dfrac 1 h} \cmod {\int_\LL \paren {\map f z - \map f w} \rd z}
      | c = Linear Combination of Contour Integrals
}}
{{eqn | o = < 
      | r = \cmod {\dfrac 1 h} \dfrac \epsilon 2 \map L \LL
      | c = Estimation Lemma for Contour Integrals, as $z \in \map {B_r} w$
}}
{{eqn | r = \dfrac {\size x + \size y} {\cmod h} \dfrac \epsilon 2 
      | c = the lengths of the line segments are $\size x$ and $\size y$
}}
{{eqn | o = \le
      | r = \epsilon
      | c = Modulus Larger than Real Part and Imaginary Part
}}
{{end-eqn}}
When $h$ tends to $0$, we have $\map {F'} w = \map f w$ by definition of differentiability.
{{qed}}