Metamath Proof Explorer

Theorem stirlingr

Description: Stirling's approximation formula for n factorial: here convergence is expressed with respect to the standard topology on the reals. The main theorem stirling is proven for convergence in the topology of complex numbers. The variable R is used to denote convergence with respect to the standard topology on the reals. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses stirlingr.1 
|- S = ( n e. NN0 |-> ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) )
stirlingr.2 
|- R = ( ~~>t ` ( topGen ` ran (,) ) )
Assertion stirlingr 
|- ( n e. NN |-> ( ( ! ` n ) / ( S ` n ) ) ) R 1

Proof

Step Hyp Ref Expression
1 stirlingr.1 
 |-  S = ( n e. NN0 |-> ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) )
2 stirlingr.2 
 |-  R = ( ~~>t ` ( topGen ` ran (,) ) )
3 1 stirling 
 |-  ( n e. NN |-> ( ( ! ` n ) / ( S ` n ) ) ) ~~> 1
4 nnuz 
 |-  NN = ( ZZ>= ` 1 )
5 1zzd 
 |-  ( T. -> 1 e. ZZ )
6 eqid 
 |-  ( n e. NN |-> ( ( ! ` n ) / ( S ` n ) ) ) = ( n e. NN |-> ( ( ! ` n ) / ( S ` n ) ) )
7 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
8 faccl 
 |-  ( n e. NN0 -> ( ! ` n ) e. NN )
9 nnre 
 |-  ( ( ! ` n ) e. NN -> ( ! ` n ) e. RR )
10 7 8 9 3syl 
 |-  ( n e. NN -> ( ! ` n ) e. RR )
11 2re 
 |-  2 e. RR
12 11 a1i 
 |-  ( n e. NN -> 2 e. RR )
13 pire 
 |-  _pi e. RR
14 13 a1i 
 |-  ( n e. NN -> _pi e. RR )
15 12 14 remulcld 
 |-  ( n e. NN -> ( 2 x. _pi ) e. RR )
16 nnre 
 |-  ( n e. NN -> n e. RR )
17 15 16 remulcld 
 |-  ( n e. NN -> ( ( 2 x. _pi ) x. n ) e. RR )
18 0re 
 |-  0 e. RR
19 18 a1i 
 |-  ( n e. NN -> 0 e. RR )
20 2pos 
 |-  0 < 2
21 20 a1i 
 |-  ( n e. NN -> 0 < 2 )
22 19 12 21 ltled 
 |-  ( n e. NN -> 0 <_ 2 )
23 pipos 
 |-  0 < _pi
24 18 13 23 ltleii 
 |-  0 <_ _pi
25 24 a1i 
 |-  ( n e. NN -> 0 <_ _pi )
26 12 14 22 25 mulge0d 
 |-  ( n e. NN -> 0 <_ ( 2 x. _pi ) )
27 7 nn0ge0d 
 |-  ( n e. NN -> 0 <_ n )
28 15 16 26 27 mulge0d 
 |-  ( n e. NN -> 0 <_ ( ( 2 x. _pi ) x. n ) )
29 17 28 resqrtcld 
 |-  ( n e. NN -> ( sqrt ` ( ( 2 x. _pi ) x. n ) ) e. RR )
30 ere 
 |-  _e e. RR
31 30 a1i 
 |-  ( n e. NN -> _e e. RR )
32 epos 
 |-  0 < _e
33 18 32 gtneii 
 |-  _e =/= 0
34 33 a1i 
 |-  ( n e. NN -> _e =/= 0 )
35 16 31 34 redivcld 
 |-  ( n e. NN -> ( n / _e ) e. RR )
36 35 7 reexpcld 
 |-  ( n e. NN -> ( ( n / _e ) ^ n ) e. RR )
37 29 36 remulcld 
 |-  ( n e. NN -> ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) e. RR )
38 1 fvmpt2 
 |-  ( ( n e. NN0 /\ ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) e. RR ) -> ( S ` n ) = ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) )
39 7 37 38 syl2anc 
 |-  ( n e. NN -> ( S ` n ) = ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) )
40 2rp 
 |-  2 e. RR+
41 40 a1i 
 |-  ( n e. NN -> 2 e. RR+ )
42 pirp 
 |-  _pi e. RR+
43 42 a1i 
 |-  ( n e. NN -> _pi e. RR+ )
44 41 43 rpmulcld 
 |-  ( n e. NN -> ( 2 x. _pi ) e. RR+ )
45 nnrp 
 |-  ( n e. NN -> n e. RR+ )
46 44 45 rpmulcld 
 |-  ( n e. NN -> ( ( 2 x. _pi ) x. n ) e. RR+ )
47 46 rpsqrtcld 
 |-  ( n e. NN -> ( sqrt ` ( ( 2 x. _pi ) x. n ) ) e. RR+ )
48 epr 
 |-  _e e. RR+
49 48 a1i 
 |-  ( n e. NN -> _e e. RR+ )
50 45 49 rpdivcld 
 |-  ( n e. NN -> ( n / _e ) e. RR+ )
51 nnz 
 |-  ( n e. NN -> n e. ZZ )
52 50 51 rpexpcld 
 |-  ( n e. NN -> ( ( n / _e ) ^ n ) e. RR+ )
53 47 52 rpmulcld 
 |-  ( n e. NN -> ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) e. RR+ )
54 39 53 eqeltrd 
 |-  ( n e. NN -> ( S ` n ) e. RR+ )
55 10 54 rerpdivcld 
 |-  ( n e. NN -> ( ( ! ` n ) / ( S ` n ) ) e. RR )
56 6 55 fmpti 
 |-  ( n e. NN |-> ( ( ! ` n ) / ( S ` n ) ) ) : NN --> RR
57 56 a1i 
 |-  ( T. -> ( n e. NN |-> ( ( ! ` n ) / ( S ` n ) ) ) : NN --> RR )
58 2 4 5 57 climreeq 
 |-  ( T. -> ( ( n e. NN |-> ( ( ! ` n ) / ( S ` n ) ) ) R 1 <-> ( n e. NN |-> ( ( ! ` n ) / ( S ` n ) ) ) ~~> 1 ) )
59 58 mptru 
 |-  ( ( n e. NN |-> ( ( ! ` n ) / ( S ` n ) ) ) R 1 <-> ( n e. NN |-> ( ( ! ` n ) / ( S ` n ) ) ) ~~> 1 )
60 3 59 mpbir 
 |-  ( n e. NN |-> ( ( ! ` n ) / ( S ` n ) ) ) R 1