lemma
proved
wrapper
phi43_gt
show as:
view Lean formalization →
formal statement (Lean)
285private lemma phi43_gt : (969030000 : ℝ) < Constants.phi ^ (43 : ℕ) := by
proof body
One-line wrapper that applies rw.
286 rw [phi_eq_goldenRatio]; exact Numerics.phi_pow43_gt