Proof by cases of integers modulo n

Stream: new members

[Julian Külshammer]

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]

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]

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]

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]

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]

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]

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

[Patrick Massot]

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

[Julian Külshammer]

@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).