Step |
Hyp |
Ref |
Expression |
1 |
|
stirlinglem2.1 |
|- A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) |
2 |
|
nnnn0 |
|- ( N e. NN -> N e. NN0 ) |
3 |
|
faccl |
|- ( N e. NN0 -> ( ! ` N ) e. NN ) |
4 |
|
nnrp |
|- ( ( ! ` N ) e. NN -> ( ! ` N ) e. RR+ ) |
5 |
2 3 4
|
3syl |
|- ( N e. NN -> ( ! ` N ) e. RR+ ) |
6 |
|
2rp |
|- 2 e. RR+ |
7 |
6
|
a1i |
|- ( N e. NN -> 2 e. RR+ ) |
8 |
|
nnrp |
|- ( N e. NN -> N e. RR+ ) |
9 |
7 8
|
rpmulcld |
|- ( N e. NN -> ( 2 x. N ) e. RR+ ) |
10 |
9
|
rpsqrtcld |
|- ( N e. NN -> ( sqrt ` ( 2 x. N ) ) e. RR+ ) |
11 |
|
epr |
|- _e e. RR+ |
12 |
11
|
a1i |
|- ( N e. NN -> _e e. RR+ ) |
13 |
8 12
|
rpdivcld |
|- ( N e. NN -> ( N / _e ) e. RR+ ) |
14 |
|
nnz |
|- ( N e. NN -> N e. ZZ ) |
15 |
13 14
|
rpexpcld |
|- ( N e. NN -> ( ( N / _e ) ^ N ) e. RR+ ) |
16 |
10 15
|
rpmulcld |
|- ( N e. NN -> ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) e. RR+ ) |
17 |
5 16
|
rpdivcld |
|- ( N e. NN -> ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) |
18 |
|
fveq2 |
|- ( n = k -> ( ! ` n ) = ( ! ` k ) ) |
19 |
|
oveq2 |
|- ( n = k -> ( 2 x. n ) = ( 2 x. k ) ) |
20 |
19
|
fveq2d |
|- ( n = k -> ( sqrt ` ( 2 x. n ) ) = ( sqrt ` ( 2 x. k ) ) ) |
21 |
|
oveq1 |
|- ( n = k -> ( n / _e ) = ( k / _e ) ) |
22 |
|
id |
|- ( n = k -> n = k ) |
23 |
21 22
|
oveq12d |
|- ( n = k -> ( ( n / _e ) ^ n ) = ( ( k / _e ) ^ k ) ) |
24 |
20 23
|
oveq12d |
|- ( n = k -> ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) = ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) ) |
25 |
18 24
|
oveq12d |
|- ( n = k -> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) = ( ( ! ` k ) / ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) ) ) |
26 |
25
|
cbvmptv |
|- ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) = ( k e. NN |-> ( ( ! ` k ) / ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) ) ) |
27 |
1 26
|
eqtri |
|- A = ( k e. NN |-> ( ( ! ` k ) / ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) ) ) |
28 |
27
|
a1i |
|- ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) -> A = ( k e. NN |-> ( ( ! ` k ) / ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) ) ) ) |
29 |
|
simpr |
|- ( ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) /\ k = N ) -> k = N ) |
30 |
29
|
fveq2d |
|- ( ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) /\ k = N ) -> ( ! ` k ) = ( ! ` N ) ) |
31 |
29
|
oveq2d |
|- ( ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) /\ k = N ) -> ( 2 x. k ) = ( 2 x. N ) ) |
32 |
31
|
fveq2d |
|- ( ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) /\ k = N ) -> ( sqrt ` ( 2 x. k ) ) = ( sqrt ` ( 2 x. N ) ) ) |
33 |
29
|
oveq1d |
|- ( ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) /\ k = N ) -> ( k / _e ) = ( N / _e ) ) |
34 |
33 29
|
oveq12d |
|- ( ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) /\ k = N ) -> ( ( k / _e ) ^ k ) = ( ( N / _e ) ^ N ) ) |
35 |
32 34
|
oveq12d |
|- ( ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) /\ k = N ) -> ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) = ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) |
36 |
30 35
|
oveq12d |
|- ( ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) /\ k = N ) -> ( ( ! ` k ) / ( ( sqrt ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) ) = ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) ) |
37 |
|
simpl |
|- ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) -> N e. NN ) |
38 |
|
simpr |
|- ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) -> ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) |
39 |
28 36 37 38
|
fvmptd |
|- ( ( N e. NN /\ ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) e. RR+ ) -> ( A ` N ) = ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) ) |
40 |
17 39
|
mpdan |
|- ( N e. NN -> ( A ` N ) = ( ( ! ` N ) / ( ( sqrt ` ( 2 x. N ) ) x. ( ( N / _e ) ^ N ) ) ) ) |
41 |
40 17
|
eqeltrd |
|- ( N e. NN -> ( A ` N ) e. RR+ ) |