---

Step * 1 1 1 1 1 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. 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. mcfinv : (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. a1 : ℝ
16. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|g[x]| ≤ a1)
17. a : ℝ
18. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|(r1/f[x])| ≤ a)
19. x : ℝ
20. x ∈ i-approx(I;n)
⊢ (|g[x]| ≤ r(r-bound(a1))) ∨ (|g[x]| ≤ r(r-bound(a)))
BY
{ ((OrLeft THEN Auto)⋅ THEN OnMaybeHyp 17 (\h. (RW (AddrC [1] (HypC h)) 0 THEN Complete (Auto)))) }

---

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.  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.  mcfinv  :  (r1/f[x])  continuous  for  x  \mmember{}  i-approx(I;n)
13.  mcg  :  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)
15.  a1  :  \mBbbR{}
16.  \mforall{}[x:\{r:\mBbbR{}|  r  \mmember{}  i-approx(I;n)\}  ].  (|g[x]|  \mleq{}  a1)
17.  a  :  \mBbbR{}
18.  \mforall{}[x:\{r:\mBbbR{}|  r  \mmember{}  i-approx(I;n)\}  ].  (|(r1/f[x])|  \mleq{}  a)
19.  x  :  \mBbbR{}
20.  x  \mmember{}  i-approx(I;n)
\mvdash{}  (|g[x]|  \mleq{}  r(r-bound(a1)))  \mvee{}  (|g[x]|  \mleq{}  r(r-bound(a)))


By

---

Latex:
((OrLeft  THEN  Auto)\mcdot{}  THEN  OnMaybeHyp  17  (\mbackslash{}h.  (RW  (AddrC  [1]  (HypC  h))  0  THEN  Complete  (Auto))))

---

Home Index