---

Step * of Lemma binomial-int

∀[a,b:ℤ]. ∀[n:ℕ].  ((a + b)^n = Σ(choose(n;i) * a^i * b^(n - i) | i < n + 1) ∈ ℤ)
BY
{ (Auto
   THEN (InstLemma `binomial` [⌜ℤ-rng⌝;⌜a⌝;⌜b⌝;⌜n⌝]⋅ THENA Auto)
   THEN (RWO "rng_sum-int" (-1) THENA Auto')
   THEN NthHypEq (-1)
   THEN EqCD
   THEN Reduce 0
   THEN Auto
   THEN ((RWO "rng_nexp-int" 0 THENA Auto') THEN EqCD THEN Auto THEN RWO "rng_nat_op-int" 0 THEN Auto THEN Auto')⋅) }

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbZ{}].  \mforall{}[n:\mBbbN{}].    ((a  +  b)\^{}n  =  \mSigma{}(choose(n;i)  *  a\^{}i  *  b\^{}(n  -  i)  |  i  <  n  +  1))


By

---

Latex:
(Auto
  THEN  (InstLemma  `binomial`  [\mkleeneopen{}\mBbbZ{}-rng\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "rng\_sum-int"  (-1)  THENA  Auto')
  THEN  NthHypEq  (-1)
  THEN  EqCD
  THEN  Reduce  0
  THEN  Auto
  THEN  ((RWO  "rng\_nexp-int"  0  THENA  Auto')
              THEN  EqCD
              THEN  Auto
              THEN  RWO  "rng\_nat\_op-int"  0
              THEN  Auto
              THEN  Auto')\mcdot{})

---

Home Index