# Zulip Chat Archive

## 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

#### Kevin Buzzard (Oct 11 2020 at 13:21):

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
```

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

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".

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

`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