---

Step * 1 1 1 1 1 1 of Lemma derivative-continuous


1. I : Interval@i
2. f : I ⟶ℝ@i
3. g : I ⟶ℝ@i
4. ∀x,y:{x:ℝ| x ∈ I} .  (g[x] ≠ g[y] ⇒ x ≠ y)@i
5. ∀k:ℕ+. ∀n:{n:ℕ+| icompact(i-approx(I;n))} .
     (∃del:{ℝ| ((r0 < del)
               ∧ (∀x,y:ℝ.
                    ((x ∈ i-approx(I;n))
                    ⇒ (y ∈ i-approx(I;n))
                    ⇒ (|y - x| ≤ del)
                    ⇒ (|f[y] - f[x] - g[x] * (y - x)| ≤ ((r1/r(k)) * |y - x|)))))})@i
6. m : {m:ℕ+| icompact(i-approx(I;m))} @i
7. n : ℕ+@i
8. i-approx(I;m) ⊆ I 
9. del : ℝ
10. r0 < del
11. ∀x,y:ℝ.
      ((x ∈ i-approx(I;m))
      ⇒ (y ∈ i-approx(I;m))
      ⇒ (|y - x| ≤ del)
      ⇒ (|f[y] - f[x] - g[x] * (y - x)| ≤ ((r1/r(2 * n)) * |y - x|)))
12. r0 < del
13. x : ℝ@i
14. y : ℝ@i
15. x ∈ i-approx(I;m)@i
16. y ∈ i-approx(I;m)@i
17. |x - y| ≤ del@i
18. |f[y] - f[x] - g[x] * (y - x)| ≤ ((r1/r(2 * n)) * |x - y|)
19. |f[x] - f[y] - g[y] * (x - y)| ≤ ((r1/r(2 * n)) * |x - y|)
⊢ (|g[x] - g[y]| * |x - y|) ≤ ((r1/r(n)) * |x - y|)
BY
{ (Assert (|f[y] - f[x] - g[x] * (y - x)| + |f[x] - f[y] - g[y] * (x - y)|) ≤ ((r1/r(n)) * |x - y|) BY
         (RWO "-1 -2" 0 THEN Auto)) }

1
1. I : Interval@i
2. f : I ⟶ℝ@i
3. g : I ⟶ℝ@i
4. ∀x,y:{x:ℝ| x ∈ I} .  (g[x] ≠ g[y] ⇒ x ≠ y)@i
5. ∀k:ℕ+. ∀n:{n:ℕ+| icompact(i-approx(I;n))} .
     (∃del:{ℝ| ((r0 < del)
               ∧ (∀x,y:ℝ.
                    ((x ∈ i-approx(I;n))
                    ⇒ (y ∈ i-approx(I;n))
                    ⇒ (|y - x| ≤ del)
                    ⇒ (|f[y] - f[x] - g[x] * (y - x)| ≤ ((r1/r(k)) * |y - x|)))))})@i
6. m : {m:ℕ+| icompact(i-approx(I;m))} @i
7. n : ℕ+@i
8. i-approx(I;m) ⊆ I 
9. del : ℝ
10. r0 < del
11. ∀x,y:ℝ.
      ((x ∈ i-approx(I;m))
      ⇒ (y ∈ i-approx(I;m))
      ⇒ (|y - x| ≤ del)
      ⇒ (|f[y] - f[x] - g[x] * (y - x)| ≤ ((r1/r(2 * n)) * |y - x|)))
12. r0 < del
13. x : ℝ@i
14. y : ℝ@i
15. x ∈ i-approx(I;m)@i
16. y ∈ i-approx(I;m)@i
17. |x - y| ≤ del@i
18. |f[y] - f[x] - g[x] * (y - x)| ≤ ((r1/r(2 * n)) * |x - y|)
19. |f[x] - f[y] - g[y] * (x - y)| ≤ ((r1/r(2 * n)) * |x - y|)
⊢ (((r1/r(2 * n)) * |x - y|) + ((r1/r(2 * n)) * |x - y|)) ≤ ((r1/r(n)) * |x - y|)

2
1. I : Interval@i
2. f : I ⟶ℝ@i
3. g : I ⟶ℝ@i
4. ∀x,y:{x:ℝ| x ∈ I} .  (g[x] ≠ g[y] ⇒ x ≠ y)@i
5. ∀k:ℕ+. ∀n:{n:ℕ+| icompact(i-approx(I;n))} .
     (∃del:{ℝ| ((r0 < del)
               ∧ (∀x,y:ℝ.
                    ((x ∈ i-approx(I;n))
                    ⇒ (y ∈ i-approx(I;n))
                    ⇒ (|y - x| ≤ del)
                    ⇒ (|f[y] - f[x] - g[x] * (y - x)| ≤ ((r1/r(k)) * |y - x|)))))})@i
6. m : {m:ℕ+| icompact(i-approx(I;m))} @i
7. n : ℕ+@i
8. i-approx(I;m) ⊆ I 
9. del : ℝ
10. r0 < del
11. ∀x,y:ℝ.
      ((x ∈ i-approx(I;m))
      ⇒ (y ∈ i-approx(I;m))
      ⇒ (|y - x| ≤ del)
      ⇒ (|f[y] - f[x] - g[x] * (y - x)| ≤ ((r1/r(2 * n)) * |y - x|)))
12. r0 < del
13. x : ℝ@i
14. y : ℝ@i
15. x ∈ i-approx(I;m)@i
16. y ∈ i-approx(I;m)@i
17. |x - y| ≤ del@i
18. |f[y] - f[x] - g[x] * (y - x)| ≤ ((r1/r(2 * n)) * |x - y|)
19. |f[x] - f[y] - g[y] * (x - y)| ≤ ((r1/r(2 * n)) * |x - y|)
20. (|f[y] - f[x] - g[x] * (y - x)| + |f[x] - f[y] - g[y] * (x - y)|) ≤ ((r1/r(n)) * |x - y|)
⊢ (|g[x] - g[y]| * |x - y|) ≤ ((r1/r(n)) * |x - y|)

---

Latex:

---

Latex:

1.  I  :  Interval@i
2.  f  :  I  {}\mrightarrow{}\mBbbR{}@i
3.  g  :  I  {}\mrightarrow{}\mBbbR{}@i
4.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    (g[x]  \mneq{}  g[y]  {}\mRightarrow{}  x  \mneq{}  y)@i
5.  \mforall{}k:\mBbbN{}\msupplus{}.  \mforall{}n:\{n:\mBbbN{}\msupplus{}|  icompact(i-approx(I;n))\}  .
          (\mexists{}del:\{\mBbbR{}|  ((r0  <  del)
                              \mwedge{}  (\mforall{}x,y:\mBbbR{}.
                                        ((x  \mmember{}  i-approx(I;n))
                                        {}\mRightarrow{}  (y  \mmember{}  i-approx(I;n))
                                        {}\mRightarrow{}  (|y  -  x|  \mleq{}  del)
                                        {}\mRightarrow{}  (|f[y]  -  f[x]  -  g[x]  *  (y  -  x)|  \mleq{}  ((r1/r(k))  *  |y  -  x|)))))\})@i
6.  m  :  \{m:\mBbbN{}\msupplus{}|  icompact(i-approx(I;m))\}  @i
7.  n  :  \mBbbN{}\msupplus{}@i
8.  i-approx(I;m)  \msubseteq{}  I 
9.  del  :  \mBbbR{}
10.  r0  <  del
11.  \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]  -  g[x]  *  (y  -  x)|  \mleq{}  ((r1/r(2  *  n))  *  |y  -  x|)))
12.  r0  <  del
13.  x  :  \mBbbR{}@i
14.  y  :  \mBbbR{}@i
15.  x  \mmember{}  i-approx(I;m)@i
16.  y  \mmember{}  i-approx(I;m)@i
17.  |x  -  y|  \mleq{}  del@i
18.  |f[y]  -  f[x]  -  g[x]  *  (y  -  x)|  \mleq{}  ((r1/r(2  *  n))  *  |x  -  y|)
19.  |f[x]  -  f[y]  -  g[y]  *  (x  -  y)|  \mleq{}  ((r1/r(2  *  n))  *  |x  -  y|)
\mvdash{}  (|g[x]  -  g[y]|  *  |x  -  y|)  \mleq{}  ((r1/r(n))  *  |x  -  y|)


By

---

Latex:
(Assert  (|f[y]  -  f[x]  -  g[x]  *  (y  -  x)|  +  |f[x]  -  f[y]  -  g[y]  *  (x  -  y)|)  \mleq{}  ((r1/r(n))  *  |x  -  y|)  BY
              (RWO  "-1  -2"  0  THEN  Auto))

---

Home Index