theorem proved tactic proof

`phi_pos`

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

formal statement (Lean)

  51theorem phi_pos : 0 < φ := by

proof body

Tactic-mode proof.

  52  simp only [φ]
  53  have h5 : Real.sqrt 5 > 2 := by
  54    have h4 : (4 : ℝ) < 5 := by norm_num
  55    have hsqrt4 : Real.sqrt 4 = 2 := by
  56      rw [show (4 : ℝ) = 2^2 by norm_num, Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 2)]
  57    calc Real.sqrt 5 > Real.sqrt 4 := Real.sqrt_lt_sqrt (by norm_num) h4
  58      _ = 2 := hsqrt4
  59  linarith
  60
  61/-- φ > 1. -/