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

phi_gt_161

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)

  69theorem phi_gt_161 : (1.61 : ℝ) < (1 + Real.sqrt 5) / 2 := by

proof body

Tactic-mode proof.

  70  have h := phi_in_phiInterval
  71  -- phiInterval.lo = 1618/1000 > 1.61
  72  have h1 : (1.61 : ℝ) < (1618 / 1000 : ℚ) := by norm_num
  73  exact lt_of_lt_of_le h1 h.1
  74
  75/-- Example: Prove φ < 1.62 (using interval hi = 1619/1000) -/

depends on (3)

Lean names referenced from this declaration's body.