---

Step * of Lemma power-sum-split

No Annotations
∀[n:ℕ]. ∀[k:ℕn + 1]. ∀[x:ℤ]. ∀[a:ℕn ⟶ ℤ].  (Σi<n.a[i]*x^i = (Σi<k.a[i]*x^i + (x^k * Σi<n - k.a[k + i]*x^i)) ∈ ℤ)
BY
{ (Auto
   THEN Unfold `power-sum` 0
   THEN (InstLemma `sum_split` [⌜n⌝;⌜λ2i.a[i] * x^i⌝;⌜k⌝]⋅ THENA Auto)
   THEN NthHypSq (-1)
   THEN RepeatFor 2 ((EqCD THEN Try (Trivial)))
   THEN Auto
   THEN (RWO "sum_scalar_mult" 0 THENA Auto)
   THEN EqCD
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n:\mBbbN{}].  \mforall{}[k:\mBbbN{}n  +  1].  \mforall{}[x:\mBbbZ{}].  \mforall{}[a:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}].
    (\mSigma{}i<n.a[i]*x\^{}i  =  (\mSigma{}i<k.a[i]*x\^{}i  +  (x\^{}k  *  \mSigma{}i<n  -  k.a[k  +  i]*x\^{}i)))


By

---

Latex:
(Auto
  THEN  Unfold  `power-sum`  0
  THEN  (InstLemma  `sum\_split`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.a[i]  *  x\^{}i\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  NthHypSq  (-1)
  THEN  RepeatFor  2  ((EqCD  THEN  Try  (Trivial)))
  THEN  Auto
  THEN  (RWO  "sum\_scalar\_mult"  0  THENA  Auto)
  THEN  EqCD
  THEN  Auto)

---

Home Index