## Stream: new members

### Topic: Proof by cases of integers modulo n

#### Julian Külshammer (Jan 17 2021 at 10:00):

I would like to prove that if $n\in \Z$ then $n(n-1)(2n-1)$ is divisible by $6$.
One of the proof strategies outside lean would be to say that $n(n-1)(2n-1)$ is divisible by $6$ if and only if $n(n-1)(2n-1)$ is $0$ in $\Z/6\Z$ and then go through all the cases of the $6$ elements of $\Z/6\Z$. Would this be possible in lean? I'm grateful for some hints on how to start.

import tactic

lemma six_div (n : ℤ) : 6 ∣ (n*(n-1)*(2*n-1)) :=
begin
sorry
end


#### Kevin Buzzard (Jan 17 2021 at 10:19):

This is certainly possible in lean (I'll knock something up) but if you just want the theorem then it would be much easier to prove using int.induction_on . Some proofs are more easily formalised than others.

#### Shing Tak Lam (Jan 17 2021 at 10:20):

import tactic
import data.zmod.basic

lemma six_div' (n : ℤ) : 6 ∣ (n*(n-1)*(2*n-1)) ↔ ((n*(n-1)*(2*n-1) : ℤ) : zmod 6) = 0 :=
begin
rw zmod.int_coe_zmod_eq_zero_iff_dvd,
norm_cast,
end

lemma six_div'' (n : ℤ) : ((n*(n-1)*(2*n-1) : ℤ) : zmod 6) = 0 :=
begin
push_cast,
set m := (n : zmod 6),
fin_cases m with [0,1,2,3,4,5],
{ -- m = 0,
sorry },
{ -- m = 1,
sorry },
-- and so on...
end

/-
Proof of the above if you don't fancy checking all 6 cases manually
lemma six_div'' (n : ℤ) : ((n*(n-1)*(2*n-1) : ℤ) : zmod 6) = 0 :=
begin
push_cast,
set m := (n : zmod 6),
fin_cases m; rw h; refl
end
-/

lemma six_div (n : ℤ) : 6 ∣ (n*(n-1)*(2*n-1)) :=
begin
rw six_div',
exact six_div'' n,
end


#### Kevin Buzzard (Jan 17 2021 at 10:46):

I have no idea why this works:

lemma six_div'' (n : ℤ) : ((n*(n-1)*(2*n-1) : ℤ) : zmod 6) = 0 :=
begin
push_cast,
set m := (n : zmod 6),
fin_cases m with [0,1,2,3,4,5];
{ rw h, apply (zmod.nat_coe_zmod_eq_zero_iff_dvd 0 6).2, simp },
end


#### Kevin Buzzard (Jan 17 2021 at 10:47):

I was initially doing stuff like norm_num, zmod.nat_coe_zmod_eq_zero_iff_dvd 84 6).2, use 14, norm_num and then when copy-pasting I noticed that even if 84 was not the result of the integer product it worked anyway.

#### Kevin Buzzard (Jan 17 2021 at 10:55):

Here's a complete proof by induction:

import tactic

lemma six_div (n : ℤ) : 6 ∣ (n*(n-1)*(2*n-1)) :=
begin
apply int.induction_on n; clear n,
{ simp },
{ rintro i ⟨m, hn⟩,
use m+i^2,
rw [mul_add (6 : ℤ), ← hn],
ring },
{ rintro i ⟨m, hn⟩,
use m-(i+1)^2,
rw [mul_sub (6 : ℤ), ← hn],
ring,
}
end


#### Kevin Buzzard (Jan 17 2021 at 10:58):

Ultimately it's barely any shorter than Shing's (partly commented) proof.

#### Patrick Massot (Jan 17 2021 at 10:59):

Did we ever follow up on https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/even.20or.20odd/near/195632609?

#### Julian Külshammer (Jan 23 2021 at 15:56):

@Kevin Buzzard @Shing Tak Lam Thanks a lot for your suggestions. The case-by-case analysis seems less complicated than I imagined. I knew one could prove it by induction but that doesn't feel like the standard choice (especially when it would come to teaching).

Last updated: Dec 20 2023 at 11:08 UTC