---

Step * 2 1 2 1 of Lemma continuous-mul


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 : ℕ+
8. ∀[x:{r:ℝ| r ∈ i-approx(I;m)} ]. (rmax(|f[x]|;|g[x]|) ≤ r(N))
9. f ∈ i-approx(I;m) ⟶ℝ
10. g ∈ i-approx(I;m) ⟶ℝ
11. d : ℝ
12. r0 < d
13. ∀x,y:ℝ.  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r((2 * n) * N))))
14. d1 : ℝ
15. r0 < d1
16. ∀x,y:ℝ.  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d1) ⇒ (|g[x] - g[y]| ≤ (r1/r((2 * n) * N))))
17. r0 < rmin(d;d1)
18. x : ℝ
19. y : ℝ
20. x ∈ i-approx(I;m)
21. y ∈ i-approx(I;m)
22. |x - y| ≤ rmin(d;d1)
⊢ (|(f[x] * g[x]) - f[x] * g[y]| + |(f[x] * g[y]) - f[y] * g[y]|) ≤ (r1/r(n))
BY
{ 
((Assert r0 ≤ |g[y]| BY
        Auto)
 THEN (Assert (|f[x] - f[y]| * |g[y]|) ≤ ((r1/r((2 * n) * N)) * |g[y]|) BY
             (BLemma `rmul_functionality_wrt_rleq` THEN Auto THEN BackThruSomeHyp THEN Auto THEN RWO "-2" 0 THEN Auto))
 THEN (Assert r0 ≤ |f[x]| BY
             Auto)
 THEN (Assert (|g[x] - g[y]| * |f[x]|) ≤ ((r1/r((2 * n) * N)) * |f[x]|) BY
             (BLemma `rmul_functionality_wrt_rleq` THEN Auto THEN BackThruSomeHyp THEN Auto THEN RWO "-4" 0 THEN Auto))
 THEN ((RWO "rabs-rmul<" (-1) THENA Auto)
       THEN (RWO "rabs-rmul<" (-3) THENA Auto)
       THEN (RWO "rmul-rsub-distrib.1< rmul-rsub-distrib.2<" 0⋅ THENA Auto))⋅)⋅ }

1
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 : ℕ+
8. ∀[x:{r:ℝ| r ∈ i-approx(I;m)} ]. (rmax(|f[x]|;|g[x]|) ≤ r(N))
9. f ∈ i-approx(I;m) ⟶ℝ
10. g ∈ i-approx(I;m) ⟶ℝ
11. d : ℝ
12. r0 < d
13. ∀x,y:ℝ.  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r((2 * n) * N))))
14. d1 : ℝ
15. r0 < d1
16. ∀x,y:ℝ.  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d1) ⇒ (|g[x] - g[y]| ≤ (r1/r((2 * n) * N))))
17. r0 < rmin(d;d1)
18. x : ℝ
19. y : ℝ
20. x ∈ i-approx(I;m)
21. y ∈ i-approx(I;m)
22. |x - y| ≤ rmin(d;d1)
23. r0 ≤ |g[y]|
24. |(f[x] - f[y]) * g[y]| ≤ ((r1/r((2 * n) * N)) * |g[y]|)
25. r0 ≤ |f[x]|
26. |(g[x] - g[y]) * f[x]| ≤ ((r1/r((2 * n) * N)) * |f[x]|)
⊢ (|f[x] * (g[x] - g[y])| + |(f[x] - f[y]) * g[y]|) ≤ (r1/r(n))

---

Latex:

---

Latex:

1.  I  :  Interval
2.  f  :  I  {}\mrightarrow{}\mBbbR{}
3.  g  :  I  {}\mrightarrow{}\mBbbR{}
4.  rmax(|f[x]|;|g[x]|)  continuous  for  x  \mmember{}  I
5.  m  :  \{m:\mBbbN{}\msupplus{}|  icompact(i-approx(I;m))\} 
6.  n  :  \mBbbN{}\msupplus{}
7.  N  :  \mBbbN{}\msupplus{}
8.  \mforall{}[x:\{r:\mBbbR{}|  r  \mmember{}  i-approx(I;m)\}  ].  (rmax(|f[x]|;|g[x]|)  \mleq{}  r(N))
9.  f  \mmember{}  i-approx(I;m)  {}\mrightarrow{}\mBbbR{}
10.  g  \mmember{}  i-approx(I;m)  {}\mrightarrow{}\mBbbR{}
11.  d  :  \mBbbR{}
12.  r0  <  d
13.  \mforall{}x,y:\mBbbR{}.
            ((x  \mmember{}  i-approx(I;m))
            {}\mRightarrow{}  (y  \mmember{}  i-approx(I;m))
            {}\mRightarrow{}  (|x  -  y|  \mleq{}  d)
            {}\mRightarrow{}  (|f[x]  -  f[y]|  \mleq{}  (r1/r((2  *  n)  *  N))))
14.  d1  :  \mBbbR{}
15.  r0  <  d1
16.  \mforall{}x,y:\mBbbR{}.
            ((x  \mmember{}  i-approx(I;m))
            {}\mRightarrow{}  (y  \mmember{}  i-approx(I;m))
            {}\mRightarrow{}  (|x  -  y|  \mleq{}  d1)
            {}\mRightarrow{}  (|g[x]  -  g[y]|  \mleq{}  (r1/r((2  *  n)  *  N))))
17.  r0  <  rmin(d;d1)
18.  x  :  \mBbbR{}
19.  y  :  \mBbbR{}
20.  x  \mmember{}  i-approx(I;m)
21.  y  \mmember{}  i-approx(I;m)
22.  |x  -  y|  \mleq{}  rmin(d;d1)
\mvdash{}  (|(f[x]  *  g[x])  -  f[x]  *  g[y]|  +  |(f[x]  *  g[y])  -  f[y]  *  g[y]|)  \mleq{}  (r1/r(n))


By

---

Latex:
((Assert  r0  \mleq{}  |g[y]|  BY
                Auto)
  THEN  (Assert  (|f[x]  -  f[y]|  *  |g[y]|)  \mleq{}  ((r1/r((2  *  n)  *  N))  *  |g[y]|)  BY
                          (BLemma  `rmul\_functionality\_wrt\_rleq`
                            THEN  Auto
                            THEN  BackThruSomeHyp
                            THEN  Auto
                            THEN  RWO  "-2"  0
                            THEN  Auto))
  THEN  (Assert  r0  \mleq{}  |f[x]|  BY
                          Auto)
  THEN  (Assert  (|g[x]  -  g[y]|  *  |f[x]|)  \mleq{}  ((r1/r((2  *  n)  *  N))  *  |f[x]|)  BY
                          (BLemma  `rmul\_functionality\_wrt\_rleq`
                            THEN  Auto
                            THEN  BackThruSomeHyp
                            THEN  Auto
                            THEN  RWO  "-4"  0
                            THEN  Auto))
  THEN  ((RWO  "rabs-rmul<"  (-1)  THENA  Auto)
              THEN  (RWO  "rabs-rmul<"  (-3)  THENA  Auto)
              THEN  (RWO  "rmul-rsub-distrib.1<  rmul-rsub-distrib.2<"  0\mcdot{}  THENA  Auto))\mcdot{})\mcdot{}

---

Home Index