---

Step * 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|)
⊢ |(a * f[y]) - a * f[x] - (a * g[x]) * (y - x)| ≤ ((r1/r(k)) * |y - x|)
BY
{ Assert ⌜((a * f[y]) - a * f[x] - (a * g[x]) * (y - x)) = (a * (f[y] - f[x] - g[x] * (y - x)))⌝⋅ }

1
.....assertion..... 
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|)
⊢ ((a * f[y]) - a * f[x] - (a * g[x]) * (y - x)) = (a * (f[y] - f[x] - g[x] * (y - x)))

2
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)))
⊢ |(a * f[y]) - a * f[x] - (a * g[x]) * (y - x)| ≤ ((r1/r(k)) * |y - x|)

---

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|)
\mvdash{}  |(a  *  f[y])  -  a  *  f[x]  -  (a  *  g[x])  *  (y  -  x)|  \mleq{}  ((r1/r(k))  *  |y  -  x|)


By

---

Latex:
Assert  \mkleeneopen{}((a  *  f[y])  -  a  *  f[x]  -  (a  *  g[x])  *  (y  -  x))  =  (a  *  (f[y]  -  f[x]  -  g[x]  *  (y  -  x)))\mkleeneclose{}\mcdot{}

---

Home Index