---

Step * 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 : ℤ ⟶ ℝ
⊢ r0 ≤ real_term_value(f;imonomial-term(m))
BY
{ ((InstLemma `mul-monomials-req` [⌜m'⌝;⌜m'⌝]⋅ THENA Auto)
   THEN (RWO  "-3" (-1) THENA Auto)
   THEN (InstLemma `mul-monomials-req` [⌜m⌝;⌜<k, []>⌝]⋅ THENA Auto)
   THEN (RWO "-2" (-1) THENA Auto)
   THEN (D -1 With ⌜f⌝  THENA Auto)
   THEN Reduce -1) }

1
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))

---

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{}
\mvdash{}  r0  \mleq{}  real\_term\_value(f;imonomial-term(m))


By

---

Latex:
((InstLemma  `mul-monomials-req`  [\mkleeneopen{}m'\mkleeneclose{};\mkleeneopen{}m'\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO    "-3"  (-1)  THENA  Auto)
  THEN  (InstLemma  `mul-monomials-req`  [\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}<k,  []>\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-2"  (-1)  THENA  Auto)
  THEN  (D  -1  With  \mkleeneopen{}f\mkleeneclose{}    THENA  Auto)
  THEN  Reduce  -1)

---

Home Index