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

phi_inv

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)

  91theorem phi_inv : 1 / φ = φ - 1 := by

proof body

Tactic-mode proof.

  92  have hsq : φ ^ 2 = φ + 1 := Constants.phi_sq_eq
  93  have hpos : 0 < φ := Constants.phi_pos
  94  have hne : φ ≠ 0 := hpos.ne'
  95  have hmul : φ * (φ - 1) = 1 := by
  96    calc
  97      φ * (φ - 1) = φ ^ 2 - φ := by ring
  98      _ = (φ + 1) - φ := by simp [hsq]
  99      _ = 1 := by ring
 100  have hdiv : φ - 1 = 1 / φ := by
 101    apply (eq_div_iff hne).2
 102    simpa [mul_comm, mul_left_comm, mul_assoc] using hmul
 103  exact hdiv.symm
 104
 105/-- φ² = φ + 1 (the defining equation) -/

used by (15)

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

depends on (6)

Lean names referenced from this declaration's body.