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 = ( n e. NN0 |-> ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) )
Assertion stirling 
|- ( n e. NN |-> ( ( ! ` n ) / ( S ` n ) ) ) ~~> 1

Proof

Step Hyp Ref Expression
1 stirling.1 
 |-  S = ( n e. NN0 |-> ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) )
2 eqid 
 |-  ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) = ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
3 eqid 
 |-  ( n e. NN |-> ( log ` ( ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) ` n ) ) ) = ( n e. NN |-> ( log ` ( ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) ` n ) ) )
4 2 3 stirlinglem14 
 |-  E. c e. RR+ ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) ~~> c
5 nfv 
 |-  F/ n c e. RR+
6 nfmpt1 
 |-  F/_ n ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
7 nfcv 
 |-  F/_ n ~~>
8 nfcv 
 |-  F/_ n c
9 6 7 8 nfbr 
 |-  F/ n ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) ~~> c
10 5 9 nfan 
 |-  F/ n ( c e. RR+ /\ ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) ~~> c )
11 eqid 
 |-  ( n e. NN |-> ( ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) ` ( 2 x. n ) ) ) = ( n e. NN |-> ( ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) ` ( 2 x. n ) ) )
12 eqid 
 |-  ( n e. NN |-> ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) = ( n e. NN |-> ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) )
13 eqid 
 |-  ( n e. NN |-> ( ( ( ( 2 ^ ( 4 x. n ) ) x. ( ( ! ` n ) ^ 4 ) ) / ( ( ! ` ( 2 x. n ) ) ^ 2 ) ) / ( ( 2 x. n ) + 1 ) ) ) = ( n e. NN |-> ( ( ( ( 2 ^ ( 4 x. n ) ) x. ( ( ! ` n ) ^ 4 ) ) / ( ( ! ` ( 2 x. n ) ) ^ 2 ) ) / ( ( 2 x. n ) + 1 ) ) )
14 eqid 
 |-  ( n e. NN |-> ( ( ( ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) ` n ) ^ 4 ) / ( ( ( n e. NN |-> ( ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) ` ( 2 x. n ) ) ) ` n ) ^ 2 ) ) ) = ( n e. NN |-> ( ( ( ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) ` n ) ^ 4 ) / ( ( ( n e. NN |-> ( ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) ` ( 2 x. n ) ) ) ` n ) ^ 2 ) ) )
15 eqid 
 |-  ( n e. NN |-> ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) ) = ( n e. NN |-> ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) )
16 simpl 
 |-  ( ( c e. RR+ /\ ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) ~~> c ) -> c e. RR+ )
17 simpr 
 |-  ( ( c e. RR+ /\ ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) ~~> c ) -> ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) ~~> c )
18 10 1 2 11 12 13 14 15 16 17 stirlinglem15 
 |-  ( ( c e. RR+ /\ ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) ~~> c ) -> ( n e. NN |-> ( ( ! ` n ) / ( S ` n ) ) ) ~~> 1 )
19 18 rexlimiva 
 |-  ( E. c e. RR+ ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) ~~> c -> ( n e. NN |-> ( ( ! ` n ) / ( S ` n ) ) ) ~~> 1 )
20 4 19 ax-mp 
 |-  ( n e. NN |-> ( ( ! ` n ) / ( S ` n ) ) ) ~~> 1