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