---

Step * 2 of Lemma derivative_functionality_wrt_subinterval


1. I : Interval
2. J : Interval
3. [f] : I ⟶ℝ
4. [f'] : I ⟶ℝ
5. J ⊆ I 
6. k : ℕ+
7. n : {n:ℕ+| icompact(i-approx(J;n)) ∧ iproper(i-approx(J;n))} 
8. m : {n:ℕ+| icompact(i-approx(I;n))} 
9. i-approx(J;n) ⊆ i-approx(I;m) 
10. ∃del:{ℝ| ((r0 < del)
             ∧ (∀x,y:ℝ.
                  ((x ∈ i-approx(I;m))
                  ⇒ (y ∈ i-approx(I;m))
                  ⇒ (|y - x| ≤ del)
                  ⇒ (|f[y] - f[x] - f'[x] * (y - x)| ≤ ((r1/r(k)) * |y - x|)))))}
⊢ ∃del:{ℝ| ((r0 < del)
           ∧ (∀x,y:ℝ.
                ((x ∈ i-approx(J;n))
                ⇒ (y ∈ i-approx(J;n))
                ⇒ (|y - x| ≤ del)
                ⇒ (|f[y] - f[x] - f'[x] * (y - x)| ≤ ((r1/r(k)) * |y - x|)))))}
BY
{ (ParallelLast
   THEN ∀h:hyp. (FLemma `i-member-approx` [h] THEN Complete (Auto)) 
   THEN RepeatFor 6 ((ParallelLast⋅ THENA Auto))) }

---

Latex:

---

Latex:

1.  I  :  Interval
2.  J  :  Interval
3.  [f]  :  I  {}\mrightarrow{}\mBbbR{}
4.  [f']  :  I  {}\mrightarrow{}\mBbbR{}
5.  J  \msubseteq{}  I 
6.  k  :  \mBbbN{}\msupplus{}
7.  n  :  \{n:\mBbbN{}\msupplus{}|  icompact(i-approx(J;n))  \mwedge{}  iproper(i-approx(J;n))\} 
8.  m  :  \{n:\mBbbN{}\msupplus{}|  icompact(i-approx(I;n))\} 
9.  i-approx(J;n)  \msubseteq{}  i-approx(I;m) 
10.  \mexists{}del:\{\mBbbR{}|  ((r0  <  del)
                          \mwedge{}  (\mforall{}x,y:\mBbbR{}.
                                    ((x  \mmember{}  i-approx(I;m))
                                    {}\mRightarrow{}  (y  \mmember{}  i-approx(I;m))
                                    {}\mRightarrow{}  (|y  -  x|  \mleq{}  del)
                                    {}\mRightarrow{}  (|f[y]  -  f[x]  -  f'[x]  *  (y  -  x)|  \mleq{}  ((r1/r(k))  *  |y  -  x|)))))\}
\mvdash{}  \mexists{}del:\{\mBbbR{}|  ((r0  <  del)
                      \mwedge{}  (\mforall{}x,y:\mBbbR{}.
                                ((x  \mmember{}  i-approx(J;n))
                                {}\mRightarrow{}  (y  \mmember{}  i-approx(J;n))
                                {}\mRightarrow{}  (|y  -  x|  \mleq{}  del)
                                {}\mRightarrow{}  (|f[y]  -  f[x]  -  f'[x]  *  (y  -  x)|  \mleq{}  ((r1/r(k))  *  |y  -  x|)))))\}


By

---

Latex:
(ParallelLast
  THEN  \mforall{}h:hyp.  (FLemma  `i-member-approx`  [h]  THEN  Complete  (Auto)) 
  THEN  RepeatFor  6  ((ParallelLast\mcdot{}  THENA  Auto)))

---

Home Index