goldenRatio_mul_fib_succ_add_fib — Mathlib

English

φ · Nat.fib(n+1) + Nat.fib(n) = φ^(n+1) (as a real).

Русский

φ · Nat.fib(n+1) + Nat.fib(n) = φ^(n+1) (как число действительное).

LaTeX

$$$ \phi \cdot (\mathrm{Nat.fib}(n+1) : \mathbb{R}) + (\mathrm{Nat.fib}(n) : \mathbb{R}) = \phi^{n+1} $$$

Lean4

/-- Relationship between the Fibonacci Sequence, Golden Ratio and its exponents -/
theorem goldenRatio_mul_fib_succ_add_fib (n : ℕ) : φ * Nat.fib (n + 1) + Nat.fib n = φ ^ (n + 1) := by
  induction n with
  | zero => simp
  | succ n ih =>
    calc
      _ = φ * (Nat.fib n) + φ ^ 2 * (Nat.fib (n + 1)) := by
        simp only [Nat.fib_add_one (Nat.succ_ne_zero n), Nat.succ_sub_succ_eq_sub, tsub_zero, Nat.cast_add,
          goldenRatio_sq];
        ring
      _ = φ * ((Nat.fib n) + φ * (Nat.fib (n + 1))) := by ring
      _ = φ ^ (n + 2) := by rw [add_comm, ih]; ring

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