---

Step * 1 1 of Lemma equipollent-factorial


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)! ∈ ℤ
BY
{ xxx(Subst' n - n ~ 0 -1 THEN Reduce (-1) THEN Auto)xxx }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  C(n;n)  =  if  n  \mleq{}z  n  then  (n)!  \mdiv{}  (n  -  n)!  else  0  fi 
3.  (C(n;n)  *  (n  -  n)!)  =  (n)!
\mvdash{}  C(n;n)  =  (n)!


By

---

Latex:
xxx(Subst'  n  -  n  \msim{}  0  -1  THEN  Reduce  (-1)  THEN  Auto)xxx

---

Home Index