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
Demostrar que existe un \(k ∈ ℕ\) tal que, para todo \(n \in ℕ\), \((n + k)^{2} ≤ 2^{n+k}\).
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Tactic example : ∃ k : ℕ, ∀ n : ℕ, (n + k) ^ 2 ≤ 2 ^ (n + k) := by sorry
Demostrar que, para todo \(n \in ℕ\), \(2n + 9 ≤ 2^{n+4}\).
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Tactic variable (n : ℕ) example : 2 * n + 9 ≤ 2 ^ (n + 4) := by sorry
Demostrar en Lean 4 que, 5²ⁿ - 2³ⁿ es divisible por 17 para todo número natural n.
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Data.Nat.Basic import Mathlib.Tactic variable (n : ℕ) open Nat example : 17 ∣ 5^(2 * n) - 2^(3 * n) := by sorry
Demostrar el teorema de Nicómaco que afirma que la suma de los cubos de los \(n\) primeros números naturales es igual que el cuadrado de la suma de los \(n\) primeros números naturales; es decir, para todo número natural n se tiene que \[ 1^3 + 2^3 + ... + n^3 = (1 + 2 + ... + n)^2 \]