avewright/proofwiki-math huggingface dataset:
Theorem: Sine Integral Function is Odd

:$\map \Si {-x} = -\map \Si x$

Proof:
{{begin-eqn}}
{{eqn | l = \map \Si {-x}
      | r = \int_0^{-x} \frac {\sin u} u \rd u
      | c = {{Defof|Sine Integral Function}}
}}
{{eqn | r = -\int_0^x \frac {\map \sin {-u} } {-u} \rd u
      | c = substituting $u \mapsto -u$
}}
{{eqn | r = -\int_0^x \frac {\sin u} u \rd u
      | c = Sine Function is Odd
}}
{{eqn | r = -\map \Si x
      | c = {{Defof|Sine Integral Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Sine Integral Function of Zero

:$\map \Si 0 = 0$

Proof:
By Sine Integral Function is Odd, $\Si$ is an odd function. 
Therefore, by Odd Function of Zero is Zero:
:$\map \Si 0 = 0$
{{qed}}
Theorem: Arctangent of Root 3 over 3

:$\map \arctan {\dfrac {\sqrt 3} 3} = \dfrac \pi 6$

Proof:
By definition, $\arctan$ is the inverse of the tangent function's restriction to $\openint {-\dfrac \pi 2} {\dfrac \pi 2}$. 
By {{tan|30}}:
:$\tan \dfrac \pi 6 = \dfrac {\sqrt 3} 3$
As $\dfrac \pi 6 \in \openint {-\dfrac \pi 2} {\dfrac \pi 2}$, we have by the definition of an inverse function: 
:$\map \arctan {\dfrac {\sqrt 3} 3} = \dfrac \pi 6$
{{qed}}
Category:Arctangent Function
nn15t5jhxmsis1q1dj91j977271rk5w
Theorem: Cardinality of Set Union/2 Sets

Let $S_1$ and $S_2$ be finite sets.
Then:
:$\card {S_1 \cup S_2} = \card {S_1} + \card {S_2} - \card {S_1 \cap S_2}$

Proof:
We have that Cardinality is Additive Function.
From Additive Function is Strongly Additive:
:$\card {S_1 \cup S_2} + \card {S_1 \cap S_2} = \card {S_1} + \card {S_2}$
from which the result follows.
{{qed}}
Theorem: Cardinality of Set Union/3 Sets

Let $S_1$, $S_2$ and $S_3$ be finite sets.
Then:
{{begin-eqn}}     
{{eqn | l = \card {S_1 \cup S_2 \cup S_3}
      | r = \card {S_1} + \card {S_2} + \card {S_3}
      | c =
}}
{{eqn | o = 
      | ro= -
      | r = \card {S_1 \cap S_2} - \card {S_1 \cap S_3} - \card {S_2 \cap S_3}
      | c =
}}
{{eqn | o = 
      | ro= +
      | r = \card {S_1 \cap S_2 \cap S_3}
      | c =
}}
{{end-eqn}}

Proof:
This is a specific example of Cardinality of Set Union: General Case.
{{qed}}
Theorem: P-adic Number times Integer Power of p is P-adic Integer

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $\Z_p$ be the $p$-adic integers.
Then:
:$\forall a \in \Q_p: \exists n \in \N: p^n a \in \Z_p$

Proof:
Let $a \in \Q_p$.
Theorem: Definite Integral to Infinity of Sine of a x^2

:$\ds \int_0^\infty \map \sin {a x^2} \rd x = \frac 1 2 \sqrt {\frac \pi {2 a} }$

Proof:
We have, by Euler's Formula: Corollary:
:$\map \exp {-i a x^2} = -i \map \sin {a x^2} + \map \cos {a x^2}$
As $\map \sin {a x^2}$ and $\map \cos {a x^2}$ are both real for real $a, x$, we therefore have:
{{begin-eqn}}
{{eqn	| l = \int_0^\infty \map \sin {a x^2} \rd x
	| r = -\int_0^\infty \map \Im {\map \exp {-i a x^2} } \rd x
}}
{{eqn	| r = -\map \Im {\int_0^\infty \map \exp {-i a x^2} \rd x}
}}
{{eqn	| r = -\frac 1 {\sqrt a} \map \Im {\int_0^\infty \map \exp {-i t^2} \rd t}
	| c = substituting $\sqrt a x = t$
}}
{{eqn	| r = -\frac 1 {\sqrt a} \map \Im {\frac 1 2 \sqrt {\frac \pi 2} \paren {1 - i} }
	| c = Definite Integral to Infinity of $\map \exp {-i x^2}$
}}
{{eqn	| r = \frac 1 2 \sqrt {\frac \pi {2 a} }
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral to Infinity of Cosine of a x^2

:$\ds \int_0^\infty \map \cos {a x^2} \rd x = \frac 1 2 \sqrt {\frac \pi {2 a} }$

Proof:
We have, by Euler's Formula: Corollary:
:$\map \exp {-i a x^2} = -i \map \sin {a x^2} + \map \cos {a x^2}$
As $\map \sin {a x^2}$ and $\map \cos {a x^2}$ are both real for real $a, x$, we therefore have:
{{begin-eqn}}
{{eqn	| l = \int_0^\infty \map \cos {a x^2} \rd x
	| r = \int_0^\infty \map \Re {\map \exp {-i a x^2} \rd x}
}}
{{eqn	| r = \map \Re {\int_0^\infty \map \exp {-i a x^2} \rd x}
}}
{{eqn	| r = \frac 1 {\sqrt a} \map \Re {\int_0^\infty \map \exp {-i t^2} \rd t}
	| c = substituting $\sqrt a x = t$
}}
{{eqn	| r = \frac 1 {\sqrt a} \map \Re {\frac 1 2 \sqrt {\frac \pi 2} \paren {1 - i} }
	| c = Definite Integral to Infinity of $\map \exp {-i x^2}$
}}
{{eqn	| r = \frac 1 2 \sqrt {\frac \pi {2 a} }
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to 2 Pi of Reciprocal of One minus 2 a Cosine x plus a Squared

:$\ds \int_0^{2 \pi} \frac {\d x} {1 - 2 a \cos x + a^2} = \frac {2 \pi} {1 - a^2}$

Proof:
{{explain|The context of this needs to be explained a little more deeply: the integrand is defined as a real function, but the analysis is actually in the complex plane. The latter needs to be brought forward so as to make it clear to the reader.}}
Let $C$ be the unit open disk centred at $0$. 
The boundary of $C$, $\partial C$, can be parameterized by: 
:$\map \gamma \theta = e^{i \theta}$
for $0 \le \theta \le 2 \pi$. 
We have: 
{{begin-eqn}}
{{eqn | l = \int_0^{2 \pi} \frac {\d x} {1 - 2 a \cos x + a^2}
      | r = \int_0^{2 \pi} \frac {\d x} {1 - a \paren {e^{i x} + e^{-i x} } + a^2}
      | c = Euler's Cosine Identity
}}
{{eqn | r = -\int_0^{2 \pi} \frac {e^{i x} } {a e^{2 i x} - \paren {a^2 + 1} e^{i x} + a} \rd x
}}
{{eqn | r = -\frac 1 a \int_0^{2 \pi} \frac {e^{i x} } {e^{2 i x} - \paren {a + \frac 1 a} e^{i x} + \frac a a} \rd x
}}
{{eqn | r = -\frac 1 a \int_0^{2 \pi} \frac {e^{i x} } {\paren {e^{i x} - \frac 1 a} \paren {e^{i x} - a} } \rd x
      | c = factorising
}}
{{eqn | r = -\frac 1 {i a} \int_{\partial C} \frac 1 {\paren {z - \frac 1 a} \paren {z - a} } \rd z
      | c = {{Defof|Complex Contour Integral}}, Derivative of Exponential Function
}}
{{end-eqn}}
The integrand has poles: 
:$z_1 = a$
and: 
:$z_2 = \dfrac 1 a$
We have $0 < a < 1$, so $\dfrac 1 a > 1$. 
So:
:$z_2$ lies outside the closed disk $\size z \le 1$
and:
:$z_1$ lies in $C$
Thus the only pole of concern is $z_1$. 
Therefore: 
{{begin-eqn}}
{{eqn | l = -\frac 1 {i a} \int_{\partial C} \frac 1 {\paren {z - \frac 1 a} \paren {z - a} } \rd z
      | r = -\frac {2 \pi} a \Res {\frac 1 {\paren {z - \frac 1 a} \paren {z - a} } } a
      | c = Cauchy's Residue Theorem
}}
{{eqn | r = -\frac {2 \pi} a \paren {\frac 1 {2 z - \paren {a + \frac 1 a} } }_{z \mathop = a}
      | c = Residue at Simple Pole, Derivative of Power
}}
{{eqn | r = -\frac {2 \pi} a \paren {\frac 1 {2 a - a - \frac 1 a} }
}}
{{eqn | r = \frac {2 \pi} {1 - a^2}
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral to Infinity of Hyperbolic Sine of a x over Exponential of b x minus One

:$\ds \int_0^\infty \frac {\sinh a x} {e^{b x} - 1} \rd x = \frac 1 {2 a} - \frac \pi {2 b} \cot \frac {a \pi} b$

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^\infty \frac {\sinh a x} {e^{b x} - 1} \rd x
	| r = \frac 1 2 \int_0^\infty \frac {e^{-b x} \paren {e^{a x} - e^{-a x} } } {1 - e^{-b x} }
	| c = {{Defof|Hyperbolic Sine}}
}}
{{eqn	| r = \frac 1 2 \int_0^\infty \paren {e^{\paren {a - b} x} - e^{-\paren {a + b} x} } \sum_{n \mathop = 0}^\infty e^{-n b x}
	| c = Sum of Infinite Geometric Sequence
}}
{{eqn	| r = \frac 1 2 \sum_{n \mathop = 0}^\infty \int_0^\infty \paren {e^{\paren {a - \paren {n + 1} b} x} - e^{-\paren {a + \paren {n + 1} b} x} } \rd x
	| c = Fubini's Theorem
}}
{{eqn	| r = \frac 1 2 \sum_{n \mathop = 0}^\infty \paren {\intlimits {\frac {e^{\paren {a - \paren {n + 1} b} x} } {a - \paren {n + 1} b} } 0 \infty - \intlimits {-\frac {e^{-\paren {a + \paren {n + 1} b} x} } {a + \paren {n + 1} b} } 0 \infty}
	| c = Derivative of Exponential of a x
}}
{{end-eqn}}
Note that as $b > a$, we have that $a - b < 0$.
As $b > 0$, we therefore have $a - \paren {n + 1} b < 0$ for all positive integer $n$.
We also have that as $a + \paren {n + 1} b > 0$, that $-\paren {a + \paren {n + 1} b} < 0$.
So, by Exponential Tends to Zero and Infinity: 
:$\ds \lim_{x \mathop \to \infty} \frac {e^{\paren {a - \paren {n + 1} b} x} } {a - \paren {n + 1} b} = 0$
and: 
:$\ds \lim_{x \mathop \to \infty} \frac {e^{-\paren {a + \paren {n + 1} b} x} } {a + \paren {n + 1} b} = 0$
We therefore have: 
{{begin-eqn}}
{{eqn	| l = \frac 1 2 \sum_{n \mathop = 0}^\infty \paren {\intlimits {\frac {e^{\paren {a - \paren {n + 1} b} x} } {a - \paren {n + 1} b} } 0 \infty - \intlimits {-\frac {e^{-\paren {a + \paren {n + 1} b} x} } {a + \paren {n + 1} b} } 0 \infty}
	| r = \frac 1 2 \sum_{n \mathop = 0}^\infty \paren {\frac 1 {\paren {n + 1} b - a} - \frac 1 {\paren {n + 1} b + a} }
	| c = Exponential of Zero
}}
{{eqn	| r = \sum_{n \mathop = 0}^\infty \frac a {\paren {n + 1}^2 b^2 - a^2}
	| c = Difference of Two Squares
}}
{{eqn	| r = -\frac 1 b \sum_{n \mathop = 1}^\infty \frac {\paren {\frac a b} } {\paren {\frac a b}^2 - n^2}
	| c = shifting the index, extracting factors
}}
{{end-eqn}}
By Mittag-Leffler Expansion for Cotangent Function, we have: 
:$\ds \pi \cot \pi z = \frac 1 z + 2 \sum_{n \mathop = 1}^\infty \frac z {z^2 - n^2}$
where $z$ is not an integer. 
Setting $z = \dfrac a b$, we have: 
:$\ds \pi \cot \frac {\pi a} b = \frac b a + 2 \sum_{n \mathop = 1}^\infty \frac {\paren {\frac a b} } {\paren {\frac a b}^2 - n^2}$
Rearrangement gives:
:$\ds \frac \pi 2 \cot \frac {\pi a} b - \frac b {2 a} = \sum_{n \mathop = 1}^\infty \frac {\paren {\frac a b} } {\paren {\frac a b}^2 - n^2}$
So: 
{{begin-eqn}}
{{eqn	| l = \int_0^\infty \frac {\sinh a x} {e^{b x} - 1} \rd x 
	| r = -\frac 1 b \sum_{n \mathop = 1}^\infty \frac {\paren {\frac a b} } {\paren {\frac a b}^2 - n^2}
}}
{{eqn	| r = \frac 1 {2 a} - \frac \pi {2 b} \cot \frac {a \pi} b
}}
{{end-eqn}}
{{qed}}
Theorem: Intersection is Empty and Union is Universe if Sets are Complementary

Let $A$ and $B$ be subsets of a universe $\Bbb U$.
Then:
:$A \cap B = \O$ and $A \cup B = \Bbb U$
{{iff}}:
:$B = \relcomp {\Bbb U} A$
where $\relcomp {\Bbb U} A$ denotes the complement of $A$ with respect to $\Bbb U$.

Proof:
From Complement Union with Superset is Universe: Corollary:
:$A \cup B = \mathbb U \iff \relcomp {\Bbb U} A \subseteq B$
and from Empty Intersection iff Subset of Complement:
:$A \cap B = \O \iff B \subseteq \relcomp {\Bbb U} A$
The result follows by definition of set equality.
{{qed}}
Theorem: Mittag-Leffler Expansion for Square of Secant Function

:$\ds \pi^2 \map {\sec^2} {\pi z} = 8 \sum_{n \mathop = 0}^\infty \frac {\paren {2 n + 1} + 4 z^2} {\paren {\paren {2 n + 1}^2 - 4 z^2}^2}$

Proof:
{{ProofWanted}}
{{Namedfor|Magnus Gustaf Mittag-Leffler|cat = Mittag-Leffler}}
Theorem: Union with Intersection equals Intersection with Union iff Subset

Let $A$, $B$ and $C$ be sets.
Then:
:$\paren {A \cap B} \cup C = A \cap \paren {B \cup C} \iff C \subseteq A$

Proof:
=== Necessary Condition ===
Let $C \subseteq A$.
We have:
{{begin-eqn}}
{{eqn | l = C
      | o = \subseteq
      | r = A
      | c = 
}}
{{eqn | ll= \leadsto
      | l = A \cap C
      | r = C
      | c = Intersection with Subset is Subset
}}
{{eqn | ll= \leadsto
      | l = \paren {A \cap B} \cup \paren {A \cap C}
      | r = \paren {A \cap B} \cup C
      | c = 
}}
{{eqn | ll= \leadsto
      | l = A \cap \paren {B \cup C}
      | r = \paren {A \cap B} \cup C
      | c = Intersection Distributes over Union
}}
{{end-eqn}}
and another way:
{{begin-eqn}}
{{eqn | l = C
      | o = \subseteq
      | r = A
      | c = 
}}
{{eqn | ll= \leadsto
      | l = A \cup C
      | r = A
      | c = Union with Superset is Superset
}}
{{eqn | ll= \leadsto
      | l = \paren {A \cup C} \cap \paren {B \cup C}
      | r = A \cap \paren {B \cup C}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {A \cap B} \cup C
      | r = A \cap \paren {B \cup C}
      | c = Intersection Distributes over Union
}}
{{end-eqn}}
Thus:
:$C \subseteq A \implies \paren {A \cap B} \cup C = A \cap \paren {B \cup C}$
{{qed|lemma}}
Theorem: Mittag-Leffler Expansion for Square of Cosecant Function

:$\ds \pi^2 \map {\csc^2} {\pi z} = \frac 1 {z^2} + 2 \sum_{n \mathop = 1}^\infty \frac {z^2 + n^2} {\paren {z^2 - n^2}^2}$

Proof:
{{ProofWanted}}
{{Namedfor|Magnus Gustaf Mittag-Leffler|cat = Mittag-Leffler}}
Theorem: (A cap C) cup (B cap Complement C) = Empty iff B subset C subset Complement A

Let $A$, $B$ and $C$ be subsets of a universe $\Bbb U$.
Then:
:$\paren {A \cap C} \cup \paren {B \cap \map \complement C} = \O \iff B \subseteq C \subseteq \map \complement A$
where $\map \complement C$ denotes the complement of $C$ in $\Bbb U$.

Proof:
{{begin-eqn}}
{{eqn | l = \paren {A \cap C} \cup \paren {B \cap \map \complement C}
      | r = \O
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = A \cap C
      | r = \O
      | c = Union is Empty iff Sets are Empty
}}
{{eqn | lo= \land
      | l = B \cap \map \complement C
      | r = \O
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = C
      | o = \subseteq
      | r = \map \complement A
      | c = Empty Intersection iff Subset of Complement
}}
{{eqn | lo= \land
      | l = B
      | o = \subseteq
      | r = C
      | c = Intersection with Complement is Empty iff Subset
}}
{{eqn | ll= \leadstoandfrom
      | l = B
      | o = \subseteq
      | r = C \subseteq \map \complement A
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Union of Intersections of 2 from 3 equals Intersection of Unions of 2 from 3

Let $A$, $B$ and $C$ be sets.
Then:
:$\paren {A \cap B} \cup \paren {B \cap C} \cup \paren {C \cap A} = \paren {A \cup B} \cap \paren {B \cup C} \cap \paren {C \cup A}$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {A \cap B} \cup \paren {B \cap C} \cup \paren {C \cap A}
      | r = \paren {B \cap \paren {A \cup C} } \cup \paren {C \cap A}
      | c = Intersection Distributes over Union
}}
{{eqn | r = \paren {B \cup \paren {C \cap A} } \cap \paren {\paren {A \cup C} \cup \paren {C \cap A} }
      | c = Union Distributes over Intersection
}}
{{eqn | r = \paren {B \cup \paren {C \cap A} } \cap \paren {C \cup A}
      | c = Intersection is Subset of Union, Union with Superset is Superset
}}
{{eqn | r = \paren {B \cup C} \cap \paren {B \cup A} \cap \paren {C \cup A}
      | c = Union Distributes over Intersection
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to 2 Pi of Reciprocal of Square of a plus b Sine x

:$\ds \int_0^{2 \pi} \frac {\d x} {\paren {a + b \sin x}^2} = \frac {2 \pi a} {\paren {a^2 - b^2}^{3/2} }$

Proof:
From Definite Integral from $0$ to $2 \pi$ of $\dfrac 1 {a + b \sin x}$, we have: 
:$\ds \int_0^{2 \pi} \frac {\d x} {a + b \sin x} = \frac {2 \pi} {\sqrt {a^2 - b^2} }$
We have: 
{{begin-eqn}}
{{eqn	| l = \frac \partial {\partial a} \int_0^{2 \pi} \frac {\d x} {a + b \sin x}
	| r = \int_0^{2 \pi} \frac \partial {\partial a} \paren {\frac 1 {a + b \sin x} } \rd x
	| c = Definite Integral of Partial Derivative 
}}
{{eqn	| r = -\int_0^{2 \pi} \frac {\d x} {\paren {a + b \sin x}^2}
	| c = Quotient Rule for Derivatives
}}
{{end-eqn}}
and: 
{{begin-eqn}}
{{eqn	| l = \frac \partial {\partial a} \paren {\frac {2 \pi} {\sqrt {a^2 - b^2} } }
	| r = 2 \pi \paren {\frac {-2 a} {2 \sqrt {a^2 - b^2} } } \paren {\frac 1 {a^2 - b^2} }
	| c = Quotient Rule for Derivatives
}}
{{eqn	| r = -\frac {2 \pi a} {\paren {a^2 - b^2}^{3/2} } 
}}
{{end-eqn}}
giving:
:$\ds \int_0^{2 \pi} \frac {\d x} {\paren {a + b \cos x}^2} = \frac {2 \pi a} {\paren {a^2 - b^2}^{3/2} }$
{{qed}}
Theorem: Definite Integral to Infinity of Reciprocal of Exponential of x minus One minus Exponential of -x over x

:$\ds \int_0^\infty \paren {\frac 1 {e^x - 1} - \frac {e^{-x} } x} \rd x = \gamma$

Proof:
{{begin-eqn}}
{{eqn | l = \gamma
      | r = \lim_{n \mathop \to \infty} \paren {\sum_{k \mathop = 1}^n \frac 1 k - \ln n}
      | c = {{Defof|Euler-Mascheroni Constant}}
}}
{{eqn | r = \lim_{n \mathop \to \infty} \paren {\sum_{k \mathop = 1}^n \paren {\int_0^1 x^{k - 1} \rd x } + \int_0^1 \frac {1 - x^{n - 1} } {\ln x} \rd x}
      | c = Primitive of Power, Definite Integral from $0$ to $1$ of $\dfrac {x^m - x^n} {\ln x}$
}}
{{eqn | r = \lim_{n \mathop \to \infty} \paren {\int_0^1 \paren {\sum_{k = 1}^n x^{k - 1} } \rd x + \int_0^1 \frac {1 - x^{n - 1} } {\ln x} \rd x}
      | c = Linear Combination of Definite Integrals
}}
{{eqn | r = \lim_{n \mathop \to \infty} \paren {\int_0^1 \paren {\frac {1 - x^n} {1 - x} + \frac {1 - x^{n - 1} } {\ln x} } \rd x}
      | c = Sum of Infinite Geometric Sequence
}}
{{eqn | r = \int_0^1 \lim_{n \mathop \to \infty} \paren {\frac {1 - x^n} {1 - x} + \frac {1 - x^{n - 1} } {\ln x} } \rd x
      | c = Lebesgue's Dominated Convergence Theorem
}}
{{eqn | r = \int_0^1 \paren {\frac 1 {1 - x} + \frac 1 {\ln x} } \rd x
      | c = Sequence of Powers of Number less than One
}}
{{end-eqn}}
Let: 
:$x = e^{-t}$
By Derivative of $e^{a x}$:
:$\dfrac {\d x} {\d t} = -e^{-t}$
By Exponential of Zero, we have: 
:as $x \to 1$, $t \to 0$.
By Exponential Tends to Zero and Infinity, we have: 
:as $x \to 0$, $t \to \infty$.
We therefore have: 
{{begin-eqn}}
{{eqn | l = \int_0^1 \paren {\frac 1 {1 - x} + \frac 1 {\ln x} } \rd x
      | r = -\int_\infty^0 e^{-t} \paren {\frac 1 {1 - e^{-t} } + \frac 1 {\map \ln {e^{-t} } } } \rd t
      | c = substituting $x = e^{-t}$
}}
{{eqn | r = \int_0^\infty e^{-t} \paren {\frac {e^t} {e^t - 1} - \frac 1 t} \rd t
      | c = Reversal of Limits of Definite Integral, {{Defof|Natural Logarithm}}
}}
{{eqn | r = \int_0^\infty \paren {\frac 1 {e^t - 1} - \frac {e^{-t} } t} \rd t
}}
{{end-eqn}}
{{qed}}
Theorem: Intersection Complement of Set with Itself is Complement

Let $A$ and $B$ be subsets of a universal set $\Bbb U$.
Let $\uparrow$ denote the operation on $A$ and $B$ defined as:
:$\paren {A \uparrow B} \iff \paren {\relcomp {\Bbb U} {A \cap B} }$
where $\relcomp {\Bbb U} A$ denotes the complement of $A$ in $\Bbb U$.
Then:
:$A \uparrow A = \relcomp {\Bbb U} A$

Proof:
{{begin-eqn}}
{{eqn | l = A \uparrow A
      | r = \relcomp {\Bbb U} {A \cap A} 
      | c = Definition of $\uparrow$
}}
{{eqn | r = \relcomp {\Bbb U} A
      | c = Set Intersection is Idempotent
}}
{{end-eqn}}
{{qed}}
Theorem: Set Intersection expressed as Intersection Complement

Let $A$ and $B$ be subsets of a universal set $\Bbb U$.
Let $\uparrow$ denote the operation on $A$ and $B$ defined as:
:$\paren {A \uparrow B} \iff \paren {\relcomp {\Bbb U} {A \cap B} }$
where $\relcomp {\Bbb U} A$ denotes the complement of $A$ in $\Bbb U$.
Then:
:$A \cap B = \paren {A \uparrow B} \uparrow \paren {A \uparrow B}$

Proof:
{{begin-eqn}}
{{eqn | l = A \cap B
      | r = \relcomp {\Bbb U} {\relcomp {\Bbb U} {A \cap B} }
      | c = Relative Complement of Relative Complement
}}
{{eqn | r = \relcomp {\Bbb U} {A \uparrow B}
      | c = Intersection Complement of Set with Itself is Complement
}}
{{eqn | r = \paren {A \uparrow B} \uparrow \paren {A \uparrow B}
      | c = Intersection Complement of Set with Itself is Complement
}}
{{end-eqn}}
{{qed}}
Theorem: Set Union expressed as Intersection Complement

Let $A$ and $B$ be subsets of a universal set $\Bbb U$.
Let $\uparrow$ denote the operation on $A$ and $B$ defined as:
:$\paren {A \uparrow B} \iff \paren {\relcomp {\Bbb U} {A \cap B} }$
where $\relcomp {\Bbb U} A$ denotes the complement of $A$ in $\Bbb U$.
Then:
:$A \cup B = \paren {A \uparrow A} \uparrow \paren {B \uparrow B}$

Proof:
{{begin-eqn}}
{{eqn | l = A \cup B
      | r = \relcomp {\Bbb U} {\relcomp {\Bbb U} A \cap \relcomp {\Bbb U} B}
      | c = De Morgan's Laws : Complement of Union
}}
{{eqn | r = \relcomp {\Bbb U} {\paren {A \uparrow A} \cap \paren {B \uparrow B} }
      | c = Intersection Complement of Set with Itself is Complement
}}
{{eqn | r = \paren {A \uparrow A} \uparrow \paren {B \uparrow B}
      | c = Intersection Complement of Set with Itself is Complement
}}
{{end-eqn}}
{{qed}}
Theorem: Element in Set iff Singleton in Powerset

Let $S$ be a set.
Then:
:$x \in S \iff \set x \in \powerset S$
where $\powerset S$ denotes the power set of $S$.

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = S
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \set x
      | o = \subseteq
      | r = S
      | c = Singleton of Element is Subset
}}
{{eqn | ll= \leadstoandfrom
      | l = \set x
      | o = \in
      | r = \powerset S
      | c = {{Defof|Power Set}}
}}
{{end-eqn}}
{{qed}}
Theorem: Singleton of Subset is Element of Powerset of Powerset

Let $S \subseteq T$ where $S$ and $T$ are both sets.
Then:
:$\set S \in \powerset {\powerset T}$
where $\powerset T$ denotes the power set of $T$.

Proof:
{{begin-eqn}}
{{eqn | l = S
      | o = \subseteq
      | r = T
      | c =
}}
{{eqn | ll= \leadsto
      | l = S
      | o = \in
      | r = \powerset T
      | c = {{Defof|Power Set}}
}}
{{eqn | ll= \leadsto
      | l = \set S
      | o = \in
      | r = \powerset {\powerset T}
      | c = Element in Set iff Singleton in Powerset
}}
{{end-eqn}}
{{qed}}
Theorem: Set Consisting of Empty Set is not Empty

Let $S$ be the set defined as:
:$S = \set \O$
Then $S$ is not the empty set.
That is:
:$\O \ne \set \O$

Proof:
We have:
:$\O \in \set \O$
and so:
:$\neg \paren {\forall x: x \notin \O}$
The result follows by definition of the empty set.
{{qed}}
Theorem: Elements of Ordered Pair do not Commute

Let $\set {a, b}$ be a doubleton, so that $a$ and $b$ are distinct objects.
Let $\tuple {a, b}$ denote the ordered pair such that the first coordinate is $a$ and the second coordinate is $b$.
Then:
:$\tuple {a, b} \ne \tuple {b, a}$

Proof:
By the Kuratowski formalization of $\tuple {a, b}$:
:$\tuple {a, b} = \set {\set a, \set {a, b} }$
and by Equality of Ordered Pairs:
:$\tuple {a, b} = \tuple {b, a} \iff a = b$
But $a \ne b$ and so:
:$\tuple {a, b} \ne \tuple {b, a}$
{{qed}}
Theorem: Definite Integral to Infinity of Cosine m x over x Squared plus a Squared

:$\ds \int_0^\infty \frac {\cos m x} {x^2 + a^2} \rd x = \frac \pi {2 a} e^{-m a}$

Proof:
From Definite Integral of Even Function:
:$\ds \frac 1 2 \int_{-\infty}^\infty \frac {\cos m x} {x^2 + a^2} \rd x = \int_0^\infty \frac {\cos m x} {x^2 + a^2} \rd x$
Let $R$ be a positive real number with $R > a$.
Let $C_1$ be the straight line segment from $-R$ to $R$.
Let $C_2$ be the arc of the circle of radius $R$ centred at the origin connecting $R$ and $-R$ anticlockwise.
{{explain|What is the context of $C_1$ and $C_2$?}}
Let $\Gamma = C_1 \cup C_2$. 
Let: 
:$\map f z = \dfrac {e^{i m z} } {z^2 + a^2}$
From Euler's Formula, we have: 
:$\map f z = \dfrac {\cos m z} {z^2 + a^2} + i \dfrac {\sin m z} {z^2 + a^2}$
So: 
{{begin-eqn}}
{{eqn | l = \int_{-\infty}^\infty \map f x \rd x
      | r = \int_{-\infty}^\infty \frac {\cos m x} {x^2 + a^2} \rd x + i \int_{-\infty}^\infty \frac {\sin m x} {x^2 + a^2} \rd x
      | c = Linear Combination of Definite Integrals
}}
{{eqn | r = \int_{-\infty}^\infty \frac {\cos m x} {x^2 + a^2} \rd x
      | c = Definite Integral of Odd Function
}}
{{end-eqn}}
Note that the integrand is meromorphic with simple poles where $z^2 + a^2 = 0$. 
That is, at $z = a i$ and $z = -a i$. 
As our semi-circular contour lies in the upper half-plane, the only pole of concern is $a i$.
As $R > a$, these poles do not lie on $C_2$, but are enclosed by the curve $\Gamma$.
We have: 
{{begin-eqn}}
{{eqn | l = \int_C \map f z \rd z
      | r = \int_{C_1} \frac {e^{i m z} } {z^2 + a^2} \rd z + \int_{C_2} \frac {e^{i m z} } {z^2 + a^2} \rd z
      | c = Contour Integral of Concatenation of Contours
}}
{{eqn | r = \int_{-R}^R \frac {e^{i m x} } {x^2 + a^2} \rd x + \int_{C_2} \frac {e^{i m z} } {z^2 + a^2} \rd z
      | c = {{Defof|Complex Contour Integral}}
}}
{{end-eqn}}
The integral over $C_2$ can be shown to vanish as $R \to \infty$:
{{begin-eqn}}
{{eqn | l = \size {\int_{C_2} \frac {e^{i m z} } {z^2 + a^2} \rd z}
      | o = \le
      | r = \frac \pi m \max_{0 \le \theta \le \pi} \size {\frac 1 {R^2 e^{2 i \theta} + 1} }
      | c = Jordan's Lemma
}}
{{eqn | r = \frac \pi m \paren {\frac 1 {R^2 - 1} } 
}}
{{eqn | o = \to
      | r = 0
      | c = as $R \to \infty$
}}
{{end-eqn}}
Taking $R \to \infty$, we have: 
{{begin-eqn}}
{{eqn | l = \int_{-\infty}^\infty \frac {e^{i m x} } {x^2 + a^2} \rd x
      | r = \int_C \frac {e^{i m z} } {z^2 + a^2} \rd z
}}
{{eqn | r = 2 \pi i \Res {\frac {e^{i m z} } {z^2 + a^2} } {a i}
      | c = Cauchy's Residue Theorem
}}
{{eqn | r = 2 \pi i \paren {\frac {e^{i m z} } {2 z} }_{z = a i}
      | c = Residue at Simple Pole
}}
{{eqn | r = 2 \pi i \frac {e^{-m a} } {2 a i}
}}
{{eqn | r = \frac \pi a e^{-m a}
}}
{{end-eqn}}
So: 
:$\ds \int_{-\infty}^\infty \frac {\cos m x} {x^2 + a^2} \rd x = \frac \pi a e^{-m a}$
giving:
:$\ds \int_0^\infty \frac {\cos m x} {x^2 + a^2} \rd x = \frac \pi {2 a} e^{-m a}$
{{qed}}