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

log_phi_lt_049

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)

  62theorem log_phi_lt_049 : Real.log ((1 + Real.sqrt 5) / 2) < (0.49 : ℝ) := by

proof body

Tactic-mode proof.

  63  have h := log_phi_in_interval
  64  -- logPhiInterval.hi = 482/1000 < 0.49
  65  have h1 : ((482 / 1000 : ℚ) : ℝ) < (0.49 : ℝ) := by norm_num
  66  exact lt_of_le_of_lt h.2 h1
  67
  68/-- Example: Prove φ > 1.61 (using interval lo = 1618/1000) -/

depends on (3)

Lean names referenced from this declaration's body.