Challenge 16: For every n ∈ N, n(n+1)(2n+1) is divisible by 6
Prove that for every \(n \in ℕ\), \(n(n+1)(2n+1)\) is divisible by \(6\).
To do so, complete the following Lean 4 theory:
import Mathlib.Tactic variable (n : ℕ) example : 6 ∣ n * (n + 1) * (2 * n + 1) := by sorry
1. Proof in natural language
Proof 1
Since 2 and 3 are coprime, to prove that \(n(n+1)(2n+1)\) is divisible by 6 it suffices to prove that it is divisible by 2 and by 3.
To prove that \(n(n+1)(2n+1)\) is divisible by 2, we consider two cases according to the remainder of dividing n by 2; that is, according to the value of \(n \bmod 2\).
Case 1: If \(n \bmod 2 = 0\), then \(n\) is divisible by 2 and, therefore, so is \(n(n+1)(2n+1)\).
Case 2: If \(n \bmod 2 = 1\), then \(n+1\) is divisible by 2 and, therefore, so is \(n(n+1)(2n+1)\).
To prove that \(n(n+1)(2n+1)\) is divisible by 3, we consider three cases according to the remainder of dividing \(n\) by 3; that is, according to the value of \(n \bmod 3\).
Case 1: If \(n \bmod 3 = 0\), then \(n\) is divisible by 3 and, therefore, so is \(n(n+1)(2n+1)\).
Case 2: If \(n \bmod 3 = 1\), then \(2n+1\) is divisible by 3 and, therefore, so is \(n(n+1)(2n+1)\).
Case 3: If \(n \bmod 3 = 2\), then \(n+1\) is divisible by 3 and, therefore, so is \(n(n+1)(2n+1)\).
Proof 2
We will prove, by induction on \(n\), that \[ 6 ∣ n(n+1)(2n+1) \]
Base case: For \(n = 0\), we trivially have that \[ 6 | 0 \times (0 + 1) \times (2 \times 0 + 1) \]
Inductive step: Suppose that \(n\) satisfies the induction hypothesis: \[ 6 ∣ n(n+1)(2n+1) \tag{IH} \] We have to prove that \[ 6 ∣ (n+1)((n+1)+1)(2(n+1)+1) \]
By the IH, there exists a \(k\) such that \[ n(n+1)(2n+1) = 6k \tag{1} \]
The difference is \[ \begin{array}{ll} (n+1)((n+1)+1)(2(n+1)+1) - n(n+1)(2n+1) &= (n+1)(n+2)(2n+3) - n(n+1)(2n+1) \\ &= (n+1)[(n+2)(2n+3) - n(2n+1)] \\ &= (n+1)[2n^2 + 7n + 6 - 2n^2 - n] \\ &= (n+1)(6n + 6) \\ &= 6(n+1)^2 \\ \end{array} \]
Therefore, \[ \begin{array}{llll} (n+1)((n+1)+1)(2(n+1)+1) &= n(n+1)(2n+1) + 6(n+1)^2 \\ &= 6k + 6(n+1)^2 &&\text{[by (1)]} \\ &= 6(k + (n+1)^2) \end{array} \] which is divisible by 6.
Proof 3
Using modular arithmetic in \(ℤ\_6\), proving that \[ 6 ∣ n \times (n + 1) \times (2 \times n + 1) \] reduces to \[ n \times (n + 1) \times (2 \times n + 1) ≡ 0 (\bmod 6) \] which holds trivially.
2. Proofs in Lean 4
import Mathlib.Tactic variable (n : ℕ) -- Proof 1 -- ======= example : 6 ∣ n * (n + 1) * (2 * n + 1) := by have h1 : Nat.Coprime 2 3 := by norm_num apply Nat.Coprime.mul_dvd_of_dvd_of_dvd h1 · -- ⊢ 2 ∣ n * (n + 1) * (2 * n + 1) have h2 : n % 2 < 2 := by omega interval_cases h4 : n % 2 · -- h4 : n % 2 = 0 have h5 : 2 ∣ n := by omega have h6 : 2 ∣ n * (n + 1) := dvd_mul_of_dvd_left h5 (n + 1) exact dvd_mul_of_dvd_left h6 (2 * n + 1) · -- h4 : n % 2 = 1 have h5 : 2 ∣ n + 1 := by omega have h6 : 2 ∣ n * (n + 1) := dvd_mul_of_dvd_right h5 n exact dvd_mul_of_dvd_left h6 (2 * n + 1) · -- ⊢ 3 ∣ n * (n + 1) * (2 * n + 1) have h3 : n % 3 < 3 := by omega interval_cases h4 : n % 3 · -- h4 : n % 3 = 0 have h5 : 3 ∣ n := by omega have h6 : 3 ∣ n * (n + 1) := dvd_mul_of_dvd_left h5 (n + 1) exact dvd_mul_of_dvd_left h6 (2 * n + 1) · -- h4 : n % 3 = 1 have h5 : 3 ∣ 2 * n + 1 := by omega exact dvd_mul_of_dvd_right h5 (n * (n + 1)) · -- h4 : n % 3 = 2 have h5 : 3 ∣ n + 1 := by omega have h6 : 3 ∣ n * (n + 1) := dvd_mul_of_dvd_right h5 n exact dvd_mul_of_dvd_left h6 (2 * n + 1) -- Proof 2 -- ======= example : 6 ∣ n * (n + 1) * (2 * n + 1) := by have h1 : Nat.Coprime 2 3 := by norm_num apply Nat.Coprime.mul_dvd_of_dvd_of_dvd h1 · -- ⊢ 2 ∣ n * (n + 1) * (2 * n + 1) have h2 : n % 2 < 2 := by omega interval_cases h4 : n % 2 · -- h4 : n % 2 = 0 have h5 : 2 ∣ n := by omega exact dvd_mul_of_dvd_left (dvd_mul_of_dvd_left h5 (n + 1)) (2 * n + 1) · -- h4 : n % 2 = 1 have h5 : 2 ∣ n + 1 := by omega exact dvd_mul_of_dvd_left (dvd_mul_of_dvd_right h5 n) (2 * n + 1) · -- ⊢ 3 ∣ n * (n + 1) * (2 * n + 1) have h3 : n % 3 < 3 := by omega interval_cases h4 : n % 3 · -- h4 : n % 3 = 0 have h5 : 3 ∣ n := by omega exact dvd_mul_of_dvd_left (dvd_mul_of_dvd_left h5 (n + 1)) (2 * n + 1) · -- h4 : n % 3 = 1 have h5 : 3 ∣ 2 * n + 1 := by omega exact dvd_mul_of_dvd_right h5 (n * (n + 1)) · -- h4 : n % 3 = 2 have h5 : 3 ∣ n + 1 := by omega exact dvd_mul_of_dvd_left (dvd_mul_of_dvd_right h5 n) (2 * n + 1) -- Proof 3 -- ======= example : 6 ∣ n * (n + 1) * (2 * n + 1) := by induction n with | zero => -- ⊢ 6 ∣ 0 * (0 + 1) * (2 * 0 + 1) use 0 | succ n ih => -- n : ℕ -- ih : 6 ∣ n * (n + 1) * (2 * n + 1) -- ⊢ 6 ∣ (n + 1) * (n + 1 + 1) * (2 * (n + 1) + 1) obtain ⟨k, hk⟩ := ih -- k : ℕ -- hk : n * (n + 1) * (2 * n + 1) = 6 * k exact ⟨k + (n + 1) ^ 2, by linear_combination hk⟩ -- Proof 4 -- ======= example : 6 ∣ n * (n + 1) * (2 * n + 1) := by induction n with | zero => -- ⊢ 6 ∣ 0 * (0 + 1) * (2 * 0 + 1) use 0 | succ n ih => -- n : ℕ -- ih : 6 ∣ n * (n + 1) * (2 * n + 1) -- ⊢ 6 ∣ (n + 1) * (n + 1 + 1) * (2 * (n + 1) + 1) have h1 : (n + 1) * ((n + 1) + 1) * (2 * (n + 1) + 1) = n * (n + 1) * (2 * n + 1) + 6 * (n + 1) ^ 2 := by ring obtain ⟨k, hk⟩ := ih -- k : ℕ -- hk : n * (n + 1) * (2 * n + 1) = 6 * k use k + (n + 1) ^ 2 -- ⊢ (n + 1) * (n + 1 + 1) * (2 * (n + 1) + 1) = 6 * (k + -- (n + 1) ^ 2) calc (n + 1) * (n + 1 + 1) * (2 * (n + 1) + 1) _ = n * (n + 1) * (2 * n + 1) + 6 * (n + 1) ^ 2 := by ring _ = 6 * k + 6 * (n + 1) ^ 2 := by rw [hk] _ = 6 * (k + (n + 1) ^ 2) := by grind -- Proof 5 -- ======= example : 6 ∣ n * (n + 1) * (2 * n + 1) := by have h : ∀ k : ZMod 6, k * (k + 1) * (2 * k + 1) = 0 := by decide rw [← ZMod.natCast_eq_zero_iff] -- ⊢ ↑(n * (n + 1) * (2 * n + 1)) = 0 push_cast -- ⊢ ↑n * (↑n + 1) * (2 * ↑n + 1) = 0 exact h n
You can inspect, modify and run the code of these proofs interactively in Lean 4 Web.
3. Collaborative solutions
Have you found a proof that differs from the published ones? You can share it in the comments below by following these steps:
- Write your proof in live.lean-lang.org and check that it compiles without errors.
- Copy the code and post it in the comments of this entry, inside a Lean code block:
```lean -- your proof ```
Comments