`phi_lt_162`

proved

show as: view math explainer →

module: IndisputableMonolith.Numerics.Interval.Tactic
domain: Numerics
line: 76 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Numerics.Interval.Tactic on GitHub at line 76.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  73  exact lt_of_lt_of_le h1 h.1
  74
  75/-- Example: Prove φ < 1.62 (using interval hi = 1619/1000) -/
  76theorem phi_lt_162 : (1 + Real.sqrt 5) / 2 < (1.62 : ℝ) := by
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.