---

Step * of Lemma derivative-mul-part1

∀I:Interval
  (True
  ⇒ (∀f1,f2,g1,g2:I ⟶ℝ.
        (f1(x) (proper)continuous for x ∈ I
        ⇒ f2(x) (proper)continuous for x ∈ I
        ⇒ g2(x) (proper)continuous for x ∈ I
        ⇒ d(f1[x])/dx = λx.g1[x] on I
        ⇒ d(f2[x])/dx = λx.g2[x] on I
        ⇒ d(f1[x] * f2[x])/dx = λx.(f1[x] * g2[x]) + (f2[x] * g1[x]) on I)))
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN (Assert i-approx(I;n) ⊆ I  BY
               Auto)
   THEN (Assert icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n)) BY
               (DVar `n' THEN Unhide THEN Auto))
   THEN Assert ⌜∃M:ℕ+. ∀x:{x:ℝ| x ∈ i-approx(I;n)} . ((|f1(x)| ≤ r(M)) ∧ (|f2(x)| ≤ r(M)) ∧ (|g2(x)| ≤ r(M)))⌝⋅) }

1
.....assertion..... 
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))
⊢ ∃M:ℕ+. ∀x:{x:ℝ| x ∈ i-approx(I;n)} . ((|f1(x)| ≤ r(M)) ∧ (|f2(x)| ≤ r(M)) ∧ (|g2(x)| ≤ r(M)))

2
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|)))))}

---

Latex:

---

Latex:
\mforall{}I:Interval
    (True
    {}\mRightarrow{}  (\mforall{}f1,f2,g1,g2:I  {}\mrightarrow{}\mBbbR{}.
                (f1(x)  (proper)continuous  for  x  \mmember{}  I
                {}\mRightarrow{}  f2(x)  (proper)continuous  for  x  \mmember{}  I
                {}\mRightarrow{}  g2(x)  (proper)continuous  for  x  \mmember{}  I
                {}\mRightarrow{}  d(f1[x])/dx  =  \mlambda{}x.g1[x]  on  I
                {}\mRightarrow{}  d(f2[x])/dx  =  \mlambda{}x.g2[x]  on  I
                {}\mRightarrow{}  d(f1[x]  *  f2[x])/dx  =  \mlambda{}x.(f1[x]  *  g2[x])  +  (f2[x]  *  g1[x])  on  I)))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  (Assert  i-approx(I;n)  \msubseteq{}  I    BY
                          Auto)
  THEN  (Assert  icompact(i-approx(I;n))  \mwedge{}  iproper(i-approx(I;n))  BY
                          (DVar  `n'  THEN  Unhide  THEN  Auto))
  THEN  Assert  \mkleeneopen{}\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)))\mkleeneclose{}\mcdot{})

---

Home Index