---

Step * 2 1 of Lemma real-binomial


1. n : ℤ
2. 0 < n
3. ∀[a,b:ℝ].  (a + b^n - 1 = Σ{r(choose(n - 1;i)) * a^n - 1 - i * b^i | 0≤i≤n - 1})
4. a : ℝ
5. b : ℝ
⊢ (Σ{(r(choose(n - 1;i)) * a^n - 1 - i * b^i) * a | 0≤i≤n - 1}
+ Σ{(r(choose(n - 1;i)) * a^n - 1 - i * b^i) * b | 0≤i≤n - 1})
= Σ{r(choose(n;i)) * a^n - i * b^i | 0≤i≤n}
BY
{ Assert ⌜Σ{(r(choose(n - 1;i)) * a^n - 1 - i * b^i) * a | 0≤i≤n - 1}
          = Σ{r(choose(n - 1;i)) * a^n - i * b^i | 0≤i≤n - 1}⌝⋅ }

1
.....assertion..... 
1. n : ℤ
2. 0 < n
3. ∀[a,b:ℝ].  (a + b^n - 1 = Σ{r(choose(n - 1;i)) * a^n - 1 - i * b^i | 0≤i≤n - 1})
4. a : ℝ
5. b : ℝ
⊢ Σ{(r(choose(n - 1;i)) * a^n - 1 - i * b^i) * a | 0≤i≤n - 1} = Σ{r(choose(n - 1;i)) * a^n - i * b^i | 0≤i≤n - 1}

2
1. n : ℤ
2. 0 < n
3. ∀[a,b:ℝ].  (a + b^n - 1 = Σ{r(choose(n - 1;i)) * a^n - 1 - i * b^i | 0≤i≤n - 1})
4. a : ℝ
5. b : ℝ
6. Σ{(r(choose(n - 1;i)) * a^n - 1 - i * b^i) * a | 0≤i≤n - 1} = Σ{r(choose(n - 1;i)) * a^n - i * b^i | 0≤i≤n - 1}
⊢ (Σ{(r(choose(n - 1;i)) * a^n - 1 - i * b^i) * a | 0≤i≤n - 1}
+ Σ{(r(choose(n - 1;i)) * a^n - 1 - i * b^i) * b | 0≤i≤n - 1})
= Σ{r(choose(n;i)) * a^n - i * b^i | 0≤i≤n}

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  \mforall{}[a,b:\mBbbR{}].    (a  +  b\^{}n  -  1  =  \mSigma{}\{r(choose(n  -  1;i))  *  a\^{}n  -  1  -  i  *  b\^{}i  |  0\mleq{}i\mleq{}n  -  1\})
4.  a  :  \mBbbR{}
5.  b  :  \mBbbR{}
\mvdash{}  (\mSigma{}\{(r(choose(n  -  1;i))  *  a\^{}n  -  1  -  i  *  b\^{}i)  *  a  |  0\mleq{}i\mleq{}n  -  1\}
+  \mSigma{}\{(r(choose(n  -  1;i))  *  a\^{}n  -  1  -  i  *  b\^{}i)  *  b  |  0\mleq{}i\mleq{}n  -  1\})
=  \mSigma{}\{r(choose(n;i))  *  a\^{}n  -  i  *  b\^{}i  |  0\mleq{}i\mleq{}n\}


By

---

Latex:
Assert  \mkleeneopen{}\mSigma{}\{(r(choose(n  -  1;i))  *  a\^{}n  -  1  -  i  *  b\^{}i)  *  a  |  0\mleq{}i\mleq{}n  -  1\}
                =  \mSigma{}\{r(choose(n  -  1;i))  *  a\^{}n  -  i  *  b\^{}i  |  0\mleq{}i\mleq{}n  -  1\}\mkleeneclose{}\mcdot{}

---

Home Index