---

Step * 2 2 of Lemma combinations-split


1. m : ℤ
2. 0 < m
3. ∀[n,k:ℕ].  C(n + k;m - 1) = (C(k;m - 1) * C(n;m - 1 - k)) ∈ ℤ supposing (n + k) ≤ (m - 1)
4. n : ℕ
5. k : ℕ
6. n + k ≠ 0
7. (n + k) ≤ m
⊢ (m * C((n + k) - 1;m - 1)) = (C(k;m) * C(n;m - k)) ∈ ℤ
BY
{ ((RW (AddrC [3;1] (LemmaC `combinations-step`)) 0 THENA Auto) THEN AutoSplit)⋅ }

1
1. m : ℤ
2. 0 < m
3. ∀[n,k:ℕ].  C(n + k;m - 1) = (C(k;m - 1) * C(n;m - 1 - k)) ∈ ℤ supposing (n + k) ≤ (m - 1)
4. n : ℕ
5. k : ℕ
6. n + k ≠ 0
7. (n + k) ≤ m
8. k = 0 ∈ ℤ
⊢ (m * C((n + k) - 1;m - 1)) = (1 * C(n;m - k)) ∈ ℤ

2
1. m : ℤ
2. 0 < m
3. ∀[n,k:ℕ].  C(n + k;m - 1) = (C(k;m - 1) * C(n;m - 1 - k)) ∈ ℤ supposing (n + k) ≤ (m - 1)
4. n : ℕ
5. k : {1...}
6. n + k ≠ 0
7. (n + k) ≤ m
⊢ (m * C((n + k) - 1;m - 1)) = ((m * C(k - 1;m - 1)) * C(n;m - k)) ∈ ℤ

---

Latex:

---

Latex:

1.  m  :  \mBbbZ{}
2.  0  <  m
3.  \mforall{}[n,k:\mBbbN{}].    C(n  +  k;m  -  1)  =  (C(k;m  -  1)  *  C(n;m  -  1  -  k))  supposing  (n  +  k)  \mleq{}  (m  -  1)
4.  n  :  \mBbbN{}
5.  k  :  \mBbbN{}
6.  n  +  k  \mneq{}  0
7.  (n  +  k)  \mleq{}  m
\mvdash{}  (m  *  C((n  +  k)  -  1;m  -  1))  =  (C(k;m)  *  C(n;m  -  k))


By

---

Latex:
((RW  (AddrC  [3;1]  (LemmaC  `combinations-step`))  0  THENA  Auto)  THEN  AutoSplit)\mcdot{}

---

Home Index