  We report on a verification of the Fundamental Theorem of Algebra in ACL2(r).
The proof consists of four parts. First, continuity for both complex-valued and
real-valued functions of complex numbers is defined, and it is shown that
continuous functions from the complex to the real numbers achieve a minimum
value over a closed square region. An important case of continuous real-valued,
complex functions results from taking the traditional complex norm of a
continuous complex function. We think of these continuous functions as having
only one (complex) argument, but in ACL2(r) they appear as functions of two
arguments. The extra argument is a "context", which is uninterpreted. For
example, it could be other arguments that are held fixed, as in an exponential
function which has a base and an exponent, either of which could be held fixed.
Second, it is shown that complex polynomials are continuous, so the norm of a
complex polynomial is a continuous real-valued function and it achieves its
minimum over an arbitrary square region centered at the origin. This part of
the proof benefits from the introduction of the "context" argument, and it
illustrates an innovation that simplifies the proofs of classical properties
with unbound parameters. Third, we derive lower and upper bounds on the norm of
non-constant polynomials for inputs that are sufficiently far away from the
origin. This means that a sufficiently large square can be found to guarantee
that it contains the global minimum of the norm of the polynomial. Fourth, it
is shown that if a given number is not a root of a non-constant polynomial,
then it cannot be the global minimum. Finally, these results are combined to
show that the global minimum must be a root of the polynomial. This result is
part of a larger effort in the formalization of complex polynomials in ACL2(r).
