---

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


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
BY
{ ((nRAdd ⌜(r1/r(k))⌝ (-2)⋅ THENA Auto) THEN RWO "-2" 0 THEN Auto) }

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]) ⇒ (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)))
⊢ ((r1/r(k)) + f[x]) < r0

---

Latex:

---

Latex:

1.  I  :  Interval
2.  f  :  \{x:\mBbbR{}|  x  \mmember{}  I\}    {}\mrightarrow{}  \mBbbR{}
3.  icompact(I)
4.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f[x]  =  f[y]))
5.  x  :  \{x:\mBbbR{}|  x  \mmember{}  I\} 
6.  r0  <  |f[x]|
7.  i-approx(I;1)  =  I
8.  k  :  \mBbbN{}\msupplus{}
9.  (r1/r(k))  <  |f[x]|
10.  d  :  \mBbbR{}
11.  r0  <  d
12.  \mforall{}x,y:\mBbbR{}.
            ((x  \mmember{}  i-approx(I;1))  {}\mRightarrow{}  (y  \mmember{}  i-approx(I;1))  {}\mRightarrow{}  (|x  -  y|  \mleq{}  d)  {}\mRightarrow{}  (|f[x]  -  f[y]|  \mleq{}  (r1/r(k))))
13.  y  :  \{x:\mBbbR{}|  x  \mmember{}  I\} 
14.  |x  -  y|  \mleq{}  d
15.  (r0  <  f[x])  {}\mRightarrow{}  (r0  <  f[y])
16.  (r0  <  f[x])  \mLeftarrow{}{}  r0  <  f[y]
17.  f[x]  <  r0
18.  (f[y]  -  (r1/r(k)))  \mleq{}  f[x]
19.  f[x]  \mleq{}  (f[y]  +  (r1/r(k)))
\mvdash{}  f[y]  <  r0


By

---

Latex:
((nRAdd  \mkleeneopen{}(r1/r(k))\mkleeneclose{}  (-2)\mcdot{}  THENA  Auto)  THEN  RWO  "-2"  0  THEN  Auto)

---

Home Index