Step
*
2
of Lemma
Riemann-sum-rsub
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. f : [a, b] ⟶ℝ
5. g : [a, b] ⟶ℝ
6. k : ℕ+
7. icompact([a, b])
8. full-partition([a, b];uniform-partition([a, b];k)) ∈ {x:ℝ| (a ≤ x) ∧ (x ≤ b)} List
9. v : {x:ℝ| (a ≤ x) ∧ (x ≤ b)} List@i
10. full-partition([a, b];uniform-partition([a, b];k)) = v ∈ ({x:ℝ| (a ≤ x) ∧ (x ≤ b)} List)@i
⊢ (Σ{(f v[i]) * (v[i + 1] - v[i]) | 0≤i≤||v|| - 2} - Σ{(g v[i]) * (v[i + 1] - v[i]) | 0≤i≤||v|| - 2})
= Σ{((f v[i]) - g v[i]) * (v[i + 1] - v[i]) | 0≤i≤||v|| - 2}
BY
{ ((RWO "rsum_linearity-rsub<" 0 THENA Auto) THEN (BLemma `rsum_functionality` THENM D 0) THEN Auto) }
1
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. f : [a, b] ⟶ℝ
5. g : [a, b] ⟶ℝ
6. k : ℕ+
7. icompact([a, b])
8. full-partition([a, b];uniform-partition([a, b];k)) ∈ {x:ℝ| (a ≤ x) ∧ (x ≤ b)} List
9. v : {x:ℝ| (a ≤ x) ∧ (x ≤ b)} List@i
10. full-partition([a, b];uniform-partition([a, b];k)) = v ∈ ({x:ℝ| (a ≤ x) ∧ (x ≤ b)} List)@i
11. i : ℤ@i
12. 0 ≤ i@i
13. i ≤ (||v|| - 2)@i
⊢ (((f v[i]) * (v[i + 1] - v[i])) - (g v[i]) * (v[i + 1] - v[i])) = (((f v[i]) - g v[i]) * (v[i + 1] - v[i]))
Latex:
Latex:
1. a : \mBbbR{}
2. b : \mBbbR{}
3. a \mleq{} b
4. f : [a, b] {}\mrightarrow{}\mBbbR{}
5. g : [a, b] {}\mrightarrow{}\mBbbR{}
6. k : \mBbbN{}\msupplus{}
7. icompact([a, b])
8. full-partition([a, b];uniform-partition([a, b];k)) \mmember{} \{x:\mBbbR{}| (a \mleq{} x) \mwedge{} (x \mleq{} b)\} List
9. v : \{x:\mBbbR{}| (a \mleq{} x) \mwedge{} (x \mleq{} b)\} List@i
10. full-partition([a, b];uniform-partition([a, b];k)) = v@i
\mvdash{} (\mSigma{}\{(f v[i]) * (v[i + 1] - v[i]) | 0\mleq{}i\mleq{}||v|| - 2\} - \mSigma{}\{(g v[i]) * (v[i + 1] - v[i]) | 0\mleq{}i\mleq{}||v||
- 2\})
= \mSigma{}\{((f v[i]) - g v[i]) * (v[i + 1] - v[i]) | 0\mleq{}i\mleq{}||v|| - 2\}
By
Latex:
((RWO "rsum\_linearity-rsub<" 0 THENA Auto) THEN (BLemma `rsum\_functionality` THENM D 0) THEN Auto)
Home
Index