Theorem stirlingr

Description: Stirling's approximation formula for n factorial: here convergence is expressed with respect to the standard topology on the reals. The main theorem stirling is proven for convergence in the topology of complex numbers. The variable R is used to denote convergence with respect to the standard topology on the reals. (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypotheses	stirlingr.1	⊢ 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) )
	stirlingr.2	⊢ 𝑅 = ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) )
Assertion	stirlingr	⊢ ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) ) 𝑅 1

Proof

Step	Hyp	Ref	Expression
1		stirlingr.1	⊢ 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) )
2		stirlingr.2	⊢ 𝑅 = ( ⇝𝑡 ‘ ( topGen ‘ ran (,) ) )
3	1	stirling	⊢ ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) ) ⇝ 1
4		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
5		1zzd	⊢ ( ⊤ → 1 ∈ ℤ )
6		eqid	⊢ ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) )
7		nnnn0	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
8		faccl	⊢ ( 𝑛 ∈ ℕ0 → ( ! ‘ 𝑛 ) ∈ ℕ )
9		nnre	⊢ ( ( ! ‘ 𝑛 ) ∈ ℕ → ( ! ‘ 𝑛 ) ∈ ℝ )
10	7 8 9	3syl	⊢ ( 𝑛 ∈ ℕ → ( ! ‘ 𝑛 ) ∈ ℝ )
11		2re	⊢ 2 ∈ ℝ
12	11	a1i	⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℝ )
13		pire	⊢ π ∈ ℝ
14	13	a1i	⊢ ( 𝑛 ∈ ℕ → π ∈ ℝ )
15	12 14	remulcld	⊢ ( 𝑛 ∈ ℕ → ( 2 · π ) ∈ ℝ )
16		nnre	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ )
17	15 16	remulcld	⊢ ( 𝑛 ∈ ℕ → ( ( 2 · π ) · 𝑛 ) ∈ ℝ )
18		0re	⊢ 0 ∈ ℝ
19	18	a1i	⊢ ( 𝑛 ∈ ℕ → 0 ∈ ℝ )
20		2pos	⊢ 0 < 2
21	20	a1i	⊢ ( 𝑛 ∈ ℕ → 0 < 2 )
22	19 12 21	ltled	⊢ ( 𝑛 ∈ ℕ → 0 ≤ 2 )
23		pipos	⊢ 0 < π
24	18 13 23	ltleii	⊢ 0 ≤ π
25	24	a1i	⊢ ( 𝑛 ∈ ℕ → 0 ≤ π )
26	12 14 22 25	mulge0d	⊢ ( 𝑛 ∈ ℕ → 0 ≤ ( 2 · π ) )
27	7	nn0ge0d	⊢ ( 𝑛 ∈ ℕ → 0 ≤ 𝑛 )
28	15 16 26 27	mulge0d	⊢ ( 𝑛 ∈ ℕ → 0 ≤ ( ( 2 · π ) · 𝑛 ) )
29	17 28	resqrtcld	⊢ ( 𝑛 ∈ ℕ → ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) ∈ ℝ )
30		ere	⊢ e ∈ ℝ
31	30	a1i	⊢ ( 𝑛 ∈ ℕ → e ∈ ℝ )
32		epos	⊢ 0 < e
33	18 32	gtneii	⊢ e ≠ 0
34	33	a1i	⊢ ( 𝑛 ∈ ℕ → e ≠ 0 )
35	16 31 34	redivcld	⊢ ( 𝑛 ∈ ℕ → ( 𝑛 / e ) ∈ ℝ )
36	35 7	reexpcld	⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 / e ) ↑ 𝑛 ) ∈ ℝ )
37	29 36	remulcld	⊢ ( 𝑛 ∈ ℕ → ( ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ∈ ℝ )
38	1	fvmpt2	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ∈ ℝ ) → ( 𝑆 ‘ 𝑛 ) = ( ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) )
39	7 37 38	syl2anc	⊢ ( 𝑛 ∈ ℕ → ( 𝑆 ‘ 𝑛 ) = ( ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) )
40		2rp	⊢ 2 ∈ ℝ+
41	40	a1i	⊢ ( 𝑛 ∈ ℕ → 2 ∈ ℝ+ )
42		pirp	⊢ π ∈ ℝ+
43	42	a1i	⊢ ( 𝑛 ∈ ℕ → π ∈ ℝ+ )
44	41 43	rpmulcld	⊢ ( 𝑛 ∈ ℕ → ( 2 · π ) ∈ ℝ+ )
45		nnrp	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ+ )
46	44 45	rpmulcld	⊢ ( 𝑛 ∈ ℕ → ( ( 2 · π ) · 𝑛 ) ∈ ℝ+ )
47	46	rpsqrtcld	⊢ ( 𝑛 ∈ ℕ → ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) ∈ ℝ+ )
48		epr	⊢ e ∈ ℝ+
49	48	a1i	⊢ ( 𝑛 ∈ ℕ → e ∈ ℝ+ )
50	45 49	rpdivcld	⊢ ( 𝑛 ∈ ℕ → ( 𝑛 / e ) ∈ ℝ+ )
51		nnz	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℤ )
52	50 51	rpexpcld	⊢ ( 𝑛 ∈ ℕ → ( ( 𝑛 / e ) ↑ 𝑛 ) ∈ ℝ+ )
53	47 52	rpmulcld	⊢ ( 𝑛 ∈ ℕ → ( ( √ ‘ ( ( 2 · π ) · 𝑛 ) ) · ( ( 𝑛 / e ) ↑ 𝑛 ) ) ∈ ℝ+ )
54	39 53	eqeltrd	⊢ ( 𝑛 ∈ ℕ → ( 𝑆 ‘ 𝑛 ) ∈ ℝ+ )
55	10 54	rerpdivcld	⊢ ( 𝑛 ∈ ℕ → ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) ∈ ℝ )
56	6 55	fmpti	⊢ ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) ) : ℕ ⟶ ℝ
57	56	a1i	⊢ ( ⊤ → ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) ) : ℕ ⟶ ℝ )
58	2 4 5 57	climreeq	⊢ ( ⊤ → ( ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) ) 𝑅 1 ↔ ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) ) ⇝ 1 ) )
59	58	mptru	⊢ ( ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) ) 𝑅 1 ↔ ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) ) ⇝ 1 )
60	3 59	mpbir	⊢ ( 𝑛 ∈ ℕ ↦ ( ( ! ‘ 𝑛 ) / ( 𝑆 ‘ 𝑛 ) ) ) 𝑅 1