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

phi_gt_onePointFive

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)

  78lemma phi_gt_onePointFive : (1.5 : ℝ) < phi := by

proof body

Tactic-mode proof.

  79  simp only [phi]
  80  have h5 : (2 : ℝ) < Real.sqrt 5 := by
  81    have h : (2 : ℝ)^2 < 5 := by norm_num
  82    rw [← Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 2)]
  83    exact Real.sqrt_lt_sqrt (by norm_num) h
  84  linarith
  85
  86/-- Tighter upper bound: φ < 1.62 (since √5 < 2.24). -/

used by (40)

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

… and 10 more