---

Step * 2 1 1 1 2 1 of Lemma rpolynomial-composition1


1. b : ℝ
2. m : ℕ+
3. v : ℝ
4. v1 : ℝ
5. a' : ℕm + 1 ⟶ ℝ
6. ∀x:ℝ. (Σ{(a' i) * x^i | 0≤i≤m} = (v1 * x) + b^m)
7. x : ℝ
⊢ Σ{(v * (a' i)) * x^i | 0≤i≤m} = (v * (v1 * x) + b^m)
BY
{ ((RWO "rmul_assoc" 0 THENA Auto) THEN (RWO "rsum_linearity2" 0 THENA Auto)) }

1
1. b : ℝ
2. m : ℕ+
3. v : ℝ
4. v1 : ℝ
5. a' : ℕm + 1 ⟶ ℝ
6. ∀x:ℝ. (Σ{(a' i) * x^i | 0≤i≤m} = (v1 * x) + b^m)
7. x : ℝ
⊢ (v * Σ{(a' i) * x^i | 0≤i≤m}) = (v * (v1 * x) + b^m)

---

Latex:

---

Latex:

1.  b  :  \mBbbR{}
2.  m  :  \mBbbN{}\msupplus{}
3.  v  :  \mBbbR{}
4.  v1  :  \mBbbR{}
5.  a'  :  \mBbbN{}m  +  1  {}\mrightarrow{}  \mBbbR{}
6.  \mforall{}x:\mBbbR{}.  (\mSigma{}\{(a'  i)  *  x\^{}i  |  0\mleq{}i\mleq{}m\}  =  (v1  *  x)  +  b\^{}m)
7.  x  :  \mBbbR{}
\mvdash{}  \mSigma{}\{(v  *  (a'  i))  *  x\^{}i  |  0\mleq{}i\mleq{}m\}  =  (v  *  (v1  *  x)  +  b\^{}m)


By

---

Latex:
((RWO  "rmul\_assoc"  0  THENA  Auto)  THEN  (RWO  "rsum\_linearity2"  0  THENA  Auto))

---

Home Index