Metamath Proof Explorer


Theorem stirlinglem2

Description: A maps to positive reals. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypothesis stirlinglem2.1
|- A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqrt ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
Assertion stirlinglem2
|- ( N e. NN -> ( A ` N ) e. RR+ )

Proof

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+ )