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 37758

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 10877	. . . . . . . . . . . . 13
3		faccl 12469	. . . . . . . . . . . . 13
4		nncn 10618	. . . . . . . . . . . . 13
5	2, 3, 4	3syl 18	. . . . . . . . . . . 12
6		2cnd 10683	. . . . . . . . . . . . . . 15
7		nncn 10618	. . . . . . . . . . . . . . 15
8	6, 7	mulcld 9664	. . . . . . . . . . . . . 14
9	8	sqrtcld 13487	. . . . . . . . . . . . 13
10		ere 14131	. . . . . . . . . . . . . . . . 17
11	10	recni 9656	. . . . . . . . . . . . . . . 16
12	11	a1i 11	. . . . . . . . . . . . . . 15
13		epos 14247	. . . . . . . . . . . . . . . . 17
14	10, 13	gt0ne0ii 10151	. . . . . . . . . . . . . . . 16
15	14	a1i 11	. . . . . . . . . . . . . . 15
16	7, 12, 15	divcld 10384	. . . . . . . . . . . . . 14
17	16, 2	expcld 12416	. . . . . . . . . . . . 13
18	9, 17	mulcld 9664	. . . . . . . . . . . 12
19		2rp 11308	. . . . . . . . . . . . . . . . 17
20	19	a1i 11	. . . . . . . . . . . . . . . 16
21		nnrp 11312	. . . . . . . . . . . . . . . 16
22	20, 21	rpmulcld 11358	. . . . . . . . . . . . . . 15
23	22	sqrtgt0d 13463	. . . . . . . . . . . . . 14
24	23	gt0ne0d 10179	. . . . . . . . . . . . 13
25		nnne0 10643	. . . . . . . . . . . . . . 15
26	7, 12, 25, 15	divne0d 10400	. . . . . . . . . . . . . 14
27		nnz 10960	. . . . . . . . . . . . . 14
28	16, 26, 27	expne0d 12422	. . . . . . . . . . . . 13
29	9, 17, 24, 28	mulne0d 10265	. . . . . . . . . . . 12
30	5, 18, 29	divcld 10384	. . . . . . . . . . 11
31		stirlinglem3.1	. . . . . . . . . . . 12
32	31	fvmpt2 5970	. . . . . . . . . . 11 $/\$
33	30, 32	mpdan 672	. . . . . . . . . 10
34	33	oveq1d 6317	. . . . . . . . 9
35		stirlinglem3.3	. . . . . . . . . . . 12
36	35	fvmpt2 5970	. . . . . . . . . . 11 $/\$
37	18, 36	mpdan 672	. . . . . . . . . 10
38	37	oveq1d 6317	. . . . . . . . 9
39	34, 38	oveq12d 6320	. . . . . . . 8
40		4nn0 10889	. . . . . . . . . . 11
41	40	a1i 11	. . . . . . . . . 10
42	5, 18, 29, 41	expdivd 12430	. . . . . . . . 9
43	42	oveq1d 6317	. . . . . . . 8
44	5, 41	expcld 12416	. . . . . . . . 9
45	18, 41	expcld 12416	. . . . . . . . 9
46	41	nn0zd 11039	. . . . . . . . . 10
47	18, 29, 46	expne0d 12422	. . . . . . . . 9
48	44, 45, 47	divcan1d 10385	. . . . . . . 8
49	39, 43, 48	3eqtrd 2467	. . . . . . 7
50	49	eqcomd 2430	. . . . . 6
51	50	oveq2d 6318	. . . . 5
52		2nn0 10887	. . . . . . . . . . . . 13
53	52	a1i 11	. . . . . . . . . . . 12
54	53, 2	nn0mulcld 10931	. . . . . . . . . . 11
55		faccl 12469	. . . . . . . . . . 11
56		nncn 10618	. . . . . . . . . . 11
57	54, 55, 56	3syl 18	. . . . . . . . . 10
58	57	sqcld 12414	. . . . . . . . 9
59	6, 8	mulcld 9664	. . . . . . . . . . . 12
60	59	sqrtcld 13487	. . . . . . . . . . 11
61	8, 12, 15	divcld 10384	. . . . . . . . . . . 12
62	61, 54	expcld 12416	. . . . . . . . . . 11
63	60, 62	mulcld 9664	. . . . . . . . . 10
64	63	sqcld 12414	. . . . . . . . 9
65	20, 22	rpmulcld 11358	. . . . . . . . . . . . 13
66	65	sqrtgt0d 13463	. . . . . . . . . . . 12
67	66	gt0ne0d 10179	. . . . . . . . . . 11
68	20	rpne0d 11347	. . . . . . . . . . . . . 14
69	6, 7, 68, 25	mulne0d 10265	. . . . . . . . . . . . 13
70	8, 12, 69, 15	divne0d 10400	. . . . . . . . . . . 12
71		2z 10970	. . . . . . . . . . . . . 14
72	71	a1i 11	. . . . . . . . . . . . 13
73	72, 27	zmulcld 11047	. . . . . . . . . . . 12
74	61, 70, 73	expne0d 12422	. . . . . . . . . . 11
75	60, 62, 67, 74	mulne0d 10265	. . . . . . . . . 10
76	63, 75, 72	expne0d 12422	. . . . . . . . 9
77	58, 64, 76	divcan1d 10385	. . . . . . . 8
78	57, 63, 75, 53	expdivd 12430	. . . . . . . . . 10
79	78	eqcomd 2430	. . . . . . . . 9
80	79	oveq1d 6317	. . . . . . . 8
81	77, 80	eqtr3d 2465	. . . . . . 7
82		fveq2 5878	. . . . . . . . . . . . . . 15
83		oveq2 6310	. . . . . . . . . . . . . . . . 17
84	83	fveq2d 5882	. . . . . . . . . . . . . . . 16
85		oveq1 6309	. . . . . . . . . . . . . . . . 17
86		id 23	. . . . . . . . . . . . . . . . 17
87	85, 86	oveq12d 6320	. . . . . . . . . . . . . . . 16
88	84, 87	oveq12d 6320	. . . . . . . . . . . . . . 15
89	82, 88	oveq12d 6320	. . . . . . . . . . . . . 14
90	89	cbvmptv 4513	. . . . . . . . . . . . 13
91	31, 90	eqtri 2451	. . . . . . . . . . . 12
92	91	a1i 11	. . . . . . . . . . 11
93		fveq2 5878	. . . . . . . . . . . . 13
94		oveq2 6310	. . . . . . . . . . . . . . 15
95	94	fveq2d 5882	. . . . . . . . . . . . . 14
96		oveq1 6309	. . . . . . . . . . . . . . 15
97		id 23	. . . . . . . . . . . . . . 15
98	96, 97	oveq12d 6320	. . . . . . . . . . . . . 14
99	95, 98	oveq12d 6320	. . . . . . . . . . . . 13
100	93, 99	oveq12d 6320	. . . . . . . . . . . 12
101	100	adantl 467	. . . . . . . . . . 11 $/\$
102		2nn 10768	. . . . . . . . . . . . 13
103	102	a1i 11	. . . . . . . . . . . 12
104		id 23	. . . . . . . . . . . 12
105	103, 104	nnmulcld 10658	. . . . . . . . . . 11
106	57, 63, 75	divcld 10384	. . . . . . . . . . 11
107	92, 101, 105, 106	fvmptd 5967	. . . . . . . . . 10
108	107	oveq1d 6317	. . . . . . . . 9
109	108	eqcomd 2430	. . . . . . . 8
110	109	oveq1d 6317	. . . . . . 7
111		eqidd 2423	. . . . . . . . . . 11
112	99	adantl 467	. . . . . . . . . . 11 $/\$
113	111, 112, 105, 63	fvmptd 5967	. . . . . . . . . 10
114	113	oveq1d 6317	. . . . . . . . 9
115	114	eqcomd 2430	. . . . . . . 8
116	115	oveq2d 6318	. . . . . . 7
117	81, 110, 116	3eqtrd 2467	. . . . . 6
118	88	cbvmptv 4513	. . . . . . . . . . 11
119	118	a1i 11	. . . . . . . . . 10
120	119	fveq1d 5880	. . . . . . . . 9
121	120	eqcomd 2430	. . . . . . . 8
122	121	oveq1d 6317	. . . . . . 7
123	122	oveq2d 6318	. . . . . 6
124	107, 106	eqeltrd 2510	. . . . . . . . . 10
125		stirlinglem3.2	. . . . . . . . . . 11
126	125	fvmpt2 5970	. . . . . . . . . 10 $/\$
127	124, 126	mpdan 672	. . . . . . . . 9
128	127	eqcomd 2430	. . . . . . . 8
129	128	oveq1d 6317	. . . . . . 7
130	35	a1i 11	. . . . . . . . . 10
131	130	fveq1d 5880	. . . . . . . . 9
132	131	eqcomd 2430	. . . . . . . 8
133	132	oveq1d 6317	. . . . . . 7
134	129, 133	oveq12d 6320	. . . . . 6
135	117, 123, 134	3eqtrd 2467	. . . . 5
136	51, 135	oveq12d 6320	. . . 4
137	136	oveq1d 6317	. . 3
138	137	mpteq2ia 4503	. 2
139	41, 2	nn0mulcld 10931	. . . . . . . 8
140	6, 139	expcld 12416	. . . . . . 7
141	49, 44	eqeltrd 2510	. . . . . . 7
142	140, 141	mulcomd 9665	. . . . . 6
143	142	oveq1d 6317	. . . . 5
144	143	oveq1d 6317	. . . 4
145	127, 124	eqeltrd 2510	. . . . . . . 8
146	145	sqcld 12414	. . . . . . 7
147	130, 119	eqtrd 2463	. . . . . . . . . 10
148	147, 112, 105, 63	fvmptd 5967	. . . . . . . . 9
149	148, 63	eqeltrd 2510	. . . . . . . 8
150	149	sqcld 12414	. . . . . . 7
151		nnne0 10643	. . . . . . . . . . . 12
152	54, 55, 151	3syl 18	. . . . . . . . . . 11
153	57, 63, 152, 75	divne0d 10400	. . . . . . . . . 10
154	107, 153	eqnetrd 2717	. . . . . . . . 9
155	127, 154	eqnetrd 2717	. . . . . . . 8
156	145, 155, 72	expne0d 12422	. . . . . . 7
157	148, 75	eqnetrd 2717	. . . . . . . 8
158	149, 157, 72	expne0d 12422	. . . . . . 7
159	141, 146, 140, 150, 156, 158	divmuldivd 10425	. . . . . 6
160	159	eqcomd 2430	. . . . 5
161	160	oveq1d 6317	. . . 4
162	33, 30	eqeltrd 2510	. . . . . . . . 9
163	162, 41	expcld 12416	. . . . . . . 8
164	38, 45	eqeltrd 2510	. . . . . . . 8
165	163, 164, 146, 156	div23d 10421	. . . . . . 7
166	165	oveq1d 6317	. . . . . 6
167	166	oveq1d 6317	. . . . 5
168	163, 146, 156	divcld 10384	. . . . . . 7
169	140, 150, 158	divcld 10384	. . . . . . 7
170	168, 164, 169	mulassd 9667	. . . . . 6
171	170	oveq1d 6317	. . . . 5
172	164, 169	mulcld 9664	. . . . . . 7
173		1cnd 9660	. . . . . . . 8
174	8, 173	addcld 9663	. . . . . . 7
175		0red 9645	. . . . . . . . 9
176	105	nnred 10625	. . . . . . . . 9
177		2re 10680	. . . . . . . . . . . 12
178	177	a1i 11	. . . . . . . . . . 11
179		nnre 10617	. . . . . . . . . . 11
180	178, 179	remulcld 9672	. . . . . . . . . 10
181		1red 9659	. . . . . . . . . 10
182	180, 181	readdcld 9671	. . . . . . . . 9
183	105	nngt0d 10654	. . . . . . . . 9
184	176	ltp1d 10538	. . . . . . . . 9
185	175, 176, 182, 183, 184	lttrd 9797	. . . . . . . 8
186	185	gt0ne0d 10179	. . . . . . 7
187	168, 172, 174, 186	divassd 10419	. . . . . 6
188	164, 140, 150, 158	div12d 10420	. . . . . . . . . 10
189	9, 17, 41	mulexpd 12431	. . . . . . . . . . . . 13
190	60, 62	sqmuld 12428	. . . . . . . . . . . . 13
191	189, 190	oveq12d 6320	. . . . . . . . . . . 12
192	148	oveq1d 6317	. . . . . . . . . . . . 13
193	38, 192	oveq12d 6320	. . . . . . . . . . . 12
194	9, 41	expcld 12416	. . . . . . . . . . . . 13
195	60	sqcld 12414	. . . . . . . . . . . . 13
196	17, 41	expcld 12416	. . . . . . . . . . . . 13
197	62	sqcld 12414	. . . . . . . . . . . . 13
198	60, 67, 72	expne0d 12422	. . . . . . . . . . . . 13
199	62, 74, 72	expne0d 12422	. . . . . . . . . . . . 13
200	194, 195, 196, 197, 198, 199	divmuldivd 10425	. . . . . . . . . . . 12
201	191, 193, 200	3eqtr4d 2473	. . . . . . . . . . 11
202	201	oveq2d 6318	. . . . . . . . . 10
203	65	rprege0d 11349	. . . . . . . . . . . . . . . 16 $/\$
204		resqrtth 13308	. . . . . . . . . . . . . . . 16 $/\$
205	203, 204	syl 17	. . . . . . . . . . . . . . 15
206	205	oveq2d 6318	. . . . . . . . . . . . . 14
207		2t2e4 10760	. . . . . . . . . . . . . . . . . . 19
208	207	eqcomi 2435	. . . . . . . . . . . . . . . . . 18
209	208	a1i 11	. . . . . . . . . . . . . . . . 17
210	209	oveq2d 6318	. . . . . . . . . . . . . . . 16
211	9, 53, 53	expmuld 12419	. . . . . . . . . . . . . . . 16
212	22	rprege0d 11349	. . . . . . . . . . . . . . . . . 18 $/\$
213		resqrtth 13308	. . . . . . . . . . . . . . . . . 18 $/\$
214	212, 213	syl 17	. . . . . . . . . . . . . . . . 17
215	214	oveq1d 6317	. . . . . . . . . . . . . . . 16
216	210, 211, 215	3eqtrd 2467	. . . . . . . . . . . . . . 15
217	6, 6, 7	mulassd 9667	. . . . . . . . . . . . . . . 16
218	207	a1i 11	. . . . . . . . . . . . . . . . 17
219	218	oveq1d 6317	. . . . . . . . . . . . . . . 16
220	217, 219	eqtr3d 2465	. . . . . . . . . . . . . . 15
221	216, 220	oveq12d 6320	. . . . . . . . . . . . . 14
222	6, 7	sqmuld 12428	. . . . . . . . . . . . . . . . 17
223		sq2 12371	. . . . . . . . . . . . . . . . . . 19
224	223	a1i 11	. . . . . . . . . . . . . . . . . 18
225	224	oveq1d 6317	. . . . . . . . . . . . . . . . 17
226	222, 225	eqtrd 2463	. . . . . . . . . . . . . . . 16
227	226	oveq1d 6317	. . . . . . . . . . . . . . 15
228		4cn 10688	. . . . . . . . . . . . . . . . . . 19
229		4ne0 10707	. . . . . . . . . . . . . . . . . . 19
230	228, 229	dividi 10341	. . . . . . . . . . . . . . . . . 18
231	230	a1i 11	. . . . . . . . . . . . . . . . 17
232	7	sqvald 12413	. . . . . . . . . . . . . . . . . . 19
233	232	oveq1d 6317	. . . . . . . . . . . . . . . . . 18
234	7, 7, 25	divcan4d 10390	. . . . . . . . . . . . . . . . . 18
235	233, 234	eqtrd 2463	. . . . . . . . . . . . . . . . 17
236	231, 235	oveq12d 6320	. . . . . . . . . . . . . . . 16
237	41	nn0cnd 10928	. . . . . . . . . . . . . . . . 17
238	7	sqcld 12414	. . . . . . . . . . . . . . . . 17
239	229	a1i 11	. . . . . . . . . . . . . . . . 17
240	237, 237, 238, 7, 239, 25	divmuldivd 10425	. . . . . . . . . . . . . . . 16
241	7	mulid2d 9662	. . . . . . . . . . . . . . . 16
242	236, 240, 241	3eqtr3d 2471	. . . . . . . . . . . . . . 15
243	227, 242	eqtrd 2463	. . . . . . . . . . . . . 14
244	206, 221, 243	3eqtrd 2467	. . . . . . . . . . . . 13
245	7, 237	mulcomd 9665	. . . . . . . . . . . . . . . . 17
246	245	oveq2d 6318	. . . . . . . . . . . . . . . 16
247	16, 41, 2	expmuld 12419	. . . . . . . . . . . . . . . 16
248	7, 12, 15, 139	expdivd 12430	. . . . . . . . . . . . . . . 16
249	246, 247, 248	3eqtr3d 2471	. . . . . . . . . . . . . . 15
250	6, 7, 6	mul32d 9844	. . . . . . . . . . . . . . . . . 18
251	250, 219	eqtrd 2463	. . . . . . . . . . . . . . . . 17
252	251	oveq2d 6318	. . . . . . . . . . . . . . . 16
253	61, 53, 54	expmuld 12419	. . . . . . . . . . . . . . . 16
254	8, 12, 15, 139	expdivd 12430	. . . . . . . . . . . . . . . 16
255	252, 253, 254	3eqtr3d 2471	. . . . . . . . . . . . . . 15
256	249, 255	oveq12d 6320	. . . . . . . . . . . . . 14
257	249, 196	eqeltrrd 2511	. . . . . . . . . . . . . . 15
258	8, 139	expcld 12416	. . . . . . . . . . . . . . 15
259	12, 139	expcld 12416	. . . . . . . . . . . . . . 15
260	46, 27	zmulcld 11047	. . . . . . . . . . . . . . . 16
261	8, 69, 260	expne0d 12422	. . . . . . . . . . . . . . 15
262	12, 15, 260	expne0d 12422	. . . . . . . . . . . . . . 15
263	257, 258, 259, 261, 262	divdiv2d 10416	. . . . . . . . . . . . . 14
264	7, 139	expcld 12416	. . . . . . . . . . . . . . . . 17
265	264, 259, 262	divcan1d 10385	. . . . . . . . . . . . . . . 16
266	265	oveq1d 6317	. . . . . . . . . . . . . . 15
267	6, 7, 139	mulexpd 12431	. . . . . . . . . . . . . . . 16
268	267	oveq2d 6318	. . . . . . . . . . . . . . 15
269	140, 264	mulcomd 9665	. . . . . . . . . . . . . . . . 17
270	269	oveq2d 6318	. . . . . . . . . . . . . . . 16
271	7, 25, 260	expne0d 12422	. . . . . . . . . . . . . . . . 17
272	6, 68, 260	expne0d 12422	. . . . . . . . . . . . . . . . 17
273	264, 264, 140, 271, 272	divdiv1d 10415	. . . . . . . . . . . . . . . 16
274	264, 271	dividd 10382	. . . . . . . . . . . . . . . . 17
275	274	oveq1d 6317	. . . . . . . . . . . . . . . 16
276	270, 273, 275	3eqtr2d 2469	. . . . . . . . . . . . . . 15
277	266, 268, 276	3eqtrd 2467	. . . . . . . . . . . . . 14
278	256, 263, 277	3eqtrd 2467	. . . . . . . . . . . . 13
279	244, 278	oveq12d 6320	. . . . . . . . . . . 12
280	279	oveq2d 6318	. . . . . . . . . . 11
281	140, 272	reccld 10377	. . . . . . . . . . . 12
282	140, 7, 281	mul12d 9843	. . . . . . . . . . 11
283	7	mulid1d 9661	. . . . . . . . . . . 12
284	140, 272	recidd 10379	. . . . . . . . . . . . 13
285	284	oveq2d 6318	. . . . . . . . . . . 12
286	283, 285, 235	3eqtr4d 2473	. . . . . . . . . . 11
287	280, 282, 286	3eqtrd 2467	. . . . . . . . . 10
288	188, 202, 287	3eqtrd 2467	. . . . . . . . 9
289	288	oveq1d 6317	. . . . . . . 8
290	238, 7, 174, 25, 186	divdiv1d 10415	. . . . . . . 8
291	289, 290	eqtrd 2463	. . . . . . 7
292	291	oveq2d 6318	. . . . . 6
293	187, 292	eqtrd 2463	. . . . 5
294	167, 171, 293	3eqtrd 2467	. . . 4
295	144, 161, 294	3eqtrd 2467	. . 3
296	295	mpteq2ia 4503	. 2
297	1, 138, 296	3eqtri 2455	1

Colors of variables: wff setvar class

Syntax hints: $/\$ wa 370

wceq 1437

wcel 1868

wne 2618 class class class wbr 4420

cmpt 4479

cfv 5598 (class class class)co 6302

cc 9538

cr 9539

cc0 9540

c1 9541

caddc 9543

cmul 9545

cle 9677

cdiv 10270

cn 10610

c2 10660

c4 10662

cn0 10870

cz 10938

crp 11303

cexp 12272

cfa 12459

csqrt 13285

ceu 14103

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1839 ax-8 1870 ax-9 1872 ax-10 1887 ax-11 1892 ax-12 1905 ax-13 2053 ax-ext 2400 ax-rep 4533 ax-sep 4543 ax-nul 4552 ax-pow 4599 ax-pr 4657 ax-un 6594 ax-inf2 8149 ax-cnex 9596 ax-resscn 9597 ax-1cn 9598 ax-icn 9599 ax-addcl 9600 ax-addrcl 9601 ax-mulcl 9602 ax-mulrcl 9603 ax-mulcom 9604 ax-addass 9605 ax-mulass 9606 ax-distr 9607 ax-i2m1 9608 ax-1ne0 9609 ax-1rid 9610 ax-rnegex 9611 ax-rrecex 9612 ax-cnre 9613 ax-pre-lttri 9614 ax-pre-lttrn 9615 ax-pre-ltadd 9616 ax-pre-mulgt0 9617 ax-pre-sup 9618 ax-addf 9619 ax-mulf 9620

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-fal 1443 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2269 df-mo 2270 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2572 df-ne 2620 df-nel 2621 df-ral 2780 df-rex 2781 df-reu 2782 df-rmo 2783 df-rab 2784 df-v 3083 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-pss 3452 df-nul 3762 df-if 3910 df-pw 3981 df-sn 3997 df-pr 3999 df-tp 4001 df-op 4003 df-uni 4217 df-int 4253 df-iun 4298 df-br 4421 df-opab 4480 df-mpt 4481 df-tr 4516 df-eprel 4761 df-id 4765 df-po 4771 df-so 4772 df-fr 4809 df-se 4810 df-we 4811 df-xp 4856 df-rel 4857 df-cnv 4858 df-co 4859 df-dm 4860 df-rn 4861 df-res 4862 df-ima 4863 df-pred 5396 df-ord 5442 df-on 5443 df-lim 5444 df-suc 5445 df-iota 5562 df-fun 5600 df-fn 5601 df-f 5602 df-f1 5603 df-fo 5604 df-f1o 5605 df-fv 5606 df-isom 5607 df-riota 6264 df-ov 6305 df-oprab 6306 df-mpt2 6307 df-om 6704 df-1st 6804 df-2nd 6805 df-wrecs 7033 df-recs 7095 df-rdg 7133 df-1o 7187 df-oadd 7191 df-er 7368 df-pm 7480 df-en 7575 df-dom 7576 df-sdom 7577 df-fin 7578 df-sup 7959 df-inf 7960 df-oi 8028 df-card 8375 df-pnf 9678 df-mnf 9679 df-xr 9680 df-ltxr 9681 df-le 9682 df-sub 9863 df-neg 9864 df-div 10271 df-nn 10611 df-2 10669 df-3 10670 df-4 10671 df-n0 10871 df-z 10939 df-uz 11161 df-q 11266 df-rp 11304 df-ico 11642 df-fz 11786 df-fzo 11917 df-fl 12028 df-seq 12214 df-exp 12273 df-fac 12460 df-bc 12488 df-hash 12516 df-shft 13119 df-cj 13151 df-re 13152 df-im 13153 df-sqrt 13287 df-abs 13288 df-limsup 13514 df-clim 13540 df-rlim 13541 df-sum 13741 df-ef 14109 df-e 14110

This theorem is referenced by: stirlinglem15 37770

W3C validator