---

Step * 1 of Lemma binomial_q

.....assertion..... 
∀[a,b:ℚ]. ∀[n:ℕ].
  (q-rng-nexp(a + b;n) = Σ0 ≤ i < n + 1. choose(n;i) ⋅<ℚ+*> (q-rng-nexp(a;i) * q-rng-nexp(b;n - i)) ∈ ℚ)
BY
{ TACTIC:Unfolds ``q-rng-nexp qsum`` 0 }

1
∀[a,b:ℚ]. ∀[n:ℕ].
  (((a + b) ↑<ℚ+*> n) = (Σ(<ℚ+*>) 0 ≤ i < n + 1. choose(n;i) ⋅<ℚ+*> ((a ↑<ℚ+*> i) * (b ↑<ℚ+*> (n - i)))) ∈ ℚ)

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}[a,b:\mBbbQ{}].  \mforall{}[n:\mBbbN{}].
    (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)))


By

---

Latex:
TACTIC:Unfolds  ``q-rng-nexp  qsum``  0

---

Home Index