avewright/proofwiki-math huggingface dataset:
Theorem: Signed Stirling Number of the First Kind of n+1 with 0

:$\map s {n + 1, 0} = 0$

Proof:
By definition of signed Stirling number of the first kind:
:$\map s {n, k} = \delta_{n k}$
where $\delta_{n k}$ is the Kronecker delta.
Thus
{{begin-eqn}}
{{eqn | l = n
      | o = \ge
      | r = 0
      | c = by hypothesis
}}
{{eqn | ll= \leadsto
      | l = n + 1
      | o = >
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = n + 1
      | o = \ne
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \delta_{\paren {n + 1} 0}
      | r = 0
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Unsigned Stirling Number of the First Kind of n+1 with 1

:$\ds {n + 1 \brack 1} = n!$

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\ds {n + 1 \brack 1} = n!$
Theorem: Stirling Number of the Second Kind of n+1 with 1

:$\ds {n + 1 \brace 1} = 1$

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\ds {n + 1 \brace 1} = 1$
Theorem: Signed Stirling Number of the First Kind of n+1 with 1

:$\map s {n + 1, 1} = \paren {-1}^n n!$

Proof:
By Relation between Signed and Unsigned Stirling Numbers of the First Kind:
:$\ds {n + 1 \brack 1} = \paren {-1}^{n + 1 + 1} \map s {n + 1, 1}$
where $\ds {n + 1 \brack 1}$ denotes an unsigned Stirling number of the first kind.
We have that:
:$\paren {-1}^{n + 1 + 1} = \paren {-1}^n$
and so:
:$\ds {n + 1 \brack 1} = \paren {-1}^n \map s {n + 1, 1}$
The result follows from Unsigned Stirling Number of the First Kind of Number with Self.
{{qed}}
Theorem: Stirling Number of the Second Kind of n+1 with 2

:$\ds {n + 1 \brace 2} = 2^n - 1$

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\ds {n + 1 \brace 2} = 2^n - 1$
Theorem: Sum over k of Unsigned Stirling Numbers of the First Kind of n with k by k choose m

Let $m, n \in \Z_{\ge 0}$.
:$\ds \sum_k {n \brack k} \binom k m = {n + 1 \brack m + 1}$
where:
:$\ds {n \brack k}$ denotes an unsigned Stirling number of the first kind
:$\dbinom k m$ denotes a binomial coefficient.

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\ds \forall m \in \Z_{\ge 0}: \sum_k {n \brack k} \binom k m = {n + 1 \brack m + 1}$
Theorem: Semantically Equivalent Terms are Equal

Let $\tau_1, \tau_2$ be terms.
Suppose that they are semantically equivalent with respect to the empty set.
Then $\tau_1 = \tau_2$.

Proof:
{{proof wanted|While an exercise, this basically requires construction of the syntactic model in order to achieve full rigour}}
Theorem: Down Mapping is Generated by Approximating Relation

Let $L = \struct {S, \wedge, \preceq}$ be a bounded below meet-continuous meet semilattice.
Let $\map {\operatorname{Ids} } L$ be the set of all ideals in $L$.
Let $I$ be an ideal in $L$.
Let $f: S \to \map {\operatorname{Ids} } L$ be a mapping such that:
:$\forall x \in S: x \preceq \sup I \implies \map f x = \set {x \wedge i: i \in I}$
and
:$\forall x \in S: x \npreceq \sup I \implies \map f x = x^\preceq$
where $x^\preceq$ denotes the lower closure of $x$.
Then
:there exists an auxiliary approximating relation $\RR$ on $S$ such that
::$\forall s \in S: \map f s = s^\RR$
where $s^\RR$ denotes the $\RR$-segment of $s$.

Proof:
Define relation $\RR$ on $S$:
:$\forall x, y \in S: \tuple {x, y} \in \RR \iff x \in \map f y$
By definition of $\RR$-segment:
:$\forall x \in S: \map f x = x^\RR$
We will prove that:
:$\RR$ is an approximating relation.
Let $x \in S$.
Suppose the case holds that:
:$x \preceq \sup I$
Thus:
{{begin-eqn}}
{{eqn | l = \map \sup {x^\RR}
      | r = \sup \map f x
}}
{{eqn | r = \sup \set {x \wedge d: d \in I}
      | c = Definition of $f$
}}
{{eqn | r = x \wedge \sup I
      | c = {{Defof|Meet-Continuous Lattice}}
}}
{{eqn | r = x
      | c = Preceding iff Meet equals Less Operand
}}
{{end-eqn}}
Suppose the case holds that
:$x \npreceq \sup I$
Thus
{{begin-eqn}}
{{eqn | l = \map \sup {x^\RR}
      | r = \sup \map f x
}}
{{eqn | r = \map \sup {x^\preceq}
      | c = Definition of $f$
}}
{{eqn | r = x
      | c = Supremum of Lower Closure of Element
}}
{{end-eqn}}
{{qed}}
Theorem: Preceding is Approximating Relation

Let $\struct {S, \preceq}$ be an ordered set.
Then $\preceq$ is an approximating relation on $S$.

Proof:
Let $x \in S$.
Define $\RR := \mathord\preceq$.
By definitions of lower closure of element and $\RR$-segment:
:$x^\preceq = x^\RR$
where:
:$x^\preceq$ denotes the lower closure of $x$
:$x^\RR$ denotes the $\RR$-segment of $x$
Thus by Supremum of Lower Closure of Element:
:$x = \map \sup {x^\preceq} = \map \sup {x^\RR}$
Hence $\preceq$ is an approximating relation on $S$.
{{qed}}
Theorem: Substitution Instance of Term is Term

Let $\beta, \tau$ be terms of predicate logic.
Let $x \in \operatorname {VAR}$ be a variable.
Let $\map \beta {x \gets \tau}$ be the substitution instance of $\beta$ substituting $\tau$ for $x$.
Then $\map \beta {x \gets \tau}$ is a term.

Proof:
Proceed by the Principle of Structural Induction on the definition of term, applied to $\beta$.
If $\beta = y$ for some variable $y$, then:
:$\map \beta {x \gets \tau} = \begin{cases} \tau & : \text {if $y = x$} \\ y &: \text {otherwise} \end{cases}$
In either case, $\map \beta {x \gets \tau}$ is a term.
If $\beta = \map f {\tau_1, \ldots, \tau_n}$ and the induction hypothesis holds for $\tau_1, \ldots, \tau_n$, then:
:$\map \beta {x \gets \tau} = \map f {\map {\tau_1} {x \gets \tau}, \ldots, \map {\tau_n} {x \gets \tau} }$
By the induction hypothesis, each $\map {\tau_i} {x \gets \tau}$ is a term.
Hence so is $\map \beta {x \gets \tau}$.
The result follows by the Principle of Structural Induction.
{{qed}}
Theorem: Substitution Instance of WFF is WFF

Let $\mathbf A$ be a WFF of predicate logic.
Let $\tau$ be a term of predicate logic.
Let $x \in \mathrm{VAR}$ be a variable.
Let $\mathbf A \left({x \gets \tau}\right)$ be the substitution instance of $\mathbf A$ substituting $\tau$ for $x$.
Then $\mathbf A \left({x \gets \tau}\right)$ is a WFF.

Proof:
Proceed by the Principle of Structural Induction on the bottom-up specification of predicate logic, applied to $\mathbf A$.
If $\mathbf A = p \left({\tau_1, \ldots, \tau_n}\right)$, then:
:$\mathbf A \left({x \gets \tau}\right) = p \left({\tau_1 \left({x \gets \tau}\right), \ldots, \tau_n \left({x \gets \tau}\right)}\right)$
where $\tau_i \left({x \gets \tau}\right)$ is the substitution instance of $\tau_i$.
By Substitution Instance of Term is Term, each such $\tau_i \left({x \gets \tau}\right)$ is again a term.
It follows that $\mathbf A \left({x \gets \tau}\right)$ is again a WFF.
If $\mathbf A = \neg \mathbf B$ and the induction hypothesis applies to $\mathbf B$, then:
:$\mathbf A \left({x \gets \tau}\right) = \neg \mathbf B \left({x \gets \tau}\right)$
and it follows from the induction hypothesis that $\mathbf A \left({x \gets \tau}\right)$ is a WFF of predicate logic.
If $\mathbf A = \mathbf B \circ \mathbf B'$ for $\circ$ one of $\land, \lor, \implies, \iff$ and the induction hypothesis applies to $\mathbf B, \mathbf B'$:
:$\mathbf A \left({x \gets \tau}\right) = \mathbf B \left({x \gets \tau}\right) \circ \mathbf B' \left({x \gets \tau}\right)$
and it follows from the induction hypothesis that $\mathbf A \left({x \gets \tau}\right)$ is a WFF of predicate logic.
If $\mathbf A = \exists x: \mathbf B$, and the induction hypothesis applies to $\mathbf B$:
:$\mathbf A \left({x \gets \tau}\right) = \exists x: \mathbf B \left({x \gets \tau}\right)$
and it follows from the induction hypothesis that $\mathbf A \left({x \gets \tau}\right)$ is a WFF of predicate logic.
If $\mathbf A = \forall x : \mathbf B$, and the induction hypothesis applies to $\mathbf B$:
:$\mathbf A \left({x \gets \tau}\right) = \forall x: \mathbf B \left({x \gets \tau}\right)$
and it follows from the induction hypothesis that $\mathbf A \left({x \gets \tau}\right)$ is a WFF of predicate logic.
The result follows by the Principle of Structural Induction.
{{qed}}
Theorem: Sum over k of Unsigned Stirling Numbers of the First Kind of n+1 with k+1 by k choose m by -1^k-m

Let $m, n \in \Z_{\ge 0}$.
:$\ds \sum_k {n + 1 \brack k + 1} \binom k m \paren {-1}^{k - m} = {n \brack m}$
where:
:$\ds {n + 1 \brack k + 1}$ etc. denotes an unsigned Stirling number of the first kind
:$\dbinom k m$ denotes a binomial coefficient.

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\ds \forall m \in \Z_{\ge 0}: \sum_k {n + 1 \brack k + 1} \binom k m \paren {-1}^{k - m} = {n \brack m}$
Theorem: Sum over k of Stirling Numbers of the Second Kind of k with m by n choose k

Let $m, n \in \Z_{\ge 0}$.
:$\ds \sum_k {k \brace m} \binom n k = {n + 1 \brace m + 1}$
where:
:$\ds {k \brace m}$ denotes a Stirling number of the second kind
:$\dbinom n k$ denotes a binomial coefficient.

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\ds \forall m \in \Z_{\ge 0}: \sum_k {k \brace m} \binom n k = {n + 1 \brace m + 1}$
Theorem: Sum over k of Stirling Numbers of the Second Kind of k+1 with m+1 by n choose k by -1^k-m

Let $m, n \in \Z_{\ge 0}$.
:$\ds \sum_k {k + 1 \brace m + 1} \binom n k \paren {-1}^{n - k} = {n \brace m}$
where:
:$\ds {k + 1 \brace m + 1}$ and so on denotes a Stirling number of the second kind
:$\dbinom n k$ denotes a binomial coefficient.

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\ds \forall m \in \Z_{\ge 0}: \sum_k {k + 1 \brace m + 1} \binom n k \paren {-1}^{n - k} = {n \brace m}$
Theorem: Universal Instantiation/Informal Statement

Suppose we have a universal statement:
:$\forall x: \map P x$
where $\forall$ is the universal quantifier and $\map P x$ is a propositional function.
Then we can deduce:
:$\map P {\mathbf a}$
where $\mathbf a$ is any arbitrary object we care to choose in the universe of discourse.
In natural language:
:''Suppose $P$ is true of everything in the universe of discourse.''
:''Let $\mathbf a$ be an element of the universe of discourse.''
:''Then $P$ is true of $\mathbf a$.''

Proof:
In the language of symbolic logic:
{{begin-eqn}}
{{eqn | q = \forall x
      | l = \map P x
      | o =
}}
{{eqn | ll= \therefore
      | l = \map P {\mathbf a}
      | o =
}}
{{end-eqn}}
{{qed}}
Theorem: Universal Instantiation/Model

Let $\map {\mathbf A} x$ be a WFF of predicate logic.
Let $\tau$ be a term which is freely substitutable for $x$ in $\mathbf A$.
Then $\forall x: \map {\mathbf A} x \implies \map {\mathbf A} \tau$ is a tautology.

Proof:
Let $\AA$ be a structure on a set $A$, and let $\sigma$ be an assignment for $\forall x: \map {\mathbf A} x \implies \map {\mathbf A} \tau$.
Define:
:$a_\tau := \mathop {\map {\operatorname{val}_\AA} \tau} \sqbrk \sigma$
the value of $\tau$ under $\sigma$.
From the definition of value under $\sigma$:
:$\map {\mathrm {val}_\AA} {\forall x: \map {\mathbf A} x \implies \map {\mathbf A} \tau} \sqbrk \sigma = \map {f^\to} {\map {\mathrm {val}_\AA} {\forall x: \map {\mathbf A} x} \sqbrk \sigma, \map {\mathrm {val}_\AA} {\map {\mathbf A} \tau} \sqbrk \sigma}$
where $f^\to$ is the truth function of $\implies$.
We thus need to ascertain that if:
:$\map {\mathrm {val}_\AA} {\forall x: \map {\mathbf A} x} \sqbrk \sigma = T$
then also:
:$\map {\mathrm {val}_\AA} {\map {\mathbf A} \tau} \sqbrk \sigma = T$
By definition of value under $\sigma$, the former amounts to:
:$\map {\mathrm {val}_\AA} {\map {\mathbf A} x} \sqbrk {\sigma + \paren {x / a} } = T$
for all $a \in A$.
By the Substitution Theorem for Well-Formed Formulas:
:$\map {\mathrm {val}_\AA} {\map {\mathbf A} \tau} \sqbrk \sigma = \map {\mathrm {val}_\AA} {\mathbf A} \sqbrk {\sigma + \paren {x / a_\tau} }$
Since $a_\tau \in A$, the conclusion follows, and $\forall x: \map {\mathbf A} x \implies \map {\mathbf A} \tau$ is a tautology.
{{qed}}
Theorem: Existential Generalisation/Model

Let $\map {\mathbf A} x$ be a WFF of predicate logic.
Let $\tau$ be a term which is freely substitutable for $x$ in $\mathbf A$.
Then $\map {\mathbf A} \tau \implies \exists x: \map {\mathbf A} x$ is a tautology.

Proof:
Let $\AA$ be a structure on a set $A$, and let $\sigma$ be an assignment for $\forall x: \map {\mathbf A} x \implies \map {\mathbf A} \tau$.
Define:
:$a_\tau := \map {\operatorname{val}_\AA} \tau \sqbrk \sigma$
the value of $\tau$ under $\sigma$.
From the definition of value under $\sigma$:
:$\map {\operatorname{val}_\AA} {\forall x: \map {\mathbf A} x \implies \map {\mathbf A} \tau} \sqbrk \sigma = \map {f^\to} {\map {\operatorname{val}_\AA} {\forall x: \map {\mathbf A} x} \sqbrk \sigma, \map {\operatorname{val}_\AA} {\map {\mathbf A} \tau} \sqbrk \sigma}$
where $f^\to$ is the truth function of $\implies$.
We thus need to ascertain that if:
:$\map {\operatorname{val}_\AA} {\map {\mathbf A} \tau} \sqbrk \sigma = \T$
then also:
:$\map {\operatorname{val}_\AA} {\exists x: \map {\mathbf A} x} \sqbrk \sigma = \T$
By the Substitution Theorem for Well-Formed Formulas, the former amounts to:
:$\map {\operatorname{val}_\AA} {\map {\mathbf A} x} \sqbrk {\sigma + \paren {x / a_\tau} } = \T$
By the definition of value under $\sigma$, the latter reduces to:
:$\map {\operatorname{val}_\AA} {\map {\mathbf A} x} \sqbrk {\sigma + \paren {x / a} } = \T$
for some $a \in A$.
Since $a_\tau \in A$, the conclusion follows, and $\map {\mathbf A} \tau \implies \exists x: \map {\mathbf A} x$ is a tautology.
{{qed}}
Theorem: Way Below is Approximating Relation

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below continuous lattice.
Then $\ll$ is an approximating relation on $S$.

Proof:
Let $x \in S$.
Define $\RR := \mathord \ll$.
By definitions of way below closure and $\RR$-segment:
:$x^\ll = x^\RR$
where:
:$x^\ll$ denotes the way below closure of $x$
:$x^\RR$ denotes the $\RR$-segment of $x$
By definition of continuous:
:$L$ satisfies the axiom of approximation.
Thus by the axiom of approximation:
:$x = \map \sup {x^\ll} = \map \sup {x^\RR}$
Hence $\ll$ is an approximating relation on $S$.
{{qed}}
Theorem: Intersection of Relation Segments of Approximating Relations equals Way Below Closure

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below meet-continuous lattice.
Let $\map {\operatorname {App} } L$ be the set of all auxiliary approximating relations on $S$.
Let $x \in S$.
Then
:$\ds \bigcap \set {x^\RR: \RR \in \map {\operatorname {App} } L} = x^\ll$

Proof:
By Intersection of Ideals with Suprema Succeed Element equals Way Below Closure of Element:
:$\ds \bigcap \set {I \in \operatorname {Ids}: x \preceq \sup I} = x^\ll$
where $\operatorname {Ids}$ denotes the set of all ideals in $L$.
For all $I \in \operatorname {Ids}$ define a mapping $m_I: S \to \operatorname {Ids}$:
:$\forall x \in S: x \preceq \sup I \implies \map {m_I} x = \set {x \wedge i: i \in I}$
and
:$\forall x \in S: x \npreceq \sup I \implies \map {m_I} x = x^\preceq$
By Intersection of Applications of Down Mappings at Element equals Way Below Closure of Element:
:$\ds \forall x \in S: \bigcap \set {\map {m_I} x: I \in \operatorname {Ids} } = x^\ll$
We will prove that
:$\set {\map {m_I} x: I \in \operatorname {Ids} } \subseteq \set {x^{\RR}: \RR \in \map {\operatorname {App} } L}$
Let $a \in \set {\map {m_I} x: I \in \operatorname {Ids} }$
Then
:$\exists I \in \operatorname {Ids}: a = \map {m_I} x$
By Down Mapping is Generated by Approximating Relation:
:$\exists \RR \in \map {\operatorname {App} } L: \forall s \in S: \map {m_I} s = s^\RR$
Then
:$a = x^\RR$
Thus
:$a \in \set {x^\RR: \RR \in \map {\operatorname {App} } L}$
{{qed|lemma}}
By Intersection of Family is Subset of Intersection of Subset of Family:
:$\ds \bigcap \set {x^\RR: \RR \in \map {\operatorname {App} } L} \subseteq x^\ll$
We will prove that
:$\set {x^\RR: \RR R \in \map {\operatorname {App} } L} \subseteq \set {I \in \operatorname {Ids}: x \preceq \sup I}$
Let $a \in \set {x^\RR: \RR \in \map {\operatorname {App} } L}$
Then
:$\exists \RR \in \map {\operatorname {App} } L: a = x^\RR$
By definition of approximating relation:
:$x = \sup a$
By Relation Segment of Auxiliary Relation is Ideal:
:$a \in \operatorname {Ids}$
Thus by definition of reflexivity:
:$a \in \set {I \in \operatorname {Ids}: x \preceq \sup I}$
{{qed|lemma}}
By Intersection of Family is Subset of Intersection of Subset of Family:
:$\ds x^\ll \subseteq \bigcap \set {x^\RR: \RR \in \map {\operatorname {App} } L}$
Hence the result by definition of set equality.
{{qed}}
Theorem: Convergent Sequence in Set of Integers/Corollary

Let $\sequence {x_n}_{n \mathop \in \N}$ be a sequence of distinct terms in the set $\Z$.
Then $\sequence {x_n}_{n \mathop \in \N}$ is not convergent.

Proof:
By Convergent Sequence in Set of Integers, $\sequence {x_n}_{n \mathop \in \N}$ is convergent {{iff}}:
:$\exists k \in \N: \forall m \in \N: m > k: x_m = x_k$
But since $\sequence {x_n}_{n \mathop \in \N}$ is a sequence of distinct terms, for all $k \ne m$, one has $x_m \ne x_k$.
The result follows.
{{qed}}
Category:Sequences
Category:Convergence
mwt8nkjgvrdp4oaxe5stysgw81lc9sc
Theorem: Limit of Monotone Real Function/Increasing

Let $f$ be a real function which is increasing and bounded above on the open interval $\openint a b$.
Let the supremum of $f$ on $\openint a b$ be $L$.
Then:
:$\ds \lim_{x \mathop \to b^-} \map f x = L$
where $\ds \lim_{x \mathop \to b^-} \map f x$ is the limit of $f$ from the left at $b$.

Proof:
Let $\epsilon > 0$.
We have to find a value of $\delta > 0$ such that $\forall x: b - \delta < x < b: \size {\map f x - L} < \epsilon$.
That is, that $L - \epsilon < \map f x < L + \epsilon$.
As $L$ is an upper bound for $f$ on $\openint a b$, $\map f x < L + \epsilon$ automatically happens.
Since $L - \epsilon$ is ''not'' an upper bound for $f$ on $\openint a b$, it follows that:
:$\exists y \in \openint a b: \map f y > L - \epsilon$
But $f$ increases on $\openint a b$.
So:
:$\forall x: y < x < b: L - \epsilon < \map f y \le \map f x$
We choose $\delta = b - y$ and hence the result.
{{qed}}
Theorem: Limit of Monotone Real Function/Decreasing

Let $f$ be a real function which is decreasing and bounded below on the open interval $\openint a b$.
Let the infimum of $f$ on $\openint a b$ be $l$.
Then:
:$\ds \lim_{x \mathop \to b^-} \map f x = l$
where $\ds \lim_{x \mathop \to b^-} \map f x$ is the limit of $f$ from the left at $b$.

Proof:
Let $\epsilon > 0$.
We have to find a value of $\delta > 0$ such that:
:$\forall x: b - \delta < x < b: \size {\map f x - l} < \epsilon$
That is:
:$l - \epsilon < \map f x < l + \epsilon$
As $l$ is a lower bound for $f$ on $\openint a b$:
:$l - \epsilon < \map f x$
automatically happens
Because $l + \epsilon$ is ''not'' a lower bound for $f$ on $\openint a b$:
:$\exists y \in \openint a b: \map f y < l + \epsilon$
But $f$ decreases on $\openint a b$.
So:
:$\forall x: y < x < b: \map f x \le \map f y < l + \epsilon$
We choose $\delta = y - a$ and hence the result.
{{qed}}
Theorem: Sum over k of m choose k by -1^m-k by k to the n

Let $m, n \in \Z_{\ge 0}$.
:$\ds \sum_k \binom m k \paren {-1}^{m - k} k^n = m! {n \brace m}$
where:
:$\dbinom m k$ denotes a binomial coefficient
:$\ds {n \brace m}$ etc. denotes a Stirling number of the second kind
:$m!$ denotes a factorial.

Proof:
The proof proceeds by induction on $m$.
For all $m \in \Z_{\ge 0}$, let $\map P m$ be the proposition:
:$\ds \forall n \in \Z_{\ge 0}: \sum_k \binom m k \paren {-1}^{m - k} k^n = m! {n \brace m}$
Theorem: Sum over k of m-n choose m+k by m+n choose n+k by Stirling Number of the Second Kind of m+k with k

Let $m, n \in \Z_{\ge 0}$.
:$\ds \sum_k \binom {m - n} {m + k} \binom {m + n} {n + k} {m + k \brace k} = {n \brack n - m}$
where:
:$\dbinom {m - n} {m + k}$ etc. denote binomial coefficients
:$\ds {m + k \brace k}$ denotes a Stirling number of the second kind
:$\ds {n \brack n - m}$ denotes an unsigned Stirling number of the first kind.

Proof:
The proof proceeds by induction on $m$.
For all $m \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\ds \forall n \in \Z_{\ge 0}: \sum_k \binom {m - n} {m + k} \binom {m + n} {n + k} {m + k \brace k} = {n \brack n - m}$
$\map P 0$ is the case:
{{begin-eqn}}
{{eqn | r = \sum_k \binom {0 - n} {0 + k} \binom {0 + n} {n + k} {0 + k \brace k}
      | o = 
      | c = 
}}
{{eqn | r = \sum_k \binom {- n} k \binom n {n + k}
      | c = Stirling Number of the Second Kind of Number with Self
}}
{{eqn | r = \sum_k \binom {- n} k \delta_{0 k}
      | c = as $\dbinom n {n + k} = 0$ for $k = 0$, and Binomial Coefficient with Self
}}
{{eqn | r = \binom {- n} 0
      | c = All terms but where $k = 0$ vanish
}}
{{eqn | r = 1
      | c = Binomial Coefficient with Zero
}}
{{eqn | r = {n \brack n - 0}
      | c = Unsigned Stirling Number of the First Kind of Number with Self
}}
{{end-eqn}}
So $\map P 0$ is seen to hold.
Theorem: Sum over k of m-n choose m+k by m+n choose n+k by Unsigned Stirling Number of the First Kind of m+k with k

Let $m, n \in \Z_{\ge 0}$.
:$\ds \sum_k \binom {m - n} {m + k} \binom {m + n} {n + k} {m + k \brack k} = {n \brace n - m}$
where:
:$\dbinom {m - n} {m + k}$ etc. denote binomial coefficients
:$\ds {m + k \brack k}$ denotes an unsigned Stirling number of the first kind
:$\ds {n \brace n - m}$ denotes a Stirling number of the second kind.

Proof:
The proof proceeds by induction on $m$.
For all $m \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\forall n \in \Z_{\ge 0}: \ds \sum_k \binom {m - n} {m + k} \binom {m + n} {n + k} {m + k \brack k} = {n \brace n - m}$
Theorem: Sum over k of Stirling Number of the Second Kind of n+1 with k+1 by Unsigned Stirling Number of the First Kind of k with m by -1^k-m

Let $m, n \in \Z_{\ge 0}$.
:$\ds \sum_k {n + 1 \brace k + 1} {k \brack m} \paren {-1}^{k - m} = \binom n m$
where:
:$\dbinom n m$ denotes a binomial coefficient
:$\ds {k \brack m}$ denotes an unsigned Stirling number of the first kind
:$\ds {n + 1 \brace k + 1}$ 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 m$ be the proposition:
:$\ds \forall m \in \Z_{\ge 0}: \sum_k {n + 1 \brace k + 1} {k \brack m} \paren {-1}^{k - m} = \binom n m$
Theorem: Sum over k to n of Unsigned Stirling Number of the First Kind of k with m by n factorial over k factorial

Let $m, n \in \Z_{\ge 0}$.
:$\ds \sum_{k \mathop \le n} {k \brack m} \frac {n!} {k!} = {n + 1 \brack m + 1}$
where:
:$\ds {k \brack m}$ denotes an unsigned Stirling number of the first kind
:$ n!$ denotes a factorial.

Proof:
The proof proceeds by induction on $n$.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\ds \forall n \in \Z_{\ge 0}: \sum_{k \mathop \le n} {k \brack m} \frac {n!} {k!} = {n + 1 \brack m + 1}$