[proofplan] We translate exact pole order into the holomorphic extendability of $(z-a)^m f$ across $a$ with nonzero value at $a$. In one direction, the Taylor expansion of this extension gives a Laurent expansion for $f$ whose first principal coefficient is nonzero. In the other direction, multiplying the assumed [Laurent series](/page/Laurent%20Series) by $(z-a)^m$ gives a holomorphic [power series](/page/Power%20Series) extension of $(z-a)^m f$ with nonzero value at $a$. The equivalent coefficient statement follows from uniqueness of Laurent expansions on a punctured disk. [/proofplan] [step:Expand the holomorphic multiple of $f$ when the pole has exact order $m$] Assume that $a$ is a pole of exact order $m$ of $f$. By the definition of exact pole order, there exist $\rho > 0$ and a [holomorphic function](/page/Holomorphic%20Function) \begin{align*} G: B(a,\rho) \to \mathbb{C} \end{align*} such that $B(a,\rho) \subset U$, \begin{align*} G(z) = (z-a)^m f(z) \end{align*} for every $z \in B(a,\rho) \setminus \{a\}$, and $G(a) \neq 0$. Since $G$ is holomorphic on the disk $B(a,\rho)$, the Taylor expansion theorem for holomorphic functions gives coefficients $(b_j)_{j \geq 0}$ in $\mathbb{C}$ such that \begin{align*} G(z) = \sum_{j=0}^{\infty} b_j (z-a)^j \end{align*} for every $z \in B(a,\rho)$, with $b_0 = G(a)$. Define coefficients $(c_k)_{k \geq -m}$ by \begin{align*} c_k := b_{k+m}. \end{align*} Then $c_{-m} = b_0 = G(a) \neq 0$. For every $z \in B(a,\rho) \setminus \{a\}$, division by $(z-a)^m$ gives \begin{align*} f(z) = \sum_{j=0}^{\infty} b_j (z-a)^{j-m} = \sum_{k=-m}^{\infty} c_k (z-a)^k. \end{align*} Thus the required Laurent expansion exists with $r := \rho$. [guided] The exact-order hypothesis is designed to remove precisely the singular part of $f$. Since $a$ is a pole of exact order $m$, the product $(z-a)^m f(z)$ has a removable singularity at $a$, and its removable extension does not vanish at $a$. Thus there are $\rho > 0$ and a holomorphic map \begin{align*} G: B(a,\rho) \to \mathbb{C} \end{align*} such that $B(a,\rho) \subset U$, \begin{align*} G(z) = (z-a)^m f(z) \end{align*} for every $z \in B(a,\rho) \setminus \{a\}$, and $G(a) \neq 0$. Now the singularity has been transferred into the explicit factor $(z-a)^{-m}$. The function $G$ itself is holomorphic on the whole disk $B(a,\rho)$, so the Taylor expansion theorem applies at the center $a$. Therefore there are coefficients $(b_j)_{j \geq 0}$ in $\mathbb{C}$ with \begin{align*} G(z) = \sum_{j=0}^{\infty} b_j (z-a)^j \end{align*} for every $z \in B(a,\rho)$. The constant coefficient is $b_0 = G(a)$, hence $b_0 \neq 0$. For $z \neq a$, we may divide the Taylor series by $(z-a)^m$. This gives \begin{align*} f(z) = (z-a)^{-m}G(z) = \sum_{j=0}^{\infty} b_j (z-a)^{j-m}. \end{align*} Reindex the series by setting $k := j-m$, so that $j = k+m$ and $k$ ranges over all integers with $k \geq -m$. Define \begin{align*} c_k := b_{k+m}. \end{align*} Then \begin{align*} f(z) = \sum_{k=-m}^{\infty} c_k (z-a)^k \end{align*} for every $z \in B(a,\rho) \setminus \{a\}$, and the first coefficient in the principal part is \begin{align*} c_{-m} = b_0 = G(a) \neq 0. \end{align*} This is exactly the desired Laurent expansion, with $r := \rho$. [/guided] [/step] [step:Recover a pole of exact order $m$ from the Laurent expansion] Conversely, assume there are $r > 0$ and coefficients $(c_k)_{k \geq -m}$ in $\mathbb{C}$ such that $B(a,r) \subset U$, $f(z) = \sum_{k=-m}^{\infty} c_k (z-a)^k$ for every $z \in B(a,r) \setminus \{a\}$, and $c_{-m} \neq 0$. Define $H: B(a,r) \to \mathbb{C}$ by $H(z) := \sum_{j=0}^{\infty} c_{j-m}(z-a)^j$. This is a power series in $z-a$, so it defines a holomorphic function on $B(a,r)$. For $z \in B(a,r) \setminus \{a\}$, multiplying the Laurent series by $(z-a)^m$ gives $H(z) = (z-a)^m f(z)$. Moreover, $H(a) = c_{-m} \neq 0$. Therefore $(z-a)^m f(z)$ extends holomorphically across $a$ with nonzero value at $a$. By the definition of pole of exact order, $a$ is a pole of exact order $m$ of $f$. [/step] [step:Use uniqueness of Laurent coefficients to obtain the equivalent formulation] On any punctured disk $B(a,r) \setminus \{a\}$ where a Laurent expansion of $f$ converges to $f$, the uniqueness theorem for Laurent coefficients says that the coefficients of the powers $(z-a)^k$ are uniquely determined by $f$ and the punctured disk. Hence the existence of an expansion beginning at $k=-m$ with $c_{-m} \neq 0$ is equivalent to saying that, in the Laurent expansion of $f$ about $a$, all coefficients with $k < -m$ vanish and the coefficient with $k=-m$ is nonzero. Combining the two directions proves the theorem. [/step]