## Stream: general

### Topic: Two is not a cube

#### Ruben Van de Velde (Oct 11 2020 at 12:33):

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 (Oct 11 2020 at 13:17):

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 (Oct 11 2020 at 13:19):

i.e. the philosophy is "generalize"

#### Mario Carneiro (Oct 11 2020 at 13:19):

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 (Oct 11 2020 at 13:20):

There's no pow_n_mono?

#### Mario Carneiro (Oct 11 2020 at 13:20):

nat.pow is oldschool

Lol

#### Mario Carneiro (Oct 11 2020 at 13:21):

But it's pretty direct from nat.pow_le_pow_of_le_left

#### Patrick Massot (Oct 11 2020 at 13:24):

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

#### Kenny Lau (Oct 11 2020 at 13:25):

what's the n that works for this case?

#### Patrick Massot (Oct 11 2020 at 13:25):

Then the proof would be something like:

begin
go_mod 4,
fin_cases r ; norm_num
end

I guess 7

#### Kenny Lau (Oct 11 2020 at 13:25):

oh right, 4 also works

#### Patrick Massot (Oct 11 2020 at 13:26):

probably go_mod should also take r as an argument.

#### Patrick Massot (Oct 11 2020 at 13:27):

Or else ask to revert r first.

#### Kenny Lau (Oct 11 2020 at 13:28):

(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 (Oct 11 2020 at 13:32):

(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 (Oct 11 2020 at 13:33):

is go_mod a tactic?

#### Kenny Lau (Oct 11 2020 at 13:33):

it's a tactic Patrick's proposed just now

#### Patrick Massot (Oct 11 2020 at 13:33):

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

#### Mario Carneiro (Oct 11 2020 at 13:36):

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 (Oct 11 2020 at 13:36):

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

#### Patrick Massot (Oct 11 2020 at 13:37):

But it should obviously be "descend".

zmod_bash?

#### Patrick Massot (Oct 11 2020 at 13:37):

That would be the combination of go_mod and fin_cases

#### Kevin Buzzard (Oct 11 2020 at 14:41):

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

#### Oliver Nash (Oct 11 2020 at 15:53):

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

#### Floris van Doorn (Oct 11 2020 at 23:51):

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

#### Floris van Doorn (Oct 11 2020 at 23:53):

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 (Oct 12 2020 at 06:18):

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 (Oct 12 2020 at 07:59):

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

#### Ruben Van de Velde (Oct 12 2020 at 07:59):

And thanks for the suggestions, everyone!

Last updated: May 13 2021 at 06:15 UTC