Metamath Proof Explorer

Theorem stirlinglem15

Description: The Stirling's formula is proven using a number of local definitions. The main theorem stirling will use this final lemma, but it will not expose the local definitions. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses stirlinglem15.1 
|- F/ n ph
stirlinglem15.2 
|- S = ( n e. NN0 |-> ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) )
stirlinglem15.3 
|- A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
stirlinglem15.4 
|- D = ( n e. NN |-> ( A ` ( 2 x. n ) ) )
stirlinglem15.5 
|- E = ( n e. NN |-> ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) )
stirlinglem15.6 
|- V = ( n e. NN |-> ( ( ( ( 2 ^ ( 4 x. n ) ) x. ( ( ! ` n ) ^ 4 ) ) / ( ( ! ` ( 2 x. n ) ) ^ 2 ) ) / ( ( 2 x. n ) + 1 ) ) )
stirlinglem15.7 
|- F = ( n e. NN |-> ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) )
stirlinglem15.8 
|- H = ( n e. NN |-> ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) )
stirlinglem15.9 
|- ( ph -> C e. RR+ )
stirlinglem15.10 
|- ( ph -> A ~~> C )
Assertion stirlinglem15 
|- ( ph -> ( n e. NN |-> ( ( ! ` n ) / ( S ` n ) ) ) ~~> 1 )

Proof

Step Hyp Ref Expression
1 stirlinglem15.1 
 |-  F/ n ph
2 stirlinglem15.2 
 |-  S = ( n e. NN0 |-> ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) )
3 stirlinglem15.3 
 |-  A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
4 stirlinglem15.4 
 |-  D = ( n e. NN |-> ( A ` ( 2 x. n ) ) )
5 stirlinglem15.5 
 |-  E = ( n e. NN |-> ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) )
6 stirlinglem15.6 
 |-  V = ( n e. NN |-> ( ( ( ( 2 ^ ( 4 x. n ) ) x. ( ( ! ` n ) ^ 4 ) ) / ( ( ! ` ( 2 x. n ) ) ^ 2 ) ) / ( ( 2 x. n ) + 1 ) ) )
7 stirlinglem15.7 
 |-  F = ( n e. NN |-> ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) )
8 stirlinglem15.8 
 |-  H = ( n e. NN |-> ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) )
9 stirlinglem15.9 
 |-  ( ph -> C e. RR+ )
10 stirlinglem15.10 
 |-  ( ph -> A ~~> C )
11 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
12 11 adantl 
 |-  ( ( ph /\ n e. NN ) -> n e. NN0 )
13 2cnd 
 |-  ( ( ph /\ n e. NN ) -> 2 e. CC )
14 picn 
 |-  _pi e. CC
15 14 a1i 
 |-  ( ( ph /\ n e. NN ) -> _pi e. CC )
16 13 15 mulcld 
 |-  ( ( ph /\ n e. NN ) -> ( 2 x. _pi ) e. CC )
17 nncn 
 |-  ( n e. NN -> n e. CC )
18 17 adantl 
 |-  ( ( ph /\ n e. NN ) -> n e. CC )
19 16 18 mulcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( 2 x. _pi ) x. n ) e. CC )
20 19 sqrtcld 
 |-  ( ( ph /\ n e. NN ) -> ( sqrt ` ( ( 2 x. _pi ) x. n ) ) e. CC )
21 ere 
 |-  _e e. RR
22 21 recni 
 |-  _e e. CC
23 22 a1i 
 |-  ( n e. NN -> _e e. CC )
24 epos 
 |-  0 < _e
25 21 24 gt0ne0ii 
 |-  _e =/= 0
26 25 a1i 
 |-  ( n e. NN -> _e =/= 0 )
27 17 23 26 divcld 
 |-  ( n e. NN -> ( n / _e ) e. CC )
28 27 11 expcld 
 |-  ( n e. NN -> ( ( n / _e ) ^ n ) e. CC )
29 28 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( ( n / _e ) ^ n ) e. CC )
30 20 29 mulcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) e. CC )
31 2 fvmpt2 
 |-  ( ( n e. NN0 /\ ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) e. CC ) -> ( S ` n ) = ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) )
32 12 30 31 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( S ` n ) = ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) )
33 32 oveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( ( ! ` n ) / ( S ` n ) ) = ( ( ! ` n ) / ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
34 15 sqrtcld 
 |-  ( ( ph /\ n e. NN ) -> ( sqrt ` _pi ) e. CC )
35 2cnd 
 |-  ( n e. NN -> 2 e. CC )
36 35 17 mulcld 
 |-  ( n e. NN -> ( 2 x. n ) e. CC )
37 36 sqrtcld 
 |-  ( n e. NN -> ( sqrt ` ( 2 x. n ) ) e. CC )
38 37 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( sqrt ` ( 2 x. n ) ) e. CC )
39 34 38 29 mulassd 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( sqrt ` _pi ) x. ( sqrt ` ( 2 x. n ) ) ) x. ( ( n / _e ) ^ n ) ) = ( ( sqrt ` _pi ) x. ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
40 nfmpt1 
 |-  F/_ n ( n e. NN |-> ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) )
41 7 40 nfcxfr 
 |-  F/_ n F
42 nfmpt1 
 |-  F/_ n ( n e. NN |-> ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) )
43 8 42 nfcxfr 
 |-  F/_ n H
44 nfmpt1 
 |-  F/_ n ( n e. NN |-> ( ( ( ( 2 ^ ( 4 x. n ) ) x. ( ( ! ` n ) ^ 4 ) ) / ( ( ! ` ( 2 x. n ) ) ^ 2 ) ) / ( ( 2 x. n ) + 1 ) ) )
45 6 44 nfcxfr 
 |-  F/_ n V
46 nnuz 
 |-  NN = ( ZZ>= ` 1 )
47 1zzd 
 |-  ( ph -> 1 e. ZZ )
48 nfmpt1 
 |-  F/_ n ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
49 3 48 nfcxfr 
 |-  F/_ n A
50 nfmpt1 
 |-  F/_ n ( n e. NN |-> ( A ` ( 2 x. n ) ) )
51 4 50 nfcxfr 
 |-  F/_ n D
52 faccl 
 |-  ( n e. NN0 -> ( ! ` n ) e. NN )
53 11 52 syl 
 |-  ( n e. NN -> ( ! ` n ) e. NN )
54 53 nnrpd 
 |-  ( n e. NN -> ( ! ` n ) e. RR+ )
55 2rp 
 |-  2 e. RR+
56 55 a1i 
 |-  ( n e. NN -> 2 e. RR+ )
57 nnrp 
 |-  ( n e. NN -> n e. RR+ )
58 56 57 rpmulcld 
 |-  ( n e. NN -> ( 2 x. n ) e. RR+ )
59 58 rpsqrtcld 
 |-  ( n e. NN -> ( sqrt ` ( 2 x. n ) ) e. RR+ )
60 epr 
 |-  _e e. RR+
61 60 a1i 
 |-  ( n e. NN -> _e e. RR+ )
62 57 61 rpdivcld 
 |-  ( n e. NN -> ( n / _e ) e. RR+ )
63 nnz 
 |-  ( n e. NN -> n e. ZZ )
64 62 63 rpexpcld 
 |-  ( n e. NN -> ( ( n / _e ) ^ n ) e. RR+ )
65 59 64 rpmulcld 
 |-  ( n e. NN -> ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) e. RR+ )
66 54 65 rpdivcld 
 |-  ( n e. NN -> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) e. RR+ )
67 3 66 fmpti 
 |-  A : NN --> RR+
68 67 a1i 
 |-  ( ph -> A : NN --> RR+ )
69 eqid 
 |-  ( n e. NN |-> ( ( A ` n ) ^ 4 ) ) = ( n e. NN |-> ( ( A ` n ) ^ 4 ) )
70 eqid 
 |-  ( n e. NN |-> ( ( D ` n ) ^ 2 ) ) = ( n e. NN |-> ( ( D ` n ) ^ 2 ) )
71 67 a1i 
 |-  ( n e. NN -> A : NN --> RR+ )
72 2nn 
 |-  2 e. NN
73 72 a1i 
 |-  ( n e. NN -> 2 e. NN )
74 id 
 |-  ( n e. NN -> n e. NN )
75 73 74 nnmulcld 
 |-  ( n e. NN -> ( 2 x. n ) e. NN )
76 71 75 ffvelcdmd 
 |-  ( n e. NN -> ( A ` ( 2 x. n ) ) e. RR+ )
77 4 fvmpt2 
 |-  ( ( n e. NN /\ ( A ` ( 2 x. n ) ) e. RR+ ) -> ( D ` n ) = ( A ` ( 2 x. n ) ) )
78 76 77 mpdan 
 |-  ( n e. NN -> ( D ` n ) = ( A ` ( 2 x. n ) ) )
79 78 76 eqeltrd 
 |-  ( n e. NN -> ( D ` n ) e. RR+ )
80 79 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( D ` n ) e. RR+ )
81 1 49 51 4 68 7 69 70 80 9 10 stirlinglem8 
 |-  ( ph -> F ~~> ( C ^ 2 ) )
82 nnex 
 |-  NN e. _V
83 82 mptex 
 |-  ( n e. NN |-> ( ( ( ( 2 ^ ( 4 x. n ) ) x. ( ( ! ` n ) ^ 4 ) ) / ( ( ! ` ( 2 x. n ) ) ^ 2 ) ) / ( ( 2 x. n ) + 1 ) ) ) e. _V
84 6 83 eqeltri 
 |-  V e. _V
85 84 a1i 
 |-  ( ph -> V e. _V )
86 eqid 
 |-  ( n e. NN |-> ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) = ( n e. NN |-> ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) )
87 eqid 
 |-  ( n e. NN |-> ( 1 / ( ( 2 x. n ) + 1 ) ) ) = ( n e. NN |-> ( 1 / ( ( 2 x. n ) + 1 ) ) )
88 eqid 
 |-  ( n e. NN |-> ( 1 / n ) ) = ( n e. NN |-> ( 1 / n ) )
89 8 86 87 88 stirlinglem1 
 |-  H ~~> ( 1 / 2 )
90 89 a1i 
 |-  ( ph -> H ~~> ( 1 / 2 ) )
91 53 nncnd 
 |-  ( n e. NN -> ( ! ` n ) e. CC )
92 37 28 mulcld 
 |-  ( n e. NN -> ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) e. CC )
93 58 sqrtgt0d 
 |-  ( n e. NN -> 0 < ( sqrt ` ( 2 x. n ) ) )
94 93 gt0ne0d 
 |-  ( n e. NN -> ( sqrt ` ( 2 x. n ) ) =/= 0 )
95 nnne0 
 |-  ( n e. NN -> n =/= 0 )
96 17 23 95 26 divne0d 
 |-  ( n e. NN -> ( n / _e ) =/= 0 )
97 27 96 63 expne0d 
 |-  ( n e. NN -> ( ( n / _e ) ^ n ) =/= 0 )
98 37 28 94 97 mulne0d 
 |-  ( n e. NN -> ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) =/= 0 )
99 91 92 98 divcld 
 |-  ( n e. NN -> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) e. CC )
100 3 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 ) ) ) )
101 99 100 mpdan 
 |-  ( n e. NN -> ( A ` n ) = ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
102 101 99 eqeltrd 
 |-  ( n e. NN -> ( A ` n ) e. CC )
103 4nn0 
 |-  4 e. NN0
104 103 a1i 
 |-  ( n e. NN -> 4 e. NN0 )
105 102 104 expcld 
 |-  ( n e. NN -> ( ( A ` n ) ^ 4 ) e. CC )
106 79 rpcnd 
 |-  ( n e. NN -> ( D ` n ) e. CC )
107 106 sqcld 
 |-  ( n e. NN -> ( ( D ` n ) ^ 2 ) e. CC )
108 79 rpne0d 
 |-  ( n e. NN -> ( D ` n ) =/= 0 )
109 2z 
 |-  2 e. ZZ
110 109 a1i 
 |-  ( n e. NN -> 2 e. ZZ )
111 106 108 110 expne0d 
 |-  ( n e. NN -> ( ( D ` n ) ^ 2 ) =/= 0 )
112 105 107 111 divcld 
 |-  ( n e. NN -> ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) e. CC )
113 7 fvmpt2 
 |-  ( ( n e. NN /\ ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) e. CC ) -> ( F ` n ) = ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) )
114 112 113 mpdan 
 |-  ( n e. NN -> ( F ` n ) = ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) )
115 114 112 eqeltrd 
 |-  ( n e. NN -> ( F ` n ) e. CC )
116 115 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) e. CC )
117 17 sqcld 
 |-  ( n e. NN -> ( n ^ 2 ) e. CC )
118 1cnd 
 |-  ( n e. NN -> 1 e. CC )
119 36 118 addcld 
 |-  ( n e. NN -> ( ( 2 x. n ) + 1 ) e. CC )
120 17 119 mulcld 
 |-  ( n e. NN -> ( n x. ( ( 2 x. n ) + 1 ) ) e. CC )
121 75 nnred 
 |-  ( n e. NN -> ( 2 x. n ) e. RR )
122 1red 
 |-  ( n e. NN -> 1 e. RR )
123 75 nngt0d 
 |-  ( n e. NN -> 0 < ( 2 x. n ) )
124 0lt1 
 |-  0 < 1
125 124 a1i 
 |-  ( n e. NN -> 0 < 1 )
126 121 122 123 125 addgt0d 
 |-  ( n e. NN -> 0 < ( ( 2 x. n ) + 1 ) )
127 126 gt0ne0d 
 |-  ( n e. NN -> ( ( 2 x. n ) + 1 ) =/= 0 )
128 17 119 95 127 mulne0d 
 |-  ( n e. NN -> ( n x. ( ( 2 x. n ) + 1 ) ) =/= 0 )
129 117 120 128 divcld 
 |-  ( n e. NN -> ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) e. CC )
130 8 fvmpt2 
 |-  ( ( n e. NN /\ ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) e. CC ) -> ( H ` n ) = ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) )
131 129 130 mpdan 
 |-  ( n e. NN -> ( H ` n ) = ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) )
132 131 129 eqeltrd 
 |-  ( n e. NN -> ( H ` n ) e. CC )
133 132 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( H ` n ) e. CC )
134 112 129 mulcld 
 |-  ( n e. NN -> ( ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) x. ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) ) e. CC )
135 3 4 5 6 stirlinglem3 
 |-  V = ( n e. NN |-> ( ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) x. ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) ) )
136 135 fvmpt2 
 |-  ( ( n e. NN /\ ( ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) x. ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) ) e. CC ) -> ( V ` n ) = ( ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) x. ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) ) )
137 134 136 mpdan 
 |-  ( n e. NN -> ( V ` n ) = ( ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) x. ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) ) )
138 114 131 oveq12d 
 |-  ( n e. NN -> ( ( F ` n ) x. ( H ` n ) ) = ( ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) x. ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) ) )
139 137 138 eqtr4d 
 |-  ( n e. NN -> ( V ` n ) = ( ( F ` n ) x. ( H ` n ) ) )
140 139 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( V ` n ) = ( ( F ` n ) x. ( H ` n ) ) )
141 1 41 43 45 46 47 81 85 90 116 133 140 climmulf 
 |-  ( ph -> V ~~> ( ( C ^ 2 ) x. ( 1 / 2 ) ) )
142 6 wallispi2 
 |-  V ~~> ( _pi / 2 )
143 climuni 
 |-  ( ( V ~~> ( ( C ^ 2 ) x. ( 1 / 2 ) ) /\ V ~~> ( _pi / 2 ) ) -> ( ( C ^ 2 ) x. ( 1 / 2 ) ) = ( _pi / 2 ) )
144 141 142 143 sylancl 
 |-  ( ph -> ( ( C ^ 2 ) x. ( 1 / 2 ) ) = ( _pi / 2 ) )
145 144 oveq1d 
 |-  ( ph -> ( ( ( C ^ 2 ) x. ( 1 / 2 ) ) / ( 1 / 2 ) ) = ( ( _pi / 2 ) / ( 1 / 2 ) ) )
146 9 rpcnd 
 |-  ( ph -> C e. CC )
147 146 sqcld 
 |-  ( ph -> ( C ^ 2 ) e. CC )
148 1cnd 
 |-  ( ph -> 1 e. CC )
149 148 halfcld 
 |-  ( ph -> ( 1 / 2 ) e. CC )
150 2cnd 
 |-  ( ph -> 2 e. CC )
151 2pos 
 |-  0 < 2
152 151 a1i 
 |-  ( ph -> 0 < 2 )
153 152 gt0ne0d 
 |-  ( ph -> 2 =/= 0 )
154 150 153 recne0d 
 |-  ( ph -> ( 1 / 2 ) =/= 0 )
155 147 149 154 divcan4d 
 |-  ( ph -> ( ( ( C ^ 2 ) x. ( 1 / 2 ) ) / ( 1 / 2 ) ) = ( C ^ 2 ) )
156 14 a1i 
 |-  ( ph -> _pi e. CC )
157 124 a1i 
 |-  ( ph -> 0 < 1 )
158 157 gt0ne0d 
 |-  ( ph -> 1 =/= 0 )
159 156 148 150 158 153 divcan7d 
 |-  ( ph -> ( ( _pi / 2 ) / ( 1 / 2 ) ) = ( _pi / 1 ) )
160 156 div1d 
 |-  ( ph -> ( _pi / 1 ) = _pi )
161 159 160 eqtrd 
 |-  ( ph -> ( ( _pi / 2 ) / ( 1 / 2 ) ) = _pi )
162 145 155 161 3eqtr3d 
 |-  ( ph -> ( C ^ 2 ) = _pi )
163 162 fveq2d 
 |-  ( ph -> ( sqrt ` ( C ^ 2 ) ) = ( sqrt ` _pi ) )
164 9 rprege0d 
 |-  ( ph -> ( C e. RR /\ 0 <_ C ) )
165 sqrtsq 
 |-  ( ( C e. RR /\ 0 <_ C ) -> ( sqrt ` ( C ^ 2 ) ) = C )
166 164 165 syl 
 |-  ( ph -> ( sqrt ` ( C ^ 2 ) ) = C )
167 163 166 eqtr3d 
 |-  ( ph -> ( sqrt ` _pi ) = C )
168 167 adantr 
 |-  ( ( ph /\ n e. NN ) -> ( sqrt ` _pi ) = C )
169 168 oveq1d 
 |-  ( ( ph /\ n e. NN ) -> ( ( sqrt ` _pi ) x. ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) = ( C x. ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
170 146 adantr 
 |-  ( ( ph /\ n e. NN ) -> C e. CC )
171 92 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) e. CC )
172 170 171 mulcomd 
 |-  ( ( ph /\ n e. NN ) -> ( C x. ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) = ( ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) x. C ) )
173 39 169 172 3eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( sqrt ` _pi ) x. ( sqrt ` ( 2 x. n ) ) ) x. ( ( n / _e ) ^ n ) ) = ( ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) x. C ) )
174 173 oveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( ( ! ` n ) / ( ( ( sqrt ` _pi ) x. ( sqrt ` ( 2 x. n ) ) ) x. ( ( n / _e ) ^ n ) ) ) = ( ( ! ` n ) / ( ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) x. C ) ) )
175 2re 
 |-  2 e. RR
176 175 a1i 
 |-  ( ( ph /\ n e. NN ) -> 2 e. RR )
177 pire 
 |-  _pi e. RR
178 177 a1i 
 |-  ( ( ph /\ n e. NN ) -> _pi e. RR )
179 176 178 remulcld 
 |-  ( ( ph /\ n e. NN ) -> ( 2 x. _pi ) e. RR )
180 0le2 
 |-  0 <_ 2
181 180 a1i 
 |-  ( ( ph /\ n e. NN ) -> 0 <_ 2 )
182 0re 
 |-  0 e. RR
183 pipos 
 |-  0 < _pi
184 182 177 183 ltleii 
 |-  0 <_ _pi
185 184 a1i 
 |-  ( ( ph /\ n e. NN ) -> 0 <_ _pi )
186 176 178 181 185 mulge0d 
 |-  ( ( ph /\ n e. NN ) -> 0 <_ ( 2 x. _pi ) )
187 12 nn0red 
 |-  ( ( ph /\ n e. NN ) -> n e. RR )
188 12 nn0ge0d 
 |-  ( ( ph /\ n e. NN ) -> 0 <_ n )
189 179 186 187 188 sqrtmuld 
 |-  ( ( ph /\ n e. NN ) -> ( sqrt ` ( ( 2 x. _pi ) x. n ) ) = ( ( sqrt ` ( 2 x. _pi ) ) x. ( sqrt ` n ) ) )
190 176 181 178 185 sqrtmuld 
 |-  ( ( ph /\ n e. NN ) -> ( sqrt ` ( 2 x. _pi ) ) = ( ( sqrt ` 2 ) x. ( sqrt ` _pi ) ) )
191 190 oveq1d 
 |-  ( ( ph /\ n e. NN ) -> ( ( sqrt ` ( 2 x. _pi ) ) x. ( sqrt ` n ) ) = ( ( ( sqrt ` 2 ) x. ( sqrt ` _pi ) ) x. ( sqrt ` n ) ) )
192 13 sqrtcld 
 |-  ( ( ph /\ n e. NN ) -> ( sqrt ` 2 ) e. CC )
193 18 sqrtcld 
 |-  ( ( ph /\ n e. NN ) -> ( sqrt ` n ) e. CC )
194 192 34 193 mulassd 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( sqrt ` 2 ) x. ( sqrt ` _pi ) ) x. ( sqrt ` n ) ) = ( ( sqrt ` 2 ) x. ( ( sqrt ` _pi ) x. ( sqrt ` n ) ) ) )
195 192 34 193 mul12d 
 |-  ( ( ph /\ n e. NN ) -> ( ( sqrt ` 2 ) x. ( ( sqrt ` _pi ) x. ( sqrt ` n ) ) ) = ( ( sqrt ` _pi ) x. ( ( sqrt ` 2 ) x. ( sqrt ` n ) ) ) )
196 176 181 187 188 sqrtmuld 
 |-  ( ( ph /\ n e. NN ) -> ( sqrt ` ( 2 x. n ) ) = ( ( sqrt ` 2 ) x. ( sqrt ` n ) ) )
197 196 eqcomd 
 |-  ( ( ph /\ n e. NN ) -> ( ( sqrt ` 2 ) x. ( sqrt ` n ) ) = ( sqrt ` ( 2 x. n ) ) )
198 197 oveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( ( sqrt ` _pi ) x. ( ( sqrt ` 2 ) x. ( sqrt ` n ) ) ) = ( ( sqrt ` _pi ) x. ( sqrt ` ( 2 x. n ) ) ) )
199 195 198 eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( ( sqrt ` 2 ) x. ( ( sqrt ` _pi ) x. ( sqrt ` n ) ) ) = ( ( sqrt ` _pi ) x. ( sqrt ` ( 2 x. n ) ) ) )
200 191 194 199 3eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( ( sqrt ` ( 2 x. _pi ) ) x. ( sqrt ` n ) ) = ( ( sqrt ` _pi ) x. ( sqrt ` ( 2 x. n ) ) ) )
201 189 200 eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( sqrt ` ( ( 2 x. _pi ) x. n ) ) = ( ( sqrt ` _pi ) x. ( sqrt ` ( 2 x. n ) ) ) )
202 201 oveq1d 
 |-  ( ( ph /\ n e. NN ) -> ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) = ( ( ( sqrt ` _pi ) x. ( sqrt ` ( 2 x. n ) ) ) x. ( ( n / _e ) ^ n ) ) )
203 202 oveq2d 
 |-  ( ( ph /\ n e. NN ) -> ( ( ! ` n ) / ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) ) = ( ( ! ` n ) / ( ( ( sqrt ` _pi ) x. ( sqrt ` ( 2 x. n ) ) ) x. ( ( n / _e ) ^ n ) ) ) )
204 91 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( ! ` n ) e. CC )
205 94 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( sqrt ` ( 2 x. n ) ) =/= 0 )
206 22 a1i 
 |-  ( ( ph /\ n e. NN ) -> _e e. CC )
207 25 a1i 
 |-  ( ( ph /\ n e. NN ) -> _e =/= 0 )
208 18 206 207 divcld 
 |-  ( ( ph /\ n e. NN ) -> ( n / _e ) e. CC )
209 95 adantl 
 |-  ( ( ph /\ n e. NN ) -> n =/= 0 )
210 18 206 209 207 divne0d 
 |-  ( ( ph /\ n e. NN ) -> ( n / _e ) =/= 0 )
211 63 adantl 
 |-  ( ( ph /\ n e. NN ) -> n e. ZZ )
212 208 210 211 expne0d 
 |-  ( ( ph /\ n e. NN ) -> ( ( n / _e ) ^ n ) =/= 0 )
213 38 29 205 212 mulne0d 
 |-  ( ( ph /\ n e. NN ) -> ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) =/= 0 )
214 9 rpne0d 
 |-  ( ph -> C =/= 0 )
215 214 adantr 
 |-  ( ( ph /\ n e. NN ) -> C =/= 0 )
216 204 171 170 213 215 divdiv1d 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) / C ) = ( ( ! ` n ) / ( ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) x. C ) ) )
217 174 203 216 3eqtr4d 
 |-  ( ( ph /\ n e. NN ) -> ( ( ! ` n ) / ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) ) = ( ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) / C ) )
218 99 ancli 
 |-  ( n e. NN -> ( n e. NN /\ ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) e. CC ) )
219 218 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( n e. NN /\ ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) e. CC ) )
220 219 100 syl 
 |-  ( ( ph /\ n e. NN ) -> ( A ` n ) = ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
221 220 eqcomd 
 |-  ( ( ph /\ n e. NN ) -> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) = ( A ` n ) )
222 221 oveq1d 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) / C ) = ( ( A ` n ) / C ) )
223 33 217 222 3eqtrd 
 |-  ( ( ph /\ n e. NN ) -> ( ( ! ` n ) / ( S ` n ) ) = ( ( A ` n ) / C ) )
224 1 223 mpteq2da 
 |-  ( ph -> ( n e. NN |-> ( ( ! ` n ) / ( S ` n ) ) ) = ( n e. NN |-> ( ( A ` n ) / C ) ) )
225 102 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( A ` n ) e. CC )
226 225 170 215 divrec2d 
 |-  ( ( ph /\ n e. NN ) -> ( ( A ` n ) / C ) = ( ( 1 / C ) x. ( A ` n ) ) )
227 1 226 mpteq2da 
 |-  ( ph -> ( n e. NN |-> ( ( A ` n ) / C ) ) = ( n e. NN |-> ( ( 1 / C ) x. ( A ` n ) ) ) )
228 146 214 reccld 
 |-  ( ph -> ( 1 / C ) e. CC )
229 82 mptex 
 |-  ( n e. NN |-> ( ( 1 / C ) x. ( A ` n ) ) ) e. _V
230 229 a1i 
 |-  ( ph -> ( n e. NN |-> ( ( 1 / C ) x. ( A ` n ) ) ) e. _V )
231 3 a1i 
 |-  ( k e. NN -> A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) )
232 simpr 
 |-  ( ( k e. NN /\ n = k ) -> n = k )
233 232 fveq2d 
 |-  ( ( k e. NN /\ n = k ) -> ( ! ` n ) = ( ! ` k ) )
234 232 oveq2d 
 |-  ( ( k e. NN /\ n = k ) -> ( 2 x. n ) = ( 2 x. k ) )
235 234 fveq2d 
 |-  ( ( k e. NN /\ n = k ) -> ( sqrt ` ( 2 x. n ) ) = ( sqrt ` ( 2 x. k ) ) )
236 232 oveq1d 
 |-  ( ( k e. NN /\ n = k ) -> ( n / _e ) = ( k / _e ) )
237 236 232 oveq12d 
 |-  ( ( k e. NN /\ n = k ) -> ( ( n / _e ) ^ n ) = ( ( k / _e ) ^ k ) )
238 235 237 oveq12d 
 |-  ( ( k e. NN /\ n = k ) -> ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) = ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) )
239 233 238 oveq12d 
 |-  ( ( k e. NN /\ n = k ) -> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) = ( ( ! ` k ) / ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) ) )
240 id 
 |-  ( k e. NN -> k e. NN )
241 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
242 faccl 
 |-  ( k e. NN0 -> ( ! ` k ) e. NN )
243 nncn 
 |-  ( ( ! ` k ) e. NN -> ( ! ` k ) e. CC )
244 241 242 243 3syl 
 |-  ( k e. NN -> ( ! ` k ) e. CC )
245 2cnd 
 |-  ( k e. NN -> 2 e. CC )
246 nncn 
 |-  ( k e. NN -> k e. CC )
247 245 246 mulcld 
 |-  ( k e. NN -> ( 2 x. k ) e. CC )
248 247 sqrtcld 
 |-  ( k e. NN -> ( sqrt ` ( 2 x. k ) ) e. CC )
249 22 a1i 
 |-  ( k e. NN -> _e e. CC )
250 25 a1i 
 |-  ( k e. NN -> _e =/= 0 )
251 246 249 250 divcld 
 |-  ( k e. NN -> ( k / _e ) e. CC )
252 251 241 expcld 
 |-  ( k e. NN -> ( ( k / _e ) ^ k ) e. CC )
253 248 252 mulcld 
 |-  ( k e. NN -> ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) e. CC )
254 55 a1i 
 |-  ( k e. NN -> 2 e. RR+ )
255 nnrp 
 |-  ( k e. NN -> k e. RR+ )
256 254 255 rpmulcld 
 |-  ( k e. NN -> ( 2 x. k ) e. RR+ )
257 256 sqrtgt0d 
 |-  ( k e. NN -> 0 < ( sqrt ` ( 2 x. k ) ) )
258 257 gt0ne0d 
 |-  ( k e. NN -> ( sqrt ` ( 2 x. k ) ) =/= 0 )
259 nnne0 
 |-  ( k e. NN -> k =/= 0 )
260 246 249 259 250 divne0d 
 |-  ( k e. NN -> ( k / _e ) =/= 0 )
261 nnz 
 |-  ( k e. NN -> k e. ZZ )
262 251 260 261 expne0d 
 |-  ( k e. NN -> ( ( k / _e ) ^ k ) =/= 0 )
263 248 252 258 262 mulne0d 
 |-  ( k e. NN -> ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) =/= 0 )
264 244 253 263 divcld 
 |-  ( k e. NN -> ( ( ! ` k ) / ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) ) e. CC )
265 231 239 240 264 fvmptd 
 |-  ( k e. NN -> ( A ` k ) = ( ( ! ` k ) / ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) ) )
266 265 264 eqeltrd 
 |-  ( k e. NN -> ( A ` k ) e. CC )
267 266 adantl 
 |-  ( ( ph /\ k e. NN ) -> ( A ` k ) e. CC )
268 nfcv 
 |-  F/_ k ( ( 1 / C ) x. ( A ` n ) )
269 nfcv 
 |-  F/_ n 1
270 nfcv 
 |-  F/_ n /
271 nfcv 
 |-  F/_ n C
272 269 270 271 nfov 
 |-  F/_ n ( 1 / C )
273 nfcv 
 |-  F/_ n x.
274 nfcv 
 |-  F/_ n k
275 49 274 nffv 
 |-  F/_ n ( A ` k )
276 272 273 275 nfov 
 |-  F/_ n ( ( 1 / C ) x. ( A ` k ) )
277 fveq2 
 |-  ( n = k -> ( A ` n ) = ( A ` k ) )
278 277 oveq2d 
 |-  ( n = k -> ( ( 1 / C ) x. ( A ` n ) ) = ( ( 1 / C ) x. ( A ` k ) ) )
279 268 276 278 cbvmpt 
 |-  ( n e. NN |-> ( ( 1 / C ) x. ( A ` n ) ) ) = ( k e. NN |-> ( ( 1 / C ) x. ( A ` k ) ) )
280 279 a1i 
 |-  ( ( ph /\ k e. NN ) -> ( n e. NN |-> ( ( 1 / C ) x. ( A ` n ) ) ) = ( k e. NN |-> ( ( 1 / C ) x. ( A ` k ) ) ) )
281 280 fveq1d 
 |-  ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( ( 1 / C ) x. ( A ` n ) ) ) ` k ) = ( ( k e. NN |-> ( ( 1 / C ) x. ( A ` k ) ) ) ` k ) )
282 simpr 
 |-  ( ( ph /\ k e. NN ) -> k e. NN )
283 146 adantr 
 |-  ( ( ph /\ k e. NN ) -> C e. CC )
284 214 adantr 
 |-  ( ( ph /\ k e. NN ) -> C =/= 0 )
285 283 284 reccld 
 |-  ( ( ph /\ k e. NN ) -> ( 1 / C ) e. CC )
286 285 267 mulcld 
 |-  ( ( ph /\ k e. NN ) -> ( ( 1 / C ) x. ( A ` k ) ) e. CC )
287 eqid 
 |-  ( k e. NN |-> ( ( 1 / C ) x. ( A ` k ) ) ) = ( k e. NN |-> ( ( 1 / C ) x. ( A ` k ) ) )
288 287 fvmpt2 
 |-  ( ( k e. NN /\ ( ( 1 / C ) x. ( A ` k ) ) e. CC ) -> ( ( k e. NN |-> ( ( 1 / C ) x. ( A ` k ) ) ) ` k ) = ( ( 1 / C ) x. ( A ` k ) ) )
289 282 286 288 syl2anc 
 |-  ( ( ph /\ k e. NN ) -> ( ( k e. NN |-> ( ( 1 / C ) x. ( A ` k ) ) ) ` k ) = ( ( 1 / C ) x. ( A ` k ) ) )
290 281 289 eqtrd 
 |-  ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( ( 1 / C ) x. ( A ` n ) ) ) ` k ) = ( ( 1 / C ) x. ( A ` k ) ) )
291 46 47 10 228 230 267 290 climmulc2 
 |-  ( ph -> ( n e. NN |-> ( ( 1 / C ) x. ( A ` n ) ) ) ~~> ( ( 1 / C ) x. C ) )
292 146 214 recid2d 
 |-  ( ph -> ( ( 1 / C ) x. C ) = 1 )
293 291 292 breqtrd 
 |-  ( ph -> ( n e. NN |-> ( ( 1 / C ) x. ( A ` n ) ) ) ~~> 1 )
294 227 293 eqbrtrd 
 |-  ( ph -> ( n e. NN |-> ( ( A ` n ) / C ) ) ~~> 1 )
295 224 294 eqbrtrd 
 |-  ( ph -> ( n e. NN |-> ( ( ! ` n ) / ( S ` n ) ) ) ~~> 1 )