---

Step * 1 1 of Lemma derivative-rinv

.....assertion..... 
1. I : Interval
2. f : I ⟶ℝ
3. g : I ⟶ℝ
4. ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ (g[x] = g[y]))
5. d(f[x])/dx = λx.g[x] on I
6. k : ℕ+
7. n : {n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))} 
8. ∀a,b:{x:ℝ| x ∈ i-approx(I;n)} .  ((a = b) ⇒ (f[a] = f[b]))
9. i-approx(I;n) ⊆ I 
10. ∀x:ℝ. ((x ∈ I) ⇒ f[x] ≠ r0)
11. ∃c:ℝ [((r0 < c) ∧ (∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ (c ≤ |f[x]|))))]
12. (r1/f[x]) continuous for x ∈ i-approx(I;n)
13. g[x] continuous for x ∈ i-approx(I;n)
14. ∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ f[x] ≠ r0)
⊢ ∃M:ℕ+. ∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ ((|g[x]| ≤ r(M)) ∧ (|(r1/f[x])| ≤ r(M))))
BY
{ (RenameVar `mcg' (-2)⋅
   THEN (Assert ∃a:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|g[x]| ≤ a) BY
               ((InstLemma `Inorm-bound` [⌜i-approx(I;n)⌝;⌜g⌝;⌜mcg⌝]⋅ THENA Auto)
                THEN (InstLemma `Inorm_wf` [⌜i-approx(I;n)⌝;⌜g⌝;⌜mcg⌝]⋅ THENA Auto)
                THEN With ⌜||g[x]||_i-approx(I;n)⌝ (D 0)⋅
                THEN Auto))
   ) }

1
1. I : Interval
2. f : I ⟶ℝ
3. g : I ⟶ℝ
4. ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ (g[x] = g[y]))
5. d(f[x])/dx = λx.g[x] on I
6. k : ℕ+
7. n : {n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))} 
8. ∀a,b:{x:ℝ| x ∈ i-approx(I;n)} .  ((a = b) ⇒ (f[a] = f[b]))
9. i-approx(I;n) ⊆ I 
10. ∀x:ℝ. ((x ∈ I) ⇒ f[x] ≠ r0)
11. ∃c:ℝ [((r0 < c) ∧ (∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ (c ≤ |f[x]|))))]
12. (r1/f[x]) continuous for x ∈ i-approx(I;n)
13. mcg : g[x] continuous for x ∈ i-approx(I;n)
14. ∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ f[x] ≠ r0)
15. ∃a:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|g[x]| ≤ a)
⊢ ∃M:ℕ+. ∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ ((|g[x]| ≤ r(M)) ∧ (|(r1/f[x])| ≤ r(M))))

---

Latex:

---

Latex:
.....assertion..... 
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.  d(f[x])/dx  =  \mlambda{}x.g[x]  on  I
6.  k  :  \mBbbN{}\msupplus{}
7.  n  :  \{n:\mBbbN{}\msupplus{}|  icompact(i-approx(I;n))  \mwedge{}  iproper(i-approx(I;n))\} 
8.  \mforall{}a,b:\{x:\mBbbR{}|  x  \mmember{}  i-approx(I;n)\}  .    ((a  =  b)  {}\mRightarrow{}  (f[a]  =  f[b]))
9.  i-approx(I;n)  \msubseteq{}  I 
10.  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  I)  {}\mRightarrow{}  f[x]  \mneq{}  r0)
11.  \mexists{}c:\mBbbR{}  [((r0  <  c)  \mwedge{}  (\mforall{}x:\mBbbR{}.  ((x  \mmember{}  i-approx(I;n))  {}\mRightarrow{}  (c  \mleq{}  |f[x]|))))]
12.  (r1/f[x])  continuous  for  x  \mmember{}  i-approx(I;n)
13.  g[x]  continuous  for  x  \mmember{}  i-approx(I;n)
14.  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  i-approx(I;n))  {}\mRightarrow{}  f[x]  \mneq{}  r0)
\mvdash{}  \mexists{}M:\mBbbN{}\msupplus{}.  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  i-approx(I;n))  {}\mRightarrow{}  ((|g[x]|  \mleq{}  r(M))  \mwedge{}  (|(r1/f[x])|  \mleq{}  r(M))))


By

---

Latex:
(RenameVar  `mcg'  (-2)\mcdot{}
  THEN  (Assert  \mexists{}a:\mBbbR{}.  \mforall{}[x:\{r:\mBbbR{}|  r  \mmember{}  i-approx(I;n)\}  ].  (|g[x]|  \mleq{}  a)  BY
                          ((InstLemma  `Inorm-bound`  [\mkleeneopen{}i-approx(I;n)\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}mcg\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  (InstLemma  `Inorm\_wf`  [\mkleeneopen{}i-approx(I;n)\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}mcg\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  With  \mkleeneopen{}||g[x]||\_i-approx(I;n)\mkleeneclose{}  (D  0)\mcdot{}
                            THEN  Auto))
  )

---

Home Index