---

Step * of Lemma ipolynomial-nonneg

∀[p:iPolynomial()]. ∀f:ℤ ⟶ ℝ. (r0 ≤ real_term_value(f;ipolynomial-term(p))) supposing ↑nonneg-poly(p)
BY
{ (Auto THEN (RWO  "assert-nonneg-poly" (-2) THENA Auto) THEN D 1 THEN Thin 2 THEN ListInd 1) }

1
1. f : ℤ ⟶ ℝ
⊢ (∀m∈[].↑nonneg-monomial(m)) ⇒ (r0 ≤ real_term_value(f;ipolynomial-term([])))

2
1. f : ℤ ⟶ ℝ
2. u : iMonomial()
3. v : iMonomial() List
4. (∀m∈v.↑nonneg-monomial(m)) ⇒ (r0 ≤ real_term_value(f;ipolynomial-term(v)))
⊢ (∀m∈[u / v].↑nonneg-monomial(m)) ⇒ (r0 ≤ real_term_value(f;ipolynomial-term([u / v])))

---

Latex:

---

Latex:
\mforall{}[p:iPolynomial()]
    \mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbR{}.  (r0  \mleq{}  real\_term\_value(f;ipolynomial-term(p)))  supposing  \muparrow{}nonneg-poly(p)


By

---

Latex:
(Auto  THEN  (RWO    "assert-nonneg-poly"  (-2)  THENA  Auto)  THEN  D  1  THEN  Thin  2  THEN  ListInd  1)

---

Home Index