---

Step * 1 1 of Lemma binomial_q


∀[a,b:ℚ]. ∀[n:ℕ].
  (((a + b) ↑<ℚ+*> n) = (Σ(<ℚ+*>) 0 ≤ i < n + 1. choose(n;i) ⋅<ℚ+*> ((a ↑<ℚ+*> i) * (b ↑<ℚ+*> (n - i)))) ∈ ℚ)
BY
{ (ProveSpecializedLemmaWReduce binomial) 0 [⌜parm{i}⌝;⌜<ℚ+*>⌝]⋅ }

---

Latex:

---

Latex:

\mforall{}[a,b:\mBbbQ{}].  \mforall{}[n:\mBbbN{}].
    (((a  +  b)  \muparrow{}<\mBbbQ{}+*>  n)
    =  (\mSigma{}(<\mBbbQ{}+*>)  0 
                            \mleq{}  i 
                            <  n  +  1
            choose(n;i)  \mcdot{}<\mBbbQ{}+*>  ((a  \muparrow{}<\mBbbQ{}+*>  i)  *  (b  \muparrow{}<\mBbbQ{}+*>  (n  -  i)))))


By

---

Latex:
(ProveSpecializedLemmaWReduce  binomial)  0  [\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}<\mBbbQ{}+*>\mkleeneclose{}]\mcdot{}

---

Home Index