---

Step * 2 2 1 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
8. k = 0 ∈ ℤ
⊢ (m * C((n + k) - 1;m - 1)) = (1 * C(n;m - k)) ∈ ℤ
BY
{ (HypSubst' (-1) 0
   THEN (RW  IntNormC 0 THENA Auto)
   THEN (RW (AddrC [3] (LemmaC `combinations-step`)) 0 THENA Auto)
   THEN AutoSplit) }

---

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
8.  k  =  0
\mvdash{}  (m  *  C((n  +  k)  -  1;m  -  1))  =  (1  *  C(n;m  -  k))


By

---

Latex:
(HypSubst'  (-1)  0
  THEN  (RW    IntNormC  0  THENA  Auto)
  THEN  (RW  (AddrC  [3]  (LemmaC  `combinations-step`))  0  THENA  Auto)
  THEN  AutoSplit)

---

Home Index