Step
*
2
1
2
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. Σ{(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))
BY
{ TACTIC:Assert
⌜Σ{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}
= (Σ{r(choose(n - 1;i - 1)) * a^n - i * b^i | 1≤i≤n - 1} + Σ{r(choose(n - 1;i)) * a^n - i * b^i | 1≤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 : ℝ
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(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}
= (Σ{r(choose(n - 1;i - 1)) * a^n - i * b^i | 1≤i≤n - 1} + Σ{r(choose(n - 1;i)) * a^n - i * b^i | 1≤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}
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. Σ{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}
= (Σ{r(choose(n - 1;i - 1)) * a^n - i * b^i | 1≤i≤n - 1} + Σ{r(choose(n - 1;i)) * a^n - i * b^i | 1≤i≤n - 1})
⊢ (Σ{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\})
= (((r1 * a\^{}n - 0 * r1)
+ \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 | 1\mleq{}i\mleq{}n - 1\})
+ (r1 * r1 * b\^{}n))
By
Latex:
TACTIC:Assert \mkleeneopen{}\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 | 1\mleq{}i\mleq{}n - 1\}
= (\mSigma{}\{r(choose(n - 1;i - 1)) * a\^{}n - i * b\^{}i | 1\mleq{}i\mleq{}n - 1\}
+ \mSigma{}\{r(choose(n - 1;i)) * a\^{}n - i * b\^{}i | 1\mleq{}i\mleq{}n - 1\})\mkleeneclose{}\mcdot{}
Home
Index