---

Step * 1 1 1 2 1 1 1 of Lemma derivative_unique


1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. g1 : I ⟶ℝ
5. g2 : I ⟶ℝ
6. x : ℝ
7. x ∈ I
8. m : ℕ+
9. n : ℕ+
10. iproper(i-approx(I;n))
11. x ∈ i-approx(I;n)
12. icompact(i-approx(I;n))
13. del : ℝ
14. r0 < del
15. ∀x,y:ℝ.
      ((x ∈ i-approx(I;n))
      ⇒ (y ∈ i-approx(I;n))
      ⇒ (|y - x| ≤ del)
      ⇒ (|f[y] - f[x] - g2[x] * (y - x)| ≤ ((r1/r(2 * m)) * |y - x|)))
16. d1 : ℝ
17. r0 < d1
18. ∀x,y:ℝ.
      ((x ∈ i-approx(I;n))
      ⇒ (y ∈ i-approx(I;n))
      ⇒ (|y - x| ≤ d1)
      ⇒ (|f[y] - f[x] - g1[x] * (y - x)| ≤ ((r1/r(2 * m)) * |y - x|)))
19. y : ℝ
20. y ∈ I
21. y ∈ i-approx(I;n)
22. |y - x| ≤ del
23. |y - x| ≤ d1
24. r0 < |y - x|
25. |f[y] - f[x] - g1[x] * (y - x)| ≤ ((r1/r(2 * m)) * |y - x|)
26. |(g2[x] * (y - x)) - f[y] - f[x]| ≤ ((r1/r(2 * m)) * |y - x|)
27. (|g2(x) - g1(x)| * |y - x|) ≤ (((r1/r(2 * m)) * |y - x|) + ((r1/r(2 * m)) * |y - x|))
28. |(f[y] - f[x] - g1[x] * (y - x)) + ((g2[x] * (y - x)) - f[y] - f[x])| = (|g2(x) - g1(x)| * |y - x|)
⊢ |g1(x) - g2(x)| ≤ (r1/r(m))
BY
{ ((RWO "rabs-difference-symmetry" 0 THENA Auto)
   THEN MoveToConcl (-2)
   THEN GenConclTerms Auto [⌜|g2(x) - g1(x)|⌝;⌜|y - x|⌝]⋅
   THEN (RWO "rmul-distrib1<" 0 THENA Auto)) }

1
1. I : Interval
2. iproper(I)
3. f : I ⟶ℝ
4. g1 : I ⟶ℝ
5. g2 : I ⟶ℝ
6. x : ℝ
7. x ∈ I
8. m : ℕ+
9. n : ℕ+
10. iproper(i-approx(I;n))
11. x ∈ i-approx(I;n)
12. icompact(i-approx(I;n))
13. del : ℝ
14. r0 < del
15. ∀x,y:ℝ.
      ((x ∈ i-approx(I;n))
      ⇒ (y ∈ i-approx(I;n))
      ⇒ (|y - x| ≤ del)
      ⇒ (|f[y] - f[x] - g2[x] * (y - x)| ≤ ((r1/r(2 * m)) * |y - x|)))
16. d1 : ℝ
17. r0 < d1
18. ∀x,y:ℝ.
      ((x ∈ i-approx(I;n))
      ⇒ (y ∈ i-approx(I;n))
      ⇒ (|y - x| ≤ d1)
      ⇒ (|f[y] - f[x] - g1[x] * (y - x)| ≤ ((r1/r(2 * m)) * |y - x|)))
19. y : ℝ
20. y ∈ I
21. y ∈ i-approx(I;n)
22. |y - x| ≤ del
23. |y - x| ≤ d1
24. r0 < |y - x|
25. |f[y] - f[x] - g1[x] * (y - x)| ≤ ((r1/r(2 * m)) * |y - x|)
26. |(g2[x] * (y - x)) - f[y] - f[x]| ≤ ((r1/r(2 * m)) * |y - x|)
27. |(f[y] - f[x] - g1[x] * (y - x)) + ((g2[x] * (y - x)) - f[y] - f[x])| = (|g2(x) - g1(x)| * |y - x|)
28. v : ℝ
29. |g2(x) - g1(x)| = v ∈ ℝ
30. v1 : ℝ
31. |y - x| = v1 ∈ ℝ
⊢ ((v * v1) ≤ ((r1/r(2 * m)) * (v1 + v1))) ⇒ (v ≤ (r1/r(m)))

---

Latex:

---

Latex:

1.  I  :  Interval
2.  iproper(I)
3.  f  :  I  {}\mrightarrow{}\mBbbR{}
4.  g1  :  I  {}\mrightarrow{}\mBbbR{}
5.  g2  :  I  {}\mrightarrow{}\mBbbR{}
6.  x  :  \mBbbR{}
7.  x  \mmember{}  I
8.  m  :  \mBbbN{}\msupplus{}
9.  n  :  \mBbbN{}\msupplus{}
10.  iproper(i-approx(I;n))
11.  x  \mmember{}  i-approx(I;n)
12.  icompact(i-approx(I;n))
13.  del  :  \mBbbR{}
14.  r0  <  del
15.  \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]  -  g2[x]  *  (y  -  x)|  \mleq{}  ((r1/r(2  *  m))  *  |y  -  x|)))
16.  d1  :  \mBbbR{}
17.  r0  <  d1
18.  \mforall{}x,y:\mBbbR{}.
            ((x  \mmember{}  i-approx(I;n))
            {}\mRightarrow{}  (y  \mmember{}  i-approx(I;n))
            {}\mRightarrow{}  (|y  -  x|  \mleq{}  d1)
            {}\mRightarrow{}  (|f[y]  -  f[x]  -  g1[x]  *  (y  -  x)|  \mleq{}  ((r1/r(2  *  m))  *  |y  -  x|)))
19.  y  :  \mBbbR{}
20.  y  \mmember{}  I
21.  y  \mmember{}  i-approx(I;n)
22.  |y  -  x|  \mleq{}  del
23.  |y  -  x|  \mleq{}  d1
24.  r0  <  |y  -  x|
25.  |f[y]  -  f[x]  -  g1[x]  *  (y  -  x)|  \mleq{}  ((r1/r(2  *  m))  *  |y  -  x|)
26.  |(g2[x]  *  (y  -  x))  -  f[y]  -  f[x]|  \mleq{}  ((r1/r(2  *  m))  *  |y  -  x|)
27.  (|g2(x)  -  g1(x)|  *  |y  -  x|)  \mleq{}  (((r1/r(2  *  m))  *  |y  -  x|)  +  ((r1/r(2  *  m))  *  |y  -  x|))
28.  |(f[y]  -  f[x]  -  g1[x]  *  (y  -  x))  +  ((g2[x]  *  (y  -  x))  -  f[y]  -  f[x])|
=  (|g2(x)  -  g1(x)|  *  |y  -  x|)
\mvdash{}  |g1(x)  -  g2(x)|  \mleq{}  (r1/r(m))


By

---

Latex:
((RWO  "rabs-difference-symmetry"  0  THENA  Auto)
  THEN  MoveToConcl  (-2)
  THEN  GenConclTerms  Auto  [\mkleeneopen{}|g2(x)  -  g1(x)|\mkleeneclose{};\mkleeneopen{}|y  -  x|\mkleeneclose{}]\mcdot{}
  THEN  (RWO  "rmul-distrib1<"  0  THENA  Auto))

---

Home Index