In mathematics, the Weierstrass Nullstellensatz is a version of the intermediate value theorem over a real closed field. It says:
Since F is real-closed, F(i) is algebraically closed, hence f(x) can be written as , where is the leading coefficient and are the roots of f. Since each nonreal root can be paired with its conjugate (which is also a root of f), we see that f can be factored in F[x] as a product of linear polynomials and polynomials of the form , .
If f changes sign between a and b, one of these factors must change sign. But is strictly positive for all x in any formally real field, hence one of the linear factors , , must change sign between a and b; i.e., the root of f satisfies .