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