theorem
proved
tactic proof
fibonacci_recurrence
show as:
view Lean formalization →
formal statement (Lean)
64theorem fibonacci_recurrence (n : ℕ) :
65 phi ^ (n + 2) = phi ^ (n + 1) + phi ^ n := by
proof body
Tactic-mode proof.
66 calc phi ^ (n + 2) = phi ^ n * phi ^ 2 := by ring
67 _ = phi ^ n * (phi + 1) := by rw [phi_sq_eq]
68 _ = phi ^ (n + 1) + phi ^ n := by ring
69
70/-- Consecutive φ-ladder rungs have ratio exactly φ. -/