---

Step * 1 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]}
14. ∃k:ℕ+. ∀x:ℝ. ((x ∈ [a, b]) ⇒ ((r1/r(k)) ≤ |f'[x]|))
⊢ False
BY
{ (Thin (-2)
   THEN D -1
   THEN (FLemma `rabs-nonzero-on-compact` [-1] THENA Auto)
   THEN Thin (-2)
   THEN (With ⌜2 * k⌝ (D 7)⋅ THENA Auto)
   THEN (With ⌜1⌝ (D (-1))⋅ THENA (Auto THEN RepUR ``i-approx iproper`` 0 THEN MemTypeCD THEN Auto))
   THEN RepUR ``i-approx`` (-1)
   THEN RepeatFor 2 (D -1)
   THEN (InstLemma `simple-partition-exists` [⌜a⌝;⌜b⌝;⌜del⌝]⋅ THENA Auto)
   THEN ExRepD) }

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. f[a] = f[b]
8. e : ℝ
9. r0 < e
10. mc : |f'[x]| continuous for x ∈ [a, b]
11. icompact([a, b])
12. k : ℕ+
13. (∀x:ℝ. ((x ∈ [a, b]) ⇒ ((r1/r(k)) ≤ f'[x]))) ∨ (∀x:ℝ. ((x ∈ [a, b]) ⇒ (f'[x] ≤ (r(-1)/r(k)))))
14. del : ℝ
15. r0 < del
16. ∀x,y:ℝ.
      (((a ≤ x) ∧ (x ≤ b))
      ⇒ ((a ≤ y) ∧ (y ≤ b))
      ⇒ (|y - x| ≤ del)
      ⇒ (|f[y] - f[x] - f'[x] * (y - x)| ≤ ((r1/r(2 * k)) * |y - x|)))
17. M : ℕ+
18. g : ℕM + 1 ⟶ {x:ℝ| x ∈ [a, b]} 
19. (g 0) = a ∈ ℝ
20. (g M) = b ∈ ℝ
21. ∀i:ℕM. (((g i) ≤ (g (i + 1))) ∧ (((g (i + 1)) - g i) ≤ del))
⊢ 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]\}
14.  \mexists{}k:\mBbbN{}\msupplus{}.  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  [a,  b])  {}\mRightarrow{}  ((r1/r(k))  \mleq{}  |f'[x]|))
\mvdash{}  False


By

---

Latex:
(Thin  (-2)
  THEN  D  -1
  THEN  (FLemma  `rabs-nonzero-on-compact`  [-1]  THENA  Auto)
  THEN  Thin  (-2)
  THEN  (With  \mkleeneopen{}2  *  k\mkleeneclose{}  (D  7)\mcdot{}  THENA  Auto)
  THEN  (With  \mkleeneopen{}1\mkleeneclose{}  (D  (-1))\mcdot{}  THENA  (Auto  THEN  RepUR  ``i-approx  iproper``  0  THEN  MemTypeCD  THEN  Auto))
  THEN  RepUR  ``i-approx``  (-1)
  THEN  RepeatFor  2  (D  -1)
  THEN  (InstLemma  `simple-partition-exists`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}del\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD)

---

Home Index