Step
*
1
1
1
1
of Lemma
add-rpolynomials
1. n : ℕ
2. m : ℕ
3. a : ℕn + 1 ⟶ ℝ
4. b : ℕm + 1 ⟶ ℝ
5. x : ℝ
6. m ≤ n
7. Σ{(a i) * x^i | 0≤i≤n} = (Σ{(a i) * x^i | 0≤i≤m} + Σ{(a (m + i + 1)) * x^m + i + 1 | 0≤i≤n - m + 1})
8. Σ{if i ≤z m then (a i) + (b i) else a i fi * x^i | 0≤i≤n}
= (Σ{if i ≤z m then (a i) + (b i) else a i fi * x^i | 0≤i≤m}
+ Σ{if m + i + 1 ≤z m then (a (m + i + 1)) + (b (m + i + 1)) else a (m + i + 1) fi * x^m + i + 1 | 0≤i≤n - m + 1})
9. Σ{if i ≤z m then (a i) + (b i) else a i fi * x^i | 0≤i≤m} = (Σ{(a i) * x^i | 0≤i≤m} + Σ{(b i) * x^i | 0≤i≤m})
10. v : ℝ
11. Σ{(a i) * x^i | 0≤i≤m} = v ∈ ℝ
12. v1 : ℝ
13. Σ{(b i) * x^i | 0≤i≤m} = v1 ∈ ℝ
⊢ ((v + Σ{(a (m + i + 1)) * x^m + i + 1 | 0≤i≤n - m + 1}) + v1)
= ((v + v1)
+ Σ{if m + i + 1 ≤z m then (a (m + i + 1)) + (b (m + i + 1)) else a (m + i + 1) fi * x^m + i + 1 | 0≤i≤n - m + 1})
BY
{ (Assert Σ{if m + i + 1 ≤z m then (a (m + i + 1)) + (b (m + i + 1)) else a (m + i + 1) fi * x^m + i + 1 | 0≤i≤n - m
+ 1}
= Σ{(a (m + i + 1)) * x^m + i + 1 | 0≤i≤n - m + 1} BY
((BLemma `rsum_functionality` THEN Auto) THEN D 0 THEN Reduce 0 THEN Auto)) }
1
1. n : ℕ
2. m : ℕ
3. a : ℕn + 1 ⟶ ℝ
4. b : ℕm + 1 ⟶ ℝ
5. x : ℝ
6. m ≤ n
7. Σ{(a i) * x^i | 0≤i≤n} = (Σ{(a i) * x^i | 0≤i≤m} + Σ{(a (m + i + 1)) * x^m + i + 1 | 0≤i≤n - m + 1})
8. Σ{if i ≤z m then (a i) + (b i) else a i fi * x^i | 0≤i≤n}
= (Σ{if i ≤z m then (a i) + (b i) else a i fi * x^i | 0≤i≤m}
+ Σ{if m + i + 1 ≤z m then (a (m + i + 1)) + (b (m + i + 1)) else a (m + i + 1) fi * x^m + i + 1 | 0≤i≤n - m + 1})
9. Σ{if i ≤z m then (a i) + (b i) else a i fi * x^i | 0≤i≤m} = (Σ{(a i) * x^i | 0≤i≤m} + Σ{(b i) * x^i | 0≤i≤m})
10. v : ℝ
11. Σ{(a i) * x^i | 0≤i≤m} = v ∈ ℝ
12. v1 : ℝ
13. Σ{(b i) * x^i | 0≤i≤m} = v1 ∈ ℝ
14. Σ{if m + i + 1 ≤z m then (a (m + i + 1)) + (b (m + i + 1)) else a (m + i + 1) fi * x^m + i + 1 | 0≤i≤n - m + 1}
= Σ{(a (m + i + 1)) * x^m + i + 1 | 0≤i≤n - m + 1}
⊢ ((v + Σ{(a (m + i + 1)) * x^m + i + 1 | 0≤i≤n - m + 1}) + v1)
= ((v + v1)
+ Σ{if m + i + 1 ≤z m then (a (m + i + 1)) + (b (m + i + 1)) else a (m + i + 1) fi * x^m + i + 1 | 0≤i≤n - m + 1})
Latex:
Latex:
1. n : \mBbbN{}
2. m : \mBbbN{}
3. a : \mBbbN{}n + 1 {}\mrightarrow{} \mBbbR{}
4. b : \mBbbN{}m + 1 {}\mrightarrow{} \mBbbR{}
5. x : \mBbbR{}
6. m \mleq{} n
7. \mSigma{}\{(a i) * x\^{}i | 0\mleq{}i\mleq{}n\}
= (\mSigma{}\{(a i) * x\^{}i | 0\mleq{}i\mleq{}m\} + \mSigma{}\{(a (m + i + 1)) * x\^{}m + i + 1 | 0\mleq{}i\mleq{}n - m + 1\})
8. \mSigma{}\{if i \mleq{}z m then (a i) + (b i) else a i fi * x\^{}i | 0\mleq{}i\mleq{}n\}
= (\mSigma{}\{if i \mleq{}z m then (a i) + (b i) else a i fi * x\^{}i | 0\mleq{}i\mleq{}m\}
+ \mSigma{}\{if m + i + 1 \mleq{}z m then (a (m + i + 1)) + (b (m + i + 1)) else a (m + i + 1) fi
* x\^{}m + i + 1 | 0\mleq{}i\mleq{}n - m + 1\})
9. \mSigma{}\{if i \mleq{}z m then (a i) + (b i) else a i fi * x\^{}i | 0\mleq{}i\mleq{}m\}
= (\mSigma{}\{(a i) * x\^{}i | 0\mleq{}i\mleq{}m\} + \mSigma{}\{(b i) * x\^{}i | 0\mleq{}i\mleq{}m\})
10. v : \mBbbR{}
11. \mSigma{}\{(a i) * x\^{}i | 0\mleq{}i\mleq{}m\} = v
12. v1 : \mBbbR{}
13. \mSigma{}\{(b i) * x\^{}i | 0\mleq{}i\mleq{}m\} = v1
\mvdash{} ((v + \mSigma{}\{(a (m + i + 1)) * x\^{}m + i + 1 | 0\mleq{}i\mleq{}n - m + 1\}) + v1)
= ((v + v1)
+ \mSigma{}\{if m + i + 1 \mleq{}z m then (a (m + i + 1)) + (b (m + i + 1)) else a (m + i + 1) fi
* x\^{}m + i + 1 | 0\mleq{}i\mleq{}n - m + 1\})
By
Latex:
(Assert \mSigma{}\{if m + i + 1 \mleq{}z m then (a (m + i + 1)) + (b (m + i + 1)) else a (m + i + 1) fi
* x\^{}m + i + 1 | 0\mleq{}i\mleq{}n - m + 1\}
= \mSigma{}\{(a (m + i + 1)) * x\^{}m + i + 1 | 0\mleq{}i\mleq{}n - m + 1\} BY
((BLemma `rsum\_functionality` THEN Auto) THEN D 0 THEN Reduce 0 THEN Auto))
Home
Index