---

Step * 1 of Lemma equipollent-factorial


1. n : ℕ
⊢ C(n;n) = (n)! ∈ ℤ
BY
{ xxx((InstLemma `combinations-formula` [⌜n⌝;⌜n⌝]⋅ THEN Auto) THEN D -2 THEN Auto)xxx }

1
1. n : ℕ
2. C(n;n) = if n ≤z n then (n)! ÷ (n - n)! else 0 fi  ∈ ℤ
3. (C(n;n) * (n - n)!) = (n)! ∈ ℤ
⊢ C(n;n) = (n)! ∈ ℤ

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
\mvdash{}  C(n;n)  =  (n)!


By

---

Latex:
xxx((InstLemma  `combinations-formula`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  D  -2  THEN  Auto)xxx

---

Home Index