---

Step * 1 1 1 1 of Lemma exp-difference-inequality

.....equality..... 
1. n : ℕ+
2. a : ℕ
3. b : ℕ
⊢ (choose(n;(n + 1) - 1) * a^((n + 1) - 1) * b^(n - (n + 1) - 1)) = a^n ∈ ℤ
BY
{ ((Subst ⌜(n + 1) - 1 ~ n⌝ 0⋅ THEN Auto)
   THEN Subst ⌜n - n ~ 0⌝ 0⋅
   THEN Auto
   THEN Reduce 0
   THEN Subst ⌜choose(n;n) ~ 1⌝ 0⋅
   THEN Auto) }

1
1. n : ℕ+
2. a : ℕ
3. b : ℕ
⊢ choose(n;n) = 1 ∈ ℕ

---

Latex:

---

Latex:
.....equality..... 
1.  n  :  \mBbbN{}\msupplus{}
2.  a  :  \mBbbN{}
3.  b  :  \mBbbN{}
\mvdash{}  (choose(n;(n  +  1)  -  1)  *  a\^{}((n  +  1)  -  1)  *  b\^{}(n  -  (n  +  1)  -  1))  =  a\^{}n


By

---

Latex:
((Subst  \mkleeneopen{}(n  +  1)  -  1  \msim{}  n\mkleeneclose{}  0\mcdot{}  THEN  Auto)
  THEN  Subst  \mkleeneopen{}n  -  n  \msim{}  0\mkleeneclose{}  0\mcdot{}
  THEN  Auto
  THEN  Reduce  0
  THEN  Subst  \mkleeneopen{}choose(n;n)  \msim{}  1\mkleeneclose{}  0\mcdot{}
  THEN  Auto)

---

Home Index