---

Step * of Lemma function-values-near-same-sign

∀I:Interval. ∀f:{x:ℝ| x ∈ I}  ⟶ ℝ.
  (icompact(I)
  ⇒ (∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (f[x] = f[y])))
  ⇒ (∀x:{x:ℝ| x ∈ I} 
        ((r0 < |f[x]|)
        ⇒ (∃d:{d:ℝ| r0 < d} 
             ∀y:{x:ℝ| x ∈ I} . ((|x - y| ≤ d) ⇒ ((r0 < f[x] ⇐⇒ r0 < f[y]) ∧ (f[x] < r0 ⇐⇒ f[y] < r0)))))))
BY
{ (Auto
   THEN (InstLemma `function-is-continuous` [⌜I⌝;⌜f⌝]⋅ THENA Auto)
   THEN (D -1 With ⌜1⌝  THENA (Auto THEN MemTypeCD THEN Auto))
   THEN (InstLemma `i-approx-of-compact` [⌜I⌝;⌜1⌝]⋅ THENA Auto)
   THEN (InstLemma `small-reciprocal-real` [⌜|f[x]|⌝]⋅ THENA Auto)
   THEN D -1
   THEN (D -4 With ⌜k⌝  THENA Auto)
   THEN D -1
   THEN D 0 With ⌜d⌝ 
   THEN Auto
   THEN (Unhide THENA Auto)
   THEN ExRepD
   THEN InstHyp [⌜x⌝;⌜y⌝] 12⋅
   THEN Auto
   THEN Try ((RWO "7" 0 THEN Auto))
   THEN (RWO "rabs-difference-bound-rleq" (-1) THENA Auto)
   THEN D -1) }

1
1. I : Interval
2. f : {x:ℝ| x ∈ I}  ⟶ ℝ
3. icompact(I)
4. ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (f[x] = f[y]))
5. x : {x:ℝ| x ∈ I} 
6. r0 < |f[x]|
7. i-approx(I;1) = I ∈ Interval
8. k : ℕ+
9. (r1/r(k)) < |f[x]|
10. d : ℝ
11. r0 < d
12. ∀x,y:ℝ.  ((x ∈ i-approx(I;1)) ⇒ (y ∈ i-approx(I;1)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(k))))
13. y : {x:ℝ| x ∈ I} 
14. |x - y| ≤ d
15. r0 < f[x]
16. (f[y] - (r1/r(k))) ≤ f[x]
17. f[x] ≤ (f[y] + (r1/r(k)))
⊢ r0 < f[y]

2
1. I : Interval
2. f : {x:ℝ| x ∈ I}  ⟶ ℝ
3. icompact(I)
4. ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (f[x] = f[y]))
5. x : {x:ℝ| x ∈ I} 
6. r0 < |f[x]|
7. i-approx(I;1) = I ∈ Interval
8. k : ℕ+
9. (r1/r(k)) < |f[x]|
10. d : ℝ
11. r0 < d
12. ∀x,y:ℝ.  ((x ∈ i-approx(I;1)) ⇒ (y ∈ i-approx(I;1)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(k))))
13. y : {x:ℝ| x ∈ I} 
14. |x - y| ≤ d
15. r0 < f[y]
16. (f[y] - (r1/r(k))) ≤ f[x]
17. f[x] ≤ (f[y] + (r1/r(k)))
⊢ r0 < f[x]

3
1. I : Interval
2. f : {x:ℝ| x ∈ I}  ⟶ ℝ
3. icompact(I)
4. ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (f[x] = f[y]))
5. x : {x:ℝ| x ∈ I} 
6. r0 < |f[x]|
7. i-approx(I;1) = I ∈ Interval
8. k : ℕ+
9. (r1/r(k)) < |f[x]|
10. d : ℝ
11. r0 < d
12. ∀x,y:ℝ.  ((x ∈ i-approx(I;1)) ⇒ (y ∈ i-approx(I;1)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(k))))
13. y : {x:ℝ| x ∈ I} 
14. |x - y| ≤ d
15. (r0 < f[x]) ⇒ (r0 < f[y])
16. (r0 < f[x]) ⇐ r0 < f[y]
17. f[x] < r0
18. (f[y] - (r1/r(k))) ≤ f[x]
19. f[x] ≤ (f[y] + (r1/r(k)))
⊢ f[y] < r0

4
1. I : Interval
2. f : {x:ℝ| x ∈ I}  ⟶ ℝ
3. icompact(I)
4. ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (f[x] = f[y]))
5. x : {x:ℝ| x ∈ I} 
6. r0 < |f[x]|
7. i-approx(I;1) = I ∈ Interval
8. k : ℕ+
9. (r1/r(k)) < |f[x]|
10. d : ℝ
11. r0 < d
12. ∀x,y:ℝ.  ((x ∈ i-approx(I;1)) ⇒ (y ∈ i-approx(I;1)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(k))))
13. y : {x:ℝ| x ∈ I} 
14. |x - y| ≤ d
15. (r0 < f[x]) ⇒ (r0 < f[y])
16. (r0 < f[x]) ⇐ r0 < f[y]
17. f[y] < r0
18. (f[y] - (r1/r(k))) ≤ f[x]
19. f[x] ≤ (f[y] + (r1/r(k)))
⊢ f[x] < r0

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}f:\{x:\mBbbR{}|  x  \mmember{}  I\}    {}\mrightarrow{}  \mBbbR{}.
    (icompact(I)
    {}\mRightarrow{}  (\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f[x]  =  f[y])))
    {}\mRightarrow{}  (\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\} 
                ((r0  <  |f[x]|)
                {}\mRightarrow{}  (\mexists{}d:\{d:\mBbbR{}|  r0  <  d\} 
                          \mforall{}y:\{x:\mBbbR{}|  x  \mmember{}  I\} 
                              ((|x  -  y|  \mleq{}  d)  {}\mRightarrow{}  ((r0  <  f[x]  \mLeftarrow{}{}\mRightarrow{}  r0  <  f[y])  \mwedge{}  (f[x]  <  r0  \mLeftarrow{}{}\mRightarrow{}  f[y]  <  r0)))))))


By

---

Latex:
(Auto
  THEN  (InstLemma  `function-is-continuous`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (D  -1  With  \mkleeneopen{}1\mkleeneclose{}    THENA  (Auto  THEN  MemTypeCD  THEN  Auto))
  THEN  (InstLemma  `i-approx-of-compact`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `small-reciprocal-real`  [\mkleeneopen{}|f[x]|\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  (D  -4  With  \mkleeneopen{}k\mkleeneclose{}    THENA  Auto)
  THEN  D  -1
  THEN  D  0  With  \mkleeneopen{}d\mkleeneclose{} 
  THEN  Auto
  THEN  (Unhide  THENA  Auto)
  THEN  ExRepD
  THEN  InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  12\mcdot{}
  THEN  Auto
  THEN  Try  ((RWO  "7"  0  THEN  Auto))
  THEN  (RWO  "rabs-difference-bound-rleq"  (-1)  THENA  Auto)
  THEN  D  -1)

---

Home Index