---

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

∀a:ℝ. ∀b:{b:ℝ| a < b} . ∀f:[a, b] ⟶ℝ.
  (∀a',b':ℝ.  (((a < a') ∧ (a' < b') ∧ (b' < b)) ⇒ (∀c:ℝ. locally-non-constant(f;a';b';c))))
  ⇒ (∀c:ℝ. ((f(a) < c) ⇒ (c < f(b)) ⇒ (∃x:ℝ. ((x ∈ (a, b)) ∧ (f(x) = c))))) 
  supposing ∀x,y:{x:ℝ| x ∈ [a, b]} .  ((x = y) ⇒ (f[x] = f[y]))
BY
{ (RepeatFor 3 (Intro)
   THEN (Assert (a, b) ⊆ [a, b]  BY
               (D 0 THEN Reduce 0 THEN Auto))
   THEN (Assert a < b BY
               Auto)
   THEN Auto
   THEN Reduce 0
   THEN Auto
   THEN (Assert f[x] continuous for x ∈ [a, b] BY
               EAuto 1)
   THEN Thin 6
   THEN PromoteHyp (-1) 6) }

1
1. a : ℝ
2. b : {b:ℝ| a < b} 
3. f : [a, b] ⟶ℝ
4. (a, b) ⊆ [a, b] 
5. a < b
6. f[x] continuous for x ∈ [a, b]
7. ∀a',b':ℝ.  (((a < a') ∧ (a' < b') ∧ (b' < b)) ⇒ (∀c:ℝ. locally-non-constant(f;a';b';c)))
8. c : ℝ
9. f(a) < c
10. c < f(b)
⊢ ∃x:ℝ. (((a < x) ∧ (x < b)) ∧ (f(x) = c))

---

Latex:

---

Latex:
\mforall{}a:\mBbbR{}.  \mforall{}b:\{b:\mBbbR{}|  a  <  b\}  .  \mforall{}f:[a,  b]  {}\mrightarrow{}\mBbbR{}.
    (\mforall{}a',b':\mBbbR{}.    (((a  <  a')  \mwedge{}  (a'  <  b')  \mwedge{}  (b'  <  b))  {}\mRightarrow{}  (\mforall{}c:\mBbbR{}.  locally-non-constant(f;a';b';c))))
    {}\mRightarrow{}  (\mforall{}c:\mBbbR{}.  ((f(a)  <  c)  {}\mRightarrow{}  (c  <  f(b))  {}\mRightarrow{}  (\mexists{}x:\mBbbR{}.  ((x  \mmember{}  (a,  b))  \mwedge{}  (f(x)  =  c))))) 
    supposing  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .    ((x  =  y)  {}\mRightarrow{}  (f[x]  =  f[y]))


By

---

Latex:
(RepeatFor  3  (Intro)
  THEN  (Assert  (a,  b)  \msubseteq{}  [a,  b]    BY
                          (D  0  THEN  Reduce  0  THEN  Auto))
  THEN  (Assert  a  <  b  BY
                          Auto)
  THEN  Auto
  THEN  Reduce  0
  THEN  Auto
  THEN  (Assert  f[x]  continuous  for  x  \mmember{}  [a,  b]  BY
                          EAuto  1)
  THEN  Thin  6
  THEN  PromoteHyp  (-1)  6)

---

Home Index