Metamath Proof Explorer


Theorem stirling

Description: Stirling's approximation formula for n factorial. The proof follows two major steps: first it is proven that S and n factorial are asymptotically equivalent, up to an unknown constant. Then, using Wallis' formula for π it is proven that the unknown constant is the square root of π and then the exact Stirling's formula is established. This is Metamath 100 proof #90. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypothesis stirling.1 S=n02πnnen
Assertion stirling nn!Sn1

Proof

Step Hyp Ref Expression
1 stirling.1 S=n02πnnen
2 eqid nn!2nnen=nn!2nnen
3 eqid nlognn!2nnenn=nlognn!2nnenn
4 2 3 stirlinglem14 c+nn!2nnenc
5 nfv nc+
6 nfmpt1 _nnn!2nnen
7 nfcv _n
8 nfcv _nc
9 6 7 8 nfbr nnn!2nnenc
10 5 9 nfan nc+nn!2nnenc
11 eqid nnn!2nnen2n=nnn!2nnen2n
12 eqid n2nnen=n2nnen
13 eqid n24nn!42n!22n+1=n24nn!42n!22n+1
14 eqid nnn!2nnenn4nnn!2nnen2nn2=nnn!2nnenn4nnn!2nnen2nn2
15 eqid nn2n2n+1=nn2n2n+1
16 simpl c+nn!2nnencc+
17 simpr c+nn!2nnencnn!2nnenc
18 10 1 2 11 12 13 14 15 16 17 stirlinglem15 c+nn!2nnencnn!Sn1
19 18 rexlimiva c+nn!2nnencnn!Sn1
20 4 19 ax-mp nn!Sn1