stirlinglem3 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > stirlinglem3		Structured version Unicode version

Theorem stirlinglem3 37226

Description: Long but simple algebraic transformations are applied to show that

, the Wallis formula for π , can be expressed in terms of

, the Stirling's approximation formula for the factorial, up to a constant factor. This will allow (in a later theorem) to determine the right constant factor to be put into the

, in order to get the exact Stirling's formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.)

**Hypotheses**
Ref	Expression
stirlinglem3.1
stirlinglem3.2
stirlinglem3.3
stirlinglem3.4

**Assertion**
Ref	Expression
stirlinglem3

Proof of Theorem stirlinglem3 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		stirlinglem3.4	. 2
2		nnnn0 10843	. . . . . . . . . . . . 13
3		faccl 12407	. . . . . . . . . . . . 13
4		nncn 10584	. . . . . . . . . . . . 13
5	2, 3, 4	3syl 18	. . . . . . . . . . . 12
6		2cnd 10649	. . . . . . . . . . . . . . 15
7		nncn 10584	. . . . . . . . . . . . . . 15
8	6, 7	mulcld 9646	. . . . . . . . . . . . . 14
9	8	sqrtcld 13417	. . . . . . . . . . . . 13
10		ere 14033	. . . . . . . . . . . . . . . . 17
11	10	recni 9638	. . . . . . . . . . . . . . . 16
12	11	a1i 11	. . . . . . . . . . . . . . 15
13		epos 14149	. . . . . . . . . . . . . . . . 17
14	10, 13	gt0ne0ii 10129	. . . . . . . . . . . . . . . 16
15	14	a1i 11	. . . . . . . . . . . . . . 15
16	7, 12, 15	divcld 10361	. . . . . . . . . . . . . 14
17	16, 2	expcld 12354	. . . . . . . . . . . . 13
18	9, 17	mulcld 9646	. . . . . . . . . . . 12
19		2rp 11270	. . . . . . . . . . . . . . . . 17
20	19	a1i 11	. . . . . . . . . . . . . . . 16
21		nnrp 11274	. . . . . . . . . . . . . . . 16
22	20, 21	rpmulcld 11320	. . . . . . . . . . . . . . 15
23	22	sqrtgt0d 13393	. . . . . . . . . . . . . 14
24	23	gt0ne0d 10157	. . . . . . . . . . . . 13
25		nnne0 10609	. . . . . . . . . . . . . . 15
26	7, 12, 25, 15	divne0d 10377	. . . . . . . . . . . . . 14
27		nnz 10927	. . . . . . . . . . . . . 14
28	16, 26, 27	expne0d 12360	. . . . . . . . . . . . 13
29	9, 17, 24, 28	mulne0d 10242	. . . . . . . . . . . 12
30	5, 18, 29	divcld 10361	. . . . . . . . . . 11
31		stirlinglem3.1	. . . . . . . . . . . 12
32	31	fvmpt2 5941	. . . . . . . . . . 11 $/\$
33	30, 32	mpdan 666	. . . . . . . . . 10
34	33	oveq1d 6293	. . . . . . . . 9
35		stirlinglem3.3	. . . . . . . . . . . 12
36	35	fvmpt2 5941	. . . . . . . . . . 11 $/\$
37	18, 36	mpdan 666	. . . . . . . . . 10
38	37	oveq1d 6293	. . . . . . . . 9
39	34, 38	oveq12d 6296	. . . . . . . 8
40		4nn0 10855	. . . . . . . . . . 11
41	40	a1i 11	. . . . . . . . . 10
42	5, 18, 29, 41	expdivd 12368	. . . . . . . . 9
43	42	oveq1d 6293	. . . . . . . 8
44	5, 41	expcld 12354	. . . . . . . . 9
45	18, 41	expcld 12354	. . . . . . . . 9
46	41	nn0zd 11006	. . . . . . . . . 10
47	18, 29, 46	expne0d 12360	. . . . . . . . 9
48	44, 45, 47	divcan1d 10362	. . . . . . . 8
49	39, 43, 48	3eqtrd 2447	. . . . . . 7
50	49	eqcomd 2410	. . . . . 6
51	50	oveq2d 6294	. . . . 5
52		2nn0 10853	. . . . . . . . . . . . 13
53	52	a1i 11	. . . . . . . . . . . 12
54	53, 2	nn0mulcld 10898	. . . . . . . . . . 11
55		faccl 12407	. . . . . . . . . . 11
56		nncn 10584	. . . . . . . . . . 11
57	54, 55, 56	3syl 18	. . . . . . . . . 10
58	57	sqcld 12352	. . . . . . . . 9
59	6, 8	mulcld 9646	. . . . . . . . . . . 12
60	59	sqrtcld 13417	. . . . . . . . . . 11
61	8, 12, 15	divcld 10361	. . . . . . . . . . . 12
62	61, 54	expcld 12354	. . . . . . . . . . 11
63	60, 62	mulcld 9646	. . . . . . . . . 10
64	63	sqcld 12352	. . . . . . . . 9
65	20, 22	rpmulcld 11320	. . . . . . . . . . . . 13
66	65	sqrtgt0d 13393	. . . . . . . . . . . 12
67	66	gt0ne0d 10157	. . . . . . . . . . 11
68	20	rpne0d 11309	. . . . . . . . . . . . . 14
69	6, 7, 68, 25	mulne0d 10242	. . . . . . . . . . . . 13
70	8, 12, 69, 15	divne0d 10377	. . . . . . . . . . . 12
71		2z 10937	. . . . . . . . . . . . . 14
72	71	a1i 11	. . . . . . . . . . . . 13
73	72, 27	zmulcld 11014	. . . . . . . . . . . 12
74	61, 70, 73	expne0d 12360	. . . . . . . . . . 11
75	60, 62, 67, 74	mulne0d 10242	. . . . . . . . . 10
76	63, 75, 72	expne0d 12360	. . . . . . . . 9
77	58, 64, 76	divcan1d 10362	. . . . . . . 8
78	57, 63, 75, 53	expdivd 12368	. . . . . . . . . 10
79	78	eqcomd 2410	. . . . . . . . 9
80	79	oveq1d 6293	. . . . . . . 8
81	77, 80	eqtr3d 2445	. . . . . . 7
82		fveq2 5849	. . . . . . . . . . . . . . 15
83		oveq2 6286	. . . . . . . . . . . . . . . . 17
84	83	fveq2d 5853	. . . . . . . . . . . . . . . 16
85		oveq1 6285	. . . . . . . . . . . . . . . . 17
86		id 22	. . . . . . . . . . . . . . . . 17
87	85, 86	oveq12d 6296	. . . . . . . . . . . . . . . 16
88	84, 87	oveq12d 6296	. . . . . . . . . . . . . . 15
89	82, 88	oveq12d 6296	. . . . . . . . . . . . . 14
90	89	cbvmptv 4487	. . . . . . . . . . . . 13
91	31, 90	eqtri 2431	. . . . . . . . . . . 12
92	91	a1i 11	. . . . . . . . . . 11
93		fveq2 5849	. . . . . . . . . . . . 13
94		oveq2 6286	. . . . . . . . . . . . . . 15
95	94	fveq2d 5853	. . . . . . . . . . . . . 14
96		oveq1 6285	. . . . . . . . . . . . . . 15
97		id 22	. . . . . . . . . . . . . . 15
98	96, 97	oveq12d 6296	. . . . . . . . . . . . . 14
99	95, 98	oveq12d 6296	. . . . . . . . . . . . 13
100	93, 99	oveq12d 6296	. . . . . . . . . . . 12
101	100	adantl 464	. . . . . . . . . . 11 $/\$
102		2nn 10734	. . . . . . . . . . . . 13
103	102	a1i 11	. . . . . . . . . . . 12
104		id 22	. . . . . . . . . . . 12
105	103, 104	nnmulcld 10624	. . . . . . . . . . 11
106	57, 63, 75	divcld 10361	. . . . . . . . . . 11
107	92, 101, 105, 106	fvmptd 5938	. . . . . . . . . 10
108	107	oveq1d 6293	. . . . . . . . 9
109	108	eqcomd 2410	. . . . . . . 8
110	109	oveq1d 6293	. . . . . . 7
111		eqidd 2403	. . . . . . . . . . 11
112	99	adantl 464	. . . . . . . . . . 11 $/\$
113	111, 112, 105, 63	fvmptd 5938	. . . . . . . . . 10
114	113	oveq1d 6293	. . . . . . . . 9
115	114	eqcomd 2410	. . . . . . . 8
116	115	oveq2d 6294	. . . . . . 7
117	81, 110, 116	3eqtrd 2447	. . . . . 6
118	88	cbvmptv 4487	. . . . . . . . . . 11
119	118	a1i 11	. . . . . . . . . 10
120	119	fveq1d 5851	. . . . . . . . 9
121	120	eqcomd 2410	. . . . . . . 8
122	121	oveq1d 6293	. . . . . . 7
123	122	oveq2d 6294	. . . . . 6
124	107, 106	eqeltrd 2490	. . . . . . . . . 10
125		stirlinglem3.2	. . . . . . . . . . 11
126	125	fvmpt2 5941	. . . . . . . . . 10 $/\$
127	124, 126	mpdan 666	. . . . . . . . 9
128	127	eqcomd 2410	. . . . . . . 8
129	128	oveq1d 6293	. . . . . . 7
130	35	a1i 11	. . . . . . . . . 10
131	130	fveq1d 5851	. . . . . . . . 9
132	131	eqcomd 2410	. . . . . . . 8
133	132	oveq1d 6293	. . . . . . 7
134	129, 133	oveq12d 6296	. . . . . 6
135	117, 123, 134	3eqtrd 2447	. . . . 5
136	51, 135	oveq12d 6296	. . . 4
137	136	oveq1d 6293	. . 3
138	137	mpteq2ia 4477	. 2
139	41, 2	nn0mulcld 10898	. . . . . . . 8
140	6, 139	expcld 12354	. . . . . . 7
141	49, 44	eqeltrd 2490	. . . . . . 7
142	140, 141	mulcomd 9647	. . . . . 6
143	142	oveq1d 6293	. . . . 5
144	143	oveq1d 6293	. . . 4
145	127, 124	eqeltrd 2490	. . . . . . . 8
146	145	sqcld 12352	. . . . . . 7
147	130, 119	eqtrd 2443	. . . . . . . . . 10
148	147, 112, 105, 63	fvmptd 5938	. . . . . . . . 9
149	148, 63	eqeltrd 2490	. . . . . . . 8
150	149	sqcld 12352	. . . . . . 7
151		nnne0 10609	. . . . . . . . . . . 12
152	54, 55, 151	3syl 18	. . . . . . . . . . 11
153	57, 63, 152, 75	divne0d 10377	. . . . . . . . . 10
154	107, 153	eqnetrd 2696	. . . . . . . . 9
155	127, 154	eqnetrd 2696	. . . . . . . 8
156	145, 155, 72	expne0d 12360	. . . . . . 7
157	148, 75	eqnetrd 2696	. . . . . . . 8
158	149, 157, 72	expne0d 12360	. . . . . . 7
159	141, 146, 140, 150, 156, 158	divmuldivd 10402	. . . . . 6
160	159	eqcomd 2410	. . . . 5
161	160	oveq1d 6293	. . . 4
162	33, 30	eqeltrd 2490	. . . . . . . . 9
163	162, 41	expcld 12354	. . . . . . . 8
164	38, 45	eqeltrd 2490	. . . . . . . 8
165	163, 164, 146, 156	div23d 10398	. . . . . . 7
166	165	oveq1d 6293	. . . . . 6
167	166	oveq1d 6293	. . . . 5
168	163, 146, 156	divcld 10361	. . . . . . 7
169	140, 150, 158	divcld 10361	. . . . . . 7
170	168, 164, 169	mulassd 9649	. . . . . 6
171	170	oveq1d 6293	. . . . 5
172	164, 169	mulcld 9646	. . . . . . 7
173		1cnd 9642	. . . . . . . 8
174	8, 173	addcld 9645	. . . . . . 7
175		0red 9627	. . . . . . . . 9
176	105	nnred 10591	. . . . . . . . 9
177		2re 10646	. . . . . . . . . . . 12
178	177	a1i 11	. . . . . . . . . . 11
179		nnre 10583	. . . . . . . . . . 11
180	178, 179	remulcld 9654	. . . . . . . . . 10
181		1red 9641	. . . . . . . . . 10
182	180, 181	readdcld 9653	. . . . . . . . 9
183	105	nngt0d 10620	. . . . . . . . 9
184	176	ltp1d 10516	. . . . . . . . 9
185	175, 176, 182, 183, 184	lttrd 9777	. . . . . . . 8
186	185	gt0ne0d 10157	. . . . . . 7
187	168, 172, 174, 186	divassd 10396	. . . . . 6
188	164, 140, 150, 158	div12d 10397	. . . . . . . . . 10
189	9, 17, 41	mulexpd 12369	. . . . . . . . . . . . 13
190	60, 62	sqmuld 12366	. . . . . . . . . . . . 13
191	189, 190	oveq12d 6296	. . . . . . . . . . . 12
192	148	oveq1d 6293	. . . . . . . . . . . . 13
193	38, 192	oveq12d 6296	. . . . . . . . . . . 12
194	9, 41	expcld 12354	. . . . . . . . . . . . 13
195	60	sqcld 12352	. . . . . . . . . . . . 13
196	17, 41	expcld 12354	. . . . . . . . . . . . 13
197	62	sqcld 12352	. . . . . . . . . . . . 13
198	60, 67, 72	expne0d 12360	. . . . . . . . . . . . 13
199	62, 74, 72	expne0d 12360	. . . . . . . . . . . . 13
200	194, 195, 196, 197, 198, 199	divmuldivd 10402	. . . . . . . . . . . 12
201	191, 193, 200	3eqtr4d 2453	. . . . . . . . . . 11
202	201	oveq2d 6294	. . . . . . . . . 10
203	65	rprege0d 11311	. . . . . . . . . . . . . . . 16 $/\$
204		resqrtth 13238	. . . . . . . . . . . . . . . 16 $/\$
205	203, 204	syl 17	. . . . . . . . . . . . . . 15
206	205	oveq2d 6294	. . . . . . . . . . . . . 14
207		2t2e4 10726	. . . . . . . . . . . . . . . . . . 19
208	207	eqcomi 2415	. . . . . . . . . . . . . . . . . 18
209	208	a1i 11	. . . . . . . . . . . . . . . . 17
210	209	oveq2d 6294	. . . . . . . . . . . . . . . 16
211	9, 53, 53	expmuld 12357	. . . . . . . . . . . . . . . 16
212	22	rprege0d 11311	. . . . . . . . . . . . . . . . . 18 $/\$
213		resqrtth 13238	. . . . . . . . . . . . . . . . . 18 $/\$
214	212, 213	syl 17	. . . . . . . . . . . . . . . . 17
215	214	oveq1d 6293	. . . . . . . . . . . . . . . 16
216	210, 211, 215	3eqtrd 2447	. . . . . . . . . . . . . . 15
217	6, 6, 7	mulassd 9649	. . . . . . . . . . . . . . . 16
218	207	a1i 11	. . . . . . . . . . . . . . . . 17
219	218	oveq1d 6293	. . . . . . . . . . . . . . . 16
220	217, 219	eqtr3d 2445	. . . . . . . . . . . . . . 15
221	216, 220	oveq12d 6296	. . . . . . . . . . . . . 14
222	6, 7	sqmuld 12366	. . . . . . . . . . . . . . . . 17
223		sq2 12309	. . . . . . . . . . . . . . . . . . 19
224	223	a1i 11	. . . . . . . . . . . . . . . . . 18
225	224	oveq1d 6293	. . . . . . . . . . . . . . . . 17
226	222, 225	eqtrd 2443	. . . . . . . . . . . . . . . 16
227	226	oveq1d 6293	. . . . . . . . . . . . . . 15
228		4cn 10654	. . . . . . . . . . . . . . . . . . 19
229		4ne0 10673	. . . . . . . . . . . . . . . . . . 19
230	228, 229	dividi 10318	. . . . . . . . . . . . . . . . . 18
231	230	a1i 11	. . . . . . . . . . . . . . . . 17
232	7	sqvald 12351	. . . . . . . . . . . . . . . . . . 19
233	232	oveq1d 6293	. . . . . . . . . . . . . . . . . 18
234	7, 7, 25	divcan4d 10367	. . . . . . . . . . . . . . . . . 18
235	233, 234	eqtrd 2443	. . . . . . . . . . . . . . . . 17
236	231, 235	oveq12d 6296	. . . . . . . . . . . . . . . 16
237	41	nn0cnd 10895	. . . . . . . . . . . . . . . . 17
238	7	sqcld 12352	. . . . . . . . . . . . . . . . 17
239	229	a1i 11	. . . . . . . . . . . . . . . . 17
240	237, 237, 238, 7, 239, 25	divmuldivd 10402	. . . . . . . . . . . . . . . 16
241	7	mulid2d 9644	. . . . . . . . . . . . . . . 16
242	236, 240, 241	3eqtr3d 2451	. . . . . . . . . . . . . . 15
243	227, 242	eqtrd 2443	. . . . . . . . . . . . . 14
244	206, 221, 243	3eqtrd 2447	. . . . . . . . . . . . 13
245	7, 237	mulcomd 9647	. . . . . . . . . . . . . . . . 17
246	245	oveq2d 6294	. . . . . . . . . . . . . . . 16
247	16, 41, 2	expmuld 12357	. . . . . . . . . . . . . . . 16
248	7, 12, 15, 139	expdivd 12368	. . . . . . . . . . . . . . . 16
249	246, 247, 248	3eqtr3d 2451	. . . . . . . . . . . . . . 15
250	6, 7, 6	mul32d 9824	. . . . . . . . . . . . . . . . . 18
251	250, 219	eqtrd 2443	. . . . . . . . . . . . . . . . 17
252	251	oveq2d 6294	. . . . . . . . . . . . . . . 16
253	61, 53, 54	expmuld 12357	. . . . . . . . . . . . . . . 16
254	8, 12, 15, 139	expdivd 12368	. . . . . . . . . . . . . . . 16
255	252, 253, 254	3eqtr3d 2451	. . . . . . . . . . . . . . 15
256	249, 255	oveq12d 6296	. . . . . . . . . . . . . 14
257	249, 196	eqeltrrd 2491	. . . . . . . . . . . . . . 15
258	8, 139	expcld 12354	. . . . . . . . . . . . . . 15
259	12, 139	expcld 12354	. . . . . . . . . . . . . . 15
260	46, 27	zmulcld 11014	. . . . . . . . . . . . . . . 16
261	8, 69, 260	expne0d 12360	. . . . . . . . . . . . . . 15
262	12, 15, 260	expne0d 12360	. . . . . . . . . . . . . . 15
263	257, 258, 259, 261, 262	divdiv2d 10393	. . . . . . . . . . . . . 14
264	7, 139	expcld 12354	. . . . . . . . . . . . . . . . 17
265	264, 259, 262	divcan1d 10362	. . . . . . . . . . . . . . . 16
266	265	oveq1d 6293	. . . . . . . . . . . . . . 15
267	6, 7, 139	mulexpd 12369	. . . . . . . . . . . . . . . 16
268	267	oveq2d 6294	. . . . . . . . . . . . . . 15
269	140, 264	mulcomd 9647	. . . . . . . . . . . . . . . . 17
270	269	oveq2d 6294	. . . . . . . . . . . . . . . 16
271	7, 25, 260	expne0d 12360	. . . . . . . . . . . . . . . . 17
272	6, 68, 260	expne0d 12360	. . . . . . . . . . . . . . . . 17
273	264, 264, 140, 271, 272	divdiv1d 10392	. . . . . . . . . . . . . . . 16
274	264, 271	dividd 10359	. . . . . . . . . . . . . . . . 17
275	274	oveq1d 6293	. . . . . . . . . . . . . . . 16
276	270, 273, 275	3eqtr2d 2449	. . . . . . . . . . . . . . 15
277	266, 268, 276	3eqtrd 2447	. . . . . . . . . . . . . 14
278	256, 263, 277	3eqtrd 2447	. . . . . . . . . . . . 13
279	244, 278	oveq12d 6296	. . . . . . . . . . . 12
280	279	oveq2d 6294	. . . . . . . . . . 11
281	140, 272	reccld 10354	. . . . . . . . . . . 12
282	140, 7, 281	mul12d 9823	. . . . . . . . . . 11
283	7	mulid1d 9643	. . . . . . . . . . . 12
284	140, 272	recidd 10356	. . . . . . . . . . . . 13
285	284	oveq2d 6294	. . . . . . . . . . . 12
286	283, 285, 235	3eqtr4d 2453	. . . . . . . . . . 11
287	280, 282, 286	3eqtrd 2447	. . . . . . . . . 10
288	188, 202, 287	3eqtrd 2447	. . . . . . . . 9
289	288	oveq1d 6293	. . . . . . . 8
290	238, 7, 174, 25, 186	divdiv1d 10392	. . . . . . . 8
291	289, 290	eqtrd 2443	. . . . . . 7
292	291	oveq2d 6294	. . . . . 6
293	187, 292	eqtrd 2443	. . . . 5
294	167, 171, 293	3eqtrd 2447	. . . 4
295	144, 161, 294	3eqtrd 2447	. . 3
296	295	mpteq2ia 4477	. 2
297	1, 138, 296	3eqtri 2435	1

Colors of variables: wff setvar class

Syntax hints: $/\$ wa 367

wceq 1405

wcel 1842

wne 2598 class class class wbr 4395

cmpt 4453

cfv 5569 (class class class)co 6278

cc 9520

cr 9521

cc0 9522

c1 9523

caddc 9525

cmul 9527

cle 9659

cdiv 10247

cn 10576

c2 10626

c4 10628

cn0 10836

cz 10905

crp 11265

cexp 12210

cfa 12397

csqrt 13215

ceu 14007

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1639 ax-4 1652 ax-5 1725 ax-6 1771 ax-7 1814 ax-8 1844 ax-9 1846 ax-10 1861 ax-11 1866 ax-12 1878 ax-13 2026 ax-ext 2380 ax-rep 4507 ax-sep 4517 ax-nul 4525 ax-pow 4572 ax-pr 4630 ax-un 6574 ax-inf2 8091 ax-cnex 9578 ax-resscn 9579 ax-1cn 9580 ax-icn 9581 ax-addcl 9582 ax-addrcl 9583 ax-mulcl 9584 ax-mulrcl 9585 ax-mulcom 9586 ax-addass 9587 ax-mulass 9588 ax-distr 9589 ax-i2m1 9590 ax-1ne0 9591 ax-1rid 9592 ax-rnegex 9593 ax-rrecex 9594 ax-cnre 9595 ax-pre-lttri 9596 ax-pre-lttrn 9597 ax-pre-ltadd 9598 ax-pre-mulgt0 9599 ax-pre-sup 9600 ax-addf 9601 ax-mulf 9602

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 975 df-3an 976 df-tru 1408 df-fal 1411 df-ex 1634 df-nf 1638 df-sb 1764 df-eu 2242 df-mo 2243 df-clab 2388 df-cleq 2394 df-clel 2397 df-nfc 2552 df-ne 2600 df-nel 2601 df-ral 2759 df-rex 2760 df-reu 2761 df-rmo 2762 df-rab 2763 df-v 3061 df-sbc 3278 df-csb 3374 df-dif 3417 df-un 3419 df-in 3421 df-ss 3428 df-pss 3430 df-nul 3739 df-if 3886 df-pw 3957 df-sn 3973 df-pr 3975 df-tp 3977 df-op 3979 df-uni 4192 df-int 4228 df-iun 4273 df-br 4396 df-opab 4454 df-mpt 4455 df-tr 4490 df-eprel 4734 df-id 4738 df-po 4744 df-so 4745 df-fr 4782 df-se 4783 df-we 4784 df-xp 4829 df-rel 4830 df-cnv 4831 df-co 4832 df-dm 4833 df-rn 4834 df-res 4835 df-ima 4836 df-pred 5367 df-ord 5413 df-on 5414 df-lim 5415 df-suc 5416 df-iota 5533 df-fun 5571 df-fn 5572 df-f 5573 df-f1 5574 df-fo 5575 df-f1o 5576 df-fv 5577 df-isom 5578 df-riota 6240 df-ov 6281 df-oprab 6282 df-mpt2 6283 df-om 6684 df-1st 6784 df-2nd 6785 df-wrecs 7013 df-recs 7075 df-rdg 7113 df-1o 7167 df-oadd 7171 df-er 7348 df-pm 7460 df-en 7555 df-dom 7556 df-sdom 7557 df-fin 7558 df-sup 7935 df-oi 7969 df-card 8352 df-pnf 9660 df-mnf 9661 df-xr 9662 df-ltxr 9663 df-le 9664 df-sub 9843 df-neg 9844 df-div 10248 df-nn 10577 df-2 10635 df-3 10636 df-4 10637 df-n0 10837 df-z 10906 df-uz 11128 df-q 11228 df-rp 11266 df-ico 11588 df-fz 11727 df-fzo 11855 df-fl 11966 df-seq 12152 df-exp 12211 df-fac 12398 df-bc 12425 df-hash 12453 df-shft 13049 df-cj 13081 df-re 13082 df-im 13083 df-sqrt 13217 df-abs 13218 df-limsup 13443 df-clim 13460 df-rlim 13461 df-sum 13658 df-ef 14012 df-e 14013

This theorem is referenced by: stirlinglem15 37238

W3C validator