---

Step * of Lemma IVT-strict-monotonic

∀I:Interval. ∀f:I ⟶ℝ.
  (((∀x,y:{x:ℝ| x ∈ I} .  ((x < y) ⇒ ((f x) < (f y)))) ∨ (∀x,y:{x:ℝ| x ∈ I} .  ((x < y) ⇒ ((f y) < (f x)))))
  ⇒ (∀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))) ∨ (((f b) ≤ x) ∧ (x ≤ (f a))))
              ⇒ (∃c:ℝ. ((((a ≤ c) ∧ (c ≤ b)) ∨ ((b ≤ c) ∧ (c ≤ a))) ∧ ((f c) = x))))))))
BY
{ (Auto
   THEN ((Assert [a, b] ⊆ I  BY EAuto 1) THEN (Assert [b, a] ⊆ I  BY EAuto 1))
   THEN ((D 3
          THENL [(InstLemma `IVT-strict-increasing` [⌜I⌝;⌜f⌝]⋅ THENA Auto)
                ; (InstLemma `IVT-strict-decreasing` [⌜I⌝;⌜f⌝]⋅ THENA Auto)]
         )
         THEN D 7
         THEN D -4
         THEN Try (((Assert ⌜False⌝⋅ THEN Auto) THEN FHyp 3 [-7] THEN Complete (Auto)))
         THEN ((InstHyp [⌜a⌝;⌜b⌝;⌜x⌝] (-1)⋅ THENA Complete (Auto))
         ORELSE (InstHyp [⌜b⌝;⌜a⌝;⌜x⌝] (-1)⋅ THENA Complete (Auto))
         )
         THEN D -1
         THEN (Assert c ∈ I BY
                     Auto)
         THEN D 0 With ⌜c⌝ 
         THEN Auto
         THEN Try ((Unhide THEN Auto))
         THEN D -1
         THEN Auto)⋅) }

---

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))))
      \mvee{}  (\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  <  y)  {}\mRightarrow{}  ((f  y)  <  (f  x)))))
    {}\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  \mneq{}  b
                {}\mRightarrow{}  (\mforall{}x:\mBbbR{}
                            (((((f  a)  \mleq{}  x)  \mwedge{}  (x  \mleq{}  (f  b)))  \mvee{}  (((f  b)  \mleq{}  x)  \mwedge{}  (x  \mleq{}  (f  a))))
                            {}\mRightarrow{}  (\mexists{}c:\mBbbR{}.  ((((a  \mleq{}  c)  \mwedge{}  (c  \mleq{}  b))  \mvee{}  ((b  \mleq{}  c)  \mwedge{}  (c  \mleq{}  a)))  \mwedge{}  ((f  c)  =  x))))))))


By

---

Latex:
(Auto
  THEN  ((Assert  [a,  b]  \msubseteq{}  I    BY  EAuto  1)  THEN  (Assert  [b,  a]  \msubseteq{}  I    BY  EAuto  1))
  THEN  ((D  3
                THENL  [(InstLemma  `IVT-strict-increasing`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            ;  (InstLemma  `IVT-strict-decreasing`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)]
              )
              THEN  D  7
              THEN  D  -4
              THEN  Try  (((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  FHyp  3  [-7]  THEN  Complete  (Auto)))
              THEN  ((InstHyp  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  (-1)\mcdot{}  THENA  Complete  (Auto))
              ORELSE  (InstHyp  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  (-1)\mcdot{}  THENA  Complete  (Auto))
              )
              THEN  D  -1
              THEN  (Assert  c  \mmember{}  I  BY
                                      Auto)
              THEN  D  0  With  \mkleeneopen{}c\mkleeneclose{} 
              THEN  Auto
              THEN  Try  ((Unhide  THEN  Auto))
              THEN  D  -1
              THEN  Auto)\mcdot{})

---

Home Index