Metamath Proof Explorer

Theorem stirlinglem14

Description: The sequence A converges to a positive real. This proves that the Stirling's formula converges to the factorial, up to a constant. In another theorem, using Wallis' formula for π& , such constant is exactly determined, thus proving the Stirling's formula. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses stirlinglem14.1 
|- A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
stirlinglem14.2 
|- B = ( n e. NN |-> ( log ` ( A ` n ) ) )
Assertion stirlinglem14 
|- E. c e. RR+ A ~~> c

Proof

Step Hyp Ref Expression
1 stirlinglem14.1 
 |-  A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
2 stirlinglem14.2 
 |-  B = ( n e. NN |-> ( log ` ( A ` n ) ) )
3 1 2 stirlinglem13 
 |-  E. d e. RR B ~~> d
4 simpl 
 |-  ( ( d e. RR /\ B ~~> d ) -> d e. RR )
5 4 rpefcld 
 |-  ( ( d e. RR /\ B ~~> d ) -> ( exp ` d ) e. RR+ )
6 nnuz 
 |-  NN = ( ZZ>= ` 1 )
7 1zzd 
 |-  ( ( d e. RR /\ B ~~> d ) -> 1 e. ZZ )
8 efcn 
 |-  exp e. ( CC -cn-> CC )
9 8 a1i 
 |-  ( ( d e. RR /\ B ~~> d ) -> exp e. ( CC -cn-> CC ) )
10 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
11 faccl 
 |-  ( n e. NN0 -> ( ! ` n ) e. NN )
12 nncn 
 |-  ( ( ! ` n ) e. NN -> ( ! ` n ) e. CC )
13 10 11 12 3syl 
 |-  ( n e. NN -> ( ! ` n ) e. CC )
14 2cnd 
 |-  ( n e. NN -> 2 e. CC )
15 nncn 
 |-  ( n e. NN -> n e. CC )
16 14 15 mulcld 
 |-  ( n e. NN -> ( 2 x. n ) e. CC )
17 16 sqrtcld 
 |-  ( n e. NN -> ( sqrt ` ( 2 x. n ) ) e. CC )
18 epr 
 |-  _e e. RR+
19 rpcn 
 |-  ( _e e. RR+ -> _e e. CC )
20 18 19 ax-mp 
 |-  _e e. CC
21 20 a1i 
 |-  ( n e. NN -> _e e. CC )
22 0re 
 |-  0 e. RR
23 epos 
 |-  0 < _e
24 22 23 gtneii 
 |-  _e =/= 0
25 24 a1i 
 |-  ( n e. NN -> _e =/= 0 )
26 15 21 25 divcld 
 |-  ( n e. NN -> ( n / _e ) e. CC )
27 26 10 expcld 
 |-  ( n e. NN -> ( ( n / _e ) ^ n ) e. CC )
28 17 27 mulcld 
 |-  ( n e. NN -> ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) e. CC )
29 2rp 
 |-  2 e. RR+
30 29 a1i 
 |-  ( n e. NN -> 2 e. RR+ )
31 nnrp 
 |-  ( n e. NN -> n e. RR+ )
32 30 31 rpmulcld 
 |-  ( n e. NN -> ( 2 x. n ) e. RR+ )
33 32 sqrtgt0d 
 |-  ( n e. NN -> 0 < ( sqrt ` ( 2 x. n ) ) )
34 33 gt0ne0d 
 |-  ( n e. NN -> ( sqrt ` ( 2 x. n ) ) =/= 0 )
35 nnne0 
 |-  ( n e. NN -> n =/= 0 )
36 15 21 35 25 divne0d 
 |-  ( n e. NN -> ( n / _e ) =/= 0 )
37 nnz 
 |-  ( n e. NN -> n e. ZZ )
38 26 36 37 expne0d 
 |-  ( n e. NN -> ( ( n / _e ) ^ n ) =/= 0 )
39 17 27 34 38 mulne0d 
 |-  ( n e. NN -> ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) =/= 0 )
40 13 28 39 divcld 
 |-  ( n e. NN -> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) e. CC )
41 1 fvmpt2 
 |-  ( ( n e. NN /\ ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) e. CC ) -> ( A ` n ) = ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
42 40 41 mpdan 
 |-  ( n e. NN -> ( A ` n ) = ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
43 42 40 eqeltrd 
 |-  ( n e. NN -> ( A ` n ) e. CC )
44 nnne0 
 |-  ( ( ! ` n ) e. NN -> ( ! ` n ) =/= 0 )
45 10 11 44 3syl 
 |-  ( n e. NN -> ( ! ` n ) =/= 0 )
46 13 28 45 39 divne0d 
 |-  ( n e. NN -> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) =/= 0 )
47 42 46 eqnetrd 
 |-  ( n e. NN -> ( A ` n ) =/= 0 )
48 43 47 logcld 
 |-  ( n e. NN -> ( log ` ( A ` n ) ) e. CC )
49 2 48 fmpti 
 |-  B : NN --> CC
50 49 a1i 
 |-  ( ( d e. RR /\ B ~~> d ) -> B : NN --> CC )
51 simpr 
 |-  ( ( d e. RR /\ B ~~> d ) -> B ~~> d )
52 4 recnd 
 |-  ( ( d e. RR /\ B ~~> d ) -> d e. CC )
53 6 7 9 50 51 52 climcncf 
 |-  ( ( d e. RR /\ B ~~> d ) -> ( exp o. B ) ~~> ( exp ` d ) )
54 8 elexi 
 |-  exp e. _V
55 nnex 
 |-  NN e. _V
56 55 mptex 
 |-  ( n e. NN |-> ( log ` ( A ` n ) ) ) e. _V
57 2 56 eqeltri 
 |-  B e. _V
58 54 57 coex 
 |-  ( exp o. B ) e. _V
59 58 a1i 
 |-  ( T. -> ( exp o. B ) e. _V )
60 55 mptex 
 |-  ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) e. _V
61 1 60 eqeltri 
 |-  A e. _V
62 61 a1i 
 |-  ( T. -> A e. _V )
63 1zzd 
 |-  ( T. -> 1 e. ZZ )
64 2 funmpt2 
 |-  Fun B
65 id 
 |-  ( k e. NN -> k e. NN )
66 rabid2 
 |-  ( NN = { n e. NN | ( log ` ( A ` n ) ) e. _V } <-> A. n e. NN ( log ` ( A ` n ) ) e. _V )
67 1 stirlinglem2 
 |-  ( n e. NN -> ( A ` n ) e. RR+ )
68 relogcl 
 |-  ( ( A ` n ) e. RR+ -> ( log ` ( A ` n ) ) e. RR )
69 elex 
 |-  ( ( log ` ( A ` n ) ) e. RR -> ( log ` ( A ` n ) ) e. _V )
70 67 68 69 3syl 
 |-  ( n e. NN -> ( log ` ( A ` n ) ) e. _V )
71 66 70 mprgbir 
 |-  NN = { n e. NN | ( log ` ( A ` n ) ) e. _V }
72 2 dmmpt 
 |-  dom B = { n e. NN | ( log ` ( A ` n ) ) e. _V }
73 71 72 eqtr4i 
 |-  NN = dom B
74 65 73 eleqtrdi 
 |-  ( k e. NN -> k e. dom B )
75 fvco 
 |-  ( ( Fun B /\ k e. dom B ) -> ( ( exp o. B ) ` k ) = ( exp ` ( B ` k ) ) )
76 64 74 75 sylancr 
 |-  ( k e. NN -> ( ( exp o. B ) ` k ) = ( exp ` ( B ` k ) ) )
77 1 a1i 
 |-  ( k e. NN -> A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) )
78 simpr 
 |-  ( ( k e. NN /\ n = k ) -> n = k )
79 78 fveq2d 
 |-  ( ( k e. NN /\ n = k ) -> ( ! ` n ) = ( ! ` k ) )
80 78 oveq2d 
 |-  ( ( k e. NN /\ n = k ) -> ( 2 x. n ) = ( 2 x. k ) )
81 80 fveq2d 
 |-  ( ( k e. NN /\ n = k ) -> ( sqrt ` ( 2 x. n ) ) = ( sqrt ` ( 2 x. k ) ) )
82 78 oveq1d 
 |-  ( ( k e. NN /\ n = k ) -> ( n / _e ) = ( k / _e ) )
83 82 78 oveq12d 
 |-  ( ( k e. NN /\ n = k ) -> ( ( n / _e ) ^ n ) = ( ( k / _e ) ^ k ) )
84 81 83 oveq12d 
 |-  ( ( k e. NN /\ n = k ) -> ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) = ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) )
85 79 84 oveq12d 
 |-  ( ( k e. NN /\ n = k ) -> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) = ( ( ! ` k ) / ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) ) )
86 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
87 faccl 
 |-  ( k e. NN0 -> ( ! ` k ) e. NN )
88 nncn 
 |-  ( ( ! ` k ) e. NN -> ( ! ` k ) e. CC )
89 86 87 88 3syl 
 |-  ( k e. NN -> ( ! ` k ) e. CC )
90 2cnd 
 |-  ( k e. NN -> 2 e. CC )
91 nncn 
 |-  ( k e. NN -> k e. CC )
92 90 91 mulcld 
 |-  ( k e. NN -> ( 2 x. k ) e. CC )
93 92 sqrtcld 
 |-  ( k e. NN -> ( sqrt ` ( 2 x. k ) ) e. CC )
94 20 a1i 
 |-  ( k e. NN -> _e e. CC )
95 24 a1i 
 |-  ( k e. NN -> _e =/= 0 )
96 91 94 95 divcld 
 |-  ( k e. NN -> ( k / _e ) e. CC )
97 96 86 expcld 
 |-  ( k e. NN -> ( ( k / _e ) ^ k ) e. CC )
98 93 97 mulcld 
 |-  ( k e. NN -> ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) e. CC )
99 29 a1i 
 |-  ( k e. NN -> 2 e. RR+ )
100 nnrp 
 |-  ( k e. NN -> k e. RR+ )
101 99 100 rpmulcld 
 |-  ( k e. NN -> ( 2 x. k ) e. RR+ )
102 101 sqrtgt0d 
 |-  ( k e. NN -> 0 < ( sqrt ` ( 2 x. k ) ) )
103 102 gt0ne0d 
 |-  ( k e. NN -> ( sqrt ` ( 2 x. k ) ) =/= 0 )
104 nnne0 
 |-  ( k e. NN -> k =/= 0 )
105 91 94 104 95 divne0d 
 |-  ( k e. NN -> ( k / _e ) =/= 0 )
106 nnz 
 |-  ( k e. NN -> k e. ZZ )
107 96 105 106 expne0d 
 |-  ( k e. NN -> ( ( k / _e ) ^ k ) =/= 0 )
108 93 97 103 107 mulne0d 
 |-  ( k e. NN -> ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) =/= 0 )
109 89 98 108 divcld 
 |-  ( k e. NN -> ( ( ! ` k ) / ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) ) e. CC )
110 77 85 65 109 fvmptd 
 |-  ( k e. NN -> ( A ` k ) = ( ( ! ` k ) / ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) ) )
111 110 109 eqeltrd 
 |-  ( k e. NN -> ( A ` k ) e. CC )
112 nnne0 
 |-  ( ( ! ` k ) e. NN -> ( ! ` k ) =/= 0 )
113 86 87 112 3syl 
 |-  ( k e. NN -> ( ! ` k ) =/= 0 )
114 89 98 113 108 divne0d 
 |-  ( k e. NN -> ( ( ! ` k ) / ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) ) =/= 0 )
115 110 114 eqnetrd 
 |-  ( k e. NN -> ( A ` k ) =/= 0 )
116 111 115 logcld 
 |-  ( k e. NN -> ( log ` ( A ` k ) ) e. CC )
117 nfcv 
 |-  F/_ n k
118 nfcv 
 |-  F/_ n log
119 nfmpt1 
 |-  F/_ n ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
120 1 119 nfcxfr 
 |-  F/_ n A
121 120 117 nffv 
 |-  F/_ n ( A ` k )
122 118 121 nffv 
 |-  F/_ n ( log ` ( A ` k ) )
123 2fveq3 
 |-  ( n = k -> ( log ` ( A ` n ) ) = ( log ` ( A ` k ) ) )
124 117 122 123 2 fvmptf 
 |-  ( ( k e. NN /\ ( log ` ( A ` k ) ) e. CC ) -> ( B ` k ) = ( log ` ( A ` k ) ) )
125 116 124 mpdan 
 |-  ( k e. NN -> ( B ` k ) = ( log ` ( A ` k ) ) )
126 125 fveq2d 
 |-  ( k e. NN -> ( exp ` ( B ` k ) ) = ( exp ` ( log ` ( A ` k ) ) ) )
127 eflog 
 |-  ( ( ( A ` k ) e. CC /\ ( A ` k ) =/= 0 ) -> ( exp ` ( log ` ( A ` k ) ) ) = ( A ` k ) )
128 111 115 127 syl2anc 
 |-  ( k e. NN -> ( exp ` ( log ` ( A ` k ) ) ) = ( A ` k ) )
129 76 126 128 3eqtrd 
 |-  ( k e. NN -> ( ( exp o. B ) ` k ) = ( A ` k ) )
130 129 adantl 
 |-  ( ( T. /\ k e. NN ) -> ( ( exp o. B ) ` k ) = ( A ` k ) )
131 6 59 62 63 130 climeq 
 |-  ( T. -> ( ( exp o. B ) ~~> ( exp ` d ) <-> A ~~> ( exp ` d ) ) )
132 131 mptru 
 |-  ( ( exp o. B ) ~~> ( exp ` d ) <-> A ~~> ( exp ` d ) )
133 53 132 sylib 
 |-  ( ( d e. RR /\ B ~~> d ) -> A ~~> ( exp ` d ) )
134 breq2 
 |-  ( c = ( exp ` d ) -> ( A ~~> c <-> A ~~> ( exp ` d ) ) )
135 134 rspcev 
 |-  ( ( ( exp ` d ) e. RR+ /\ A ~~> ( exp ` d ) ) -> E. c e. RR+ A ~~> c )
136 5 133 135 syl2anc 
 |-  ( ( d e. RR /\ B ~~> d ) -> E. c e. RR+ A ~~> c )
137 136 rexlimiva 
 |-  ( E. d e. RR B ~~> d -> E. c e. RR+ A ~~> c )
138 3 137 ax-mp 
 |-  E. c e. RR+ A ~~> c