phi_pos

formal source

  48  nlinarith [Real.sq_sqrt h5, sq_nonneg (Real.sqrt 5)]
  49
  50/-- φ is positive. -/
  51theorem phi_pos : 0 < φ := by
  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. -/
  62theorem phi_gt_one : φ > 1 := by
  63  simp only [φ]
  64  have h5 : Real.sqrt 5 > 2 := by
  65    have h4 : (4 : ℝ) < 5 := by norm_num
  66    have hsqrt4 : Real.sqrt 4 = 2 := by
  67      rw [show (4 : ℝ) = 2^2 by norm_num, Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 2)]
  68    calc Real.sqrt 5 > Real.sqrt 4 := Real.sqrt_lt_sqrt (by norm_num) h4
  69      _ = 2 := hsqrt4
  70  linarith
  71
  72/-- φ < 2. -/
  73theorem phi_lt_two : φ < 2 := by
  74  simp only [φ]
  75  have h5 : Real.sqrt 5 < 3 := by
  76    have h9 : (5 : ℝ) < 9 := by norm_num
  77    have hsqrt9 : Real.sqrt 9 = 3 := by
  78      rw [show (9 : ℝ) = 3^2 by norm_num, Real.sqrt_sq (by norm_num : (3 : ℝ) ≥ 0)]
  79    calc Real.sqrt 5 < Real.sqrt 9 := Real.sqrt_lt_sqrt (by norm_num) h9
  80      _ = 3 := hsqrt9
  81  linarith