---

Step * of Lemma IVT-strict-decreasing

No Annotations
∀I:Interval. ∀f:I ⟶ℝ.
  ((∀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 b) ≤ x) ∧ (x ≤ (f a))) ⇒ (∃c:ℝ. (((a ≤ c) ∧ (c ≤ b)) ∧ ((f c) = x))))))))
BY
{ ((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-strict-increasing` [⌜I⌝;⌜λx.-(f x)⌝;⌜a⌝;⌜b⌝;⌜-(x)⌝]⋅ THENA Auto)
   THEN All Reduce
   THEN Auto) }

1
1. I : Interval
2. f : I ⟶ℝ
3. ∀x,y:{x:ℝ| x ∈ I} .  ((x < y) ⇒ ((f y) < (f x)))
4. ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ ((f x) = (f y)))
5. a : {x:ℝ| x ∈ I} 
6. b : {x:ℝ| x ∈ I} 
7. a < b
8. x : ℝ
9. (f b) ≤ x
10. x ≤ (f a)
11. [a, b] ⊆ I 
12. x1 : {x:ℝ| x ∈ I} 
13. y : {x:ℝ| x ∈ I} 
14. x1 < y
⊢ -(f x1) < -(f y)

2
1. I : Interval
2. f : I ⟶ℝ
3. ∀x,y:{x:ℝ| x ∈ I} .  ((x < y) ⇒ ((f y) < (f x)))
4. ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ ((f x) = (f y)))
5. a : {x:ℝ| x ∈ I} 
6. b : {x:ℝ| x ∈ I} 
7. a < b
8. x : ℝ
9. (f b) ≤ x
10. x ≤ (f a)
11. [a, b] ⊆ I 
12. ∃c:ℝ [(((a ≤ c) ∧ (c ≤ b)) ∧ (-(f c) = -(x)))]
⊢ ∃c:ℝ. (((a ≤ c) ∧ (c ≤ b)) ∧ ((f c) = x))

---

Latex:

---

Latex:
No  Annotations
\mforall{}I:Interval.  \mforall{}f:I  {}\mrightarrow{}\mBbbR{}.
    ((\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  <  b)
                {}\mRightarrow{}  (\mforall{}x:\mBbbR{}.  ((((f  b)  \mleq{}  x)  \mwedge{}  (x  \mleq{}  (f  a)))  {}\mRightarrow{}  (\mexists{}c:\mBbbR{}.  (((a  \mleq{}  c)  \mwedge{}  (c  \mleq{}  b))  \mwedge{}  ((f  c)  =  x))))))))


By

---

Latex:
((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-strict-increasing`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}\mlambda{}x.-(f  x)\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}-(x)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  All  Reduce
  THEN  Auto)

---

Home Index