Theorem: Stirling's Formula

The factorial function can be approximated by the formula:
:$n! \sim \sqrt {2 \pi n} \paren {\dfrac n e}^n$
where $\sim$ denotes asymptotically equal.

Proof:
Let $a_n = \dfrac {n!} {\sqrt {2 n} \paren {\frac n e}^n}$.
=== Part 1 ===
It will be shown that:
:$\ds \lim_{n \mathop \to \infty} a_n = a$
for some constant $a$.
This will imply that:
:$\ds \lim_{n \mathop \to \infty} \frac {n!} {a \sqrt{2 n} \paren {\frac n e}^n} = 1$
By applying Power Series Expansion for $\map \ln {1 + x}$:
{{begin-eqn}}
{{eqn | l = \map \ln {\frac {n + 1} n}
      | r = \map \ln {n + 1} - \map \ln n
      | c = Difference of Logarithms
}}
{{eqn | r = \map \ln {n + 1} + \map \ln 2 - \map \ln 2 - \map \ln n
      | c = adding $0$
}}
{{eqn | r = \map \ln {2 n + 2} - \map \ln {2 n}
      | c = Sum of Logarithms
}}
{{eqn | r = \map \ln {2 n + 2} - \map \ln {2 n + 1} + \map \ln {2 n + 1} - \map \ln {2 n}
      | c = adding $0$
}}
{{eqn | r = \map \ln {\dfrac {2 n + 2} {2 n + 1} } - \map \ln {\dfrac {2 n} {2 n + 1} } 
      | c = Difference of Logarithms
}}
{{eqn | r = \map \ln {1 + \frac 1 {2 n + 1} } - \map \ln {1 - \frac 1 {2 n + 1} }
      | c = setting $x = \dfrac 1 {2 n + 1}$
}}
{{eqn | r = \sum_{k \mathop = 1}^\infty \paren {-1}^{k - 1} \frac 1 k {\paren {\frac 1 {2 n + 1} }^k} - \paren {-\sum_{k \mathop = 1}^\infty \frac 1 k {\paren {\frac 1 {2 n + 1} }^k} }
      | c = Power Series Expansion for Logarithm of 1 + x and Power Series Expansion for Logarithm of 1 - x
}}
{{eqn | r = 2 \sum_{k \mathop = 0}^\infty \frac 1 {2 k + 1} \paren {\frac 1 {2 n + 1} }^{2 k + 1}
      | c = even terms cancel out; odd terms doubled
}}
{{end-eqn}}
Let $b_n = \ln a_n$.
{{begin-eqn}}
{{eqn | l = b_n
      | r = \map \ln {\dfrac {n!} {\sqrt {2 n} \paren {\frac n e}^n} }
      | c = 
}}
{{eqn | r = \map \ln {n!} - \dfrac 1 2 \map \ln {2 n} - n \map \ln {\frac n e}
      | c = Sum of Logarithms and Difference of Logarithms
}}
{{eqn | l = b_n - b_{n + 1}
      | r = \paren {\map \ln {n!} - \dfrac 1 2 \map \ln {2 n} - n \map \ln {\frac n e} } - \paren {\map \ln {\paren {n + 1}!} - \dfrac 1 2 \map \ln {2 n + 2} - \paren {n + 1} \map \ln {\frac {n + 1} e} }
      | c = 
}}
{{eqn | r = \map \ln {\dfrac {n!} {\paren {n + 1}!} } + \dfrac 1 2 \map \ln {\dfrac {2 n + 2} {2 n} } + n \map \ln {\frac {n + 1} n} + \map \ln {n + 1} - \map \ln e
      | c = Sum of Logarithms and Difference of Logarithms
}}
{{eqn | r = n \map \ln {\frac {n + 1} n} + \dfrac 1 2 \map \ln {\dfrac {n + 1} n} -  \map \ln {n + 1} + \map \ln {n + 1} - \map \ln e
      | c = rearranging
}}
{{eqn | r = \paren {n + \frac 1 2} \map \ln {\frac {n + 1} n} - 1
      | c = 
}}
{{eqn | r = \paren {n + \frac 1 2} 2 \sum_{k \mathop = 0}^\infty \frac 1 {2 k + 1} \paren {\frac 1 {2 n + 1} }^{2 k + 1} - 1
      | c = substituting from above and Power Series Expansion for Logarithm of 1 + x
}}
{{eqn | r = \paren {2 n + 1} \sum_{k \mathop = 0}^\infty \frac 1 {2 k + 1} \paren {\frac 1 {2 n + 1} }^{2 k + 1} - 1
      | c = 
}}
{{eqn | n = 1
      | r = \sum_{k \mathop = 1}^\infty \frac 1 {2 k + 1} \paren {\frac 1 {2 n + 1} }^{2 k} 
      | c = canceling $k = 0$ from sum
}}
{{eqn | o = >
      | r = 0
      | c =
}}
{{eqn | l = b_n
      | o = >
      | r = b_{n + 1}
      | c = 
}}
{{end-eqn}}
so the sequence $\sequence {b_n}$ is (strictly) decreasing.
From $(1)$:
{{begin-eqn}}
{{eqn | l = b_n - b_{n + 1}
      | r = \sum_{k \mathop = 1}^\infty \frac 1 {2 k + 1} \paren {\frac 1 {2 n + 1} }^{2 k}
      | c =
}}
{{eqn | ll= \leadsto
      | l = b_n - b_{n + 1}
      | o = <
      | r = \sum_{k \mathop = 1}^\infty \paren {\frac 1 {2 n + 1} }^{2 k}
      | c = as $\dfrac 1 {2 k + 1} < 1$
}}
{{eqn | r = \dfrac {\paren {\dfrac 1 {2 n + 1} }^2} {1 - \paren {\dfrac 1 {2 n + 1} }^2}
      | c = Sum of Infinite Geometric Sequence
}}
{{eqn | r = \dfrac {\paren {\dfrac 1 {2 n + 1} }^2} {1 - \paren {\dfrac 1 {2 n + 1} }^2} \dfrac {\paren {2 n + 1}^2} {\paren {2 n + 1}^2}
      | c = multiplying by $1$
}}
{{eqn | r = \dfrac 1 {\paren {2 n + 1}^2 - 1}
      | c = 
}}
{{eqn | r = \frac 1 {4 n \paren {n + 1} }
      | c = 
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = b_1 - b_n
      | r = \sum_{m \mathop = 1}^{n - 1} b_m - b_{m + 1}
      | c = {{Defof|Telescoping Series}}
}}
{{eqn | r = \frac 1 4 \sum_{m \mathop = 1}^{n - 1} \frac 1 {m \paren {m + 1} }
      | c = from above
}}
{{eqn | o = <
      | r = \frac 1 4 \sum_{m \mathop = 1}^\infty \frac 1 {m \paren {m + 1} }
      | c = all the way to $\infty$
}}
{{eqn | r = \frac 1 4
      | c = Sum from $1$ to $n$ of $\dfrac 1 {r \paren {r + 1} }$
}}
{{end-eqn}}
and so: 
{{begin-eqn}}
{{eqn | l = b_1
      | r = \map \ln {1!} - \dfrac 1 2 \map \ln 2 - \map \ln {\frac 1 e}
      | c = 
}}
{{eqn | r = 1 - \dfrac 1 2 \map \ln 2
      | c = 
}}
{{end-eqn}}
and:
:$b_1 - b_n < \dfrac 1 4$
Therefore:
:$b_n > b_1 - \dfrac 1 4 = \dfrac 3 4 - \dfrac 1 2 \map \ln 2$
Thus by definition $\sequence {b_n}$ is bounded below. 
By Monotone Convergence Theorem, it follows that $\sequence {b_n}$ is convergent.
Let $b$ denote its limit. 
Then:
:$\ds \lim_{n \mathop \to \infty} a_n = e^{\lim_{n \mathop \to \infty} b_n} = e^b = a$
as required.
{{qed|lemma}}
=== Part 2 ===
By Wallis's Product, we have:
{{begin-eqn}}
{{eqn | l = \frac \pi 2
      | r = \prod_{k \mathop = 1}^\infty \frac {2 k} {2 k - 1} \cdot \frac {2 k} {2 k + 1}
      | c = 
}}
{{eqn | r = \prod \paren {\frac 2 1 \cdot \frac 2 3} \paren {\frac 4 3 \cdot \frac 4 5} \paren {\frac 6 5 \cdot \frac 6 7} \cdots
      | c = 
}}
{{eqn | r = \lim_{n \mathop \to \infty} \dfrac 1 {2 n + 1} \prod_{k \mathop = 1}^n \frac {\paren {2 k}^2} {\paren {2 k - 1}^2}
      | c = 
}}
{{eqn | r = \lim_{n \mathop \to \infty} \dfrac 1 {2 n + 1} \prod_{k \mathop = 1}^n \frac {\paren {2 k}^2} {\paren {2 k - 1}^2} \dfrac {\paren {2 k}^2} {\paren {2 k}^2}
      | c = multiplying by $1$
}}
{{eqn | r = \lim_{n \mathop \to \infty} \dfrac 1 {2 n + 1} \prod_{k \mathop = 1}^n \frac {2^4 k^4} {\paren {\paren {2 k - 1} \paren {2 k} }^2}
      | c = 
}}
{{eqn | n = 2
      | r = \lim_{n \mathop \to \infty} \frac {2^{4 n} \paren {n!}^4} {\paren {\paren {2 n}!}^2 \paren {2 n + 1} }
      | c = 
}}
{{end-eqn}}
In Part 1 it was proved that:
:$n! \sim a \sqrt {2 n} \paren {\dfrac n e}^n$
Substituting for $n!$ in $(2)$ yields:
{{begin-eqn}}
{{eqn | l = \frac \pi 2
      | r = \lim_{n \mathop \to \infty} \frac {2^{4 n} \paren {n!}^4} {\paren {\paren {2 n}!}^2 \paren {2 n + 1} }
      | c = 
}}
{{eqn | r = \lim_{n \mathop \to \infty} \frac {2^{4 n} \paren {a \sqrt {2 n} \paren {\dfrac n e}^n}^4} {\paren {\paren {a \sqrt {4 n} \paren {\dfrac {2 n} e}^{2 n} } }^2 \paren {2 n + 1} }
      | c = 
}}
{{eqn | r = \lim_{n \mathop \to \infty} \frac {2^{4 n} a^4 \paren {4 n^2} n^{4 n} e^{-4 n} } {a^2 \paren {4 n} 2^{4 n} n^{4 n} e^{-4 n} \paren {2 n + 1} }
      | c = Power of Power
}}
{{eqn | r = a^2 \lim_{n \mathop \to \infty} \frac n {2 n + 1}
      | c = as most of it cancels out
}}
{{eqn | r = \frac {a^2} 2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a
      | r = \sqrt \pi
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}