avewright/proofwiki-math huggingface dataset:
Theorem: Definite Integral to Infinity of Reciprocal of x Squared plus a Squared

:$\ds \int_0^\infty \dfrac {\d x} {x^2 + a^2} = \frac \pi {2 a}$
for $a \ne 0$.

Proof:
Let $C_R$ be the semicircular contour of radius $R$ situated on the upper half plane, centred at the origin, traversed anti-clockwise.
Let $\Gamma_R = C_R \cup \closedint {-R} R$.
Then, by Contour Integral of Concatenation of Contours:
:$\ds \oint_{\Gamma_R} \frac {\d z} {z^2 + a^2} = \int_{C_R} \frac {\d z} {z^2 + a^2} + \int_{-R}^R \frac {\d x} {x^2 + a^2}$
we have: 
{{begin-eqn}}
{{eqn | l = \size {\int_{C_R} \frac {\d z} {z^2 + a^2} }
      | o = \le
      | r = \pi R \cdot \max_{0 \mathop \le \theta \mathop \le \pi} \size {\frac 1 {R^2 e^{2 i \theta} + a^2} }
      | c = Estimation Lemma for Contour Integrals
}}
{{eqn | r = \frac {\pi R} {R^2 + a^2}
}}
{{eqn | o = \le
      | r = \frac {\pi R} {R^2}
}}
{{eqn | r = \frac \pi R
}}
{{eqn | o = \to
      | r = 0
      | c = as $R \to \infty$
}}
{{end-eqn}}
from which:
:$\ds \lim_{R \mathop \to \infty} \oint_{\Gamma_R} \frac {\d z} {z^2 + a^2} = \lim_{R \mathop \to \infty} \int_{-R}^R \frac {\d x} {x^2 + a^2} = \int_{-\infty}^\infty \frac {\d x} {x^2 + a^2}$
The integrand is meromorphic.
So by Cauchy's Residue Theorem:
:$\ds \lim_{R \mathop \to \infty} \oint_{\Gamma_R} \frac {\d z} {z^2 + a^2} = 2 \pi i \sum \Res {\frac 1 {z^2 + a^2} } {z_0}$
where the summation runs over the poles of $\dfrac 1 {z^2 + a^2}$.
The integrand can be written as:
:$\dfrac 1 {\paren {z - a i} \paren {z + a i} }$
From this it can be observed that the integrand has only two simple poles: $z_0 = a i$ and $z_0 = -a i$.
Only the former of these lies in the contour, so:
{{begin-eqn}}
{{eqn | l = \lim_{R \mathop \to \infty} \oint_{\Gamma_R} \frac {\d z} {z^2 + a^2}
      | r = 2 \pi i \Res {\frac 1 {z^2 + a^2} } {a i}
}}
{{eqn | r = 2 \pi i \cdot \frac 1 {\map {\frac \d {\d z} } {z^2 + a^2}_{z \mathop = a i} }
      | c = Residue at Simple Pole
}}
{{eqn | r = 2 \pi i \cdot \frac 1 {2 a i}
      | c = Derivative of Power
}}
{{eqn | r = \frac \pi a
}}
{{end-eqn}}
So: 
:$\ds \int_{-\infty}^\infty \frac {\d x} {x^2 + a^2} = \frac \pi a$
From Definite Integral of Even Function:
:$\ds \int_{-\infty}^\infty \frac {\d x} {x^2 + a^2} = 2 \int_0^\infty \frac {\d x} {x^2 + a^2}$
Hence: 
:$\ds \int_0^\infty \frac {\d x} {x^2 + a^2} = \frac \pi {2 a}$
{{qed}}
Theorem: Definite Integral to Infinity of Reciprocal of 1 plus Power of x/Corollary

:$\ds \int_0^\infty \frac 1 {a^n + x^n} \rd x = \frac \pi {n a^{n - 1} } \map \csc {\frac \pi n}$

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^\infty \frac 1 {a^n + x^n} \rd x
	| r = \frac 1 {a^n} \int_0^\infty \frac 1 {1 + \paren {\frac x a}^n} \rd x
}}
{{eqn	| r = \frac 1 {a^n} \cdot \frac 1 {\frac 1 a} \int_0^\infty \frac 1 {1 + \paren {\frac x a}^n} \map \rd {\frac x a}
	| c = Primitive of Function of Constant Multiple
}}
{{eqn	| r = \frac a {a^n} \cdot \frac \pi n \map \csc {\frac \pi n}
	| c = Definite Integral to Infinity of $\dfrac 1 {1 + x^n}$
}}
{{eqn	| r = \frac \pi {n a^{n - 1} } \map \csc {\frac \pi n}
}}
{{end-eqn}}
{{qed}}
Category:Definite Integral to Infinity of Reciprocal of 1 plus Power of x
6hjbjx4orh49ud3fcyz5fr7d68er376
Theorem: Definite Integral to Infinity of Power of x over 1 + x

:$\ds \int_0^\infty \dfrac {x^{p - 1} \rd x} {1 + x} = \frac \pi {\sin \pi p}$
for $0 < p < 1$.

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^\infty \frac {x^{p - 1} \rd x} {1 + x} 
	| r = \int_0^\infty \frac 1 {p x^{p - 1} } \cdot \frac {x^{p - 1} \rd t} {1 + t^{1 / p} }
	| c = substituting $t = x^p$
}}
{{eqn	| r = \frac 1 p \int_0^\infty \frac {\rd t} {1 + t^{1 / p} }
}}
{{eqn	| r = \frac 1 p \cdot \frac \pi {\frac 1 p} \map \csc {\frac \pi {\frac 1 p} }
	| c = as $0 < p < 1$, $\dfrac 1 p > 1$, so we can apply Definite Integral to Infinity of $\dfrac 1 {1 + x^n}$
}}
{{eqn	| r = \pi \map \csc {\pi p}
}}
{{eqn	| r = \frac \pi {\sin \pi p}
	| c = {{Defof|Cosecant}}
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral to Infinity of Power of x over 1 + x

:$\ds \int_0^\infty \dfrac {x^{p - 1} \rd x} {1 + x} = \frac \pi {\sin \pi p}$
for $0 < p < 1$.

Proof:
{{ProofWanted|We can probably use Primitive of Power of x by Power of a x + b but I can see it being a long slog}}
Theorem: Definite Integral to Infinity of Power of x over Power of x plus Power of a

:$\ds \int_0^\infty \dfrac {x^m \rd x} {x^n + a^n} = \frac {\pi a^{m + 1 - n} } {n \map \sin {\paren {m + 1} \frac \pi n} }$
for $0 < m + 1 < n$.

Proof:
{{begin-eqn}}
{{eqn | l = \int_0^\infty \dfrac {x^m \rd x} {x^n + a^n}
      | r = \int_0^\infty \dfrac {x^m \rd x} {\paren {x^{m + 1} }^{\frac n {m + 1} } + \paren {a^{m + 1} }^{\frac n {m + 1} } }
}}
{{eqn | r = \frac 1 {m + 1} \int_0^\infty \dfrac 1 {u^{\frac n {m + 1} } + \paren {a^{m + 1} }^{\frac n {m + 1} } } \rd u
      | c = substituting $u = x^{m + 1}$
}}
{{eqn | r = \frac \pi {\paren {m + 1} \paren {\frac n {m + 1} \paren {a^{m + 1} }^{\frac n {m + 1} - 1} } } \map \csc {\frac {\paren {m + 1} \pi} n}
      | c = Definite Integral to Infinity of $\dfrac 1 {1 + x^n}$: Corollary
}}
{{eqn | r = \frac {\pi a^{m + 1} } {n a^{\paren {m + 1} \frac n {m + 1} } } \map \csc {\frac {\paren {m + 1} \pi} n}
}}
{{eqn | r = \frac {\pi a^{m + 1 - n} } {n \map \sin {\paren {m + 1} \frac \pi n} }
      | c = Cosecant is Reciprocal of Sine
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral to Infinity of Power of x over 1 + 2 x Cosine Beta + x Squared

:$\ds \int_0^\infty \dfrac {x^m \rd x} {1 + 2 x \cos \beta + x^2} = \frac \pi {\sin m x} \frac {\sin m \beta} {\sin \beta}$

Proof:
{{ProofWanted|write $x^2 + 2 x \cos \beta + 1 \equiv \paren {x + e^{i \beta} } \paren {x + e^{-i \beta} }$ then use partial fractions. Ugly so will do later.}}
Theorem: Definite Integral from 0 to a of Reciprocal of Root of a Squared minus x Squared

:$\ds \int_0^a \dfrac {\d x} {\sqrt {a^2 - x^2} } = \frac \pi 2$
for $a > 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \int_0^a \dfrac {\d x} {\sqrt {a^2 - x^2} }
      | r = \int_0^{\mathop \to a} \dfrac {\d x} {\sqrt {a^2 - x^2} }
      | c = as $\dfrac 1 {\sqrt {a^2 - x^2} }$ does not exist for $x = a$
}}
{{eqn | r = \lim_{\gamma \mathop \to a} \int_0^\gamma \dfrac {\d x} {\sqrt {a^2 - x^2} }
      | c = {{Defof|Improper Integral on Open Above Interval}}
}}
{{eqn | r = \lim_{\gamma \mathop \to a} \intlimits {\arcsin \frac x a} 0 \gamma
      | c = Primitive of $\dfrac 1 {\sqrt {a^2 - x^2} }$
}}
{{eqn | r = \lim_{\gamma \mathop \to a} \paren {\arcsin \frac \gamma a - \arcsin 0}
      | c = 
}}
{{eqn | r = \lim_{\gamma \mathop \to a} \arcsin \frac \gamma a
      | c = Arcsine of Zero is Zero
}}
{{eqn | r = \arcsin \frac a a
      | c = 
}}
{{eqn | r = \arcsin 1
      | c = 
}}
{{eqn | r = \frac \pi 2
      | c = Arcsine of One is Half Pi
}}
{{end-eqn}}
{{qed}}
Theorem: Universal Property of Free Abelian Group on Set

Let $S$ be a set.
Let $\struct {\Z^{\paren S}, \iota}$ be the free abelian group on $S$.
Let $\struct {G, +}$ be an abelian group.
Let $f: S \to G$ be a mapping.
Then there exists a unique group homomorphism $g : \Z^{\paren S} \to G$ with $g \circ \iota = f$:
:$\xymatrix{S \ar[d]_\iota \ar[r]^{\forall f} & G\\ \Z^{\paren S} \ar@{-->}[ru]_{\exists ! g} & }$

Proof:
For $x \in S$, the characteristic map $\phi_x$ of $x$ is defined as:
:$\map {\phi_x} s = \begin{cases} 1 & \quad \text{ if } s = x \\ 0 & \quad \text{ if } s \ne x \end{cases}$
The maps $\set {\phi_x \ : \ x \in S}$ form a basis for $\Z^{\paren S}$.
If $\phi \in \Z^{\paren S}$, then it can be expressed uniquely as a finite sum 
:$\ds \phi = \sum_i n_i \phi_{x_i}$
where $\phi$ maps each $x_i$ to $n_i \in \Z$, and maps each element of $S$ not present in this sum to $0$.
$\iota$ maps $x \in S$ to $\phi_x \in \Z^{\paren S}$.
So, in order to satisfy $g \circ \iota = f$, we must have $\map g {\phi_x} = \map f x$ for every $x \in S$. 
Since $g$ has to be a homomorphism, it must satisfy $\map g {\phi + \phi'} = \map g \phi + \map g {\phi'}$.
So, for $\phi \in \Z^{\paren S}$:
:$\ds \map g \phi = \map g {\sum_i n_i \phi_{x_i} } = \sum_i \map g {n_i \phi_{x_i} } = \sum_i n_i \map g {\phi_{x_i} } = \sum_i n_i \map f {x_i}$
Therefore, the value of $\map g \phi$ is unique, for every $\phi \in \Z^{\paren S}$.
So, the homomorphism $g$ that satisfies $g \circ \iota = f$ is unique.
{{Proofread}}
Theorem: Definite Integral from 0 to a of Root of a Squared minus x Squared

:$\ds \int_0^a \sqrt {a^2 - x^2} \rd x = \frac {\pi a^2} 4$
for $a > 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \int_0^a \sqrt {a^2 - x^2} \rd x
      | r = \intlimits {\frac {x \sqrt {a^2 - x^2} } 2 + \frac {a^2} 2 \arcsin \frac x a} 0 a
      | c = Primitive of $\sqrt {a^2 - x^2}$
}}
{{eqn | r = \paren {\frac {a \sqrt {a^2 - a^2} } 2 + \frac {a^2} 2 \arcsin \frac a a} - \paren {\frac {0 \sqrt {a^2 - x^2} } 2 + \frac {a^2} 2 \arcsin \frac 0 a}
      | c = 
}}
{{eqn | r = \frac {a^2} 2 \arcsin 1 - \frac {a^2} 2 \arcsin 0
      | c = removing vanishing terms
}}
{{eqn | r = \frac {a^2} 2 \arcsin 1
      | c = Sine of Zero is Zero
}}
{{eqn | r = \frac \pi 2 \frac {a^2} 2
      | c = Sine of Right Angle
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Definite Integral from 0 to a of Root of a Squared minus x Squared

:$\ds \int_0^a \sqrt {a^2 - x^2} \rd x = \frac {\pi a^2} 4$
for $a > 0$.

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^a \sqrt {a^2 - x^2} \rd x
	| r = \frac {a^{1 + \frac 2 2} } 2 \frac {\map \Gamma {\frac 1 2} \map \Gamma {1 + \frac 1 2} } {\map \Gamma {\frac 1 2 + \frac 1 2 + 1} } 
	| c = Definite Integral from 0 to a of $x^m \paren {a^n - x^n}^p$
}}
{{eqn	| r = \frac {a^2} 2 \frac {\map \Gamma {\frac 3 2} \map \Gamma {\frac 1 2} } {\map \Gamma 2}
}}
{{eqn	| r = \frac {a^2} {2 \times 1!} \paren {\frac 1 2} \paren {\map \Gamma {\frac 1 2} }^2 
	| c = Gamma Difference Equation, Gamma Function Extends Factorial
}}
{{eqn	| r = \frac {\pi a^2} 4
	| c = Gamma Function of One Half
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to a of x^m by (a^n - x^n)^p

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

Proof:
{{begin-eqn}}
{{eqn | l = \int_0^a x^m \paren {a^n - x^n}^p \rd x
      | r = a \int_0^1 \paren {a u}^m \paren {a^n - \paren {a u}^n}^p \rd u
      | c = substituting $x = a u$
}}
{{eqn | r = a \times a^m \times a^{n p} \int_0^1 u^m \paren {1 - u^n}^p \rd u
}}
{{eqn | r = \frac {a^{m + 1 + n p} } n \int_0^1 \frac {u^m} {u^{n - 1} } \paren {1 - t}^p \rd u
      | c = substituting $t = u^n$
}}
{{eqn | r = \frac {a^{m + 1 + n p} } n \int_0^1 t^{\frac {m - n + 1} n} \paren {1 - t}^p \rd u
}}
{{eqn | r = \frac {a^{m + 1 + n p} } n \map \Beta {\frac {m + 1} n, p + 1}
      | c = {{Defof|Beta Function|index = 1}}
}}
{{eqn | r = \frac {a^{m + 1 + n p} \, \map \Gamma {\frac {m + 1} n} \map \Gamma {p + 1} } {n \map \Gamma {\frac {m + 1} n + p + 1} }
      | c = {{Defof|Beta Function|index = 3}}
}}
{{end-eqn}}
{{qed}}
Theorem: Equivalence of Definitions of Complement of Subgroup

Let $G$ be a group with identity $e$.
Let $H$ and $K$ be subgroups.
{{TFAE|def = Complement of Subgroup}}

Proof:
=== Definition $1$ implies Definition $2$ ===
Let $G = H K$.
Then $H K$ is a group.
By Subset Product of Subgroups:
:$H K = K H$
Thus $K H = G$.
{{qed|lemma}}
Theorem: Equivalent Characterizations of Finer Equivalence Relation

Let $X$ be a set.
Let $\equiv$ and $\sim$ be equivalence relations on $X$.
{{TFAE}}
# $\equiv$ is finer than $\sim$:
#:$\forall x, y \in X : x \equiv y \implies x \sim y$
#The graph of $\equiv$ is contained in the graph of $\sim$.
#Every $\equiv$-equivalence class is contained in a $\sim$-equivalence class.
#Every $\sim$-equivalence class is saturated under $\equiv$.

Proof:
=== 1 implies 2 ===
{{begin-eqn}}
{{eqn | l = \tuple {x, y}
      | o = \in
      | r = \map \TT \equiv
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \equiv
      | r = y
      | c = {{Defof|Graph of Relation}}
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \sim
      | r = y
      | c = from $1$
}}
{{eqn | ll= \leadstoandfrom
      | l = \tuple {x, y}
      | o = \in
      | r = \map \TT \sim
      | c = {{Defof|Graph of Relation}}
}}
{{end-eqn}}
By definition of subset, $\map \TT \equiv \subseteq \map \TT \sim$.
{{qed|lemma}}
Theorem: Equivalence of Definitions of Finer Topology

Let $S$ be a set.
Let $\tau_1$ and $\tau_2$ be topologies on $S$.
{{TFAE|def = Finer Topology}}

Proof:
Let $I_S: \struct {S, \tau_1} \to \struct {S, \tau_2}$ be the identity mapping on $S$.
Then:
{{begin-eqn}}
{{eqn | l = \tau_1
      | o = \supseteq
      | r = \tau_2
      | c = {{Defof|Finer Topology|index = 1}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall U \subseteq S
      | l = U \in \tau_2
      | o = \implies
      | r = U \in \tau_1
      | c = {{Defof|Superset}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall U \subseteq S
      | l = U \in \tau_2
      | o = \implies
      | r = \map {I_S^{-1} } U \in \tau_1
      | c = as $\map {I_S^{-1} } U = U$: {{Defof|Identity Mapping}}
}}
{{end-eqn}}
$\quad \; \leadstoandfrom \: \: I_S$ is continuous, by definition of a continuous mapping, which is {{Defof|Finer Topology|index = 2}}.
{{qed}}
Category:Topology
0i0ebs4ay8j2dswrx3z5bq1tj16g23u
Theorem: Definite Integral from 0 to Infinity of x^m over (x^n + a^n)^r

:$\ds \int_0^\infty \frac {x^m \rd x} {\paren {a^n + x^n}^r} = \frac {\paren {-1}^{r - 1} \pi a^{m + 1 - n r} \, \map \Gamma {\frac {m + 1} n} } {n \sin \frac {\paren {m + 1} \pi} n \paren {r - 1}! \, \map \Gamma {\frac {m + 1} n - r + 1} }$
for:
:$0 < m + 1 < n r$
:$r + 1 - \dfrac {m + 1} n \notin \N_{>0}$
:$r \in \N_{>0}$.

Proof:
{{begin-eqn}}
{{eqn | l = u
      | r = \frac {x^n} {a^n}
      | c =
}}
{{eqn | ll= \leadsto
      | l = \d u
      | r = \frac {n x^{n - 1} } {a^n} \rd x
      | c = Power Rule for Derivatives
}}
{{eqn | l = \d u
      | r = \frac {n \paren {a \times u^{\frac 1 n} }^{n - 1} } {a^n} \rd x
      | c = substituting for $x$
}}
{{eqn | ll= \leadsto
      | l = \d x
      | r = \frac a n u^{\frac 1 n - 1} \rd u
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \int_0^\infty \frac {x^m \rd x} {\paren {a^n + x^n}^r}
      | r = \int_0^\infty \frac {\paren {a \times u^{\frac 1 n} }^m } {\paren {a^n + \paren {a \times u^{\frac 1 n} }^n}^r} \frac a n u^{\frac 1 n - 1} \rd u
      | c = Integration by Substitution
}}
{{eqn | r = \frac {a^{m + 1 - r n} } n \int_0^\infty \frac {\paren {u^{\frac 1 n} }^m} {\paren {1 + \paren {u^{\frac 1 n} }^n}^r} u^{\frac 1 n - 1} \rd u
      | c = factoring out constants
}}
{{eqn | r = \frac {a^{m + 1 - r n} } n \int_0^\infty \frac {u^{\frac {m + 1} n - 1} } {\paren {1 + u}^r} \rd u
      | c = simplifying
}}
{{eqn | r = \frac {a^{m + 1 - r n} } n \map \Beta {\frac {m + 1} n, r - \frac {m + 1} n}
      | c = Beta Function as Integral of Power of $t$ over Power of $t + 1$
}}
{{eqn | r = \frac {a^{m + 1 - r n} } n \frac {\map \Gamma {\frac {m + 1} n} \map \Gamma {r - \frac {m + 1} n} } {\map \Gamma r}
      | c = {{Defof|Beta Function|index = 3}}
}}
{{eqn | l =
      | r = \frac {\pi a^{m + 1 - r n} \map \Gamma {\frac {m + 1} n} } {n \map \Gamma r} \frac \pi {\map \sin {\pi \paren {r - \frac {m + 1 } n} } \map \Gamma {1 - \paren {r - \frac {m + 1} n} } }
      | c = Euler's Reflection Formula with restriction $r + 1 - \dfrac {m + 1} n \notin \N_{>0}$
}}
{{eqn | l =
      | r = \frac {\pi a^{m + 1 - r n} \map \Gamma {\frac {m + 1} n} } {n \map \sin {\pi \paren {r - \frac {m + 1} n} } \map \Gamma r \map \Gamma {1 - r + \frac {m + 1} n} } 
      | c = merging fractions
}}
{{eqn | l =
      | r = \frac {\pi a^{m + 1 - r n} \map \Gamma {\frac {m + 1} n} } {n \paren {-1}^r \map \sin {\pi \paren {-\frac {m + 1} n} } \paren {r - 1}! \map \Gamma {1 - r + \frac {m + 1} n} } 
      | c = Sine of Angle plus Integer Multiple of Pi and Gamma Function Extends Factorial with restriction $r \in \N_{>0}$
}}
{{eqn | l =
      | r = \frac {\paren {-1}^{r - 1} \pi a^{m + 1 - r n} \map \Gamma {\frac {m + 1} n} } {n \map \sin {\frac {\paren {m + 1} \pi} n} \paren {r - 1}! \map \Gamma {1 - r + \frac {m + 1} n} } 
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to Pi of Sine of m x by Sine of n x

Let $m, n \in \Z$ be integers.
Then:
:$\ds \int_0^\pi \sin m x \sin n x \rd x = \begin{cases} 0 & : m \ne n \\ \dfrac \pi 2 & : m = n \end{cases}$
That is:
:$\ds \int_0^\pi \sin m x \sin n x \rd x = \dfrac \pi 2 \delta_{m n}$
where $\delta_{m n}$ is the Kronecker delta.

Proof:
Let $m \ne n$.
{{begin-eqn}}
{{eqn | l = \int \sin m x \sin n x \rd x
      | r = \frac {\sin \paren {m - n} x} {2 \paren {m - n} } - \frac {\sin \paren {m + n} x} {2 \paren {m + n} } + C
      | c = Primitive of $\sin m x \sin n x$
}}
{{eqn | ll= \leadsto
      | l = \int_0^\pi \sin m x \sin n x \rd x
      | r = \intlimits {\frac {\sin \paren {m - n} x} {2 \paren {m - n} } - \frac {\sin \paren {m + n} x} {2 \paren {m + n} } } 0 \pi
      | c = 
}}
{{eqn | r = \paren {\frac {\sin \paren {m - n} \pi} {2 \paren {m - n} } - \frac {\sin \paren {m + n} \pi} {2 \paren {m + n} } }
      | c = 
}}
{{eqn | o = 
      | ro= -
      | r = \paren {\frac {\sin 0} {2 \paren {m - n} } - \frac {\sin 0} {2 \paren {m + n} } }
      | c = 
}}
{{eqn | r = \frac {\sin \paren {m - n} \pi} {2 \paren {m - n} } - \frac {\sin \paren {m + n} \pi} {2 \paren {m + n} }
      | c = Sine of Zero is Zero
}}
{{eqn | r = 0
      | c = Sine of Multiple of Pi
}}
{{end-eqn}}
{{qed|lemma}}
When $m = n$ we have:
{{begin-eqn}}
{{eqn | l = \int \sin m x \sin m x \rd x
      | r = \int \sin^2 m x \rd x
      | c = 
}}
{{eqn | r = \frac x 2 - \frac {\sin 2 m x} {4 m} + C
      | c = Primitive of $\sin^2 m x$
}}
{{eqn | ll= \leadsto
      | l = \int_0^\pi \sin m x \sin m x \rd x
      | r = \intlimits {\frac x 2 - \frac {\sin 2 m x} {4 m} } 0 \pi
      | c = 
}}
{{eqn | r = \paren {\frac \pi 2 - \frac {\sin \paren {2 m \pi} } {4 m} } - \paren {\frac 0 2 - \frac {\sin 0} {4 m} }
      | c = 
}}
{{eqn | r = \frac \pi 2 - \frac {\sin \paren {2 m \pi} } {4 m}
      | c = Sine of Zero is Zero
}}
{{eqn | r = \frac \pi 2
      | c = Sine of Multiple of Pi
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to Pi of Cosine of m x by Cosine of n x

Let $m, n \in \Z$ be integers.
Then:
:$\ds \int_0^\pi \cos m x \cos n x \rd x = \begin {cases} 0 & : m \ne n \\ \dfrac \pi 2 & : m = n \end {cases}$
That is:
:$\ds \int_0^\pi \cos m x \cos n x \rd x = \dfrac \pi 2 \delta_{m n}$
where $\delta_{m n}$ is the Kronecker delta.

Proof:
Let $m \ne n$.
{{begin-eqn}}
{{eqn | l = \int \cos m x \cos n x \rd x
      | r = \frac {\map \sin {\paren {m - n} x} } {2 \paren {m - n} } + \frac {\map \sin {\paren {m + n} x} } {2 \paren {m + n} } + C
      | c = Primitive of $\cos m x \cos n x$
}}
{{eqn | ll= \leadsto
      | l = \int_0^\pi \cos m x \cos n x \rd x
      | r = \intlimits {\frac {\map \sin {\paren {m - n} x} } {2 \paren {m - n} } + \frac {\map \sin {\paren {m + n} x} } {2 \paren {m + n} } } 0 \pi
      | c = 
}}
{{eqn | r = \paren {\frac {\map \sin {\paren {m - n} \pi} } {2 \paren {m - n} } + \frac {\map \sin {\paren {m + n} \pi} } {2 \paren {m + n} } }
      | c = 
}}
{{eqn | o = 
      | ro= -
      | r = \paren {\frac {\sin 0} {2 \paren {m - n} } + \frac {\sin 0} {2 \paren {m + n} } }
      | c = 
}}
{{eqn | r = \frac {\map \sin {\paren {m - n} \pi} } {2 \paren {m - n} } + \frac {\map \sin {\paren {m + n} \pi} } {2 \paren {m + n} }
      | c = Sine of Zero is Zero
}}
{{eqn | r = 0
      | c = Sine of Multiple of Pi
}}
{{end-eqn}}
{{qed|lemma}}
When $m = n$ we have:
{{begin-eqn}}
{{eqn | l = \int \cos m x \cos m x \rd x
      | r = \int \cos^2 m x \rd x
      | c = 
}}
{{eqn | r = \frac x 2 + \frac {\sin 2 m x} {4 m} + C
      | c = Primitive of $\cos^2 m x$
}}
{{eqn | ll= \leadsto
      | l = \int_0^\pi \cos m x \cos m x \rd x
      | r = \intlimits {\frac x 2 + \frac {\sin 2 m x} {4 m} } 0 \pi
      | c = 
}}
{{eqn | r = \paren {\frac \pi 2 + \frac {\map \sin {2 m \pi} } {4 m} } - \paren {\frac 0 2 + \frac {\sin 0} {4 m} }
      | c = 
}}
{{eqn | r = \frac \pi 2 + \frac {\map \sin {2 m \pi} } {4 m}
      | c = Sine of Zero is Zero
}}
{{eqn | r = \frac \pi 2
      | c = Sine of Multiple of Pi
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to Half Pi of Square of Sine x

:$\ds \int_0^{\frac \pi 2} \sin^2 x \rd x = \frac \pi 4$

Proof:
{{begin-eqn}}
{{eqn | l = \int \sin^2 x \rd x
      | r = \frac x 2 - \frac {\sin 2 x} 4 + C
      | c = Primitive of $\sin^2 x$
}}
{{eqn | ll= \leadsto
      | l = \int_0^{\frac \pi 2} \sin^2 x \rd x
      | r = \intlimits {\frac x 2 - \frac {\sin 2 x} 4} 0 {\frac \pi 2}
      | c = 
}}
{{eqn | r = \paren {\frac \pi 4 - \frac {\sin \pi} 4} - \paren {\frac 0 2 - \frac {\sin 0} 4}
      | c = 
}}
{{eqn | r = \frac \pi 4
      | c = Sine of Multiple of Pi and simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to Half Pi of Square of Sine x

:$\ds \int_0^{\frac \pi 2} \sin^2 x \rd x = \frac \pi 4$

Proof:
We have: 
{{begin-eqn}}
{{eqn	| l = \int_0^{\frac \pi 2} \sin^2 x \rd x
	| r = \int_0^{\frac \pi 2} \sin^2 \paren {\frac \pi 2 - x} \rd x
	| c = Integral between Limits is Independent of Direction
}}
{{eqn	| r = \int_0^{\frac \pi 2} \cos^2 x \rd x
	| c = Sine of Complement equals Cosine
}}
{{end-eqn}}
So:
{{begin-eqn}}
{{eqn	| l = 2 \int_0^{\frac \pi 2} \sin^2 x \rd x
	| r = \int_0^{\frac \pi 2} \paren {\sin^2 x + \cos^2 x} \rd x
}}
{{eqn	| r = \int_0^{\frac \pi 2} \rd x
	| c = Sum of Squares of Sine and Cosine
}}
{{eqn	| r = \frac \pi 2
	| c = Primitive of Constant
}}
{{end-eqn}}
giving:
:$\ds \int_0^{\frac \pi 2} \sin^2 x \rd x = \frac \pi 4$
{{qed}}
Theorem: Definite Integral from 0 to Half Pi of Square of Cosine x

:$\ds \int_0^{\frac \pi 2} \cos^2 x \rd x = \frac \pi 4$

Proof:
{{begin-eqn}}
{{eqn | l = \int \cos^2 x \rd x
      | r = \frac x 2 + \frac {\sin 2 x} 4 + C
      | c = Primitive of $\cos^2 x$
}}
{{eqn | ll= \leadsto
      | l = \int_0^{\frac \pi 2} \cos^2 x \rd x
      | r = \intlimits {\frac x 2 + \frac {\sin 2 x} 4} 0 {\frac \pi 2}
      | c = 
}}
{{eqn | r = \paren {\frac \pi 4 + \frac {\sin \pi} 4} - \paren {\frac 0 2 + \frac {\sin 0} 4}
      | c = 
}}
{{eqn | r = \frac \pi 4
      | c = Sine of Multiple of Pi and simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to Half Pi of Square of Cosine x

:$\ds \int_0^{\frac \pi 2} \cos^2 x \rd x = \frac \pi 4$

Proof:
We have: 
{{begin-eqn}}
{{eqn	| l = \int_0^{\frac \pi 2} \cos^2 x \rd x
	| r = \int_0^{\frac \pi 2} \map {\cos^2} {\frac \pi 2 - x} \rd x
	| c = Integral between Limits is Independent of Direction
}}
{{eqn	| r = \int_0^{\frac \pi 2} \sin^2 x \rd x
	| c = Cosine of Complement equals Sine
}}
{{end-eqn}}
So:
{{begin-eqn}}
{{eqn	| l = 2 \int_0^{\frac \pi 2} \cos^2 x \rd x
	| r = \int_0^{\frac \pi 2} \paren {\sin^2 x + \cos^2 x} \rd x
}}
{{eqn	| r = \int_0^{\frac \pi 2} \rd x
	| c = Sum of Squares of Sine and Cosine
}}
{{eqn	| r = \frac \pi 2
	| c = Primitive of Constant
}}
{{end-eqn}}
giving:
:$\ds \int_0^{\frac \pi 2} \cos^2 x \rd x = \frac \pi 4$
{{qed}}