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 31376

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 10798	. . . . . . . . . . . . 13
3		faccl 12325	. . . . . . . . . . . . 13
4		nncn 10540	. . . . . . . . . . . . 13
5	2, 3, 4	3syl 20	. . . . . . . . . . . 12
6		2cnd 10604	. . . . . . . . . . . . . . 15
7		nncn 10540	. . . . . . . . . . . . . . 15
8	6, 7	mulcld 9612	. . . . . . . . . . . . . 14
9	8	sqrtcld 13224	. . . . . . . . . . . . 13
10		ere 13679	. . . . . . . . . . . . . . . . 17
11	10	recni 9604	. . . . . . . . . . . . . . . 16
12	11	a1i 11	. . . . . . . . . . . . . . 15
13		epos 13794	. . . . . . . . . . . . . . . . 17
14	10, 13	gt0ne0ii 10085	. . . . . . . . . . . . . . . 16
15	14	a1i 11	. . . . . . . . . . . . . . 15
16	7, 12, 15	divcld 10316	. . . . . . . . . . . . . 14
17	16, 2	expcld 12272	. . . . . . . . . . . . 13
18	9, 17	mulcld 9612	. . . . . . . . . . . 12
19		2rp 11221	. . . . . . . . . . . . . . . . 17
20	19	a1i 11	. . . . . . . . . . . . . . . 16
21		nnrp 11225	. . . . . . . . . . . . . . . 16
22	20, 21	rpmulcld 11268	. . . . . . . . . . . . . . 15
23	22	sqrtgt0d 13200	. . . . . . . . . . . . . 14
24	23	gt0ne0d 10113	. . . . . . . . . . . . 13
25		nnne0 10564	. . . . . . . . . . . . . . 15
26	7, 12, 25, 15	divne0d 10332	. . . . . . . . . . . . . 14
27		nnz 10882	. . . . . . . . . . . . . 14
28	16, 26, 27	expne0d 12278	. . . . . . . . . . . . 13
29	9, 17, 24, 28	mulne0d 10197	. . . . . . . . . . . 12
30	5, 18, 29	divcld 10316	. . . . . . . . . . 11
31		stirlinglem3.1	. . . . . . . . . . . 12
32	31	fvmpt2 5955	. . . . . . . . . . 11 $/\$
33	30, 32	mpdan 668	. . . . . . . . . 10
34	33	oveq1d 6297	. . . . . . . . 9
35		stirlinglem3.3	. . . . . . . . . . . 12
36	35	fvmpt2 5955	. . . . . . . . . . 11 $/\$
37	18, 36	mpdan 668	. . . . . . . . . 10
38	37	oveq1d 6297	. . . . . . . . 9
39	34, 38	oveq12d 6300	. . . . . . . 8
40		4nn0 10810	. . . . . . . . . . 11
41	40	a1i 11	. . . . . . . . . 10
42	5, 18, 29, 41	expdivd 12286	. . . . . . . . 9
43	42	oveq1d 6297	. . . . . . . 8
44	5, 41	expcld 12272	. . . . . . . . 9
45	18, 41	expcld 12272	. . . . . . . . 9
46	41	nn0zd 10960	. . . . . . . . . 10
47	18, 29, 46	expne0d 12278	. . . . . . . . 9
48	44, 45, 47	divcan1d 10317	. . . . . . . 8
49	39, 43, 48	3eqtrd 2512	. . . . . . 7
50	49	eqcomd 2475	. . . . . 6
51	50	oveq2d 6298	. . . . 5
52		2nn0 10808	. . . . . . . . . . . . 13
53	52	a1i 11	. . . . . . . . . . . 12
54	53, 2	nn0mulcld 10853	. . . . . . . . . . 11
55		faccl 12325	. . . . . . . . . . 11
56		nncn 10540	. . . . . . . . . . 11
57	54, 55, 56	3syl 20	. . . . . . . . . 10
58	57	sqcld 12270	. . . . . . . . 9
59	6, 8	mulcld 9612	. . . . . . . . . . . 12
60	59	sqrtcld 13224	. . . . . . . . . . 11
61	8, 12, 15	divcld 10316	. . . . . . . . . . . 12
62	61, 54	expcld 12272	. . . . . . . . . . 11
63	60, 62	mulcld 9612	. . . . . . . . . 10
64	63	sqcld 12270	. . . . . . . . 9
65	20, 22	rpmulcld 11268	. . . . . . . . . . . . 13
66	65	sqrtgt0d 13200	. . . . . . . . . . . 12
67	66	gt0ne0d 10113	. . . . . . . . . . 11
68	20	rpne0d 11257	. . . . . . . . . . . . . 14
69	6, 7, 68, 25	mulne0d 10197	. . . . . . . . . . . . 13
70	8, 12, 69, 15	divne0d 10332	. . . . . . . . . . . 12
71		2z 10892	. . . . . . . . . . . . . 14
72	71	a1i 11	. . . . . . . . . . . . 13
73	72, 27	zmulcld 10968	. . . . . . . . . . . 12
74	61, 70, 73	expne0d 12278	. . . . . . . . . . 11
75	60, 62, 67, 74	mulne0d 10197	. . . . . . . . . 10
76	63, 75, 72	expne0d 12278	. . . . . . . . 9
77	58, 64, 76	divcan1d 10317	. . . . . . . 8
78	57, 63, 75, 53	expdivd 12286	. . . . . . . . . 10
79	78	eqcomd 2475	. . . . . . . . 9
80	79	oveq1d 6297	. . . . . . . 8
81	77, 80	eqtr3d 2510	. . . . . . 7
82		fveq2 5864	. . . . . . . . . . . . . . 15
83		oveq2 6290	. . . . . . . . . . . . . . . . 17
84	83	fveq2d 5868	. . . . . . . . . . . . . . . 16
85		oveq1 6289	. . . . . . . . . . . . . . . . 17
86		id 22	. . . . . . . . . . . . . . . . 17
87	85, 86	oveq12d 6300	. . . . . . . . . . . . . . . 16
88	84, 87	oveq12d 6300	. . . . . . . . . . . . . . 15
89	82, 88	oveq12d 6300	. . . . . . . . . . . . . 14
90	89	cbvmptv 4538	. . . . . . . . . . . . 13
91	31, 90	eqtri 2496	. . . . . . . . . . . 12
92	91	a1i 11	. . . . . . . . . . 11
93		fveq2 5864	. . . . . . . . . . . . 13
94		oveq2 6290	. . . . . . . . . . . . . . 15
95	94	fveq2d 5868	. . . . . . . . . . . . . 14
96		oveq1 6289	. . . . . . . . . . . . . . 15
97		id 22	. . . . . . . . . . . . . . 15
98	96, 97	oveq12d 6300	. . . . . . . . . . . . . 14
99	95, 98	oveq12d 6300	. . . . . . . . . . . . 13
100	93, 99	oveq12d 6300	. . . . . . . . . . . 12
101	100	adantl 466	. . . . . . . . . . 11 $/\$
102		2nn 10689	. . . . . . . . . . . . 13
103	102	a1i 11	. . . . . . . . . . . 12
104		id 22	. . . . . . . . . . . 12
105	103, 104	nnmulcld 10579	. . . . . . . . . . 11
106	57, 63, 75	divcld 10316	. . . . . . . . . . 11
107	92, 101, 105, 106	fvmptd 5953	. . . . . . . . . 10
108	107	oveq1d 6297	. . . . . . . . 9
109	108	eqcomd 2475	. . . . . . . 8
110	109	oveq1d 6297	. . . . . . 7
111		eqidd 2468	. . . . . . . . . . 11
112	99	adantl 466	. . . . . . . . . . 11 $/\$
113	111, 112, 105, 63	fvmptd 5953	. . . . . . . . . 10
114	113	oveq1d 6297	. . . . . . . . 9
115	114	eqcomd 2475	. . . . . . . 8
116	115	oveq2d 6298	. . . . . . 7
117	81, 110, 116	3eqtrd 2512	. . . . . 6
118	88	cbvmptv 4538	. . . . . . . . . . 11
119	118	a1i 11	. . . . . . . . . 10
120	119	fveq1d 5866	. . . . . . . . 9
121	120	eqcomd 2475	. . . . . . . 8
122	121	oveq1d 6297	. . . . . . 7
123	122	oveq2d 6298	. . . . . 6
124	107, 106	eqeltrd 2555	. . . . . . . . . 10
125		stirlinglem3.2	. . . . . . . . . . 11
126	125	fvmpt2 5955	. . . . . . . . . 10 $/\$
127	124, 126	mpdan 668	. . . . . . . . 9
128	127	eqcomd 2475	. . . . . . . 8
129	128	oveq1d 6297	. . . . . . 7
130	35	a1i 11	. . . . . . . . . 10
131	130	fveq1d 5866	. . . . . . . . 9
132	131	eqcomd 2475	. . . . . . . 8
133	132	oveq1d 6297	. . . . . . 7
134	129, 133	oveq12d 6300	. . . . . 6
135	117, 123, 134	3eqtrd 2512	. . . . 5
136	51, 135	oveq12d 6300	. . . 4
137	136	oveq1d 6297	. . 3
138	137	mpteq2ia 4529	. 2
139	41, 2	nn0mulcld 10853	. . . . . . . 8
140	6, 139	expcld 12272	. . . . . . 7
141	49, 44	eqeltrd 2555	. . . . . . 7
142	140, 141	mulcomd 9613	. . . . . 6
143	142	oveq1d 6297	. . . . 5
144	143	oveq1d 6297	. . . 4
145	127, 124	eqeltrd 2555	. . . . . . . 8
146	145	sqcld 12270	. . . . . . 7
147	130, 119	eqtrd 2508	. . . . . . . . . 10
148	147, 112, 105, 63	fvmptd 5953	. . . . . . . . 9
149	148, 63	eqeltrd 2555	. . . . . . . 8
150	149	sqcld 12270	. . . . . . 7
151		nnne0 10564	. . . . . . . . . . . 12
152	54, 55, 151	3syl 20	. . . . . . . . . . 11
153	57, 63, 152, 75	divne0d 10332	. . . . . . . . . 10
154	107, 153	eqnetrd 2760	. . . . . . . . 9
155	127, 154	eqnetrd 2760	. . . . . . . 8
156	145, 155, 72	expne0d 12278	. . . . . . 7
157	148, 75	eqnetrd 2760	. . . . . . . 8
158	149, 157, 72	expne0d 12278	. . . . . . 7
159	141, 146, 140, 150, 156, 158	divmuldivd 10357	. . . . . 6
160	159	eqcomd 2475	. . . . 5
161	160	oveq1d 6297	. . . 4
162	33, 30	eqeltrd 2555	. . . . . . . . 9
163	162, 41	expcld 12272	. . . . . . . 8
164	38, 45	eqeltrd 2555	. . . . . . . 8
165	163, 164, 146, 156	div23d 10353	. . . . . . 7
166	165	oveq1d 6297	. . . . . 6
167	166	oveq1d 6297	. . . . 5
168	163, 146, 156	divcld 10316	. . . . . . 7
169	140, 150, 158	divcld 10316	. . . . . . 7
170	168, 164, 169	mulassd 9615	. . . . . 6
171	170	oveq1d 6297	. . . . 5
172	164, 169	mulcld 9612	. . . . . . 7
173		ax-1cn 9546	. . . . . . . . 9
174	173	a1i 11	. . . . . . . 8
175	8, 174	addcld 9611	. . . . . . 7
176		0re 9592	. . . . . . . . . 10
177	176	a1i 11	. . . . . . . . 9
178	105	nnred 10547	. . . . . . . . 9
179		2re 10601	. . . . . . . . . . . 12
180	179	a1i 11	. . . . . . . . . . 11
181		nnre 10539	. . . . . . . . . . 11
182	180, 181	remulcld 9620	. . . . . . . . . 10
183		1re 9591	. . . . . . . . . . 11
184	183	a1i 11	. . . . . . . . . 10
185	182, 184	readdcld 9619	. . . . . . . . 9
186	105	nngt0d 10575	. . . . . . . . 9
187	178	ltp1d 10472	. . . . . . . . 9
188	177, 178, 185, 186, 187	lttrd 9738	. . . . . . . 8
189	188	gt0ne0d 10113	. . . . . . 7
190	168, 172, 175, 189	divassd 10351	. . . . . 6
191	164, 140, 150, 158	div12d 10352	. . . . . . . . . 10
192	9, 17, 41	mulexpd 12287	. . . . . . . . . . . . 13
193	60, 62	sqmuld 12284	. . . . . . . . . . . . 13
194	192, 193	oveq12d 6300	. . . . . . . . . . . 12
195	148	oveq1d 6297	. . . . . . . . . . . . 13
196	38, 195	oveq12d 6300	. . . . . . . . . . . 12
197	9, 41	expcld 12272	. . . . . . . . . . . . 13
198	60	sqcld 12270	. . . . . . . . . . . . 13
199	17, 41	expcld 12272	. . . . . . . . . . . . 13
200	62	sqcld 12270	. . . . . . . . . . . . 13
201	60, 67, 72	expne0d 12278	. . . . . . . . . . . . 13
202	62, 74, 72	expne0d 12278	. . . . . . . . . . . . 13
203	197, 198, 199, 200, 201, 202	divmuldivd 10357	. . . . . . . . . . . 12
204	194, 196, 203	3eqtr4d 2518	. . . . . . . . . . 11
205	204	oveq2d 6298	. . . . . . . . . 10
206	65	rprege0d 11259	. . . . . . . . . . . . . . . 16 $/\$
207		resqrtth 13046	. . . . . . . . . . . . . . . 16 $/\$
208	206, 207	syl 16	. . . . . . . . . . . . . . 15
209	208	oveq2d 6298	. . . . . . . . . . . . . 14
210		2t2e4 10681	. . . . . . . . . . . . . . . . . . 19
211	210	eqcomi 2480	. . . . . . . . . . . . . . . . . 18
212	211	a1i 11	. . . . . . . . . . . . . . . . 17
213	212	oveq2d 6298	. . . . . . . . . . . . . . . 16
214	9, 53, 53	expmuld 12275	. . . . . . . . . . . . . . . 16
215	22	rprege0d 11259	. . . . . . . . . . . . . . . . . 18 $/\$
216		resqrtth 13046	. . . . . . . . . . . . . . . . . 18 $/\$
217	215, 216	syl 16	. . . . . . . . . . . . . . . . 17
218	217	oveq1d 6297	. . . . . . . . . . . . . . . 16
219	213, 214, 218	3eqtrd 2512	. . . . . . . . . . . . . . 15
220	6, 6, 7	mulassd 9615	. . . . . . . . . . . . . . . 16
221	210	a1i 11	. . . . . . . . . . . . . . . . 17
222	221	oveq1d 6297	. . . . . . . . . . . . . . . 16
223	220, 222	eqtr3d 2510	. . . . . . . . . . . . . . 15
224	219, 223	oveq12d 6300	. . . . . . . . . . . . . 14
225	6, 7	sqmuld 12284	. . . . . . . . . . . . . . . . 17
226		sq2 12226	. . . . . . . . . . . . . . . . . . 19
227	226	a1i 11	. . . . . . . . . . . . . . . . . 18
228	227	oveq1d 6297	. . . . . . . . . . . . . . . . 17
229	225, 228	eqtrd 2508	. . . . . . . . . . . . . . . 16
230	229	oveq1d 6297	. . . . . . . . . . . . . . 15
231		4cn 10609	. . . . . . . . . . . . . . . . . . 19
232		4ne0 10628	. . . . . . . . . . . . . . . . . . 19
233	231, 232	dividi 10273	. . . . . . . . . . . . . . . . . 18
234	233	a1i 11	. . . . . . . . . . . . . . . . 17
235	7	sqvald 12269	. . . . . . . . . . . . . . . . . . 19
236	235	oveq1d 6297	. . . . . . . . . . . . . . . . . 18
237	7, 7, 25	divcan4d 10322	. . . . . . . . . . . . . . . . . 18
238	236, 237	eqtrd 2508	. . . . . . . . . . . . . . . . 17
239	234, 238	oveq12d 6300	. . . . . . . . . . . . . . . 16
240	41	nn0cnd 10850	. . . . . . . . . . . . . . . . 17
241	7	sqcld 12270	. . . . . . . . . . . . . . . . 17
242	232	a1i 11	. . . . . . . . . . . . . . . . 17
243	240, 240, 241, 7, 242, 25	divmuldivd 10357	. . . . . . . . . . . . . . . 16
244	7	mulid2d 9610	. . . . . . . . . . . . . . . 16
245	239, 243, 244	3eqtr3d 2516	. . . . . . . . . . . . . . 15
246	230, 245	eqtrd 2508	. . . . . . . . . . . . . 14
247	209, 224, 246	3eqtrd 2512	. . . . . . . . . . . . 13
248	7, 240	mulcomd 9613	. . . . . . . . . . . . . . . . 17
249	248	oveq2d 6298	. . . . . . . . . . . . . . . 16
250	16, 41, 2	expmuld 12275	. . . . . . . . . . . . . . . 16
251	7, 12, 15, 139	expdivd 12286	. . . . . . . . . . . . . . . 16
252	249, 250, 251	3eqtr3d 2516	. . . . . . . . . . . . . . 15
253	6, 7, 6	mul32d 9785	. . . . . . . . . . . . . . . . . 18
254	253, 222	eqtrd 2508	. . . . . . . . . . . . . . . . 17
255	254	oveq2d 6298	. . . . . . . . . . . . . . . 16
256	61, 53, 54	expmuld 12275	. . . . . . . . . . . . . . . 16
257	8, 12, 15, 139	expdivd 12286	. . . . . . . . . . . . . . . 16
258	255, 256, 257	3eqtr3d 2516	. . . . . . . . . . . . . . 15
259	252, 258	oveq12d 6300	. . . . . . . . . . . . . 14
260	252, 199	eqeltrrd 2556	. . . . . . . . . . . . . . 15
261	8, 139	expcld 12272	. . . . . . . . . . . . . . 15
262	12, 139	expcld 12272	. . . . . . . . . . . . . . 15
263	46, 27	zmulcld 10968	. . . . . . . . . . . . . . . 16
264	8, 69, 263	expne0d 12278	. . . . . . . . . . . . . . 15
265	12, 15, 263	expne0d 12278	. . . . . . . . . . . . . . 15
266	260, 261, 262, 264, 265	divdiv2d 10348	. . . . . . . . . . . . . 14
267	7, 139	expcld 12272	. . . . . . . . . . . . . . . . 17
268	267, 262, 265	divcan1d 10317	. . . . . . . . . . . . . . . 16
269	268	oveq1d 6297	. . . . . . . . . . . . . . 15
270	6, 7, 139	mulexpd 12287	. . . . . . . . . . . . . . . 16
271	270	oveq2d 6298	. . . . . . . . . . . . . . 15
272	140, 267	mulcomd 9613	. . . . . . . . . . . . . . . . 17
273	272	oveq2d 6298	. . . . . . . . . . . . . . . 16
274	7, 25, 263	expne0d 12278	. . . . . . . . . . . . . . . . 17
275	6, 68, 263	expne0d 12278	. . . . . . . . . . . . . . . . 17
276	267, 267, 140, 274, 275	divdiv1d 10347	. . . . . . . . . . . . . . . 16
277	267, 274	dividd 10314	. . . . . . . . . . . . . . . . 17
278	277	oveq1d 6297	. . . . . . . . . . . . . . . 16
279	273, 276, 278	3eqtr2d 2514	. . . . . . . . . . . . . . 15
280	269, 271, 279	3eqtrd 2512	. . . . . . . . . . . . . 14
281	259, 266, 280	3eqtrd 2512	. . . . . . . . . . . . 13
282	247, 281	oveq12d 6300	. . . . . . . . . . . 12
283	282	oveq2d 6298	. . . . . . . . . . 11
284	140, 275	reccld 10309	. . . . . . . . . . . 12
285	140, 7, 284	mul12d 9784	. . . . . . . . . . 11
286	7	mulid1d 9609	. . . . . . . . . . . 12
287	140, 275	recidd 10311	. . . . . . . . . . . . 13
288	287	oveq2d 6298	. . . . . . . . . . . 12
289	286, 288, 238	3eqtr4d 2518	. . . . . . . . . . 11
290	283, 285, 289	3eqtrd 2512	. . . . . . . . . 10
291	191, 205, 290	3eqtrd 2512	. . . . . . . . 9
292	291	oveq1d 6297	. . . . . . . 8
293	241, 7, 175, 25, 189	divdiv1d 10347	. . . . . . . 8
294	292, 293	eqtrd 2508	. . . . . . 7
295	294	oveq2d 6298	. . . . . 6
296	190, 295	eqtrd 2508	. . . . 5
297	167, 171, 296	3eqtrd 2512	. . . 4
298	144, 161, 297	3eqtrd 2512	. . 3
299	298	mpteq2ia 4529	. 2
300	1, 138, 299	3eqtri 2500	1

Colors of variables: wff setvar class

Syntax hints: $/\$ wa 369

wceq 1379

wcel 1767

wne 2662 class class class wbr 4447

cmpt 4505

cfv 5586 (class class class)co 6282

cc 9486

cr 9487

cc0 9488

c1 9489

caddc 9491

cmul 9493

cle 9625

cdiv 10202

cn 10532

c2 10581

c4 10583

cn0 10791

cz 10860

crp 11216

cexp 12129

cfa 12315

csqrt 13023

ceu 13653

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6574 ax-inf2 8054 ax-cnex 9544 ax-resscn 9545 ax-1cn 9546 ax-icn 9547 ax-addcl 9548 ax-addrcl 9549 ax-mulcl 9550 ax-mulrcl 9551 ax-mulcom 9552 ax-addass 9553 ax-mulass 9554 ax-distr 9555 ax-i2m1 9556 ax-1ne0 9557 ax-1rid 9558 ax-rnegex 9559 ax-rrecex 9560 ax-cnre 9561 ax-pre-lttri 9562 ax-pre-lttrn 9563 ax-pre-ltadd 9564 ax-pre-mulgt0 9565 ax-pre-sup 9566 ax-addf 9567 ax-mulf 9568

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-fal 1385 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-se 4839 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5549 df-fun 5588 df-fn 5589 df-f 5590 df-f1 5591 df-fo 5592 df-f1o 5593 df-fv 5594 df-isom 5595 df-riota 6243 df-ov 6285 df-oprab 6286 df-mpt2 6287 df-om 6679 df-1st 6781 df-2nd 6782 df-recs 7039 df-rdg 7073 df-1o 7127 df-oadd 7131 df-er 7308 df-pm 7420 df-en 7514 df-dom 7515 df-sdom 7516 df-fin 7517 df-sup 7897 df-oi 7931 df-card 8316 df-pnf 9626 df-mnf 9627 df-xr 9628 df-ltxr 9629 df-le 9630 df-sub 9803 df-neg 9804 df-div 10203 df-nn 10533 df-2 10590 df-3 10591 df-4 10592 df-n0 10792 df-z 10861 df-uz 11079 df-q 11179 df-rp 11217 df-ico 11531 df-fz 11669 df-fzo 11789 df-fl 11893 df-seq 12071 df-exp 12130 df-fac 12316 df-bc 12343 df-hash 12368 df-shft 12857 df-cj 12889 df-re 12890 df-im 12891 df-sqrt 13025 df-abs 13026 df-limsup 13250 df-clim 13267 df-rlim 13268 df-sum 13465 df-ef 13658 df-e 13659

This theorem is referenced by: stirlinglem15 31388

W3C validator