Theorem: Stirling's Formula/Refinement

A refinement of Stirling's Formula is:
:$n! = \sqrt {2 \pi n} \paren {\dfrac n e}^n \paren {1 + \dfrac 1 {12 n} + \map \OO  {\dfrac 1 {n^2} } }$

Proof:
From Limit of Error in Stirling's Formula, we have:
:$e^{1 / \paren {12 n + 1} } < \dfrac {n!} {\sqrt {2 \pi n} n^n e^{-n} } < e^{1 / 12 n}$
We also have:
{{begin-eqn}}
{{eqn | l = e^{1 / 12 n}
      | r = 1 + \frac 1 {12 n} + \frac 1 {2!} \paren {\frac 1 {12 n} }^2 + \frac 1 {3!} \paren {\frac 1 {12 n} }^3 + \cdots
      | c = Taylor Series Expansion for Exponential Function
}}
{{eqn | r = 1 + \frac 1 {12 n} + \paren {\frac 1 {12 n} }^2 \paren {\frac 1 {2!} + \frac 1 {3!} \paren {\frac 1 {12 n} }  + \cdots }
      | c = 
}}
{{eqn | o = <
      | r = 1 + \frac 1 {12 n} + \paren {\frac 1 {12 n} }^2 \paren {1 + \frac 1 {1!} + \frac 1 {2!} + \frac 1 {3!}  + \cdots }
      | c = $\forall n \in \N_{\ge 1}$; $1 > \dfrac 1 {12 n}$
}}
{{eqn | r = 1 + \frac 1 {12 n} + \paren {\frac 1 {12 n} }^2 \paren {e }
      | c = {{Defof|Euler's Number as Limit of Series}}
}}
{{eqn | ll = \leadsto
      | n = 1
      | l = e^{1 / 12 n}
      | o = <
      | r = 1 + \frac 1 {12 n} + \paren {\frac e {144} } \paren {\frac 1 {n^2} }
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = e^{1 / \paren {12 n + 1} }
      | r = 1 + \frac 1 {12 n + 1} + \frac 1 {2!} \paren {\frac 1 {12 n + 1} }^2 + \frac 1 {3!} \paren {\frac 1 {12 n + 1} }^3 + \cdots
      | c = Taylor Series Expansion for Exponential Function
}}
{{eqn | o = >
      | r = 1 + \frac 1 {12 n + 1}
      | c = 
}}
{{eqn | r =  1 + \frac 1 {12 n} - \frac 1 {12 n \paren {12 n + 1} }
      | c = 
}}
{{eqn | r =  1 + \frac 1 {12 n} - \frac 1 {144 n^2 + 12 n }
      | c = 
}}
{{eqn | ll = \leadsto
      | n = 2
      | l = e^{1 / \paren {12 n + 1} }
      | o = >
      | r = 1 + \frac 1 {12 n} - \paren {\dfrac 1 {156} } \paren {\frac 1 {n^2} }
      | c = 
}}
{{end-eqn}}
From the {{Defof|Big-O Notation/Real|Big-O Notation}}:
The statement:
:$\map f x = \map \OO {\map g x}$ as $x \to \infty$
is equivalent to:
:$\size {\map f x} \le c \cdot \size {\map g x}$
for $x$ sufficiently large.
We have:
{{begin-eqn}}
{{eqn | l = e^{1 / \paren {12 n + 1} }
      | o = <
      | m = \dfrac {n!} {\sqrt {2 \pi n} n^n e^{-n} }
      | ro = <
      | rr = e^{1 / 12 n}
      | c = Limit of Error in Stirling's Formula
}}
{{eqn | ll = \leadsto
      | l = 1 + \frac 1 {12 n} - \paren {\dfrac 1 {156} } \paren {\frac 1 {n^2} }
      | o = <
      | m = \dfrac {n!} {\sqrt {2 \pi n} n^n e^{-n} }
      | ro = <
      | rr = 1 + \frac 1 {12 n} + \paren {\frac e {144} } \paren {\frac 1 {n^2} }
      | c = from $\paren 1$ and $\paren 2$ above
}}
{{eqn | ll = \leadsto
      | l = - \paren {\dfrac 1 {156} } \paren {\frac 1 {n^2} }
      | o = <
      | m = \dfrac {n!} {\sqrt {2 \pi n} n^n e^{-n} } - \paren {1 + \frac 1 {12 n} }
      | ro = <
      | rr = \paren {\frac e {144} } \paren {\frac 1 {n^2} }
      | c = subtracting $1 + \dfrac 1 {12 n}$ throughout
}}
{{end-eqn}}
Hence:
:$\ds \size {\dfrac {n!} {\sqrt {2 \pi n} n^n e^{-n} } - \paren {1 + \frac 1 {12 n} } } \lt \dfrac e {144} \cdot \size {\dfrac 1 {n^2} }$
Therefore:
{{begin-eqn}}
{{eqn | l = \dfrac {n!} {\sqrt {2 \pi n} n^n e^{-n} } - \paren {1 + \frac 1 {12 n} } 
      | r = \map \OO  {\dfrac 1 {n^2} }
      | c = {{Defof|Big-O Notation/Real|Big-O Notation}}
}}
{{eqn | ll = \leadsto
      | l = \dfrac {n!} {\sqrt {2 \pi n} n^n e^{-n} }
      | r = \paren {1 + \frac 1 {12 n} } + \map \OO  {\dfrac 1 {n^2} }
      | c = moving $\paren {1 + \dfrac 1 {12 n} }$ to the {{RHS}}
}}
{{eqn | ll = \leadsto
      | l = n!
      | r = \sqrt {2 \pi n} \paren {\dfrac n e}^n \paren {1 + \dfrac 1 {12 n} + \map \OO  {\dfrac 1 {n^2} } }
      | c = multiplying through by $\sqrt {2 \pi n} \paren {\dfrac n e}^n$
}}
{{end-eqn}}
{{qed}}