---

Step * of Lemma continuous-mul

∀I:Interval. ∀f,g:I ⟶ℝ.  (f[x] continuous for x ∈ I ⇒ g[x] continuous for x ∈ I ⇒ f[x] * g[x] continuous for x ∈ I)
BY
{ (Auto
   THEN (Assert rmax(|f[x]|;|g[x]|) continuous for x ∈ I BY
               (ProveRealContinuous THEN Auto))
   THEN PromoteHyp (-1) 4
   THEN D 0
   THEN Auto
   THEN RepeatFor 2 ((With ⌜m⌝ (D 5)⋅ THENA Auto))
   THEN Assert ⌜∃N:ℕ+. ∀[x:{r:ℝ| r ∈ i-approx(I;m)} ]. (rmax(|f[x]|;|g[x]|) ≤ r(N))⌝⋅) }

1
.....assertion..... 
1. I : Interval
2. f : I ⟶ℝ
3. g : I ⟶ℝ
4. rmax(|f[x]|;|g[x]|) continuous for x ∈ I
5. m : {m:ℕ+| icompact(i-approx(I;m))} 
6. n : ℕ+
7. ∀n:ℕ+
     (∃d:{ℝ| ((r0 < d)
             ∧ (∀x,y:ℝ.
                  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(n))))))})
8. ∀n:ℕ+
     (∃d:{ℝ| ((r0 < d)
             ∧ (∀x,y:ℝ.
                  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|g[x] - g[y]| ≤ (r1/r(n))))))})
⊢ ∃N:ℕ+. ∀[x:{r:ℝ| r ∈ i-approx(I;m)} ]. (rmax(|f[x]|;|g[x]|) ≤ r(N))

2
1. I : Interval
2. f : I ⟶ℝ
3. g : I ⟶ℝ
4. rmax(|f[x]|;|g[x]|) continuous for x ∈ I
5. m : {m:ℕ+| icompact(i-approx(I;m))} 
6. n : ℕ+
7. ∀n:ℕ+
     (∃d:{ℝ| ((r0 < d)
             ∧ (∀x,y:ℝ.
                  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(n))))))})
8. ∀n:ℕ+
     (∃d:{ℝ| ((r0 < d)
             ∧ (∀x,y:ℝ.
                  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|g[x] - g[y]| ≤ (r1/r(n))))))})
9. ∃N:ℕ+. ∀[x:{r:ℝ| r ∈ i-approx(I;m)} ]. (rmax(|f[x]|;|g[x]|) ≤ r(N))
⊢ ∃d:{ℝ| ((r0 < d)
         ∧ (∀x,y:ℝ.
              ((x ∈ i-approx(I;m))
              ⇒ (y ∈ i-approx(I;m))
              ⇒ (|x - y| ≤ d)
              ⇒ (|(f[x] * g[x]) - f[y] * g[y]| ≤ (r1/r(n))))))}

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}f,g:I  {}\mrightarrow{}\mBbbR{}.
    (f[x]  continuous  for  x  \mmember{}  I  {}\mRightarrow{}  g[x]  continuous  for  x  \mmember{}  I  {}\mRightarrow{}  f[x]  *  g[x]  continuous  for  x  \mmember{}  I)


By

---

Latex:
(Auto
  THEN  (Assert  rmax(|f[x]|;|g[x]|)  continuous  for  x  \mmember{}  I  BY
                          (ProveRealContinuous  THEN  Auto))
  THEN  PromoteHyp  (-1)  4
  THEN  D  0
  THEN  Auto
  THEN  RepeatFor  2  ((With  \mkleeneopen{}m\mkleeneclose{}  (D  5)\mcdot{}  THENA  Auto))
  THEN  Assert  \mkleeneopen{}\mexists{}N:\mBbbN{}\msupplus{}.  \mforall{}[x:\{r:\mBbbR{}|  r  \mmember{}  i-approx(I;m)\}  ].  (rmax(|f[x]|;|g[x]|)  \mleq{}  r(N))\mkleeneclose{}\mcdot{})

---

Home Index