---

Step * 1 1 1 of Lemma Rolles-theorem


1. a : ℝ
2. b : ℝ
3. a < b
4. f : [a, b] ⟶ℝ
5. f' : [a, b] ⟶ℝ
6. f'[x] continuous for x ∈ [a, b]
7. d(f[x])/dx = λx.f'[x] on [a, b]
8. f[a] = f[b]
9. e : ℝ
10. r0 < e
11. mc : |f'[x]| continuous for x ∈ [a, b]
12. icompact([a, b])
13. r0 < inf{|f'[x]||x ∈ [a, b]}
⊢ False
BY
{ (Assert ∃k:ℕ+. ∀x:ℝ. ((x ∈ [a, b]) ⇒ ((r1/r(k)) ≤ |f'[x]|)) BY
         (InstLemma `small-reciprocal-real` [⌜inf{|f'[x]||x ∈ [a, b]}⌝]⋅
          THEN Auto
          THEN D -1
          THEN With ⌜k⌝ (D 0)⋅
          THEN Auto
          THEN ((InstLemma `range-inf-property` [⌜[a, b]⌝;⌜λ2x.|f'[x]|⌝;⌜mc⌝]⋅ THENA Auto)
                THEN D (-1)
                THEN Thin (-1)
                THEN With ⌜|f'[x]|⌝ (D (-1))⋅
                THEN Auto
                THEN D -1
                THEN Auto
                THEN RepUR ``rset-member rrange`` 0
                THEN With ⌜x⌝ (D 0)⋅
                THEN Auto)⋅)) }

1
1. a : ℝ
2. b : ℝ
3. a < b
4. f : [a, b] ⟶ℝ
5. f' : [a, b] ⟶ℝ
6. f'[x] continuous for x ∈ [a, b]
7. d(f[x])/dx = λx.f'[x] on [a, b]
8. f[a] = f[b]
9. e : ℝ
10. r0 < e
11. mc : |f'[x]| continuous for x ∈ [a, b]
12. icompact([a, b])
13. r0 < inf{|f'[x]||x ∈ [a, b]}
14. ∃k:ℕ+. ∀x:ℝ. ((x ∈ [a, b]) ⇒ ((r1/r(k)) ≤ |f'[x]|))
⊢ False

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  a  <  b
4.  f  :  [a,  b]  {}\mrightarrow{}\mBbbR{}
5.  f'  :  [a,  b]  {}\mrightarrow{}\mBbbR{}
6.  f'[x]  continuous  for  x  \mmember{}  [a,  b]
7.  d(f[x])/dx  =  \mlambda{}x.f'[x]  on  [a,  b]
8.  f[a]  =  f[b]
9.  e  :  \mBbbR{}
10.  r0  <  e
11.  mc  :  |f'[x]|  continuous  for  x  \mmember{}  [a,  b]
12.  icompact([a,  b])
13.  r0  <  inf\{|f'[x]||x  \mmember{}  [a,  b]\}
\mvdash{}  False


By

---

Latex:
(Assert  \mexists{}k:\mBbbN{}\msupplus{}.  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  [a,  b])  {}\mRightarrow{}  ((r1/r(k))  \mleq{}  |f'[x]|))  BY
              (InstLemma  `small-reciprocal-real`  [\mkleeneopen{}inf\{|f'[x]||x  \mmember{}  [a,  b]\}\mkleeneclose{}]\mcdot{}
                THEN  Auto
                THEN  D  -1
                THEN  With  \mkleeneopen{}k\mkleeneclose{}  (D  0)\mcdot{}
                THEN  Auto
                THEN  ((InstLemma  `range-inf-property`  [\mkleeneopen{}[a,  b]\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.|f'[x]|\mkleeneclose{};\mkleeneopen{}mc\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  D  (-1)
                            THEN  Thin  (-1)
                            THEN  With  \mkleeneopen{}|f'[x]|\mkleeneclose{}  (D  (-1))\mcdot{}
                            THEN  Auto
                            THEN  D  -1
                            THEN  Auto
                            THEN  RepUR  ``rset-member  rrange``  0
                            THEN  With  \mkleeneopen{}x\mkleeneclose{}  (D  0)\mcdot{}
                            THEN  Auto)\mcdot{}))

---

Home Index