---

Step * 2 1 2 2 1 1 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. Σ{(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}
8. i : ℤ@i
9. i ≠ 0
10. 1 ≤ i
11. i ≤ (n - 1)
⊢ (r(choose(n - 1;i - 1) + choose(n - 1;i)) * a^n - i * b^i)
= ((r(choose(n - 1;i - 1)) * a^n - i * b^i) + (r(choose(n - 1;i)) * a^n - i * b^i))
BY
{ TACTIC:((RWO "radd-int<" 0 THENA Auto)
          THEN GenConclTerms Auto [⌜r(choose(n - 1;i - 1))⌝;⌜r(choose(n - 1;i))⌝
               ;⌜a^n - i⌝;⌜b^i⌝]⋅
          ) }

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}
8. i : ℤ@i
9. i ≠ 0
10. 1 ≤ i
11. i ≤ (n - 1)
12. v : ℝ@i
13. r(choose(n - 1;i - 1)) = v ∈ ℝ
14. v1 : ℝ@i
15. r(choose(n - 1;i)) = v1 ∈ ℝ
16. v2 : ℝ@i
17. a^n - i = v2 ∈ ℝ
18. v3 : ℝ@i
19. b^i = v3 ∈ ℝ
⊢ ((v + v1) * v2 * v3) = ((v * v2 * v3) + (v1 * v2 * v3))

---

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


By

---

Latex:
TACTIC:((RWO  "radd-int<"  0  THENA  Auto)
                THEN  GenConclTerms  Auto  [\mkleeneopen{}r(choose(n  -  1;i  -  1))\mkleeneclose{};\mkleeneopen{}r(choose(n  -  1;i))\mkleeneclose{}
                          ;\mkleeneopen{}a\^{}n  -  i\mkleeneclose{};\mkleeneopen{}b\^{}i\mkleeneclose{}]\mcdot{}
                )

---

Home Index