---

Step * 1 1 1 1 2 1 1 of Lemma IVT-locally-non-constant-open


1. a : ℝ
2. b : {b:ℝ| a < b} 
3. f : [a, b] ⟶ℝ
4. (a, b) ⊆ [a, b] 
5. a < b
6. ∀a',b':ℝ.  (((a < a') ∧ (a' < b') ∧ (b' < b)) ⇒ (∀c:ℝ. locally-non-constant(f;a';b';c)))
7. c : ℝ
8. (f a) < c
9. c < (f b)
10. k : ℕ+
11. (r1/r(k)) < (c - f a)
12. d : ℝ
13. r0 < d
14. ∀x,y:ℝ.  (((a ≤ x) ∧ (x ≤ b)) ⇒ ((a ≤ y) ∧ (y ≤ b)) ⇒ (|x - y| ≤ d) ⇒ (|(f x) - f y| ≤ (r1/r(k))))
15. a < ravg(a;b)
16. ravg(a;b) < b
17. a < rmin(a + d;ravg(a;b))
18. rmin(a + d;ravg(a;b)) < b
19. ((f rmin(a + d;ravg(a;b))) - (r1/r(k))) ≤ (f a)
20. (f a) ≤ ((f rmin(a + d;ravg(a;b))) + (r1/r(k)))
21. a < rmin(a + d;ravg(a;b))
22. rmin(a + d;ravg(a;b)) < b
⊢ (f rmin(a + d;ravg(a;b))) < c
BY
{ (nRAdd ⌜(r1/r(k))⌝ (-4)⋅ THENA Auto) }

1
1. a : ℝ
2. b : {b:ℝ| a < b} 
3. f : [a, b] ⟶ℝ
4. (a, b) ⊆ [a, b] 
5. a < b
6. ∀a',b':ℝ.  (((a < a') ∧ (a' < b') ∧ (b' < b)) ⇒ (∀c:ℝ. locally-non-constant(f;a';b';c)))
7. c : ℝ
8. (f a) < c
9. c < (f b)
10. k : ℕ+
11. (r1/r(k)) < (c - f a)
12. d : ℝ
13. r0 < d
14. ∀x,y:ℝ.  (((a ≤ x) ∧ (x ≤ b)) ⇒ ((a ≤ y) ∧ (y ≤ b)) ⇒ (|x - y| ≤ d) ⇒ (|(f x) - f y| ≤ (r1/r(k))))
15. a < ravg(a;b)
16. ravg(a;b) < b
17. a < rmin(a + d;ravg(a;b))
18. rmin(a + d;ravg(a;b)) < b
19. (f rmin(a + d;ravg(a;b))) ≤ ((f a) + (r1/r(k)))
20. (f a) ≤ ((f rmin(a + d;ravg(a;b))) + (r1/r(k)))
21. a < rmin(a + d;ravg(a;b))
22. rmin(a + d;ravg(a;b)) < b
⊢ (f rmin(a + d;ravg(a;b))) < c

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \{b:\mBbbR{}|  a  <  b\} 
3.  f  :  [a,  b]  {}\mrightarrow{}\mBbbR{}
4.  (a,  b)  \msubseteq{}  [a,  b] 
5.  a  <  b
6.  \mforall{}a',b':\mBbbR{}.    (((a  <  a')  \mwedge{}  (a'  <  b')  \mwedge{}  (b'  <  b))  {}\mRightarrow{}  (\mforall{}c:\mBbbR{}.  locally-non-constant(f;a';b';c)))
7.  c  :  \mBbbR{}
8.  (f  a)  <  c
9.  c  <  (f  b)
10.  k  :  \mBbbN{}\msupplus{}
11.  (r1/r(k))  <  (c  -  f  a)
12.  d  :  \mBbbR{}
13.  r0  <  d
14.  \mforall{}x,y:\mBbbR{}.
            (((a  \mleq{}  x)  \mwedge{}  (x  \mleq{}  b))  {}\mRightarrow{}  ((a  \mleq{}  y)  \mwedge{}  (y  \mleq{}  b))  {}\mRightarrow{}  (|x  -  y|  \mleq{}  d)  {}\mRightarrow{}  (|(f  x)  -  f  y|  \mleq{}  (r1/r(k))))
15.  a  <  ravg(a;b)
16.  ravg(a;b)  <  b
17.  a  <  rmin(a  +  d;ravg(a;b))
18.  rmin(a  +  d;ravg(a;b))  <  b
19.  ((f  rmin(a  +  d;ravg(a;b)))  -  (r1/r(k)))  \mleq{}  (f  a)
20.  (f  a)  \mleq{}  ((f  rmin(a  +  d;ravg(a;b)))  +  (r1/r(k)))
21.  a  <  rmin(a  +  d;ravg(a;b))
22.  rmin(a  +  d;ravg(a;b))  <  b
\mvdash{}  (f  rmin(a  +  d;ravg(a;b)))  <  c


By

---

Latex:
(nRAdd  \mkleeneopen{}(r1/r(k))\mkleeneclose{}  (-4)\mcdot{}  THENA  Auto)

---

Home Index