avewright/proofwiki-math huggingface dataset:
Theorem: Definition:Constructed Semantics/Instance 1/Factor Principle

The Factor Principle:
:$\left({p \implies q}\right) \implies \left({\left({r \lor p}\right) \implies \left ({r \lor q}\right)}\right)$
is a tautology in Instance 1 of constructed semantics.

Proof:
By the definitional abbreviation for the conditional:
:$\mathbf A \implies \mathbf B =_{\text{def}} \neg \mathbf A \lor \mathbf B$
the Factor Principle can be written as:
:$\neg \left({\neg p \lor q}\right) \lor \left({\neg \left({r \lor p}\right) \lor \left ({r \lor q}\right)}\right)$
This evaluates as follows:
:$\begin{array}{|ccccc|c|cccccccc|} \hline
\neg & (\neg & p & \lor & q) & \lor & (\neg & (r & \lor & p) & \lor & (r & \lor & q)) \\
\hline
1 & 2 & 1 & 2 & 1 & 2 & 2 & 1 & 1 & 1 & 2 & 1 & 1 & 1 \\
1 & 2 & 1 & 2 & 1 & 2 & 1 & 2 & 2 & 1 & 2 & 2 & 2 & 1 \\
1 & 2 & 1 & 2 & 2 & 2 & 2 & 1 & 1 & 1 & 2 & 1 & 2 & 2 \\
1 & 2 & 1 & 2 & 2 & 2 & 1 & 2 & 2 & 1 & 2 & 2 & 2 & 2 \\
2 & 1 & 2 & 1 & 1 & 2 & 1 & 1 & 2 & 2 & 1 & 1 & 1 & 1 \\
2 & 1 & 2 & 1 & 1 & 2 & 1 & 2 & 2 & 2 & 2 & 2 & 2 & 1 \\
1 & 1 & 2 & 2 & 2 & 2 & 1 & 1 & 2 & 2 & 2 & 1 & 2 & 2 \\
1 & 1 & 2 & 2 & 2 & 2 & 1 & 2 & 2 & 2 & 2 & 2 & 2 & 2 \\
\hline
\end{array}$
{{qed}}
Category:Formal Semantics
g378broae9uk77f3lxwet48mpsu2f3y
Theorem: Weak Inequality of Integers iff Strict Inequality with Integer plus One

Let $a, b \in \Z$ be integers.
{{TFAE}}
:$(1): \quad a \le b$
:$(2): \quad a < b + 1$
where:
:$\le$ is the ordering on the integers
:$<$ is the strict ordering on the integers.

Proof:
{{ProofWanted}}
Category:Orderings on Integers
o50pjpmex3eprkvlhweb2aux9n6498h
Theorem: Set of Orbits forms Partition

Let $G$ be a group.
Let $X$ be a set.
Let $G$ act on $X$.
Then the set of orbits of the group action forms a partition of $X$.

Proof:
Follows from the Fundamental Theorem on Equivalence Relations.
{{qed}}
Theorem: Interior of Closure is Regular Open

Let $T = \struct {S, \tau}$ be a topological space.
Let $H \subseteq S$.
Then $H^{- \circ}$ is regular open.

Proof:
We must show that $H^{- \circ - \circ} = H^{- \circ}$.
First we show that $H^{- \circ - \circ} \subseteq H^{- \circ}$.
By the definition of interior:
:$H^{- \circ} \subseteq H^-$
By Topological Closure of Subset is Subset of Topological Closure:
:$H^{- \circ -} \subseteq H^{--} = H^-$
By Interior of Subset:
:$H^{- \circ - \circ } \subseteq H^{- \circ}$
{{qed|lemma}}
Next we show $H^{- \circ - \circ} \supseteq H^{- \circ}$.
Again by the definition of interior:
:$H^{- \circ -} \supseteq H^{- \circ}$
By Interior of Subset:
:$H^{- \circ - \circ}  \supseteq H^{- \circ \circ} = H^{- \circ}$
{{qed|lemma}}
Thus by definition of set equality:
:$H^{- \circ - \circ} = H^{- \circ}$
{{qed}}
Theorem: Lobachevsky Integral Formula

Let $f$ be a continuous real function, periodic with period $\pi$.
Then:
:$\ds \int_0^\infty \frac {\sin x} x \map f x \rd x = \int_0^{\frac \pi 2} \map f x \rd x$

Proof:
{{ProofWanted}}
{{Namedfor|Nikolai Ivanovich Lobachevsky|cat = Lobachevsky}}
Category:Integral Calculus
Category:Definite Integrals involving Sine Function
0zmhrxuk54mssdudgepztl6s6lqsgus
Theorem: Upper Bound for Abscissa of Absolute Convergence of Product of Dirichlet Series

Let $f, g: \N \to \C$ be arithmetic functions with Dirichlet convolution $h = f * g$.
Let $F, G, H$ be their Dirichlet series.
Let $\sigma_f, \sigma_g, \sigma_h$ be their abscissae of absolute convergence.
Then:
:$\sigma_h \le \max \set {\sigma_f, \sigma_g}$

Proof:
Follows from Dirichlet Series of Convolution of Arithmetic Functions
{{ProofWanted}}
Category:Dirichlet Series
e03r49gdkg8ry56gqsgk754xuk3dgql
Theorem: Riemann Zeta Function in terms of Dirichlet Eta Function

Let $\zeta$ be the Riemann zeta function.
Let $\eta$ be the Dirichlet eta function.
Let $s \in \C$ be a complex number with real part $\sigma > 1$.
Then:
:$\map \zeta s = \dfrac 1 {1 - 2^{1 - s} } \map \eta s$

Proof:
{{begin-eqn}}
{{eqn | l = \map \zeta s - \map \eta s
      | r = \sum_{n \mathop = 1}^\infty \frac 1 {n^s} - \sum_{n \mathop = 1}^\infty \frac{\paren {-1}^{n - 1} } {n^s}
      | c = {{Defof|Riemann Zeta Function}}, {{Defof|Dirichlet Eta Function}}
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \paren {\frac 1 {n^s} + \frac {\paren {-1}^n} {n^s} }
      | c = Sum of Summations equals Summation of Sum
}}
{{eqn | r = 2 \sum_{n \mathop = 1}^\infty \frac 1 {\paren {2 n}^s} 
}}
{{eqn | r = 2^{1 - s} \sum_{n \mathop = 1}^\infty \frac 1 {n^s} 
}}
{{eqn | r = 2^{1 - s} \map \zeta s
      | c = {{Defof|Riemann Zeta Function}}
}}
{{eqn | ll= \leadsto
      | l = \paren {1 - 2^{1 - s} } \map \zeta s 
      | r = \map \eta s
}}
{{eqn | ll= \leadsto
      | l = \map \zeta s 
      | r = \frac 1 {1 - 2^{1 - s} } \map \eta s
}}
{{end-eqn}}
{{qed}}
Theorem: Functional Equation for Riemann Zeta Function

Let $\zeta$ be the Riemann zeta function.
Let $\map \zeta s$ have an analytic continuation for $\map \Re s > 0$.
Then:
:$\pi^{-s/2 } \map \Gamma {\dfrac s 2} \map \zeta s = \pi^{\paren {s/2 - 1/2 } } \map \Gamma {\dfrac {1 - s} 2} \map \zeta {1 - s}$
where $\Gamma$ is the gamma function

Proof:
Let $\ds \map \omega x = \sum_{n \mathop = 1}^\infty e^{-\pi n^2 x}$.
Then from Integral Representation of Riemann Zeta Function in terms of Jacobi Theta Function we have:
:$(1): \quad \ds \pi^{-s / 2} \map \Gamma {\frac s 2} \map \zeta s = -\frac 1 {s \paren {1 - s} } + \int_1^\infty \paren {x^{s / 2 - 1} + x^{- s / 2 - 1 / 2} } \map \omega x \rd x$
We observe that this integral is invariant under $s \mapsto 1 - s$.
Then:
{{begin-eqn}}
{{eqn | l = \pi^{-\paren {1 - s } / 2} \map \Gamma {\frac {1 - s} 2} \map \zeta {1 - s}
      | r = -\frac 1 {\paren {1 - s} \paren {1 - \paren {1 - s} } } + \int_1^\infty \paren {x^{\paren {1 - s} / 2 - 1} + x^{-\paren {1 - s} / 2 - 1 / 2} } \map \omega x \rd x
      | c = setting $s \mapsto 1 - s$
}}
{{eqn | r = - \frac 1 {\paren {1 - s} s} + \int_1^\infty \paren {x^{- s / 2 - 1 / 2 } + x^{s / 2 - 1} } \map \omega x \rd x
      | c = 
}}
{{eqn | r = \pi^{-s / 2} \map \Gamma {\frac s 2} \map \zeta s
      | c = from $(1)$
}}
{{end-eqn}}
as required.
{{qed}}
Theorem: Integral Representation of Riemann Zeta Function in terms of Fractional Part

Let $\zeta$ be the Riemann zeta function.
Let $s \in \C$ be a complex number with real part $\sigma > 1$.
Then 
:$\ds \map \zeta s = \frac s {s - 1} - s \int_1^\infty \fractpart x x^{-s - 1} \rd x$
where $\fractpart x$ denotes the fractional part of $x$.

Proof:
First, we observe that:
{{begin-eqn}}
{{eqn | l = \sum_{n \mathop = 1}^\infty \dfrac {n - 1} {n^s}
      | r = \sum_{n \mathop = 0}^\infty \dfrac n {\paren {n + 1}^s}
      | c = {{Corollary|Translation of Index Variable of Summation}}
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \dfrac n {\paren {n + 1}^s}
      | c = $0$th term vanishes
}}
{{eqn | r = \dfrac 1 {2^s} + \dfrac 2 {3^s} + \dfrac 3 {4^s} + \cdots
      | c = 
}}
{{end-eqn}}
Rearranging terms, we get:
{{begin-eqn}}
{{eqn | l = \sum_{n \mathop = 1}^\infty \dfrac n {n^s} - \sum_{n \mathop = 1}^\infty \dfrac 1 {n^s}
      | r = \sum_{n \mathop = 1}^\infty \dfrac n {\paren {n + 1}^s}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sum_{n \mathop = 1}^\infty \dfrac 1 {n^s}
      | r = \sum_{n \mathop = 1}^\infty \dfrac n {n^s} - \sum_{n \mathop = 1}^\infty \dfrac n {\paren {n + 1}^s}
      | c = 
}}
{{end-eqn}}
Therefore, we have:
{{begin-eqn}}
{{eqn | n = 1
      | l = \sum_{n \mathop = 1}^\infty n^{-s}
      | r = \sum_{n \mathop = 1}^\infty n \paren {n^{-s} - \paren {n + 1}^{-s} }
      | c = 
}}
{{end-eqn}}
Next we note:
{{begin-eqn}}
{{eqn | l = \int_n^{n + 1} x^{-s - 1} \rd x
      | r = \intlimits {-\dfrac 1 s x^{-s} } n {n + 1}
      | c = 
}}
{{eqn | n = 2
      | r = \dfrac 1 s \paren {n^{-s} - \paren {n + 1}^{-s} }
      | c = 
}}
{{end-eqn}}
Therefore, we have:
{{begin-eqn}}
{{eqn | l = \sum_{n \mathop = 1}^\infty n^{-s}
      | r = \sum_{n \mathop = 1}^\infty n \paren {n^{-s} - \paren {n + 1}^{-s} }
      | c = from $\paren {1}$ above
}}
{{eqn | r = s \sum_{n \mathop = 1}^\infty n \int_n^{n + 1} x^{-s - 1} \rd x
      | c = from $\paren {2}$ above
}}
{{eqn | r = s \int_1^\infty \floor x x^{-s - 1} \rd x
      | c = where $\floor x$ denotes the floor function of $x$
}}
{{eqn | r = s \int_1^\infty \paren {x - \fractpart x } x^{-s - 1} \rd x
      | c = {{Defof|Fractional Part}}
}}
{{eqn | r = s \int_1^\infty x^{-s} \rd x - s \int_1^\infty \fractpart x x^{-s - 1} \rd x
      | c = Linear Combination of Complex Integrals
}}
{{eqn | r = s \intlimits {\dfrac 1 {-s + 1} x^{-s + 1} } 1 {\infty} - s \int_1^\infty \fractpart x x^{-s - 1} \rd x
      | c = Primitive of Power
}}
{{eqn | r = \frac s {s - 1} - s \int_1^\infty \fractpart x x^{-s - 1} \rd x
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Binomial Form of Relation between Riemann Zeta Function and Dirichlet Eta Function

Let $\zeta$ be the Riemann zeta function.
Let $s \in \C$ be a complex number with real part $\map \Re s > 1$.
Then:
$\ds \map \zeta s = \frac 1 {1 - 2^{1 - s} } \sum_{n \mathop = 0}^\infty \paren {\frac 1 {2^{n + 1} } \sum_{k \mathop = 0}^n \paren {-1}^k \binom n k \paren {k + 1}^{-s} }$

Proof:
Use Riemann Zeta Function in terms of Dirichlet Eta Function and Binomial Theorem.
{{ProofWanted}}
Category:Riemann Zeta Function
hms61q95kwv0fzzoq7ei3khzdgyap9t
Theorem: Analytic Continuations of Riemann Zeta Function to Complex Plane

The Riemann zeta function $\zeta$ has a unique analytic continuation to $\C \setminus \set 1$.

Proof:
Note that by Riemann Zeta Function is Analytic, $\map \zeta s$ is indeed analytic for $\map \Re s > 1$.
By Complex Plane minus Point is Connected, $\C \setminus \set 1$ is connected.
By Uniqueness of Analytic Continuation, there is at most one analytic continuation of $\zeta$ to $\C \setminus \set 1$.
{{finish|link to proofs of various analytic continuations}}
* Functional Equation for Riemann Zeta Function, analyticity is shown at Analytic Continuation of Riemann Zeta Function
* The stepwise method as in Riemann Zeta Function in terms of Dirichlet Eta Function
Theorem: Analytic Continuations of Riemann Zeta Function to Right Half-Plane

The Riemann zeta function has a unique analytic continuation to $\set {s \in \C : \map \Re s > 0} \setminus \set 1$, the half-plane $\map \Re s > 0$ minus the point $s = 1$.

Proof:
Note that by Riemann Zeta Function is Analytic, $\map \zeta s$ is indeed analytic for $\map \Re s > 1$.
By Complex Half-Plane minus Point is Connected, $\set {\sigma > 0} \setminus \set 1$ is connected.
By Uniqueness of Analytic Continuation, there is at most one analytic continuation of $\zeta$ to $\set {\sigma > 0} \setminus \set 1$.
By either:
* Analytic Continuation of Riemann Zeta Function using Dirichlet Eta Function
* Analytic Continuation of Riemann Zeta Function using Mellin Transform of Fractional Part
* Analytic Continuation of Riemann Zeta Function using Jacobi Theta Function
there exists one.
{{qed}}
Theorem: Functional Equation for Completed Riemann Zeta Function

Let $\xi : \C \to \C$ be the completed Riemann zeta function.
Let $s\in \C$ be a complex number.
Then:
:$\map \xi s = \map \xi {1 - s}$

Proof:
{{ProofWanted|Use Functional Equation for Riemann Zeta Function.}}
Category:Riemann Zeta Function
Category:Reflection Formulas
b6817fdc3ocmub9axym4500feep3v52
Theorem: Dirichlet Series of Inverse of Arithmetic Function

Let $f : \N \to\C$ be an arithmetic function.
Let $g : \N \to \C$ be an Dirichlet inverse of $f$.
Let $F, G$ be their Dirichlet series.
Let $s \in \C$ such that both $\map F s$ and $\map G s$ converge absolutely.
Then $\map F s \cdot \map G s = 1$.

Proof:
Let $\varepsilon$ be the identity arithmetic function.
By Dirichlet Series of Identity Arithmetic Function, $\varepsilon$ has Dirichlet series $\map E s = 1$.
By Dirichlet Series of Convolution of Arithmetic Functions, $\map F s \map G s = 1$.
{{qed}}
Category:Dirichlet Series
339fjb352cdslw7atl3gk5041grpmt7
Theorem: Invertibility of Arithmetic Functions

Let $f: \N \to \C$ be an arithmetic function.
Then $f$ has a Dirichlet inverse {{iff}}:
:$\map f 1 \ne 0$

Proof:
Let $*$ denote Dirichlet convolution.
Let $\varepsilon$ denote the identity arithmetic function.
Theorem: Equivalence of Definitions of Consistent Set of Formulas

{{TFAE|def = Consistent (Logic)/Proof System/Propositional Logic|view = Consistent Proof System for Propositional Logic}}
Let $\LL_0$ be the language of propositional logic.
Let $\mathscr P$ be a proof system for $\LL_0$.
Let $\FF$ be a collection of logical formulas.

Proof:
=== Definition 1 implies Definition 2 ===
Suppose that $\FF \not \vdash_{\mathscr P} \phi$.
{{AimForCont}} that there exists $\psi$ such that $\FF \vdash_{\mathscr P} \psi$ and $\FF \vdash_{\mathscr P} \neg \psi$.
Then by the Rule of Explosion (Variant 3):
:$\psi, \neg \psi \vdash_{\mathscr P} \phi$
and therefore, combining the two above lines:
:$\FF \vdash_{\mathscr P} \phi$
which is a contradiction.
{{qed|lemma}}
Theorem: Analytic Continuation of Riemann Zeta Function using Dirichlet Eta Function

Let $\zeta$ be the Riemann zeta function.
Let $\eta$ be the Dirichlet Eta Function.
Then:
:$\dfrac 1 {1 - 2^{1 - s} } \map \eta s$
defines an analytic continuation of $\zeta$ to the half-plane $\map \Re s > 0$ minus $s = 1$.

Proof:
By Riemann Zeta Function in terms of Dirichlet Eta Function, it coincides with $\zeta$ for $\map \Re s > 1$.
By Dirichlet Eta Function is Analytic, it is analytic for $\map \Re s > 0$, except at $s = 1$.
{{qed}}
Theorem: Complex Modulus of Real Number equals Absolute Value

Let $x \in \R$ be a real number.
Then the complex modulus of $x$ equals the absolute value of $x$.

Proof:
Let $x = x + 0 i \in \R$.
Then:
{{begin-eqn}}
{{eqn | l = \cmod {x + 0 i}
      | r = \sqrt {x^2 + 0^2}
      | c = {{Defof|Complex Modulus}}
}}
{{eqn | r = \sqrt {x^2}
      | c = 
}}
{{eqn | r = \size x
      | c = {{Defof|Absolute Value|index = 2}}
}}
{{end-eqn}}
{{qed}}
Theorem: Equivalence of Definitions of Ceiling Function

Let $x$ be a real number.
{{TFAE|def = Ceiling Function}}

Proof:
=== Definition 1 equals Definition 2 ===
Follows from Infimum of Set of Integers equals Smallest Element.
{{qed|lemma}}
Theorem: Characterizing Property of Infimum of Subset of Real Numbers

Let $S \subset \R$ be a non-empty subset of the real numbers.
Let $S$ be bounded below.
Let $\alpha \in \R$.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$\alpha$ is the infimum of $S$}}
{{item|(2):|$\alpha$ is a lower bound for $S$ and $\forall \epsilon \in \R_{> 0}: \exists x \in S: x < \alpha + \epsilon$}}
{{end-itemize}}

Proof:
=== $(1)$ implies $(2)$ ===
Let $\alpha$ be the infimum of $S$.
Then by definition, $\alpha$ is a lower bound for $S$.
Let $\epsilon>0$.
Because $\alpha+\epsilon>\alpha$, it is not a lower bound for $S$.
Thus there exists $x\in S$ with $x < \alpha + \epsilon$.
{{qed|lemma}}
Theorem: Characterizing Property of Supremum of Subset of Real Numbers

Let $S \subset \R$ be a non-empty subset of the real numbers.
Let $S$ be bounded above.
Let $\omega \in \R$.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$\omega$ is the supremum of $S$}}
{{item|(2):|$\omega$ is an upper bound for $S$ and $\forall \epsilon \in \R_{> 0}: \exists x \in S: x > \omega - \epsilon$}}
{{end-itemize}}

Proof:
=== $(1)$ implies $(2)$ ===
Let $\omega$ be the supremum of $S$.
Then by definition, $\omega$ is an upper bound for $S$.
Let $\epsilon > 0$.
Because $\omega - \epsilon < \omega$, it is not an upper bound for $S$.
Thus there exists $x\in S$ with $x > \omega - \epsilon$.
{{qed|lemma}}
Theorem: Limit of Positive Real Sequence is Positive

Let $\sequence {x_n}$ be a sequence of positive real numbers.
Let $x_n$ converge to $L$.
Then $L \ge 0$.

Proof:
{{AimForCont}} $L < 0$.
Then for any $n \in \N$:
{{begin-eqn}}
{{eqn | l = \size {x_n - L}
      | r = x_n - L
      | c = $x_n \ge 0 > L$
}}
{{eqn | o = \ge
      | r = -L
      | c = $> 0$
}}
{{end-eqn}}
This contradicts {{Defof|Convergent Real Sequence}}.
Hence we must have $L \ge 0$.
{{qed}}
Category:Convergence
pxp5gu8p4oqesdba1ntolkfn6lqw4fz
Theorem: Real Sequence with Nonzero Limit is Eventually Nonzero

Let $\sequence {x_n}$ be a real sequence.
Let $\sequence {x_n}$ converge to $a \ne 0$.
Then:
:$\exists N \in \N: \forall n \ge N: x_n \ne 0$
That is, eventually every term of $\sequence {x_n}$ becomes non-zero.

Proof:
Suppose $a > 0$. 
By Sequence Converges to Within Half Limit:
:$\exists N \in \N: \forall n > N: x_n > \dfrac a 2 > 0$
Now suppose $a < 0$. 
By Sequence Converges to Within Half Limit:
:$\exists N \in \N: \forall n > N: x_n < \dfrac a 2 < 0$
This shows that if $a \ne 0$:
:$\exists N \in \N: \forall n > N: x_n \ne 0$
{{qed}}
Theorem: Mittag-Leffler Expansion for Cotangent Function

:$\ds \pi \cot \pi z = \frac 1 z + 2 \sum_{n \mathop = 1}^\infty \frac z {z^2 - n^2}$
where:
:$z \in \C$ is not an integer
:$\cot$ is the cotangent function.

Proof:
From {{Corollary|Mittag-Leffler Expansion for Cotangent Function|1}}, we have:
{{begin-eqn}}
{{eqn | l = \frac \pi {2 n} \map \cot {\frac {\pi m} {2 n} }
      | r = \frac 1 m + \sum_{k \mathop = 1}^\infty \paren {\frac 1 {2 k n + m} - \frac 1 {2 k n - m} }
      | c = 
}}
{{eqn | r = \frac 1 m + \paren {\frac 1 {2 n + m} - \frac 1 {2 n - m} } + \paren {\frac 1 {4 n + m} - \frac 1 {4 n - m} } + \paren {\frac 1 {6 n + m} - \frac 1 {6 n - m} } + \cdots
      | c = 
}}
{{end-eqn}}
Let $m := 1$ and $n := 2$.
Then:
{{begin-eqn}}
{{eqn | l = \frac \pi 4 \map \cot {\frac \pi 4}
      | r = 1 + \sum_{k \mathop = 1}^\infty \paren {\frac 1 {4 k + 1} - \frac 1 {4 k - 1} }
      | c = 
}}
{{eqn | r = 1 + \sum_{k \mathop = 1}^\infty \paren {-\frac 1 {4 k - 1} + \frac 1 {4 k + 1} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac \pi 4
      | r = 1 + \paren {-\frac 1 3 + \frac 1 5} + \paren {-\frac 1 7 + \frac 1 9} + \paren {-\frac 1 {11} + \frac 1 {13} } + \cdots
      | c = {{cot|45}}
}}
{{end-eqn}}
{{qed}}
Theorem: Mittag-Leffler Expansion for Cotangent Function

:$\ds \pi \cot \pi z = \frac 1 z + 2 \sum_{n \mathop = 1}^\infty \frac z {z^2 - n^2}$
where:
:$z \in \C$ is not an integer
:$\cot$ is the cotangent function.

Proof:
Let $\LL$ denote the logarithmic derivative.
On the open set $\C \setminus \Z$ we have:
{{begin-eqn}}
{{eqn | l = \pi \cot \pi z 
      | r = \map \LL {\map \sin {\pi z} }
      | c = Primitive of Cotangent Function, or a complex version thereof
}}
{{eqn | r = \map \LL {\pi z \prod_{n \mathop = 1}^\infty \paren {1 - \frac {z^2} {n^2} } }
      | c = Euler Formula for Sine Function
}}
{{eqn | r = \map \LL {\pi z} + \sum_{n \mathop = 1}^\infty \map \LL {1 - \frac {z^2} {n^2} }
      | c = Logarithmic Derivative of Infinite Product of Analytic Functions
}}
{{eqn | r = \frac \pi {\pi z} + \sum_{n \mathop = 1}^\infty \frac 1 {1 - \frac {z^2} {n^2} } \cdot \map {\frac \d {\d z} } {1 - \frac {z^2} {n^2} }
      | c = {{Defof|Logarithmic Derivative of Meromorphic Function}}
}}
{{eqn | r = \frac 1 z - 2 \sum_{n \mathop = 1}^\infty \frac z {n^2 - z^2}
      | c = Derivative of Power
}}
{{eqn | r = \frac 1 z + 2 \sum_{n \mathop = 1}^\infty \frac z {z^2 - n^2}
}}
{{end-eqn}}
{{qed}}
Theorem: Mittag-Leffler Expansion for Cotangent Function

:$\ds \pi \cot \pi z = \frac 1 z + 2 \sum_{n \mathop = 1}^\infty \frac z {z^2 - n^2}$
where:
:$z \in \C$ is not an integer
:$\cot$ is the cotangent function.

Proof:
Let $\map \zeta s$ be the Riemann zeta function.
Let $\ds \map g z = \sum_{n \mathop = 1}^\infty z^n \map \zeta {2 n}$ be the  generating function of $\map \zeta {2 n}$
By Power Series Expansion for Cotangent Function, for $\size z < 1$:
{{begin-eqn}}
{{eqn | l = \pi \map \cot {\pi z}
      | r = \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n \pi^{2 n} 2^{2 n} B_{2 n} \, z^{2 n - 1} } {\paren {2 n}!}
}}
{{eqn | ll= \leadsto
      | l = \pi z \map \cot {\pi z}
      | r = 1 + \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^n \pi^{2 n} 2^{2 n} B_{2 n} \, z^{2 n} } {\paren {2 n}!}
}}
{{eqn | ll= \leadsto
      | l = \frac {\pi z \map \cot {\pi z} - 1} {-2}
      | r = \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n + 1} \pi^{2 n} 2^{2 n - 1} B_{2 n} \, z^{2 n} } {\paren {2 n}!}
}}
{{end-eqn}}
By Riemann Zeta Function at Even Integers:
:$\map \zeta {2 n} = \dfrac {\paren {-1}^{n + 1} \pi^{2 n} 2^{2 n - 1} B_{2 n}  } {\paren {2 n}!}$
Thus:
{{begin-eqn}}
{{eqn | l = \dfrac {\pi z \map \cot {\pi z} - 1} {-2}
      | r = \sum_{n \mathop = 1}^\infty \map \zeta {2 n} z^{2 n} 
}}
{{eqn | r = \map g {z^2}
}}
{{end-eqn}}
By Analytic Continuation of Generating Function of Dirichlet Series and Uniqueness of Analytic Continuation: 
:$\ds \dfrac {\pi z \map \cot {\pi z} - 1} {-2} = \sum_{n \mathop = 1}^\infty \dfrac {z^2} {n^2 - z^2}$
for all of $\C$, as this is the overlap of their domains.
Thus:
{{begin-eqn}}
{{eqn | l = \pi z \map \cot {\pi z} - 1
      | r =  2 \sum_{n \mathop = 1}^\infty \frac {z^2} {z^2 - n^2}
}}
{{eqn | ll= \leadsto
      | l = \pi z \map \cot {\pi z}
      | r =  1 + 2 \sum_{n \mathop = 1}^\infty \frac {z^2} {z^2 - n^2}
}}
{{eqn | ll= \leadsto
      | l = \pi \map \cot {\pi z}
      | r = \frac 1 z + 2 \sum_{n \mathop = 1}^\infty \frac z {z^2 - n^2}
}}
{{end-eqn}}
{{qed}}
Theorem: Mittag-Leffler Expansion for Cotangent Function

:$\ds \pi \cot \pi z = \frac 1 z + 2 \sum_{n \mathop = 1}^\infty \frac z {z^2 - n^2}$
where:
:$z \in \C$ is not an integer
:$\cot$ is the cotangent function.

Proof:
We have that:
:$\cot \pi x = \dfrac {\cos \pi x} {\sin \pi x}$
has a denominator which is $0$ at $x = 0, \pm 1, \pm 2, \ldots$.
Hence the limitation on the domain of $x \cot \pi x$ to exclude integer $x$.
Having established that, we should be able to express $\cot \pi x$ in the form:
:$\cot \pi x = \dfrac a x + \ds \sum_{n \mathop = 1}^\infty \paren {\frac {b_n} {x - n} + \frac {c_n} {x + n} }$
{{explain|why should we be able to express the cotangent in this form?}}
using a partial fractions expansion.
By evaluating the coefficients $b_n$ and $c_n$ in the usual manner, they are found to be:
{{explain|Link to what this usual manner is}}
{{finish|Do the work}}
:$\forall n \in \N: b_n = c_n = \dfrac 1 \pi$
The result follows.
{{qed}}
Theorem: Mittag-Leffler Expansion for Cotangent Function

:$\ds \pi \cot \pi z = \frac 1 z + 2 \sum_{n \mathop = 1}^\infty \frac z {z^2 - n^2}$
where:
:$z \in \C$ is not an integer
:$\cot$ is the cotangent function.

Proof:
From the Euler Formula for Sine Function:
:$\ds \sin x = x \prod_{n \mathop = 1}^\infty \paren {1 - \frac {x^2} {n^2 \pi^2} }$
Taking the logarithm of both sides:
{{begin-eqn}}
{{eqn | l = \map \ln {\sin x}
      | r = \ln x + \sum_{n \mathop = 1}^\infty \map \ln {1 - \frac {x^2} {n^2 \pi^2} }
      | c = 
}}
{{eqn | r = \ln x + \sum_{n \mathop = 1}^\infty \map \ln {\frac {n^2 \pi^2 - x^2} {n^2 \pi^2} }
      | c = 
}}
{{end-eqn}}
Differentiating {{WRT|Differentiation}} $x$:
{{begin-eqn}}
{{eqn | l = \cot x
      | r = \dfrac 1 x + \sum_{n \mathop = 1}^\infty \dfrac {\dfrac {-2 x} {n^2 \pi^2} } {\paren {\dfrac {n^2 \pi^2 - x^2} {n^2 \pi^2} } }
      | c = Derivative of Composite Function
}}
{{eqn | r = \dfrac 1 x + \sum_{n \mathop = 1}^\infty \frac {-2 x} {n^2 \pi^2 - x^2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \cot x
      | r = \frac 1 x + 2 x \sum_{n \mathop = 1}^\infty \frac 1 {x^2 - n^2 \pi^2}
      | c = moving the $-1$ to the denominator
}}
{{eqn | ll= \leadsto
      | l = \pi \map \cot {\pi x}
      | r = \pi \paren {\frac 1 {\pi x} + 2 \paren {\pi x} \sum_{n \mathop = 1}^\infty \frac 1 {\paren {\pi x}^2 - n^2 \pi^2} }
      | c = multiplying by $\pi$ and entering $\pi x$
}}
{{eqn | ll= \leadsto
      | l = \pi \map \cot {\pi x}
      | r = \frac 1 x + 2 x \sum_{n \mathop = 1}^\infty \frac 1 {x^2 - n^2 }
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}