---

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


1. a : ℝ
2. b : {b:ℝ| a < b} 
3. f : [a, b] ⟶ℝ
4. (a, b) ⊆ [a, b] 
5. a < b
6. ∀a',b':ℝ.  (((a < a') ∧ (a' < b') ∧ (b' < b)) ⇒ (∀c:ℝ. locally-non-constant(f;a';b';c)))
7. c : ℝ
8. f(a) < c
9. c < f(b)
10. ∀n:ℕ+
      (∃d:ℝ [((r0 < d)
            ∧ (∀x,y:ℝ.  (((a ≤ x) ∧ (x ≤ b)) ⇒ ((a ≤ y) ∧ (y ≤ b)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(n))))))])
⊢ ∃a':ℝ. (((a < a') ∧ (a' < b)) ∧ (f(a') < c))
BY
{ ((InstLemma `small-reciprocal-real` [⌜c - f(a)⌝]⋅
    THENA (Auto THEN (MemTypeCD THEN Auto) THEN nRAdd ⌜f(a)⌝ 0⋅ THEN Auto)
    )
   THEN ExRepD
   THEN (D -3 With ⌜k⌝  THENA Auto)
   THEN ExRepD) }

1
1. a : ℝ
2. b : {b:ℝ| a < b} 
3. f : [a, b] ⟶ℝ
4. (a, b) ⊆ [a, b] 
5. a < b
6. ∀a',b':ℝ.  (((a < a') ∧ (a' < b') ∧ (b' < b)) ⇒ (∀c:ℝ. locally-non-constant(f;a';b';c)))
7. c : ℝ
8. f(a) < c
9. c < f(b)
10. k : ℕ+
11. (r1/r(k)) < (c - f(a))
12. d : ℝ
13. r0 < d
14. ∀x,y:ℝ.  (((a ≤ x) ∧ (x ≤ b)) ⇒ ((a ≤ y) ∧ (y ≤ b)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(k))))
⊢ ∃a':ℝ. (((a < a') ∧ (a' < b)) ∧ (f(a') < c))

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \{b:\mBbbR{}|  a  <  b\} 
3.  f  :  [a,  b]  {}\mrightarrow{}\mBbbR{}
4.  (a,  b)  \msubseteq{}  [a,  b] 
5.  a  <  b
6.  \mforall{}a',b':\mBbbR{}.    (((a  <  a')  \mwedge{}  (a'  <  b')  \mwedge{}  (b'  <  b))  {}\mRightarrow{}  (\mforall{}c:\mBbbR{}.  locally-non-constant(f;a';b';c)))
7.  c  :  \mBbbR{}
8.  f(a)  <  c
9.  c  <  f(b)
10.  \mforall{}n:\mBbbN{}\msupplus{}
            (\mexists{}d:\mBbbR{}  [((r0  <  d)
                        \mwedge{}  (\mforall{}x,y:\mBbbR{}.
                                  (((a  \mleq{}  x)  \mwedge{}  (x  \mleq{}  b))
                                  {}\mRightarrow{}  ((a  \mleq{}  y)  \mwedge{}  (y  \mleq{}  b))
                                  {}\mRightarrow{}  (|x  -  y|  \mleq{}  d)
                                  {}\mRightarrow{}  (|f[x]  -  f[y]|  \mleq{}  (r1/r(n))))))])
\mvdash{}  \mexists{}a':\mBbbR{}.  (((a  <  a')  \mwedge{}  (a'  <  b))  \mwedge{}  (f(a')  <  c))


By

---

Latex:
((InstLemma  `small-reciprocal-real`  [\mkleeneopen{}c  -  f(a)\mkleeneclose{}]\mcdot{}
    THENA  (Auto  THEN  (MemTypeCD  THEN  Auto)  THEN  nRAdd  \mkleeneopen{}f(a)\mkleeneclose{}  0\mcdot{}  THEN  Auto)
    )
  THEN  ExRepD
  THEN  (D  -3  With  \mkleeneopen{}k\mkleeneclose{}    THENA  Auto)
  THEN  ExRepD)

---

Home Index