theorem
proved
tactic proof
phi_pow_fib
show as:
view Lean formalization →
formal statement (Lean)
51theorem phi_pow_fib : ∀ n : ℕ, phi ^ (n + 2) =
52 (Nat.fib (n + 2) : ℝ) * phi + (Nat.fib (n + 1) : ℝ) := by
proof body
Tactic-mode proof.
53 intro n
54 induction n with
55 | zero =>
56 show phi ^ 2 = (Nat.fib 2 : ℝ) * phi + (Nat.fib 1 : ℝ)
57 rw [phi_sq]; push_cast; ring
58 | succ k ih =>
59 -- φ^(k+3) = φ^(k+2) · φ = (F(k+2)·φ + F(k+1)) · φ
60 -- = F(k+2)·φ² + F(k+1)·φ
61 -- = F(k+2)·(φ + 1) + F(k+1)·φ
62 -- = (F(k+2) + F(k+1))·φ + F(k+2)
63 -- = F(k+3)·φ + F(k+2)
64 have hsucc : phi ^ (k + 1 + 2) = phi ^ (k + 2) * phi := by ring
65 rw [hsucc, ih]
66 have hsq : phi^2 = phi + 1 := phi_sq
67 have hfib_rec : (Nat.fib (k + 1 + 2) : ℝ) =
68 (Nat.fib (k + 2) : ℝ) + (Nat.fib (k + 1) : ℝ) := by
69 have hnat : Nat.fib (k + 1 + 2) = Nat.fib (k + 1) + Nat.fib (k + 2) :=
70 Nat.fib_add_two
71 push_cast [hnat]; ring
72 rw [hfib_rec]
73 nlinarith [hsq]
74
75/-- Fibonacci coefficients are strictly increasing from n ≥ 1 (since F(1)=F(2)=1,
76 strict starts at n=2). -/