---

Step * 1 1 1 1 1 2 1 1 1 1 1 1 1 1 3 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))
22. v : ℝ
23. Σ{f[g (i + 1)] - f[g i] - f'[g i] * ((g (i + 1)) - g i) | 0≤i≤M - 1} = v ∈ ℝ
24. (Σ{f'[g k] * ((g (k + 1)) - g k) | 0≤k≤M - 1} + v) = r0
25. |v| ≤ ((r1/r(2 * k)) * (b - a))
26. (Σ{(r1/r(k)) * ((g (i + 1)) - g i) | 0≤i≤M - 1} ≤ Σ{f'[g k] * ((g (k + 1)) - g k) | 0≤k≤M - 1})
∨ (Σ{f'[g k] * ((g (k + 1)) - g k) | 0≤k≤M - 1} ≤ Σ{(r(-1)/r(k)) * ((g (i + 1)) - g i) | 0≤i≤M - 1})
⊢ False
BY
{ ((RWO "rsum_linearity2" (-1) THENA Auto)
   THEN (Assert Σ{(g (k + 1)) - g k | 0≤k≤M - 1} = (b - a) BY
               (InstLemma `rsum-telescopes` [⌜0⌝;⌜M - 1⌝;⌜λ2k.g (k + 1)⌝;⌜λ2k.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. v : ℝ
23. Σ{f[g (i + 1)] - f[g i] - f'[g i] * ((g (i + 1)) - g i) | 0≤i≤M - 1} = v ∈ ℝ
24. (Σ{f'[g k] * ((g (k + 1)) - g k) | 0≤k≤M - 1} + v) = r0
25. |v| ≤ ((r1/r(2 * k)) * (b - a))
26. (((r1/r(k)) * Σ{(g (i + 1)) - g i | 0≤i≤M - 1}) ≤ Σ{f'[g k] * ((g (k + 1)) - g k) | 0≤k≤M - 1})
∨ (Σ{f'[g k] * ((g (k + 1)) - g k) | 0≤k≤M - 1} ≤ ((r(-1)/r(k)) * Σ{(g (i + 1)) - g i | 0≤i≤M - 1}))
27. Σ{(g (k + 1)) - g k | 0≤k≤M - 1} = (b - a)
⊢ 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))
22.  v  :  \mBbbR{}
23.  \mSigma{}\{f[g  (i  +  1)]  -  f[g  i]  -  f'[g  i]  *  ((g  (i  +  1))  -  g  i)  |  0\mleq{}i\mleq{}M  -  1\}  =  v
24.  (\mSigma{}\{f'[g  k]  *  ((g  (k  +  1))  -  g  k)  |  0\mleq{}k\mleq{}M  -  1\}  +  v)  =  r0
25.  |v|  \mleq{}  ((r1/r(2  *  k))  *  (b  -  a))
26.  (\mSigma{}\{(r1/r(k))  *  ((g  (i  +  1))  -  g  i)  |  0\mleq{}i\mleq{}M  -  1\}  \mleq{}  \mSigma{}\{f'[g  k]  *  ((g  (k  +  1))  -  g  k)  |  0\mleq{}k\mleq{}M  -  1\})
\mvee{}  (\mSigma{}\{f'[g  k]  *  ((g  (k  +  1))  -  g  k)  |  0\mleq{}k\mleq{}M  -  1\}  \mleq{}  \mSigma{}\{(r(-1)/r(k))  *  ((g  (i  +  1))  -  g  i)  |  0\mleq{}i\mleq{}M  -  1\})
\mvdash{}  False


By

---

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

---

Home Index