---

Step * 1 2 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)))
⊢ |(a * f[y]) - a * f[x] - (a * g[x]) * (y - x)| ≤ ((r1/r(k)) * |y - x|)
BY
{ ((Assert x ∈ I BY
          ∀h:hyp. (FLemma `i-member-approx` [h] THEN Complete (Auto)) )
   THEN (Assert y ∈ I BY
               ∀h:hyp. (FLemma `i-member-approx` [h] THEN Complete (Auto)) )
   ) }

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


By

---

Latex:
((Assert  x  \mmember{}  I  BY
                \mforall{}h:hyp.  (FLemma  `i-member-approx`  [h]  THEN  Complete  (Auto))  )
  THEN  (Assert  y  \mmember{}  I  BY
                          \mforall{}h:hyp.  (FLemma  `i-member-approx`  [h]  THEN  Complete  (Auto))  )
  )

---

Home Index