lemma proved term proof

`log_phi_bound`

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

formal statement (Lean)

  66lemma log_phi_bound : (0.481211 : ℝ) ≤ Real.log Real.goldenRatio ∧
  67    Real.log Real.goldenRatio ≤ (0.481212 : ℝ) := by

Term-mode proof.

  68  constructor <;> num_ineq
  69
  70end IntervalProofs
  71end Numerics
  72end IndisputableMonolith