avewright/proofwiki-math huggingface dataset:
Theorem: Cardinality of Even and Odd Permutations on Finite Set

Let $n \in \N_{> 0}$ be a natural number greater than $0$.
Let $S$ be a set of cardinality $n$.
Let $S_n$ denote the symmetric group on $S$ of order $n$.
Let $R_e$ and $R_o$ denote the subsets of $S_n$ consisting of even permutations and odd permutations respectively.
Then the cardinality of both $R_e$ and $R_o$ is $\dfrac {n!} 2$.

Proof:
From Order of Symmetric Group:
:$\order {S_n} = n!$
where:
:$\order {S_n}$ denotes the order of $S_n$
:$n!$ denotes the factorial of $n$.
By definition:
:$\card {R_e} + \card {R_o} = \order {S_n}$
From Odd and Even Permutations of Set are Equivalent:
:$\card {R_e} = \card {R_o}$
The result follows.
{{qed}}
Theorem: Congruence Modulo Integer is Equivalence Relation

For all $z \in \Z$, congruence modulo $z$ is an equivalence relation.

Proof:
Checking in turn each of the criteria for equivalence:
Theorem: Integer Combination of Coprime Integers/General Result

Let $a_1, a_2, \ldots, a_n$ be integers.
Then $\gcd \set {a_1, a_2, \ldots, a_n} = 1$ {{iff}} there exists an integer combination of them equal to $1$:
:$\exists m_1, m_2, \ldots, m_n \in \Z: \ds \sum_{k \mathop = 1}^n m_k a_k = 1$

Proof:
First let $\exists m_1, m_2, \ldots, m_n \in \Z: \ds \sum_{k \mathop = 1}^n m_k a_k = 1$.
Let $\gcd \set {a_1, a_2, \ldots, a_n} = d$.
Then $\ds \sum_{k \mathop = 1}^n m_k a_k$ has $d$ as a divisor.
That means $d$ is a divisor of $1$.
Thus $\gcd \set {a_1, a_2, \ldots, a_n} = 1$.
{{qed|lemma}}
It remains to be shown that if $\gcd \set {a_1, a_2, \ldots, a_n} = 1$, then $\exists m_1, m_2, \ldots, m_n \in \Z: \ds \sum_{k \mathop = 1}^n m_k a_k = 1$.
The proof proceeds by induction.
For all $n \in \Z_{\ge 2}$, let $\map P n$ be the proposition:
:$\gcd \set {a_1, a_2, \ldots, a_n} = 1 \iff \exists m_1, m_2, \ldots, m_n \in \Z: \ds \sum_{k \mathop = 1}^n m_k a_k = 1$
Theorem: Beta Function of x with y+m+1

Let $\map \Beta {x, y}$ denote the Beta function.
Then:
:$\map \Beta {x, y} = \dfrac {\map {\Gamma_m} y m^x} {\map {\Gamma_m} {x + y} } \map \Beta {x, y + m + 1}$
where $\Gamma_m$ is the partial Gamma function:
{{begin-eqn}}
{{eqn  | l = \map {\Gamma_m} y
       | r = \dfrac {m^y m!} {y \paren {y + 1} \paren {y + 2} \cdots \paren {y + m} }
       | c = 
}}
{{eqn  | r = \dfrac {m^y m!} { y^{\overline {m + 1} } }
       | c = 
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn  | l = \map \Beta {x, y}
       | r = \dfrac {x + y} y \map \Beta {x, y + 1}
       | c = Beta Function of x with y+1 by x+y over y
}}
{{eqn  | r = \paren {\dfrac {x + y} y } \paren {\dfrac {x + y + 1} {y + 1} } \map \Beta {x, y + 1 + 1}
       | c = applying Beta Function of x with y+1 by x+y over y a second time
}}
{{eqn  | r = \dfrac {\paren {x + y}^{\overline {m + 1} } } {y^{\overline {m + 1} } } \map \Beta {x, y + m + 1}
       | c = after $m + 1$ times: rising factorial: $y^{\overline {m + 1} } = y \paren {y + 1} \cdots \paren {y + m}$
}}
{{end-eqn}}
Also:
{{begin-eqn}}
{{eqn | l = \map \Beta {y, m + 1}
      | r = \map \Beta {y, m} \dfrac m {y + m}
      | c = Beta Function of x with y+1 by x+y over y
}}
{{eqn | r = \dfrac {m!} {\paren {y + 1}^{\overline m} } \map \Beta {y, 1}
      | c = 
}}
{{eqn | r = \dfrac {m!} {y^{\overline {m + 1} } }
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \map \Beta {x + y, m + 1}
      | r = \map \Beta {x + y, m} \dfrac m {x + y + m}
      | c = Beta Function of x with y+1 by x+y over y
}}
{{eqn | r = \dfrac {m!} {\paren {x + y}^{\overline {m + 1} } }
      | c = 
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \map \Beta {x, y}
      | r = \dfrac {\map \Beta {y, m + 1} } {\map \Beta {x + y, m + 1} } \map \Beta {x, y + m + 1}
      | c = 
}}
{{eqn | r = \dfrac {\paren {\dfrac {m!} {y^{\overline {m + 1} } } } } {\paren {\dfrac {m!} {\paren {x + y}^{\overline {m + 1} } } } } \map \Beta {x, y + m + 1}
      | c = 
}}
{{eqn | r = \paren {\dfrac {\map {\Gamma_m} y} {m^y} } \paren {\dfrac {m^{x + y} } {\map {\Gamma_m} {x + y} } } \map \Beta {x, y + m + 1}
      | c = $\dfrac {m!} {y^{\overline {m + 1} } } = \dfrac {\map {\Gamma_m} y} {m^y}$ and $\dfrac {\paren {x + y}^{\overline {m + 1} } } {m! }  = \dfrac {m^{x + y} } {\map {\Gamma_m} {x + y} }$
}}
{{eqn | r = \dfrac {\map {\Gamma_m} y m^x} {\map {\Gamma_m} {x + y} } \map \Beta {x, y + m + 1}
      | c = $m^y$ cancels
}}
{{end-eqn}}
{{qed}}
Theorem: Beta Function of x with y+m+1

Let $\map \Beta {x, y}$ denote the Beta function.
Then:
:$\map \Beta {x, y} = \dfrac {\map {\Gamma_m} y m^x} {\map {\Gamma_m} {x + y} } \map \Beta {x, y + m + 1}$
where $\Gamma_m$ is the partial Gamma function:
{{begin-eqn}}
{{eqn  | l = \map {\Gamma_m} y
       | r = \dfrac {m^y m!} {y \paren {y + 1} \paren {y + 2} \cdots \paren {y + m} }
       | c = 
}}
{{eqn  | r = \dfrac {m^y m!} { y^{\overline {m + 1} } }
       | c = 
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn  | l = \map \Beta {x, y}
       | r = \dfrac {x + y} y \map \Beta {x, y + 1}
       | c = Beta Function of x with y+1 by x+y over y
}}
{{eqn  | r = \paren {\dfrac {x + y} y } \paren {\dfrac {x + y + 1} {y + 1} } \map \Beta {x, y + 1 + 1}
       | c = applying Beta Function of x with y+1 by x+y over y a second time
}}
{{eqn  | r = \dfrac {\paren {x + y}^{\overline {m + 1} } } {y^{\overline {m + 1} } } \map \Beta {x, y + m + 1}
       | c = after $m + 1$ times: rising factorial: $y^{\overline {m + 1} } = y \paren {y + 1} \cdots \paren {y + m}$
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn  | l = \map \Beta {x, y}
       | r = \dfrac {\paren {x + y}^{\overline {m + 1} } } {y^{\overline {m + 1} } } \map \Beta {x, y + m + 1}
       | c = 
}}
{{eqn  | r = \paren {\dfrac {m^x m^y m!} {m^x m^y m!} } \dfrac {\paren {\dfrac 1 {y^{\overline {m + 1} } } } } {\paren {\dfrac 1 {\paren {x + y}^{\overline {m + 1} } } } } \map \Beta {x, y + m + 1}
       | c = multiplying by $1$ and rearranging
}}
{{eqn  | r = \dfrac {\paren {\dfrac {m^x m^y m!} {y^{\overline {m + 1} } } } } {\paren {\dfrac {m^x m^y m!} {\paren {x + y}^{\overline {m + 1} } } } } \map \Beta {x, y + m + 1}
       | c = 
}}
{{eqn  | r = \dfrac {\paren {\dfrac {m^y m!} {y^{\overline {m + 1} } } } m^x } {\paren {\dfrac {m^x m^y m!} {\paren {x + y}^{\overline {m + 1} } } } } \map \Beta {x, y + m + 1}
       | c = isolating $m^x$
}}
{{eqn  | r = \dfrac {\map {\Gamma_m} y m^x} {\map {\Gamma_m} {x + y} } \map \Beta {x, y + m + 1}
       | c = $\map {\Gamma_m} y = \dfrac {m^y m!} { y^{\overline {m + 1} } }$ and $\map {\Gamma_m} {x + y} = \dfrac {m^{x + y} m!} { \paren {x + y}^{\overline {m + 1} } }$
}}
{{end-eqn}}
{{qed}}
Theorem: Beta Function expressed using Gamma Functions

Let $\map \Beta {x, y}$ denote the Beta function.
Then:
:$\map \Beta {x, y} = \dfrac {\map \Gamma x \, \map \Gamma y} {\map \Gamma {x + y} }$
where $\Gamma$ is the Gamma function:

Proof:
From Beta Function of x with y+m+1:
:$\map \Beta {x, y} = \dfrac {\map {\Gamma_m} y \, m^x} {\map {\Gamma_m} {x + y} } \map \Beta {x, y + m + 1}$
where $\Gamma_m$ is the partial Gamma function:
:$\map {\Gamma_m} y := \dfrac {m^y m!} {y \paren {y + 1} \paren {y + 2} \dotsm \paren {y + m} }$
From Partial Gamma Function expressed as Integral:
{{begin-eqn}}
{{eqn | l = \map {\Gamma_m} x
      | r = m^x \int_0^1 \paren {1 - t}^m t^{x - 1} \rd t
      | c = 
}}
{{eqn | r = m^x \, \map \Beta {x, m + 1}
      | c = 
}}
{{end-eqn}}
Thus:
:$\ds \lim_{m \mathop \to \infty} m^x \, \map \Beta {x, m + 1} = \map \Gamma x$
As $m^x$ is monotone, it does not matter if $m$ is integer or real.
Thus:
:$\ds \lim_{m \mathop \to \infty} \paren {m + y}^x \, \map \Beta {x, m + y + 1} = \map \Gamma x$
Hence:
{{begin-eqn}}
{{eqn | l = \map \Beta {x, y}
      | r = \lim_{m \mathop \to \infty} \dfrac {\map {\Gamma_m} y \, m^x} {\map {\Gamma_m} {x + y} } \map \Beta {x, y + m + 1}
      | c = 
}}
{{eqn | r = \lim_{m \mathop \to \infty} \dfrac {\map {\Gamma_m} y \, m^x} {\map {\Gamma_m} {x + y} } \frac {\map \Gamma x} {\paren {m + y}^x}
      | c = 
}}
{{eqn | r = \lim_{m \mathop \to \infty} \dfrac {\map {\Gamma_m} y \, \map \Gamma x} {\map {\Gamma_m} {x + y} }
      | c = as $\ds \lim_{m \mathop \to \infty} \frac {m^x} {\paren {m + y}^x} = 1$
}}
{{eqn | r = \dfrac {\map \Gamma y \, \map \Gamma x} {\map \Gamma {x + y} }
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Binomial Coefficient expressed using Beta Function

Let $\dbinom r k$ denote a binomial coefficient.
Then:
:$\dbinom r k = \dfrac 1 {\paren {r + 1} \map B {k + 1, r - k + 1} }$

Proof:
{{begin-eqn}}
{{eqn | l = \dbinom r k
      | r = \dfrac {r!} {k! \, \paren {r - k}!}
      | c = {{Defof|Binomial Coefficient/Integers|Binomial Coefficient|index = 1}}
}}
{{eqn | r = \dfrac {\map \Gamma {r + 1} } {\map \Gamma {k + 1} \map \Gamma {r - k + 1} }
      | c = Gamma Function Extends Factorial
}}
{{eqn | r = \dfrac {\map \Gamma {r + 2} } {r + 1} \dfrac 1 {\map \Gamma {k + 1} \map \Gamma {r - k + 1} }
      | c = Gamma Difference Equation
}}
{{eqn | r = \dfrac 1 {r + 1} \dfrac {\map \Gamma {r + 2} } {\map \Gamma {k + 1} \map \Gamma {r - k + 1} }
      | c = rearranging
}}
{{eqn | r = \dfrac 1 {r + 1} \dfrac 1 {\map B {k + 1, r - k + 1} }
      | c = {{Defof|Beta Function|index = 3}}
}}
{{end-eqn}}
{{qed}}
Theorem: Symmetry Rule for Binomial Coefficients/Complex Numbers

For all $z, w \in \C$ such that it is not the case that $z$ is a negative integer and $w$ an integer:
:$\dbinom z w = \dbinom z {z - w}$

Proof:
From the definition of the binomial coefficient:
:$\dbinom z w := \ds \lim_{\zeta \mathop \to z} \lim_{\omega \mathop \to w} \dfrac {\map \Gamma {\zeta + 1} } {\map \Gamma {\omega + 1} \map \Gamma {\zeta - \omega + 1} }$
where $\Gamma$ denotes the Gamma function.
{{begin-eqn}}
{{eqn | l = \dbinom z w
      | r = \lim_{\zeta \mathop \to z} \lim_{\omega \mathop \to w} \dfrac {\map \Gamma {\zeta + 1} } {\map \Gamma {\omega + 1} \map \Gamma {\zeta - \omega + 1} }
      | c = 
}}
{{eqn | r = \lim_{\zeta \mathop \to z} \lim_{\omega \mathop \to w} \dfrac {\map \Gamma {\zeta + 1} } {\map \Gamma {\zeta - \omega + 1} \map \Gamma {\omega + 1} }
      | c = 
}}
{{eqn | r = \lim_{\zeta \mathop \to z} \lim_{\omega \mathop \to w} \dfrac {\map \Gamma {\zeta + 1} } {\map \Gamma {\zeta - \omega + 1} \map \Gamma {\zeta - \paren {\zeta - \omega} + 1} }
      | c = 
}}
{{eqn | r = \dbinom z {z - w}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Factors of Binomial Coefficient/Complex Numbers

For all $z, w \in \C$ such that it is not the case that $z$ is a negative integer and $w$ an integer:
:$\dbinom z w = \dfrac z w \dbinom {z - 1} {w - 1}$
where $\dbinom z w$ is a binomial coefficient.

Proof:
{{begin-eqn}}
{{eqn | l = \dbinom z w
      | r = \lim_{\zeta \mathop \to z} \lim_{\omega \mathop \to w} \dfrac {\Gamma \left({\zeta + 1}\right)} {\Gamma \left({\omega + 1}\right) \Gamma \left({\zeta - \omega + 1}\right)}
      | c = {{Defof|Binomial Coefficient/Complex Numbers|Binomial Coefficient}}
}}
{{eqn | r = \lim_{\zeta \mathop \to z} \lim_{\omega \mathop \to w} \dfrac {\zeta \Gamma \left({\zeta}\right)} {\omega \Gamma \left({\omega}\right) \Gamma \left({\zeta - \omega + 1}\right)}
      | c = Gamma Difference Equation
}}
{{eqn | r = \lim_{\zeta \mathop \to z} \lim_{\omega \mathop \to w} \dfrac \zeta \omega \dfrac {\Gamma \left({\left({\zeta - 1}\right) + 1}\right)} {\omega \Gamma \left({\left({\omega - 1}\right) + 1}\right) \Gamma \left({\left({\zeta - 1}\right) - \left({\omega - 1}\right) + 1}\right)}
      | c = rearrangement
}}
{{eqn | r = \dfrac z w \dbinom {z - 1} {w - 1}
      | c = {{Defof|Binomial Coefficient/Complex Numbers|Binomial Coefficient}}
}}
{{end-eqn}}
{{qed}}
Theorem: Pascal's Rule/Complex Numbers

For all $z, w \in \C$ such that it is not the case that $z$ is a negative integer and $w$ an integer:
:$\dbinom z {w - 1} + \dbinom z w = \dbinom {z + 1} w$
where $\dbinom z w$ is a binomial coefficient.

Proof:
{{begin-eqn}}
{{eqn | l = \binom z {w - 1} + \binom z w
      | r = \lim_{\zeta \mathop \to z} \lim_{\omega \mathop \to w} \dfrac {\map \Gamma {\zeta + 1} } {\map \Gamma \omega \map \Gamma {\zeta - \omega + 2} } + \lim_{\zeta \mathop \to z} \lim_{\omega \mathop \to w} \dfrac {\map \Gamma {\zeta + 1} } {\map \Gamma {\omega + 1} \map \Gamma {\zeta - \omega + 1} }
      | c = {{Defof|Binomial Coefficient/Complex Numbers|Binomial Coefficient}}
}}
{{eqn | r = \lim_{\zeta \mathop \to z} \lim_{\omega \mathop \to w} \paren {\dfrac {\map \Gamma {\zeta + 1} } {\map \Gamma \omega \map \Gamma {\zeta - \omega + 2} } + \dfrac {\map \Gamma {\zeta + 1} } {\map \Gamma {\omega + 1} \map \Gamma {\zeta - \omega + 1} } }
      | c = Sum Rule for Limits of Complex Functions
}}
{{eqn | r = \lim_{\zeta \mathop \to z} \lim_{\omega \mathop \to w} \paren {\dfrac {\map \Gamma {\zeta + 1} } {\map \Gamma \omega \paren {\zeta - \omega + 1} \map \Gamma {\zeta - \omega + 1} } + \dfrac {\map \Gamma {\zeta + 1} } {\omega \map \Gamma \omega \map \Gamma {\zeta - \omega + 1} } }
      | c = Gamma Difference Equation
}}
{{eqn | r = \lim_{\zeta \mathop \to z} \lim_{\omega \mathop \to w} \paren {\dfrac {\omega \map \Gamma {\zeta + 1} + \paren {\zeta - \omega + 1} \map \Gamma {\zeta + 1} } {\omega \map \Gamma \omega \paren {\zeta - \omega + 1} \map \Gamma {\zeta - \omega + 1} } }
      | c = common demonimator
}}
{{eqn | r = \lim_{\zeta \mathop \to z} \lim_{\omega \mathop \to w} \paren {\dfrac {\omega \map \Gamma {\zeta + 1} + \paren {\zeta - \omega + 1} \map \Gamma {\zeta + 1} } {\map \Gamma {\omega + 1} \map \Gamma {\zeta - \omega + 2} } }
      | c = Gamma Difference Equation
}}
{{eqn | r = \lim_{\zeta \mathop \to z} \lim_{\omega \mathop \to w} \paren {\dfrac {\map \Gamma {\zeta + 1} \paren {\zeta - \omega + 1 + \omega} } {\map \Gamma {\omega + 1} \map \Gamma {\zeta - \omega + 2} } }
      | c = 
}}
{{eqn | r = \lim_{\zeta \mathop \to z} \lim_{\omega \mathop \to w} \paren {\dfrac {\map \Gamma {\zeta + 1} \paren {\zeta + 1} } {\map \Gamma {\omega + 1} \map \Gamma {\zeta - \omega + 2} } }
      | c = 
}}
{{eqn | r = \lim_{\zeta \mathop \to z} \lim_{\omega \mathop \to w} \paren {\dfrac {\map \Gamma {\zeta + 2} } {\map \Gamma {\omega + 1} \map \Gamma {\zeta - \omega + 2} } }
      | c = Gamma Difference Equation
}}
{{eqn | r = \binom {z + 1} w
      | c = {{Defof|Binomial Coefficient/Complex Numbers|Binomial Coefficient}}
}}
{{end-eqn}}
{{qed}}
Theorem: Product of r Choose m with m Choose k/Complex Numbers

For all $z, w \in \C$ such that it is not the case that $z$ is a negative integer and $t, w$ integers:
:$\dbinom z t \dbinom t w = \dbinom z w \dbinom {z - w} {t - w}$
where $\dbinom z w$ is a binomial coefficient.

Proof:
{{begin-eqn}}
{{eqn | l = \dbinom z t \dbinom t w
      | r = \lim_{\zeta \mathop \to z} \lim_{\tau \mathop \to t} \dfrac {\map \Gamma {\zeta + 1} } {\map \Gamma {\tau + 1} \map \Gamma {\zeta - \tau + 1} } \lim_{\tau \mathop \to t} \lim_{\omega \mathop \to w} \dfrac {\map \Gamma {\tau + 1} } {\map \Gamma {\omega + 1} \map \Gamma {\tau - \omega + 1} }
      | c = {{Defof|Binomial Coefficient|subdef = Complex Numbers}}
}}
{{eqn | r = \lim_{\zeta \mathop \to z} \lim_{\tau \mathop \to t} \paren {\dfrac {\map \Gamma {\zeta + 1} } {\map \Gamma {\tau + 1} \map \Gamma {\zeta - \tau + 1} } \dfrac {\map \Gamma {\tau + 1} } {\map \Gamma {\omega + 1} \map \Gamma {\tau - \omega + 1} } }
      | c = Product Rule for Limits of Complex Functions
}}
{{eqn | r = \lim_{\zeta \mathop \to z} \lim_{\tau \mathop \to t} \paren {\dfrac {\map \Gamma {\zeta + 1} } {\map \Gamma {\zeta - \tau + 1} \map \Gamma {\omega + 1} \map \Gamma {\tau - \omega + 1} } }
      | c = 
}}
{{eqn | r = \lim_{\zeta \mathop \to z} \lim_{\tau \mathop \to t} \paren {\dfrac {\map \Gamma {\zeta + 1} \map \Gamma {\zeta - \omega + 1} } {\map \Gamma {\omega + 1} \map \Gamma {\zeta - \omega + 1} \map \Gamma {\zeta - \tau + 1} \map \Gamma {\tau - \omega + 1} } }
      | c = 
}}
{{eqn | r = \binom z w \binom {z - w} {t - w}
      | c = {{Defof|Binomial Coefficient|subdef = Complex Numbers}}
}}
{{end-eqn}}
{{qed}}
Theorem: Chu-Vandermonde Identity/Extended

Let $r, s, \alpha, \beta \in \C$ be complex numbers.
Then:
:$\ds \sum_{k \mathop \in \Z} \dbinom r {\alpha + k} \dbinom s {\beta - k} = \dbinom {r + s} {\alpha + \beta}$
where $\dbinom r {\alpha + k}$ denotes a binomial coefficient.

Proof:
From the Chu-Vandermonde Identity, we have:
:$\ds \sum_{k \mathop \in \Z} \binom r k \binom s {n - k} = \binom {r + s} n$
Let $n = \alpha + \beta$
Let $k = \alpha + k$
Then:
:$\ds \sum_{k \mathop \in \Z} \binom r {\alpha + k} \binom s {\alpha + \beta - \paren {\alpha + k} } = \binom {r + s} {\alpha + \beta}$
:$\ds \sum_{k \mathop \in \Z} \binom r {\alpha + k} \binom s {\beta - k } = \binom {r + s} {\alpha + \beta}$
{{qed}}
{{questionable|Where is the proof that you can take a result in the real numbers and just extend it to complex numbers?}}
{{Namedfor|Chu Shih-chieh|name2 = Alexandre-Théophile Vandermonde|cat = Chu|cat2 = Vandermonde}}
Theorem: Beta Function of Half with Half

:$\map \Beta {\dfrac 1 2, \dfrac 1 2} = \pi$
where $\Beta$ denotes the Beta function.

Proof:
By definition of the Beta function:
:$\ds \map \Beta {x, y} := 2 \int_0^{\pi / 2} \paren {\sin \theta}^{2 x - 1} \paren {\cos \theta}^{2 y - 1} \rd \theta$
Thus:
{{begin-eqn}}
{{eqn | l = \map \Beta {\dfrac 1 2, \dfrac 1 2}
      | r = 2 \int_0^{\pi / 2} \paren {\sin \theta}^{2 \times \frac 1 2 - 1} \paren {\cos \theta}^{2 \times \frac 1 2 - 1} \rd \theta
      | c = 
}}
{{eqn | r = 2 \int_0^{\pi / 2} \paren {\sin \theta}^0 \paren {\cos \theta}^0 \rd \theta
      | c = 
}}
{{eqn | r = 2 \int_0^{\pi / 2} \rd \theta
      | c = 
}}
{{eqn | r = 2 \bigintlimits \theta 0 {\pi / 2}
      | c = 
}}
{{eqn | r = 2 \paren {\pi / 2 - 0}
      | c = 
}}
{{eqn | r = \pi
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Beta Function of Half with Half

:$\map \Beta {\dfrac 1 2, \dfrac 1 2} = \pi$
where $\Beta$ denotes the Beta function.

Proof:
By definition of the Beta function:
:$\ds \map \Beta {x, y} := \int_{\mathop \to 0}^{\mathop \to 1} t^{x - 1} \paren {1 - t}^{y - 1} \rd t$
Thus:
{{begin-eqn}}
{{eqn | l = \map \Beta {\dfrac 1 2, \dfrac 1 2}
      | r = \int_{\mathop \to 0}^{\mathop \to 1} t^{\frac 1 2 - 1} \paren {1 - t}^{\frac 1 2 - 1} \rd t
      | c = 
}}
{{eqn | r = \int_{\mathop \to 0}^{\mathop \to 1} \dfrac {\rd t} {\sqrt {t \paren {1 - t} } }
      | c = 
}}
{{end-eqn}}
Let $t = \sin^2 \theta$.
Then:
:$\rd t = 2 \sin \theta \cos \theta \rd \theta$
and:
{{begin-eqn}}
{{eqn | l = t
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sin^2 \theta
      | r = 0
      | c = 
}}
{{eqn | l = t
      | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sin^2 \theta
      | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \theta
      | r = \pi / 2
      | c = 
}}
{{end-eqn}}
and so:
{{begin-eqn}}
{{eqn | l = \map \Beta {\dfrac 1 2, \dfrac 1 2}
      | r = \int_{\mathop \to 0}^{\mathop \to \pi / 2} \frac {2 \sin \theta \cos \theta \rd \theta} {\sin \theta \sqrt {1 - \sin^2 \theta} }
      | c = Integration by Substitution
}}
{{eqn | r = \int_{\mathop \to 0}^{\mathop \to \pi / 2} \frac {2 \sin \theta \cos \theta \rd \theta} {\sin \theta \cos \theta}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \int_{\mathop \to 0}^{\mathop \to \pi / 2} 2 \rd \theta
      | c = 
}}
{{eqn | r = \bigintlimits {2 \theta} 0 {\pi / 2}
      | c = 
}}
{{eqn | r = 2 \times \pi / 2 - 0
      | c = 
}}
{{eqn | r = \pi
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Beta Function of Half with Half

:$\map \Beta {\dfrac 1 2, \dfrac 1 2} = \pi$
where $\Beta$ denotes the Beta function.

Proof:
By definition of the Beta function:
:$\ds \map \Beta {x, y} := \int_{\mathop \to 0}^{\mathop \to 1} t^{x - 1} \paren {1 - t}^{y - 1} \rd t$
Thus:
{{begin-eqn}}
{{eqn | l = \map \Beta {\dfrac 1 2, \dfrac 1 2}
      | r = \int_{\mathop \to 0}^{\mathop \to 1} t^{\frac 1 2 - 1} \paren {1 - t}^{\frac 1 2 - 1} \rd t
      | c = 
}}
{{eqn | r = \int_{\mathop \to 0}^{\mathop \to 1} \dfrac {\rd t} {t^{1/2} \paren {1 - t}^{1/2} }
      | c = 
}}
{{end-eqn}}
Let $t = u^2$.
Then:
:$\rd t = 2 u \rd u$
and:
{{begin-eqn}}
{{eqn | l = t
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = u^2
      | r = 0
      | c = 
}}
{{eqn | l = t
      | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = u^2
      | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = u
      | r = 1
      | c = 
}}
{{end-eqn}}
and so:
{{begin-eqn}}
{{eqn | l = \map \Beta {\dfrac 1 2, \dfrac 1 2}
      | r = \int_{\mathop \to 0}^{\mathop \to 1} \frac {2 u \rd u} {u \paren {1 - u^2}^{1/2} }
      | c = Integration by Substitution
}}
{{eqn | r = 2 \int_{\mathop \to 0}^{\mathop \to 1} \frac {\rd u} {\sqrt {\paren {1 - u^2} } }
      | c = 
}}
{{eqn | r = 2 \bigintlimits {\arcsin u} 0 1
      | c = Primitive of $\dfrac 1 {\sqrt {1 - u^2} }$
}}
{{eqn | r = 2 \times \pi / 2 - 0
      | c = 
}}
{{eqn | r = \pi
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Binomial Coefficient of Real Number with Half

:$\dbinom r {1 / 2} = \dfrac {2^{2 r + 1} } {\dbinom {2 r} r \pi}$
where $\dbinom r {1 / 2}$ denotes a binomial coefficient.

Proof:
{{begin-eqn}}
{{eqn | l = \dbinom r {1 / 2}
      | r = \lim_{\rho \mathop \to r} \dfrac {\map \Gamma {\rho + 1} } {\map \Gamma {\frac 1 2 + 1} \map \Gamma {\rho - \frac 1 2 + 1} }
      | c = {{Defof|Binomial Coefficient/Complex Numbers|Binomial Coefficient}}
}}
{{eqn | r = \lim_{\rho \mathop \to r} \dfrac {\map \Gamma {\rho + 1} } {\frac 1 2 \map \Gamma {\frac 1 2} \map \Gamma {\rho + \frac 1 2} }
      | c = Gamma Difference Equation
}}
{{eqn | r = \lim_{\rho \mathop \to r} \dfrac {2 \map \Gamma {\rho + 1} } {\sqrt \pi \, \map \Gamma {\rho + \frac 1 2} }
      | c = Gamma Function of One Half
}}
{{end-eqn}}
Legendre's Duplication Formula gives:
:$\forall z \notin \set {-\dfrac n 2: n \in \N}: \map \Gamma z \map \Gamma {z + \dfrac 1 2} = 2^{1 - 2 z} \sqrt \pi \, \map \Gamma {2 z}$
and so:
:$(1): \quad \map \Gamma {\rho + \dfrac 1 2} = \dfrac {2^{1 - 2 \rho} \sqrt \pi \, \map \Gamma {2 \rho} } {\map \Gamma \rho}$
Hence:
{{begin-eqn}}
{{eqn | l = \dbinom r {1 / 2}
      | r = \lim_{\rho \mathop \to r} \dfrac {2 \map \Gamma {\rho + 1} } {\sqrt \pi \, \dfrac {2^{1 - 2 \rho} \sqrt \pi \, \map \Gamma {2 \rho} } {\map \Gamma \rho} }
      | c = from $(1)$
}}
{{eqn | r = \lim_{\rho \mathop \to r} \dfrac {2 \map \Gamma {\rho + 1} \map \Gamma \rho} {\pi 2^{1 - 2 \rho} \map \Gamma {2 \rho} }
      | c = 
}}
{{eqn | r = \lim_{\rho \mathop \to r} \dfrac {2^{2 \rho - 1} 2 \map \Gamma {\rho + 1} \map \Gamma \rho} {\pi \map \Gamma {2 \rho} }
      | c = rearranging and simplifying
}}
{{eqn | r = \lim_{\rho \mathop \to r} \dfrac {2^{2 \rho} } {\pi \dfrac {\map \Gamma {2 \rho} } {\map \Gamma \rho \map \Gamma {\rho + 1} } }
      | c = rearranging
}}
{{eqn | r = \lim_{\rho \mathop \to r} \dfrac {2^{2 \rho} } {\pi \dfrac {\rho \map \Gamma {2 \rho + 1} } {2 \rho \map \Gamma {\rho + 1} \map \Gamma {\rho + 1} } }
      | c = Gamma Difference Equation twice
}}
{{eqn | r = \lim_{\rho \mathop \to r} \dfrac {2^{2 \rho + 1} } {\pi \dfrac {\map \Gamma {2 \rho + 1} } {\map \Gamma {\rho + 1} \map \Gamma {\rho + 1} } }
      | c = simplifying
}}
{{eqn | r = \dfrac {2^{2 r + 1} } {\dbinom {2 r} r \pi}
      | c = {{Defof|Binomial Coefficient/Complex Numbers|Binomial Coefficient}}
}}
{{end-eqn}}
{{qed}}