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

phi_pos

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)

  19lemma phi_pos : 0 < phi := by

proof body

Tactic-mode proof.

  20  have htwo : 0 < (2 : ℝ) := by norm_num
  21  -- Use that √5 > 0
  22  have hroot_pos : 0 < Real.sqrt 5 := by
  23    have : (0 : ℝ) < 5 := by norm_num
  24    exact Real.sqrt_pos.mpr this
  25  have hnum_pos : 0 < 1 + Real.sqrt 5 := by exact add_pos_of_pos_of_nonneg (by norm_num) (le_of_lt hroot_pos)
  26  simpa [phi] using (div_pos hnum_pos htwo)
  27

depends on (1)

Lean names referenced from this declaration's body.