Metamath Proof Explorer


Theorem stirlinglem2

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

Ref Expression
Hypothesis stirlinglem2.1 𝐴 = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
Assertion stirlinglem2 ( 𝑁 ∈ ℕ → ( 𝐴𝑁 ) ∈ ℝ+ )

Proof

Step Hyp Ref Expression
1 stirlinglem2.1 𝐴 = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) )
2 nnnn0 ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
3 faccl ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℕ )
4 nnrp ( ( ! ‘ 𝑁 ) ∈ ℕ → ( ! ‘ 𝑁 ) ∈ ℝ+ )
5 2 3 4 3syl ( 𝑁 ∈ ℕ → ( ! ‘ 𝑁 ) ∈ ℝ+ )
6 2rp 2 ∈ ℝ+
7 6 a1i ( 𝑁 ∈ ℕ → 2 ∈ ℝ+ )
8 nnrp ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
9 7 8 rpmulcld ( 𝑁 ∈ ℕ → ( 2 · 𝑁 ) ∈ ℝ+ )
10 9 rpsqrtcld ( 𝑁 ∈ ℕ → ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ+ )
11 epr e ∈ ℝ+
12 11 a1i ( 𝑁 ∈ ℕ → e ∈ ℝ+ )
13 8 12 rpdivcld ( 𝑁 ∈ ℕ → ( 𝑁 / e ) ∈ ℝ+ )
14 nnz ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
15 13 14 rpexpcld ( 𝑁 ∈ ℕ → ( ( 𝑁 / e ) ↑ 𝑁 ) ∈ ℝ+ )
16 10 15 rpmulcld ( 𝑁 ∈ ℕ → ( ( √ ‘ ( 2 · 𝑁 ) ) · ( ( 𝑁 / e ) ↑ 𝑁 ) ) ∈ ℝ+ )
17 5 16 rpdivcld ( 𝑁 ∈ ℕ → ( ( ! ‘ 𝑁 ) / ( ( √ ‘ ( 2 · 𝑁 ) ) · ( ( 𝑁 / e ) ↑ 𝑁 ) ) ) ∈ ℝ+ )
18 fveq2 ( 𝑛 = 𝑘 → ( ! ‘ 𝑛 ) = ( ! ‘ 𝑘 ) )
19 oveq2 ( 𝑛 = 𝑘 → ( 2 · 𝑛 ) = ( 2 · 𝑘 ) )
20 19 fveq2d ( 𝑛 = 𝑘 → ( √ ‘ ( 2 · 𝑛 ) ) = ( √ ‘ ( 2 · 𝑘 ) ) )
21 oveq1 ( 𝑛 = 𝑘 → ( 𝑛 / e ) = ( 𝑘 / e ) )
22 id ( 𝑛 = 𝑘𝑛 = 𝑘 )
23 21 22 oveq12d ( 𝑛 = 𝑘 → ( ( 𝑛 / e ) ↑ 𝑛 ) = ( ( 𝑘 / e ) ↑ 𝑘 ) )
24 20 23 oveq12d ( 𝑛 = 𝑘 → ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) = ( ( √ ‘ ( 2 · 𝑘 ) ) · ( ( 𝑘 / e ) ↑ 𝑘 ) ) )
25 18 24 oveq12d ( 𝑛 = 𝑘 → ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) = ( ( ! ‘ 𝑘 ) / ( ( √ ‘ ( 2 · 𝑘 ) ) · ( ( 𝑘 / e ) ↑ 𝑘 ) ) ) )
26 25 cbvmptv ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( ( √ ‘ ( 2 · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( ! ‘ 𝑘 ) / ( ( √ ‘ ( 2 · 𝑘 ) ) · ( ( 𝑘 / e ) ↑ 𝑘 ) ) ) )
27 1 26 eqtri 𝐴 = ( 𝑘 ∈ ℕ ↦ ( ( ! ‘ 𝑘 ) / ( ( √ ‘ ( 2 · 𝑘 ) ) · ( ( 𝑘 / e ) ↑ 𝑘 ) ) ) )
28 27 a1i ( ( 𝑁 ∈ ℕ ∧ ( ( ! ‘ 𝑁 ) / ( ( √ ‘ ( 2 · 𝑁 ) ) · ( ( 𝑁 / e ) ↑ 𝑁 ) ) ) ∈ ℝ+ ) → 𝐴 = ( 𝑘 ∈ ℕ ↦ ( ( ! ‘ 𝑘 ) / ( ( √ ‘ ( 2 · 𝑘 ) ) · ( ( 𝑘 / e ) ↑ 𝑘 ) ) ) ) )
29 simpr ( ( ( 𝑁 ∈ ℕ ∧ ( ( ! ‘ 𝑁 ) / ( ( √ ‘ ( 2 · 𝑁 ) ) · ( ( 𝑁 / e ) ↑ 𝑁 ) ) ) ∈ ℝ+ ) ∧ 𝑘 = 𝑁 ) → 𝑘 = 𝑁 )
30 29 fveq2d ( ( ( 𝑁 ∈ ℕ ∧ ( ( ! ‘ 𝑁 ) / ( ( √ ‘ ( 2 · 𝑁 ) ) · ( ( 𝑁 / e ) ↑ 𝑁 ) ) ) ∈ ℝ+ ) ∧ 𝑘 = 𝑁 ) → ( ! ‘ 𝑘 ) = ( ! ‘ 𝑁 ) )
31 29 oveq2d ( ( ( 𝑁 ∈ ℕ ∧ ( ( ! ‘ 𝑁 ) / ( ( √ ‘ ( 2 · 𝑁 ) ) · ( ( 𝑁 / e ) ↑ 𝑁 ) ) ) ∈ ℝ+ ) ∧ 𝑘 = 𝑁 ) → ( 2 · 𝑘 ) = ( 2 · 𝑁 ) )
32 31 fveq2d ( ( ( 𝑁 ∈ ℕ ∧ ( ( ! ‘ 𝑁 ) / ( ( √ ‘ ( 2 · 𝑁 ) ) · ( ( 𝑁 / e ) ↑ 𝑁 ) ) ) ∈ ℝ+ ) ∧ 𝑘 = 𝑁 ) → ( √ ‘ ( 2 · 𝑘 ) ) = ( √ ‘ ( 2 · 𝑁 ) ) )
33 29 oveq1d ( ( ( 𝑁 ∈ ℕ ∧ ( ( ! ‘ 𝑁 ) / ( ( √ ‘ ( 2 · 𝑁 ) ) · ( ( 𝑁 / e ) ↑ 𝑁 ) ) ) ∈ ℝ+ ) ∧ 𝑘 = 𝑁 ) → ( 𝑘 / e ) = ( 𝑁 / e ) )
34 33 29 oveq12d ( ( ( 𝑁 ∈ ℕ ∧ ( ( ! ‘ 𝑁 ) / ( ( √ ‘ ( 2 · 𝑁 ) ) · ( ( 𝑁 / e ) ↑ 𝑁 ) ) ) ∈ ℝ+ ) ∧ 𝑘 = 𝑁 ) → ( ( 𝑘 / e ) ↑ 𝑘 ) = ( ( 𝑁 / e ) ↑ 𝑁 ) )
35 32 34 oveq12d ( ( ( 𝑁 ∈ ℕ ∧ ( ( ! ‘ 𝑁 ) / ( ( √ ‘ ( 2 · 𝑁 ) ) · ( ( 𝑁 / e ) ↑ 𝑁 ) ) ) ∈ ℝ+ ) ∧ 𝑘 = 𝑁 ) → ( ( √ ‘ ( 2 · 𝑘 ) ) · ( ( 𝑘 / e ) ↑ 𝑘 ) ) = ( ( √ ‘ ( 2 · 𝑁 ) ) · ( ( 𝑁 / e ) ↑ 𝑁 ) ) )
36 30 35 oveq12d ( ( ( 𝑁 ∈ ℕ ∧ ( ( ! ‘ 𝑁 ) / ( ( √ ‘ ( 2 · 𝑁 ) ) · ( ( 𝑁 / e ) ↑ 𝑁 ) ) ) ∈ ℝ+ ) ∧ 𝑘 = 𝑁 ) → ( ( ! ‘ 𝑘 ) / ( ( √ ‘ ( 2 · 𝑘 ) ) · ( ( 𝑘 / e ) ↑ 𝑘 ) ) ) = ( ( ! ‘ 𝑁 ) / ( ( √ ‘ ( 2 · 𝑁 ) ) · ( ( 𝑁 / e ) ↑ 𝑁 ) ) ) )
37 simpl ( ( 𝑁 ∈ ℕ ∧ ( ( ! ‘ 𝑁 ) / ( ( √ ‘ ( 2 · 𝑁 ) ) · ( ( 𝑁 / e ) ↑ 𝑁 ) ) ) ∈ ℝ+ ) → 𝑁 ∈ ℕ )
38 simpr ( ( 𝑁 ∈ ℕ ∧ ( ( ! ‘ 𝑁 ) / ( ( √ ‘ ( 2 · 𝑁 ) ) · ( ( 𝑁 / e ) ↑ 𝑁 ) ) ) ∈ ℝ+ ) → ( ( ! ‘ 𝑁 ) / ( ( √ ‘ ( 2 · 𝑁 ) ) · ( ( 𝑁 / e ) ↑ 𝑁 ) ) ) ∈ ℝ+ )
39 28 36 37 38 fvmptd ( ( 𝑁 ∈ ℕ ∧ ( ( ! ‘ 𝑁 ) / ( ( √ ‘ ( 2 · 𝑁 ) ) · ( ( 𝑁 / e ) ↑ 𝑁 ) ) ) ∈ ℝ+ ) → ( 𝐴𝑁 ) = ( ( ! ‘ 𝑁 ) / ( ( √ ‘ ( 2 · 𝑁 ) ) · ( ( 𝑁 / e ) ↑ 𝑁 ) ) ) )
40 17 39 mpdan ( 𝑁 ∈ ℕ → ( 𝐴𝑁 ) = ( ( ! ‘ 𝑁 ) / ( ( √ ‘ ( 2 · 𝑁 ) ) · ( ( 𝑁 / e ) ↑ 𝑁 ) ) ) )
41 40 17 eqeltrd ( 𝑁 ∈ ℕ → ( 𝐴𝑁 ) ∈ ℝ+ )