---

Step * of Lemma binomial-inequality1

∀[a,b:ℕ]. ∀[n:ℕ+].  ((a^n + b^n) ≤ (a + b)^n)
BY
{ xxx(InstLemma `binomial-int` []
      THEN RepeatFor 3 (ParallelLast')
      THEN (HypSubst' (-1) 0 THENA Auto)
      THEN Thin (-1))xxx }

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

---

Latex:

---

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


By

---

Latex:
xxx(InstLemma  `binomial-int`  []
        THEN  RepeatFor  3  (ParallelLast')
        THEN  (HypSubst'  (-1)  0  THENA  Auto)
        THEN  Thin  (-1))xxx

---

Home Index