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 que existen infinitos números primos.
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Tactic import Mathlib.Data.Nat.Prime.Defs open Nat example (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p := by sorry