---

Step * 1 of Lemma rmul-nonzero-on


1. I : Interval
2. f : I ⟶ℝ
3. g : I ⟶ℝ
4. m : {m:ℕ+| icompact(i-approx(I;m))} 
5. c : ℝ
6. r0 < c
7. ∀x:ℝ. ((x ∈ i-approx(I;m)) ⇒ (c ≤ |g[x]|))
8. c1 : ℝ
9. r0 < c1
10. ∀x:ℝ. ((x ∈ i-approx(I;m)) ⇒ (c1 ≤ |f[x]|))
11. r0 < (c1 * c)
12. x : ℝ
13. x ∈ i-approx(I;m)
14. x ∈ I
15. c1 ≤ |f[x]|
16. c ≤ |g[x]|
⊢ (c1 * c) ≤ |f[x] * g[x]|
BY
{ ((RWO "rabs-rmul" 0 THENA Auto)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN (GenConclTerm ⌜|g[x]|⌝⋅ THENA Auto)
   THEN (GenConclTerm ⌜|f[x]|⌝⋅ THENA Auto)
   THEN Auto
   THEN RWO "-1 -2" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Interval
2.  f  :  I  {}\mrightarrow{}\mBbbR{}
3.  g  :  I  {}\mrightarrow{}\mBbbR{}
4.  m  :  \{m:\mBbbN{}\msupplus{}|  icompact(i-approx(I;m))\} 
5.  c  :  \mBbbR{}
6.  r0  <  c
7.  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  i-approx(I;m))  {}\mRightarrow{}  (c  \mleq{}  |g[x]|))
8.  c1  :  \mBbbR{}
9.  r0  <  c1
10.  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  i-approx(I;m))  {}\mRightarrow{}  (c1  \mleq{}  |f[x]|))
11.  r0  <  (c1  *  c)
12.  x  :  \mBbbR{}
13.  x  \mmember{}  i-approx(I;m)
14.  x  \mmember{}  I
15.  c1  \mleq{}  |f[x]|
16.  c  \mleq{}  |g[x]|
\mvdash{}  (c1  *  c)  \mleq{}  |f[x]  *  g[x]|


By

---

Latex:
((RWO  "rabs-rmul"  0  THENA  Auto)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  (GenConclTerm  \mkleeneopen{}|g[x]|\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}|f[x]|\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Auto
  THEN  RWO  "-1  -2"  0
  THEN  Auto)

---

Home Index