Theorem stirlinglem14 30020

Description: The sequence A converges to a positive real. This proves that the Stirling's formula converges to the factorial, up to a constant. In another theorem, using Wallis' formula for π& , such constant is exactly determined, thus proving the Stirling's formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.)

Hypotheses

Ref	Expression
stirlinglem14.1	|- A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
stirlinglem14.2	|- B = ( n e. NN |-> ( log ` ( A ` n ) ) )

Assertion

Ref	Expression
stirlinglem14	|- E. c e. RR+ A ~~> c

Distinct variable group:   A, c

Allowed substitution hints:   A( n)   B( n, c)

Proof of Theorem stirlinglem14

Dummy variables d k are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		stirlinglem14.1	. . 3 |- A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
2		stirlinglem14.2	. . 3 |- B = ( n e. NN |-> ( log ` ( A ` n ) ) )
3	1, 2	stirlinglem13 30019	. 2 |- E. d e. RR B ~~> d
4		simpl 457	. . . . 5 |- ( ( d e. RR /\ B ~~> d ) -> d e. RR )
5	4	rpefcld 13491	. . . 4 |- ( ( d e. RR /\ B ~~> d ) -> ( exp ` d ) e. RR+ )
6		nnuz 10997	. . . . . 6 |- NN = ( ZZ>= ` 1 )
7		1z 10777	. . . . . . 7 |- 1 e. ZZ
8	7	a1i 11	. . . . . 6 |- ( ( d e. RR /\ B ~~> d ) -> 1 e. ZZ )
9		efcn 22024	. . . . . . 7 |- exp e. ( CC -cn-> CC )
10	9	a1i 11	. . . . . 6 |- ( ( d e. RR /\ B ~~> d ) -> exp e. ( CC -cn-> CC ) )
11		nnnn0 10687	. . . . . . . . . . . . 13 |- ( n e. NN -> n e. NN0 )
12		faccl 12162	. . . . . . . . . . . . 13 |- ( n e. NN0 -> ( ! ` n ) e. NN )
13		nncn 10431	. . . . . . . . . . . . 13 |- ( ( ! ` n ) e. NN -> ( ! ` n ) e. CC )
14	11, 12, 13	3syl 20	. . . . . . . . . . . 12 |- ( n e. NN -> ( ! ` n ) e. CC )
15		2cnd 10495	. . . . . . . . . . . . . . 15 |- ( n e. NN -> 2 e. CC )
16		nncn 10431	. . . . . . . . . . . . . . 15 |- ( n e. NN -> n e. CC )
17	15, 16	mulcld 9507	. . . . . . . . . . . . . 14 |- ( n e. NN -> ( 2 x. n ) e. CC )
18	17	sqrcld 13025	. . . . . . . . . . . . 13 |- ( n e. NN -> ( sqr ` ( 2 x. n ) ) e. CC )
19		epr 13592	. . . . . . . . . . . . . . . . 17 |- _e e. RR+
20		rpcn 11100	. . . . . . . . . . . . . . . . 17 |- ( _e e. RR+ -> _e e. CC )
21	19, 20	ax-mp 5	. . . . . . . . . . . . . . . 16 |- _e e. CC
22	21	a1i 11	. . . . . . . . . . . . . . 15 |- ( n e. NN -> _e e. CC )
23		0re 9487	. . . . . . . . . . . . . . . . 17 |- 0 e. RR
24		epos 13591	. . . . . . . . . . . . . . . . 17 |- 0 < _e
25	23, 24	gtneii 9587	. . . . . . . . . . . . . . . 16 |- _e =/= 0
26	25	a1i 11	. . . . . . . . . . . . . . 15 |- ( n e. NN -> _e =/= 0 )
27	16, 22, 26	divcld 10208	. . . . . . . . . . . . . 14 |- ( n e. NN -> ( n / _e ) e. CC )
28	27, 11	expcld 12109	. . . . . . . . . . . . 13 |- ( n e. NN -> ( ( n / _e ) ^ n ) e. CC )
29	18, 28	mulcld 9507	. . . . . . . . . . . 12 |- ( n e. NN -> ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) e. CC )
30		2rp 11097	. . . . . . . . . . . . . . . . 17 |- 2 e. RR+
31	30	a1i 11	. . . . . . . . . . . . . . . 16 |- ( n e. NN -> 2 e. RR+ )
32		nnrp 11101	. . . . . . . . . . . . . . . 16 |- ( n e. NN -> n e. RR+ )
33	31, 32	rpmulcld 11144	. . . . . . . . . . . . . . 15 |- ( n e. NN -> ( 2 x. n ) e. RR+ )
34	33	sqrgt0d 13001	. . . . . . . . . . . . . 14 |- ( n e. NN -> 0 < ( sqr ` ( 2 x. n ) ) )
35	34	gt0ne0d 10005	. . . . . . . . . . . . 13 |- ( n e. NN -> ( sqr ` ( 2 x. n ) ) =/= 0 )
36		nnne0 10455	. . . . . . . . . . . . . . 15 |- ( n e. NN -> n =/= 0 )
37	16, 22, 36, 26	divne0d 10224	. . . . . . . . . . . . . 14 |- ( n e. NN -> ( n / _e ) =/= 0 )
38		nnz 10769	. . . . . . . . . . . . . 14 |- ( n e. NN -> n e. ZZ )
39	27, 37, 38	expne0d 12115	. . . . . . . . . . . . 13 |- ( n e. NN -> ( ( n / _e ) ^ n ) =/= 0 )
40	18, 28, 35, 39	mulne0d 10089	. . . . . . . . . . . 12 |- ( n e. NN -> ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) =/= 0 )
41	14, 29, 40	divcld 10208	. . . . . . . . . . 11 |- ( n e. NN -> ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) e. CC )
42	1	fvmpt2 5880	. . . . . . . . . . 11 |- ( ( n e. NN /\ ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) e. CC ) -> ( A ` n ) = ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
43	41, 42	mpdan 668	. . . . . . . . . 10 |- ( n e. NN -> ( A ` n ) = ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
44	43, 41	eqeltrd 2539	. . . . . . . . 9 |- ( n e. NN -> ( A ` n ) e. CC )
45		nnne0 10455	. . . . . . . . . . . 12 |- ( ( ! ` n ) e. NN -> ( ! ` n ) =/= 0 )
46	11, 12, 45	3syl 20	. . . . . . . . . . 11 |- ( n e. NN -> ( ! ` n ) =/= 0 )
47	14, 29, 46, 40	divne0d 10224	. . . . . . . . . 10 |- ( n e. NN -> ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) =/= 0 )
48	43, 47	eqnetrd 2741	. . . . . . . . 9 |- ( n e. NN -> ( A ` n ) =/= 0 )
49	44, 48	logcld 22138	. . . . . . . 8 |- ( n e. NN -> ( log ` ( A ` n ) ) e. CC )
50	2, 49	fmpti 5965	. . . . . . 7 |- B : NN --> CC
51	50	a1i 11	. . . . . 6 |- ( ( d e. RR /\ B ~~> d ) -> B : NN --> CC )
52		simpr 461	. . . . . 6 |- ( ( d e. RR /\ B ~~> d ) -> B ~~> d )
53	4	recnd 9513	. . . . . 6 |- ( ( d e. RR /\ B ~~> d ) -> d e. CC )
54	6, 8, 10, 51, 52, 53	climcncf 20592	. . . . 5 |- ( ( d e. RR /\ B ~~> d ) -> ( exp o. B ) ~~> ( exp ` d ) )
55	9	elexi 3078	. . . . . . . . 9 |- exp e. _V
56		nnex 10429	. . . . . . . . . . 11 |- NN e. _V
57	56	mptex 6047	. . . . . . . . . 10 |- ( n e. NN |-> ( log ` ( A ` n ) ) ) e. _V
58	2, 57	eqeltri 2535	. . . . . . . . 9 |- B e. _V
59	55, 58	coex 6629	. . . . . . . 8 |- ( exp o. B ) e. _V
60	59	a1i 11	. . . . . . 7 |- ( T. -> ( exp o. B ) e. _V )
61	56	mptex 6047	. . . . . . . . 9 |- ( n e. NN |-> ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) e. _V
62	1, 61	eqeltri 2535	. . . . . . . 8 |- A e. _V
63	62	a1i 11	. . . . . . 7 |- ( T. -> A e. _V )
64	7	a1i 11	. . . . . . 7 |- ( T. -> 1 e. ZZ )
65	2	funmpt2 5553	. . . . . . . . . 10 |- Fun B
66		id 22	. . . . . . . . . . 11 |- ( k e. NN -> k e. NN )
67		rabid2 2994	. . . . . . . . . . . . 13 |- ( NN = { n e. NN | ( log ` ( A ` n ) ) e. _V } <-> A. n e. NN ( log ` ( A ` n ) ) e. _V )
68		nnrp 11101	. . . . . . . . . . . . . . . . 17 |- ( ( ! ` n ) e. NN -> ( ! ` n ) e. RR+ )
69	11, 12, 68	3syl 20	. . . . . . . . . . . . . . . 16 |- ( n e. NN -> ( ! ` n ) e. RR+ )
70	33	rpsqrcld 13000	. . . . . . . . . . . . . . . . 17 |- ( n e. NN -> ( sqr ` ( 2 x. n ) ) e. RR+ )
71	19	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( n e. NN -> _e e. RR+ )
72	32, 71	rpdivcld 11145	. . . . . . . . . . . . . . . . . 18 |- ( n e. NN -> ( n / _e ) e. RR+ )
73	72, 38	rpexpcld 12132	. . . . . . . . . . . . . . . . 17 |- ( n e. NN -> ( ( n / _e ) ^ n ) e. RR+ )
74	70, 73	rpmulcld 11144	. . . . . . . . . . . . . . . 16 |- ( n e. NN -> ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) e. RR+ )
75	69, 74	rpdivcld 11145	. . . . . . . . . . . . . . 15 |- ( n e. NN -> ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) e. RR+ )
76	43, 75	eqeltrd 2539	. . . . . . . . . . . . . 14 |- ( n e. NN -> ( A ` n ) e. RR+ )
77		relogcl 22143	. . . . . . . . . . . . . 14 |- ( ( A ` n ) e. RR+ -> ( log ` ( A ` n ) ) e. RR )
78		elex 3077	. . . . . . . . . . . . . 14 |- ( ( log ` ( A ` n ) ) e. RR -> ( log ` ( A ` n ) ) e. _V )
79	76, 77, 78	3syl 20	. . . . . . . . . . . . 13 |- ( n e. NN -> ( log ` ( A ` n ) ) e. _V )
80	67, 79	mprgbir 2894	. . . . . . . . . . . 12 |- NN = { n e. NN | ( log ` ( A ` n ) ) e. _V }
81	2	dmmpt 5431	. . . . . . . . . . . 12 |- dom B = { n e. NN | ( log ` ( A ` n ) ) e. _V }
82	80, 81	eqtr4i 2483	. . . . . . . . . . 11 |- NN = dom B
83	66, 82	syl6eleq 2549	. . . . . . . . . 10 |- ( k e. NN -> k e. dom B )
84		fvco 5866	. . . . . . . . . 10 |- ( ( Fun B /\ k e. dom B ) -> ( ( exp o. B ) ` k ) = ( exp ` ( B ` k ) ) )
85	65, 83, 84	sylancr 663	. . . . . . . . 9 |- ( k e. NN -> ( ( exp o. B ) ` k ) = ( exp ` ( B ` k ) ) )
86	1	a1i 11	. . . . . . . . . . . . . 14 |- ( k e. NN -> A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) ) )
87		simpr 461	. . . . . . . . . . . . . . . 16 |- ( ( k e. NN /\ n = k ) -> n = k )
88	87	fveq2d 5793	. . . . . . . . . . . . . . 15 |- ( ( k e. NN /\ n = k ) -> ( ! ` n ) = ( ! ` k ) )
89	87	oveq2d 6206	. . . . . . . . . . . . . . . . 17 |- ( ( k e. NN /\ n = k ) -> ( 2 x. n ) = ( 2 x. k ) )
90	89	fveq2d 5793	. . . . . . . . . . . . . . . 16 |- ( ( k e. NN /\ n = k ) -> ( sqr ` ( 2 x. n ) ) = ( sqr ` ( 2 x. k ) ) )
91	87	oveq1d 6205	. . . . . . . . . . . . . . . . 17 |- ( ( k e. NN /\ n = k ) -> ( n / _e ) = ( k / _e ) )
92	91, 87	oveq12d 6208	. . . . . . . . . . . . . . . 16 |- ( ( k e. NN /\ n = k ) -> ( ( n / _e ) ^ n ) = ( ( k / _e ) ^ k ) )
93	90, 92	oveq12d 6208	. . . . . . . . . . . . . . 15 |- ( ( k e. NN /\ n = k ) -> ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) = ( ( sqr ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) )
94	88, 93	oveq12d 6208	. . . . . . . . . . . . . 14 |- ( ( k e. NN /\ n = k ) -> ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) = ( ( ! ` k ) / ( ( sqr ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) ) )
95		nnnn0 10687	. . . . . . . . . . . . . . . 16 |- ( k e. NN -> k e. NN0 )
96		faccl 12162	. . . . . . . . . . . . . . . 16 |- ( k e. NN0 -> ( ! ` k ) e. NN )
97		nncn 10431	. . . . . . . . . . . . . . . 16 |- ( ( ! ` k ) e. NN -> ( ! ` k ) e. CC )
98	95, 96, 97	3syl 20	. . . . . . . . . . . . . . 15 |- ( k e. NN -> ( ! ` k ) e. CC )
99		2cnd 10495	. . . . . . . . . . . . . . . . . 18 |- ( k e. NN -> 2 e. CC )
100		nncn 10431	. . . . . . . . . . . . . . . . . 18 |- ( k e. NN -> k e. CC )
101	99, 100	mulcld 9507	. . . . . . . . . . . . . . . . 17 |- ( k e. NN -> ( 2 x. k ) e. CC )
102	101	sqrcld 13025	. . . . . . . . . . . . . . . 16 |- ( k e. NN -> ( sqr ` ( 2 x. k ) ) e. CC )
103	21	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( k e. NN -> _e e. CC )
104	25	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( k e. NN -> _e =/= 0 )
105	100, 103, 104	divcld 10208	. . . . . . . . . . . . . . . . 17 |- ( k e. NN -> ( k / _e ) e. CC )
106	105, 95	expcld 12109	. . . . . . . . . . . . . . . 16 |- ( k e. NN -> ( ( k / _e ) ^ k ) e. CC )
107	102, 106	mulcld 9507	. . . . . . . . . . . . . . 15 |- ( k e. NN -> ( ( sqr ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) e. CC )
108	30	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( k e. NN -> 2 e. RR+ )
109		nnrp 11101	. . . . . . . . . . . . . . . . . . 19 |- ( k e. NN -> k e. RR+ )
110	108, 109	rpmulcld 11144	. . . . . . . . . . . . . . . . . 18 |- ( k e. NN -> ( 2 x. k ) e. RR+ )
111	110	sqrgt0d 13001	. . . . . . . . . . . . . . . . 17 |- ( k e. NN -> 0 < ( sqr ` ( 2 x. k ) ) )
112	111	gt0ne0d 10005	. . . . . . . . . . . . . . . 16 |- ( k e. NN -> ( sqr ` ( 2 x. k ) ) =/= 0 )
113		nnne0 10455	. . . . . . . . . . . . . . . . . 18 |- ( k e. NN -> k =/= 0 )
114	100, 103, 113, 104	divne0d 10224	. . . . . . . . . . . . . . . . 17 |- ( k e. NN -> ( k / _e ) =/= 0 )
115		nnz 10769	. . . . . . . . . . . . . . . . 17 |- ( k e. NN -> k e. ZZ )
116	105, 114, 115	expne0d 12115	. . . . . . . . . . . . . . . 16 |- ( k e. NN -> ( ( k / _e ) ^ k ) =/= 0 )
117	102, 106, 112, 116	mulne0d 10089	. . . . . . . . . . . . . . 15 |- ( k e. NN -> ( ( sqr ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) =/= 0 )
118	98, 107, 117	divcld 10208	. . . . . . . . . . . . . 14 |- ( k e. NN -> ( ( ! ` k ) / ( ( sqr ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) ) e. CC )
119	86, 94, 66, 118	fvmptd 5878	. . . . . . . . . . . . 13 |- ( k e. NN -> ( A ` k ) = ( ( ! ` k ) / ( ( sqr ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) ) )
120	119, 118	eqeltrd 2539	. . . . . . . . . . . 12 |- ( k e. NN -> ( A ` k ) e. CC )
121		nnne0 10455	. . . . . . . . . . . . . . 15 |- ( ( ! ` k ) e. NN -> ( ! ` k ) =/= 0 )
122	95, 96, 121	3syl 20	. . . . . . . . . . . . . 14 |- ( k e. NN -> ( ! ` k ) =/= 0 )
123	98, 107, 122, 117	divne0d 10224	. . . . . . . . . . . . 13 |- ( k e. NN -> ( ( ! ` k ) / ( ( sqr ` ( 2 x. k ) ) x. ( ( k / _e ) ^ k ) ) ) =/= 0 )
124	119, 123	eqnetrd 2741	. . . . . . . . . . . 12 |- ( k e. NN -> ( A ` k ) =/= 0 )
125	120, 124	logcld 22138	. . . . . . . . . . 11 |- ( k e. NN -> ( log ` ( A ` k ) ) e. CC )
126		nfcv 2613	. . . . . . . . . . . 12 |- F/_ n k
127		nfcv 2613	. . . . . . . . . . . . 13 |- F/_ n log
128		nfmpt1 4479	. . . . . . . . . . . . . . 15 |- F/_ n ( n e. NN |-> ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )
129	1, 128	nfcxfr 2611	. . . . . . . . . . . . . 14 |- F/_ n A
130	129, 126	nffv 5796	. . . . . . . . . . . . 13 |- F/_ n ( A ` k )
131	127, 130	nffv 5796	. . . . . . . . . . . 12 |- F/_ n ( log ` ( A ` k ) )
132		fveq2 5789	. . . . . . . . . . . . 13 |- ( n = k -> ( A ` n ) = ( A ` k ) )
133	132	fveq2d 5793	. . . . . . . . . . . 12 |- ( n = k -> ( log ` ( A ` n ) ) = ( log ` ( A ` k ) ) )
134	126, 131, 133, 2	fvmptf 5889	. . . . . . . . . . 11 |- ( ( k e. NN /\ ( log ` ( A ` k ) ) e. CC ) -> ( B ` k ) = ( log ` ( A ` k ) ) )
135	125, 134	mpdan 668	. . . . . . . . . 10 |- ( k e. NN -> ( B ` k ) = ( log ` ( A ` k ) ) )
136	135	fveq2d 5793	. . . . . . . . 9 |- ( k e. NN -> ( exp ` ( B ` k ) ) = ( exp ` ( log ` ( A ` k ) ) ) )
137		eflog 22144	. . . . . . . . . 10 |- ( ( ( A ` k ) e. CC /\ ( A ` k ) =/= 0 ) -> ( exp ` ( log ` ( A ` k ) ) ) = ( A ` k ) )
138	120, 124, 137	syl2anc 661	. . . . . . . . 9 |- ( k e. NN -> ( exp ` ( log ` ( A ` k ) ) ) = ( A ` k ) )
139	85, 136, 138	3eqtrd 2496	. . . . . . . 8 |- ( k e. NN -> ( ( exp o. B ) ` k ) = ( A ` k ) )
140	139	adantl 466	. . . . . . 7 |- ( ( T. /\ k e. NN ) -> ( ( exp o. B ) ` k ) = ( A ` k ) )
141	6, 60, 63, 64, 140	climeq 13147	. . . . . 6 |- ( T. -> ( ( exp o. B ) ~~> ( exp ` d ) <-> A ~~> ( exp ` d ) ) )
142	141	trud 1379	. . . . 5 |- ( ( exp o. B ) ~~> ( exp ` d ) <-> A ~~> ( exp ` d ) )
143	54, 142	sylib 196	. . . 4 |- ( ( d e. RR /\ B ~~> d ) -> A ~~> ( exp ` d ) )
144		breq2 4394	. . . . 5 |- ( c = ( exp ` d ) -> ( A ~~> c <-> A ~~> ( exp ` d ) ) )
145	144	rspcev 3169	. . . 4 |- ( ( ( exp ` d ) e. RR+ /\ A ~~> ( exp ` d ) ) -> E. c e. RR+ A ~~> c )
146	5, 143, 145	syl2anc 661	. . 3 |- ( ( d e. RR /\ B ~~> d ) -> E. c e. RR+ A ~~> c )
147	146	rexlimiva 2932	. 2 |- ( E. d e. RR B ~~> d -> E. c e. RR+ A ~~> c )
148	3, 147	ax-mp 5	1 |- E. c e. RR+ A ~~> c

Syntax hints:   <-> wb 184   /\ wa 369   = wceq 1370   T. wtru 1371   e. wcel 1758   =/= wne 2644   E.wrex 2796   {crab 2799   _Vcvv 3068   class class class wbr 4390   |-> cmpt 4448   dom cdm 4938   o. ccom 4942   Fun wfun 5510   -->wf 5512   ` cfv 5516  (class class class)co 6190   CCcc 9381   RRcr 9382   0cc0 9383   1c1 9384   x. cmul 9388   / cdiv 10094   NNcn 10423   2c2 10472   NN0cn0 10680   ZZcz 10747   RR+crp 11092   ^cexp 11966   !cfa 12152   sqrcsqr 12824   ~~> cli 13064   expce 13449   _eceu 13450   -cn->ccncf 20568   logclog 22122

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-rep 4501  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629  ax-un 6472  ax-inf2 7948  ax-cnex 9439  ax-resscn 9440  ax-1cn 9441  ax-icn 9442  ax-addcl 9443  ax-addrcl 9444  ax-mulcl 9445  ax-mulrcl 9446  ax-mulcom 9447  ax-addass 9448  ax-mulass 9449  ax-distr 9450  ax-i2m1 9451  ax-1ne0 9452  ax-1rid 9453  ax-rnegex 9454  ax-rrecex 9455  ax-cnre 9456  ax-pre-lttri 9457  ax-pre-lttrn 9458  ax-pre-ltadd 9459  ax-pre-mulgt0 9460  ax-pre-sup 9461  ax-addf 9462  ax-mulf 9463

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-fal 1376  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-nel 2647  df-ral 2800  df-rex 2801  df-reu 2802  df-rmo 2803  df-rab 2804  df-v 3070  df-sbc 3285  df-csb 3387  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3736  df-if 3890  df-pw 3960  df-sn 3976  df-pr 3978  df-tp 3980  df-op 3982  df-uni 4190  df-int 4227  df-iun 4271  df-iin 4272  df-br 4391  df-opab 4449  df-mpt 4450  df-tr 4484  df-eprel 4730  df-id 4734  df-po 4739  df-so 4740  df-fr 4777  df-se 4778  df-we 4779  df-ord 4820  df-on 4821  df-lim 4822  df-suc 4823  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-f1 5521  df-fo 5522  df-f1o 5523  df-fv 5524  df-isom 5525  df-riota 6151  df-ov 6193  df-oprab 6194  df-mpt2 6195  df-of 6420  df-om 6577  df-1st 6677  df-2nd 6678  df-supp 6791  df-recs 6932  df-rdg 6966  df-1o 7020  df-2o 7021  df-oadd 7024  df-er 7201  df-map 7316  df-pm 7317  df-ixp 7364  df-en 7411  df-dom 7412  df-sdom 7413  df-fin 7414  df-fsupp 7722  df-fi 7762  df-sup 7792  df-oi 7825  df-card 8210  df-cda 8438  df-pnf 9521  df-mnf 9522  df-xr 9523  df-ltxr 9524  df-le 9525  df-sub 9698  df-neg 9699  df-div 10095  df-nn 10424  df-2 10481  df-3 10482  df-4 10483  df-5 10484  df-6 10485  df-7 10486  df-8 10487  df-9 10488  df-10 10489  df-n0 10681  df-z 10748  df-dec 10857  df-uz 10963  df-q 11055  df-rp 11093  df-xneg 11190  df-xadd 11191  df-xmul 11192  df-ioo 11405  df-ioc 11406  df-ico 11407  df-icc 11408  df-fz 11539  df-fzo 11650  df-fl 11743  df-mod 11810  df-seq 11908  df-exp 11967  df-fac 12153  df-bc 12180  df-hash 12205  df-shft 12658  df-cj 12690  df-re 12691  df-im 12692  df-sqr 12826  df-abs 12827  df-limsup 13051  df-clim 13068  df-rlim 13069  df-sum 13266  df-ef 13455  df-e 13456  df-sin 13457  df-cos 13458  df-tan 13459  df-pi 13460  df-dvds 13638  df-struct 14278  df-ndx 14279  df-slot 14280  df-base 14281  df-sets 14282  df-ress 14283  df-plusg 14353  df-mulr 14354  df-starv 14355  df-sca 14356  df-vsca 14357  df-ip 14358  df-tset 14359  df-ple 14360  df-ds 14362  df-unif 14363  df-hom 14364  df-cco 14365  df-rest 14463  df-topn 14464  df-0g 14482  df-gsum 14483  df-topgen 14484  df-pt 14485  df-prds 14488  df-xrs 14542  df-qtop 14547  df-imas 14548  df-xps 14550  df-mre 14626  df-mrc 14627  df-acs 14629  df-mnd 15517  df-submnd 15567  df-mulg 15650  df-cntz 15937  df-cmn 16383  df-psmet 17918  df-xmet 17919  df-met 17920  df-bl 17921  df-mopn 17922  df-fbas 17923  df-fg 17924  df-cnfld 17928  df-top 18619  df-bases 18621  df-topon 18622  df-topsp 18623  df-cld 18739  df-ntr 18740  df-cls 18741  df-nei 18818  df-lp 18856  df-perf 18857  df-cn 18947  df-cnp 18948  df-haus 19035  df-cmp 19106  df-tx 19251  df-hmeo 19444  df-fil 19535  df-fm 19627  df-flim 19628  df-flf 19629  df-xms 20011  df-ms 20012  df-tms 20013  df-cncf 20570  df-limc 21457  df-dv 21458  df-ulm 21958  df-log 22124  df-cxp 22125

This theorem is referenced by:  stirling  30022