---

Step * 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. ∃a:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|g[x]| ≤ a)
16. ∃a:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|(r1/f[x])| ≤ a)
⊢ ∃M:ℕ+. ∀x:ℝ. ((x ∈ i-approx(I;n)) ⇒ ((|g[x]| ≤ r(M)) ∧ (|(r1/f[x])| ≤ r(M))))
BY
{ (ExRepD
   THEN With ⌜imax(r-bound(a1);r-bound(a))⌝ (D 0)⋅
   THEN Auto
   THEN (RWW "rmax-int<" 0 THENA Auto)
   THEN Try ((BLemma `rmax_ub` 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. 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)))

2
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)
21. |g[x]| ≤ r(imax(r-bound(a1);r-bound(a)))
⊢ (|(r1/f[x])| ≤ r(r-bound(a1))) ∨ (|(r1/f[x])| ≤ r(r-bound(a)))

---

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.  \mexists{}a:\mBbbR{}.  \mforall{}[x:\{r:\mBbbR{}|  r  \mmember{}  i-approx(I;n)\}  ].  (|g[x]|  \mleq{}  a)
16.  \mexists{}a:\mBbbR{}.  \mforall{}[x:\{r:\mBbbR{}|  r  \mmember{}  i-approx(I;n)\}  ].  (|(r1/f[x])|  \mleq{}  a)
\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:
(ExRepD
  THEN  With  \mkleeneopen{}imax(r-bound(a1);r-bound(a))\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  (RWW  "rmax-int<"  0  THENA  Auto)
  THEN  Try  ((BLemma  `rmax\_ub`  THEN  Auto)))\mcdot{}

---

Home Index