---

Step * 1 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 : ℝ
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)))))])
BY
{ (Assert ∃z:ℝ. ((((r(2) * a1) + b1/r(3)) ≤ z) ∧ (z ≤ ((r(2) * b1) + a1/r(3))) ∧ f(z) ≠ c) BY
         ((Assert locally-non-constant-rational(f;a;b;c) BY
                 ((BLemma `locally-non-constant-via-rational` THEN Auto) THEN EAuto 1))
          THEN All Reduce
          THEN UnfoldTopAb (-1)
          THEN (InstHyp [⌜((r(2) * a1) + b1/r(3))⌝;⌜((r(2) * b1) + a1/r(3))⌝] (-1)⋅ THENA Auto)
          THEN ExRepD
          THEN (Evaluate ⌜nn = n ∈ ℕ+⌝⋅ THENA Auto)
          THEN Eliminate
          ⌜n⌝⋅
          THEN (Evaluate ⌜zz = z ∈ ℤ⌝⋅ THENA Auto)
          THEN Eliminate
          ⌜z⌝⋅
          THEN With ⌜(r(zz))/nn⌝ (D 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)
15. ∃z:ℝ. ((((r(2) * a1) + b1/r(3)) ≤ z) ∧ (z ≤ ((r(2) * b1) + a1/r(3))) ∧ f(z) ≠ c)
⊢ ∃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  :  \mBbbR{}
11.  b1  :  \mBbbR{}
12.  (a1  \mmember{}  [a,  b])  \mwedge{}  (f(a1)  \mleq{}  c)
13.  (b1  \mmember{}  [a,  b])  \mwedge{}  (c  \mleq{}  f(b1))  \mwedge{}  (a1  <  b1)
14.  (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)
\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:
(Assert  \mexists{}z:\mBbbR{}.  ((((r(2)  *  a1)  +  b1/r(3))  \mleq{}  z)  \mwedge{}  (z  \mleq{}  ((r(2)  *  b1)  +  a1/r(3)))  \mwedge{}  f(z)  \mneq{}  c)  BY
              ((Assert  locally-non-constant-rational(f;a;b;c)  BY
                              ((BLemma  `locally-non-constant-via-rational`  THEN  Auto)  THEN  EAuto  1))
                THEN  All  Reduce
                THEN  UnfoldTopAb  (-1)
                THEN  (InstHyp  [\mkleeneopen{}((r(2)  *  a1)  +  b1/r(3))\mkleeneclose{};\mkleeneopen{}((r(2)  *  b1)  +  a1/r(3))\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
                THEN  ExRepD
                THEN  (Evaluate  \mkleeneopen{}nn  =  n\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  Eliminate
                \mkleeneopen{}n\mkleeneclose{}\mcdot{}
                THEN  (Evaluate  \mkleeneopen{}zz  =  z\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  Eliminate
                \mkleeneopen{}z\mkleeneclose{}\mcdot{}
                THEN  With  \mkleeneopen{}(r(zz))/nn\mkleeneclose{}  (D  0)\mcdot{}
                THEN  Auto))

---

Home Index