---

Step * of Lemma IVT-locally-non-constant

∀a:ℝ. ∀b:{b:ℝ| a < b} . ∀f:[a, b] ⟶ℝ.
  ∀c:ℝ. ((f(a) ≤ c) ⇒ (c ≤ f(b)) ⇒ locally-non-constant(f;a;b;c) ⇒ (∃x:ℝ [((x ∈ [a, b]) ∧ (f(x) = c))])) 
  supposing ∀x,y:{x:ℝ| x ∈ [a, b]} .  ((x = y) ⇒ (f[x] = f[y]))
BY
{ (InstLemma `intermediate-value-lemma\'` []
   THEN RepeatFor 4 ((ParallelLast' THENA Auto))
   THEN (Assert a ≤ b BY
               (DVar `b' THEN Unhide THEN Auto))
   THEN Auto
   THEN (BHyp 5 THENA Auto)
   THEN Thin 5
   THEN InstConcl [⌜(r(2)/r(3))⌝]⋅
   THEN Auto) }

1
1. a : ℝ
2. b : {b:ℝ| a < b} 
3. f : [a, b] ⟶ℝ
4. ∀x,y:{x:ℝ| x ∈ [a, b]} .  ((x = y) ⇒ (f[x] = f[y]))
5. a ≤ b
6. c : ℝ
7. f(a) ≤ c
8. c ≤ f(b)
9. locally-non-constant(f;a;b;c)
10. a1 : {a1:ℝ| (a1 ∈ [a, b]) ∧ (f(a1) ≤ c)} 
11. b1 : {b1:ℝ| (b1 ∈ [a, b]) ∧ (c ≤ f(b1)) ∧ (a1 < b1)} 
⊢ ∃a2:{a2:ℝ| (a2 ∈ [a, b]) ∧ (f(a2) ≤ c)} . (∃b2:{b2:ℝ| (b2 ∈ [a, b]) ∧ (c ≤ f(b2))}  [((a1 ≤ a2) ∧ (a2 < b2) ∧ (b2 ≤ b1\000C) ∧ ((b2 - a2) ≤ ((b1 - a1) * (r(2)/r(3)))))])

---

Latex:

---

Latex:
\mforall{}a:\mBbbR{}.  \mforall{}b:\{b:\mBbbR{}|  a  <  b\}  .  \mforall{}f:[a,  b]  {}\mrightarrow{}\mBbbR{}.
    \mforall{}c:\mBbbR{}
        ((f(a)  \mleq{}  c)
        {}\mRightarrow{}  (c  \mleq{}  f(b))
        {}\mRightarrow{}  locally-non-constant(f;a;b;c)
        {}\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:
(InstLemma  `intermediate-value-lemma\mbackslash{}'`  []
  THEN  RepeatFor  4  ((ParallelLast'  THENA  Auto))
  THEN  (Assert  a  \mleq{}  b  BY
                          (DVar  `b'  THEN  Unhide  THEN  Auto))
  THEN  Auto
  THEN  (BHyp  5  THENA  Auto)
  THEN  Thin  5
  THEN  InstConcl  [\mkleeneopen{}(r(2)/r(3))\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index