lemma
proved
wrapper
phi59_gt
show as:
view Lean formalization →
formal statement (Lean)
84private lemma phi59_gt : (2138898000000 : ℝ) < Constants.phi ^ (59 : ℕ) := by
proof body
One-line wrapper that applies rw.
85 rw [phi_eq_goldenRatio]; exact Numerics.phi_pow59_gt