---

Step * 2 1 2 2 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. Σ{(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}
7. Σ{(r(choose(n - 1;i)) * a^n - 1 - i * b^i) * b | 0≤i≤n - 1} = Σ{r(choose(n - 1;i - 1)) * a^n - i * b^i | 1≤i≤n}
⊢ (Σ{r(choose(n - 1;i)) * a^n - i * b^i | 0≤i≤n - 1} + Σ{r(choose(n - 1;i - 1)) * a^n - i * b^i | 1≤i≤n})
= (Σ{r(if (i =z 0) ∨b(i =z n) then 1 else choose(n - 1;i - 1) + choose(n - 1;i) fi ) * a^n - i * b^i | 0≤i≤n - 1}
  + (r(if (n =z 0) ∨b(n =z n) then 1 else choose(n - 1;n - 1) + choose(n - 1;n) fi ) * a^n - n * b^n))
BY
{ TACTIC:((Subst' (n =z 0) ∨b(n =z n) ~ tt 0 THENA Auto)
          THEN Reduce 0
          THEN (Subst' n - n ~ 0 0 THENA Auto)
          THEN Reduce 0
          THEN (RW (AddrC [2;1] (LemmaC `rsum-split-first`)) 0 THENA Auto)
          THEN Reduce 0) }

1
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}
7. Σ{(r(choose(n - 1;i)) * a^n - 1 - i * b^i) * b | 0≤i≤n - 1} = Σ{r(choose(n - 1;i - 1)) * a^n - i * b^i | 1≤i≤n}
⊢ (Σ{r(choose(n - 1;i)) * a^n - i * b^i | 0≤i≤n - 1} + Σ{r(choose(n - 1;i - 1)) * a^n - i * b^i | 1≤i≤n})
= (((r1 * a^n - 0 * r1)
  + Σ{r(if (i =z 0) ∨b(i =z n) then 1 else choose(n - 1;i - 1) + choose(n - 1;i) fi ) * a^n - i * b^i | 1≤i≤n - 1})
  + (r1 * r1 * b^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{}
6.  \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\}
7.  \mSigma{}\{(r(choose(n  -  1;i))  *  a\^{}n  -  1  -  i  *  b\^{}i)  *  b  |  0\mleq{}i\mleq{}n  -  1\}
=  \mSigma{}\{r(choose(n  -  1;i  -  1))  *  a\^{}n  -  i  *  b\^{}i  |  1\mleq{}i\mleq{}n\}
\mvdash{}  (\mSigma{}\{r(choose(n  -  1;i))  *  a\^{}n  -  i  *  b\^{}i  |  0\mleq{}i\mleq{}n  -  1\}
+  \mSigma{}\{r(choose(n  -  1;i  -  1))  *  a\^{}n  -  i  *  b\^{}i  |  1\mleq{}i\mleq{}n\})
=  (\mSigma{}\{r(if  (i  =\msubz{}  0)  \mvee{}\msubb{}(i  =\msubz{}  n)  then  1  else  choose(n  -  1;i  -  1)  +  choose(n  -  1;i)  fi  )
    *  a\^{}n  -  i
    *  b\^{}i  |  0\mleq{}i\mleq{}n  -  1\}
    +  (r(if  (n  =\msubz{}  0)  \mvee{}\msubb{}(n  =\msubz{}  n)  then  1  else  choose(n  -  1;n  -  1)  +  choose(n  -  1;n)  fi  )
        *  a\^{}n  -  n
        *  b\^{}n))


By

---

Latex:
TACTIC:((Subst'  (n  =\msubz{}  0)  \mvee{}\msubb{}(n  =\msubz{}  n)  \msim{}  tt  0  THENA  Auto)
                THEN  Reduce  0
                THEN  (Subst'  n  -  n  \msim{}  0  0  THENA  Auto)
                THEN  Reduce  0
                THEN  (RW  (AddrC  [2;1]  (LemmaC  `rsum-split-first`))  0  THENA  Auto)
                THEN  Reduce  0)

---

Home Index