Lemma 5.7.5 — Rational approximation with a bounded denominator

Read-back model: unavailable (the exact runtime model identifier is not exposed).

For every real number $x$ and every natural number $n$ satisfying $0<n$, there exists a rational number $q$ such that, writing $d=q.\mathrm{den}$, one has $0<d$, $d\le n$, and $|x-q|\le 1/(d(n+1))$. The denominator $q.\mathrm{den}$ is a natural number: it is the positive denominator in the canonical reduced expression $q=a/d$, where $a\in\mathbb Z$, $d\in\mathbb N$, $d\ne0$, and the natural-number gcd of $|a|$ and $d$ is $1$; in particular the denominator of every integer rational, including $0$, is $1$. The bounds on $d$ are natural-number inequalities, whereas $q$, $d$, and $n$ are interpreted as real numbers in the absolute-value inequality, whose division and addition are real operations. Positivity of $d$ is explicitly included in the conclusion and also holds for every rational number by its representation; together with $n>0$ it makes the real denominator $d(n+1)$ positive. The number $x$ may be any real number, rational or irrational and of any sign, and the existentially quantified $q$ has no imposed sign or numerator bound. The case $n=0$ is excluded; $n=1$ is included and requires $d=1$ and $|x-q|\le1/2$. The error bound is non-strict, and neither uniqueness nor infinitely many choices of $q$ is asserted. There are no further assumptions.