theorem
proved
term proof
phi_fixed_point'
show as:
view Lean formalization →
formal statement (Lean)
27theorem phi_fixed_point' : phi = 1 + phi⁻¹ := by
proof body
Term-mode proof.
28 have hphi_pos : phi > 0 := phi_pos
29 have hphi_ne : phi ≠ 0 := ne_of_gt hphi_pos
30 -- From phi_squared: φ² = φ + 1
31 -- Divide both sides by φ: φ = 1 + 1/φ
32 have h := phi_squared
33 field_simp at h ⊢
34 linarith
35
36/-- φ > 1: The golden ratio is strictly greater than 1.
37
38 This is already proven in Constants.lean -/