---

Step * 1 1 of Lemma derivative-const-mul

.....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)))
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)) )
   THEN (GenConclTerm ⌜f[y]⌝⋅ THENA Auto)
   THEN (GenConclTerm ⌜f[x]⌝⋅ THENA Auto)
   THEN (GenConclTerm ⌜g[x]⌝⋅ THENA Auto)
   THEN All Thin) }

1
1. a : ℝ
2. x : ℝ
3. y : ℝ
4. v : ℝ
5. v1 : ℝ
6. v2 : ℝ
⊢ ((a * v) - a * v1 - (a * v2) * (y - x)) = (a * (v - v1 - v2 * (y - x)))

---

Latex:

---

Latex:
.....assertion..... 
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))  =  (a  *  (f[y]  -  f[x]  -  g[x]  *  (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))  )
  THEN  (GenConclTerm  \mkleeneopen{}f[y]\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}f[x]\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}g[x]\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin)

---

Home Index