---

Step * 2 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 : {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)) ∈ ℤ
BY
{ (InstHyp [⌜n⌝;⌜k - 1⌝] 3⋅ THENA Auto) }

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 : {1...}
6. n + k ≠ 0
7. (n + k) ≤ m
8. C(n + (k - 1);m - 1) = (C(k - 1;m - 1) * C(n;m - 1 - k - 1)) ∈ ℤ
⊢ (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  :  \{1...\}
6.  n  +  k  \mneq{}  0
7.  (n  +  k)  \mleq{}  m
\mvdash{}  (m  *  C((n  +  k)  -  1;m  -  1))  =  ((m  *  C(k  -  1;m  -  1))  *  C(n;m  -  k))


By

---

Latex:
(InstHyp  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}k  -  1\mkleeneclose{}]  3\mcdot{}  THENA  Auto)

---

Home Index