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

phi_lt_162

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)

  76theorem phi_lt_162 : (1 + Real.sqrt 5) / 2 < (1.62 : ℝ) := by

proof body

Tactic-mode proof.

  77  have h := phi_in_phiInterval
  78  -- phiInterval.hi = 1619/1000 < 1.62
  79  have h1 : ((1619 / 1000 : ℚ) : ℝ) < (1.62 : ℝ) := by norm_num
  80  exact lt_of_le_of_lt h.2 h1
  81
  82end IndisputableMonolith.Numerics.Interval

depends on (4)

Lean names referenced from this declaration's body.