pellZd_succ_succ — Mathlib

English

For a > 1, pellZd(a, n+2) + pellZd(a, n) = 2 a · pellZd(a, n+1).

Русский

Для a > 1 выполняется: pellZd(a, n+2) + pellZd(a, n) = 2 a · pellZd(a, n+1).

LaTeX

$$$\\text{pellZd}(a, n+2) + \\text{pellZd}(a, n) = 2 a \\cdot \\text{pellZd}(a, n+1).$$$

Lean4

theorem pellZd_succ_succ (n) : pellZd a1 (n + 2) + pellZd a1 n = (2 * a : ℕ) * pellZd a1 (n + 1) :=
  by
  have : (1 : ℤ√(d a1)) + ⟨a, 1⟩ * ⟨a, 1⟩ = ⟨a, 1⟩ * (2 * a) :=
    by
    rw [Zsqrtd.natCast_val]
    change (⟨_, _⟩ : ℤ√(d a1)) = ⟨_, _⟩
    rw [dz_val]
    dsimp [az]
    ext <;> dsimp <;> ring_nf
  simpa [mul_add, mul_comm, mul_left_comm, add_comm] using congr_arg (· * pellZd a1 n) this

Похожие утверждения