---

Step * 1 1 of Lemma continuous-rinv


1. I : Interval
2. f : I ⟶ℝ
3. m : {m:ℕ+| icompact(i-approx(I;m))} 
4. n : ℕ+
5. ∀n:ℕ+
     (∃d:{ℝ| ((r0 < d)
             ∧ (∀x,y:ℝ.
                  ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(n))))))})
6. k : ℕ+
7. ∀x:ℝ. ((x ∈ i-approx(I;m)) ⇒ ((r1/r(k)) ≤ |f[x]|))
8. ∀x:ℝ. ((x ∈ i-approx(I;m)) ⇒ f[x] ≠ r0)
9. d : ℝ
10. r0 < d
11. x : ℝ
12. y : ℝ
13. x ∈ i-approx(I;m)
14. y ∈ i-approx(I;m)
15. |x - y| ≤ d
16. |f[x] - f[y]| ≤ (r1/r((k * k) * n))
⊢ |(r1/f[x]) - (r1/f[y])| ≤ (r1/r(n))
BY
{ (MoveToConcl (-1)
   THEN (Assert f[x] ≠ r0 ∧ f[y] ≠ r0 ∧ ((r1/r(k)) ≤ |f[x]|) ∧ ((r1/r(k)) ≤ |f[y]|) BY
               Auto)
   THEN MoveToConcl (-1)
   THEN ∀h:hyp. (FLemma `i-member-approx` [h] THENA Complete (Auto)) 
   THEN (GenConclTerm ⌜f[x]⌝⋅ THENA Auto)
   THEN (GenConclTerm ⌜f[y]⌝⋅ THENA Auto)
   THEN All Thin
   THEN Auto)⋅ }

1
1. n : ℕ+
2. k : ℕ+
3. v : ℝ
4. v1 : ℝ
5. v ≠ r0
6. v1 ≠ r0
7. (r1/r(k)) ≤ |v|
8. (r1/r(k)) ≤ |v1|
9. |v - v1| ≤ (r1/r((k * k) * n))
⊢ |(r1/v) - (r1/v1)| ≤ (r1/r(n))

---

Latex:

---

Latex:

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


By

---

Latex:
(MoveToConcl  (-1)
  THEN  (Assert  f[x]  \mneq{}  r0  \mwedge{}  f[y]  \mneq{}  r0  \mwedge{}  ((r1/r(k))  \mleq{}  |f[x]|)  \mwedge{}  ((r1/r(k))  \mleq{}  |f[y]|)  BY
                          Auto)
  THEN  MoveToConcl  (-1)
  THEN  \mforall{}h:hyp.  (FLemma  `i-member-approx`  [h]  THENA  Complete  (Auto)) 
  THEN  (GenConclTerm  \mkleeneopen{}f[x]\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}f[y]\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  Auto)\mcdot{}

---

Home Index