avewright/proofwiki-math huggingface dataset:
Theorem: Map from Set of Continuous Functions on Interval to Set of their Integrals

Let $\Bbb I = \closedint a b$ be a closed interval on the set of real numbers $\R$ such that $a < b$.
Let $A$ denote the set of all continuous real functions $f: \Bbb I \to \R$.
Let $B \subseteq A$ denote the set of all functions differentiable on $\Bbb I$ whose derivative is continuous on $\Bbb I$.
Let $C \subseteq B$ denote the subset of $B$ which consists of all elements of $B$ such that $\map f a = 0$.
For each $f \in A$, let $h$ denote the mapping defined as:
:$\map {\paren {\map h f} } x = \ds \int_a^x \map f t \rd t$
Then:
:$h: A \to C$

Proof:
Let $f \in A$ be an arbitrary continuous real function $f: \Bbb I \to \R$.
From Continuous Real Function is Darboux Integrable, $\map {\paren {\map h f} } x$ exists and is continuous on $\Bbb I$.
Let $x = a$.
Then we have:
{{begin-eqn}}
{{eqn | l = \map {\paren {\map h f} } x
      | r = \int_a^x \map f t \rd t
      | c = Definition of $h$
}}
{{eqn | ll= \leadsto
      | l = \map {\paren {\map h f} } a
      | r = \int_a^a \map f t \rd t
      | c = 
}}
{{eqn | r = 0
      | c = Definite Integral on Zero Interval
}}
{{end-eqn}}
Thus $h$ is a continuous real function on $\Bbb I$ such that $\map h a = 0$.
Further, by definition, $\ds \int \map f t \rd t$ is the primitive of $f$, and exists by dint of the above.
It follows from the Fundamental Theorem of Calculus that $f = \map {\dfrac \d {\d x} } h$ and so $\map h x$ is functions differentiable on $\Bbb I$.
Thus it is shown that $C \subseteq B \subseteq A$ and the result follows.
{{qed}}
Theorem: Definite Integral from 0 to Half Pi of Reciprocal of One plus Power of Tan x

:$\ds \int_0^{\pi/2} \frac {\d x} {1 + \tan^m x} = \frac \pi 4$

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^{\pi/2} \frac {\d x} {1 + \tan^m x} 
	| r = \int_0^{\pi/2} \frac {\cos^m x} {\cos^m x + \sin^m x} \rd x
	| c = multiplying by $\dfrac {\cos^m x} {\cos^m x}$
}}
{{eqn	| r = \int_0^{\pi/2} \frac {\map {\cos^m} {\frac \pi 2 - x} } {\map {\cos^m} {\frac \pi 2 - x} + \map {\sin^m} {\frac \pi 2 - x} } \rd x
	| c = Integral between Limits is Independent of Direction
}}
{{eqn	| r = \int_0^{\pi/2} \frac {\sin^m x} {\sin^m x + \cos^m x} \rd x
	| c = Cosine of Complement equals Sine, Sine of Complement equals Cosine
}}
{{end-eqn}}
So:
{{begin-eqn}}
{{eqn	| l = 2 \int_0^{\pi/2} \frac {\d x} {1 + \tan^m x}
	| r = \int_0^{\pi/2} \frac {\sin^m x + \cos^m x} {\sin^m x + \cos^m x} \rd x
}}
{{eqn	| r = \int_0^{\pi/2} \rd x
}}
{{eqn	| r = \frac \pi 2
	| c = Primitive of Constant
}}
{{end-eqn}}
giving: 
:$\ds \int_0^{\pi/2} \frac {\d x} {1 + \tan^m x} = \frac \pi 4$
{{qed}}
Theorem: Definite Integral from 0 to 1 of Power of x by Power of Logarithm of x

:$\ds \int_0^1 x^m \paren {\ln x}^n \rd x = \frac {\paren {-1}^n \map \Gamma {n + 1} } {\paren {m + 1}^{n + 1} }$

Proof:
Let: 
:$x = \map \exp {-\dfrac u {m + 1} }$
Then, by Derivative of Exponential Function: 
:$\dfrac {\d x} {\d u} = -\dfrac 1 {m + 1} \map \exp {-\dfrac u {m + 1} }$
We have by Exponential of Zero: 
:as $x \to 1$, $u \to 0$
We also have, by Exponential Tends to Zero and Infinity: 
:as $x \to 0$, $u \to \infty$
So: 
{{begin-eqn}}
{{eqn | l = \int_0^1 x^m \paren {\ln x}^n \rd x
      | r = \int_\infty^0 \paren {\map \exp {-\frac u {m + 1} } }^m \paren {-\frac u {m + 1} }^n \paren {-\frac 1 {m + 1} \map \exp {-\frac u {m + 1} } \rd u}
      | c = Integration by Substitution
}}
{{eqn | r = \frac 1 {m + 1} \int_0^\infty \paren {\map \exp {-\frac u {m + 1} } }^m \paren {-\frac u {m + 1} }^n \paren {\map \exp {-\frac u {m + 1} } \rd u}
      | c = Reversal of Limits of Definite Integral
}}
{{eqn | r = \frac {\paren {-1}^n} {m + 1} \int_0^\infty \map \exp {-u \paren {\frac m {m + 1} + \frac 1 {m + 1} } } \frac {u^n} {\paren {m + 1}^n} \rd u
      | c = Exponential of Sum, Power of Power
}}
{{eqn | r = \frac {\paren {-1}^n} {\paren {m + 1}^{n + 1} }  \int_0^\infty e^{-u} u^{\paren {n + 1} - 1} \rd u
}}
{{eqn | r = \frac {\paren {-1}^n \map \Gamma {n + 1} } {\paren {m + 1}^{n + 1} }
      | c = {{Defof|Gamma Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to 1 of Power of x by Power of Logarithm of x

:$\ds \int_0^1 x^m \paren {\ln x}^n \rd x = \frac {\paren {-1}^n \map \Gamma {n + 1} } {\paren {m + 1}^{n + 1} }$

Proof:
From Primitive of Power, we have: 
:$\ds \int_0^1 x^m \rd x = \frac 1 {m + 1}$
We have: 
{{begin-eqn}}
{{eqn | l = \frac {\d^n} {\d m^n} \int_0^1 x^m \rd x
      | r = \int_0^1 \frac {\partial^n} {\partial m^n} x^m \rd x
      | c = Definite Integral of Partial Derivative
}}
{{eqn | r = \int_0^1 x^m \paren {\ln x}^n \rd x
      | c = Derivative of Power of Constant
}}
{{end-eqn}}
So: 
{{begin-eqn}}
{{eqn | l = \int_0^1 x^m \paren {\ln x}^n \rd x
      | r = \map {\frac {\d^n} {\d m^n} } {\frac 1 {m + 1} } 
}}
{{eqn | r = \map {\frac {\d^{n + 1} } {\d m^{n + 1} } } {\map \ln {m + 1} } 
      | c = Derivative of Natural Logarithm
}}
{{eqn | r = \frac {\paren {-1}^n \map \Gamma {n + 1} } {\paren {m + 1}^{n + 1} }
      | c = $n$th Derivative of Natural Logarithm
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral to Infinity of Exponential of -a x by Sine of b x

:$\ds \int_0^\infty e^{-a x} \sin b x \rd x = \frac b {a^2 + b^2}$

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^\infty e^{-a x} \sin b x \rd x
	| r = \intlimits {\frac {e^{-a x} \paren {-a \sin b x - b \cos b x} } {a^2 + b^2} } 0 \infty
	| c = Primitive of $e^{a x} \sin b x$
}}
{{eqn	| r = -\lim_{x \mathop \to \infty} \paren {\frac {e^{-a x} \paren {a \sin b x + b \cos b x} } {a^2 + b^2} } + \frac {e^0 \paren {a \sin 0 + b \cos 0} } {a^2 + b^2} 
}}
{{eqn	| r = -\lim_{x \mathop \to \infty} \paren {\frac {e^{-a x} \paren {a \sin b x + b \cos b x} } {a^2 + b^2} } +\frac b {a^2 + b^2}
	| c = Exponential of Zero, Sine of Zero is Zero, Cosine of Zero is One
}}
{{end-eqn}}
Note that we have, by Linear Combination of Sine and Cosine: 
:$\ds 0 \le \size {\frac {e^{-a x} \paren {a \sin b x + b \cos b x} } {a^2 + b^2} } \le \frac {e^{-a x} \sqrt {a^2 + b^2} } {a^2 + b^2} = \frac {e^{-a x} } {\sqrt {a^2 + b^2} }$
By Exponential Tends to Zero and Infinity: 
:$\ds \lim_{x \mathop \to \infty} \paren {\frac {e^{-a x} } {\sqrt {a^2 + b^2} } } = 0$
So by the Squeeze Theorem: 
:$\ds \lim_{x \mathop \to \infty} \paren {\frac {e^{-a x} \paren {a \sin b x + b \cos b x} } {a^2 + b^2} } = 0$
So: 
:$\ds \int_0^\infty e^{-a x} \sin b x \rd x = \frac b {a^2 + b^2}$
{{qed}}
Theorem: Sum of Exponential of i k x

:$\ds \sum_{k \mathop = 0}^n \map \exp {i k x} = \paren {i \sin \frac {n x} 2 + \cos \frac {n x} 2} \frac {\map \sin {\frac {\paren {n + 1} x} 2} } {\sin \frac x 2}$

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 0}^n \map \exp {i k x} 
      | r = \frac {\map \exp {i x \paren {n + 1} } - 1} {\map \exp {i x} - 1}
      | c = Sum of Geometric Sequence
}}
{{eqn | r = \frac {\map \exp {\frac {i x \paren {n + 1} } 2} \paren {\map \exp {\frac {i x \paren {n + 1} } 2} - \map \exp {\frac {-i x \paren {n + 1} } 2} } } {\map \exp {\frac {i x} 2} \paren {\map \exp {\frac {i x} 2} - \map \exp {-\frac {i x} 2} } }
      | c = factoring $\dfrac {\map \exp {\frac {i x \paren {n + 1} } 2} } {\map \exp {\frac {i x} 2} }$
}}
{{eqn | r = \map \exp {\frac {i x n} 2} \frac {2 i \map \sin {\frac {\paren {n + 1} x} 2} } {2 i \sin \frac x 2}
      | c = {{Corollary|Exponential of Sum of Real Numbers}}, Euler's Sine Identity
}}
{{eqn | r = \paren {i \sin \frac {n x} 2 + \cos \frac {n x} 2} \frac {\map \sin {\frac {\paren {n + 1} x} 2} } {\sin \frac x 2}
      | c = Euler's Formula
}}
{{end-eqn}}
{{qed}}
Category:Exponential Function
fcuspzx2wydztd2f35p55l6oi2dr8rj
Theorem: Möbius Transformation is Bijection/Restriction to Reals

Let $a, b, c, d \in \R$ be real numbers.
Let $f: \R^* \to \R^*$ be the Möbius transformation restricted to the real numbers:
:<nowiki>$\map f x = \begin {cases} \dfrac {a x + b} {c x + d} & : x \ne -\dfrac d c \\
\infty & : x = -\dfrac d c \\
\dfrac a c & : x = \infty \\
\infty & : x = \infty \text { and } c = 0 \end {cases}$</nowiki>
Then:
:$f: \R^* \to \R^*$ is a bijection
{{iff}}:
:$a c - b d \ne 0$

Proof:
First we note that as Real Addition is Closed and Real Multiplication is Closed:
:$\Dom {\R^*} \subseteq \R^*$
{{explain|What is $\Dom {\R^*}$?}}
Recall from Möbius Transformation is Bijection that the Möbius transformation on the extended complex plane is a bijection {{iff}} $a c - b d \ne 0$.
From Restriction of Injection is Injection, if $a c - b d \ne 0$ {{iff}} $f$ is an injection.
As the inverse $f^{-1}$ of $f$ is also the restriction of a Möbius transformation, it follows that $f^{-1}$ is also an injection.
Hence the result from Injection is Bijection iff Inverse is Injection.
{{qed}}
Theorem: Extension of Extension of Mapping is Extension

Let $A, B, C, S$ be sets such that $A \subseteq B \subseteq C$.
Let $f: A \to S$, $g: B \to S$ and $h: C \to S$ be mappings such that:
:$g$ is an extension of $f$ to $B$
:$h$ is an extension of $g$ to $C$.
Then $h$ is an extension of $f$ to $C$.

Proof:
By definition of extension:
:$\forall x \in A: \map f x = \map g x$
and:
:$\forall x \in B: \map g x = \map h x$
and so:
:$\forall x \in A: \map g x = \map h x$
from which it follows that:
:$\forall x \in A: \map f x = \map h x$
{{qed}}
Theorem: Indexed Cartesian Space is Set of all Mappings

Let $I$ be an indexing set.
Let $\ds \prod_{i \mathop \in I} S$ denote the cartesian space of $S$ indexed by $I$.
Then $\ds \prod_{i \mathop \in I} S$ is the set of all mappings from $I$ to $S$, and hence the notation:
:$S^I := \ds \prod_{i \mathop \in I} S$

Proof:
Let $\family {S_i}_{i \mathop \in I}$ be an indexed family of sets.
By definition of the Cartesian product of $\family {S_i}_{i \mathop \in I}$:
:$(1): \quad \ds \prod_{i \mathop \in I} S_i := \set {f: \paren {f: I \to \bigcup_{i \mathop \in I} S_i} \land \paren {\forall i \in I: \paren {\map f i \in S_i} } }$
where $f$ denotes a mapping.
We have that that:
:$\forall i \in I: S_i = S$
From Set Union is Idempotent:
:$\ds \bigcup_{i \mathop \in I} S = S$
Hence when $S_i = S$ for all $i \in I$, $(1)$ can be written:
:$\ds \prod_{i \mathop \in I} S = \set {f: \paren {f: I \to S} \land \paren {\forall i \in I: \paren {\map f i \in S_i} } }$
which is exactly the definition of $S^I$ towards which we are aiming.
{{qed}}
Theorem: Definite Integral from 0 to 1 of Logarithm of x over One plus x

:$\ds \int_0^1 \frac {\ln x} {1 + x} \rd x = -\frac {\pi^2} {12}$

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^1 \frac {\ln x} {1 + x} \rd x
	| r = \int_0^1 \frac {\ln x} {1 - \paren {-x} } \rd x
}}
{{eqn	| r = \int_0^1 \ln x \paren {\sum_{n \mathop = 0}^\infty \paren {-x}^n} \rd x
	| c = Sum of Infinite Geometric Sequence
}}
{{eqn	| r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \int_0^1 x^n \ln x \rd x
	| c = Fubini's Theorem
}}
{{eqn	| r = \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^{n + 1} \map \Gamma 2} {\paren {n + 1}^2}
	| c = Definite Integral from $0$ to $1$ of $x^m \paren {\ln x}^n$
}}
{{eqn	| r = \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^n 1!} {n^2}
	| c = Gamma Function Extends Factorial, shifting the index
}}
{{eqn	| r = -\sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n + 1} } {n^2}
	| c = writing $-\paren {-1}^{n + 1} = \paren {-1}^{n + 2} = \paren {-1}^2 \paren {-1}^n = \paren {-1}^n$
}}
{{eqn	| r = -\frac {\pi^2} {12}
	| c = Sum of Reciprocals of Squares Alternating in Sign
}}
{{end-eqn}}
{{qed}}
Theorem: Equivalence of Definitions of Convergent Sequence in Metric Space/Definition 1 iff Definition 2

Let $M = \struct {A, d}$ be a metric space or a pseudometric space.
Let $\sequence {x_k}$ be a sequence in $A$.
{{TFAE|def = Convergent Sequence|context = Metric Space|contextview = Metric Spaces}}

Proof:
By definition of an open ball:
:$\forall n \in \N: \map d {x_n, l} < \epsilon \iff x_n \in \map {B_\epsilon} l$
The result follows.
Theorem: Equivalence of Definitions of Convergent Sequence in Metric Space/Definition 1 iff Definition 3

Let $M = \struct {A, d}$ be a metric space or a pseudometric space.
Let $\sequence {x_k}$ be a sequence in $A$.
{{TFAE|def = Convergent Sequence|context = Metric Space|contextview = Metric Spaces}}

Proof:
By definition of a convergent real sequence:
:$\ds \lim_{n \mathop \to \infty} \map d {x_n, l} = 0$
{{iff}}
:$\forall \epsilon \in \R_{>0}: \exists N \in \R_{>0}: n > N \implies \size {\map d {x_n, l} - 0} < \epsilon$ 
From Distance in Pseudometric is Non-Negative:
:$\forall x, y \in A: \map d {x, y} \ge 0$
Hence:
:$\forall n \in \N: \map d {x_n, l} = \size {\map d {x_n, l}} = \size {\map d {x_n, l} - 0}$
The result follows.
Theorem: Definite Integral from 0 to 1 of Logarithm of x over One minus x

:$\ds \int_0^1 \frac {\ln x} {1 - x} \rd x = -\frac {\pi^2} 6$

Proof:
{{begin-eqn}}
{{eqn | l = \int_0^1 \frac {\ln x} {1 - x} \rd x
      | r = \int_0^1 \ln x \paren {\sum_{n \mathop = 0}^\infty x^n} \rd x
      | c = Sum of Infinite Geometric Sequence
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {\int_0^1 x^n \ln x \rd x}
      | c = Fubini's Theorem
}}
{{eqn | r = -\sum_{n \mathop = 0}^\infty \frac {\map \Gamma 2} {\paren {n + 1}^2}
      | c = Definite Integral from $0$ to $1$ of $x^m \paren {\ln x}^n$: $n \gets 1$, $m \gets n$
}}
{{eqn | r = -\sum_{n \mathop = 1}^\infty \frac 1 {n^2}
      | c = shifting the index, Gamma Function Extends Factorial
}}
{{eqn | r = -\frac {\pi^2} 6
      | c = Basel Problem
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to 1 of Logarithm of One plus x over x

:$\ds \int_0^1 \frac {\map \ln {1 + x} } x \rd x = \frac {\pi^2} {12}$

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^1 \frac {\map \ln {1 + x} } x \rd x
	| r = \int_0^1 \frac 1 x \paren {\sum_{n \mathop = 1}^\infty \paren {-1}^{n - 1} \frac {x^n} n} \rd x
	| c = Power Series Expansion for $\map \ln {1 + x}$
}}
{{eqn	| r = \sum_{n \mathop = 1}^\infty \paren {\frac {\paren {-1}^{n - 1} } n \int_0^1 x^{n - 1} \rd x}
	| c = Power Series is Termwise Integrable within Radius of Convergence
}}
{{eqn	| r = \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} } {n^2} 
	| c = Primitive of Power
}}
{{eqn	| r = \frac {\pi^2} {12}
	| c = Sum of Reciprocals of Squares Alternating in Sign
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to 1 of Logarithm of One minus x over x

:$\ds \int_0^1 \frac {\map \ln {1 - x} } x \rd x = -\frac {\pi^2} 6$

Proof:
{{begin-eqn}}
{{eqn | l = \int_0^1 \frac {\map \ln {1 - x} } x \rd x
      | r = -\int_0^1 \frac 1 x \paren {\sum_{n \mathop = 1}^\infty \frac {x^n} n} \rd x
      | c = Power Series Expansion for $\map \ln {1 - x}$
}}
{{eqn | r = -\sum_{n \mathop = 1}^\infty \paren {\frac 1 n  \int_0^1 x^{n - 1} \rd x}
      | c = Power Series is Termwise Integrable within Radius of Convergence
}}
{{eqn | r = -\sum_{n \mathop = 1}^\infty \frac 1 {n^2}
      | c = Primitive of Power
}}
{{eqn | r = -\frac {\pi^2} 6
      | c = Basel Problem
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral to Infinity of Exponential of -a x by Cosine of b x

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

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^\infty e^{-a x} \cos b x \rd x
	| r = \intlimits {\frac {e^{-a x} \paren {-a \cos b x + b \sin b x} } {a^2 + b^2} } 0 \infty
	| c = Primitive of $e^{a x} \cos b x$
}}
{{eqn	| r = \lim_{x \mathop \to \infty} \paren {\frac {e^{-a x} \paren {-a \cos b x + b \sin b x} } {a^2 + b^2} } + \frac {e^0 \paren {a \cos 0 - b \sin 0} } {a^2 + b^2}
}}
{{eqn	| r = \lim_{x \mathop \to \infty} \paren {\frac {e^{-a x} \paren {-a \cos b x + b \sin b x} } {a^2 + b^2} } + \frac a {a^2 + b^2}
	| c = Exponential of Zero, Cosine of Zero is One, Sine of Zero is Zero
}}
{{end-eqn}}
Note that we have, by Linear Combination of Sine and Cosine: 
:$\ds 0 \le \size {\frac {e^{-a x} \paren {-a \cos b x + b \sin x} } {a^2 + b^2} } \le \frac {e^{-a x} \sqrt {a^2 + b^2} } {a^2 + b^2} = \frac {e^{-a x} } {\sqrt {a^2 + b^2} }$
By Exponential Tends to Zero and Infinity: 
:$\ds \lim_{x \mathop \to \infty} \paren {\frac {e^{-a x} } {\sqrt {a^2 + b^2} } } = 0$
So by the Squeeze Theorem: 
:$\ds \lim_{x \mathop \to \infty} \paren {\frac {e^{-a x} \paren {-a \cos b x + b \sin x} } {a^2 + b^2} } = 0$
So: 
:$\ds \int_0^\infty e^{-a x} \cos b x \rd x = \frac a {a^2 + b^2}$
{{qed}}
Theorem: Set of Sets can be Defined as Family

Let $\Bbb S$ be a set of sets.
Then $\Bbb S$ can be defined as an indexed family of sets.

Proof:
Let $S: \Bbb S \to \Bbb S$ denote the identity mapping on $\Bbb S$:
:$\forall i \in \Bbb S: S_i = i$
where we use $S_i$ to mean the image of $i$ under $S$:
:$S_i := \map S i$
Then we can consider $S$ as an indexing function from $\Bbb S$ to $\Bbb S$.
Hence in this case $\Bbb S$ is at the same time both:
:an indexing set
and:
:the set indexed by itself.
It follows that each of the sets $i \in \Bbb S$ is both:
:an index
and:
:a term $S_i$ of the family of elements of $\Bbb S$ indexed by $\Bbb S$.
Thus we would write $\Bbb S$ as:
:$\family {S_i}_{i \mathop \in \Bbb S}$
{{qed}}
Theorem: Definite Integral to Infinity of Exponential of -a x minus Exponential of -b x over x

:$\ds \int_0^\infty \frac {e^{-a x} - e^{-b x} } x \rd x = \ln \frac b a$

Proof:
Note that the integrand is of the form: 
:$\ds \int_0^\infty \frac {\map f {a x} - \map f {b x} } x \rd x$
where:
:$\map f x = e^{-x}$
We have, by Derivative of Exponential Function:
:$\map {f'} x = -e^{-x}$
which is continuous on $\R$.
We also have, by Exponential Tends to Zero and Infinity: 
:$\ds \lim_{x \mathop \to \infty} \map f x = \lim_{x \mathop \to \infty} e^{-x} = 0$
As $f$ is continuously differentiable, and $\ds \lim_{x \mathop \to \infty} \map f x$ exists and is finite, we may apply Frullani's Integral, giving: 
{{begin-eqn}}
{{eqn	| l = \int_0^\infty \frac {e^{-a x} - e^{-b x} } x \rd x
	| r = \paren {\lim_{x \mathop \to \infty} e^{-x} - e^0} \ln \frac a b
}}
{{eqn	| r = -\ln \frac a b
	| c = Exponential of Zero
}}
{{eqn	| r = \ln \frac b a
	| c = Logarithm of Reciprocal
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral to Infinity of Exponential of -a x^2

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

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^\infty e^{-a x^2} \rd x
	| r = \int_0^\infty e^{-\paren {\sqrt a x}^2} \rd x
}}
{{eqn	| r = \frac 1 {\sqrt a} \int_0^\infty e^{-t^2} \rd t
	| c = substituting $t = \sqrt a x$
}}
{{eqn	| r = \frac 1 2 \sqrt {\frac \pi a}
	| c = Integral to Infinity of $e^{-t^2}$
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to 1 of Difference of Powers of x over Logarithm of x

:$\ds \int_0^1 \frac {x^m - x^n} {\ln x} \rd x = \map \ln {\frac {m + 1} {n + 1} }$

Proof:
Let: 
:$x = e^{-u}$
We have, by Derivative of Exponential Function:
:$\dfrac {\d x} {\d u} = -e^{-u}$ 
By Exponential Tends to Zero and Infinity: 
:as $x \to 0$, $u \to \infty$
By Exponential of Zero: 
:as $x \to 1$, $u \to 0$.
So:
{{begin-eqn}}
{{eqn	| l = \int_0^1 \frac {x^m - x^n} {\ln x} \rd x
	| r = -\int_\infty^0 e^{-u} \frac {e^{-m u} - e^{-n u} } {\ln e^{-u} } \rd u
	| c = substituting $x = e^{-u}$
}}
{{eqn	| r = -\int_0^\infty \frac {e^{-\paren {m + 1} u} - e^{-\paren {n + 1} u} } u \rd u
	| c = Reversal of Limits of Definite Integral, Exponential of Sum
}}
{{eqn	| r = \int_0^\infty \frac {e^{-\paren {n + 1} u} - e^{-\paren {m + 1} u} } u \rd u
}}
{{eqn	| r = \map \ln {\frac {m + 1} {n + 1} }
	| c = Definite Integral to Infinity of $\dfrac {e^{-a x} - e^{-b x} } x$
}}
{{end-eqn}}
{{qed}}
Theorem: Union is Commutative/Family of Sets

Let $\family {S_i}_{i \mathop \in I}$ be an indexed family of sets.
Let $\ds I = \bigcup_{i \mathop \in I} S_i$ denote the union of  $\family {S_i}_{i \mathop \in I}$.
Let $J \subseteq I$ be a subset of $I$.
Then:
:$\ds \bigcup_{i \mathop \in I} S_i = \bigcup_{j \mathop \in J} S_j \cup \bigcup_{k \mathop \in \relcomp I J} S_k = \bigcup_{k \mathop \in \relcomp I J} S_k \cup \bigcup_{j \mathop \in J} S_j$
where $\relcomp I J$ denotes the complement of $J$ relative to $I$.

Proof:
We have that both $\ds \bigcup_{j \mathop \in J} S_j$ and $\ds \bigcup_{k \mathop \in \relcomp I J} S_k$ are sets.
Hence by Union is Commutative we have:
:$\bigcup_{j \mathop \in J} S_j \cup \bigcup_{k \mathop \in \relcomp I J} S_k = \bigcup_{k \mathop \in \relcomp I J} S_k \cup \bigcup_{j \mathop \in J} S_j$
It remains to be demonstrated that $\ds \bigcup_{i \mathop \in I} S_i = \bigcup_{j \mathop \in J} S_j \cup \bigcup_{k \mathop \in \relcomp I J} S_k$.
So:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \bigcup_{i \mathop \in I} S_i
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \exists i \in I: x
      | o = \in
      | r = S_i
      | c = {{Defof|Union of Family}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \exists j \in J: x
      | o = \in
      | r = S_j
      | c = {{Defof|Relative Complement}}
}}
{{eqn | lo= \lor
      | l = \exists k \in \relcomp I J: x
      | o = \in
      | r = S_k
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \bigcup_{j \mathop \in J} S_j
      | c = {{Defof|Union of Family}}
}}
{{eqn | lo= \lor
      | l = x
      | o = \in
      | r = \bigcup_{k \mathop \in \relcomp I J} S_k
      | c = {{Defof|Union of Family}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \bigcup_{j \mathop \in J} S_j \cup \bigcup_{k \mathop \in \relcomp I J} S_k
      | c = {{Defof|Set Union}}
}}
{{end-eqn}}
That is:
:$\ds x \in \bigcup_{i \mathop \in I} S_i \iff x \in \bigcup_{j \mathop \in J} S_j \cup \bigcup_{k \mathop \in \relcomp I J} S_k$
The result follows by definition of set equality.
{{qed}}
Theorem: Intersection is Commutative/Family of Sets

Let $\family {S_i}_{i \mathop \in I}$ be an indexed family of sets.
Let $\ds I = \bigcap_{i \mathop \in I} S_i$ denote the intersection of $\family {S_i}_{i \mathop \in I}$.
Let $J \subseteq I$ be a subset of $I$.
Then:
:$\ds \bigcap_{i \mathop \in I} S_i = \bigcap_{j \mathop \in J} S_j \cap \bigcap_{k \mathop \in \relcomp I J} S_k = \bigcap_{k \mathop \in \relcomp I J} S_k \cap \bigcap_{j \mathop \in J} S_j$
where $\relcomp I J$ denotes the complement of $J$ relative to $I$.

Proof:
We have that both $\ds \bigcap_{j \mathop \in J} S_j$ and $\ds \bigcap_{k \mathop \in \relcomp I J} S_k$ are sets.
Hence by Intersection is Commutative we have:
:$\ds \bigcap_{j \mathop \in J} S_j \cap \bigcap_{k \mathop \in \relcomp I J} S_k = \bigcap_{k \mathop \in \relcomp I J} S_k \cap \bigcap_{j \mathop \in J} S_j$
It remains to be demonstrated that $\ds \bigcap_{i \mathop \in I} S_i = \bigcap_{j \mathop \in J} S_j \cap \bigcap_{k \mathop \in \relcomp I J} S_k$.
So:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \bigcap_{i \mathop \in I} S_i
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall i \in I
      | l = x
      | o = \in
      | r = S_i
      | c = {{Defof|Intersection of Family}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall j \in J
      | l = x
      | o = \in
      | r = S_j
      | c = {{Defof|Relative Complement}}
}}
{{eqn | lo= \land
      | q = \forall k \in \relcomp I J
      | l = x
      | o = \in
      | r = S_k
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \bigcap_{j \mathop \in J} S_j
      | c = {{Defof|Intersection of Family}}
}}
{{eqn | lo= \land
      | l = x
      | o = \in
      | r = \bigcap_{k \mathop \in \relcomp I J} S_k
      | c = {{Defof|Intersection of Family}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \bigcap_{j \mathop \in J} S_j \cap \bigcap_{k \mathop \in \relcomp I J} S_k
      | c = {{Defof|Set Intersection}}
}}
{{end-eqn}}
That is:
:$\ds x \in \bigcap_{i \mathop \in I} S_i \iff x \in \bigcap_{j \mathop \in J} S_j \cap \bigcap_{k \mathop \in \relcomp I J} S_k$
The result follows by definition of set equality.
{{qed}}