pith. machine review for the scientific record. sign in
lemma proved tactic proof

phi_fifth_eq

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 135lemma phi_fifth_eq : phi^5 = 5 * phi + 3 := by

proof body

Tactic-mode proof.

 136  calc phi^5 = phi * phi^4 := by ring
 137    _ = phi * (3 * phi + 2) := by rw [phi_fourth_eq]
 138    _ = 3 * phi^2 + 2 * phi := by ring
 139    _ = 3 * (phi + 1) + 2 * phi := by rw [phi_sq_eq]
 140    _ = 5 * phi + 3 := by ring
 141
 142/-! ### Bounds from Fibonacci identities -/
 143
 144/-- φ³ is between 4.0 and 4.25.
 145    φ³ = 2φ + 1 ≈ 4.236. -/

used by (9)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.