---

Step * of Lemma imonomial-nonneg-lemma

∀[k:ℕ+]. ∀[m,m':iMonomial()].
  ∀f:ℤ ⟶ ℝ. (r0 ≤ real_term_value(f;imonomial-term(m))) supposing mul-monomials(m';m') = mul-monomials(m;<k, []>) ∈ iMo\000Cnomial()
BY
{ ((D 0 THENA Auto)
   THEN (Assert <k, []> ∈ iMonomial() BY
               (Auto THEN MemTypeCD THEN Auto THEN D 0 THEN Reduce 0 THEN Auto))
   THEN Auto) }

1
1. k : ℕ+
2. <k, []> ∈ iMonomial()
3. m : iMonomial()
4. m' : iMonomial()
5. mul-monomials(m';m') = mul-monomials(m;<k, []>) ∈ iMonomial()
6. f : ℤ ⟶ ℝ
⊢ r0 ≤ real_term_value(f;imonomial-term(m))

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}\msupplus{}].  \mforall{}[m,m':iMonomial()].
    \mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbR{}.  (r0  \mleq{}  real\_term\_value(f;imonomial-term(m))) 
    supposing  mul-monomials(m';m')  =  mul-monomials(m;<k,  []>)


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (Assert  <k,  []>  \mmember{}  iMonomial()  BY
                          (Auto  THEN  MemTypeCD  THEN  Auto  THEN  D  0  THEN  Reduce  0  THEN  Auto))
  THEN  Auto)

---

Home Index