Wallis の公式の系より
$$\underset{n\to \mathrm{\infty }}{lim}\frac{\sqrt{n}\cdot {}_{2n}{\mathrm{C}}_n}{4^n}=\frac{1}{\sqrt{\pi }}$$
である．いま
$$b_n=\frac{4^n(n!{)}^2}{\sqrt{n}(2n)!}=\frac{4^n}{\sqrt{n}\cdot {}_{2n}{\mathrm{C}}_n}$$
であるから
$$\underset{n\to \mathrm{\infty }}{lim}{b}_n=\sqrt{\pi }$$
を得る．

$$f(x)=\log (1+x)-x+\frac{x^2}{2}-\frac{x^3}{3}+\frac{x^4}{4}$$
とおく．
$$f^{\prime }(x)=\frac{1}{1+x}-(1-x+x^2-x^3)=\frac{1}{1+x}-\frac{1-x^4}{1+x}=\frac{x^4}{x+1}>0$$
であるから，$f(x)$ は $0<x<1$ で単調に増加する．ゆえに
$$\log (1+x)-x+\frac{x^2}{2}-\frac{x^3}{3}+\frac{x^4}{4}=f(x)\geqq f(0)=0$$
を整理すれば求める不等式の左辺が評価できる．
$$g(x)=\log (1+x)-x+\frac{x^2}{2}-\frac{x^3}{3}$$
とおく．
$$g^{\prime }(x)=\frac{1}{1+x}-(1-x+x^2)=\frac{1}{1+x}-\frac{1+x^3}{1+x}=-\frac{x^3}{1+x}<0$$
であるから，$g(x)$ は $0<x<1$ で単調に減少する．ゆえに
$$\log (1+x)-x+\frac{x^2}{2}-\frac{x^3}{3}=g(x)\leqq g(0)=0$$
を整理すれば求める不等式の右辺が評価できる．

$$\begin{array}{rcl}\frac{a_n}{a_{n+1}}& =& \frac{n!}{\sqrt{n}{n}^n{e}^{-n}}\cdot \frac{\sqrt{n+1}(n+1{)}^{n+1}{e}^{-n-1}}{(n+1)!}\\ & =& \frac{n!}{\sqrt{n}{n}^n{e}^{-n}}\cdot \frac{\sqrt{n+1}(n+1)(n+1{)}^n{e}^{-n}{e}^{-1}}{(n+1)n!}\\ & =& \frac{\sqrt{n+1}}{\sqrt{n}}\cdot \frac{(n+1{)}^n}{n^n}\cdot e^{-1}\\ & =& \sqrt{\frac{n+1}{n}}{\left(\frac{n+1}{n}\right)}^n\cdot \frac{1}{e}\\ & =& {\left(\frac{n+1}{n}\right)}^{n+\frac{1}{2}}\cdot \frac{1}{e}\end{array}$$

であるから

$$\log \frac{a_n}{a_{n+1}}=\log {\left(\frac{n+1}{n}\right)}^{n+\frac{1}{2}}\cdot \frac{1}{e}=(n+\frac{1}{2})\log (1+\frac{1}{n})-1$$

が成り立つ．いま，$n\geqq 2$ であるから $0<1/n<1$ である．補題 3 において $x=1/n$ とすれば
$$\frac{1}{n}-\frac{1}{2n^2}+\frac{1}{3n^3}-\frac{1}{4n^4}<\log (1+\frac{1}{n})<\frac{1}{n}-\frac{1}{2n^2}+\frac{1}{3n^3}$$
$$\frac{1}{12n^2}-\frac{1}{12n^3}-\frac{1}{8n^4}<(n+\frac{1}{2})\log (1+\frac{1}{n})-1<\frac{1}{12n^2}+\frac{1}{6n^3}$$
$$\frac{1}{12n^2}-\frac{1}{12n^3}-\frac{1}{8n^4}<\log \frac{a_n}{a_{n+1}}<\frac{1}{12n^2}+\frac{1}{6n^3}$$
が成り立つ．不等式の最左辺については，$n\geqq 2$ のとき
$$\frac{1}{12n^2}-\frac{1}{12n^3}-\frac{1}{8n^4}=\frac{2n^2-2n+3}{24n^4}>0$$
が成り立っている．最右辺については，$n>1$ のとき
$$\frac{2}{n(n+1)}-\frac{1}{n^2}=\frac{n-1}{n^2(n+1)}>0$$
より
$$\frac{1}{n^2}<\frac{2}{n(n+1)}$$
が成り立つことに注意すれば
$$\frac{1}{12n^2}+\frac{1}{6n^3}<\frac{1}{12n^2}+\frac{1}{6n^2}=\frac{1}{4n^2}<\frac{1}{2n(n+1)}$$
を得る．したがって
$$0<\log \frac{a_n}{a_{n+1}}<\frac{1}{2n(n+1)}$$
が示された．

$$\begin{array}{rcl}\log \frac{a_n}{a_{2n}}& =& \log \frac{a_n}{a_{n+1}}\cdot \frac{a_{n+1}}{a_{n+2}}\cdots \frac{a_{2n-2}}{a_{2n-1}}\cdot \frac{a_{2n-1}}{a_{2n}}\\ & =& \log \frac{a_n}{a_{n+1}}+\log \frac{a_{n+1}}{a_{n+2}}+\cdots +\log \frac{a_{2n-2}}{a_{2n-1}}+\log \frac{a_{2n-1}}{a_{2n}}\\ & =& \sum _{k=1}^n\log \frac{a_{n+k-1}}{a_{n+k}}\end{array}$$

である．$\log (a_n/a_{n+1})$ の評価より
$$0<\sum _{k=1}^n\log \frac{a_{n+k-1}}{a_{n+k}}<\sum _{k=1}^n\frac{1}{2(n+k-1)(n+k)}$$
であるが，最右辺については部分分数分解を用いて
$$\begin{array}{rcl}\sum _{k=1}^n\frac{1}{2(n+k-1)(n+k)}& =& \frac{1}{2}\sum _{k=1}^n\frac{1}{(n+k-1)(n+k)}\\ & =& \frac{1}{2}\sum _{k=1}^n(\frac{1}{n+k-1}-\frac{1}{n+k})\\ & =& \frac{1}{2}\{(\frac{1}{n}-\frac{1}{n+1})+(\frac{1}{n+1}-\frac{1}{n+2})+\\ & & \cdots +(\frac{1}{n+n-1}-\frac{1}{n+n})\}\\ & =& \frac{1}{2}(\frac{1}{n}-\frac{1}{2n})\\ & =& \frac{1}{4n}\end{array}$$
と計算できる．したがって
$$0<\log \frac{a_n}{a_{2n}}<\frac{1}{4n}$$
が成り立つ．ここで $n\to \mathrm{\infty }$ の極限をとれば，はさみうちの原理より
$$\underset{n\to \mathrm{\infty }}{lim}\log \frac{a_n}{a_{2n}}=0$$
ゆえに
$$\underset{n\to \mathrm{\infty }}{lim}\frac{a_n}{a_{2n}}=1$$
である．

$$

$$\begin{array}{rcl}{a}_n^2& =& \frac{n!}{\sqrt{n}{n}^n{e}^{-n}}\cdot \frac{n!}{\sqrt{n}{n}^n{e}^{-n}}\\ & =& \frac{4^n(n!{)}^2}{\sqrt{n}(2n)!}\cdot \frac{(2n)!}{4^n\cdot \sqrt{2}\cdot \sqrt{n}{n}^{2n}{e}^{-2n}}\cdot \sqrt{2}\\ & =& \frac{4^n(n!{)}^2}{\sqrt{n}(2n)!}\cdot \frac{(2n)!}{\sqrt{2n}(2n{)}^{2n}{e}^{-2n}}\cdot \sqrt{2}\\ & =& b_n\cdot a_{2n}\cdot \sqrt{2}\end{array}$$
$$

であるから
$$a_n=\sqrt{2}{b}_n\cdot \frac{a_{2n}}{a_n}$$
が成り立つ．したがって $\{a_n\}$ の定義から
$$\underset{n\to \mathrm{\infty }}{lim}\frac{n!}{\sqrt{2\pi n}(n/e{)}^n}=\underset{n\to \mathrm{\infty }}{lim}\frac{a_n}{\sqrt{2\pi }}=\underset{n\to \mathrm{\infty }}{lim}\frac{b_n}{\sqrt{\pi }}\cdot \frac{a_{2n}}{a_n}=1\cdot 1=1$$

を得る．