---

Step * 2 1 of Lemma binomial_q


1. a : ℚ
2. b : ℚ
3. n : ℕ
4. q-rng-nexp(a + b;n) = Σ0 ≤ i < n + 1. choose(n;i) ⋅<ℚ+*> (q-rng-nexp(a;i) * q-rng-nexp(b;n - i)) ∈ ℚ
⊢ a + b ↑ n = Σ0 ≤ i < n + 1. choose(n;i) ⋅<ℚ+*> (a ↑ i * b ↑ n - i) ∈ ℚ
BY
{ (RWO "qexp-eq-q-rng-nexp" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbQ{}
2.  b  :  \mBbbQ{}
3.  n  :  \mBbbN{}
4.  q-rng-nexp(a  +  b;n)  =  \mSigma{}0  \mleq{}  i  <  n  +  1.  choose(n;i)  \mcdot{}<\mBbbQ{}+*>  (q-rng-nexp(a;i)  *  q-rng-nexp(b;n  -  i))
\mvdash{}  a  +  b  \muparrow{}  n  =  \mSigma{}0  \mleq{}  i  <  n  +  1.  choose(n;i)  \mcdot{}<\mBbbQ{}+*>  (a  \muparrow{}  i  *  b  \muparrow{}  n  -  i)


By

---

Latex:
(RWO  "qexp-eq-q-rng-nexp"  0  THEN  Auto)

---

Home Index