---

Step * of Lemma real-term-nonneg

∀[t:int_term()]. ∀f:ℤ ⟶ ℝ. (r0 ≤ real_term_value(f;t)) supposing ↑nonneg-poly(int_term_to_ipoly(t))
BY
{ (Auto THEN InstLemma `ipolynomial-nonneg` [int_term_to_ipoly(t);⌜f⌝]⋅ THEN Auto) }

1
1. t : int_term()
2. ↑nonneg-poly(int_term_to_ipoly(t))
3. f : ℤ ⟶ ℝ
4. r0 ≤ real_term_value(f;ipolynomial-term(int_term_to_ipoly(t)))
⊢ r0 ≤ real_term_value(f;t)

---

Latex:

---

Latex:
\mforall{}[t:int\_term()].  \mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbR{}.  (r0  \mleq{}  real\_term\_value(f;t))  supposing  \muparrow{}nonneg-poly(int\_term\_to\_ipoly(t))


By

---

Latex:
(Auto  THEN  InstLemma  `ipolynomial-nonneg`  [int\_term\_to\_ipoly(t);\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index