lean_workbook_plus_48247

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Let $n$ be a positive integer number and $x_n=(3+\sqrt 5)^n+(3-\sqrt 5)^n$ . Prove that : $2^n|x_n\ ,\ \forall\ n\in\mathbb{N}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_48247 (n : ℕ) (hn : 0 < n) (x_n : ℝ) (hx_n : x_n = (3 + Real.sqrt 5)^n + (3 - Real.sqrt 5)^n) : 2^n ∣ x_n   :=  by sorry

Source