---

Step * 2 of Lemma derivative-mul-part1


1. I : Interval
2. True
3. f1 : I ⟶ℝ
4. f2 : I ⟶ℝ
5. g1 : I ⟶ℝ
6. g2 : I ⟶ℝ
7. f1(x) (proper)continuous for x ∈ I
8. f2(x) (proper)continuous for x ∈ I
9. g2(x) (proper)continuous for x ∈ I
10. d(f1[x])/dx = λx.g1[x] on I
11. d(f2[x])/dx = λx.g2[x] on I
12. k : ℕ+
13. n : {n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))} 
14. i-approx(I;n) ⊆ I 
15. icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))
16. ∃M:ℕ+. ∀x:{x:ℝ| x ∈ i-approx(I;n)} . ((|f1(x)| ≤ r(M)) ∧ (|f2(x)| ≤ r(M)) ∧ (|g2(x)| ≤ r(M)))
⊢ ∃del:{ℝ| ((r0 < del)
           ∧ (∀x,y:ℝ.
                ((x ∈ i-approx(I;n))
                ⇒ (y ∈ i-approx(I;n))
                ⇒ (|y - x| ≤ del)
                ⇒ (|(f1[y] * f2[y]) - f1[x] * f2[x] - ((f1[x] * g2[x]) + (f2[x] * g1[x])) * (y - x)| ≤ ((r1/r(k))
                   * |y - x|)))))}
BY
{ (D (-1)
   THEN ∀h:hyp. (Unfold `derivative` h THEN (InstHyp [⌜(3 * M) * k⌝;⌜n⌝] h⋅ THENA Auto) THEN Thin h THEN D -1) 
   THEN Unfold `proper-continuous` 7
   THEN (InstHyp [⌜n⌝;⌜(3 * M) * k⌝] 7⋅ THENA Auto)
   THEN D -1) }

1
1. I : Interval
2. True
3. f1 : I ⟶ℝ
4. f2 : I ⟶ℝ
5. g1 : I ⟶ℝ
6. g2 : I ⟶ℝ
7. ∀m:{m:ℕ+| icompact(i-approx(I;m)) ∧ iproper(i-approx(I;m))} . ∀n:ℕ+.
     (∃d:{ℝ| ((r0 < d)
             ∧ (∀x,y:ℝ.
                  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|f1(x) - f1(y)| ≤ (r1/r(n))))))})
8. f2(x) (proper)continuous for x ∈ I
9. g2(x) (proper)continuous for x ∈ I
10. k : ℕ+
11. n : {n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))} 
12. i-approx(I;n) ⊆ I 
13. icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))
14. M : ℕ+
15. ∀x:{x:ℝ| x ∈ i-approx(I;n)} . ((|f1(x)| ≤ r(M)) ∧ (|f2(x)| ≤ r(M)) ∧ (|g2(x)| ≤ r(M)))
16. del : ℝ
17. [%14] : (r0 < del)
∧ (∀x,y:ℝ.
     ((x ∈ i-approx(I;n))
     ⇒ (y ∈ i-approx(I;n))
     ⇒ (|y - x| ≤ del)
     ⇒ (|f2[y] - f2[x] - g2[x] * (y - x)| ≤ ((r1/r((3 * M) * k)) * |y - x|))))
18. d1 : ℝ
19. [%19] : (r0 < d1)
∧ (∀x,y:ℝ.
     ((x ∈ i-approx(I;n))
     ⇒ (y ∈ i-approx(I;n))
     ⇒ (|y - x| ≤ d1)
     ⇒ (|f1[y] - f1[x] - g1[x] * (y - x)| ≤ ((r1/r((3 * M) * k)) * |y - x|))))
20. d : ℝ
21. [%24] : (r0 < d)
∧ (∀x,y:ℝ.  ((x ∈ i-approx(I;n)) ⇒ (y ∈ i-approx(I;n)) ⇒ (|x - y| ≤ d) ⇒ (|f1(x) - f1(y)| ≤ (r1/r((3 * M) * k)))))
⊢ ∃del:{ℝ| ((r0 < del)
           ∧ (∀x,y:ℝ.
                ((x ∈ i-approx(I;n))
                ⇒ (y ∈ i-approx(I;n))
                ⇒ (|y - x| ≤ del)
                ⇒ (|(f1[y] * f2[y]) - f1[x] * f2[x] - ((f1[x] * g2[x]) + (f2[x] * g1[x])) * (y - x)| ≤ ((r1/r(k))
                   * |y - x|)))))}

---

Latex:

---

Latex:

1.  I  :  Interval
2.  True
3.  f1  :  I  {}\mrightarrow{}\mBbbR{}
4.  f2  :  I  {}\mrightarrow{}\mBbbR{}
5.  g1  :  I  {}\mrightarrow{}\mBbbR{}
6.  g2  :  I  {}\mrightarrow{}\mBbbR{}
7.  f1(x)  (proper)continuous  for  x  \mmember{}  I
8.  f2(x)  (proper)continuous  for  x  \mmember{}  I
9.  g2(x)  (proper)continuous  for  x  \mmember{}  I
10.  d(f1[x])/dx  =  \mlambda{}x.g1[x]  on  I
11.  d(f2[x])/dx  =  \mlambda{}x.g2[x]  on  I
12.  k  :  \mBbbN{}\msupplus{}
13.  n  :  \{n:\mBbbN{}\msupplus{}|  icompact(i-approx(I;n))  \mwedge{}  iproper(i-approx(I;n))\} 
14.  i-approx(I;n)  \msubseteq{}  I 
15.  icompact(i-approx(I;n))  \mwedge{}  iproper(i-approx(I;n))
16.  \mexists{}M:\mBbbN{}\msupplus{}.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  i-approx(I;n)\}  .  ((|f1(x)|  \mleq{}  r(M))  \mwedge{}  (|f2(x)|  \mleq{}  r(M))  \mwedge{}  (|g2(x)|  \mleq{}  r(M)))
\mvdash{}  \mexists{}del:\{\mBbbR{}|  ((r0  <  del)
                      \mwedge{}  (\mforall{}x,y:\mBbbR{}.
                                ((x  \mmember{}  i-approx(I;n))
                                {}\mRightarrow{}  (y  \mmember{}  i-approx(I;n))
                                {}\mRightarrow{}  (|y  -  x|  \mleq{}  del)
                                {}\mRightarrow{}  (|(f1[y]  *  f2[y])  -  f1[x]  *  f2[x]  -  ((f1[x]  *  g2[x])  +  (f2[x]  *  g1[x]))
                                      *  (y  -  x)|  \mleq{}  ((r1/r(k))  *  |y  -  x|)))))\}


By

---

Latex:
(D  (-1)
  THEN  \mforall{}h:hyp.  (Unfold  `derivative`  h
                              THEN  (InstHyp  [\mkleeneopen{}(3  *  M)  *  k\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]  h\mcdot{}  THENA  Auto)
                              THEN  Thin  h
                              THEN  D  -1) 
  THEN  Unfold  `proper-continuous`  7
  THEN  (InstHyp  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}(3  *  M)  *  k\mkleeneclose{}]  7\mcdot{}  THENA  Auto)
  THEN  D  -1)

---

Home Index