---

Step * 1 2 1 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. a' : ℝ
11. a < a'
12. a' < b
13. f(a') < c
14. k : ℕ+
15. (r1/r(k)) < (f(b) - c)
16. d : ℝ
17. r0 < d
18. ∀x,y:ℝ.  (((a ≤ x) ∧ (x ≤ b)) ⇒ ((a ≤ y) ∧ (y ≤ b)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(k))))
⊢ ∃b':ℝ. (((a' < b') ∧ (b' < b)) ∧ (c < f(b')))
BY
{ ((InstLemma `ravg-between` [⌜a'⌝;⌜b⌝]⋅ THENA Auto)
   THEN (Assert rmax(b - d;ravg(a';b)) < b BY
               (BLemma `rmax_strict_lb` THEN Auto THEN nRAdd ⌜d - b⌝ 0⋅ THEN Auto))
   THEN (Assert a' < rmax(b - d;ravg(a';b)) BY
               (BLemma `rmax_strict_ub` THEN Auto))
   THEN ((InstHyp [⌜rmax(b - d;ravg(a';b))⌝;⌜b⌝] (-4)⋅ THENM (D 0 With ⌜rmax(b - d;ravg(a';b))⌝  THEN Auto))
         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. a' : ℝ
11. a < a'
12. a' < b
13. f(a') < c
14. k : ℕ+
15. (r1/r(k)) < (f(b) - c)
16. d : ℝ
17. r0 < d
18. ∀x,y:ℝ.  (((a ≤ x) ∧ (x ≤ b)) ⇒ ((a ≤ y) ∧ (y ≤ b)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(k))))
19. a' < ravg(a';b)
20. ravg(a';b) < b
21. rmax(b - d;ravg(a';b)) < b
22. a' < rmax(b - d;ravg(a';b))
⊢ |rmax(b - d;ravg(a';b)) - b| ≤ d

2
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. a' : ℝ
11. a < a'
12. a' < b
13. f(a') < c
14. k : ℕ+
15. (r1/r(k)) < (f(b) - c)
16. d : ℝ
17. r0 < d
18. ∀x,y:ℝ.  (((a ≤ x) ∧ (x ≤ b)) ⇒ ((a ≤ y) ∧ (y ≤ b)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(k))))
19. a' < ravg(a';b)
20. ravg(a';b) < b
21. rmax(b - d;ravg(a';b)) < b
22. a' < rmax(b - d;ravg(a';b))
23. |f[rmax(b - d;ravg(a';b))] - f[b]| ≤ (r1/r(k))
24. a' < rmax(b - d;ravg(a';b))
25. rmax(b - d;ravg(a';b)) < b
⊢ c < f(rmax(b - d;ravg(a';b)))

---

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.  a'  :  \mBbbR{}
11.  a  <  a'
12.  a'  <  b
13.  f(a')  <  c
14.  k  :  \mBbbN{}\msupplus{}
15.  (r1/r(k))  <  (f(b)  -  c)
16.  d  :  \mBbbR{}
17.  r0  <  d
18.  \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))))
\mvdash{}  \mexists{}b':\mBbbR{}.  (((a'  <  b')  \mwedge{}  (b'  <  b))  \mwedge{}  (c  <  f(b')))


By

---

Latex:
((InstLemma  `ravg-between`  [\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  rmax(b  -  d;ravg(a';b))  <  b  BY
                          (BLemma  `rmax\_strict\_lb`  THEN  Auto  THEN  nRAdd  \mkleeneopen{}d  -  b\mkleeneclose{}  0\mcdot{}  THEN  Auto))
  THEN  (Assert  a'  <  rmax(b  -  d;ravg(a';b))  BY
                          (BLemma  `rmax\_strict\_ub`  THEN  Auto))
  THEN  ((InstHyp  [\mkleeneopen{}rmax(b  -  d;ravg(a';b))\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]  (-4)\mcdot{}
              THENM  (D  0  With  \mkleeneopen{}rmax(b  -  d;ravg(a';b))\mkleeneclose{}    THEN  Auto)
              )
              THENA  Auto
              ))

---

Home Index