Proof of Nuprl Lemma : Rolles-theorem

Step * 1 1 1 1 1 2 1 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))
22. (Σ{f'[g k] * ((g (k + 1)) - g k) | 0≤k≤M - 1}
+ Σ{f[g (k + 1)] - f[g k] - f'[g k] * ((g (k + 1)) - g k) | 0≤k≤M - 1})
= r0

23. |Σ{f[g (i + 1)] - f[g i] - f'[g i] * ((g (i + 1)) - g i) | 0≤i≤M - 1}| ≤ ((r1/r(2 * k))

* Σ{|(g (i + 1)) - g i| | 0≤i≤M - 1})
⊢ False
BY

{ (Assert |Σ{f[g (i + 1)] - f[g i] - f'[g i] * ((g (i + 1)) - g i) | 0≤i≤M - 1}| ≤ ((r1/r(2 * k)) * (b - a)) BY

((Assert Σ{(g (k + 1)) - g k | 0≤k≤M - 1} = (b - a) BY

                 (InstLemma `rsum-telescopes` [⌜0⌝;⌜M - 1⌝;⌜λ₂k.g (k + 1)⌝;⌜λ₂k.g k⌝]⋅ THEN Auto))⋅

          THEN (Assert Σ{|(g (i + 1)) - g i| | 0≤i≤M - 1} = Σ{(g (k + 1)) - g k | 0≤k≤M - 1} BY

                      (BLemma `rsum_functionality`
                       THEN Auto
                       THEN (D 0 THEN Auto)
                       THEN RWO "rabs-of-nonneg" 0
                       THEN Auto
                       THEN nRAdd ⌜g k1⌝ 0⋅
                       THEN Auto))
          THEN (RWO "-3" 0 THENA Auto)
          THEN RWW "-1 -2" 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. 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] * ((g (k + 1)) - g k) | 0≤k≤M - 1}
+ Σ{f[g (k + 1)] - f[g k] - f'[g k] * ((g (k + 1)) - g k) | 0≤k≤M - 1})
= r0

23. |Σ{f[g (i + 1)] - f[g i] - f'[g i] * ((g (i + 1)) - g i) | 0≤i≤M - 1}| ≤ ((r1/r(2 * k))

* Σ{|(g (i + 1)) - g i| | 0≤i≤M - 1})

24. |Σ{f[g (i + 1)] - f[g i] - f'[g i] * ((g (i + 1)) - g i) | 0≤i≤M - 1}| ≤ ((r1/r(2 * k)) * (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. (\mSigma{}\{f'[g k] * ((g (k + 1)) - g k) | 0\mleq{}k\mleq{}M - 1\} + \mSigma{}\{f[g (k + 1)] - f[g k] - f'[g k] * ((g (k + 1)) - g k) | 0\mleq{}k\mleq{}M - 1\}) = r0 23. |\mSigma{}\{f[g (i + 1)] - f[g i] - f'[g i] * ((g (i + 1)) - g i) | 0\mleq{}i\mleq{}M - 1\}| \mleq{} ((r1/r(2 * k)) * \mSigma{}\{|(g (i + 1)) - g i| | 0\mleq{}i\mleq{}M - 1\}) \mvdash{} False By Latex: (Assert |\mSigma{}\{f[g (i + 1)] - f[g i] - f'[g i] * ((g (i + 1)) - g i) | 0\mleq{}i\mleq{}M - 1\}| \mleq{} ((r1/r(2 * k)) * (b - a)) BY ((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))\mcdot{} THEN (Assert \mSigma{}\{|(g (i + 1)) - g i| | 0\mleq{}i\mleq{}M - 1\} = \mSigma{}\{(g (k + 1)) - g k | 0\mleq{}k\mleq{}M - 1\} BY (BLemma `rsum\_functionality` THEN Auto THEN (D 0 THEN Auto) THEN RWO "rabs-of-nonneg" 0 THEN Auto THEN nRAdd \mkleeneopen{}g k1\mkleeneclose{} 0\mcdot{} THEN Auto)) THEN (RWO "-3" 0 THENA Auto) THEN RWW "-1 -2" 0 THEN Auto)) Home Index