---

Step * 4 1 1 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. d : ℝ
10. r0 < d
11. ∀x,y:ℝ.  ((x ∈ i-approx(I;1)) ⇒ (y ∈ i-approx(I;1)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(k))))
12. y : {x:ℝ| x ∈ I} 
13. |x - y| ≤ d
14. (r0 < f[x]) ⇒ (r0 < f[y])
15. (r0 < f[x]) ⇐ r0 < f[y]
16. f[y] < r0
17. (f[y] - (r1/r(k))) ≤ f[x]
18. f[x] ≤ (f[y] + (r1/r(k)))
19. r0 ≤ (r1/r(k))
20. (r1/r(k)) < (f[y] + (r1/r(k)))
⊢ f[x] < r0
BY
{ ((Assert r0 < f[y] BY Auto) THEN Auto) }

---

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.  d  :  \mBbbR{}
10.  r0  <  d
11.  \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))))
12.  y  :  \{x:\mBbbR{}|  x  \mmember{}  I\} 
13.  |x  -  y|  \mleq{}  d
14.  (r0  <  f[x])  {}\mRightarrow{}  (r0  <  f[y])
15.  (r0  <  f[x])  \mLeftarrow{}{}  r0  <  f[y]
16.  f[y]  <  r0
17.  (f[y]  -  (r1/r(k)))  \mleq{}  f[x]
18.  f[x]  \mleq{}  (f[y]  +  (r1/r(k)))
19.  r0  \mleq{}  (r1/r(k))
20.  (r1/r(k))  <  (f[y]  +  (r1/r(k)))
\mvdash{}  f[x]  <  r0


By

---

Latex:
((Assert  r0  <  f[y]  BY  Auto)  THEN  Auto)

---

Home Index