Two is not a cube

Stream: general

[Ruben Van de Velde]

Is there any easier way to prove this?

lemma two_not_cube {r : ℕ} : r ^ 3 ≠ 2 :=
begin
  rcases r with (rfl|rfl|k),
  {norm_num},
  {norm_num},
  apply ne_of_gt,
  calc 2 < 2 ^ 3 : by norm_num
  ... ≤ (k + 2) ^ 3 : nat.pow_le_pow_of_le_left (nat.le_add_left _ _) _
end

[Kevin Buzzard]

For me the lemma in the library should be that if f from nat to some ordered thing is monotone, and if f(n) <t<f(n+1) then t is not in the range of f

[Kenny Lau]

i.e. the philosophy is "generalize"

[Mario Carneiro]

lemma not_cube {a} (n : ℕ) (h1 : n ^ 3 < a) (h2 : a < (n+1) ^ 3) (r) : r ^ 3 ≠ a :=
begin
  cases le_or_lt r n,
  { linarith [nat.pow_le_pow_of_le_left h 3] },
  { linarith [show (n+1)^3 ≤ _, from nat.pow_le_pow_of_le_left h 3] },
end

lemma two_not_cube {r : ℕ} : r ^ 3 ≠ 2 :=
not_cube 1 (by norm_num) (by norm_num) r

[Kevin Buzzard]

There's no pow_n_mono?

[Mario Carneiro]

nat.pow is oldschool

[Kevin Buzzard]

Lol

[Mario Carneiro]

But it's pretty direct from nat.pow_le_pow_of_le_left

[Patrick Massot]

We should also have a tactic "descends to zmod n and norm_num working in zmod n.

[Kenny Lau]

what's the n that works for this case?

[Patrick Massot]

Then the proof would be something like:

begin
  go_mod 4,
  fin_cases r ; norm_num
end

[Kenny Lau]

I guess 7

[Kenny Lau]

oh right, 4 also works

[Patrick Massot]

probably go_mod should also take r as an argument.

[Patrick Massot]

Or else ask to revert r first.

[Kenny Lau]

(modified from Mario's code)

import tactic

lemma two_not_cube {r : ℕ} : r ^ 3 ≠ 2 :=
begin
  cases le_or_lt r 2 with h h,
  { revert r, exact dec_trivial },
  { refine ne_of_gt (lt_trans _ $ pow_lt_pow_of_lt_left h _ _); norm_num }
end

[Kenny Lau]

(Patrick's suggestion)

import tactic data.zmod.basic

lemma two_not_cube {r : ℕ} : r ^ 3 ≠ 2 :=
begin
  intro h,
  apply_fun (coe : ℕ → zmod 4) at h,
  norm_cast at h,
  rw nat.cast_pow at h, -- why didn't norm_cast do this?
  generalize_hyp : (r : zmod 4) = r4 at h,
  revert r4, dec_trivial
end

[Mario Carneiro]

is go_mod a tactic?

[Kenny Lau]

it's a tactic Patrick's proposed just now

[Patrick Massot]

Mario, you get to choose the name if you write that tactic.

[Mario Carneiro]

I have no objections to the name (well..) but I was just double checking that it hadn't been added when I wasn't looking

[Patrick Massot]

I used "go" because "descend" or "lift" are so controversial here.

[Patrick Massot]

But it should obviously be "descend".

[Mario Carneiro]

zmod_bash?

[Patrick Massot]

That would be the combination of go_mod and fin_cases

[Kevin Buzzard]

p works iff it's 1 mod 3 and not of the form x^2+27y^2 -- a passing number theorist.

[Oliver Nash]

I was really hoping this was a question over ℚ rather than ℕ so that I could suggest this approach.

[Floris van Doorn]

@Mario Carneiro's not_cube can be easily proven with ne_of_monotone_of_lt_of_lt after #4482 is merged.

[Floris van Doorn]

Oliver Nash said:

I was really hoping this was a question over ℚ rather than ℕ so that I could suggest this approach.

r ^ 3 = 1 ^ 3 + 1 ^ 3 has no solutions by FLT, so the same proof appoach still works :)

[Kevin Buzzard]

Wiles' proof only works for p>=5 because the Frey curve can have torsion when p=3, so really you're relying on something much older (Euler I guess)

[Ruben Van de Velde]

Not finding a way to do Euler without this fact, though

[Ruben Van de Velde]

And thanks for the suggestions, everyone!