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

phi_lt_two

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)

  43lemma phi_lt_two : phi < 2 := by

proof body

Tactic-mode proof.

  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
  50  have hnum_lt : 1 + Real.sqrt 5 < 4 := by linarith
  51  have : (1 + Real.sqrt 5) / 2 < 4 / 2 := div_lt_div_of_pos_right hnum_lt (by norm_num)
  52  simp only [phi]
  53  linarith
  54
  55/-! ### φ irrationality -/
  56
  57/-- φ is irrational (degree 2 algebraic, not rational).
  58
  59    Proof: Our φ equals Mathlib's golden ratio, which is proven irrational
  60    via the irrationality of √5 (5 is prime, hence not a perfect square). -/

used by (23)

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

depends on (14)

Lean names referenced from this declaration's body.