theorem proved term proof

`one_sub_phi_inv_eq_phi_inv_sq`

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

formal statement (Lean)

  50theorem one_sub_phi_inv_eq_phi_inv_sq : 1 - phi⁻¹ = phi⁻¹ ^ 2 := by

proof body

Term-mode proof.

  51  have hphi : phi ≠ 0 := phi_ne_zero
  52  have hphi_sq : phi ^ 2 = phi + 1 := phi_sq_eq
  53  field_simp [hphi]
  54  nlinarith [sq_pos_of_pos phi_pos, hphi_sq]
  55
  56/-- The two band boundaries sum to one. -/

depends on (11)

Lean names referenced from this declaration's body.

phi_ne_zero in IndisputableMonolith.Constants decl_use
phi_sq_eq in IndisputableMonolith.Constants decl_use
one in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
band in IndisputableMonolith.Foundation.PreLogicalCost decl_use
one in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
phi_ne_zero in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
phi_sq_eq in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
phi_ne_zero in IndisputableMonolith.PhiSupport.Lemmas decl_use
one in IndisputableMonolith.QFT.SpinStatistics decl_use
two in IndisputableMonolith.QFT.SpinStatistics decl_use
one in IndisputableMonolith.RecogSpec.Core decl_use