theorem proved tactic proof

`phi_gt_onePointSixOneEight`

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

formal statement (Lean)

  84theorem phi_gt_onePointSixOneEight : φ > (1.618 : ℝ) := by

proof body

Tactic-mode proof.

  85  simp only [φ]
  86  have h5 : Real.sqrt 5 > (2.236 : ℝ) := by
  87    have h : (2.236 : ℝ)^2 < 5 := by norm_num
  88    rw [← Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 2.236)]
  89    exact Real.sqrt_lt_sqrt (by norm_num) h
  90  linarith
  91
  92/-- φ < 1.619. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

phi_gt_onePointSix in IndisputableMonolith.Foundation.PhiForcing decl_use