Irrationality of the square root of two (source code)

= Irrationality of the square root of two
{title2=$\sqrt2\notin\mathbb Q$}

If $\sqrt2=p/q$ in lowest terms, then $p^2=2q^2$ makes $p$ even. Substituting $p=2r$ then makes $q$ even, contradicting that the integers are coprime. More quantitatively, $|2q^2-p^2|\geq1$ for every nonzero integer $q$, and factoring the difference of squares gives $|\sqrt2-p/q|\geq1/(4q^2)$. To verify the constant, for $p/q\in[1,2]$ the other factor $\sqrt2+p/q$ is less than four; outside this interval the approximation error is at least $\sqrt2-1>1/4$.