avewright/proofwiki-math huggingface dataset:
Theorem: Sum over k of n+k Choose 2 k by 2 k Choose k by -1^k over k+1

:$\ds \sum_k \binom {n + k} {2 k} \binom {2 k} k \frac {\paren {-1}^k} {k + 1} = \sqbrk {n = 0}$

Proof:
{{begin-eqn}}
{{eqn | r = \sum_k \binom {n + k} {2 k} \binom {2 k} k \frac {\left({-1}\right)^k} {k + 1}
      | o = 
      | c = 
}}
{{eqn | r = \sum_k \binom {n + k} k \binom n k \frac {\left({-1}\right)} {k + 1}
      | c = Product of $\dbinom r m$ with $\dbinom m k$
}}
{{eqn | r = \sum_k \binom {n + k} k \binom {n + 1} {k + 1} \frac {\left({-1}\right)^k} {n + 1}
      | c = Factors of Binomial Coefficient
}}
{{eqn | r = \frac 1 {n + 1} \sum_k \binom {- \left({n + 1}\right)} k \binom {n + 1} {k + 1}
      | c = Negated Upper Index of Binomial Coefficient
}}
{{eqn | r = \frac 1 {n + 1} \binom {n + 1 - \left({n + 1}\right)} {n + 1 - 1 + 0}
      | c = Sum over $k$ of $\dbinom r {m + k} \dbinom s {n + k}$
}}
{{eqn | r = \frac 1 {n + 1} \binom 0 n
      | c = 
}}
{{eqn | r = \left[{n = 0}\right]
      | c = {{Defof|Binomial Coefficient}}
}}
{{end-eqn}}
{{qed}}
Theorem: Sum over k of n+k Choose m+2k by 2k Choose k by -1^k over k+1

:$\ds \sum_k \binom {n + k} {m + 2 k} \binom {2 k} k \frac {\paren {-1}^k} {k + 1} = \binom {n - 1} {m - 1}$

Proof:
From Sum over $k$ of $\dbinom {r - k} m \dbinom {s + k} n$:
:$\ds \sum_{k \mathop = 0}^r \binom {r - k} m \binom {s + k} n = \binom {r + s + 1} {m + n + 1}$
Setting $r = n + k - 1$, $m = 2 k$, $s = 0$, $n = m - 1$ and using $j$ as the index variable, this gives us:
:$\ds \sum_{j \mathop = 0}^{n + k - 1} \binom {n + k - 1 - j} {2 k} \binom j {m - 1} = \dbinom {n + k} {m + 2 k}$
This leads to:
:$\ds \sum_k \binom {n + k} {m + 2 k} \binom {2 k} k \frac {\paren {-1}^k} {k + 1} = \sum_k \sum_{j \mathop = 0}^{n + k - 1} \binom {n + k - 1 - j} {2 k} \binom {2 k} k \binom j {m - 1} \frac {\paren {-1} } {k + 1}$
Note that the terms of the above are $0$ when $n \le j < n + k - 1$.
This means that $k \ge 1$.
So:
:$0 \le n + k - 1 - j \le k - i < 2 k$
Thus the first binomial coefficient in the above will vanish.
The condition on the second summation can then be replaced by $0 \le j < n$.
After exchange of summation and application of Sum over $k$ of $\dbinom {n + k} {2 k} \dbinom {2 k} k \dfrac {-1^k} {k + 1}$ converts it into:
:$\ds \sum_{0 \mathop \le j \mathop < n} \binom j {m - 1} \delta_{\paren {n \mathop - 1} \mathop j}$
where $\delta_{\paren {n \mathop - 1} \mathop j}$ denotes the Kronecker delta.
All terms are therefore $0$ except where $j = n - 1$.
Hence the result.
{{qed}}
Theorem: Sum over k of n+k Choose m+2k by 2k Choose k by -1^k over k+1

:$\ds \sum_k \binom {n + k} {m + 2 k} \binom {2 k} k \frac {\paren {-1}^k} {k + 1} = \binom {n - 1} {m - 1}$

Proof:
Let:
:$\ds S := \sum_k \binom {n + k} {m + 2 k} \binom {2 k} k \frac {\paren {-1}^k} {k + 1}$
Then:
{{begin-eqn}}
{{eqn | l = \binom {2 k + 1} {k + 1}
      | r = \binom {2 k} k \frac {2 k + 1} {k + 1}
      | c = Factors of Binomial Coefficient
}}
{{eqn | ll= \leadsto
      | l = \binom {2 k} k
      | r = \binom {2 k + 1} {k + 1} \frac {k + 1} {2 k + 1}
      | c = 
}}
{{eqn | r = \binom {2 k + 1} k \frac {k + 1} {2 k + 1}
      | c = Symmetry Rule for Binomial Coefficients
}}
{{end-eqn}}
Also:
{{begin-eqn}}
{{eqn | l = \binom {n + k} {m + 2 k}
      | r = \paren {-1}^{n + k - m - 2 k} \binom {-\paren {m + 2 k + 1} } {n + k - m - 2 k}
      | c = Moving Top Index to Bottom in Binomial Coefficient
}}
{{eqn | r = \paren {-1}^{n - m - k} \binom {- m - 2 k - 1} {n - m - k}
      | c = 
}}
{{end-eqn}}
Reassembling $S$:
:$\ds S = \sum_k \binom {1 + 2 k} k \binom {-m - 2 k - 1} {n - m - k} \frac {\paren {-1}^{n - m} } {1 + 2 k}$
Recall Sum over $k$ of $\dbinom {r - t k} k$ by $\dbinom {s - t \paren {n - k} } {n - k}$ by $\dfrac r {r - t k}$:
:$\ds \sum_{k \mathop \ge 0} \binom {r - t k} k \binom {s - t \paren {n - k} } {n - k} \frac r {r - t k} = \binom {r + s - t n} n$
Making the following substitutions:
:$r \gets 1$
:$t \gets -2$
:$n \gets n - m$
we obtain:
{{begin-eqn}}
{{eqn | l = s + 2 \paren {n - m - k}
      | r = - m - 2 k - 1
}}
{{eqn | ll= \leadsto
      | l = s
      | r = m - 2 n - 1
}}
{{eqn | ll= \leadsto
      | l = \sum_{k \mathop \ge 0} \binom {r - t k} k \binom {s - t \paren {n - k} } {n - k} \frac r {r - t k}
      | r = \sum_{k \mathop \ge 0} \binom {1 + 2 k} k \binom {- m - 2 k - 1} {n - m - k} \frac 1 {1 + 2 k}
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = S
      | r = \paren {-1}^{n - m} \sum_k \binom {1 + 2 k} k \binom {- m - 2 k - 1} {n - m - k} \frac 1 {1 + 2 k}
      | c = 
}}
{{eqn | r = \paren {-1}^{n - m} \binom {1 + \paren {m - 2 n - 1} + 2 \paren {n - m} } {n - m}
      | c = 
}}
{{eqn | r = \paren {-1}^{n - m} \binom {- m} {n - m}
      | c = 
}}
{{eqn | r = \binom {n - 1} {n - m}
      | c = Negated Upper Index of Binomial Coefficient
}}
{{eqn | r = \binom {n - 1} {m - 1}
      | c = Symmetry Rule for Binomial Coefficients
}}
{{end-eqn}}
{{qed}}
Theorem: Intersection of Ideals with Suprema Succeed Element equals Way Below Closure of Element

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a complete lattice.
Let $x \in S$.
Then:
:$\ds \bigcap \set {I \in \mathit {Ids}: x \preceq \sup I} = x^\ll$
where $\mathit {Ids}$ denotes the set of all ideals in $L$.

Proof:
By Supremum of Lower Closure of Element:
:$\map \sup {x^\preceq} = x$
By Lower Closure of Element is Ideal:
:$x^\preceq \in \mathit {Ids}$
Then by definition of reflexivity:
:$x^\preceq \in \set {I \in \mathit {Ids}: x \preceq \sup I}$
We will prove that:
:$\ds \bigcap \set {I \in \mathit {Ids}: x \preceq \sup I} \subseteq x^\ll$
Let $z \in \ds \bigcap \set {I \in \mathit {Ids}: x \preceq \sup I}$
By definition of intersection:
:$\forall I \in \mathit {Ids}: x \preceq \sup I \implies z \in I$
By Way Below iff Second Operand Preceding Supremum of Ideal implies First Operand is Element of Ideal:
:$z \ll x$
Thus by definition of way below closure:
:$z \in x^\ll$
{{qed|lemma}}
By definition of set equality, it remains to prove the pposite inclusion.
Let $z \in x^\ll$
By definition of way below closure:
:$z \ll x$
We will prove that
:$\forall Y \in \set {I \in \mathit {Ids}: x \preceq \sup I}: z \in Y$
Let $Y \in \set {I \in \mathit {Ids}: x \preceq \sup I}$
Then
:$Y \in \mathit {Ids}$ and $x \preceq \sup Y$
Thus Way Below iff Second Operand Preceding Supremum of Ideal implies First Operand is Element of Ideal:
:$z \in Y$
{{qed|lemma}}
Thus by definition of intersection:
:$z \in \ds \bigcap \set {I \in \mathit {Ids}: x \preceq \sup I}$
{{qed}}
Theorem: Way Below Closure is Ideal in Bounded Below Join Semilattice

Let $L = \struct {S, \vee, \preceq}$ be a bounded below join semilattice.
Let $x \in S$.
Then
:$x^\ll$ is ideal in $L$.

Proof:
By Way Below Closure is Directed in Bounded Below Join Semilattice:
:$x^\ll$ is a non-empty directed set.
Let $y \in x^\ll, z \in S$ such that
:$z \preceq y$
By definition of way below closure:
:$y \ll x$
By definition of reflexivity:
:$x \preceq x$
By Preceding and Way Below implies Way Below:
:$z \ll x$
Thus by definition of way below closure:
:$z \in x^\ll$
Thus by definition
:$x^\ll$ is a lower section.
Thus by definition
:$x^\ll$ is an ideal in $L$.
{{qed}}
Theorem: Sum over k of r-kt Choose k by r over r-kt by s-(n-k)t Choose n-k by s over s-(n-k)t

For $n \in \Z_{\ge 0}$:
:$\ds \sum_k \map {A_k} {r, t} \map {A_{n - k} } {s, t} = \map {A_n} {r + s, t}$
where $\map {A_n} {x, t}$ is the polynomial of degree $n$ defined as:
:$\map {A_n} {x, t} = \dbinom {x - n t} n \dfrac x {x - n t}$
where $x \ne n t$.

Proof:
Let:
:$\ds S = \sum_k \map {A_k} {r, t} \map {A_{n - k} } {s, t}$
Both sides of the statement of the theorem are polynomials in $r$, $s$ and $t$.
Therefore it can be assumed that $r \ne k t \ne s$ for $0 \le k \le n$ or something will become undefined.
By replacing the polynomials $A_n$ with their binomial coefficient definitions, the theorem can be expressed as:
:$\ds S = \sum_k \dbinom {r - k t} k  \dbinom {s - \paren {n - k} t} {n - k} \dfrac r {r - k t} \dfrac s {s - \paren {n - k} t}$
Using the technique of partial fractions:
:$\dfrac 1 {r - k t} \dfrac 1 {s - \paren {n - k} t} = \dfrac 1 {r + s - n t} \paren {\dfrac 1 {r - k t} + \dfrac 1 {s - \paren {n - k} t} }$
Thus:
:$\ds S = \frac s {r + s - n t} \sum_k \dbinom {r - k t} k \dbinom {s - \paren {n - k} t} {n - k} \dfrac r {r - k t} + \frac r {r + s - n t} \sum_k \dbinom {r - k t} k \dbinom {s - \paren {n - k} t} {n - k} \dfrac s {s - \paren {n - k} t}$
From Sum over $k$ of $\dbinom {r - t k} k \dbinom {s - t \paren {n - k} } {n - k} \dfrac r {r - t k}$:
:$\ds \sum_{k \mathop \ge 0} \binom {r - t k} k \binom {s - t \paren {n - k} } {n - k} \frac r {r - t k} = \binom {r + s - t n} n$
for $r, s, t \in \R, n \in \Z$.
Thus we have:
:$S = \dfrac s {r + s - n t} \dbinom {r + s - t n} n + \dfrac r {r + s - n t} \dbinom {s + r - t n} n$
after changing $k$ to $n - k$ in the second term.
That is:
:$S = \dbinom {r + s - n t} n \dfrac {r + s} {r + s - n t}$
which is $\map {A_n} {r + s, t}$.
{{qed}}
Theorem: Sum over k of r-kt Choose k by r over r-kt by s-(n-k)t Choose n-k by s over s-(n-k)t

For $n \in \Z_{\ge 0}$:
:$\ds \sum_k \map {A_k} {r, t} \map {A_{n - k} } {s, t} = \map {A_n} {r + s, t}$
where $\map {A_n} {x, t}$ is the polynomial of degree $n$ defined as:
:$\map {A_n} {x, t} = \dbinom {x - n t} n \dfrac x {x - n t}$
where $x \ne n t$.

Proof:
From Sum over $k$ of $\dbinom {r - k t} k$ by $\dfrac r {r - k t}$ by $z^k$:
:$\ds \sum_k \map {A_k} {r, t} z^k = x^r$
and:
:$\ds \sum_k \map {A_k} {s, t} z^k = x^s$
Hence:
{{begin-eqn}}
{{eqn | l = x^{r + s}
      | r = \sum_k \map {A_k} {r, t} z^k \sum_k \map {A_k} {s, t} z^k
      | c = 
}}
{{eqn | r = \sum_k \map {A_k} {r + s, t} z^k
      | c = 
}}
{{end-eqn}}
Taking the $z^n$ coefficient:
{{begin-eqn}}
{{eqn | l = \sum_k \map {A_k} {r, t} z^k \sum_k \map {A_{n - k} } {s, t} z^{n - k}
      | r = \map {A_n} {r + s, t} z^n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sum_k \map {A_k} {r, t} \sum_k \map {A_{n - k} } {s, t}
      | r = \map {A_n} {r + s, t}
}}
{{end-eqn}}
{{qed}}
Theorem: Sum over k of r Choose k by -1^r-k by Polynomial

Let $r \in \Z_{\ge 0}$.
Then:
:$\ds \sum_k \binom r k \paren {-1}^{r - k} \map {P_r} k = r! \, b_r$
where:
:$\map {P_r} k = b_0 + b_1 k + \cdots + b_r k^r$ is a polynomial in $k$ of degree $r$.

Proof:
From the {{Corollary|Sum over k of r Choose k by s+k Choose n by -1^r-k|disp = Sum over $k$ of $\dbinom r k \dbinom {s + k} n \paren {-1}^{r - k}$}}:
:$\ds \sum_k \binom r k \binom k n \paren {-1}^{r - k} = \delta_{n r}$
where $\delta_{n r}$ denotes the Kronecker delta.
Thus when $n \ne r$:
:$\ds \sum_k \binom r k \binom k n \paren {-1}^{r - k} = 0$
and so:
:$\ds \sum_k \binom r k \paren {-1}^{r - k} \paren {c_0 \binom k 0 + c_1 \binom k 1 + \cdots + c_m \binom k m} = c_r$
as the only term left standing is the $r$th one.
Choosing the coefficients $c_i$ as appropriate, a polynomial in $k$ can be expressed as a summation of binomial coefficients in the form:
:$c_0 \dbinom k 0 + c_1 \dbinom k 1 + \cdots + c_m \dbinom k m$
Thus we can rewrite such a polynomial in $k$ as:
:$b_0 + b_1 k + \cdots + b_r k^r$
Since each $c_m \dbinom k m$ is a polynomial of degree $m$, it follows that the only one with a non-zero degree $r$ term is $c_r \dbinom k r$.
The coefficient of $k^r$ in $c_r \dbinom k r$ must be equal to $b_r$, that is:
:$b_r = \dfrac {c_r}{r!}$
Hence the result.
{{qed}}
Theorem: Sum over k of r Choose k by -1^r-k by Polynomial

Let $r \in \Z_{\ge 0}$.
Then:
:$\ds \sum_k \binom r k \paren {-1}^{r - k} \map {P_r} k = r! \, b_r$
where:
:$\map {P_r} k = b_0 + b_1 k + \cdots + b_r k^r$ is a polynomial in $k$ of degree $r$.

Proof:
From Summation of Powers over Product of Differences:
:$\ds \sum_{j \mathop = 1}^n \begin {pmatrix} {\dfrac { {x_j}^r} {\ds \prod_{\substack {1 \mathop \le k \mathop \le n \\ k \mathop \ne j} } \paren {x_j - x_k} } } \end {pmatrix} = \begin {cases} 0 & : 0 \le r < n - 1 \\ 1 & : r = n - 1 \\ \ds \sum_{j \mathop = 1}^n x_j & : r = n \end {cases}$
Now we have:
{{begin-eqn}}
{{eqn | l = \frac {\paren {-1}^k \dbinom n k} {n!}
      | r = \frac {\paren {-1}^k} {k! \paren {n - k}!}
      | c = 
}}
{{eqn | r = \frac {\paren {-1}^k} {\ds \prod_{\substack {1 \mathop \le k \mathop \le n \\ k \mathop \ne j} } \paren {k - j} }
      | c = 
}}
{{end-eqn}}
{{proof wanted|in progress}}
Theorem: Sum over k of r Choose k by s-kt Choose r by -1^k

Let $r \in \Z_{\ge 0}$.
Then:
:$\ds \sum_k \binom r k \binom {s - k t} r \paren {-1}^k = t^r$
where $\dbinom r k$ etc. are binomial coefficients.

Proof:
From Sum over $k$ of $\dbinom r k \paren {-1}^k$ by Polynomial:
:$\ds \sum_k \binom r k \paren {-1}^{r - k} \map {P_r} k = r! \, b_r$
where:
:$\map {P_r} k = b_0 + b_1 k + \cdots + b_r k^r$ is a polynomial in $k$ of degree $r$.
{{proof wanted}}
Theorem: Sum over k of -2 Choose k

:$\ds \sum_{k \mathop = 0}^n \binom {-2} k = \paren {-1}^n \ceiling {\dfrac {n + 1} 2}$
where:
:$\dbinom {-2} k$ is a binomial coefficient
:$\ceiling x$ denotes the ceiling of $x$.

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 0}^n \binom {-2} k
      | r = \sum_{k \mathop = 0}^n \paren {-1} \binom {k - \paren {-2} - 1} k
      | c = Negated Upper Index of Binomial Coefficient
}}
{{eqn | r = \sum_{k \mathop = 0}^n \paren {-1} \binom {k + 1} k
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 0}^n \paren {-1} \paren {k + 1}
      | c = Binomial Coefficient with Self minus One
}}
{{eqn | r = 1 - 2 + 3 - 4 + \cdots \pm \paren {n + 1}
      | c = 
}}
{{eqn | r = \paren {1 + 2 + 3 + 4 + \cdots + \paren {n + 1} } - 2 \times \paren {2 + 4 + 6 + 8 + \cdots + m}
      | c = where $m = n$ or $m = n + 1$ according to whether $n$ is odd or even
}}
{{end-eqn}}
When $n$ is even, we have:
{{begin-eqn}}
{{eqn | r = \paren {1 + 2 + 3 + 4 + \cdots + \paren {n + 1} } - 2 \times \paren {2 + 4 + 6 + 8 + \cdots + n}
      | o = 
      | c = 
}}
{{eqn | r = \paren {1 + 2 + 3 + 4 + \cdots + \paren {n + 1} } - 4 \paren {1 + 2 + 3 + 4 + \cdots + \frac n 2}
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 2}^{n + 1} k - 4 \sum_{k \mathop = 1}^{\frac n 2} k
      | c = 
}}
{{eqn | r = \frac {\paren {n + 1} \paren {n + 2} } 2 - 4 \frac {\frac n 2 \paren {\frac n 2 + 1} } 2
      | c = Closed Form for Triangular Numbers
}}
{{eqn | r = \frac {\paren {n + 1} \paren {n + 2} } 2 - \frac {n \paren {n + 2} } 2
      | c = simplifying
}}
{{eqn | r = \frac {\paren {n + 2} \paren {n + 1 - n} } 2
      | c = simplifying
}}
{{eqn | r = \frac {n + 2} 2
      | c = simplifying
}}
{{end-eqn}}
As $n$ is even, $n + 1$ is odd, and so:
:$\dfrac {n + 2} 2 = \paren {-1}^n \ceiling {\dfrac {n + 1} 2}$
{{qed|lemma}}
When $n$ is odd, we have:
{{begin-eqn}}
{{eqn | r = \paren {1 + 2 + 3 + 4 + \cdots + \paren {n + 1} } - 2 \times \paren {2 + 4 + 6 + 8 + \cdots + n + 1}
      | o = 
      | c = 
}}
{{eqn | r = \paren {1 + 2 + 3 + 4 + \cdots + \paren {n + 1} } - 4 \paren {1 + 2 + 3 + 4 + \cdots + \frac {n + 1} 2}
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 2}^{n + 1} k - 4 \sum_{k \mathop = 1}^{\frac {n + 1} 2} k
      | c = 
}}
{{eqn | r = \frac {\paren {n + 1} \paren {n + 2} } 2 - 4 \frac {\frac {n + 1} 2 \paren {\frac {n + 1} 2 + 1} } 2
      | c = Closed Form for Triangular Numbers
}}
{{eqn | r = \frac {\paren {n + 1} \paren {n + 2} } 2 - \frac {\paren {n + 1} \paren {n + 3} } 2
      | c = simplifying
}}
{{eqn | r = \frac {\paren {n + 1} \paren {\paren {n + 2} - \paren {n + 3} } } 2
      | c = simplifying
}}
{{eqn | r = \paren {-1} \frac {n + 1} 2
      | c = simplifying
}}
{{end-eqn}}
As $n$ is odd, $n + 1$ is even, and so $\dfrac {n + 1} 2$ is an integer.
Thus from Real Number is Integer iff equals Ceiling:
:$\paren {-1} \dfrac {n + 1} 2 = \paren {-1}^n \ceiling {\dfrac {n + 1} 2}$
{{qed|lemma}}
Thus:
:$\ds \sum_{k \mathop = 0}^n \binom {-2} k = \paren {-1}^n \ceiling {\dfrac {n + 1} 2}$
whether $n$ is odd or even.
Hence the result.
{{qed}}
Theorem: Sum over k of m Choose k by k minus m over 2

:$\ds \sum_{k \mathop = 0}^n \binom m k \paren {k - \dfrac m 2} = -\dfrac m 2 \binom {m - 1} n$
where $\dbinom m k$ etc. are binomial coefficients.

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 0}^n \binom m k \paren {k - \dfrac m 2}
      | r = \sum_{k \mathop = 0}^n k \binom m k - \dfrac m 2 \sum_{k \mathop = 0}^n \binom m k
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 0}^n m \binom {m - 1} {k - 1} - \dfrac m 2 \sum_{k \mathop = 0}^n \binom m k
      | c = Factors of Binomial Coefficient
}}
{{eqn | r = \dfrac m 2 \sum_{k \mathop = 0}^n \paren {2 \binom {m - 1} {k - 1} - \binom m k}
      | c = 
}}
{{eqn | r = \dfrac m 2 \sum_{k \mathop = 0}^n \paren {2 \binom {m - 1} {k - 1} - \paren {\binom {m - 1} {k - 1} + \binom {m - 1} k} }
      | c = Pascal's Rule
}}
{{eqn | r = \dfrac m 2 \sum_{k \mathop = 0}^n \paren {\binom {m - 1} {k - 1} - \binom {m - 1} k}
      | c = simplifying
}}
{{eqn | r = \dfrac m 2 \paren {\binom {m - 1} {-1} - \binom {m - 1} n}
      | c = as the series telescopes
}}
{{eqn | r = -\dfrac m 2 \binom {m - 1} n
      | c = {{Defof|Binomial Coefficient}} for negative lower index
}}
{{end-eqn}}
{{qed}}
Theorem: Binomial Coefficient is instance of Gaussian Binomial Coefficient

Let $\dbinom r m_q$ denote the Gaussian binomial coefficient:
Then:
:$\ds \lim_{q \mathop \to 1^-} \dbinom r m_q = \dbinom r m$
where $\dbinom r m$ denotes the conventional binomial coefficient.

Proof:
We have by definition of Gaussian binomial coefficient:
:$\ds \dbinom r m_q = \prod_{k \mathop = 0}^{m - 1} \dfrac {1 - q^{r - k} } {1 - q^{k + 1} }$
Consider a typical factor of this continued product:
{{begin-eqn}}
{{eqn | l = \dfrac {1 - q^{r - k} } {1 - q^{k + 1} }
      | r = \dfrac {\paren {1 - q^{r - k} } / \paren {1 - q} } {\paren {1 - q^{k + 1} } / \paren {1 - q} }
      | c = multiplying top and bottom by $1 - q$
}}
{{eqn | r = \dfrac {\sum_{j \mathop = 0}^{r - k - 1} q^j} {\sum_{j \mathop = 0}^k q^j}
      | c = Sum of Geometric Sequence
}}
{{eqn | ll= \leadsto
      | l = \lim_{q \mathop \to 1^-} \dfrac {1 - q^{r - k} } {1 - q^{k + 1} }
      | r = \lim_{q \mathop \to 1^-} \dfrac {\sum_{j \mathop = 0}^{r - k - 1} q^j} {\sum_{j \mathop = 0}^k q^j}
      | c = 
}}
{{eqn | r = \dfrac {\sum_{j \mathop = 0}^{r - k - 1} 1} {\sum_{j \mathop = 0}^k 1}
      | c = 
}}
{{eqn | r = \dfrac {r - k} {k + 1}
      | c = 
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \lim_{q \mathop \to 1^-} \dbinom r k_q
      | r = \prod_{k \mathop = 0}^{m - 1} \dfrac {r - k} {k + 1}
      | c = 
}}
{{eqn | r = \prod_{k \mathop = 1}^m \dfrac {r + 1 - k} k
      | c = Translation of Index Variable of Product
}}
{{eqn | r = \dbinom r m
      | c = {{Defof|Binomial Coefficient}}
}}
{{end-eqn}}
{{qed}}
Theorem: Multinomial Coefficient expressed as Product of Binomial Coefficients

:$\dbinom {k_1 + k_2 + \cdots + k_m} {k_1, k_2, \ldots, k_m} = \dbinom {k_1 + k_2} {k_1} \dbinom {k_1 + k_2 + k_3} {k_1 + k_2} \cdots \dbinom {k_1 + k_2 + \cdots + k_m} {k_1 + k_2 + \cdots + k_{m - 1} }$
where:
:$\dbinom {k_1 + k_2 + \cdots + k_m} {k_1, k_2, \ldots, k_m}$ denotes a multinomial coefficient
:$\dbinom {k_1 + k_2} {k_1}$ etc. denotes binomial coefficients.

Proof:
The proof proceeds by induction.
For all $m \in \Z_{> 1}$, let $\map P m$ be the proposition:
:$\dbinom {k_1 + k_2 + \cdots + k_m} {k_1, k_2, \ldots, k_m} = \dbinom {k_1 + k_2} {k_1} \dbinom {k_1 + k_2 + k_3} {k_1 + k_2} \cdots \dbinom {k_1 + k_2 + \cdots + k_m} {k_1 + k_2 + \cdots + k_{m - 1} }$
Theorem: Equivalence of Definitions of Semantic Equivalence for Predicate Logic

Let $\mathbf A, \mathbf B$ be WFFs of predicate logic.
{{TFAE|def = Semantic Equivalence for Predicate Logic|view = semantic equivalence|context = Predicate Logic|contextview = predicate logic}}

Proof:
Let $\AA$ be a structure for predicate logic.
Let $\sigma$ be an assignment for $\mathbf A \iff \mathbf B$ in $\AA$.
Then the value of $\mathbf A \iff \mathbf B$ under $\sigma$ is given by:
:$\map {f^\leftrightarrow} {\map {\operatorname{val}_\AA} {\mathbf A} \sqbrk \sigma, \map {\operatorname{val}_\AA} {\mathbf B} \sqbrk \sigma}$
and from the definition of $f^\leftrightarrow$ we see that $\AA, \sigma \models_{\mathrm{PL_A}} \mathbf A \iff \mathbf B$ {{iff}}:
:$\map {\operatorname{val}_\AA} {\mathbf A} \sqbrk \sigma = \map {\operatorname{val}_\AA} {\mathbf B} \sqbrk \sigma$
Because the possible values are just $\T$ and $\F$, this is equivalent to:
:$\map {\operatorname{val}_\AA} {\mathbf A} \sqbrk \sigma = \T$ {{iff}} $\map {\operatorname{val}_\AA} {\mathbf B} \sqbrk \sigma = \T$
which by definition of $\mathrm{PL_A}$-model amounts to:
:$\AA, \sigma \models_{\mathrm{PL_A}} \mathbf A$ {{iff}} $\AA, \sigma \models_{\mathrm{PL_A}} \mathbf B$
Because $\AA$ and $\sigma$ were arbitrary, the above equivalence holds for all such $\AA$ and $\sigma$.
The result follows by definition of tautology.
{{qed}}
Category:Definitions/Semantic Equivalence for Predicate Logic
9oo5jchxrb5cw6dabko6qhcqff553fn
Theorem: Universal Closures are Semantically Equivalent

Let $\mathbf A$ be a WFF of predicate logic.
Let $\mathbf B, \mathbf B'$ be universal closures of $\mathbf A$.
Then $\mathbf B$ and $\mathbf B'$ are semantically equivalent.

Proof:
Let $\AA$ be a structure for predicate logic.
Let $\mathbf B$ be any universal closure of $\mathbf A$.
Then $\mathbf B$ is a sentence of the form:
:$\forall x_1: \cdots \forall x_n: \mathbf A$
By definition of the models relation:
:$\AA \models_{\mathrm{PL}} \mathbf B$ {{iff}} $\map {\operatorname{val}_\AA} {\mathbf B} = \T$ 
Hence, recursively applying the definition of $\map {\operatorname{val}_\AA} \cdot \sqbrk \sigma$, we see:
:$\map {\operatorname{val}_\AA} {\mathbf B} \sqbrk \O = \T$ {{iff}} $\forall a_1, \ldots, a_n \in A: \mathop{\map {\operatorname{val}_\AA} {\mathbf A} } \sqbrk {\dfrac{x_1} {a_1} + \ldots + \dfrac{x_n} {a_n} } = \T$
where $\dfrac{x_1} {a_1} + \ldots + \dfrac{x_n} {a_n}$ denotes the iterated extension of an assignment.
By Value of Formula under Assignment Determined by Free Variables:
$\map {\operatorname{val}_\AA} {\mathbf A} \sqbrk {\dfrac{x_1} {a_1} + \ldots + \dfrac{x_n} {a_n} }$ only depends on the $a_i$ for the free variables $x_i$ in $\mathbf A$.
Because we check all possible $a_i \in A$ and all free variables $x_i$ in $\mathbf A$ are quantified over in $\mathbf B$, it follows that:
:$\forall a_1, \ldots, a_n \in A: \map {\operatorname{val}_\AA} {\mathbf A} \sqbrk {\dfrac{x_1} {a_1} + \ldots + \dfrac{x_n} {a_n} } = \T$
{{iff}}:
:$\forall a_1, \ldots, a_k \in A: \map {\operatorname{val}_\AA} {\mathbf A} \sqbrk {\dfrac{x_1} {a_1} + \ldots + \dfrac{x_k} {a_k} } = \T$
where $x_1, \ldots, x_k$ are the free variables of $\mathbf A$.
But this last condition does not depend on $\mathbf B$ beyond that it be a universal closure.
Hence, for any two universal closures $\mathbf B, \mathbf B'$ of $\mathbf A$:
:$\AA \models_{\mathrm{PL}} \mathbf B$ {{iff}} $\AA \models_{\mathrm{PL}} \mathbf B$
The result follows by definition of semantic equivalence.
{{qed}}
Theorem: Meet-Continuous iff if Element Precedes Supremum of Directed Subset then Element equals Supremum of Meet of Element by Directed Subset

Let $L = \struct {S, \vee, \wedge, \preceq}$ be an up-complete lattice.
Then
:$L$ is meet-continuous
{{iff}}:
:$\forall x \in S$, the directed subset $D$ of $S: x \preceq \sup D \implies x = \sup \set {x \wedge d: d \in D}$

Proof:
=== Sufficient Condition ===
Let $L$ be meet-continuous.
Let $x$ be an element of $S$, $D$ be a directed subset of $S$ such that
:$x \preceq \sup D$
Thus
{{begin-eqn}}
{{eqn | l = x
      | r = x \wedge \sup D
      | c = Preceding iff Meet equals Less Operand
}}
{{eqn | r = \sup \set {x \wedge d: d \in D}
      | c = {{Defof|Meet-Continuous Lattice}}
}}
{{end-eqn}}
{{qed|lemma}}