This is a complement to Srivatsan Narayanan's answer above on rational approximations to irrationals.
Peter Markstein, in his book IA-64 and Elementary Functions, Prentice-Hall, 2000, has this very nice Exclusion Theorem in Section 6.3, pages 91 and 92. This theorem was used in the design of the code for the elementary functions on Intel's IA-64 processor, which gives correctly rounded results. I reproduce Section 6.3 verbatim:
When seeking the root of a polynomial with integer coefficients, it is possible to determine the number of significant digits in an approximation which will guarantee correct rounding to a given precision, when the approximation is rational (floating point numbers are always rational). The exclusion theorem exemplifies the analysis carried out by Dirichlet [10] and Liouville in their early studies of transcendental numbers.
Theorem (the Exclusion Theorem.)
Let $\xi$ be a root of the polynomial $p_n(x) = \sum_{i=0}^n c_ix^i$, and let $a/b$ be an approximation sufficiently close to $\xi$, where $a$, $b$, and $c_i$ are integers. Then $|\xi-a/b| \ge M(\xi)/b^n$, where $M(\xi)$ is a constant which depends on $\xi$ and $p_n$.
Proof. First, observe that
$$
\left|p_n\left(\frac{a}{b}\right)\right| = \left|\sum_{i=0}^n\frac{c_ia^ib^{n-i}}{b^n}\right| \ge \frac{1}{b^n}
$$
when $a/b$ is not exactly $\xi$, because all quantities in the numerator of the summation are integers. Consider the interval $(\xi-1,\xi + 1)$. If $a/b \in (\xi-1,\xi + 1)$, and $a/b$ is closer to $\xi$ than any other root of $p_n$, then from the mean value theorem,
$$
p_n\left(\frac{a}{b}\right) - p_n(\xi) = \left(\frac{a}{b} - \xi\right)p_{n}'(w),\, w\in \left(\frac{a}{b},\xi\right)
$$
Since $p_n(\xi) = 0$,
$$
\left|\frac{a}{b} - \xi\right| \ge \left|\frac{1}{b^n p_{n}'(w)}\right|
$$
$p_{n}'(w)$ can be replaced by the maximum value it takes on in the interval $(\xi-1,\xi + 1)$, giving $|a/b - \xi| \ge M(\xi)/b^n$. $\blacksquare$
Using the exclusion theorem, an interval around $\xi$ can be determined within which no rational number having $b$ as its denominator can exist. If a computation is to be rounded to $p$ bits, then taking $b=2^{p+1}$ will establish an interval about $\xi$ in which no number halfway between two numbers of precision $p$ can lie. Computing an approximation to $\xi$ which lies in the excluded interval guarantees that rounding to $p$ precision is correct.
Real numbers which are the roots of polynomials with integer coefficients are called algebraic numbers; all other real numbers are transcendental. The algebraic numbers are distinguished by the exclusion theorem, which establishes for a given integer $b$, an interval within which no rational approximation with a denominator $b$ can exist. For transcendental numbers $\tau$, approximations generally can be found which are arbitrarily close to $\tau$. The lack of a similar exclusion theorem for approximations to transcendental numbers is the cause of difficulty in rounding transcendental functions correctly with modest effort.
[End of Section 6.3, verbatim]
See also Ng -- Argument Reduction for Huge Arguments