---

Step * 1 2 1 1 1 of Lemma derivative-const-mul


1. a : ℝ
2. I : Interval
3. f : I ⟶ℝ
4. g : I ⟶ℝ
5. k : ℕ+
6. n : {n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))} 
7. r(-r-bound(a)) ≤ a
8. a ≤ r(r-bound(a))
9. del : ℝ
10. r0 < del
11. x : ℝ
12. y : ℝ
13. x ∈ i-approx(I;n)
14. y ∈ i-approx(I;n)
15. |y - x| ≤ del
16. |f[y] - f[x] - g[x] * (y - x)| ≤ ((r1/r(r-bound(a) * k)) * |y - x|)
17. ((a * f[y]) - a * f[x] - (a * g[x]) * (y - x)) = (a * (f[y] - f[x] - g[x] * (y - x)))
18. x ∈ I
19. y ∈ I
20. |a| ≤ r(r-bound(a))
⊢ (|a| * |f[y] - f[x] - g[x] * (y - x)|) ≤ ((r1/r(k)) * |y - x|)
BY
{ (MoveToConcl (-1)
   THEN MoveToConcl (-4)
   THEN (GenConclTerm ⌜f[y] - f[x] - g[x] * (y - x)⌝⋅ THENA Auto)
   THEN (GenConclTerm  ⌜r-bound(a)⌝⋅ THENA Auto)
   THEN (GenConclTerm  ⌜y - x⌝⋅ THENA Auto)
   THEN All Thin) }

1
1. a : ℝ
2. k : ℕ+
3. v : ℝ
4. v1 : ℕ+
5. v2 : ℝ
⊢ (|v| ≤ ((r1/r(v1 * k)) * |v2|)) ⇒ (|a| ≤ r(v1)) ⇒ ((|a| * |v|) ≤ ((r1/r(k)) * |v2|))

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  I  :  Interval
3.  f  :  I  {}\mrightarrow{}\mBbbR{}
4.  g  :  I  {}\mrightarrow{}\mBbbR{}
5.  k  :  \mBbbN{}\msupplus{}
6.  n  :  \{n:\mBbbN{}\msupplus{}|  icompact(i-approx(I;n))  \mwedge{}  iproper(i-approx(I;n))\} 
7.  r(-r-bound(a))  \mleq{}  a
8.  a  \mleq{}  r(r-bound(a))
9.  del  :  \mBbbR{}
10.  r0  <  del
11.  x  :  \mBbbR{}
12.  y  :  \mBbbR{}
13.  x  \mmember{}  i-approx(I;n)
14.  y  \mmember{}  i-approx(I;n)
15.  |y  -  x|  \mleq{}  del
16.  |f[y]  -  f[x]  -  g[x]  *  (y  -  x)|  \mleq{}  ((r1/r(r-bound(a)  *  k))  *  |y  -  x|)
17.  ((a  *  f[y])  -  a  *  f[x]  -  (a  *  g[x])  *  (y  -  x))  =  (a  *  (f[y]  -  f[x]  -  g[x]  *  (y  -  x)))
18.  x  \mmember{}  I
19.  y  \mmember{}  I
20.  |a|  \mleq{}  r(r-bound(a))
\mvdash{}  (|a|  *  |f[y]  -  f[x]  -  g[x]  *  (y  -  x)|)  \mleq{}  ((r1/r(k))  *  |y  -  x|)


By

---

Latex:
(MoveToConcl  (-1)
  THEN  MoveToConcl  (-4)
  THEN  (GenConclTerm  \mkleeneopen{}f[y]  -  f[x]  -  g[x]  *  (y  -  x)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConclTerm    \mkleeneopen{}r-bound(a)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConclTerm    \mkleeneopen{}y  -  x\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin)

---

Home Index