---

Step * 1 1 2 of Lemma choose-inequality1


1. n : ℕ
2. i : ℕn
3. n * choose(n - 1;i) < choose(n;i)
4. ((i)! * (n - i)!) * n * choose(n - 1;i) < (n)!
⊢ False
BY
{ Subst ⌜((i)! * (n - i)!) * n * choose(n - 1;i) ~ (n - i) * n * choose(n - 1;i) * (i)! * (n - 1 - i)!⌝ (-1)⋅ }

1
.....equality..... 
1. n : ℕ
2. i : ℕn
3. n * choose(n - 1;i) < choose(n;i)
4. ((i)! * (n - i)!) * n * choose(n - 1;i) < (n)!
⊢ ((i)! * (n - i)!) * n * choose(n - 1;i) ~ (n - i) * n * choose(n - 1;i) * (i)! * (n - 1 - i)!

2
1. n : ℕ
2. i : ℕn
3. n * choose(n - 1;i) < choose(n;i)
4. (n - i) * n * choose(n - 1;i) * (i)! * (n - 1 - i)! < (n)!
⊢ False

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  i  :  \mBbbN{}n
3.  n  *  choose(n  -  1;i)  <  choose(n;i)
4.  ((i)!  *  (n  -  i)!)  *  n  *  choose(n  -  1;i)  <  (n)!
\mvdash{}  False


By

---

Latex:
Subst  \mkleeneopen{}((i)!  *  (n  -  i)!)  *  n  *  choose(n  -  1;i)  \msim{}  (n  -  i)
              *  n
              *  choose(n  -  1;i)
              *  (i)!
              *  (n  -  1  -  i)!\mkleeneclose{}  (-1)\mcdot{}

---

Home Index