phi_pow_11_eq

proof body

Tactic-mode proof.

  88  have hsq := phi_sq_eq
  89  have h6 := phi_sixth_eq
  90  have h7 := phi_pow_7_eq
  91  have h8 : phi ^ 8 = 21 * phi + 13 := by
  92    calc phi ^ 8 = phi * phi ^ 7 := by ring
  93      _ = phi * (13 * phi + 8) := by rw [h7]
  94      _ = 13 * phi ^ 2 + 8 * phi := by ring
  95      _ = 13 * (phi + 1) + 8 * phi := by rw [hsq]
  96      _ = 21 * phi + 13 := by ring
  97  have h9 : phi ^ 9 = 34 * phi + 21 := by
  98    calc phi ^ 9 = phi * phi ^ 8 := by ring
  99      _ = phi * (21 * phi + 13) := by rw [h8]
 100      _ = 21 * phi ^ 2 + 13 * phi := by ring
 101      _ = 21 * (phi + 1) + 13 * phi := by rw [hsq]
 102      _ = 34 * phi + 21 := by ring
 103  have h10 : phi ^ 10 = 55 * phi + 34 := by
 104    calc phi ^ 10 = phi * phi ^ 9 := by ring
 105      _ = phi * (34 * phi + 21) := by rw [h9]
 106      _ = 34 * phi ^ 2 + 21 * phi := by ring
 107      _ = 34 * (phi + 1) + 21 * phi := by rw [hsq]
 108      _ = 55 * phi + 34 := by ring
 109  calc phi ^ 11 = phi * phi ^ 10 := by ring
 110    _ = phi * (55 * phi + 34) := by rw [h10]
 111    _ = 55 * phi ^ 2 + 34 * phi := by ring
 112    _ = 55 * (phi + 1) + 34 * phi := by rw [hsq]
 113    _ = 89 * phi + 55 := by ring
 114