---

Step * of Lemma binomial_q

No Annotations
∀[a,b:ℚ]. ∀[n:ℕ].  (a + b ↑ n = Σ0 ≤ i < n + 1. choose(n;i) ⋅<ℚ+*> (a ↑ i * b ↑ n - i) ∈ ℚ)
BY
{ TACTIC:Assert ⌜∀[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))
                   ∈ ℚ)⌝⋅ }

1
.....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)) ∈ ℚ)

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

---

Latex:

---

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


By

---

Latex:
TACTIC:Assert  \mkleeneopen{}\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)))\mkleeneclose{}\mcdot{}

---

Home Index