avewright/proofwiki-math huggingface dataset:
Theorem: Deduction Theorem

Let $\mathscr H$ be instance 1 of a Hilbert proof system.
Then the deduction rule:
::$\dfrac{U,\mathbf A \vdash \mathbf B}{U \vdash \mathbf A \implies \mathbf B}$
is a derived rule for $\mathscr H$.

Proof:
For any proof of $U, \mathbf A \vdash \mathbf B$, we indicate how to transform it into a proof of $U \vdash \mathbf A \implies \mathbf B$ without using the deduction rule.
This is done by applying the Second Principle of Mathematical Induction to the length $n$ of the proof of $U,\mathbf A \vdash \mathbf B$.
If $n = 1$, then one of the following must occur:
* $\mathbf B \in U$
* $\mathbf B = \mathbf A$
* $\mathbf B$ is an axiom or a theorem of $\mathscr H$
In the first case, obviously $U \vdash \mathbf B$.
By '''Axiom 1''', $U \vdash \mathbf B \implies \paren {\mathbf A \implies \mathbf B}$.
By Modus Ponens, $U \vdash \mathbf A \implies \mathbf B$.
In the second case, $U \vdash \mathbf A \implies \mathbf A$ by the Law of Identity.
Finally, in the third case, we have $U \vdash \mathbf B$.
As in the first case, we conclude $U \vdash \mathbf A \implies \mathbf B$.
If $n > 1$, the only other option for arriving at $U, \mathbf A \vdash \mathbf B$ is through Modus Ponens.
That is to say, two earlier lines of the proof contain:
:$U, \mathbf A \vdash \mathbf C$
:$U, \mathbf A \vdash \mathbf C \implies \mathbf B$
for some WFF $\mathbf C$.
But then these sequents have shorter proofs.
Hence, they satisfy the induction hypothesis.
Thus, we may infer:
:$U \vdash \mathbf A \implies \mathbf C$
:$U \vdash \mathbf A \implies \paren {\mathbf C \implies \mathbf B}$
This allows us to give the following proof of $U \vdash \mathbf A \implies \mathbf B$:
{{BeginTableau|U \vdash \mathbf A \implies \mathbf B|nohead = 1}}
{{TableauLine | n = 1
  | f = U \vdash \mathbf A \implies \mathbf C
  | rtxt = Hypothesis
}}
{{TableauLine | n = 2
  | f = U \vdash \mathbf A \implies \paren {\mathbf C \implies \mathbf B}
  | rtxt = Hypothesis
}}
{{TableauLine | n = 3
  | f = U \vdash \paren {\mathbf A \implies \paren {\mathbf C \implies \mathbf B} } \implies \paren {\paren {\mathbf A \implies \mathbf C} \implies \paren {\mathbf A \implies \mathbf B} }
  | rtxt = Axiom 2
}}
{{ModusPonens | 4 || U \vdash \paren {\mathbf A \implies \mathbf C} \implies \paren {\mathbf A \implies \mathbf B} | 2 | 3}}
{{ModusPonens | 5 || U \vdash \mathbf A \implies \mathbf B | 1 | 4}}
{{EndTableau}}
The result follows by the Second Principle of Mathematical Induction.
{{qed}}
Theorem: Soundness Theorem for Hilbert Proof System

Let $\mathscr H$ be instance 1 of a Hilbert proof system.
Let $\mathrm{BI}$ be the formal semantics of boolean interpretations.
Then $\mathscr H$ is a sound proof system for $\mathrm{BI}$:
:Every $\mathscr H$-theorem is a tautology.

Proof:
Recall the axioms of $\mathscr H$:
{{begin-axiom}}
{{axiom | lc = '''Axiom $1$:'''
        | m  = \mathbf A \implies \paren {\mathbf B \implies \mathbf A}
}}
{{axiom | lc = '''Axiom $2$:'''
        | m  = \paren {\mathbf A \implies \paren {\mathbf B \implies \mathbf C} } \implies \paren {\paren {\mathbf A \implies \mathbf B} \implies \paren {\mathbf A \implies \mathbf C} }
}}
{{axiom | lc = '''Axiom $3$:'''
        | m  = \paren {\neg \mathbf B \implies \neg \mathbf A} \implies \paren {\mathbf A \implies \mathbf B}
}}
{{end-axiom}}
That these are tautologies is shown on, respectively:
:True Statement is implied by Every Statement
:Self-Distributive Law for Conditional
{{WIP|See Talk:Self-Distributive Law for Conditional for Lord_Farin's take on this}}
:Rule of Transposition
That Modus Ponens infers tautologies from tautologies is shown on:
:Modus Ponendo Ponens
Since:
:All axioms of $\mathscr H$ are tautologies;
:All rules of inference of $\mathscr H$ preserve tautologies
it is guaranteed that every formal proof in $\mathscr H$ results in a tautology.
That is, all $\mathscr H$-theorems are tautologies.
{{qed}}
Theorem: Equivalence of Definitions of Dominate (Set Theory)

Let $S, T$ be sets.
{{TFAE|def = Dominate (Set Theory)|view = Dominate|context = Set Theory}}

Proof:
=== Definition 1 implies Definition 2 ===
Let $f: S \to T$ be an injection.
By Injection to Image is Bijection, $f$ is a bijection from $S$ to the image of $f$.
{{qed|lemma}}
Theorem: Immediate Successor under Total Ordering is Unique

Let $\preceq$ be a total ordering.
Let $b$ be an immediate successor to $a$.
Then $b$ is unique.
That is, if $b$ and $b'$ are both immediate successor to $a$, then $b = b'$.

Proof:
Let $b$ and $b'$ both be immediate successors to $a$.
We have that $\preceq$ is a total ordering.
{{WLOG}}:
:$b \preceq b'$
By virtue of $b'$ being a immediate successor of $a$:
:$\neg \exists c \in S: a \prec c \prec b'$
However, since $b$ is also an immediate successor:
:$a \prec b$
Hence, it cannot be the case that $b \prec b'$.
Since $b \preceq b'$, it follows that $b = b'$.
Hence the result.
{{qed}}
Theorem: Immediate Predecessor under Total Ordering is Unique

Let $\preceq$ be a total ordering.
Let $a$ be an immediate predecessor to $b$.
Then $a$ is unique.
That is, if $a$ and $a'$ are both immediate predecessors to $b$, then $a = a'$.

Proof:
Let $a$ and $a'$ both be immediate predecessors of $b$.
We have that $\preceq$ is a total ordering.
{{WLOG}}, suppose:
:$a \preceq a'$
By virtue of $a$ being a immediate predecessor of $b$:
:$\neg \exists c \in S: a \prec c \prec b$
However, since $a'$ is also an immediate predecessor:
:$a' \prec b$
Hence, it cannot be the case that $a \prec a'$.
Since $a \preceq a'$, it follows that $a = a'$.
Hence the result.
{{qed}}
Theorem: Equivalence of Definitions of Complex Inverse Tangent Function

{{TFAE|def = Complex Inverse Tangent}}
Let $S$ be the subset of the complex plane:
:$S = \C \setminus \set {0 + i, 0 - i}$

Proof:
The proof strategy is to how that for all $z \in \C$:
:$\set {w \in \C: \tan w = z} = \set {\dfrac 1 {2 i} \map \ln {\dfrac {i - z} {i + z} } + k \pi: k \in \Z}$
Note that when $z = 0 + i$:
{{begin-eqn}}
{{eqn | l = i - z
      | r = 0 + 0 i
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {i - z} {i + z}
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \ln {\dfrac {i - z} {i + z} }
      | o = 
      | r = \text {is undefined}
      | c = 
}}
{{end-eqn}}
Similarly, when $z = 0 - i$:
{{begin-eqn}}
{{eqn | l = i + z
      | r = 0 + 0 i
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {i - z} {i + z}
      | o = 
      | r = \text {is undefined}
      | c = 
}}
{{end-eqn}}
Thus let $z \in \C \setminus \set {0 + i, 0 - i}$.
Theorem: Equivalence of Definitions of Complex Inverse Cotangent Function

{{TFAE|def = Complex Inverse Cotangent}}
Let $S$ be the subset of the complex plane:
:$S = \C \setminus \set {0 + i, 0 - i}$

Proof:
The proof strategy is to how that for all $z \in S$:
:$\set {w \in \C: \cot w = z} = \set {\dfrac 1 {2 i} \map \ln {\dfrac {z + i} {z - i} } + k \pi: k \in \Z}$
Note that when $z = 0 - i$:
{{begin-eqn}}
{{eqn | l = z + i
      | r = 0 + 0 i
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {z + i} {z - i}
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \ln {\dfrac {z + i} {z - i} }
      | o = 
      | r = \text {is undefined}
      | c = 
}}
{{end-eqn}}
Similarly, when $z = 0 + i$:
{{begin-eqn}}
{{eqn | l = z - i
      | r = 0 + 0 i
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {z + i} {z - i}
      | o = 
      | r = \text {is undefined}
      | c = 
}}
{{end-eqn}}
Thus let $z \in \C \setminus \set {0 + i, 0 - i}$.
Theorem: Equivalence of Definitions of Complex Inverse Hyperbolic Tangent

{{TFAE|def = Complex Inverse Hyperbolic Tangent}}
Let $S$ be the subset of the complex plane:
:$S = \C \setminus \set {-1 + 0 i, 1 + 0 i}$

Proof:
The proof strategy is to how that for all $z \in S$:
:$\set {w \in \C: z = \tanh w} = \set {\dfrac 1 2 \map \ln {\dfrac {1 + z} {1 - z} } + k \pi i: k \in \Z}$
Note that when $z = -1 + 0 i$:
{{begin-eqn}}
{{eqn | l = 1 + z
      | r = 0 + 0 i
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {1 + z} {1 - z}
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \ln {\dfrac {1 + z} {1 - z} }
      | o = 
      | r = \text {is undefined}
      | c = 
}}
{{end-eqn}}
Similarly, when $z = 1 + 0 i$:
{{begin-eqn}}
{{eqn | l = 1 - z
      | r = 0 + 0 i
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {1 + z} {1 - z}
      | o = 
      | r = \text {is undefined}
      | c = 
}}
{{end-eqn}}
Thus let $z \in \C \setminus \set {-1 + 0 i, 1 + 0 i}$.
Theorem: Equivalence of Definitions of Complex Inverse Hyperbolic Cotangent

{{TFAE|def = Complex Inverse Hyperbolic Cotangent}}
Let $S$ be the subset of the complex plane:
:$S = \C \setminus \set {-1 + 0 i, 1 + 0 i}$

Proof:
The proof strategy is to how that for all $z \in S$:
:$\set {w \in \C: z = \coth w} = \set {\dfrac 1 2 \map \ln {\dfrac {z + 1} {z - 1} } + k \pi i: k \in \Z}$
Note that when $z = -1 + 0 i$:
{{begin-eqn}}
{{eqn | l = z + 1
      | r = 0 + 0 i
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {z + 1} {z - 1}
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \ln {\dfrac {z + 1} {z - 1} }
      | o = 
      | r = \text {is undefined}
      | c = 
}}
{{end-eqn}}
Similarly, when $z = 1 + 0 i$:
{{begin-eqn}}
{{eqn | l = z - 1
      | r = 0 + 0 i
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {z + 1} {z - 1}
      | o = 
      | r = \text {is undefined}
      | c = 
}}
{{end-eqn}}
Thus let $z \in \C \setminus \set {-1 + 0 i, 1 + 0 i}$.
Theorem: Natural Numbers form Inductive Set

Let $\N$ denote the natural numbers as subset of the real numbers $\R$.
Then $\N$ is an inductive set.

Proof:
By definition of the natural numbers:
:$\N = \ds \bigcap \II$
where $\II$ is the collection of all inductive sets.
Suppose that $n \in \N$.
Then by definition of intersection:
:$\forall I \in \II: n \in I$
Because all these $I$ are inductive:
:$\forall I \in \II: n + 1 \in I$
Again by definition of intersection:
:$n + 1 \in \N$
{{qed}}
Theorem: Natural Numbers form Inductive Set

Let $\N$ denote the natural numbers as subset of the real numbers $\R$.
Then $\N$ is an inductive set.

Proof:
By the given definition of the natural numbers:
:$\N = \bigcap \II$
where $\II$ is the collection of all inductive sets.
The result is a direct application of Intersection of Inductive Set as Subset of Real Numbers is Inductive Set.
{{qed}}
Theorem: Square Root of Complex Number in Cartesian Form

Let $z \in \C$ be a complex number.
Let $z = x + i y$ where $x, y \in \R$ are real numbers.
Let $z$ not be wholly real, that is, such that $y \ne 0$.
Then the square root of $z$ is given by:
:$z^{1/2} = \pm \paren {a + i b}$
where:
{{begin-eqn}}
{{eqn | l = a
      | r = \sqrt {\frac {x + \sqrt {x^2 + y^2} } 2}
      | c = 
}}
{{eqn | l = b
      | r = \frac y {\cmod y} \sqrt {\frac {-x + \sqrt {x^2 + y^2} } 2}
      | c = 
}}
{{end-eqn}}

Proof:
We have that:
:$-15 - 8 i = 17 \map \cis {\theta + 2 k \pi}$
where:
:$\cos \theta = -\dfrac {15} {17}$
:$\sin \theta = -\dfrac 8 {17}$
Then the square roots of $-15 - 8 i$ are:
{{begin-eqn}}
{{eqn | n = 1
      | l = z_1
      | r = \sqrt {17} \cis \dfrac \theta 2
      | c = 
}}
{{eqn | n = 2
      | l = z_2
      | r = \sqrt {17} \, \map \cis {\dfrac \theta 2 + \pi}
      | c = 
}}
{{eqn | r = -\sqrt {17} \cis \dfrac \theta 2
      | c = 
}}
{{end-eqn}}
We have that:
{{begin-eqn}}
{{eqn | l = \cos \dfrac \theta 2
      | r = \pm \sqrt {\dfrac {1 + \cos \theta} 2}
      | c = 
}}
{{eqn | r = \pm \sqrt {\dfrac {1 - 15 / 17} 2}
      | c = 
}}
{{eqn | r = \pm \dfrac 1 {\sqrt {17} }
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \sin \dfrac \theta 2
      | r = \pm \sqrt {\dfrac {1 - \cos \theta} 2}
      | c = 
}}
{{eqn | r = \pm \sqrt {\dfrac {1 + 15 / 17} 2}
      | c = 
}}
{{eqn | r = \pm \dfrac 4 {\sqrt {17} }
      | c = 
}}
{{end-eqn}}
As $\theta$ is in the third quadrant, $\dfrac \theta 2$ is in the second quadrant.
Hence:
{{begin-eqn}}
{{eqn | l = \cos \dfrac \theta 2
      | r = -\dfrac 1 {\sqrt {17} }
      | c = 
}}
{{eqn | l = \sin \dfrac \theta 2
      | r = \dfrac 4 {\sqrt {17} }
      | c = 
}}
{{end-eqn}}
Hence from $(1)$ and $(2)$:
{{begin-eqn}}
{{eqn | l = z_1
      | r = -1 + 4 i
      | c = 
}}
{{eqn | l = z_2
      | r = 1 - 4 i
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Zero is Identity in Naturally Ordered Semigroup

Let $\struct {S, \circ, \preceq}$ be a naturally ordered semigroup.
Let $0$ be the zero of $\struct {S, \circ, \preceq}$.
Then $0$ is the identity for $\circ$.
That is:
:$\forall n \in S: n \circ 0 = n = 0 \circ n$

Proof:
By definition of an ordering:
:$0 \preceq 0$
Thus from {{NOSAxiom|3}}:
:$\exists p \in S: 0 \circ p = 0$
By the definition of zero:
:$0 \preceq 0 \circ 0$ and $0 \preceq p$
Thus since $\preceq$ is compatible with $\circ$:
:$0 \circ 0 \preceq 0 \circ p = 0$
Thus:
:$0 \circ 0 \preceq 0$ and $0 \preceq 0 \circ 0$ 
Hence, as $\preceq$ is antisymmetric, it follows that:
:$0 \circ 0 = 0$
Because $\struct {S, \circ, \preceq}$ is a semigroup, $\circ$ is associative. 
So:
:$\forall n \in S: \paren {n \circ 0} \circ 0 = n \circ \paren {0 \circ 0} = n \circ 0$
Thus from {{NOSAxiom|2}}:
:$\forall n \in S: n \circ 0 = n$
Similarly:
:$\forall n \in S: 0 \circ \paren {0 \circ n} = \paren {0 \circ 0} \circ n = 0 \circ n$
meaning:
:$\forall n \in S: 0 \circ n = n$
Thus:
:$\forall n \in S: n \circ 0 = n = 0 \circ n$
and so $0$ is the identity for $\circ$.
{{Qed}}
Theorem: Reduction Formula for Integral of Power of Sine

Let $n \in \Z_{> 0}$ be a (strictly) positive integer.
Let:
:$I_n := \ds \int \sin^n x \rd x$
Then:
:$I_n = \dfrac {n - 1} n I_{n - 2} - \dfrac {\sin^{n - 1} x \cos x} n$
is a reduction formula for $\ds \int \sin^n x \rd x$.

Proof:
Let $n \ge 2$.
Let:
:$\ds I_n := \int \sin^n x \rd x$
Then:
{{begin-eqn}}
{{eqn | l = I_n
      | r = \int \sin^n x \rd x
      | c = 
}}
{{eqn | r = \int \sin^{n - 1} x \sin x \rd x
      | c = 
}}
{{eqn | r = \int \sin^{n - 1} x \map \rd {-\cos x}
      | c = Derivative of Cosine Function
}}
{{eqn | r = - \sin^{n - 1} x \cos x - \int \paren {-\cos x} \map \rd {\sin^{n - 1} x}
      | c = Integration by Parts
}}
{{eqn | r = - \sin^{n - 1} x \cos x - \int \paren {-\cos x} \paren {n - 1} \sin^{n - 2} x \cos x \rd x
      | c = Derivative of Power and Chain Rule for Derivatives
}}
{{eqn | r = - \sin^{n - 1} x \cos x + \paren {n - 1} \int \sin^{n - 2} x \cos^2 x \rd x
      | c = Linear Combination of Primitives and rearranging
}}
{{eqn | r = - \sin^{n - 1} x \cos x + \paren {n - 1} \int \sin^{n - 2} x \paren {1 - \sin^2 x} \rd x
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = - \sin^{n - 1} x \cos x + \paren {n - 1} \int \sin^{n - 2} x \rd x - \paren {n - 1} \int \sin^n x \rd x
      | c = 
}}
{{eqn | r = - \sin^{n - 1} x \cos x + \paren {n - 1} I_{n - 2} - \paren {n - 1} I_n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = n I_n
      | r = - \sin^{n - 1} x \cos x + \paren {n - 1} I_{n - 2}
      | c = adding $\paren {n - 1} I_n$ to both sides
}}
{{eqn | ll= \leadsto
      | l = I_n
      | r = \dfrac {n - 1} n I_{n - 2} - \dfrac {\sin^{n - 1} x \cos x} n
      | c = dividing by $n$ and rearranging
}}
{{end-eqn}}
thus demonstrating the identity for all $n \ge 2$.
When $n = 1$ this degenerates to:
{{begin-eqn}}
{{eqn | l = \int \sin x \rd x
      | r = \dfrac 0 1 \int \frac 1 {\sin x} \rd x - \dfrac {\sin^0 x \cos x} 1
      | c = 
}}
{{eqn | r = 0 - 1 \cdot \cos x
      | c = 
}}
{{eqn | r = -\cos x
      | c =
}}
{{end-eqn}}
From Primitive of Sine Function this shows that the identity still holds for $n = 1$.
{{qed}}
Theorem: Reduction Formula for Integral of Power of Sine

Let $n \in \Z_{> 0}$ be a (strictly) positive integer.
Let:
:$I_n := \ds \int \sin^n x \rd x$
Then:
:$I_n = \dfrac {n - 1} n I_{n - 2} - \dfrac {\sin^{n - 1} x \cos x} n$
is a reduction formula for $\ds \int \sin^n x \rd x$.

Proof:
With a view to expressing the problem in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = \sin^{n - 1} x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \paren {n - 1} \sin ^{n - 2} x \cos x
      | c = Chain Rule for Derivatives, Derivative of Sine Function, Derivative of Power
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = \sin x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = -\cos x
      | c = Primitive of Sine Function
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \sin^n x \rd x
      | r = \int \sin^{n - 1} x \sin x \rd x
      | c = 
}}
{{eqn | r = \sin^{n - 1} x \paren {-\cos x} - \int \paren {-\cos x} \paren {\paren {n - 1} \sin^{n - 2} x \cos x} \rd x
      | c = Integration by Parts
}}
{{eqn | r = \int \paren {n - 1} \sin^{n - 2} x \cos^2 x \rd x - \sin^{n - 1} x \cos x
      | c = rearranging
}}
{{eqn | r = \int \paren {n - 1} \sin^{n - 2} x \paren {1 - \sin^2 x} \rd x - \sin^{n - 1} x \cos x
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \paren {n - 1} \int \sin^{n - 2} x \rd x - \paren {n - 1} \int \sin^n x \rd x - \sin^{n - 1} x \cos x
      | c = Linear Combination of Primitives
}}
{{eqn | ll= \leadsto
      | l = n \int \sin^n x \rd x
      | r = \paren {n - 1} \int \sin^{n - 2} x \rd x - \sin^{n - 1} x \cos x
      | c = rearranging
}}
{{eqn | ll= \leadsto
      | l = \int \sin^n x \rd x
      | r = \dfrac {n - 1} n \int \sin^{n - 2} x \rd x - \dfrac {\sin^{n - 1} x \cos x} n
      | c = dividing both sides by $n$
}}
{{end-eqn}}
{{qed}}
Theorem: Reduction Formula for Definite Integral of Power of Sine

Let $n \in \Z_{> 0}$ be a positive integer.
Let $I_n$ be defined as:
:$\ds I_n = \int_0^{\frac \pi 2} \sin^n x \rd x$
Then $\sequence {I_n}$ is a decreasing sequence of real numbers which satisfies:
:$n I_n = \paren {n - 1} I_{n - 2}$
Thus:
:$I_n = \dfrac {n - 1} n  I_{n - 2}$
is a reduction formula for $I_n$.

Proof:
From Shape of Sine Function:
:$\forall x \in \closedint 0 {\dfrac \pi 2}: 0 \le \sin x \le 1$
and so on the same interval:
:$0 \le \sin^{n + 1} x \le \sin^n x$
therefore:
:$\forall n \in \N: 0 < I_{n + 1} < I_n$
From Reduction Formula for Integral of Power of Sine:
:$\ds \int \sin^n x \rd x = \dfrac {n - 1} n \int \sin^{n - 2} x \rd x - \dfrac {\sin^{n - 1} x \cos x} n$
Thus:
{{begin-eqn}}
{{eqn | l = I_n
      | r = \int_0^{\frac \pi 2} \sin^n x \rd x
      | c = 
}}
{{eqn | r = \dfrac {n - 1} n \int_0^{\frac \pi 2} \sin^{n - 2} x \rd x - \intlimits {\dfrac {\sin^{n - 1} x \cos x} n} 0 {\pi / 2}
      | c = 
}}
{{eqn | r = \dfrac {n - 1} n I_{n - 2} - \frac {\paren {\sin^{n - 1} \frac \pi 2 \cos \frac \pi 2 - \sin^{n - 1} 0 \cos 0} } n
      | c = 
}}
{{eqn | r = \dfrac {n - 1} n I_{n - 2} - \frac {\paren {0 - \sin^{n - 1} 0 \cos 0} } n
      | c = Cosine of Right Angle
}}
{{eqn | r = \dfrac {n - 1} n I_{n - 2} - \frac {\paren {0 - 0} } n
      | c = Sine of Zero is Zero
}}
{{eqn | ll= \leadsto
      | l = n I_n
      | r = \paren {n - 1} I_{n - 2}
      | c = multiplying both sides by $n$
}}
{{end-eqn}}
{{qed}}
Theorem: Stirling's Formula/Proof 2/Lemma 4

Let $I_n$ be defined as:
:$\ds I_n = \int_0^{\frac \pi 2} \sin^n x \rd x$
Then:
:$\ds \lim_{n \mathop \to \infty} \frac {I_{2 n} } {I_{2 n + 1} } = 1$

Proof:
{{begin-eqn}}
{{eqn | l = n I_n
      | r = \paren {n - 1} I_{n - 2}
      | cc= Reduction Formula for Definite Integral of Power of Sine
}}
{{eqn | ll= \leadsto
      | l = 1
      | o = <
      | r = \frac {I_{ 2n} } {I_{2 n + 1} }
      | cc= 
}}
{{eqn | o = <
      | r = \frac {I_{2 n - 1} } {I_{2 n + 1} }
      | cc= Reduction Formula for Definite Integral of Power of Sine
}}
{{eqn | r = \frac {2 n + 1}  {2 n}
      | cc= Reduction Formula for Definite Integral of Power of Sine
}}
{{eqn | o = \to
      | r = 1
      | c = as $n \to \infty$
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to Half Pi of Even Power of Sine x

{{begin-eqn}}
{{eqn | l = \int_0^{\frac \pi 2} \sin^{2 n} x \rd x
      | r = \dfrac {\paren {2 n}!} {\paren {2^n n!}^2} \dfrac \pi 2
      | c = 
}}
{{eqn | r = \dfrac {1 \cdot 3 \cdot 5 \cdots \paren {2 n - 1} } {2 \cdot 4 \cdot 6 \cdots 2 n} \dfrac \pi 2
      | c = 
}}
{{end-eqn}}
for $n \in \Z_{>0}$.

Proof:
{{improve|This would be more rigorous if implemented as a formal induction proof.}}
Let $I_n = \ds \int_0^{\frac \pi 2} \sin^n x \rd x$.
Then:
{{begin-eqn}}
{{eqn | l = I_{2 n}
      | r = \frac {2 n - 1} {2 n} I_{2 n - 2}
      | c = Reduction Formula for Definite Integral of Power of Sine
}}
{{eqn | r = \frac {\paren {2 n - 1} \paren {2 n - 3} } {2 n \paren {2 n - 2} } I_{2 n - 4}
      | c = Reduction Formula for Definite Integral of Power of Sine again
}}
{{eqn | r = \frac {\paren {2 n - 1} \paren {2 n - 3} \cdots 1} {2 n \paren {2 n - 2} \cdots 2} I_0
      | c = Reduction Formula for Definite Integral of Power of Sine until the end
}}
{{eqn | r = \frac {\paren {2 n - 1} \paren {2 n - 3} \cdots 1} {2 n \paren {2 n - 2} \cdots 2} \int_0^{\pi / 2} \rd x
      | c = Definition of $I_n$
}}
{{eqn | r = \frac {\paren {2 n - 1} \paren {2 n - 3} \cdots 1} {2 n \paren {2 n - 2} \cdots 2} \bigintlimits x 0 {\pi / 2}
      | c = Integral of Constant
}}
{{eqn | r = \frac {\paren {2 n - 1} \paren {2 n - 3} \cdots 1} {2 n \paren {2 n - 2} \cdots 2} \frac \pi 2
      | c = Integral of Constant
}}
{{eqn | r = \frac {2n \paren {2 n - 1} \paren {2 n - 2} \paren {2 n - 3} \cdots 2 \cdot 1} {\paren {2 n}^2 \paren {2 n - 2}^2 \cdots 2^2} \frac \pi 2
      | c = multiplying top and bottom by bottom
}}
{{eqn | r = \frac {2n \paren {2 n - 1} \paren {2 n - 2} \paren {2 n - 3} \cdots 2 \cdot 1} {\paren {2^n}^2 n^2 \paren {n - 1}^2 \cdots 1^2} \frac \pi 2
      | c = extracting factor of $\paren {2^n}^2$ from the bottom
}}
{{eqn | r = \frac {\paren {2 n}!} {\paren {2^n}^2 \paren {n!}^2} \frac \pi 2
      | c = {{Defof|Factorial}}
}}
{{eqn | r = \frac {\paren {2 n}!} {\paren {2^n n!}^2} \frac \pi 2
      | c = rearranging 
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to Half Pi of Odd Power of Sine x

{{begin-eqn}}
{{eqn | l = \int_0^{\frac \pi 2} \sin^{2 n + 1} x \rd x
      | r = \dfrac {\paren {2^n n!}^2} {\paren {2 n + 1}!}
      | c = 
}}
{{eqn | r = \dfrac {2 \cdot 4 \cdot 6 \cdots 2 n} {3 \cdot 5 \cdot 7 \cdots \paren {2 n + 1} }
      | c = 
}}
{{end-eqn}}
for $n \in \Z_{>0}$.

Proof:
{{improve|This would be more rigorous if implemented as a formal induction proof.}}
Let $I_n = \ds \int_0^{\frac \pi 2} \sin^n x \rd x$.
Then:
{{begin-eqn}}
{{eqn | l = I_{2 n + 1}
      | r = \frac {2 n} {2 n + 1} I_{2 n - 1}
      | c = Reduction Formula for Definite Integral of Power of Sine
}}
{{eqn | r = \frac {2 n \paren {2 n - 2} } {\paren {2 n + 1} \paren {2 n - 1} } I_{2 n - 3}
      | c = Reduction Formula for Definite Integral of Power of Sine again
}}
{{eqn | r = \frac {2 n \paren {2 n - 2} \dotsm 2} {\paren {2 n + 1} \paren {2 n - 1} \dotsm 3} I_1
      | c = Reduction Formula for Definite Integral of Power of Sine until the end
}}
{{eqn | r = \frac {2 n \paren {2 n - 2} \dotsm 2} {\paren {2 n + 1} \paren {2 n - 1} \dotsm 3} \int_0^{\pi / 2} \sin x \rd x
      | c = Definition of $I_n$
}}
{{eqn | r = \frac {2 n \paren {2 n - 2} \dotsm 2} {\paren {2 n + 1} \paren {2 n - 1} \dotsm 3} \bigintlimits {-\cos x} 0 {\pi / 2}
      | c = Primitive of Sine Function
}}
{{eqn | r = \frac {2 n \paren {2 n - 2} \dotsm 2} {\paren {2 n + 1} \paren {2 n - 1} \dotsm 3} \paren {0 - \paren {-1} }
      | c = Cosine of Right Angle and Cosine of Zero is One
}}
{{eqn | r = \frac {2 n \paren {2 n - 2} \dotsm 2} {\paren {2 n + 1} \paren {2 n - 1} \dotsm 3}
      | c = 
}}
{{eqn | r = \frac {\paren {2 n}^2 \paren {2 n - 2}^2 \dotsm 2^2} {\paren {2 n + 1} \paren {2 n} \paren {2 n - 1} \paren {2 n - 2} \paren {2 n - 3} \dotsm 3 \cdot 2}
      | c = multiplying top and bottom by top
}}
{{eqn | r = \frac {\paren {2 n}^2 n^2 \paren {n - 1}^2 \dotsm 1^2} {\paren {2 n + 1} \paren {2 n} \paren {2 n - 1} \paren {2 n - 2} \paren {2 n - 3} \dotsm 3 \cdot 2}
      | c = extracting factor of $\paren {2^n}^2$ from the top
}}
{{eqn | r = \frac {\paren {2^n n!}^2} {\paren {2 n + 1}!}
      | c = {{Defof|Factorial}}
}}
{{end-eqn}}
{{qed}}