## An irrationality proof involving cube roots

[examples

newbies

Isar

]
According to myth, the discovery that √2 was irrational so horrified the students of Pythagoras that it was kept secret upon pain of death. Its irrationality was thought to be paradoxical because √2 could be constructed as the hypotenuse of a right triangle, and therefore definitely “existed”, while all numbers were assumed to be rational. A while back, I formalised a new proof of the irrationality of √2. Just recently, I stumbled upon an exam question: to prove the irrationality of ∛2+∛3. Its proof uses different techniques, but it’s not at all hard. Why not pause for a moment to prove it for yourself before looking at the formal treatment below?

### The informal proof

Let’s begin by defining $x = \sqrt[3]2+\sqrt[3]3$. It’s natural to see what happens if we cube both sides. Multiplying out and collecting the terms on the right hand side, we find that $x^3 = 5 + 3x\sqrt[3]6$. But this can’t be right: if $x$ is rational then so is $x^3$, which equals the right hand side, which must also be rational. In that case, $\sqrt[3]6$ is a rational number. It obviously isn’t.

Formalising this argument in Isabelle/HOL, we get a nice Isar proof.

### The calculation

We begin by stating the desired claim. A rather obscure feature of Isar syntax is the ability to make a definition right in the theorem statement. Any such definitions will be expanded in the final theorem, once we have proved it.

lemma cuberoot_irrational: defines "x ≡ root 3 2 + root 3 3" shows "x ∉ ℚ"

Now we commence the proof. Another Isar fine point: omitting the proof method after the
`proof`

keyword calls for the default method, which in this case
is to assume the formula, stripped of its initial negation.
In order to obtain the number 5 without complications, we pre-evaluate
the cube roots of 8 and 27.
As in the informal proof, we quickly deduce that the right-hand side is rational.

proof assume "x ∈ ℚ" moreover have "root 3 8 = 2" "root 3 27 = 3" by auto then have xcubed: "x^3 = 5 + 3 * x * root 3 6" by (simp add: x_def algebra_simps eval_nat_numeral flip: real_root_mult) ultimately have Q: "5 + 3 * x * root 3 6 ∈ ℚ" by (metis Rats_power ‹x ∈ ℚ›)

### A nested proof

We could have proved that $\sqrt[3]6$ is irrational separately, but we can just as easily embed it in the larger proof. The argument should be familiar: we write $\sqrt[3]6$ as $a/b$, the ratio of two coprime integers. We then demonstrate that both $a$ and $b$ are divisible by two. See if you can follow the reasoning in the Isar text below.

have "root 3 6 ∉ ℚ" proof assume "root 3 6 ∈ ℚ" then obtain a b where "a / b = root 3 6" and cop: "coprime a b" "b≠0" by (smt (verit, best) Rats_cases') then have "(a/b)^3 = 6" by auto then have eq: "a^3 = 2*3 * b^3" using of_int_eq_iff by (fastforce simp: divide_simps ‹b≠0›) then have p: "2 dvd a" by (metis coprime_left_2_iff_odd coprime_power_right_iff dvd_triv_left mult.assoc) then obtain c where "a = 2*c" by blast with eq have "2 dvd b" by (simp add: eval_nat_numeral) (metis even_mult_iff even_numeral odd_numeral) with p and cop show False by fastforce qed

### Finishing up

We know that the right side of our calculation above must be rational, although $\sqrt[3]6$ is irrational. Just a tiny bit more work remains. We need to show that $3x$ is nonzero as well as rational. Given that extra fact, the contradiction is found automatically, thanks to Sledgehammer.

moreover have "3*x ∈ ℚ - {0}" using xcubed by (force simp: ‹x ∈ ℚ›) ultimately have "3 * x * root 3 6 ∉ ℚ" using Rats_divide by force with Q show False by (metis Rats_diff Rats_number_of add.commute add_uminus_conv_diff diff_add_cancel) qed

Another Isar fine point: note how `moreover`

is used to collect facts.
Each instance of `moreover`

records the fact just proved, and this sequence terminates
with `ultimately`

, when all the recorded facts are made available to the next proof method.
Above, `ultimately`

delivers two facts (that $\sqrt[3]6$ is irrational and that $3x$
is a nonzero rational) to conclude that $3x\sqrt[3]6$ is irrational.
The point of moreover/ultimately is to reduce our reliance on labels.

The Isabelle theory file is available to download. You can also check out a much more sophisticated proof, that exponentials are irrational.