Step
*
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})
⊢ ((Σ{(a i) * x^i | 0≤i≤m} + Σ{(a (m + i + 1)) * x^m + i + 1 | 0≤i≤n - m + 1}) + Σ{(b i) * x^i | 0≤i≤m})
= (Σ{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})
BY
{ ((Assert Σ{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}) BY
(RWO "rsum_linearity1<" 0
THEN Auto
THEN BLemma `rsum_functionality`
THEN Auto
THEN D 0
THEN Reduce 0
THEN Auto))
THEN (RWO "-1" 0 THENA Auto)
THEN GenConclTerms Auto [⌜Σ{(a i) * x^i | 0≤i≤m}⌝;⌜Σ{(b i) * x^i | 0≤i≤m}⌝]⋅) }
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 ∈ ℝ
⊢ ((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\})
\mvdash{} ((\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\})
+ \mSigma{}\{(b i) * x\^{}i | 0\mleq{}i\mleq{}m\})
= (\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\})
By
Latex:
((Assert \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\}) BY
(RWO "rsum\_linearity1<" 0
THEN Auto
THEN BLemma `rsum\_functionality`
THEN Auto
THEN D 0
THEN Reduce 0
THEN Auto))
THEN (RWO "-1" 0 THENA Auto)
THEN GenConclTerms Auto [\mkleeneopen{}\mSigma{}\{(a i) * x\^{}i | 0\mleq{}i\mleq{}m\}\mkleeneclose{};\mkleeneopen{}\mSigma{}\{(b i) * x\^{}i | 0\mleq{}i\mleq{}m\}\mkleeneclose{}]\mcdot{})
Home
Index