lemma proved term proof

`phi_minus_one_abs_lt_one`

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

formal statement (Lean)

  96lemma phi_minus_one_abs_lt_one : |Real.goldenRatio - 1| < 1 := by

Term-mode proof.

  97  rw [phi_minus_one_abs]
  98  exact phi_sub_one_lt_one
  99
 100/-- Helper: ‖(x : ℂ)‖ = |x| for real x -/

Lean names referenced from this declaration's body.

for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
phi_minus_one_abs in IndisputableMonolith.Numerics.Interval.Log decl_use
phi_sub_one_lt_one in IndisputableMonolith.Numerics.Interval.PhiBounds decl_use