---

Step * 1 of Lemma ipolynomial-nonneg


1. f : ℤ ⟶ ℝ
⊢ (∀m∈[].↑nonneg-monomial(m)) ⇒ (r0 ≤ real_term_value(f;ipolynomial-term([])))
BY
{ (RepUR ``ipolynomial-term`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbR{}
\mvdash{}  (\mforall{}m\mmember{}[].\muparrow{}nonneg-monomial(m))  {}\mRightarrow{}  (r0  \mleq{}  real\_term\_value(f;ipolynomial-term([])))


By

---

Latex:
(RepUR  ``ipolynomial-term``  0  THEN  Auto)

---

Home Index