---

Step * 1 2 1 2 of Lemma derivative-rinv


1. I : Interval
2. f : I ⟶ℝ
3. g : I ⟶ℝ
4. ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ (g[x] = g[y]))
5. k : ℕ+
6. n : {n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))} 
7. ∀a,b:{x:ℝ| x ∈ i-approx(I;n)} .  ((a = b) ⇒ (f[a] = f[b]))
8. i-approx(I;n) ⊆ I 
9. ∀x:ℝ. ((x ∈ I) ⇒ f[x] ≠ r0)
10. ∃c:ℝ [((r0 < c) ∧ (∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ (c ≤ |f[x]|))))]
11. (r1/f[x]) continuous for x ∈ i-approx(I;n)
12. g[x] continuous for x ∈ i-approx(I;n)
13. ∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ f[x] ≠ r0)
14. M : ℕ+
15. ∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ ((|g[x]| ≤ r(M)) ∧ (|(r1/f[x])| ≤ r(M))))
16. del : ℝ
17. r0 < del
18. ∀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((2 * M * M) * k)) * |y - x|)))
19. (2 * (M * M) * M * M) * k ∈ ℕ+
20. d : ℝ
21. r0 < d
22. ∀x,y:ℝ.
      ((x ∈ i-approx(I;n))
      ⇒ (y ∈ i-approx(I;n))
      ⇒ (|x - y| ≤ d)
      ⇒ (|f[x] - f[y]| ≤ (r1/r((2 * (M * M) * M * M) * k))))
23. r0 < rmin(del;d)
24. x : ℝ
25. y : ℝ
26. x ∈ i-approx(I;n)
27. y ∈ i-approx(I;n)
28. |y - x| ≤ rmin(del;d)
⊢ |(r1/f[y]) - (r1/f[x]) - (-(g[x])/f[x] * f[x]) * (y - x)| ≤ ((r1/r(k)) * |y - x|)
BY
{ TACTIC:((Assert (|y - x| ≤ del) ∧ (|y - x| ≤ d) BY
                 (RWO  "-1" 0 THEN Auto))
          THEN D -1
          THEN RepeatFor 2 (∀h:hyp. (FHyp h [-2] THENA Auto) ⋅)
          THEN (Assert (|g[x]| ≤ r(M)) ∧ (|(r1/f[x])| ≤ r(M)) BY
                      Auto)
          THEN (Assert (|g[y]| ≤ r(M)) ∧ (|(r1/f[y])| ≤ r(M)) BY
                      Auto)) }

1
1. I : Interval
2. f : I ⟶ℝ
3. g : I ⟶ℝ
4. ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ (g[x] = g[y]))
5. k : ℕ+
6. n : {n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))} 
7. ∀a,b:{x:ℝ| x ∈ i-approx(I;n)} .  ((a = b) ⇒ (f[a] = f[b]))
8. i-approx(I;n) ⊆ I 
9. ∀x:ℝ. ((x ∈ I) ⇒ f[x] ≠ r0)
10. ∃c:ℝ [((r0 < c) ∧ (∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ (c ≤ |f[x]|))))]
11. (r1/f[x]) continuous for x ∈ i-approx(I;n)
12. g[x] continuous for x ∈ i-approx(I;n)
13. ∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ f[x] ≠ r0)
14. M : ℕ+
15. ∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ ((|g[x]| ≤ r(M)) ∧ (|(r1/f[x])| ≤ r(M))))
16. del : ℝ
17. r0 < del
18. ∀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((2 * M * M) * k)) * |y - x|)))
19. (2 * (M * M) * M * M) * k ∈ ℕ+
20. d : ℝ
21. r0 < d
22. ∀x,y:ℝ.
      ((x ∈ i-approx(I;n))
      ⇒ (y ∈ i-approx(I;n))
      ⇒ (|x - y| ≤ d)
      ⇒ (|f[x] - f[y]| ≤ (r1/r((2 * (M * M) * M * M) * k))))
23. r0 < rmin(del;d)
24. x : ℝ
25. y : ℝ
26. x ∈ i-approx(I;n)
27. y ∈ i-approx(I;n)
28. |y - x| ≤ rmin(del;d)
29. |y - x| ≤ del
30. |y - x| ≤ d
31. |f[y] - f[x] - g[x] * (y - x)| ≤ ((r1/r((2 * M * M) * k)) * |y - x|)
32. |f[y] - f[x]| ≤ (r1/r((2 * (M * M) * M * M) * k))
33. (|g[x]| ≤ r(M)) ∧ (|(r1/f[x])| ≤ r(M))
34. (|g[y]| ≤ r(M)) ∧ (|(r1/f[y])| ≤ r(M))
⊢ |(r1/f[y]) - (r1/f[x]) - (-(g[x])/f[x] * f[x]) * (y - x)| ≤ ((r1/r(k)) * |y - x|)

---

Latex:

---

Latex:

1.  I  :  Interval
2.  f  :  I  {}\mrightarrow{}\mBbbR{}
3.  g  :  I  {}\mrightarrow{}\mBbbR{}
4.  \mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (g[x]  =  g[y]))
5.  k  :  \mBbbN{}\msupplus{}
6.  n  :  \{n:\mBbbN{}\msupplus{}|  icompact(i-approx(I;n))  \mwedge{}  iproper(i-approx(I;n))\} 
7.  \mforall{}a,b:\{x:\mBbbR{}|  x  \mmember{}  i-approx(I;n)\}  .    ((a  =  b)  {}\mRightarrow{}  (f[a]  =  f[b]))
8.  i-approx(I;n)  \msubseteq{}  I 
9.  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  I)  {}\mRightarrow{}  f[x]  \mneq{}  r0)
10.  \mexists{}c:\mBbbR{}  [((r0  <  c)  \mwedge{}  (\mforall{}x:\mBbbR{}.  ((x  \mmember{}  i-approx(I;n))  {}\mRightarrow{}  (c  \mleq{}  |f[x]|))))]
11.  (r1/f[x])  continuous  for  x  \mmember{}  i-approx(I;n)
12.  g[x]  continuous  for  x  \mmember{}  i-approx(I;n)
13.  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  i-approx(I;n))  {}\mRightarrow{}  f[x]  \mneq{}  r0)
14.  M  :  \mBbbN{}\msupplus{}
15.  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  i-approx(I;n))  {}\mRightarrow{}  ((|g[x]|  \mleq{}  r(M))  \mwedge{}  (|(r1/f[x])|  \mleq{}  r(M))))
16.  del  :  \mBbbR{}
17.  r0  <  del
18.  \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((2  *  M  *  M)  *  k))  *  |y  -  x|)))
19.  (2  *  (M  *  M)  *  M  *  M)  *  k  \mmember{}  \mBbbN{}\msupplus{}
20.  d  :  \mBbbR{}
21.  r0  <  d
22.  \mforall{}x,y:\mBbbR{}.
            ((x  \mmember{}  i-approx(I;n))
            {}\mRightarrow{}  (y  \mmember{}  i-approx(I;n))
            {}\mRightarrow{}  (|x  -  y|  \mleq{}  d)
            {}\mRightarrow{}  (|f[x]  -  f[y]|  \mleq{}  (r1/r((2  *  (M  *  M)  *  M  *  M)  *  k))))
23.  r0  <  rmin(del;d)
24.  x  :  \mBbbR{}
25.  y  :  \mBbbR{}
26.  x  \mmember{}  i-approx(I;n)
27.  y  \mmember{}  i-approx(I;n)
28.  |y  -  x|  \mleq{}  rmin(del;d)
\mvdash{}  |(r1/f[y])  -  (r1/f[x])  -  (-(g[x])/f[x]  *  f[x])  *  (y  -  x)|  \mleq{}  ((r1/r(k))  *  |y  -  x|)


By

---

Latex:
TACTIC:((Assert  (|y  -  x|  \mleq{}  del)  \mwedge{}  (|y  -  x|  \mleq{}  d)  BY
                              (RWO    "-1"  0  THEN  Auto))
                THEN  D  -1
                THEN  RepeatFor  2  (\mforall{}h:hyp.  (FHyp  h  [-2]  THENA  Auto)  \mcdot{})
                THEN  (Assert  (|g[x]|  \mleq{}  r(M))  \mwedge{}  (|(r1/f[x])|  \mleq{}  r(M))  BY
                                        Auto)
                THEN  (Assert  (|g[y]|  \mleq{}  r(M))  \mwedge{}  (|(r1/f[y])|  \mleq{}  r(M))  BY
                                        Auto))

---

Home Index