---

Step * 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) ≤ m
⊢ C(n + k;m) = (C(k;m) * C(n;m - k)) ∈ ℤ
BY
{ ((RW (AddrC [2] (LemmaC `combinations-step`)) 0 THENA (Auto THEN 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) ≤ m
7. (n + k) = 0 ∈ ℤ
⊢ 1 = (C(k;m) * 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 : ℕ
6. n + k ≠ 0
7. (n + k) ≤ m
⊢ (m * C((n + k) - 1;m - 1)) = (C(k;m) * 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)  \mleq{}  m
\mvdash{}  C(n  +  k;m)  =  (C(k;m)  *  C(n;m  -  k))


By

---

Latex:
((RW  (AddrC  [2]  (LemmaC  `combinations-step`))  0  THENA  (Auto  THEN  Auto'))  THEN  AutoSplit)

---

Home Index