This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝑁 ∈ ℕ → ( 𝐴 ‘ 𝑁 ) ∈ ℝ+ )