Step
*
2
1
1
1
1
2
2
1
1
1
2
1
1
1
of Lemma
Riemann-integral-additive
1. a : ℝ
2. b : {b:ℝ| a ≤ b}
3. f : {f:[a, b] ⟶ℝ| ifun(f;[a, b])}
4. c : ℝ
5. a ≤ c
6. c ≤ b
7. λx.f[x] ∈ {f:[a, b] ⟶ℝ| ifun(f;[a, b])}
8. ∫ f[x] dx on [a, c] ∈ ℝ
9. ∫ f[x] dx on [c, b] ∈ ℝ
10. m : ℕ+
11. ifun(f;[a, b])
12. ifun(f;[a, c])
13. ifun(f;[c, b])
14. N1 : ℕ
15. ∀k:ℕ
((N1 ≤ k)
⇒ (|S(λx.f[x];full-partition([a, c];uniform-partition([a, c];k + 1))) - ∫ f[x] dx on [a, c]| ≤ (r1/r(3 * m))))
16. N : ℕ
17. ∀k:ℕ
((N ≤ k)
⇒ (|S(λx.f[x];full-partition([c, b];uniform-partition([c, b];k + 1))) - ∫ f[x] dx on [c, b]| ≤ (r1/r(3 * m))))
18. d : {d:ℝ| r0 < d}
19. ∀p:partition([a, b])
((partition-mesh([a, b];p) ≤ d)
⇒ (∀y:partition-choice(full-partition([a, b];p))
(|S(λx.f[x];full-partition([a, b];p)) - ∫ f[x] dx on [a, b]| ≤ (r1/r(3 * m)))))
20. ∀k:ℕ. (uniform-partition([a, c];k + 1) @ [c / uniform-partition([c, b];k + 1)] ∈ partition([a, b]))
21. M : ℕ
22. ∀k:ℕ
((M ≤ k) ⇒ (partition-mesh([a, b];uniform-partition([a, c];k + 1) @ [c / uniform-partition([c, b];k + 1)]) ≤ d))
23. k : ℕ
24. N1 ≤ k
25. N ≤ k
26. M ≤ k
27. |S(λx.f[x];full-partition([a, c];uniform-partition([a, c];k + 1))) - ∫ f[x] dx on [a, c]| ≤ (r1/r(3 * m))
28. |S(λx.f[x];full-partition([c, b];uniform-partition([c, b];k + 1))) - ∫ f[x] dx on [c, b]| ≤ (r1/r(3 * m))
29. λi.if i ≤z k
then default-partition-choice(full-partition([a, c];uniform-partition([a, c];k + 1))) i
else default-partition-choice(full-partition([c, b];uniform-partition([c, b];k + 1))) (i - k + 1)
fi ∈ partition-choice(full-partition([a, b];uniform-partition([a, c];k + 1)
@ [c / uniform-partition([c, b];k + 1)]))
30. |S(λx.f[x];full-partition([a, b];uniform-partition([a, c];k + 1) @ [c / uniform-partition([c, b];k + 1)]))
- ∫ f[x] dx on [a, b]| ≤ (r1/r(3 * m))
31. v : partition([a, c])
32. uniform-partition([a, c];k + 1) = v ∈ partition([a, c])
33. v1 : partition([c, b])
34. uniform-partition([c, b];k + 1) = v1 ∈ partition([c, b])
⊢ Σ{f[if i ≤z k
then default-partition-choice(full-partition([a, c];v)) i
else default-partition-choice(full-partition([c, b];v1)) (i - k + 1)
fi ]
* (full-partition([a, b];v @ [c / v1])[i + 1] - full-partition([a, b];v @ [c / v1])[i]) | 0≤i≤||full-partition([a, b];v
@ [c / v1])|| - 2}
= (Σ{f[default-partition-choice(full-partition([a, c];v)) i]
* (full-partition([a, c];v)[i + 1] - full-partition([a, c];v)[i]) | 0≤i≤||full-partition([a, c];v)|| - 2}
+ Σ{f[default-partition-choice(full-partition([c, b];v1)) i]
* (full-partition([c, b];v1)[i + 1] - full-partition([c, b];v1)[i]) | 0≤i≤||full-partition([c, b];v1)|| - 2})
BY
{ GenConclTerms (EAuto 1) [⌜full-partition([a, c];v)⌝;⌜full-partition([c, b];v1)⌝]⋅ }
1
1. a : ℝ
2. b : {b:ℝ| a ≤ b}
3. f : {f:[a, b] ⟶ℝ| ifun(f;[a, b])}
4. c : ℝ
5. a ≤ c
6. c ≤ b
7. λx.f[x] ∈ {f:[a, b] ⟶ℝ| ifun(f;[a, b])}
8. ∫ f[x] dx on [a, c] ∈ ℝ
9. ∫ f[x] dx on [c, b] ∈ ℝ
10. m : ℕ+
11. ifun(f;[a, b])
12. ifun(f;[a, c])
13. ifun(f;[c, b])
14. N1 : ℕ
15. ∀k:ℕ
((N1 ≤ k)
⇒ (|S(λx.f[x];full-partition([a, c];uniform-partition([a, c];k + 1))) - ∫ f[x] dx on [a, c]| ≤ (r1/r(3 * m))))
16. N : ℕ
17. ∀k:ℕ
((N ≤ k)
⇒ (|S(λx.f[x];full-partition([c, b];uniform-partition([c, b];k + 1))) - ∫ f[x] dx on [c, b]| ≤ (r1/r(3 * m))))
18. d : {d:ℝ| r0 < d}
19. ∀p:partition([a, b])
((partition-mesh([a, b];p) ≤ d)
⇒ (∀y:partition-choice(full-partition([a, b];p))
(|S(λx.f[x];full-partition([a, b];p)) - ∫ f[x] dx on [a, b]| ≤ (r1/r(3 * m)))))
20. ∀k:ℕ. (uniform-partition([a, c];k + 1) @ [c / uniform-partition([c, b];k + 1)] ∈ partition([a, b]))
21. M : ℕ
22. ∀k:ℕ
((M ≤ k) ⇒ (partition-mesh([a, b];uniform-partition([a, c];k + 1) @ [c / uniform-partition([c, b];k + 1)]) ≤ d))
23. k : ℕ
24. N1 ≤ k
25. N ≤ k
26. M ≤ k
27. |S(λx.f[x];full-partition([a, c];uniform-partition([a, c];k + 1))) - ∫ f[x] dx on [a, c]| ≤ (r1/r(3 * m))
28. |S(λx.f[x];full-partition([c, b];uniform-partition([c, b];k + 1))) - ∫ f[x] dx on [c, b]| ≤ (r1/r(3 * m))
29. λi.if i ≤z k
then default-partition-choice(full-partition([a, c];uniform-partition([a, c];k + 1))) i
else default-partition-choice(full-partition([c, b];uniform-partition([c, b];k + 1))) (i - k + 1)
fi ∈ partition-choice(full-partition([a, b];uniform-partition([a, c];k + 1)
@ [c / uniform-partition([c, b];k + 1)]))
30. |S(λx.f[x];full-partition([a, b];uniform-partition([a, c];k + 1) @ [c / uniform-partition([c, b];k + 1)]))
- ∫ f[x] dx on [a, b]| ≤ (r1/r(3 * m))
31. v : partition([a, c])
32. uniform-partition([a, c];k + 1) = v ∈ partition([a, c])
33. v1 : partition([c, b])
34. uniform-partition([c, b];k + 1) = v1 ∈ partition([c, b])
35. v2 : ℝ List
36. full-partition([a, c];v) = v2 ∈ (ℝ List)
37. v3 : ℝ List
38. full-partition([c, b];v1) = v3 ∈ (ℝ List)
⊢ Σ{f[if i ≤z k then default-partition-choice(v2) i else default-partition-choice(v3) (i - k + 1) fi ]
* (full-partition([a, b];v @ [c / v1])[i + 1] - full-partition([a, b];v @ [c / v1])[i]) | 0≤i≤||full-partition([a, b];v
@ [c / v1])|| - 2}
= (Σ{f[default-partition-choice(v2) i] * (v2[i + 1] - v2[i]) | 0≤i≤||v2|| - 2}
+ Σ{f[default-partition-choice(v3) i] * (v3[i + 1] - v3[i]) | 0≤i≤||v3|| - 2})
Latex:
Latex:
1. a : \mBbbR{}
2. b : \{b:\mBbbR{}| a \mleq{} b\}
3. f : \{f:[a, b] {}\mrightarrow{}\mBbbR{}| ifun(f;[a, b])\}
4. c : \mBbbR{}
5. a \mleq{} c
6. c \mleq{} b
7. \mlambda{}x.f[x] \mmember{} \{f:[a, b] {}\mrightarrow{}\mBbbR{}| ifun(f;[a, b])\}
8. \mint{} f[x] dx on [a, c] \mmember{} \mBbbR{}
9. \mint{} f[x] dx on [c, b] \mmember{} \mBbbR{}
10. m : \mBbbN{}\msupplus{}
11. ifun(f;[a, b])
12. ifun(f;[a, c])
13. ifun(f;[c, b])
14. N1 : \mBbbN{}
15. \mforall{}k:\mBbbN{}
((N1 \mleq{} k)
{}\mRightarrow{} (|S(\mlambda{}x.f[x];full-partition([a, c];uniform-partition([a, c];k + 1)))
- \mint{} f[x] dx on [a, c]| \mleq{} (r1/r(3 * m))))
16. N : \mBbbN{}
17. \mforall{}k:\mBbbN{}
((N \mleq{} k)
{}\mRightarrow{} (|S(\mlambda{}x.f[x];full-partition([c, b];uniform-partition([c, b];k + 1)))
- \mint{} f[x] dx on [c, b]| \mleq{} (r1/r(3 * m))))
18. d : \{d:\mBbbR{}| r0 < d\}
19. \mforall{}p:partition([a, b])
((partition-mesh([a, b];p) \mleq{} d)
{}\mRightarrow{} (\mforall{}y:partition-choice(full-partition([a, b];p))
(|S(\mlambda{}x.f[x];full-partition([a, b];p)) - \mint{} f[x] dx on [a, b]| \mleq{} (r1/r(3 * m)))))
20. \mforall{}k:\mBbbN{}
(uniform-partition([a, c];k + 1) @ [c / uniform-partition([c, b];k + 1)] \mmember{} partition([a, b]))
21. M : \mBbbN{}
22. \mforall{}k:\mBbbN{}
((M \mleq{} k)
{}\mRightarrow{} (partition-mesh([a, b];uniform-partition([a, c];k + 1)
@ [c / uniform-partition([c, b];k + 1)]) \mleq{} d))
23. k : \mBbbN{}
24. N1 \mleq{} k
25. N \mleq{} k
26. M \mleq{} k
27. |S(\mlambda{}x.f[x];full-partition([a, c];uniform-partition([a, c];k + 1)))
- \mint{} f[x] dx on [a, c]| \mleq{} (r1/r(3 * m))
28. |S(\mlambda{}x.f[x];full-partition([c, b];uniform-partition([c, b];k + 1)))
- \mint{} f[x] dx on [c, b]| \mleq{} (r1/r(3 * m))
29. \mlambda{}i.if i \mleq{}z k
then default-partition-choice(full-partition([a, c];uniform-partition([a, c];k + 1))) i
else default-partition-choice(full-partition([c, b];uniform-partition([c, b];k + 1)))
(i - k + 1)
fi \mmember{} partition-choice(full-partition([a, b];uniform-partition([a, c];k + 1)
@ [c / uniform-partition([c, b];k + 1)]))
30. |S(\mlambda{}x.f[x];full-partition([a, b];uniform-partition([a, c];k + 1)
@ [c / uniform-partition([c, b];k + 1)])) - \mint{} f[x] dx on [a, b]| \mleq{} (r1/r(3 * m))
31. v : partition([a, c])
32. uniform-partition([a, c];k + 1) = v
33. v1 : partition([c, b])
34. uniform-partition([c, b];k + 1) = v1
\mvdash{} \mSigma{}\{f[if i \mleq{}z k
then default-partition-choice(full-partition([a, c];v)) i
else default-partition-choice(full-partition([c, b];v1)) (i - k + 1)
fi ]
* (full-partition([a, b];v @ [c / v1])[i + 1] - full-partition([a, b];v
@ [c / v1])[i]) | 0\mleq{}i\mleq{}||full-partition([a, b];v @ [c / v1])|| - 2\}
= (\mSigma{}\{f[default-partition-choice(full-partition([a, c];v)) i]
* (full-partition([a, c];v)[i + 1]
- full-partition([a, c];v)[i]) | 0\mleq{}i\mleq{}||full-partition([a, c];v)|| - 2\}
+ \mSigma{}\{f[default-partition-choice(full-partition([c, b];v1)) i]
* (full-partition([c, b];v1)[i + 1]
- full-partition([c, b];v1)[i]) | 0\mleq{}i\mleq{}||full-partition([c, b];v1)|| - 2\})
By
Latex:
GenConclTerms (EAuto 1) [\mkleeneopen{}full-partition([a, c];v)\mkleeneclose{};\mkleeneopen{}full-partition([c, b];v1)\mkleeneclose{}]\mcdot{}
Home
Index