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

phi_in_phiInterval

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)

  56theorem phi_in_phiInterval : phiInterval.contains ((1 + Real.sqrt 5) / 2) := by

proof body

Tactic-mode proof.

  57  simp only [Interval.contains, phiInterval]
  58  constructor
  59  · have h := phi_gt_1618
  60    have h1 : ((1618 / 1000 : ℚ) : ℝ) < (1 + Real.sqrt 5) / 2 := by
  61      calc ((1618 / 1000 : ℚ) : ℝ) = (1.618 : ℝ) := by norm_num
  62        _ < (1 + Real.sqrt 5) / 2 := h
  63    exact le_of_lt h1
  64  · have h := phi_lt_16185
  65    have h1 : (1 + Real.sqrt 5) / 2 < ((1619 / 1000 : ℚ) : ℝ) := by
  66      calc (1 + Real.sqrt 5) / 2 < (1.6185 : ℝ) := h
  67        _ < (1.619 : ℝ) := by norm_num
  68        _ = ((1619 / 1000 : ℚ) : ℝ) := by norm_num
  69    exact le_of_lt h1
  70
  71/-- φ = (1 + √5)/2 (Mathlib definition) -/

used by (5)

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

depends on (9)

Lean names referenced from this declaration's body.