---

Step * of Lemma exp-difference-inequality

∀[n:ℕ+]. ∀[a,b:ℕ].  (((a + b)^n - a^n) ≤ (n * b * (a + b)^(n - 1)))
BY
{ (Auto
   THEN (InstLemma `binomial-int` [⌜a⌝;⌜b⌝;⌜n⌝]⋅ THENA Auto)
   THEN (RWO "-1" 0 THENA Auto)
   THEN Thin (-1)
   THEN (InstLemma `binomial-int` [⌜a⌝;⌜b⌝;⌜n - 1⌝]⋅ THENA Auto)
   THEN ((RWO "-1" 0 THENA (Auto THEN Auto')) THEN Thin (-1) THEN (RWO "sum_scalar_mult" 0 THENA (Auto THEN Auto')))⋅) }

1
1. n : ℕ+
2. a : ℕ
3. b : ℕ
⊢ (Σ(choose(n;i) * a^i * b^(n - i) | i < n + 1) - a^n) ≤ (n
  * Σ(b * choose(n - 1;i) * a^i * b^(n - 1 - i) | i < (n - 1) + 1))

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[a,b:\mBbbN{}].    (((a  +  b)\^{}n  -  a\^{}n)  \mleq{}  (n  *  b  *  (a  +  b)\^{}(n  -  1)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `binomial-int`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  Thin  (-1)
  THEN  (InstLemma  `binomial-int`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}n  -  1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ((RWO  "-1"  0  THENA  (Auto  THEN  Auto'))
              THEN  Thin  (-1)
              THEN  (RWO  "sum\_scalar\_mult"  0  THENA  (Auto  THEN  Auto')))\mcdot{})

---

Home Index