---

Step * 4 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[y] < r0
18. (f[y] - (r1/r(k))) ≤ f[x]
19. f[x] ≤ (f[y] + (r1/r(k)))
⊢ f[x] < r0
BY
{ ((Assert r0 ≤ (r1/r(k)) BY Auto) THEN (RWO "rabs-strict-ub" 9 THENA Auto) THEN D 9) }

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[y] < r0
18. (f[y] - (r1/r(k))) ≤ f[x]
19. f[x] ≤ (f[y] + (r1/r(k)))
20. r0 ≤ (r1/r(k))
⊢ f[x] < r0

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[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)))
20. r0 ≤ (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[y]  <  r0
18.  (f[y]  -  (r1/r(k)))  \mleq{}  f[x]
19.  f[x]  \mleq{}  (f[y]  +  (r1/r(k)))
\mvdash{}  f[x]  <  r0


By

---

Latex:
((Assert  r0  \mleq{}  (r1/r(k))  BY  Auto)  THEN  (RWO  "rabs-strict-ub"  9  THENA  Auto)  THEN  D  9)

---

Home Index