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