Question on a constructive proof of irrationality of $\sqrt 2$

Here is the constructive proof of $\sqrt 2 \not \in \mathbb Q$ found on this page :

Given positive integers $a$ and $b$, because the valuation (i.e., highest power of 2 dividing a number) of $2b^2$ is odd, while the valuation of $a^2$ is even, they must be distinct integers; thus $|2 b^2 - a^2| \geq 1$. Then

$$\left|\sqrt2 - \frac{a}{b}\right| = \frac{|2b^2-a^2|}{b^2(\sqrt{2}+a/b)} \ge \frac{1}{b^2(\sqrt2 + a / b)} \ge \frac{1}{3b^2},$$

the latter inequality being true because we assume $\frac{a}{b} \leq 3- \sqrt{2}$ (otherwise the quantitative apartness can be trivially established).

I don't understand why the first equality holds: why is it possible to divide by $\sqrt 2 + a/b$, since it is not yet known whether this number is zero... ?

• The argument is interesting, but the result says (IMHO) more about our ability to approximate $\sqrt2$ by rational numbers. After all, the fact that the approximation error is not zero, i.e. the numerator is $\ge1$, is the beef in seeing that $\sqrt2$ is irrational. Anyway, I added that tag as well. – Jyrki Lahtonen Dec 26 '15 at 17:58
• Is it a constructive fact that the valuation of $b^2$ is odd while the valuation of $a^2$ is even? It's obvious by contradiction, but I don't see why it should be constructive. – Patrick Stevens Dec 27 '15 at 10:01
• That should be the valuation of $2b^2$, not $b^2$. – TonyK Dec 27 '15 at 10:02
• @Patrick Stevens : if $b = 2^k n$ with $n$ odd, then $2b^2 = 2^{2k+1}n^2$ with $n^2$ odd ; therefore the $2$-adic valuation of $2b^2$ is odd. No need of "reductio ad absurdum". – Watson Dec 29 '15 at 12:15
• – Watson Feb 4 '18 at 22:58

$\sqrt{2}$ and $a/b$ are both (strictly) positive, so $\sqrt{2} + a/b$ cannot be zero.
Given positive integers $a$ and $b$.