phi_pos

formal source

  16/-- Golden ratio φ as a concrete real. -/
  17noncomputable def phi : ℝ := (1 + Real.sqrt 5) / 2
  18
  19lemma phi_pos : 0 < phi := by
  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
  28lemma one_lt_phi : 1 < phi := by
  29  have htwo : 0 < (2 : ℝ) := by norm_num
  30  have hsqrt_gt : Real.sqrt 1 < Real.sqrt 5 := by
  31    simpa [Real.sqrt_one] using (Real.sqrt_lt_sqrt (by norm_num) (by norm_num : (1 : ℝ) < 5))
  32  have h2lt : (2 : ℝ) < 1 + Real.sqrt 5 := by
  33    have h1lt : (1 : ℝ) < Real.sqrt 5 := by simpa [Real.sqrt_one] using hsqrt_gt
  34    linarith
  35  have hdiv : (2 : ℝ) / 2 < (1 + Real.sqrt 5) / 2 := (div_lt_div_of_pos_right h2lt htwo)
  36  have hone_lt : 1 < (1 + Real.sqrt 5) / 2 := by simpa using hdiv
  37  simpa [phi] using hone_lt
  38
  39lemma phi_ge_one : 1 ≤ phi := le_of_lt one_lt_phi
  40lemma phi_ne_zero : phi ≠ 0 := ne_of_gt phi_pos
  41lemma phi_ne_one : phi ≠ 1 := ne_of_gt one_lt_phi
  42
  43lemma phi_lt_two : phi < 2 := by
  44  have hsqrt5_lt : Real.sqrt 5 < 3 := by
  45    have h5_lt_9 : (5 : ℝ) < 9 := by norm_num
  46    have h9_eq : Real.sqrt 9 = 3 := by
  47      rw [show (9 : ℝ) = 3^2 by norm_num, Real.sqrt_sq (by norm_num : (3 : ℝ) ≥ 0)]
  48    have : Real.sqrt 5 < Real.sqrt 9 := Real.sqrt_lt_sqrt (by norm_num) h5_lt_9
  49    rwa [h9_eq] at this