Fix a point z in the annulus and treat z as a constant. Multiplying the series by z, term by term, scales the sum by z. This holds for all z in the annulus. Therefore, we can increment the exponents, and the new series converges to zf. Similarly, decrementing the exponents yields f/z.
Multiply by an appropriate power of z, so that the laurent series becomes a power series. The series is still equal to 0 over the annulus.
If the first nonzero term in the series has exponent n, divide through by zn, giving a series with a nonzero constant term, that is still equal to 0 on the annulus.
This power series converges inside the annulus, so apply the previous theorem, and f converges inside the disk. In other words, we have found its "circle of convergence". Furthermore, f is analytic throughout the circle.
Draw a contour around the origin, running through the annulus. Since f is 0 on the annulus, the integral of f(y)/y, around this contour, is 0. Apply an earlier theorem, and f(0) = 0. But remember, f has a nonzero constant, so we have reached a contradiction.
The representation of an analytic function, as a laurent series, is unique. This does not prove the laurent series exists; only that it is unique. However, if f is analytic on a disk, rather than an annulus, then the power series does exist, and is unique, and any attempt to compute the laurent series will produce the power series, as we discussed earlier.
A function that is analytic at 0 has a well defined list of derivatives, and a unique representation as a powerseries, which converges in a neighborhood about 0. This does not mean every power series leads to an analytic function. It has to converge on some nonzero z, or we're out of luck. Set an = n factorial, and the sum of anzn does not converge, no matter how small z is. The terms don't approach 0.
Suppose f is a function that is represented by a laurent series, yet the laurent operator produces infinitely many terms with negative exponents. Multiply f by a power of z, so that its laurent series is actually a power series. When the laurent coefficients are computed, the resulting series is a shifted version of the original. In other words, it still has infinitely many terms with negative exponents. Since f is represented by a power series, it is analytic at 0. Such a function produces its power series; there are no terms with negative exponents. This is a contradiction.
If f is analytic on an annulus about 0, and f is the sum of a laurent series, that laurent series is unique, and can be derived via contour integrals on the inner and outer circles. If f = 5/z3+3/z+z2, the laurent series for f has to be 5/z3+3/z+z2.