Suppose to the contrary that $\sqrt{2}$ is rational. By definition, then there are integers $p, q \in \mathbb{Z}$ such that $\sqrt{2} = p / q$. Without loss of generality, we may assume that $q, p$ are coprime. Multiplying each side by $q$ and then squaring both sides, we obtain
\begin{equation}
2 q^2
= (\sqrt{2} q)^2
= p^2
\end{equation}
Since $q$ is a basic integer, result
R4198: Binary product of basic integers is a basic integer shows that so is $q^2$. Thus, by definition, $p^2$ is an
D5: Even integer. Result
R4199: Binary product of odd basic integers is odd shows that $p^2$ must be odd if $p$ is. Since $p^2$ is even, therefore $p$ must also be even. By definition, there is an integer $m \in \mathbb{Z}$ such that $p = 2 m$. Combining this with the previous equation, we have
\begin{equation}
2 q^2 = p^2 = (2 m)^2 = 4 m^2
\end{equation}
Dividing each side by $2$, this gives $q^2 = 2 m^2$. Since $m$ is an integer, then so is $m^2$. Hence, $q^2$ is even, which necessitates that also $q$ is even. Now both $p$ and $q$ are even and thus have a common factor $2$. This is a contradiction since we assumed that $p$ and $q$ are coprime. Assuming that $\sqrt{2}$ is rational leads to a contradiction, so it must be that $\sqrt{2}$ is irrational. $\square$
