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

phiInvCubed_eq_two_phi_minus_three

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)

  69theorem phiInvCubed_eq_two_phi_minus_three : 1 / phi^3 = 2 * phi - 3 := by

proof body

Tactic-mode proof.

  70  have hpos : phi^3 ≠ 0 := ne_of_gt (pow_pos phi_pos 3)
  71  have hsq : phi^2 = phi + 1 := phi_sq_eq
  72  have h3 : phi^3 = 2 * phi + 1 := phi_cubed_eq
  73  have hkey : phi^3 * (2 * phi - 3) = 1 := by nlinarith [hsq, h3]
  74  rw [eq_comm, eq_div_iff hpos]
  75  linarith [hkey]
  76
  77/-! ## Domain instances. -/
  78
  79/-- Senolytic target ratio. -/

used by (1)

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.