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