avewright/proofwiki-math huggingface dataset:
Theorem: Smallest Element is Infimum

Let $\struct {S, \preceq}$ be an ordered set.
Let $T \subseteq S$.
Let $T$ have a smallest element $m$.
Then $m$ is the infimum of $T$ in $S$.

Proof:
Let $M$ be the smallest element of $T$.
Then by definition:
:$\forall x \in T: m \preceq x$
By definition of infimum, it is necessary to show that:
:$(1): \quad m$ is a lower bound of $T$ in $S$
:$(2): \quad L \preceq m$ for all lower bounds $L$ of $T$ in $S$.
By Smallest Element is Lower Bound, $m$ is a lower bound of $T$ in $S$.
It remains to be shown that:
:$L \preceq m$ for all lower bounds $L$ of $T$ in $S$.
Let $L \in S$ be a lower bound of $T$ in $S$.
By definition of lower bound:
:$\forall t \in T: L \preceq t$
We have that $m \in T$.
Therefore:
:$L \preceq m$
Hence the result.
{{qed}}
Theorem: Floor Function/Examples/Floor of 1.1

:$\floor {1 \cdotp 1} = 1$

Proof:
We have that:
:$1 \le 1 \cdotp 1 < 2$
Hence $1$ is the floor of $1 \cdotp 1$ by definition.
{{qed}}
Theorem: Floor Function/Examples/Floor of -1.1

:$\floor {-1 \cdotp 1} = -2$

Proof:
We have that:
:$-2 \le -1 \cdotp 1 < -1$
Hence $-2$ is the floor of $-1 \cdotp 1$ by definition.
{{qed}}
Theorem: Ceiling Function/Examples/Ceiling of -1.1

:$\ceiling {-1 \cdotp 1} = -1$

Proof:
We have that:
:$-2 < -1 \cdotp 1 \le -1$
Hence $-1$ is the ceiling of $-1 \cdotp 1$ by definition.
{{qed}}
Theorem: Floor Function/Examples/Floor of 0.99999

:$\floor {0 \cdotp 99999} = 0$

Proof:
We have that:
:$0 \le 0 \cdotp 99999 < 1$
Hence $0$ is the floor of $0 \cdotp 99999$ by definition.
{{qed}}
Theorem: Floor Function/Examples/Floor of Binary Logarithm of 35

:$\floor {\lg 35} = 5$
where:
:$\lg x$ denotes the '''binary logarithm ($\log_2$)''' of $x$

Proof:
{{begin-eqn}}
{{eqn | l = \lg 32
      | o = \le
      | m = \lg 35
      | mo= <
      | r = \lg 64
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 5
      | o = \le
      | m = \lg 35
      | mo= <
      | r = 6
      | c = 
}}
{{end-eqn}}
Hence $5$ is the floor of $\lg 35$ by definition.
{{qed}}
Theorem: Modulo Operation/Examples/100 mod 3

:$100 \bmod 3 = 1$

Proof:
By definition of modulo operation:
:$x \bmod y := x - y \floor {\dfrac x y}$
for $y \ne 0$.
We have:
:$\dfrac {100} 3 = 33 + \dfrac 1 3$
and so:
:$\floor {\dfrac {100} 3} = 33$
Thus:
{{begin-eqn}}
{{eqn | l = 100 \bmod 3
      | r = 100 - 3 \times \floor {\dfrac {100} 3}
      | c = 
}}
{{eqn | r = 100 - 3 \times 33
      | c = 
}}
{{eqn | r = 1
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Modulo Operation/Examples/100 mod 7

:$100 \bmod 7 = 2$

Proof:
By definition of modulo operation:
:$x \bmod y := x - y \floor {\dfrac x y}$
for $y \ne 0$.
We have:
:$\dfrac {100} 7 = 14 + \dfrac 2 7$
and so:
:$\floor {\dfrac {100} 7} = 14$
Thus:
{{begin-eqn}}
{{eqn | l = 100 \bmod 7
      | r = 100 - 7 \times \floor {\dfrac {100} 7}
      | c = 
}}
{{eqn | r = 100 - 7 \times 14
      | c = 
}}
{{eqn | r = 2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Modulo Operation/Examples/-100 mod 7

:$-100 \bmod 7 = 5$

Proof:
By definition of modulo operation:
:$x \bmod y := x - y \floor {\dfrac x y}$
for $y \ne 0$.
We have:
:$\dfrac {-100} 7 = -15 + \dfrac 5 7$
and so:
:$\floor {\dfrac {-100} 7} = -15$
Thus:
{{begin-eqn}}
{{eqn | l = -100 \bmod 7
      | r = -100 - 7 \times \floor {\dfrac {-100} 7}
      | c = 
}}
{{eqn | r = -100 + 7 \times 15
      | c = 
}}
{{eqn | r = 5
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Modulo Operation/Examples/-100 mod 0

:$-100 \bmod 0 = -100$

Proof:
By definition of modulo $0$:
:$\forall x \in \R: x \bmod 0 = x$
Hence:
:$-100 \bmod 0 = -100$
{{qed}}
Theorem: Modulo Operation/Examples/5 mod -3

:$5 \bmod -3 = -1$

Proof:
By definition of modulo operation:
:$x \bmod y := x - y \floor {\dfrac x y}$
for $y \ne 0$.
We have:
:$\dfrac 5 {-3} = -2 + \dfrac 1 3$
and so:
:$\floor {\dfrac 5 {-3} } = -2$
Thus:
{{begin-eqn}}
{{eqn | l = 5 \bmod -3
      | r = 5 - \paren {-3} \times \floor {\dfrac 5 {-3} }
      | c = 
}}
{{eqn | r = 5 - \paren {-3} \times \paren {-2}
      | c = 
}}
{{eqn | r = 5 - 3 \times 2
      | c = 
}}
{{eqn | r = -1
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Modulo Operation/Examples/18 mod -3

:$18 \bmod -3 = 0$

Proof:
By definition of modulo operation:
:$x \bmod y := x - y \floor {\dfrac x y}$
for $y \ne 0$.
We have:
:$\dfrac {18} {-3} = -6 + \dfrac 0 3$
and so:
:$\floor {\dfrac {18} {-3} } = -6$
Thus:
{{begin-eqn}}
{{eqn | l = 18 \bmod -3
      | r = 18 - \paren {-3} \times \floor {\dfrac {18} {-3} }
      | c = 
}}
{{eqn | r = 18 - \paren {-3} \times \paren {-6}
      | c = 
}}
{{eqn | r = 18 - 3 \times 6
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Modulo Operation/Examples/-2 mod -3

:$-2 \bmod -3 = -2$

Proof:
By definition of modulo operation:
:$x \bmod y := x - y \floor {\dfrac x y}$
for $y \ne 0$.
We have:
:$\dfrac {-2} {-3} = 0 + \dfrac 2 3$
and so:
:$\floor {\dfrac {-2} {-3} } = 0$
Thus:
{{begin-eqn}}
{{eqn | l = -2 \bmod -3
      | r = -2 - \paren {-3} \times \floor {\dfrac {-2} {-3} }
      | c = 
}}
{{eqn | r = -2 - \paren {-3} \times 0
      | c = 
}}
{{eqn | r = -2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Modulo Operation/Examples/1.1 mod 1

:$1 \cdotp 1 \bmod 1 = 0 \cdotp 1$

Proof:
By definition of modulo $1$:
:$x \bmod 1 = x - \floor x$
Thus:
{{begin-eqn}}
{{eqn | l = 1 \cdotp 1 \bmod 1
      | r = 1 \cdotp 1 - \floor {1 \cdotp 1}
      | c = 
}}
{{eqn | r = 1 \cdotp 1 - 1
      | c = 
}}
{{eqn | r = 0 \cdotp 1
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Modulo Operation/Examples/0.11 mod 0.1

:$0 \cdotp 11 \bmod 0 \cdotp 1 = 0 \cdotp 01$

Proof:
By definition of modulo operation:
:$x \bmod y := x - y \floor {\dfrac x y}$
for $y \ne 0$.
We have:
{{begin-eqn}}
{{eqn | l = \dfrac {0 \cdotp 11} {0 \cdotp 1}
      | r = \dfrac {1 \cdotp 1} 1
      | c = 
}}
{{eqn | r = 1 \cdotp 1
      | c = 
}}
{{end-eqn}}
and so:
:$\floor {\dfrac {0 \cdotp 11} {0 \cdotp 1} } = 1$
Thus:
{{begin-eqn}}
{{eqn | l = 0 \cdotp 11 \bmod 0 \cdotp 1
      | r = 0 \cdotp 11 - 0 \cdotp 1 \times \floor {\dfrac {0 \cdotp 11} {0 \cdotp 1} }
      | c = 
}}
{{eqn | r = 0 \cdotp 11 - 0 \cdotp 1 \times 1
      | c = 
}}
{{eqn | r = 0 \cdotp 01
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Modulo Operation/Examples/0.11 mod -0.1

:$0 \cdotp 11 \bmod -0 \cdotp 1 = -0 \cdotp 09$

Proof:
By definition of modulo operation:
:$x \bmod y := x - y \floor {\dfrac x y}$
for $y \ne 0$.
We have:
{{begin-eqn}}
{{eqn | l = \dfrac {0 \cdotp 11} {-0 \cdotp 1}
      | r = \dfrac {1 \cdotp 1} {-1}
      | c = 
}}
{{eqn | r = -1 \cdotp 1
      | c = 
}}
{{end-eqn}}
and so:
:$\floor {\dfrac {0 \cdotp 11} {-0 \cdotp 1} } = -2$
Thus:
{{begin-eqn}}
{{eqn | l = 0 \cdotp 11 \bmod -0 \cdotp 1
      | r = 0 \cdotp 11 - \paren {-0 \cdotp 1} \times \floor {\dfrac {0 \cdotp 11} {-0 \cdotp 1} }
      | c = 
}}
{{eqn | r = 0 \cdotp 11 - \paren {-0 \cdotp 1} \times \paren {-2}
      | c = 
}}
{{eqn | r = 0 \cdotp 11 - 0 \cdotp 2
      | c = 
}}
{{eqn | r = -0 \cdotp 09
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Modulo Operation as Integer Difference by Quotient

Let $x, y, z \in \R$ be real numbers.
Let $y > 0$.
Let $0 \le z < y$.
Let:
:$\dfrac {x - z} y = k$
for some integer $k$.
Then:
:$z \equiv x \bmod y$
where $\bmod$ denotes the modulo operation.

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \dfrac {x - z} y
      | r = k
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = x
      | r = z - k y
      | c = 
}}
{{end-eqn}}
We also have:
:$0 \le z < y$
Hence:
:$0 \le \dfrac z y < 1$
and so by definition of floor function:
:$(2): \quad \floor {\dfrac z y} = 0$
Thus:
{{begin-eqn}}
{{eqn | l = x \bmod y
      | r = x - y \floor {\dfrac x y}
      | c = {{Defof|Modulo Operation}}: note that $y \ne 0$ by hypothesis
}}
{{eqn | r = \paren {z - k y} - y \floor {\dfrac {z - k y} y}
      | c = from $(1)$
}}
{{eqn | r = z - k y - y \floor {\dfrac z y - k}
      | c = 
}}
{{eqn | r = z - k y - y \paren {\floor {\dfrac z y} - k}
      | c = Floor of Number plus Integer
}}
{{eqn | r = z - k y + k y - y \floor {\dfrac z y}
      | c = 
}}
{{eqn | r = z - y \times 0
      | c = from $(2)$
}}
{{end-eqn}}
The result follows.
{{Qed}}
Theorem: Common Factor Cancelling in Congruence/Corollary 1/Warning

Let $a$ ''not'' be coprime to $m$.
Then it is not necessarily the case that:
:$x \equiv y \pmod m$

Proof:
Proof by Counterexample:
Let $a = 6, b = 21, x = 7, y = 12, m = 15$.
We note that $\map \gcd {6, 15} = 3$ and so $6$ and $15$ are not coprime.
We have that:
{{begin-eqn}}
{{eqn | l = 6
      | o = \equiv
      | r = 6
      | rr= \pmod {15}
      | c = 
}}
{{eqn | l = 21
      | o = \equiv
      | r = 6
      | rr= \pmod {15}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a
      | o = \equiv
      | r = b
      | rr= \pmod {15}
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = 6 \times 7
      | r = 42
      | c = 
}}
{{eqn | o = \equiv
      | r = 12
      | rr= \pmod {15}
      | c = 
}}
{{eqn | l = 21 \times 12
      | r = 252
      | c = 
}}
{{eqn | o = \equiv
      | r = 12
      | rr= \pmod {15}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a x
      | o = \equiv
      | r = b y
      | rr= \pmod {15}
      | c = 
}}
{{end-eqn}}
But:
{{begin-eqn}}
{{eqn | l = 7
      | o = \equiv
      | r = 7
      | rr= \pmod {15}
      | c = 
}}
{{eqn | l = 12
      | o = \equiv
      | r = 12
      | rr= \pmod {15}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \not \equiv
      | r = y
      | rr= \pmod {15}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Congruence by Factors of Modulo/Warning

Let $r$ ''not'' be coprime to $s$.
Then it is not necessarily the case that:
:$a \equiv b \pmod {r s}$ {{iff}} $a \equiv b \pmod r$ and $a \equiv b \pmod s$
where $a \equiv b \pmod r$ denotes that $a$ is congruent modulo $r$ to $b$.

Proof:
Proof by Counterexample:
Let $a = 30, b = 40, r = 2, s = 10$.
We have that:
{{begin-eqn}}
{{eqn | l = 30
      | o = \equiv
      | r = 40
      | rr= \pmod 2
      | c = 
}}
{{eqn | l = 30
      | o = \equiv
      | r = 40
      | rr= \pmod {10}
      | c = 
}}
{{eqn-intertext|But note that:}}
{{eqn | l = 30
      | o = \not \equiv
      | r = 40
      | rr= \pmod {20}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Euler Phi Function of 2

:$\map \phi 2 = 1$

Proof:
From Euler Phi Function of Prime:
:$\map \phi p = p - 1$
As $2$ is a prime number it follows that:
:$\map \phi 2 = 2 - 1 = 1$
{{qed}}
Theorem: Existence of Abscissa of Convergence

Let $\ds \map f s = \sum_{n \mathop = 1}^\infty a_n n^{-s}$ be a Dirichlet series.
Let the series $\ds \sum_{n \mathop = 1}^\infty \size {a_n n^{-s} }$ not converge for all $s \in \C$, or diverge for all $s \in \C$.
Then there exists a real number $\sigma_c$ such that $\map f s$ converges for all $s = \sigma + i t$ with $\sigma > \sigma_c$, and does not converge for all $s$ with $\sigma < \sigma_c$.
We call $\sigma_c$ the '''abscissa of convergence''' of the Dirichlet series.

Proof:
Let $S$ be the set of all complex numbers $s$ such that $\map f s$ converges.
By hypothesis, there is some $s_0 = \sigma_0 + i t_0 \in \C$ such that $\map f {s_0}$ converges, so $S$ is not empty.
{{questionable|Which hypothesis?}}
Moreover, $S$ is bounded below, for otherwise it follows from Dirichlet Series Convergence Lemma that $\map f s$ converges for all $s \in \C$, a contradiction of our assumptions.
Therefore the infimum:
:$\sigma_c = \inf \set {\sigma: s = \sigma + i t \in S} \in \R$
is well defined.
Now if $s = \sigma + it$ with $\sigma > \sigma_c$, then there is $s' = \sigma' + i t' \in S$ with $\sigma' < \sigma$, and $\map f {s'}$ is convergent.
Then it follows from Dirichlet Series Convergence Lemma that $\map f s$ is convergent.
If $s = \sigma + it$ with $\sigma < \sigma_c$, and $\map f s$ is convergent then $s$ contradicts the definition of $\sigma_c$.
Therefore, $\sigma_c$ has the claimed properties.
{{qed}}
Theorem: Factorial as Sum of Series of Subfactorial by Falling Factorial over Factorial

{{begin-eqn}}
{{eqn | l = n!
      | r = \sum_{k \mathop \ge 0} \dfrac { {!k} \, n^{\underline k} } {k!}
      | c = 
}}
{{eqn | r = \dfrac { !0 \times n^{\underline 0} } {0!} + \dfrac { {!1} \times n^{\underline 1} } {1!} + \dfrac { {!2} \times n^{\underline 2} } {2!} + \dfrac { {!3} \times n^{\underline 3} } {3!} + \cdots
      | c = 
}}
{{eqn | r = 1 + \left({1 - \dfrac 1 {1 !} }\right) n + \left({1 - \dfrac 1 {1 !} + \dfrac 1 {2 !} }\right) n \left({n - 1}\right) + \left({1 - \dfrac 1 {1 !} + \dfrac 1 {2 !} - \dfrac 1 {3 !} }\right) n \left({n - 1}\right) \left({n - 2}\right) + \cdots
      | c = 
}}
{{end-eqn}}

Proof:
Let $n$ be a non-negative integer.
We assume a solution of the form:
:$(1): \quad n! = a_0 + a_1 n + a_2 n \paren {n - 1} + a_3 n \paren {n - 1} \paren {n - 2} + \cdots$
We can express $(1)$ using binomial coefficients:
:$(2): \quad n! = \ds \sum_k \dbinom n k k! a_k$
Then:
{{begin-eqn}}
{{eqn | l = \sum_n n! \binom m n \paren {-1}^{n - k}
      | r = \sum_n \paren {\sum_k \binom n k k! \, a_k} \binom m n \paren {-1}^{n - k}
      | c = substituting for $n!$ from $(2)$
}}
{{eqn | r = \sum_k k! \, a_k \sum_n \binom n k \binom m n \paren {-1}^{m - n}
      | c = changing order of summation
}}
{{eqn | r = \sum_k k! \, a_k \delta_{k m}
      | c = {{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}$}}
}}
{{eqn | r = m! \, a_m
      | c = as the $m$th term is the only one left standing
}}
{{eqn | ll= \leadsto
      | l = a_m
      | r = \sum_{n \mathop \ge 0} \paren {-1}^{m - n} \dfrac {n!} {m!} \binom m n
      | c = 
}}
{{eqn | r = \sum_{n \mathop = 0}^m \paren {-1}^{m - n} \dfrac {n!} {m!} \dfrac {m!} {n! \, \paren {m - n}!}
      | c = {{Defof|Binomial Coefficient}}
}}
{{eqn | r = \sum_{n \mathop = 0}^m \frac {\paren {-1}^{m - n} } {\paren {m - n}!}
      | c = simplifying
}}
{{eqn | r = \sum_{n \mathop = 0}^m \frac {\paren {-1}^n} {n!}
      | c = Permutation of Indices of Summation
}}
{{end-eqn}}
{{qed}}
Theorem: Factorial of Half

:$\left({\dfrac 1 2}\right)! = \dfrac {\sqrt \pi} 2$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {\dfrac 1 2}!
      | r = \map \Gamma {1 + \dfrac 1 2}
      | c = Gamma Function Extends Factorial
}}
{{eqn | r = \dfrac 1 2 \map \Gamma {\dfrac 1 2}
      | c = Gamma Difference Equation
}}
{{eqn | r = \dfrac 1 2 \sqrt {\pi}
      | c = Gamma Function of One Half
}}
{{end-eqn}}
{{qed}}
Theorem: Factorial of Half

:$\left({\dfrac 1 2}\right)! = \dfrac {\sqrt \pi} 2$

Proof:
From Infinite Product of Product of Sequence of n plus alpha over Sequence of n plus beta:
{{:Infinite Product of Product of Sequence of n plus alpha over Sequence of n plus beta}}
Setting:
:$k = 2$
:$\alpha_1 = \alpha_2 = 0$
:$\beta_1 = -\dfrac 1 2, \beta_2 = \dfrac 1 2$
we see that:
:$\alpha_1 + \alpha_2 = \beta_1 + \beta_2$
So this reduces to:
{{begin-eqn}}
{{eqn | l = \prod_{n \mathop \ge 1} \dfrac n {n - \frac 1 2} \dfrac n {n + \frac 1 2}
      | r = \dfrac {\map \Gamma {1 - \frac 1 2} \map \Gamma {1 + \frac 1 2} } {\map \Gamma 1 \map \Gamma 1}
      | c = 
}}
{{eqn | r = \map \Gamma {\frac 1 2} \map \Gamma {1 + \frac 1 2}
      | c = as $\map \Gamma 1 = 0! = 1$
}}
{{eqn | r = 2 \map \Gamma {1 + \frac 1 2}^2
      | c = Gamma Difference Equation
}}
{{end-eqn}}
We then note that by Wallis's Product:
:$\ds \prod_{n \mathop \ge 1} \dfrac n {n - \frac 1 2} \dfrac n {n + \frac 1 2} = \frac \pi 2$
Thus:
{{begin-eqn}}
{{eqn | l = \frac \pi 2
      | r = 2 \map \Gamma {1 + \frac 1 2}^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac \pi 4
      | r = \paren {\paren {\frac 1 2}!}^2
      | c = Gamma Function Extends Factorial
}}
{{eqn | ll= \leadsto
      | l = \paren {\frac 1 2}!
      | r = \frac {\sqrt \pi} 2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Integer to Power of Itself Less One Falling is Factorial

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

Proof:
{{begin-eqn}}
{{eqn | l = n^{\underline {n - 1} }
      | r = \dfrac {n!} {\left({n - \left({n - 1}\right)}\right)!}
      | c = Falling Factorial as Quotient of Factorials
}}
{{eqn | r = \dfrac {n!} {1!}
      | c = 
}}
{{eqn | r = n!
      | c = Factorial of $1$
}}
{{end-eqn}}
{{qed}}
Category:Falling Factorials
bh4xpr99b4kgrrvf6xuijumw5kx1z4v
Theorem: Recursive Form of Generalized Termial

The termial function as defined on the real numbers fulfils the identity:
:$x? = x + \paren {x - 1}?$

Proof:
By definition of the termial on the real numbers:
:$x? = \dfrac {x \paren {x + 1} } 2$
Thus:
{{begin-eqn}}
{{eqn | l = x? - x
      | r = \dfrac {x \paren {x + 1} } 2 - x
      | c = {{Defof|Termial/Real Numbers|Termial}}
}}
{{eqn | r = \dfrac {x \paren {x + 1} - 2 x} 2
      | c = 
}}
{{eqn | r = \dfrac {x^2 + x - 2 x} 2
      | c = 
}}
{{eqn | r = \dfrac {x^2 - x} 2
      | c = 
}}
{{eqn | r = \dfrac {\paren {x - 1} x} 2
      | c = 
}}
{{eqn | r = \paren {x - 1}?
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Euler Form of Gamma Function at Positive Integers

The Euler form of the Gamma function:
:$\ds \map \Gamma z := \lim_{m \mathop \to \infty} \frac {m^z m!} {z \paren {z + 1} \paren {z + 2} \cdots \paren {z + m} }$
converges to the factorial function at positive integers:
:$\ds \lim_{m \mathop \to \infty} \frac {m^n m!} {\paren {n + 1} \paren {n + 2} \cdots \paren {n + m} } = n!$

Proof:
{{begin-eqn}}
{{eqn | l = \lim_{m \mathop \to \infty} \frac {m^n m!} {\paren {n + 1} \paren {n + 2} \cdots \paren {n + m} }
      | r = \lim_{m \mathop \to \infty} \frac {m^n m!} {\frac {\paren {n + m}!} {n!} }
      | c = 
}}
{{eqn | r = n! \lim_{m \mathop \to \infty} \frac {m^n} {\paren {m + 1} \paren {m + 2} \cdots \paren {m + n} }
      | c = 
}}
{{eqn | r = n!
      | c = 
}}
{{end-eqn}}
Now we have from Factorial of Integer plus Reciprocal of Integer that:
:$\ds \lim_{m \mathop \to \infty} \dfrac {\paren {m + n}!} {m! m^n} = 1$
Now:
{{begin-eqn}}
{{eqn | l = \dfrac {n! \paren {n + 1} \paren {n + 2} \cdots \paren {n + m} } {m! m^n}
      | r = \dfrac {\paren {m + n}!} {m! m^n}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \lim_{m \mathop \to \infty} \dfrac {n! \paren {n + 1} \paren {n + 2} \cdots \paren {n + m} } {m! m^n}
      | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \lim_{m \mathop \to \infty} \dfrac {m! m^n} {\paren {n + 1} \paren {n + 2} \cdots \paren {n + m} }
      | r = n!
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Gamma Function of Minus One Half

:$\map \Gamma {-\dfrac 1 2} = -2 \sqrt \pi$

Proof:
{{begin-eqn}}
{{eqn | l = \map \Gamma {-\dfrac 1 2}
      | r = \frac {\map \Gamma {\frac 1 2} } {-1/2}
      | c = Gamma Difference Equation
}}
{{eqn | r = -2 \, \map \Gamma {\frac 1 2}
      | c = 
}}
{{eqn | r = -2 \sqrt \pi
      | c = Gamma Function of One Half
}}
{{end-eqn}}
{{qed}}
Theorem: Legendre's Theorem/Corollary

Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Let $B$ be the binary representation of $n$.
Let $r$ be the number of unit digits in $B$.
Let $n!$ denote the factorial of $n$.
Then $2^{n - r}$ is a divisor of $n!$, but $2^{n - r + 1}$ is not.

Proof:
$n$ can be represented as:
{{begin-eqn}}
{{eqn | l = n
      | r = \sum_{j \mathop = 1}^r 2^{e_j}
      | c = where $e_1 > e_2 > \cdots > e_r > 0$
}}
{{eqn | r = 2^{e_1} + 2^{e_2} + \cdots + 2^{e_r}
      | c = 
}}
{{end-eqn}}
where all of $e_1, e_2, \ldots, e_r$ are integers.
Then $r$ is the sum of the digits in $n$ as a binary number.
From Legendre's Theorem, we have:
:$\mu = \dfrac {n - r} {2 - 1}$
Hence the result.
{{qed}}
{{Namedfor|Adrien-Marie Legendre}}
Theorem: Diameter of N-Cube

Let $Q_n = \closedint {c - R} {c + R}^n$ be an $n$-cube in Euclidean $n$-Space equipped with the usual metric.
Then the diameter of $Q_n$ is given by:
:$\map \diam {Q_n} = 2 R \sqrt n$

Proof:
Write: 
:$Q_n = \ds \prod_{i \mathop = 1}^n \closedint {c - R} {c + R}_i$
Let $x, y \in Q_n$
By the definition of the usual metric, the distance between any two points $x$ and $y$ is given by:
:$\ds \map d {y - x} = \paren {\sum_{i \mathop = 1}^n \paren {y_i - x_i}^2}^{1 / 2}$
By Positive Power Function on Non-negative Reals is Strictly Increasing, this quantity is maximal when each summand is maximal.
Consider $x_i, y_i$ in the $i$th interval:
:$\closedint {c - R} {c + R}_i$
To maximize $\size {y_i - x_i}$, take $x_i = \min \closedint {c - R} {c + R}_i$ and $y_i = \max \closedint {c - R} {c + R}_i$.
Then:
:$\size {y_i - x_i} = \size {c + R - \paren {c - R} } = 2$
By the definition of an $n$-cube, each interval is of the same length.
Thus:
{{begin-eqn}}
{{eqn | l = \paren {\map \sup {\map d {y - x} } }^2
      | r = \map \sup {\sum_{i \mathop = 1}^n \paren {y_i - x_i}^2 }
}}
{{eqn | r = \paren {\sum_{i \mathop = 1}^n \paren {2 R}^2}
}}
{{eqn | r = \paren {2 R}^2 n
      | c = Sum of Identical Terms
}}
{{eqn | r = \paren {2 R \sqrt n}^2
}}
{{end-eqn}}
{{qed}}
Category:Real Analysis
n1jjh3v62a9aznw8onim3ryt7wycmja
Theorem: Legendre's Theorem

Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Let $p$ be a prime number.
Let $n$ be expressed in base $p$ representation.
Let $r$ be the digit sum of the representation of $n$ in base $p$.
Then $n!$ is divisible by $p^\mu$ but not by $p^{\mu + 1}$, where:
:$\mu = \dfrac {n - r} {p - 1}$

Proof:
$n$ can be represented as:
{{begin-eqn}}
{{eqn | l = n
      | r = \sum_{j \mathop = 0}^m a_j p^j
      | c = where $0 \le a_j < p$
}}
{{eqn | r = a_0 + a_1 p + a_2 p^2 + \cdots + a_m p^m
      | c = for some $m > 0$
}}
{{end-eqn}}
Using De Polignac's Formula, we may extract all the powers of $p$ from $n!$.
:$\mu = \ds \sum_{k \mathop > 0} \floor {\dfrac n {p^k} }$
where $\mu$ is the multiplicity of $p$ in $n!$:
:$p^\mu \divides n!$
:$p^{\mu + 1} \nmid n!$
We have that:
{{begin-eqn}}
{{eqn | l = \floor {\dfrac {n!} p}
      | r = \floor {\dfrac {a_0 + a_1 p + a_2 p^2 + a_3 p^3 + \cdots + a_m p^m} p}
      | c = 
}}
{{eqn | r = a_1 + a_2 p + a_3 p^2 + \cdots + a_m p^{m - 1}
      | c = 
}}
{{eqn | l = \floor {\dfrac {n!} {p^2} }
      | r = \floor {\dfrac {a_0 + a_1 p + a_2 p^2 +  + a_2 p^2 + \cdots + a_m p^m} {p^2} }
      | c = 
}}
{{eqn | r = a_2 + a_3 p + \cdots + a_m p^{m - 2}
      | c = 
}}
{{eqn | o = \vdots
}}
{{eqn | l = \floor {\dfrac {n!} {p^m} }
      | r = \floor {\dfrac {a_0 + a_1 p + a_2 p^2 +  + a_2 p^2 + \cdots + a_m p^m} {p^m} }
      | c = 
}}
{{eqn | r = a_m
      | c = 
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \mu
      | r = a_m \paren {p^{m - 1} + p^{m - 2} + \cdots + p + 1}
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = a_{m - 1} \paren {p^{m - 2} + p^{m - 3} + \cdots + p + 1}
      | c = 
}}
{{eqn | o = \vdots
}}
{{eqn | o = 
      | ro= +
      | r = a_2 \paren {p + 1}
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = a_1
      | c = 
}}
{{eqn | r = a_m \paren {\dfrac {p^m - 1} {p - 1} } + a_{m - 1} \paren {\dfrac {p^{m - 1} - 1} {p - 1} }
      | c = Sum of Geometric Sequence
}}
{{eqn | o = \vdots
}}
{{eqn | o = 
      | ro= +
      | r = a_2 \paren {\dfrac {p^2 - 1} {p - 1} } + a_1 \paren {\dfrac {p^1 - 1} {p - 1} } + a_0 \paren {\dfrac {p^0 - 1} {p - 1} }
      | c = where the last term evaluates to $0$
}}
{{eqn | r = \dfrac {\paren {a_m p^m + a_{m - 1} p^{m - 1} + \cdots + a_2 p^2 + a_1 p + a_0} - \paren {a_m + a_{m - 1} + \cdots + a_2 + a_1 + a_0} } {p - 1}
      | c = 
}}
{{eqn | r = \dfrac {n - r} {p - 1}
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
{{Namedfor|Adrien-Marie Legendre|cat = Legendre}}