---

Step * 2 1 1 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 : ℝ
6. i : ℤ@i
7. 0 ≤ i
8. i ≤ (n - 1)
⊢ ((r(choose(n - 1;i)) * a^n - 1 - i * b^i) * a) = (r(choose(n - 1;i)) * a^n - i * b^i)
BY
{ TACTIC:((RW (AddrC [2;2;1] (LemmaC `rnexp_step`)) 0 THENA Auto)
          THEN Subst' n - i - 1 ~ n - 1 - i 0
          THEN Auto
          THEN nRNorm 0
          THEN Auto) }

---

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{}
6.  i  :  \mBbbZ{}@i
7.  0  \mleq{}  i
8.  i  \mleq{}  (n  -  1)
\mvdash{}  ((r(choose(n  -  1;i))  *  a\^{}n  -  1  -  i  *  b\^{}i)  *  a)  =  (r(choose(n  -  1;i))  *  a\^{}n  -  i  *  b\^{}i)


By

---

Latex:
TACTIC:((RW  (AddrC  [2;2;1]  (LemmaC  `rnexp\_step`))  0  THENA  Auto)
                THEN  Subst'  n  -  i  -  1  \msim{}  n  -  1  -  i  0
                THEN  Auto
                THEN  nRNorm  0
                THEN  Auto)

---

Home Index