---

Step * of Lemma derivative-add

∀[I:Interval]. ∀[f1,f2,g1,g2:I ⟶ℝ].
  (d(f1[x])/dx = λx.g1[x] on I ⇒ d(f2[x])/dx = λx.g2[x] on I ⇒ d(f1[x] + f2[x])/dx = λx.g1[x] + g2[x] on I)
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN ∀h:hyp. (Unfold `derivative` h THEN (InstHyp [⌜2 * k⌝;⌜n⌝] h⋅ THENA Auto) THEN Thin h THEN D -1) 
   THEN With ⌜rmin(del;d1)⌝ (D 0)⋅
   THEN Auto
   THEN ∀h:hyp. (FLemma `i-member-approx` [h] THEN Auto) 
   THEN EAuto 1⋅) }

1
1. I : Interval
2. f1 : I ⟶ℝ
3. f2 : I ⟶ℝ
4. g1 : I ⟶ℝ
5. g2 : I ⟶ℝ
6. k : ℕ+
7. n : {n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))} 
8. del : ℝ
9. r0 < del
10. ∀x,y:ℝ.
      ((x ∈ i-approx(I;n))
      ⇒ (y ∈ i-approx(I;n))
      ⇒ (|y - x| ≤ del)
      ⇒ (|f2[y] - f2[x] - g2[x] * (y - x)| ≤ ((r1/r(2 * k)) * |y - x|)))
11. d1 : ℝ
12. r0 < d1
13. ∀x,y:ℝ.
      ((x ∈ i-approx(I;n))
      ⇒ (y ∈ i-approx(I;n))
      ⇒ (|y - x| ≤ d1)
      ⇒ (|f1[y] - f1[x] - g1[x] * (y - x)| ≤ ((r1/r(2 * k)) * |y - x|)))
14. r0 < rmin(del;d1)
15. x : ℝ
16. y : ℝ
17. x ∈ i-approx(I;n)
18. y ∈ i-approx(I;n)
19. |y - x| ≤ rmin(del;d1)
20. y ∈ I
21. x ∈ I
⊢ |(f1[y] + f2[y]) - f1[x] + f2[x] - (g1[x] + g2[x]) * (y - x)| ≤ ((r1/r(k)) * |y - x|)

---

Latex:

---

Latex:
\mforall{}[I:Interval].  \mforall{}[f1,f2,g1,g2:I  {}\mrightarrow{}\mBbbR{}].
    (d(f1[x])/dx  =  \mlambda{}x.g1[x]  on  I
    {}\mRightarrow{}  d(f2[x])/dx  =  \mlambda{}x.g2[x]  on  I
    {}\mRightarrow{}  d(f1[x]  +  f2[x])/dx  =  \mlambda{}x.g1[x]  +  g2[x]  on  I)


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  \mforall{}h:hyp.  (Unfold  `derivative`  h
                              THEN  (InstHyp  [\mkleeneopen{}2  *  k\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]  h\mcdot{}  THENA  Auto)
                              THEN  Thin  h
                              THEN  D  -1) 
  THEN  With  \mkleeneopen{}rmin(del;d1)\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  \mforall{}h:hyp.  (FLemma  `i-member-approx`  [h]  THEN  Auto) 
  THEN  EAuto  1\mcdot{})

---

Home Index