Step
*
2
1
1
1
1
2
2
1
1
1
1
1
1
1
1
1
1
1
2
1
1
1
2
of Lemma
Riemann-integral-additive
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. f : {f:[a, b] ⟶ℝ| ifun(f;[a, b])}
5. c : ℝ
6. a ≤ c
7. c ≤ b
8. λx.f[x] ∈ {f:[a, b] ⟶ℝ| ifun(f;[a, b])}
9. ∫ f[x] dx on [a, c] ∈ ℝ
10. ∫ f[x] dx on [c, b] ∈ ℝ
11. m : ℕ+
12. ifun(f;[a, b])
13. ifun(f;[a, c])
14. ifun(f;[c, b])
15. N1 : ℕ
16. ∀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))))
17. N : ℕ
18. ∀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))))
19. d : {d:ℝ| r0 < d}
20. ∀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)))))
21. ∀k:ℕ. (uniform-partition([a, c];k + 1) @ [c / uniform-partition([c, b];k + 1)] ∈ partition([a, b]))
22. M : ℕ
23. ∀k:ℕ
((M ≤ k) ⇒ (partition-mesh([a, b];uniform-partition([a, c];k + 1) @ [c / uniform-partition([c, b];k + 1)]) ≤ d))
24. k : ℕ
25. N1 ≤ k
26. N ≤ k
27. M ≤ k
28. |S(λx.f[x];full-partition([a, c];uniform-partition([a, c];k + 1))) - ∫ f[x] dx on [a, c]| ≤ (r1/r(3 * m))
29. |S(λx.f[x];full-partition([c, b];uniform-partition([c, b];k + 1))) - ∫ f[x] dx on [c, b]| ≤ (r1/r(3 * m))
30. ∀y:partition-choice(full-partition([a, b];uniform-partition([a, c];k + 1) @ [c / uniform-partition([c, b];k + 1)]))
(|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 : ℝ List
32. partitions([a, c];v)
33. uniform-partition([a, c];k + 1) = v ∈ partition([a, c])
34. v1 : ℝ List
35. partitions([c, b];v1)
36. uniform-partition([c, b];k + 1) = v1 ∈ partition([c, b])
37. x : i:ℕ(||v @ [c]|| + 1) - 1 ⟶ {x:ℝ| ([a / (v @ [c])][i] ≤ x) ∧ (x ≤ [a / (v @ [c])][i + 1])}
38. y : i:ℕ(||v1 @ [b]|| + 1) - 1 ⟶ {x:ℝ| ([c / (v1 @ [b])][i] ≤ x) ∧ (x ≤ [c / (v1 @ [b])][i + 1])}
39. i : ℕ(||(v @ [c]) @ v1 @ [b]|| + 1) - 1
40. ¬(i ≤ k)
41. ||v|| = k ∈ ℤ
42. ||v1|| = k ∈ ℤ
43. i = (k + 1) ∈ ℤ
44. (y 0) = (y 0) ∈ {x:ℝ| ([c / (v1 @ [b])][0] ≤ x) ∧ (x ≤ [c / (v1 @ [b])][0 + 1])}
⊢ {x:ℝ| ([c / (v1 @ [b])][0] ≤ x) ∧ (x ≤ [c / (v1 @ [b])][0 + 1])} ⊆r {x:ℝ| (c ≤ x) ∧ (x ≤ v1 @ [b][0])}
BY
{ (Reduce 0 THEN (GenConclTerm ⌜v1 @ [b][0]⌝⋅ THENA Auto)) }
1
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. f : {f:[a, b] ⟶ℝ| ifun(f;[a, b])}
5. c : ℝ
6. a ≤ c
7. c ≤ b
8. λx.f[x] ∈ {f:[a, b] ⟶ℝ| ifun(f;[a, b])}
9. ∫ f[x] dx on [a, c] ∈ ℝ
10. ∫ f[x] dx on [c, b] ∈ ℝ
11. m : ℕ+
12. ifun(f;[a, b])
13. ifun(f;[a, c])
14. ifun(f;[c, b])
15. N1 : ℕ
16. ∀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))))
17. N : ℕ
18. ∀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))))
19. d : {d:ℝ| r0 < d}
20. ∀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)))))
21. ∀k:ℕ. (uniform-partition([a, c];k + 1) @ [c / uniform-partition([c, b];k + 1)] ∈ partition([a, b]))
22. M : ℕ
23. ∀k:ℕ
((M ≤ k) ⇒ (partition-mesh([a, b];uniform-partition([a, c];k + 1) @ [c / uniform-partition([c, b];k + 1)]) ≤ d))
24. k : ℕ
25. N1 ≤ k
26. N ≤ k
27. M ≤ k
28. |S(λx.f[x];full-partition([a, c];uniform-partition([a, c];k + 1))) - ∫ f[x] dx on [a, c]| ≤ (r1/r(3 * m))
29. |S(λx.f[x];full-partition([c, b];uniform-partition([c, b];k + 1))) - ∫ f[x] dx on [c, b]| ≤ (r1/r(3 * m))
30. ∀y:partition-choice(full-partition([a, b];uniform-partition([a, c];k + 1) @ [c / uniform-partition([c, b];k + 1)]))
(|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 : ℝ List
32. partitions([a, c];v)
33. uniform-partition([a, c];k + 1) = v ∈ partition([a, c])
34. v1 : ℝ List
35. partitions([c, b];v1)
36. uniform-partition([c, b];k + 1) = v1 ∈ partition([c, b])
37. x : i:ℕ(||v @ [c]|| + 1) - 1 ⟶ {x:ℝ| ([a / (v @ [c])][i] ≤ x) ∧ (x ≤ [a / (v @ [c])][i + 1])}
38. y : i:ℕ(||v1 @ [b]|| + 1) - 1 ⟶ {x:ℝ| ([c / (v1 @ [b])][i] ≤ x) ∧ (x ≤ [c / (v1 @ [b])][i + 1])}
39. i : ℕ(||(v @ [c]) @ v1 @ [b]|| + 1) - 1
40. ¬(i ≤ k)
41. ||v|| = k ∈ ℤ
42. ||v1|| = k ∈ ℤ
43. i = (k + 1) ∈ ℤ
44. (y 0) = (y 0) ∈ {x:ℝ| ([c / (v1 @ [b])][0] ≤ x) ∧ (x ≤ [c / (v1 @ [b])][0 + 1])}
45. v2 : ℝ
46. v1 @ [b][0] = v2 ∈ ℝ
⊢ {x:ℝ| (c ≤ x) ∧ (x ≤ v2)} ⊆r {x:ℝ| (c ≤ x) ∧ (x ≤ v2)}
Latex:
Latex:
1. a : \mBbbR{}
2. b : \mBbbR{}
3. a \mleq{} b
4. f : \{f:[a, b] {}\mrightarrow{}\mBbbR{}| ifun(f;[a, b])\}
5. c : \mBbbR{}
6. a \mleq{} c
7. c \mleq{} b
8. \mlambda{}x.f[x] \mmember{} \{f:[a, b] {}\mrightarrow{}\mBbbR{}| ifun(f;[a, b])\}
9. \mint{} f[x] dx on [a, c] \mmember{} \mBbbR{}
10. \mint{} f[x] dx on [c, b] \mmember{} \mBbbR{}
11. m : \mBbbN{}\msupplus{}
12. ifun(f;[a, b])
13. ifun(f;[a, c])
14. ifun(f;[c, b])
15. N1 : \mBbbN{}
16. \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))))
17. N : \mBbbN{}
18. \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))))
19. d : \{d:\mBbbR{}| r0 < d\}
20. \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)))))
21. \mforall{}k:\mBbbN{}
(uniform-partition([a, c];k + 1) @ [c / uniform-partition([c, b];k + 1)] \mmember{} partition([a, b]))
22. M : \mBbbN{}
23. \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))
24. k : \mBbbN{}
25. N1 \mleq{} k
26. N \mleq{} k
27. M \mleq{} k
28. |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))
29. |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))
30. \mforall{}y:partition-choice(full-partition([a, b];uniform-partition([a, c];k + 1)
@ [c / uniform-partition([c, b];k + 1)]))
(|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 : \mBbbR{} List
32. partitions([a, c];v)
33. uniform-partition([a, c];k + 1) = v
34. v1 : \mBbbR{} List
35. partitions([c, b];v1)
36. uniform-partition([c, b];k + 1) = v1
37. x : i:\mBbbN{}(||v @ [c]|| + 1) - 1 {}\mrightarrow{} \{x:\mBbbR{}| ([a / (v @ [c])][i] \mleq{} x) \mwedge{} (x \mleq{} [a / (v @ [c])][i + 1])\}
38. y : i:\mBbbN{}(||v1 @ [b]|| + 1) - 1 {}\mrightarrow{} \{x:\mBbbR{}|
([c / (v1 @ [b])][i] \mleq{} x) \mwedge{} (x \mleq{} [c / (v1 @ [b])][i + 1])\}
39. i : \mBbbN{}(||(v @ [c]) @ v1 @ [b]|| + 1) - 1
40. \mneg{}(i \mleq{} k)
41. ||v|| = k
42. ||v1|| = k
43. i = (k + 1)
44. (y 0) = (y 0)
\mvdash{} \{x:\mBbbR{}| ([c / (v1 @ [b])][0] \mleq{} x) \mwedge{} (x \mleq{} [c / (v1 @ [b])][0 + 1])\} \msubseteq{}r \{x:\mBbbR{}|
(c \mleq{} x)
\mwedge{} (x \mleq{} v1 @ [b][0])\}
By
Latex:
(Reduce 0 THEN (GenConclTerm \mkleeneopen{}v1 @ [b][0]\mkleeneclose{}\mcdot{} THENA Auto))
Home
Index