---

Step * of Lemma real-binomial

No Annotations
∀[n:ℕ]. ∀[a,b:ℝ].  (a + b^n = Σ{r(choose(n;i)) * a^n - i * b^i | 0≤i≤n})
BY
{ (InductionOnNat THEN Reduce 0 THEN Auto) }

1
1. n : ℤ
2. a : ℝ
3. b : ℝ
⊢ r1 = Σ{r(choose(0;i)) * a^0 - i * b^i | 0≤i≤0}

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 : ℝ
⊢ a + b^n = Σ{r(choose(n;i)) * a^n - i * b^i | 0≤i≤n}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n:\mBbbN{}].  \mforall{}[a,b:\mBbbR{}].    (a  +  b\^{}n  =  \mSigma{}\{r(choose(n;i))  *  a\^{}n  -  i  *  b\^{}i  |  0\mleq{}i\mleq{}n\})


By

---

Latex:
(InductionOnNat  THEN  Reduce  0  THEN  Auto)

---

Home Index