---

Step * of Lemma power-sum_functionality_wrt_le

∀m:ℤ. ∀n,x:ℕ. ∀a,b:ℕn ⟶ ℤ.  ((∀i:ℕn. (a[i] ≤ b[i])) ⇒ (Σi<n.a[i]*x^i ≤ Σi<n.b[i]*x^i))
BY
{ ((Auto THEN Unfold `power-sum` 0) THEN BLemma `sum_le` THEN Auto) }

1
1. m : ℤ@i
2. n : ℕ@i
3. x : ℕ@i
4. a : ℕn ⟶ ℤ@i
5. b : ℕn ⟶ ℤ@i
6. ∀i:ℕn. (a[i] ≤ b[i])@i
7. i : ℕn@i
⊢ (a[i] * x^i) ≤ (b[i] * x^i)

---

Latex:

---

Latex:
\mforall{}m:\mBbbZ{}.  \mforall{}n,x:\mBbbN{}.  \mforall{}a,b:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}.    ((\mforall{}i:\mBbbN{}n.  (a[i]  \mleq{}  b[i]))  {}\mRightarrow{}  (\mSigma{}i<n.a[i]*x\^{}i  \mleq{}  \mSigma{}i<n.b[i]*x\^{}i))


By

---

Latex:
((Auto  THEN  Unfold  `power-sum`  0)  THEN  BLemma  `sum\_le`  THEN  Auto)

---

Home Index