Reto 16: Para todo n ∈ N, n(n+1)(2n+1) es divisible por 6
Demostrar que para todo \(n \in ℕ\), \(n(n+1)(2n+1)\) es divisible por \(6\).
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Tactic variable (n : ℕ) example : 6 ∣ n * (n + 1) * (2 * n + 1) := by sorry
1. Demostración en lenguaje natural
1ª demostración
Como 2 y 3 son primos entre sí, para demostrar que \(n(n+1)(2n+1)\) es divisible por 6 basta demostrar que lo es por 2 y por 3.
Para demostrar que \(n(n+1)(2n+1)\) es divisible por 2, consideramos dos casos según el resto de dividir n entre 2; es decir, según el valor de \(n \bmod 2\).
Caso 1: Si \(n \bmod 2 = 0\), entonces \(n\) es divisible entre 2 y, por tanto, también lo es \(n(n+1)(2n+1)\).
Caso 2: Si \(n \bmod 2 = 1\), entonces \(n+1\) es divisible entre 2 y, por tanto, también lo es \(n(n+1)(2n+1)\).
Para demostrar que \(n(n+1)(2n+1)\) es divisible por 3, consideramos tres casos según el resto de dividir \(n\) entre 3; es decir, según el valor de \(n \bmod 3\).
Caso 1: Si \(n \bmod 3 = 0\), entonces \(n\) es divisible entre 3 y, por tanto, también lo es \(n(n+1)(2n+1)\).
Caso 2: Si \(n \bmod 3 = 1\), entonces \(2n+1\) es divisible entre 3 y, por tanto, también lo es \(n(n+1)(2n+1)\).
Caso 3: Si \(n \bmod 3 = 2\), entonces \(n+1\) es divisible entre 3 y, por tanto, también lo es \(n(n+1)(2n+1)\).
2ª demostración
Demostraremos, por inducción en \(n\), que \[ 6 ∣ n(n+1)(2n+1) \]
Base: Para \(n = 0\), se tiene trivialmente que \[ 6 | 0 \times (0 + 1) \times (2 \times 0 + 1) \]
Paso de inducción: Supongamos que \(n\) verifica la hipótesis de inducción: \[ 6 ∣ n(n+1)(2n+1) \tag{HI} \] Tenemos que demostrar que \[ 6 ∣ (n+1)((n+1)+1)(2(n+1)+1) \]
Por la HI, existe un \(k\) tal que \[ n(n+1)(2n+1) = 6k \tag{1} \]
La diferencia es \[ \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} \]
Por tanto, \[ \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{[por (1)]} \\ &= 6(k + (n+1)^2) \end{array} \] que es divisible por 6.
3ª demostración
Usando aritmética modular en \(ℤ\_6\), demostrar que \[ 6 ∣ n \times (n + 1) \times (2 \times n + 1) \] se reduce a \[ n \times (n + 1) \times (2 \times n + 1) ≡ 0 (\bmod 6) \] lo que se verifica trivialmente.
2. Demostraciones en Lean 4
import Mathlib.Tactic variable (n : ℕ) -- 1ª demostración -- =============== 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) -- 2ª demostración -- =============== 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) -- 3ª demostración -- =============== 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⟩ -- 4ª demostración -- =============== 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 -- 5ª demostración -- =============== 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
Es posible consultar, modificar y ejecutar el código de estas demostraciones de forma interactiva en Lean 4 Web.