---

Step * 1 1 of Lemma imonomial-nonneg-lemma


1. k : ℕ+
2. <k, []> ∈ iMonomial()
3. m : iMonomial()
4. m' : iMonomial()
5. mul-monomials(m';m') = mul-monomials(m;<k, []>) ∈ iMonomial()
6. f : ℤ ⟶ ℝ
7. imonomial-term(mul-monomials(m;<k, []>)) ≡ imonomial-term(m') (*) imonomial-term(m')
8. (real_term_value(f;imonomial-term(m')) * real_term_value(f;imonomial-term(m')))
= (real_term_value(f;imonomial-term(m)) * real_term_value(f;imonomial-term(<k, []>)))
⊢ r0 ≤ real_term_value(f;imonomial-term(m))
BY
{ (MoveToConcl (-1)
   THEN GenConclTerms Auto [⌜real_term_value(f;imonomial-term(m'))⌝;⌜real_term_value(f;imonomial-term(m))⌝]⋅
   THEN RepUR ``imonomial-term`` 0
   THEN All Thin
   THEN Auto) }

1
1. k : ℕ+
2. v : ℝ
3. v1 : ℝ
4. (v * v) = (v1 * r(k))
⊢ r0 ≤ v1

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  <k,  []>  \mmember{}  iMonomial()
3.  m  :  iMonomial()
4.  m'  :  iMonomial()
5.  mul-monomials(m';m')  =  mul-monomials(m;<k,  []>)
6.  f  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbR{}
7.  imonomial-term(mul-monomials(m;<k,  []>))  \mequiv{}  imonomial-term(m')  (*)  imonomial-term(m')
8.  (real\_term\_value(f;imonomial-term(m'))  *  real\_term\_value(f;imonomial-term(m')))
=  (real\_term\_value(f;imonomial-term(m))  *  real\_term\_value(f;imonomial-term(<k,  []>)))
\mvdash{}  r0  \mleq{}  real\_term\_value(f;imonomial-term(m))


By

---

Latex:
(MoveToConcl  (-1)
  THEN  GenConclTerms  Auto  [\mkleeneopen{}real\_term\_value(f;imonomial-term(m'))\mkleeneclose{};
  \mkleeneopen{}real\_term\_value(f;imonomial-term(m))\mkleeneclose{}]\mcdot{}
  THEN  RepUR  ``imonomial-term``  0
  THEN  All  Thin
  THEN  Auto)

---

Home Index