In mathematics, the Weierstrass Nullstellensatz is a version of the intermediate value theorem over a real closed field. It says:
Given a polynomial formula_1 in one variable with coefficients in a real closed field "F" and formula_2 in formula_3, if formula_4, then there exists a formula_5 in formula_3 such that formula_7 and formula_8.
Proof.
Since "F" is real-closed, "F"("i") is algebraically closed, hence "f"("x") can be written as formula_9, where formula_10 is the leading coefficient and formula_11 are the roots of "f". Since each nonreal root formula_12 can be paired with its conjugate formula_13 (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 formula_14, formula_15.
If "f" changes sign between "a" and "b", one of these factors must change sign. But formula_16 is strictly positive for all "x" in any formally real field, hence one of the linear factors formula_17, formula_18, must change sign between "a" and "b"; i.e., the root formula_19 of "f" satisfies <math>a<\alpha_j.