avewright/proofwiki-math huggingface dataset:
Theorem: Constant to Power of Number of Distinct Prime Divisors is Multiplicative Function

Let $c \in \R$ be a constant.
Let $f: \N \to \R$ denotes the mapping defined as:
:$\forall n \in \N: \map f n = c^k$
where $k$ is number of distinct primes that divide $n$.
Then $f$ is multiplicative.

Proof:
Let $r, s \in \Z$ such that $r \perp s$.
Let $r$ be composed of $p$ distinct primes:
:$r_1, r_2, \ldots r_p$
Thus:
:$\map f r = c^p$
Let $s$ be composed of $q$ distinct primes:
:$s_1, s_2, \ldots s_q$
Thus:
:$\map f s = c^q$
As $r \perp s$, all the $r_k$ and $s_k$ are distinct.
Thus $r s$ is composed of:
:the $p$ distinct primes $r_1, r_2, \ldots r_p$
and:
:the $q$ distinct primes $s_1, s_2, \ldots s_q$
which is a total of $p + q$ distinct primes.
Thus:
{{begin-eqn}}
{{eqn | l = \map f {r s}
      | r = c^{p + q}
      | c = Definition of $f$
}}
{{eqn | r = c^p c^q
      | c = Product of Powers
}}
{{eqn | r = \map f r \map f s
      | c = from above
}}
{{end-eqn}}
Hence the result.
{{Qed}}
Theorem: Product of Multiplicative Functions is Multiplicative

Let $f: \N \to \C$ and $g: \N \to \C$ be multiplicative functions.
Then their pointwise product:
:$f \times g: \Z \to \Z: \forall s \in S: \map {\paren {f \times g} } s := \map f s \times \map g s$
is also multiplicative.

Proof:
Let $f$ and $g$ be multiplicative.
Let $m \perp n$.
Then:
{{begin-eqn}}
{{eqn | l = \map {f \times g} {m \times n}
      | r = \map f {m \times n} \times \map g {m \times n}
      | c = {{Defof|Pointwise Multiplication of Integer-Valued Functions}}
}}
{{eqn | r = \map f m \times \map f n \times \map g m \times \map g n
      | c = {{Defof|Multiplicative Arithmetic Function}}
}}
{{eqn | r = \map f m \times \map g m \times \map f n \times \map g n
      | c = Integer Multiplication is Commutative
}}
{{eqn | r = \paren {\map {f \times g} m} \times \paren {\map {f \times g} n}
      | c = {{Defof|Pointwise Multiplication of Integer-Valued Functions}}
}}
{{end-eqn}}
Hence the result by definition of multiplicative function.
{{qed}}
Theorem: Segment of Auxiliary Relation Mapping is Element of Increasing Mappings Satisfying Inclusion in Lower Closure

Let $R = \struct {S, \preceq}$ be an ordered set.
Let $\map {\mathit {Ids} } R$ be the set of all ideals in $R$.
Let $L = \struct {\map {\mathit {Ids} } R, \precsim}$ be an ordered set where $\precsim \mathop = \subseteq {\restriction_{\map {\mathit {Ids} } R \times \map {\mathit {Ids} } R} }$.
Let $r$ be an auxiliary relation on $S$.
Let $M = \struct {F, \preccurlyeq}$ be the ordered set of increasing mappings $g$ satisfying $\forall x \in S: \map g x \subseteq x^\preceq$.
Let $f: S \to \map {\mathit {Ids} } R$ be a mapping such that:
:$\forall x \in S: \map f x = x^r$
where $x^r$ denotes the $r$-segment of $x$.
Then:
:$(1): \quad f \in F$
Let $h: S \to \map {\mathit {Ids} } R: x \mapsto x^\preceq$
Then:
:$(2): \quad h \in F \land f \preccurlyeq h$
Let $k: S \to \map {\mathit {Ids} } R: x \mapsto \set \bot$
where $\bot$ denotes the smallest element in $L$.
Then:
:$(3): \quad k \in F$ and $k \preccurlyeq f$

Proof:
=== Condition $(1)$ ===
By Segment of Auxiliary Relation Mapping is Increasing:
:$f$ is an increasing mapping.
By Segment of Auxiliary Relation is Subset of Lower Closure:
:$\forall x \in S: x^r \subseteq x^\preceq$
By definition of $f$:
:$\forall x \in S: \map f x \subseteq x^\preceq$
Thus
:$f \in F$
{{qed|lemma}}
Theorem: Singleton of Bottom is Ideal

Let $\struct {S, \preceq}$ be a bounded below ordered set.
Then
:$\set \bot$ is an ideal in $\struct {S, \preceq}$
where $\bot$ denotes the smallest element in $S$.

Proof:
=== Non-empty ===
By definition of singleton:
:$\bot \in \set \bot$
By definition:
:$\set \bot$ is a non-empty set.
{{qed|lemma}}
Theorem: Number of Digits in Factorial

Let $n!$ denote the factorial of $n$.
The number of digits in $n!$ is approximately:
:$1 + \floor {\dfrac 1 2 \paren {\log_{10} 2 + \log_{10} \pi} + \dfrac 1 2 \log_{10} n + n \paren {\log_{10} n - \log_{10} e} }$
when $n!$ is shown in decimal notation.
This evaluates to:
:$1 + \floor {\paren {n + \dfrac 1 2} \log_{10} n - 0.43429 \ 4481 \, n + 0.39908 \ 9934}$

Proof:
From Stirling's Formula:
:$n! \sim \sqrt {2 \pi n} \paren {\dfrac n e}^n$
from which the result can be calculated.
To count the number of digits:
{{begin-eqn}}
{{eqn | l = \log_{10} n!
      | o = \sim
      | r = \log_{10} \paren {\sqrt {2 \pi n} \paren {\dfrac n e}^n}
      | c = Stirling's Formula
}}
{{eqn | r = \log_{10} \paren {\sqrt {2 \pi n} } + \log_{10} \paren {\paren {\dfrac n e}^n}
      | c = Sum of Logarithms
}}
{{eqn | r = \frac 1 2 \log_{10} 2 \pi n + n \log_{10} \paren {\dfrac n e}
      | c = Logarithm of Power
}}
{{eqn | r = \frac 1 2 \paren {\log_{10} 2 + \log_{10} \pi} + \frac 1 2 \log_{10} n + n \paren {\log_{10} n - \log_{10} e}
      | c = Sum of Logarithms, Difference of Logarithms
}}
{{end-eqn}}
We have:
:Common Logarithm of $2$: $\log_{10} 2 \approx 0.30102 \ 9996$
:Common Logarithm of $\pi$: $\log_{10} \pi \approx 0.49714 \ 9873$
:Common Logarithm of $e$: $\log_{10} e \approx 0.43429 \ 4481$
Hence:
{{begin-eqn}}
{{eqn | l = \log_{10} n!
      | o = \sim
      | r = \frac 1 2 \paren {0.30102 \ 9996 + 0.49714 \ 9873} + \frac 1 2 \log_{10} n + n \paren {\log_{10} n - 0.43429 \ 4481}
      | c = 
}}
{{eqn | r = \paren {n + \frac 1 2} \log_{10} n - 0.43429 \ 4481 \, n + 0.39908 \ 9934
      | c = 
}}
{{end-eqn}}
Hence the result from Number of Digits in Number.
{{qed}}
Category:Factorials
0zbi8a1z1m657d85coj0ordx7zugwqc
Theorem: Rising Factorial in terms of Falling Factorial

:$x^{\overline n} = \paren {x + n - 1}^{\underline n}$

Proof:
{{begin-eqn}}
{{eqn | l = x^{\overline n}
      | r = \prod_{j \mathop = 0}^{n - 1} \paren {x + j}
      | c = {{Defof|Rising Factorial}}
}}
{{eqn | r = x \paren {x + 1} \cdots \paren {x + n - 1}
      | c = {{Defof|Continued Product}}
}}
{{eqn | r = \paren {x + n - 1} \paren {x + n - 2} \cdots \paren {x + 1} x
      | c = reversing the order
}}
{{eqn | r = \prod_{j \mathop = 0}^{n - 1} \paren {\paren {x + n - 1} - j}
      | c = {{Defof|Falling Factorial}}
}}
{{eqn | r = \paren {x + n - 1}^{\underline n}
      | c = {{Defof|Continued Product}}
}}
{{end-eqn}}
{{qed}}
Theorem: Rising Factorial in terms of Falling Factorial of Negative

:$x^{\overline k} = \paren {-1}^k \paren {-x}^{\underline k}$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {-x}^{\underline k}
      | r = \prod_{j \mathop = 0}^{k - 1} \paren {-x - j}
      | c = {{Defof|Falling Factorial}}
}}
{{eqn | r = \prod_{j \mathop = 0}^{k - 1} \paren {-1} \paren {x + j}
      | c = 
}}
{{eqn | r = \prod_{j \mathop = 0}^{k - 1} \paren {-1} \prod_{j \mathop = 0}^{k - 1} \paren {x + j}
      | c = Product of Products
}}
{{eqn | r = \paren {-1}^k \prod_{j \mathop = 0}^{k - 1} \paren {x + j}
      | c = 
}}
{{eqn | r = \paren {-1}^k x^{\overline k}
      | c = {{Defof|Rising Factorial}}
}}
{{eqn | ll= \leadsto
      | l = \paren {-1}^k \paren {-x}^{\underline k}
      | r = \paren {-1}^{2 k} x^{\overline k}
      | c = multiplying both sides by $\paren {-1}^k$
}}
{{eqn | r = x^{\overline k}
      | c = $-1$ to an even power is $1$
}}
{{end-eqn}}
{{qed}}
Theorem: Falling Factorial as Quotient of Factorials

:$x^{\underline n} = \dfrac {x!} {\paren {x - n}!} = \dfrac {\map \Gamma {x + 1} } {\map \Gamma {x - n + 1} }$

Proof:
{{begin-eqn}}
{{eqn | l = x^{\underline n}
      | r = \prod_{j \mathop = 0}^{n - 1} \paren {x - j}
      | c = {{Defof|Falling Factorial}}
}}
{{eqn | r = x \paren {x - 1} \paren {x - 2} \dotsm \paren {x - n + 1}
      | c = 
}}
{{eqn | r = \dfrac {x!} {\paren {x - n}!}
      | c = {{Defof|Factorial}}
}}
{{eqn | r = \dfrac {\map \Gamma {x + 1} } {\map \Gamma {x - n + 1} }
      | c = {{Defof|Gamma Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: One to Integer Rising is Integer Factorial

:$1^{\overline n} = n!$

Proof:
{{begin-eqn}}
{{eqn | l = 1^{\overline n}
      | r = \dfrac {\paren {1 + n - 1}!} {\paren {1 - 1}!}
      | c = Rising Factorial as Quotient of Factorials
}}
{{eqn | r = \dfrac {n!} {0!}
      | c = 
}}
{{eqn | r = n!
      | c = Factorial of Zero
}}
{{end-eqn}}
{{qed}}
Category:Rising Factorials
Category:Factorials
4dcqx0irfqi9tnnvf7ysu9tdczqi1vu
Theorem: Number to Power of One Rising is Itself

:$x^{\overline 1} = x$

Proof:
{{begin-eqn}}
{{eqn | l = x^{\overline 1}
      | r = \dfrac {\map \Gamma {x + 1} } {\map \Gamma x}
      | c = Rising Factorial as Quotient of Factorials
}}
{{eqn | r = x
      | c = Gamma Difference Equation
}}
{{end-eqn}}
{{qed}}
Category:Rising Factorials
sa1f6ul61j0vgsfk8waanaiyu8o7pg1
Theorem: Integer to Power of Itself Falling is Factorial

:$n^{\underline n} = n!$

Proof:
{{begin-eqn}}
{{eqn | l = n^{\underline n}
      | r = \dfrac {n!} {\paren {n - n}!}
      | c = Falling Factorial as Quotient of Factorials
}}
{{eqn | r = \dfrac {n!} {0!}
      | c = 
}}
{{eqn | r = n!
      | c = Factorial of Zero
}}
{{end-eqn}}
{{qed}}
Category:Falling Factorials
opk3w0uaoprxmpgvd9rzvqako48cfx9
Theorem: Number to Power of One Falling is Itself

:$x^{\underline 1} = x$

Proof:
{{begin-eqn}}
{{eqn | l = x^{\underline 1}
      | r = \dfrac {\Gamma \left({x + 1}\right)} {\Gamma \left({x - 1 + 1}\right)}
      | c = Falling Factorial as Quotient of Factorials
}}
{{eqn | r = \dfrac {\Gamma \left({x + 1}\right)} {\Gamma \left({x}\right)}
      | c = 
}}
{{eqn | r = x
      | c = Gamma Difference Equation
}}
{{end-eqn}}
{{qed}}
Category:Falling Factorials
jjmyfhhwutxv5dyo2xhk3s6plb6w4nx
Theorem: Number of Permutations of One Less

:${}^{n - 1} P_n = {}^n P_n$
where ${}^k P_n$ denotes the number of ordered selections of $k$ objects from $n$.

Proof:
{{begin-eqn}}
{{eqn | l = {}^{n - 1} P_n
      | r = \dfrac {n!} {\paren {n - \paren {n - 1} }!}
      | c = Number of Permutations
}}
{{eqn | r = \dfrac {n!} {1!}
      | c = 
}}
{{eqn | r = n!
      | c = 
}}
{{eqn | r = {}^n P_n
      | c = Number of Permutations
}}
{{end-eqn}}
{{qed}}
Theorem: Number of Permutations of One Less

:${}^{n - 1} P_n = {}^n P_n$
where ${}^k P_n$ denotes the number of ordered selections of $k$ objects from $n$.

Proof:
{{begin-eqn}}
{{eqn | l = {}^{n - 1} P_n
      | r = n^{\underline {n - 1} }
      | c = Number of Permutations: $n^{\underline {n - 1} }$ denotes Falling Factorial
}}
{{eqn | r = n!
      | c = Integer to Power of Itself Less One Falling is Factorial
}}
{{eqn | r = {}^n P_n
      | c = Number of Permutations
}}
{{end-eqn}}
{{qed}}
Theorem: Binomial Coefficient with Two/Corollary

:$\forall n \in \N: \dbinom n 2 = T_{n - 1} = \dfrac {n \paren {n - 1} } 2$
where $T_n$ is the $n$th triangular number.

Proof:
From the definition of binomial coefficient:
:$\dbinom n 2 = \dfrac {n!} {2! \paren {n - 2}!}$
The result follows directly from the definition of the factorial:
:$2! = 1 \times 2$
{{qed}}
Theorem: Increasing Mappings Satisfying Inclusion in Lower Closure is Isomorphic to Auxiliary Relations

Let $R = \struct {S, \preceq}$ be a bounded below join semilattice.
Let $\map {\operatorname{Ids} } R$ be the set of all ideals in $R$.
Let $L = \struct {\map {\operatorname{Ids} } R, \precsim}$ be an ordered set where $\precsim \mathop = \subseteq\restriction_{\map {\operatorname{Ids} } R \times \map {\operatorname{Ids} } R}$.
Let $M = \struct {F, \preccurlyeq}$ be the ordered set of increasing mappings $g:S \to \map {\operatorname{Ids} } R$ satisfying $\forall x \in S: \map g x \subseteq x^\preceq$.
Let $\map {\operatorname{Aux} } R$ be the set of all auxiliary relations on $S$.
Let $P = \struct {\map {\operatorname{Aux} } R, \precsim'}$ be an ordered set where $\precsim' \mathop = \subseteq\restriction_{\map {\operatorname{Aux} } R \times \map {\operatorname{Aux} } R}$.
Then
:there exists an order isomorphism between $P$ and $M$

Proof:
By Segment of Auxiliary Relation Mapping is Element of Increasing Mappings Satisfying Inclusion in Lower Closure define $G: \map {\operatorname{Aux} } R \to F$:
:$\forall \RR \in \map {\operatorname{Aux} } R: \map G \RR = \paren {S \ni x \mapsto x^\RR}$
We will prove by Order Isomorphism is Surjective Order Embedding that:
:$G$ is an order isomorphism.
Theorem: Binomial Theorem/Abel's Generalisation

:$\ds \paren {x + y}^n = \sum_k \binom n k x \paren {x - k z}^{k - 1} \paren {y + k z}^{n - k}$

Proof:
By admitting $y = \paren {x + y} - x$, we have that:
:$\paren {x + y}^n = \paren {x + \paren {x + y} - x}^n$
Expanding the {{RHS}} in powers of $\paren {x + y}$:
{{begin-eqn}}
{{eqn | o = 
      | r = \sum_k \binom n k x \paren {x - k z}^{k - 1} \paren {y + k z}^{n - k}
      | c = 
}}
{{eqn | r = \sum_k \binom n k x \paren {x - k z}^{k - 1} \paren {x + \paren {x + y} + k z}^{n - k}
      | c = 
}}
{{eqn | r = \sum_k \binom n k x \paren {x - k z}^{k - 1} \sum_j \paren {x + y}^j \paren {-x + k z}^{n - k - j} \binom {n - k} j
      | c = 
}}
{{eqn | r = \sum_j \binom n j \paren {x + y})^j \sum_k \binom {n - j} {n - j - k} x \paren {x - k z}^{k - 1} \paren {-x + k z}^{n - k - j}
      | c = 
}}
{{eqn | r = \sum_{j \mathop \le n} \binom n j \paren {x + y}^j 0^{n - j}
      | c = Abel's Generalisation of Binomial Theorem: Special Case $x + y = 0$
}}
{{eqn | r = \paren {x + y}^n
      | c = Binomial Theorem
}}
{{end-eqn}}
{{qed}}
Theorem: Binomial Theorem/Abel's Generalisation

:$\ds \paren {x + y}^n = \sum_k \binom n k x \paren {x - k z}^{k - 1} \paren {y + k z}^{n - k}$

Proof:
From this formula:
:$(1): \quad \ds \sum_{k \mathop \in \Z} \binom n k x \paren {x + k z}^{k - 1} y \paren {y + \paren {n - k} z}^{n - k - 1} = \paren {x + y} \paren {x + y + n z}^{n - 1}$
The given formula:
:$\ds \paren {x + y}^n = \sum_k \binom n k x \paren {x - k z}^{k - 1} \paren {y + k z}^{n - k}$
can then be transformed into $(1)$ by
{{finish|somehow}}
Theorem: Binomial Theorem/Abel's Generalisation

:$\ds \paren {x + y}^n = \sum_k \binom n k x \paren {x - k z}^{k - 1} \paren {y + k z}^{n - k}$

Proof:
From Hurwitz's Generalisation of Binomial Theorem:
:$(1): \quad \paren {x + y}^n = \ds \sum x \paren {x + \epsilon_1 z_1 + \cdots + \epsilon_n z_n}^{\epsilon_1 + \cdots + \epsilon_n - 1} \paren {y - \epsilon_1 z_1 - \cdots - \epsilon_n z_n}^{n - \epsilon_1 - \cdots - \epsilon_n}$
Setting $z = z_1 = z_2 = \cdots z_n$ we have:
{{begin-eqn}}
{{eqn | o = 
      | r = \sum x \paren {x + \epsilon_1 z + \cdots + \epsilon_n z}^{\epsilon_1 + \cdots + \epsilon_n - 1} \paren {y - \epsilon_1 z - \cdots - \epsilon_n z}^{n - \epsilon_1 - \cdots - \epsilon_n}
      | c = 
}}
{{eqn | r = \sum \binom n k x \paren {x + k z}^{k - 1} \paren {y - k z}^{n - k}
      | c = where $\epsilon_1 + \cdots + \epsilon_n = k$
}}
{{eqn | r = \sum \binom n {n - k} x \paren {x + k z}^{k - 1} \paren {y - k z}^{n - k}
      | c = Symmetry Rule for Binomial Coefficients
}}
{{eqn | r = \sum \binom n k x \paren {x - k z}^{k - 1} \paren {y + k z}^{n - k}
      | c = 
}}
{{end-eqn}}
Hence the result.
Theorem: Sum over k of r Choose m+k by s Choose n+k

Let $s \in \R, r \in \Z_{\ge 0}, m, n \in \Z$.
Then:
:$\ds \sum_k \binom r {m + k} \binom s {n + k} = \binom {r + s} {r - m + n}$

Proof:
{{begin-eqn}}
{{eqn | l = \sum_k \binom r {m + k} \binom s {n + k}
      | r = \sum_k \binom r {r - m - k} \binom s {s - n - k}
      | c = Symmetry Rule for Binomial Coefficients
}}
{{eqn | r = \sum_k \binom r k \binom s {s - n - \left({r - m - k}\right)}
      | c = Change of Index Variable of Summation
}}
{{eqn | r = \sum_k \binom r k \binom s {r - m - k + n}
      | c = Symmetry Rule for Binomial Coefficients
}}
{{eqn | r = \sum_k \binom r k \binom s {\left({r - m + n}\right) - k}
      | c = 
}}
{{eqn | r = \binom {r + s} {r - m + n}
      | c = Chu-Vandermonde Identity
}}
{{end-eqn}}
{{qed}}
Theorem: Sum over k of r Choose k by s+k Choose n by -1^r-k

Let $s \in \R, r \in \Z_{\ge 0}, n \in \Z$.
Then:
:$\ds \sum_k \binom r k \binom {s + k} n \paren {-1}^{r - k} = \binom s {n - r}$

Proof:
The proof proceeds by induction on $r$.
For all $r \in \Z_{>0}$, let $\map P r$ be the proposition:
:$\ds \sum_k \binom r k \binom {s + k} n \paren {-1}^{r - k} = \binom s {n - r}$
=== Basis for the Induction ===
$\map P 0$ is the case:
{{begin-eqn}}
{{eqn | l = \sum_k \binom 0 k \binom {s + k} n \paren {-1}^{0 - k}
      | r = \delta_{0 k} \binom {s + k} n \paren {-1}^{0 - k}
      | c = Zero Choose n
}}
{{eqn | r = \binom s n
      | c = All terms vanish but for $k = 0$
}}
{{eqn | r = \binom s {n - 0}
      | c = 
}}
{{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 m$ is true, where $m \ge 0$, then it logically follows that $\map P {m + 1}$ is true.
This is the induction hypothesis:
:$\ds \sum_k \binom m k \binom {s + k} n \paren {-1}^{m - k} = \binom s {n - m}$
from which it is to be shown that:
:$\ds \sum_k \binom {m + 1} k \binom {s + k} n \paren {-1}^{m + 1 - k} = \binom s {n - \paren {m + 1} }$
=== Induction Step ===
This is the induction step:
{{begin-eqn}}
{{eqn | o = 
      | r = \sum_k \binom {m + 1} k \binom {s + k} n \paren {-1}^{m + 1 - k}
      | c = 
}}
{{eqn | r = \sum_k \paren {\binom m k + \binom m {k - 1} } \binom {s + k} n \paren {-1}^{m + 1 - k}
      | c = Pascal's Rule
}}
{{eqn | r = \sum_k \binom m k \binom {s + k} n \paren {-1}^{m + 1 - k} + \sum_k \binom m {k - 1} \binom {s + k} n \paren {-1}^{m + 1 - k}
      | c = 
}}
{{eqn | r = -\sum_k \binom m k \binom {s + k} n \paren {-1}^{m - k} + \sum_k \binom m {k - 1} \binom {s + k} n \paren {-1}^{m + 1 - k}
      | c = 
}}
{{eqn | r = -\binom s {n - m} + \sum_k \binom m {k - 1} \binom {s + k} n \paren {-1}^{m + 1 - k} 
      | c = Induction Hypothesis
}}
{{eqn | r = -\binom s {n - m} + \sum_k \binom m {k - 1} \paren {\binom {s + k - 1} n + \binom {s + k - 1} {n - 1} } \paren {-1}^{m + 1 - k}
      | c = Pascal's Rule
}}
{{eqn | r = -\binom s {n - m} + \sum_k \binom m {k - 1} \binom {s + k - 1} n \paren {-1}^{m - \paren {k - 1} }
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \sum_k \binom m {k - 1} \binom {s + k - 1} {n - 1} \paren {-1}^{m - \paren {k - 1} }
      | c = 
}}
{{eqn | r = -\binom s {n - m} + \sum_k \binom m k \binom {s + k} n \paren {-1}^{m - k} + \sum_k \binom m k \binom {s + k} {n - 1} \paren {-1}^{m - k}
      | c = Translation of Index Variable of Summation
}}
{{eqn | r = -\binom s {n - m} + \binom s {n - m} + \binom s {n - 1 - m}
      | c = Induction Hypothesis
}}
{{eqn | r = \binom s {n - \paren {m + 1} }
      | c = simplifying
}}
{{end-eqn}}
So $\map P m \implies \map P {m + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\ds \sum_k \binom r k \binom {s + k} n \paren {-1}^{r - k} = \binom s {n - r}$
for all $s \in \R, r \in \Z_{\ge 0}, n \in \Z$.
{{qed}}
Theorem: Sum over k of r-k Choose m by s+k Choose n

Let $m, n, r, s \in \Z_{\ge 0}$ such that $n \ge s$.
Then:
:$\ds \sum_{k \mathop = 0}^r \binom {r - k} m \binom {s + k} n = \binom {r + s + 1} {m + n + 1}$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = \sum_{k \mathop = 0}^r \binom {r - k} m \binom {s + k} n
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 0}^r \binom {-\left({m + 1}\right)} {r - k - m} \binom {-\left({n + 1}\right)} {s + k - m} \left({-1}\right)^{r - m + s - m}
      | c = Moving Top Index to Bottom in Binomial Coefficient
}}
{{eqn | r = \binom {-\left({m + 1}\right) - \left({n + 1}\right)} {r - m + s - m} \left({-1}\right)^{r - m + s - m}
      | c = Chu-Vandermonde Identity
}}
{{eqn | r = \binom {r + s + 1} {m + n + 1}
      | c = Moving Top Index to Bottom in Binomial Coefficient
}}
{{end-eqn}}
{{qed}}
Theorem: Sum over k of r-tk Choose k by s-t(n-k) Choose n-k by r over r-tk

Let $r, s, t \in \R, n \in \Z$.
Then:
:$\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$

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$
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}$
:for $x \ne n t$
:$z = x^{t + 1} - x^t$.
From Sum over $k$ of $\dbinom {r - k t} k$ by $z^k$:
:$\ds \sum_k \dbinom {r - t k} k z^k = \frac {x^{r + 1} } {\paren {t + 1} x - t}$
Thus:
{{begin-eqn}}
{{eqn | l = \sum_k \map {A_k} {r, t} z^k \sum_k \dbinom {s - t k} k z^k
      | r = \frac {x^r x^{s + 1} } {\paren {t + 1} x - t}
      | c = 
}}
{{eqn | r = \frac {x^{\paren {r + s} + 1} } {\paren {t + 1} x - t}
      | c = 
}}
{{eqn | r = \sum_k \dbinom {r + s - t k} k z^k
      | c = 
}}
{{end-eqn}}
Equating coefficients of $z$:
{{begin-eqn}}
{{eqn | l = \sum_k \map {A_k} {r, t} z^k \sum_k \dbinom {s - \paren {n - k} t} k z^{n - k}
      | r = \binom {r + s - n t} n z^n
      | c = 
}}
{{eqn | l = \sum_k \dbinom {r - k t} k \dfrac r {r - k t} z^k \dbinom {s - \paren {n - k} t} k z^{n - k}
      | r = \binom {r + s - n t} n z^n
      | c = 
}}
{{eqn | l = \sum_k \dbinom {r - k t} k \dbinom {s - \paren {n - k} t} k \dfrac r {r - k t}
      | r = \binom {r + s - t n} n
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sum over k of r Choose k by s Choose k by k

:$\ds \sum_k \binom r k \binom s k k = \binom {r + s - 1} {r - 1} s$

Proof:
{{begin-eqn}}
{{eqn | l = \sum_k \binom r k \binom s k k
      | r = \sum_k \binom r k \binom {s - 1} {k - 1} s
      | c = Factors of Binomial Coefficient
}}
{{eqn | r = s \sum_k \binom r k \binom {s - 1} {k - 1}
      | c = as $s$ is constant
}}
{{eqn | r = s \binom {r + s - 1} {r - 1}
      | c = Sum over $k$ of $\dbinom r {m + k} \dbinom s {n + k}$: $s \gets s - 1$, $m \gets 0$, $n \gets -1$
}}
{{end-eqn}}
{{qed}}
Theorem: Relation Segment is Increasing

Let $S$ be a set.
Let $\RR, \QQ$ be relations on $S$ such that
:$\RR \subseteq \QQ$
Let $x \in S$.
Then
:$x^\RR \subseteq x^\QQ$
where $x^\RR$ denotes the $\RR$-segment of $x$.

Proof:
Let $y \in x^\RR$.
By definition of $\RR$-segment:
:$\tuple {y, x} \in \RR$
By definition of subset:
:$\tuple {y, x} \in \QQ$
Thus by definition of $\QQ$-segment:
:$y \in x^\QQ$
{{qed}}
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 \mathop \ge 0} \binom {n + k} n \binom {n + 1} {k + 1} \left({-1}\right)^k
      | c = Symmetry Rule for Binomial Coefficients and rearranging
}}
{{eqn | r = -\frac 1 {n + 1} \sum_{k \mathop \ge 1} \binom {n - 1 + k} n \binom {n + 1} k \left({-1}\right)^k
      | c = Translation of Index Variable of Summation
}}
{{eqn | r = -\frac 1 {n + 1} \sum_{k \mathop \ge 0} \binom {n - 1 + k} n \binom {n + 1} k \left({-1}\right)^k + \frac 1 {n + 1} \binom {n - 1} n
      | c = separating out the case where $k = 0$
}}
{{eqn | r = -\frac 1 {n + 1} \left({-1}\right)^{n + 1} \binom {n - 1} {-1} + \frac 1 {n + 1} \binom {n - 1} n
      | c = Sum over $k$ of $\dbinom r k \dbinom {s + k} n (-1)^{r - k}$
}}
{{eqn | r = \frac 1 {n + 1} \binom {n - 1} n
      | c = as $\dbinom {n - 1} {-1} = 0$
}}
{{eqn | r = \left[{n = 0}\right]
      | c = as $\dbinom {n - 1} n = 1 \iff n = 0$
}}
{{end-eqn}}
{{qed}}