---

Step * 1 of Lemma power-sum_functionality_wrt_le


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)
BY
{ ((Assert a[i] ≤ b[i] BY Auto) THEN Mul ⌜x^i⌝ (-1)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  m  :  \mBbbZ{}@i
2.  n  :  \mBbbN{}@i
3.  x  :  \mBbbN{}@i
4.  a  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}@i
5.  b  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}@i
6.  \mforall{}i:\mBbbN{}n.  (a[i]  \mleq{}  b[i])@i
7.  i  :  \mBbbN{}n@i
\mvdash{}  (a[i]  *  x\^{}i)  \mleq{}  (b[i]  *  x\^{}i)


By

---

Latex:
((Assert  a[i]  \mleq{}  b[i]  BY  Auto)  THEN  Mul  \mkleeneopen{}x\^{}i\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto)

---

Home Index