avewright/proofwiki-math huggingface dataset:
Theorem: Gaussian Binomial Coefficient of 1

:$\dbinom 1 m_q = \delta_{0 m} + \delta_{1 m}$
That is:
:$\dbinom 1 m_q = \begin{cases} 1 & : m = 0 \text { or } m = 1 \\0 & : \text{otherwise} \end{cases}$
where $\dbinom 1 m_q$ denotes a Gaussian binomial coefficient.

Proof:
By definition of Gaussian binomial coefficient:
:$\dbinom 1 m_q = \ds \prod_{k \mathop = 0}^{m - 1} \dfrac {1 - q^{1 - k} } {1 - q^{k + 1} }$
When $m = 0$ the continued product on the {{RHS}} is vacuous, and so:
:$\dbinom 1 0_q = 1$
Let $m > 1$.
Then:
{{begin-eqn}}
{{eqn | l = \dbinom 1 m_q
      | r = \prod_{k \mathop = 0}^{m - 1} \dfrac {1 - q^{1 - k} } {1 - q^{k + 1} }
      | c = {{Defof|Gaussian Binomial Coefficient}}
}}
{{eqn | r = \paren {\dfrac {1 - q^{1 - 0} } {1 - q^{0 + 1} } } \paren {\dfrac {1 - q^{1 - 1} } {1 - q^{1 + 1} } } \paren {\dfrac {1 - q^{1 - 2} } {1 - q^{2 + 1} } } \cdots \paren {\dfrac {1 - q^{1 - \paren {m - 1} } } {1 - q^{\paren {m - 1} + 1} } }
      | c = 
}}
{{eqn | r = \paren {\dfrac {1 - q} {1 - q} } \paren {\dfrac {1 - q^0} {1 - q^2} } \paren {\dfrac {1 - q^{-1} } {1 - q^3} } \cdots \paren {\dfrac {1 - q^{2 - m} } {1 - q^m} }
      | c = 
}}
{{end-eqn}}
When $m > 1$ there exists a factor $1 - q^0 = 0$ in the numerator of the {{RHS}}.
Hence when $m > 1$ we have that $\dbinom 1 m_q = 0$.
We are left with:
{{begin-eqn}}
{{eqn | l = \dbinom 1 1_q
      | r = \prod_{k \mathop = 0}^0 \dfrac {1 - q^{1 - k} } {1 - q^{k + 1} }
      | c = {{Defof|Gaussian Binomial Coefficient}}
}}
{{eqn | r = \dfrac {1 - q^{1 - 0} } {1 - q^{0 + 1} }
}}
{{eqn | r = \dfrac {1 - q} {1 - q}
      | c = 
}}
{{eqn | r = 1
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Gaussian Binomial Coefficients
oo9eck2im768qx0f1l8zuog04uomyba
Theorem: Negated Upper Index of Gaussian Binomial Coefficient

:$\dbinom r k_q = \paren {-1}^k \dbinom {k - r - 1} k_q q^{k r - k \paren {k - 1} / 2}$

Proof:
First note that:
{{begin-eqn}}
{{eqn | l = 1 - q^t
      | r = q^{-t} \dfrac {1 - q^t} {q^{-t} }
      | c = 
}}
{{eqn | r = \dfrac {q^{-t} - 1} {q^{-t} }
      | c = 
}}
{{eqn | r = q^t \paren {q^{-t} - 1}
      | c = 
}}
{{eqn | n = 1
      | r = -q^t \paren {1 - q^{-t} }
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \binom r k_q
      | r = \prod_{j \mathop = 0}^{k - 1} \dfrac {1 - q^{r - j} } {1 - q^{j + 1} }
      | c = {{Defof|Gaussian Binomial Coefficient}}
}}
{{eqn | r = \prod_{j \mathop = 0}^{k - 1} \dfrac {-q^{r - j} \paren {1 - q^{-\paren {r - j} } } } {1 - q^{j + 1} }
      | c = from $(1)$
}}
{{eqn | r = \paren {-1}^k \prod_{j \mathop = 0}^{k - 1} \dfrac {q^{r - j} \paren {1 - q^{-\paren {r - j} } } } {1 - q^{j + 1} }
      | c = 
}}
{{eqn | r = \paren {-1}^k \prod_{j \mathop = 0}^{k - 1} \dfrac {q^{-\paren {j - r} } \paren {1 - q^{j - r} } } {1 - q^{j + 1} }
      | c = 
}}
{{eqn | r = \paren {-1}^k \prod_{j \mathop = 0}^{k - 1} \dfrac {q^{-\paren {\paren {k - 1} - j - r} } \paren {1 - q^{\paren {k - 1} - j - r} } } {1 - q^{j + 1} }
      | c = Permutation of Indices of Product
}}
{{eqn | r = \paren {-1}^k \prod_{j \mathop = 0}^{k - 1} \dfrac {1 - q^{\paren {k - r - 1} - j} } {1 - q^{j + 1} } \prod_{j \mathop = 0}^{k - 1} q^{-\paren {\paren {k - 1} - j - r} }
      | c = 
}}
{{eqn | r = \paren {-1}^k \prod_{j \mathop = 0}^{k - 1} \dfrac {1 - q^{\paren {k - r - 1} - j} } {1 - q^{j + 1} } \prod_{j \mathop = 1}^k q^j \prod_{j \mathop = 0}^{k - 1} q^{r - k}
      | c = 
}}
{{eqn | r = \paren {\paren {-1}^k \prod_{j \mathop = 0}^{k - 1} \dfrac {1 - q^{k - r - 1 - j} } {1 - q^{j + 1} } } q^{k r - k \paren {k - 1} / 2}
      | c = Closed Form for Triangular Numbers and algebra
}}
{{eqn | r = \paren {-1}^k \dbinom {k - r - 1} k_q q^{k r - k \paren {k - 1} / 2}
      | c = {{Defof|Gaussian Binomial Coefficient}}
}}
{{end-eqn}}
{{qed}}
Theorem: Chu-Vandermonde Identity for Gaussian Binomial Coefficients

{{begin-eqn}}
{{eqn | l = \binom {r + s} n_q
      | r = \sum_k \binom r k_q \binom s {n - k}_q q^{\paren {r - k} \paren {n - k} }
      | c = 
}}
{{eqn | r = \sum_k \binom r k_q \binom s {n - k}_q q^{\paren {s - n + k} k}
      | c = 
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{n \mathop \in \Z} \dbinom {r + s} n_q q^{n \paren {n - 1} / 2} x^n
      | r = \prod_{k \mathop = 1}^{r + s} \paren {1 + q^{k - 1} x}
      | c = Gaussian Binomial Theorem
}}
{{eqn | r = \prod_{k \mathop = 1}^r \paren {1 + q^{k - 1} x} \prod_{k \mathop = r + 1}^s \paren {1 + q^{k - 1} x}
      | c = 
}}
{{eqn | r = \prod_{k \mathop = 1}^r \paren {1 + q^{k - 1} x} \prod_{k \mathop = 1}^{s - r} \paren {1 + q^{r + k - 1} x}
      | c = Translation of Index Variable of Product
}}
{{end-eqn}}
{{ProofWanted|Not sure what direction to take this in}}
{{Namedfor|Chu Shih-chieh|name2 = Alexandre-Théophile Vandermonde|cat = Chu|cat2 = Vandermonde}}
Theorem: Symmetry Rule for Gaussian Binomial Coefficients

Let $q \in \R_{\ne 1}, n \in \Z_{>0}, k \in \Z$.
Then:
:$\dbinom n k_q = \dbinom n {n - k}_q$
where $\dbinom n k_q$ is a Gaussian binomial coefficient.

Proof:
If $k < 0$ then $n - k > n$.
Similarly, if $k > n$, then $n - k < 0$.
In both cases:
:$\dbinom n k_q = \dbinom n {n - k}_q = 0$
{{explain|While we do indeed know that $\dbinom n k {{=}} 0$ for $k < 0$ and $k > n$, we haven't demonstrated anywhere that this still holds for $\dbinom n k_q$.}}
Let $0 \le k \le n$.
Consider the case $k \le \dfrac n 2$.
Then $k \le n - k$.
{{begin-eqn}}
{{eqn | l = \binom n {n - k}_q
      | r = \prod_{j \mathop = 0}^{\paren {n - k} - 1} \frac {1 - q^{n - j} } {1 - q^{j + 1} }
      | c = {{Defof|Gaussian Binomial Coefficient}}
}}
{{eqn | r = \paren {\frac {1 - q^{n - 0} } {1 - q^{0 + 1} } } \paren {\frac {1 - q^{n - 1} } {1 - q^{1 + 1} } } \paren {\frac {1 - q^{n - 2} } {1 - q^{2 + 1} } } \cdots \paren {\frac {1 - q^{n - \paren {\paren {n - k} - 1} } } {1 - q^{\paren {\paren {n - k} - 1} + 1} } }
      | c = 
}}
{{eqn | r = \paren {\frac {1 - q^{n - 0} } {1 - q^{0 + 1} } } \paren {\frac {1 - q^{n - 1} } {1 - q^{1 + 1} } } \paren {\frac {1 - q^{n - 2} } {1 - q^{2 + 1} } } \cdots \paren {\frac {1 - q^{n - \paren {k - 1} } } {1 - q^{\paren {k - 1} + 1} } } \paren {\frac {1 - q^{n - k} } {1 - q^{k + 1} } } \cdots \paren {\frac {1 - q^{k + 1} } {1 - q^{n - k} } }
      | c = 
}}
{{eqn | r = \paren {\frac {1 - q^{n - 0} } {1 - q^{0 + 1} } } \paren {\frac {1 - q^{n - 1} } {1 - q^{1 + 1} } } \paren {\frac {1 - q^{n - 2} } {1 - q^{2 + 1} } } \cdots \paren {\frac {1 - q^{n - \paren {k - 1} } } {1 - q^{\paren {k - 1} + 1} } }
      | c = as the tail cancels out
}}
{{eqn | r = \binom n k_q
      | c = {{Defof|Gaussian Binomial Coefficient}}
}}
{{end-eqn}}
The case $k \ge \dfrac n 2$ can be done by observing:
:$n - k \le \dfrac n 2$
and hence by the above:
:$\dbinom n k_q = \dbinom n {n - \paren {n - k} }_q = \dbinom n {n - k}_q$
{{qed}}
Theorem: Reflection Rule for Gaussian Binomial Coefficients

Let $q \in \R_{\ne 1}, n \in \Z_{>0}, k \in \Z$.
Then:
:$\dbinom n k_q = q^{k \paren {n - k} } \dbinom n k_{q^{-1} }$
where $\dbinom n k_q$ is a Gaussian binomial coefficient.

Proof:
{{begin-eqn}}
{{eqn | l = \dbinom n k_{q^{-1} }
      | r = \prod_{j \mathop = 0}^{k - 1} \dfrac {1 - \paren {q^{-1} }^{n - j} } {1 - \paren {q^{-1} }^{j + 1} }
      | c = {{Defof|Gaussian Binomial Coefficient}}
}}
{{eqn | r = \prod_{j \mathop = 0}^{k - 1} \dfrac {\frac {q^{n - j} - 1} {q^{n - j} } } {\frac {q^{j + 1} - 1} {q^{j + 1} } }
      | c = 
}}
{{eqn | r = \prod_{j \mathop = 0}^{k - 1} \dfrac {q^{j + 1} } {q^{n - j} } \dfrac {q^{n - j} - 1} {q^{j + 1} - 1}
      | c = 
}}
{{eqn | r = \prod_{j \mathop = 0}^{k - 1} q^{1 - n + 2 j} \dfrac {1 - q^{n - j} } {1 - q^{j + 1} }
      | c = 
}}
{{eqn | r = \paren {q^{1 - n} }^k \prod_{j \mathop = 0}^{k - 1} q^{2 j} \dfrac {1 - q^{n - j} } {1 - q^{j + 1} }
      | c = 
}}
{{eqn | r = q^{k - n k} q^{k \paren {k - 1} } \prod_{j \mathop = 0}^{k - 1} \dfrac {1 - q^{n - j} } {1 - q^{j + 1} }
      | c = Closed Form for Triangular Numbers: $\ds \sum_{j \mathop = 0}^{k - 1} 2 j = 2 \sum_{j \mathop = 1}^{k - 1} j = 2 \dfrac {\paren {k - 1} k} 2$
}}
{{eqn | r = q^{k^2 - n k} \prod_{j \mathop = 0}^{k - 1} \dfrac {1 - q^{n - j} } {1 - q^{j + 1} }
      | c = 
}}
{{eqn | r = \dfrac 1 {q^{k \paren {n - k} } } \dbinom n k_q
      | c = {{Defof|Gaussian Binomial Coefficient}}
}}
{{end-eqn}}
{{qed}}
Theorem: Gaussian Binomial Theorem/Real Numbers

Let $r \in \R$ be a real number.
:$\ds \sum_{k \mathop \in \Z} \dbinom r k_q q^{k \paren {k - 1} / 2} x^k = \prod_{k \mathop \ge 0} \dfrac {1 + q^k x} {1 + q^{r + k} x}$
where:
:$\dbinom r k_q$ denotes a Gaussian binomial coefficient
:$x \in \R: \size x < 1$
:$q \in \R: \size q < 1$.

Proof:
{{ProofWanted}}
{{Namedfor|Carl Friedrich Gauss}}
Theorem: Gaussian Binomial Theorem/Negation of Upper Index

Let $r \in \R$ be a real number.
{{begin-eqn}}
{{eqn | l = \prod_{k \mathop \ge 0} \dfrac {1 + q^{k + r + 1} x} {1 + q^k x}
      | r = \sum_{k \mathop \in \Z} \dbinom {-r - 1} k_q q^{k \left({k - 1}\right) / 2} \left({-q^{r + 1} x}\right)^k
      | c = 
}}
{{eqn | r = \sum_{k \mathop \in \Z} \dbinom {k + r} x^k
      | c = 
}}
{{end-eqn}}
where:
:$\dbinom r k_q$ denotes a Gaussian binomial coefficient.
:$x \in \R: \left\lvert{x}\right\rvert < 1$
:$q \in \R: \left\lvert{q}\right\rvert < 1$.

Proof:
{{ProofWanted}}
{{Namedfor|Carl Friedrich Gauss}}
Theorem: Binomial Coefficient n Choose k by n Plus 1 Minus n Choose k + 1

Let $\sequence {A_{n k} }$ be a sequence defined on $n, k \in \Z_{\ge 0}$ as:
:$A_{n k} = \begin{cases} 1 & : k = 0 \\
0 & : k \ne 0, n = 0 \\
A_{\paren {n - 1} k} + A_{\paren {n - 1} \paren {k - 1} } + \dbinom n k & : \text{otherwise}
\end{cases}$
Then the closed form for $A_{n k}$ is given as:
:$A_{n k} = \paren {n + 1} \dbinom n k - \dbinom n {k + 1}$

Proof:
The proof proceeds by induction on $n$.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$A_{n k} = \paren {n + 1} \dbinom n k - \dbinom n {k + 1} + \dbinom n k$
=== Basis for the Induction ===
$\map P 0$ is the case $A_{0 k}$:
Let $k = 0$.
Then:
{{begin-eqn}}
{{eqn | l = A_{0 k}
      | r = 1
      | c = 
}}
{{eqn | r = \paren {0 + 1} \dbinom 0 0 - \dbinom 0 {0 + 1}
      | c = Zero Choose n
}}
{{end-eqn}}
Let $k > 0$.
Then:
{{begin-eqn}}
{{eqn | l = A_{0 k}
      | r = 0
      | c = 
}}
{{eqn | r = \paren {0 + 1} \dbinom 0 k - \dbinom 0 {k + 1}
      | c = Zero Choose n
}}
{{end-eqn}}
Thus $\map P 0$ is seen to hold.
This is the basis for the induction.
=== Induction Hypothesis ===
Now it needs to be shown that, if $\map P r$ is true, where $r \ge 0$, then it logically follows that $\map P {r + 1}$ is true.
So this is the induction hypothesis:
:$A_{r k} = \paren {r + 1} \dbinom r k - \dbinom r {k + 1}$
from which it is to be shown that:
:$A_{\paren {r + 1} k} = \paren {r + 2} \dbinom {r + 1} k - \dbinom {r + 1} {k + 1}$
=== Induction Step ===
This is the induction step:
{{begin-eqn}}
{{eqn | l = A_{\paren {r + 1} k}
      | r = A_{r k} + A_{r \paren {k - 1} } + \dbinom {r + 1} k
      | c = {{hypothesis}}
}}
{{eqn | r = \paren {r + 1} \dbinom r k - \dbinom r {k + 1} + \paren {r + 1} \dbinom r {k - 1} - \dbinom r k + \dbinom {r + 1} k
      | c = Induction Hypothesis
}}
{{eqn | r = \paren {r + 1} \paren {\dbinom r k + \dbinom r {k - 1} } - \paren {\dbinom r {k + 1} + \dbinom r k} + \dbinom {r + 1} k
      | c = 
}}
{{eqn | r = \paren {r + 1} \dbinom {r + 1} k - \dbinom {r + 1} {k + 1} + \dbinom {r + 1} k
      | c = Pascal's Rule
}}
{{eqn | r = \paren {r + 2} \dbinom {r + 1} k - \dbinom {r + 1} {k + 1}
      | c = 
}}
{{end-eqn}}
So $\map P r \implies \map P {r + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\forall n, k \in \Z_{\ge 0}: A_{n k} = \paren {n + 1} \dbinom n k - \dbinom n {k + 1}$
{{qed}}
Theorem: Cardinality of Set of Combinations with Repetition

Let $S$ be a finite set with $n$ elements
The number of $k$-combinations of $S$ with repetition is given by:
:$N = \dbinom {n + k - 1} k$

Proof:
Let the elements of $S$ be (totally) ordered in some way, by assigning an index to each element.
Thus let $S = \left\{ {a_1, a_2, a_3, \ldots, a_n}\right\}$.
Thus each $k$-combination of $S$ with repetition can be expressed as:
:$\left\{ {\left\{ {a_{r_1}, a_{r_1}, \ldots, a_{r_k} }\right\} }\right\}$
where:
:$r_1, r_2, \ldots, r_k$ are all elements of $\left\{ {1, 2, \ldots, n}\right\}$
and such that:
:$r_1 \le r_2 \le \cdots \le r_k$
Hence the problem reduces to the number of integer solutions $\left({r_1, r_2, \ldots, r_k}\right)$ such that $1 \le r_1 \le r_2 \le \cdots \le r_k \le n$.
This is the same as the number of solutions to:
:$0 < r_1 < r_2 + 1 < \cdots < r_k + k - 1 < n + k$
which is the same as the number of solutions to:
:$0 < s_1 < s_2 < \cdots < s_k < n + k$
which is the number of ways to choose $k$ elements from $n + k - 1$.
This is the same as the number of subsets as a set with $n + k - 1$ elements.
From Cardinality of Set of Subsets:
:$N = \dbinom {n + k - 1} k$
{{qed}}
Theorem: Sum over k of Unsigned Stirling Number of the First Kind of n+1 with k+1 by Stirling Number of the Second Kind of k with m by -1^k-m

Let $m, n \in \Z_{\ge 0}$.
:$\ds \sum_k {n + 1 \brack k + 1} {k \brace m} \paren {-1}^{k - m} = \sqbrk {n \ge m} \dfrac {n!} {m!}$
where:
:$\sqbrk {n \ge m}$ is Iverson's convention
:$\ds {n + 1 \brack k + 1}$ denotes an unsigned Stirling number of the first kind
:$\ds {k \brace m}$ denotes a Stirling number of the second kind.

Proof:
The proof proceeds by induction on $n$.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\ds \sum_k {n + 1 \brack k + 1} {k \brace m} \paren {-1}^{k - m} = \sqbrk {n \ge m} \dfrac {n!} {m!}$
Theorem: Dixon's Identity/General Case

For $l, m, n \in \Z_{\ge 0}$:
:$\ds \sum_{k \mathop \in \Z} \paren {-1}^k \dbinom {l + m} {l + k} \dbinom {m + n} {m + k} \dbinom {n + l} {n + k} = \dfrac {\paren {l + m + n}!} {l! \, m! \, n!}$

Proof:
From Sum over $k$ of $\dbinom {m - r + s} k$ by $\dbinom {n + r - s} {n - k}$ by $\dbinom {r + k} {m + n}$:
:$\ds \sum_{k \mathop \in \Z} \binom {m - r + s} k \binom {n + r - s} {n - k} \binom {r + k} {m + n} = \binom r m \binom s n$
Setting $\tuple {m, n, r, s, k} \gets \tuple {m + k, l - k, m + n, n + l, j}$ into the equation above, we obtain:
{{begin-eqn}}
{{eqn  | l = \binom r m \binom s n
       | r = \sum_{j \mathop \in \Z} \binom {m - r + s} k \binom {n + r - s} {n - k} \binom {r + k} {m + n}
       | c = before substitution
}}
{{eqn  | l = \binom {m + n} {m + k} \binom {n + l} {l - k}
       | r = \sum_{j \mathop \in \Z} \binom {\paren {m + k} - \paren {m + n} + \paren {n + l} } j \binom {\paren {l - k} + \paren {m + n} - \paren {n + l} } {\paren {l - k} - j} \binom {\paren {m + n } + j} {\paren {m + k} + \paren {l - k} }
       | c = after substitution
}}
{{eqn  | l = \binom {m + n} {m + k} \binom {n + l} {n + k}
       | r = \sum_{j \mathop \in \Z} \binom {l + k} j \binom {m - k} {l - k - j} \binom {m + n + j} {m + l}
       | c = simplifying and Symmetry Rule for Binomial Coefficients
}}
{{end-eqn}}
On the {{LHS}}, we have:
{{begin-eqn}}
{{eqn  | l = \sum_{k \mathop \in \Z} \paren {-1}^k \dbinom {l + m} {l + k} \dbinom {m + n} {m + k} \dbinom {n + l} {n + k}
       | r = \sum_{k \mathop \in \Z} \paren {-1}^k \dbinom {l + m} {l + k} \paren {\sum_{j \mathop \in \Z} \binom {l + k} j \binom {m - k} {l - k - j} \binom {m + n + j} {m + l} }
       | c = substituting from above
}}
{{eqn | r = \sum_{k \mathop \in \Z} \sum_{j \mathop \in \Z} \paren {-1}^k \dbinom {l + m} {l + k} \dbinom {l + k} j \dbinom {m - k} {l - k - j} \dbinom {m + n + j} {m + l}
      | c = 
}}
{{eqn | r = \sum_{k \mathop \in \Z} \sum_{j \mathop \in \Z} \paren {-1}^k \dfrac {\paren {l + m}!} {\paren {l + k}!\paren {m - k}!} \dfrac {\paren {l + k}!} {j!\paren {l - j + k}!} \dfrac {\paren {m - k}!} {\paren {l - j - k}!\paren {j - l + m}!} \dfrac {\paren {m + n + j}!} {\paren {m + l}!\paren {j - l + n}!}
      | c = {{Defof|Binomial Coefficient}}
}}
{{eqn | r = \sum_{k \mathop \in \Z} \sum_{j \mathop \in \Z} \paren {-1}^k \dfrac 1 {j!\paren {l - j + k}!} \dfrac 1 {\paren {l - j - k}!\paren {j - l + m}!} \dfrac {\paren {m + n + j}!} {\paren {j - l + n}!}
      | c = $\paren {l + m}!$, $\paren {l + k}!$ and $\paren {m - k}!$ cancel
}}
{{end-eqn}}
Unless $j = l$ and $k = 0$ the sum on $k$ vanishes.
Therefore:
:$\ds \sum_{k \mathop \in \Z} \paren {-1}^k \dbinom {l + m} {l + k} \dbinom {m + n} {m + k} \dbinom {n + l} {n + k} = \dfrac {\paren {l + m + n}!} {l! \, m! \, n!}$
{{qed}}
{{Namedfor|Alfred Cardew Dixon|cat = Dixon, A.C.}}
Theorem: Dixon's Identity

For $n \in \Z_{\ge 0}$:
:$\ds \sum_{k \mathop \in \Z} \paren {-1}^k \binom {2 n} {n + k}^3 = \dfrac {\paren {3 n}!} {\paren {n!}^3}$

Proof:
Follows directly from Dixon's Identity/General Case:
:$\ds \sum_{k \mathop \in \Z} \paren {-1}^k \dbinom {l + m} {l + k} \dbinom {m + n} {m + k} \dbinom {n + l} {n + k} = \dfrac {\paren {l + m + n}!} {l! \, m! \, n!}$
setting $l = m = n$.
{{qed}}
{{Namedfor|Alfred Cardew Dixon|cat = Dixon, A.C.}}
Theorem: Dixon's Identity/Gaussian Binomial Form/Formulation 2

For $l, m, n \in \Z_{\ge 0}$:
:$\ds \sum_{k \mathop \in \Z} \paren {-1}^k \dbinom {l + m} {l + k}_q \dbinom {m + n} {m + k}_q \dbinom {n + l} {n + k}_q = \dfrac {\paren {l + m + n}!_q} {l!_q \, m!_q \, n!_q}$
where:
:$\dbinom {l + m} {l + k}_q$ denotes a Gaussian binomial coefficient
:$l!_q$ is defined as $\ds \prod_{k \mathop = 1}^n \paren {1 + q + \cdots + q^{k - 1} }$

Proof:
{{ProofWanted}}
{{Namedfor|Alfred Cardew Dixon}}
Theorem: Dixon's Identity/Gaussian Binomial Form/Formulation 1

For $l, m, n \in \Z_{\ge 0}$:
:$\ds \sum_{k \mathop \in \Z} \paren {-1}^k \dbinom {m - r - s} k_q \dbinom {n + r - s} {n - k}_q \dbinom {r + k} {m + n}_q = \dbinom r m_q \dbinom s n_q$
where $\dbinom r m_q$ denotes a Gaussian binomial coefficient

Proof:
{{ProofWanted}}
{{Namedfor|Alfred Cardew Dixon}}
Theorem: Uniqueness of Real z such that x Choose n+1 Equals y Choose n+1 Plus z Choose n

Let $n \in \Z_{\ge 0}$ be a positive integer.
Let $x, y \in \R$ be real numbers which satisfy:
:$n \le y \le x \le y + 1$
Then there exists a unique real number $z$ such that:
:$\dbinom x {n + 1} = \dbinom y {n + 1} + \dbinom z n$
where $n - 1 \le z \le y$.

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \dbinom y {n + 1}
      | o = \le
      | r = \dbinom x {n + 1}
      | c = Ordering of Binomial Coefficients
}}
{{eqn | o = \le
      | r = \dbinom {y + 1} {n + 1}
      | c = 
}}
{{eqn | r = \dbinom y {n + 1} + \dbinom y n
      | c = Pascal's Rule
}}
{{end-eqn}}
{{finish}}
Theorem: X Choose n leq y Choose n + z Choose n-1 where n leq y leq x leq y+1 and n-1 leq z leq y

Let $n \in \Z_{\ge 0}$ be a positive integer.
Let $x, y \in \R$ be real numbers which satisfy:
:$n \le y \le x \le y + 1$
Let $z$ be the unique real number $z$ such that:
:$\dbinom x {n + 1} = \dbinom y {n + 1} + \dbinom z n$
where $n - 1 \le z \le y$.
Its uniqueness is proved at Uniqueness of Real $z$ such that $\dbinom x {n + 1} = \dbinom y {n + 1} + \dbinom z n$.
Then:
:$\dbinom x n \le \dbinom y n + \dbinom z {n - 1}$

Proof:
If $z \ge n$, then from Ordering of Binomial Coefficients:
:$\dbinom z {n + 1} \le \dbinom y {n + 1}$
Otherwise $n - 1 \le z \le n$, and:
:$\dbinom z {n + 1} \le 0 \le \dbinom y {n + 1}$
In either case:
:$(1): \quad \dbinom z {n + 1} \le \dbinom y {n + 1}$
Therefore:
{{begin-eqn}}
{{eqn | l = \dbinom {z + 1} {n + 1}
      | r = \dbinom z {n + 1} + \dbinom z n
      | c = Pascal's Rule
}}
{{eqn | o = \le
      | r = \dbinom y {n + 1} + \dbinom z n
      | c = 
}}
{{eqn | r = \dbinom x {n + 1}
      | c = by hypothesis
}}
{{end-eqn}}
and so $x \ge z + 1$.
Now we are to show that every term of the summation:
:$\ds \binom x {n + 1} - \binom y {n + 1} = \sum_{k \mathop \ge 0} \dbinom {z - k} {n - k} t_k$
where:
:$t_k = \dbinom {x - z - 1 + k} {k + 1} - \dbinom {y - z - 1 + k} {k + 1}$
is negative.
Because $z \ge n - 1$, the binomial coefficient $\dbinom {z - k} {n - k}$ is non-negative.
Because $x \ge z + 1$, the binomial coefficient $\dbinom {x - z - 1 + k} {k + 1}$ is also non-negative.
Therefore:
:$z \le y \le x$
implies that:
:$\dbinom {y - z - 1 + k} {k + 1} \le \dbinom {x - z - 1 + k} {k + 1}$
When $x = y$ and $z = n - 1$ the result becomes:
:$\dbinom x n \le \dbinom x n + \dbinom {n - 1} {n - 1}$
which reduces to:
:$\dbinom x n \le \dbinom x n + 1$
which is true.
Otherwise:
{{begin-eqn}}
{{eqn | l = \dbinom x n - \dbinom y n - \dbinom z {n - 1}
      | r = \sum_{k \mathop \ge 0} \dbinom {z - k} {n - 1 - k} \left({t_k - \delta_{k 0} }\right)
      | c = where $\delta_{k 0}$ is the Kronecker delta
}}
{{eqn | r = \sum_{k \mathop \ge 0} \dfrac {n - k} {z - n + 1} \dbinom {z - k} {n - k} \left({t_k - \delta_{k 0} }\right)
      | c = Factors of Binomial Coefficient
}}
{{end-eqn}}
This is less than or equal to:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop \ge 0} \dfrac {n - 1} {z - n + 1} \dbinom {z - k} {n - k} \left({t_k - \delta_{k 0} }\right)
      | r = \dfrac {n - 1} {z - n + 1} \left({\dbinom x {n + 1} - \dbinom y {n + 1} - \dbinom z n}\right)
      | c = 
}}
{{eqn | r = 0
      | c = because $t_0 - 1 = x - y - 1 \le 0$
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Upper Bound for Binomial Coefficient

Let $n, k \in \Z$ such that $n \ge k \ge 0$.
Then:
:$\dbinom n k \le \left({\dfrac {n e} k}\right)^k$
where $\dbinom n k$ denotes a binomial coefficient.

Proof:
From Lower and Upper Bound of Factorial, we have that:
:$\dfrac {k^k} {e^{k - 1} } \le k!$
so that:
:$(1): \quad \dfrac 1 {k!} \le \dfrac {e^{k - 1} } {k^k}$
Then:
{{begin-eqn}}
{{eqn | l = \dbinom n k
      | r = \dfrac {n^\underline k} {k!}
      | c = {{Defof|Binomial Coefficient}}
}}
{{eqn | o = \le
      | r = \dfrac {n^k} {k!}
      | c = 
}}
{{eqn | o = \le
      | r = \dfrac {n^k e^{k - 1} } {k^k}
      | c = from $(1)$
}}
{{eqn | o = \le
      | r = \dfrac {n^k e^k} {k^k}
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Lower Bound for Binomial Coefficient

Let $n, k \in \Z$ such that $n \ge k \ge 0$.
Then:
:$\dbinom n k \ge \paren {\dfrac {\paren {n - k} e} k}^k \dfrac 1 {e k}$
where $\dbinom n k$ denotes a binomial coefficient.

Proof:
From Lower and Upper Bound of Factorial, we have that:
:$k! \le \dfrac {k^{k + 1} } {e^{k - 1} }$
so that:
:$(1): \quad \dfrac 1 {k!} \ge \dfrac {e^{k - 1} } {k^{k + 1} }$
Then:
{{begin-eqn}}
{{eqn | l = \dbinom n k
      | r = \dfrac {n^\underline k} {k!}
      | c = {{Defof|Binomial Coefficient}}
}}
{{eqn | o = \ge
      | r = \dfrac {\paren {n - k}^k} {k!}
      | c = 
}}
{{eqn | o = \ge
      | r = \dfrac {\paren {n - k}^k e^{k - 1} } {k^{k + 1} }
      | c = from $(1)$
}}
{{eqn | r = \dfrac {\paren {n - k}^k e^k} {k^k} \dfrac 1 {e k}
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Sum over k of n Choose k by p^k by (1-p)^n-k by Absolute Value of k-np

Let $n \in \Z_{\ge 0}$ be a non-negative integer.
Then:
:$\ds \sum_{k \mathop \in \Z} \dbinom n k p^k \paren {1 - p}^{n - k} \size {k - n p} = 2 \ceiling {n p} \dbinom n {\ceiling {n p} } p^{\ceiling {n p} } \paren {1 - p}^{n - 1 - \ceiling {n p} }$

Proof:
Let $t_k = k \dbinom n k p^k \paren {1 - p}^{n + 1 - k}$.
Then:
:$t_k - t_{k + 1} = \dbinom n k p^k \paren {1 - p}^{n - k} \paren {k - n p}$
Thus the stated summation is:
:$\ds \sum_{k \mathop < \ceiling {n p} } \paren {t_{k + 1} - t_k} + \sum_{k \mathop \ge \ceiling {n p} } \paren {t_k - t_{k + 1} } = 2 t_{\ceiling {n p} }$
{{qed}}