---

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


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)))))])
BY
{ (D -2
   THEN (Assert (a1 ∈ [a, b]) ∧ (f(a1) ≤ c) BY
               (Unhide THEN Auto))
   THEN Thin (-3)
   THEN D -2
   THEN (Assert (b1 ∈ [a, b]) ∧ (c ≤ f(b1)) ∧ (a1 < b1) BY
               (Unhide THEN Auto))
   THEN Thin (-3)
   THEN (Assert (a1 < ((r(2) * a1) + b1/r(3)))
               ∧ (((r(2) * a1) + b1/r(3)) < ((r(2) * b1) + a1/r(3)))
               ∧ (((r(2) * b1) + a1/r(3)) < b1) BY
               (Auto THEN nRMul ⌜r(3)⌝ 0⋅ 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 : ℝ
11. b1 : ℝ
12. (a1 ∈ [a, b]) ∧ (f(a1) ≤ c)
13. (b1 ∈ [a, b]) ∧ (c ≤ f(b1)) ∧ (a1 < b1)
14. (a1 < ((r(2) * a1) + b1/r(3)))
∧ (((r(2) * a1) + b1/r(3)) < ((r(2) * b1) + a1/r(3)))
∧ (((r(2) * b1) + a1/r(3)) < 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:

1.  a  :  \mBbbR{}
2.  b  :  \{b:\mBbbR{}|  a  <  b\} 
3.  f  :  [a,  b]  {}\mrightarrow{}\mBbbR{}
4.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .    ((x  =  y)  {}\mRightarrow{}  (f[x]  =  f[y]))
5.  a  \mleq{}  b
6.  c  :  \mBbbR{}
7.  f(a)  \mleq{}  c
8.  c  \mleq{}  f(b)
9.  locally-non-constant(f;a;b;c)
10.  a1  :  \{a1:\mBbbR{}|  (a1  \mmember{}  [a,  b])  \mwedge{}  (f(a1)  \mleq{}  c)\} 
11.  b1  :  \{b1:\mBbbR{}|  (b1  \mmember{}  [a,  b])  \mwedge{}  (c  \mleq{}  f(b1))  \mwedge{}  (a1  <  b1)\} 
\mvdash{}  \mexists{}a2:\{a2:\mBbbR{}|  (a2  \mmember{}  [a,  b])  \mwedge{}  (f(a2)  \mleq{}  c)\} 
      (\mexists{}b2:\{b2:\mBbbR{}|  (b2  \mmember{}  [a,  b])  \mwedge{}  (c  \mleq{}  f(b2))\}    [((a1  \mleq{}  a2)
                                                                              \mwedge{}  (a2  <  b2)
                                                                              \mwedge{}  (b2  \mleq{}  b1)
                                                                              \mwedge{}  ((b2  -  a2)  \mleq{}  ((b1  -  a1)  *  (r(2)/r(3)))))])


By

---

Latex:
(D  -2
  THEN  (Assert  (a1  \mmember{}  [a,  b])  \mwedge{}  (f(a1)  \mleq{}  c)  BY
                          (Unhide  THEN  Auto))
  THEN  Thin  (-3)
  THEN  D  -2
  THEN  (Assert  (b1  \mmember{}  [a,  b])  \mwedge{}  (c  \mleq{}  f(b1))  \mwedge{}  (a1  <  b1)  BY
                          (Unhide  THEN  Auto))
  THEN  Thin  (-3)
  THEN  (Assert  (a1  <  ((r(2)  *  a1)  +  b1/r(3)))
                          \mwedge{}  (((r(2)  *  a1)  +  b1/r(3))  <  ((r(2)  *  b1)  +  a1/r(3)))
                          \mwedge{}  (((r(2)  *  b1)  +  a1/r(3))  <  b1)  BY
                          (Auto  THEN  nRMul  \mkleeneopen{}r(3)\mkleeneclose{}  0\mcdot{}  THEN  Auto)))

---

Home Index