lemma proved tactic proof

`phi_pow_7_eq`

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

formal statement (Lean)

  57private lemma phi_pow_7_eq : phi ^ 7 = 13 * phi + 8 := by

proof body

Tactic-mode proof.

  58  have h6 := phi_sixth_eq
  59  have hsq := phi_sq_eq
  60  calc phi ^ 7 = phi * phi ^ 6 := by ring
  61    _ = phi * (8 * phi + 5) := by rw [h6]
  62    _ = 8 * phi ^ 2 + 5 * phi := by ring
  63    _ = 8 * (phi + 1) + 5 * phi := by rw [hsq]
  64    _ = 13 * phi + 8 := by ring
  65

used by (4)

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

phi_pow_11_eq in IndisputableMonolith.Masses.NumericalPredictions decl_use
phi_pow_7_gt_28 in IndisputableMonolith.Masses.NumericalPredictions decl_use
phi_pow_7_gt_29 in IndisputableMonolith.Masses.NumericalPredictions decl_use
phi_pow_7_lt_30 in IndisputableMonolith.Masses.NumericalPredictions decl_use

depends on (3)

Lean names referenced from this declaration's body.

phi_sixth_eq in IndisputableMonolith.Constants decl_use
phi_sq_eq in IndisputableMonolith.Constants decl_use
phi_sq_eq in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use