---

Step * 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) ≤ m
7. (n + k) = 0 ∈ ℤ
⊢ 1 = (C(k;m) * C(n;m - k)) ∈ ℤ
BY
{ ((Subst ⌜n ~ 0⌝ 0⋅ THEN Auto')
   THEN (Subst ⌜k ~ 0⌝ 0⋅ THEN Auto')
   THEN Reduce 0
   THEN RWO "combinations-step" 0
   THEN Reduce 0
   THEN Auto)⋅ }

---

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


By

---

Latex:
((Subst  \mkleeneopen{}n  \msim{}  0\mkleeneclose{}  0\mcdot{}  THEN  Auto')
  THEN  (Subst  \mkleeneopen{}k  \msim{}  0\mkleeneclose{}  0\mcdot{}  THEN  Auto')
  THEN  Reduce  0
  THEN  RWO  "combinations-step"  0
  THEN  Reduce  0
  THEN  Auto)\mcdot{}

---

Home Index