---

Step * of Lemma IVT-strict-increasing

∀I:Interval. ∀f:I ⟶ℝ.
  ((∀x,y:{x:ℝ| x ∈ I} .  ((x < y) ⇒ ((f x) < (f y))))
  ⇒ (∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ ((f x) = (f y))))
  ⇒ (∀a,b:{x:ℝ| x ∈ I} .
        ((a < b) ⇒ (∀x:ℝ. ((((f a) ≤ x) ∧ (x ≤ (f b))) ⇒ (∃c:ℝ [(((a ≤ c) ∧ (c ≤ b)) ∧ ((f c) = x))]))))))
BY
{ (Auto
   THEN (InstLemma `strict-monotonic-is-locally-non-constant`  [⌜I⌝;⌜f⌝;⌜a⌝;⌜b⌝;⌜x⌝] ⋅ THENA Auto)
   THEN (Assert [a, b] ⊆ I  BY
               (D 0 THEN Reduce 0 THEN Auto THEN InstLemma `i-member-between` [⌜I⌝;⌜a⌝;⌜b⌝]⋅ THEN Auto))
   THEN (InstLemma `IVT-locally-non-constant` [⌜a⌝;⌜b⌝;⌜f⌝;⌜x⌝]⋅ THENM Reduce -1)
   THEN Auto
   THEN Unfold `r-ap` -1
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}f:I  {}\mrightarrow{}\mBbbR{}.
    ((\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  <  y)  {}\mRightarrow{}  ((f  x)  <  (f  y))))
    {}\mRightarrow{}  (\mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  ((f  x)  =  (f  y))))
    {}\mRightarrow{}  (\mforall{}a,b:\{x:\mBbbR{}|  x  \mmember{}  I\}  .
                ((a  <  b)
                {}\mRightarrow{}  (\mforall{}x:\mBbbR{}.  ((((f  a)  \mleq{}  x)  \mwedge{}  (x  \mleq{}  (f  b)))  {}\mRightarrow{}  (\mexists{}c:\mBbbR{}  [(((a  \mleq{}  c)  \mwedge{}  (c  \mleq{}  b))  \mwedge{}  ((f  c)  =  x))]))))))


By

---

Latex:
(Auto
  THEN  (InstLemma  `strict-monotonic-is-locally-non-constant`    [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  \mcdot{}  THENA  Auto)
  THEN  (Assert  [a,  b]  \msubseteq{}  I    BY
                          (D  0
                            THEN  Reduce  0
                            THEN  Auto
                            THEN  InstLemma  `i-member-between`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}
                            THEN  Auto))
  THEN  (InstLemma  `IVT-locally-non-constant`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENM  Reduce  -1)
  THEN  Auto
  THEN  Unfold  `r-ap`  -1
  THEN  Trivial)

---

Home Index