---

Step * of Lemma derivative-const-mul

∀a:ℝ. ∀I:Interval. ∀f,g:I ⟶ℝ.  (d(f[x])/dx = λx.g[x] on I ⇒ d(a * f[x])/dx = λx.a * g[x] on I)
BY
{ (Auto
   THEN ((D 0 THEN Auto)
         THEN (InstLemma `r-bound-property` [⌜a⌝]⋅ THENA Auto)
         THEN (With ⌜r-bound(a) * k⌝ (D 5)⋅ THENA Auto)
         THEN (With ⌜n⌝ (D (-1))⋅ THEN Auto)
         THEN ParallelLast
         THEN ∀h:hyp. (FLemma `i-member-approx` [h] THEN Complete (Auto)) 
         THEN RepeatFor 6 ((ParallelLast' THENA 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|)
⊢ |(a * f[y]) - a * f[x] - (a * g[x]) * (y - x)| ≤ ((r1/r(k)) * |y - x|)

---

Latex:

---

Latex:
\mforall{}a:\mBbbR{}.  \mforall{}I:Interval.  \mforall{}f,g:I  {}\mrightarrow{}\mBbbR{}.    (d(f[x])/dx  =  \mlambda{}x.g[x]  on  I  {}\mRightarrow{}  d(a  *  f[x])/dx  =  \mlambda{}x.a  *  g[x]  on  I)


By

---

Latex:
(Auto
  THEN  ((D  0  THEN  Auto)
              THEN  (InstLemma  `r-bound-property`  [\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (With  \mkleeneopen{}r-bound(a)  *  k\mkleeneclose{}  (D  5)\mcdot{}  THENA  Auto)
              THEN  (With  \mkleeneopen{}n\mkleeneclose{}  (D  (-1))\mcdot{}  THEN  Auto)
              THEN  ParallelLast
              THEN  \mforall{}h:hyp.  (FLemma  `i-member-approx`  [h]  THEN  Complete  (Auto)) 
              THEN  RepeatFor  6  ((ParallelLast'  THENA  Auto)))
  )

---

Home Index