Reto 15: Existe un k ∈ ℕ tal que, para todo n ∈ ℕ, (n + k)² ≤ 2ⁿ⁺ᵏ

José A. Alonso

Retos en Lean 4/Teoría de números/Inducción

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

Reto 14: Para todo n ∈ ℕ, 2n + 9 ≤ 2ⁿ⁺⁴

José A. Alonso

Retos en Lean 4/Teoría de números/Inducción

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

José A. Alonso

Retos en Lean 4/Teoría de números/Inducción

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