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	\|- S = ( n e. NN0 \|-> ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) )
	stirlingr.2	\|- R = ( ~~>t ` ( topGen ` ran (,) ) )
Assertion	stirlingr	\|- ( n e. NN \|-> ( ( ! ` n ) / ( S ` n ) ) ) R 1

Proof

Step	Hyp	Ref	Expression
1		stirlingr.1	\|- S = ( n e. NN0 \|-> ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) )
2		stirlingr.2	\|- R = ( ~~>t ` ( topGen ` ran (,) ) )
3	1	stirling	\|- ( n e. NN \|-> ( ( ! ` n ) / ( S ` n ) ) ) ~~> 1
4		nnuz	\|- NN = ( ZZ>= ` 1 )
5		1zzd	\|- ( T. -> 1 e. ZZ )
6		eqid	\|- ( n e. NN \|-> ( ( ! ` n ) / ( S ` n ) ) ) = ( n e. NN \|-> ( ( ! ` n ) / ( S ` n ) ) )
7		nnnn0	\|- ( n e. NN -> n e. NN0 )
8		faccl	\|- ( n e. NN0 -> ( ! ` n ) e. NN )
9		nnre	\|- ( ( ! ` n ) e. NN -> ( ! ` n ) e. RR )
10	7 8 9	3syl	\|- ( n e. NN -> ( ! ` n ) e. RR )
11		2re	\|- 2 e. RR
12	11	a1i	\|- ( n e. NN -> 2 e. RR )
13		pire	\|- _pi e. RR
14	13	a1i	\|- ( n e. NN -> _pi e. RR )
15	12 14	remulcld	\|- ( n e. NN -> ( 2 x. _pi ) e. RR )
16		nnre	\|- ( n e. NN -> n e. RR )
17	15 16	remulcld	\|- ( n e. NN -> ( ( 2 x. _pi ) x. n ) e. RR )
18		0re	\|- 0 e. RR
19	18	a1i	\|- ( n e. NN -> 0 e. RR )
20		2pos	\|- 0 < 2
21	20	a1i	\|- ( n e. NN -> 0 < 2 )
22	19 12 21	ltled	\|- ( n e. NN -> 0 <_ 2 )
23		pipos	\|- 0 < _pi
24	18 13 23	ltleii	\|- 0 <_ _pi
25	24	a1i	\|- ( n e. NN -> 0 <_ _pi )
26	12 14 22 25	mulge0d	\|- ( n e. NN -> 0 <_ ( 2 x. _pi ) )
27	7	nn0ge0d	\|- ( n e. NN -> 0 <_ n )
28	15 16 26 27	mulge0d	\|- ( n e. NN -> 0 <_ ( ( 2 x. _pi ) x. n ) )
29	17 28	resqrtcld	\|- ( n e. NN -> ( sqrt ` ( ( 2 x. _pi ) x. n ) ) e. RR )
30		ere	\|- _e e. RR
31	30	a1i	\|- ( n e. NN -> _e e. RR )
32		epos	\|- 0 < _e
33	18 32	gtneii	\|- _e =/= 0
34	33	a1i	\|- ( n e. NN -> _e =/= 0 )
35	16 31 34	redivcld	\|- ( n e. NN -> ( n / _e ) e. RR )
36	35 7	reexpcld	\|- ( n e. NN -> ( ( n / _e ) ^ n ) e. RR )
37	29 36	remulcld	\|- ( n e. NN -> ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) e. RR )
38	1	fvmpt2	\|- ( ( n e. NN0 /\ ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) e. RR ) -> ( S ` n ) = ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) )
39	7 37 38	syl2anc	\|- ( n e. NN -> ( S ` n ) = ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) )
40		2rp	\|- 2 e. RR+
41	40	a1i	\|- ( n e. NN -> 2 e. RR+ )
42		pirp	\|- _pi e. RR+
43	42	a1i	\|- ( n e. NN -> _pi e. RR+ )
44	41 43	rpmulcld	\|- ( n e. NN -> ( 2 x. _pi ) e. RR+ )
45		nnrp	\|- ( n e. NN -> n e. RR+ )
46	44 45	rpmulcld	\|- ( n e. NN -> ( ( 2 x. _pi ) x. n ) e. RR+ )
47	46	rpsqrtcld	\|- ( n e. NN -> ( sqrt ` ( ( 2 x. _pi ) x. n ) ) e. RR+ )
48		epr	\|- _e e. RR+
49	48	a1i	\|- ( n e. NN -> _e e. RR+ )
50	45 49	rpdivcld	\|- ( n e. NN -> ( n / _e ) e. RR+ )
51		nnz	\|- ( n e. NN -> n e. ZZ )
52	50 51	rpexpcld	\|- ( n e. NN -> ( ( n / _e ) ^ n ) e. RR+ )
53	47 52	rpmulcld	\|- ( n e. NN -> ( ( sqrt ` ( ( 2 x. _pi ) x. n ) ) x. ( ( n / _e ) ^ n ) ) e. RR+ )
54	39 53	eqeltrd	\|- ( n e. NN -> ( S ` n ) e. RR+ )
55	10 54	rerpdivcld	\|- ( n e. NN -> ( ( ! ` n ) / ( S ` n ) ) e. RR )
56	6 55	fmpti	\|- ( n e. NN \|-> ( ( ! ` n ) / ( S ` n ) ) ) : NN --> RR
57	56	a1i	\|- ( T. -> ( n e. NN \|-> ( ( ! ` n ) / ( S ` n ) ) ) : NN --> RR )
58	2 4 5 57	climreeq	\|- ( T. -> ( ( n e. NN \|-> ( ( ! ` n ) / ( S ` n ) ) ) R 1 <-> ( n e. NN \|-> ( ( ! ` n ) / ( S ` n ) ) ) ~~> 1 ) )
59	58	mptru	\|- ( ( n e. NN \|-> ( ( ! ` n ) / ( S ` n ) ) ) R 1 <-> ( n e. NN \|-> ( ( ! ` n ) / ( S ` n ) ) ) ~~> 1 )
60	3 59	mpbir	\|- ( n e. NN \|-> ( ( ! ` n ) / ( S ` n ) ) ) R 1

Metamath Proof Explorer

Theorem stirlingr

Proof