---

Step * of Lemma power-sum-linear

∀[n:ℕ]. ∀[x:ℤ]. ∀[a,b:ℕn ⟶ ℤ]. ∀[c,d:ℤ].
  (Σi<n.(c * a[i]) + (d * b[i])*x^i = ((c * Σi<n.a[i]*x^i) + (d * Σi<n.b[i]*x^i)) ∈ ℤ)
BY
{ xxx(Auto THEN Unfold `power-sum` 0)xxx }

1
1. n : ℕ
2. x : ℤ
3. a : ℕn ⟶ ℤ
4. b : ℕn ⟶ ℤ
5. c : ℤ
6. d : ℤ
⊢ Σ(((c * a[i]) + (d * b[i])) * x^i | i < n) = ((c * Σ(a[i] * x^i | i < n)) + (d * Σ(b[i] * x^i | i < n))) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x:\mBbbZ{}].  \mforall{}[a,b:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[c,d:\mBbbZ{}].
    (\mSigma{}i<n.(c  *  a[i])  +  (d  *  b[i])*x\^{}i  =  ((c  *  \mSigma{}i<n.a[i]*x\^{}i)  +  (d  *  \mSigma{}i<n.b[i]*x\^{}i)))


By

---

Latex:
xxx(Auto  THEN  Unfold  `power-sum`  0)xxx

---

Home Index