---

Step * 1 of Lemma continuous-rinv


1. I : Interval
2. f : I ⟶ℝ
3. m : {m:ℕ+| icompact(i-approx(I;m))} 
4. n : ℕ+
5. c : ℝ
6. (r0 < c) ∧ (∀x:ℝ. ((x ∈ i-approx(I;m)) ⇒ (c ≤ |f[x]|)))
7. ∀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))))))})
⊢ ∃d:{ℝ| ((r0 < d)
         ∧ (∀x,y:ℝ.
              ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|(r1/f[x]) - (r1/f[y])| ≤ (r1/r(n))))))}
BY
{ (D 6
   THEN ((InstLemma `small-reciprocal-real` [⌜c⌝]⋅ THENM D -1) THENA Auto)
   THEN (Assert ∀x:ℝ. ((x ∈ i-approx(I;m)) ⇒ ((r1/r(k)) ≤ |f[x]|)) BY
               (ParallelOp 7 THEN Auto THEN (FLemma `i-member-approx` [-3] THEN Auto)⋅))
   THEN (Assert ∀x:ℝ. ((x ∈ i-approx(I;m)) ⇒ f[x] ≠ r0) BY
               (ParallelOp 7
                THEN ParallelLast
                THEN BLemma `rabs-positive-iff` 
                THEN Auto
                THEN ∀h:hyp. (FLemma `i-member-approx` [h] THEN Auto) ))
   THEN ThinVar `c'
   THEN (InstHyp [⌜(k * k) * n⌝] (-4)⋅ THENA Auto)
   THEN ParallelLast'
   THEN ∀h:hyp. (FLemma `i-member-approx` [h] THENA Complete (Auto)) 
   THEN Try (Complete (Auto))
   THEN RepeatFor 6 ((ParallelLast' THENA Auto))) }

1
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))

---

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.  c  :  \mBbbR{}
6.  (r0  <  c)  \mwedge{}  (\mforall{}x:\mBbbR{}.  ((x  \mmember{}  i-approx(I;m))  {}\mRightarrow{}  (c  \mleq{}  |f[x]|)))
7.  \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))))))\})
\mvdash{}  \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{}  (|(r1/f[x])  -  (r1/f[y])|  \mleq{}  (r1/r(n))))))\}


By

---

Latex:
(D  6
  THEN  ((InstLemma  `small-reciprocal-real`  [\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENM  D  -1)  THENA  Auto)
  THEN  (Assert  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  i-approx(I;m))  {}\mRightarrow{}  ((r1/r(k))  \mleq{}  |f[x]|))  BY
                          (ParallelOp  7  THEN  Auto  THEN  (FLemma  `i-member-approx`  [-3]  THEN  Auto)\mcdot{}))
  THEN  (Assert  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  i-approx(I;m))  {}\mRightarrow{}  f[x]  \mneq{}  r0)  BY
                          (ParallelOp  7
                            THEN  ParallelLast
                            THEN  BLemma  `rabs-positive-iff` 
                            THEN  Auto
                            THEN  \mforall{}h:hyp.  (FLemma  `i-member-approx`  [h]  THEN  Auto)  ))
  THEN  ThinVar  `c'
  THEN  (InstHyp  [\mkleeneopen{}(k  *  k)  *  n\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)
  THEN  ParallelLast'
  THEN  \mforall{}h:hyp.  (FLemma  `i-member-approx`  [h]  THENA  Complete  (Auto)) 
  THEN  Try  (Complete  (Auto))
  THEN  RepeatFor  6  ((ParallelLast'  THENA  Auto)))

---

Home Index