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