Here's the specific result - it's a standard result in elementary number theory. Suppose x is irrational and p/q is a rational in lowest terms with q > 0, and

Here's the specific result - it's a standard result in elementary number theory. Suppose x is irrational and p/q is a rational in lowest terms with q > 0, and |x - p/q| < 1/(2 q^2). Then p/q is a convergent in the continued fraction expansion for x. Using this, you can show that 355/113 is the best rational approximation to pi with denominator less than 1000. (Assume that there's a better approximation, and use the result to get a contradiction.) I wrote this up in my number theory notes (https://sites.millersville.edu/bikenaga/number-theory/approximation-by-rationals/approximation-by-rationals.html https://sites.millersville.edu/bikenaga/number-theory/approx... and https://sites.millersville.edu/bikenaga/number-theory/approximation-by-rationals/approximation-by-rationals.pdf https://sites.millersville.edu/bikenaga/number-theory/approx... [pdf]).