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

phi_lt_onePointSixTwo

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)

  87lemma phi_lt_onePointSixTwo : phi < (1.62 : ℝ) := by

proof body

Tactic-mode proof.

  88  simp only [phi]
  89  have h5 : Real.sqrt 5 < (2.24 : ℝ) := by
  90    have h : (5 : ℝ) < (2.24 : ℝ)^2 := by norm_num
  91    have h24_pos : (0 : ℝ) ≤ 2.24 := by norm_num
  92    rw [← Real.sqrt_sq h24_pos]
  93    exact Real.sqrt_lt_sqrt (by norm_num) h
  94  linarith
  95
  96/-- Even tighter lower bound: φ > 1.61. -/

used by (40)

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

… and 10 more