---

Step * 1 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. 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
BY
{ (Assert Σ{f[g (k + 1)] - f[g k] | 0≤k≤M - 1} = r0 BY
         (InstLemma `rsum-telescopes` [⌜0⌝;⌜M - 1⌝;⌜λ2k.f[g (k + 1)]⌝;⌜λ2k.f[g k]⌝]⋅ 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. 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))
22. Σ{f[g (k + 1)] - f[g k] | 0≤k≤M - 1} = (f[g ((M - 1) + 1)] - f[g 0])
⊢ Σ{f[g (k + 1)] - f[g k] | 0≤k≤M - 1} = r0

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


By

---

Latex:
(Assert  \mSigma{}\{f[g  (k  +  1)]  -  f[g  k]  |  0\mleq{}k\mleq{}M  -  1\}  =  r0  BY
              (InstLemma  `rsum-telescopes`  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}M  -  1\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}k.f[g  (k  +  1)]\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}k.f[g  k]\mkleeneclose{}]\mcdot{}  THEN  Auto))\mcdot{}

---

Home Index