Factorial cosine iterated limit detects rationality (source code)

= Factorial cosine iterated limit detects rationality
{title2=$\lim_{m\to\infty}\lim_{n\to\infty}\cos^{2n}(m!\pi x)=\mathbf1_{\mathbb Q}(x)$}

For fixed $m$, the inner <limit> is one precisely when $m!x$ is an <integer>, and zero otherwise, because $|\cos(\pi y)|=1$ exactly at integers and powers of a number with modulus below one tend to zero. If $x=p/q$ is a <rational number>, $q$ divides $m!$ for every $m\geq q$, making the inner limit eventually one. If $x$ is an <irrational number>, multiplication by a nonzero integer cannot make it integral, making every inner limit zero. The order of the two limits is essential to this argument.