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 31812

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 10809	. . . . . . . . . . . . 13
3		faccl 12345	. . . . . . . . . . . . 13
4		nncn 10551	. . . . . . . . . . . . 13
5	2, 3, 4	3syl 20	. . . . . . . . . . . 12
6		2cnd 10615	. . . . . . . . . . . . . . 15
7		nncn 10551	. . . . . . . . . . . . . . 15
8	6, 7	mulcld 9619	. . . . . . . . . . . . . 14
9	8	sqrtcld 13250	. . . . . . . . . . . . 13
10		ere 13806	. . . . . . . . . . . . . . . . 17
11	10	recni 9611	. . . . . . . . . . . . . . . 16
12	11	a1i 11	. . . . . . . . . . . . . . 15
13		epos 13922	. . . . . . . . . . . . . . . . 17
14	10, 13	gt0ne0ii 10096	. . . . . . . . . . . . . . . 16
15	14	a1i 11	. . . . . . . . . . . . . . 15
16	7, 12, 15	divcld 10327	. . . . . . . . . . . . . 14
17	16, 2	expcld 12292	. . . . . . . . . . . . 13
18	9, 17	mulcld 9619	. . . . . . . . . . . 12
19		2rp 11236	. . . . . . . . . . . . . . . . 17
20	19	a1i 11	. . . . . . . . . . . . . . . 16
21		nnrp 11240	. . . . . . . . . . . . . . . 16
22	20, 21	rpmulcld 11283	. . . . . . . . . . . . . . 15
23	22	sqrtgt0d 13226	. . . . . . . . . . . . . 14
24	23	gt0ne0d 10124	. . . . . . . . . . . . 13
25		nnne0 10575	. . . . . . . . . . . . . . 15
26	7, 12, 25, 15	divne0d 10343	. . . . . . . . . . . . . 14
27		nnz 10893	. . . . . . . . . . . . . 14
28	16, 26, 27	expne0d 12298	. . . . . . . . . . . . 13
29	9, 17, 24, 28	mulne0d 10208	. . . . . . . . . . . 12
30	5, 18, 29	divcld 10327	. . . . . . . . . . 11
31		stirlinglem3.1	. . . . . . . . . . . 12
32	31	fvmpt2 5948	. . . . . . . . . . 11 $/\$
33	30, 32	mpdan 668	. . . . . . . . . 10
34	33	oveq1d 6296	. . . . . . . . 9
35		stirlinglem3.3	. . . . . . . . . . . 12
36	35	fvmpt2 5948	. . . . . . . . . . 11 $/\$
37	18, 36	mpdan 668	. . . . . . . . . 10
38	37	oveq1d 6296	. . . . . . . . 9
39	34, 38	oveq12d 6299	. . . . . . . 8
40		4nn0 10821	. . . . . . . . . . 11
41	40	a1i 11	. . . . . . . . . 10
42	5, 18, 29, 41	expdivd 12306	. . . . . . . . 9
43	42	oveq1d 6296	. . . . . . . 8
44	5, 41	expcld 12292	. . . . . . . . 9
45	18, 41	expcld 12292	. . . . . . . . 9
46	41	nn0zd 10974	. . . . . . . . . 10
47	18, 29, 46	expne0d 12298	. . . . . . . . 9
48	44, 45, 47	divcan1d 10328	. . . . . . . 8
49	39, 43, 48	3eqtrd 2488	. . . . . . 7
50	49	eqcomd 2451	. . . . . 6
51	50	oveq2d 6297	. . . . 5
52		2nn0 10819	. . . . . . . . . . . . 13
53	52	a1i 11	. . . . . . . . . . . 12
54	53, 2	nn0mulcld 10864	. . . . . . . . . . 11
55		faccl 12345	. . . . . . . . . . 11
56		nncn 10551	. . . . . . . . . . 11
57	54, 55, 56	3syl 20	. . . . . . . . . 10
58	57	sqcld 12290	. . . . . . . . 9
59	6, 8	mulcld 9619	. . . . . . . . . . . 12
60	59	sqrtcld 13250	. . . . . . . . . . 11
61	8, 12, 15	divcld 10327	. . . . . . . . . . . 12
62	61, 54	expcld 12292	. . . . . . . . . . 11
63	60, 62	mulcld 9619	. . . . . . . . . 10
64	63	sqcld 12290	. . . . . . . . 9
65	20, 22	rpmulcld 11283	. . . . . . . . . . . . 13
66	65	sqrtgt0d 13226	. . . . . . . . . . . 12
67	66	gt0ne0d 10124	. . . . . . . . . . 11
68	20	rpne0d 11272	. . . . . . . . . . . . . 14
69	6, 7, 68, 25	mulne0d 10208	. . . . . . . . . . . . 13
70	8, 12, 69, 15	divne0d 10343	. . . . . . . . . . . 12
71		2z 10903	. . . . . . . . . . . . . 14
72	71	a1i 11	. . . . . . . . . . . . 13
73	72, 27	zmulcld 10982	. . . . . . . . . . . 12
74	61, 70, 73	expne0d 12298	. . . . . . . . . . 11
75	60, 62, 67, 74	mulne0d 10208	. . . . . . . . . 10
76	63, 75, 72	expne0d 12298	. . . . . . . . 9
77	58, 64, 76	divcan1d 10328	. . . . . . . 8
78	57, 63, 75, 53	expdivd 12306	. . . . . . . . . 10
79	78	eqcomd 2451	. . . . . . . . 9
80	79	oveq1d 6296	. . . . . . . 8
81	77, 80	eqtr3d 2486	. . . . . . 7
82		fveq2 5856	. . . . . . . . . . . . . . 15
83		oveq2 6289	. . . . . . . . . . . . . . . . 17
84	83	fveq2d 5860	. . . . . . . . . . . . . . . 16
85		oveq1 6288	. . . . . . . . . . . . . . . . 17
86		id 22	. . . . . . . . . . . . . . . . 17
87	85, 86	oveq12d 6299	. . . . . . . . . . . . . . . 16
88	84, 87	oveq12d 6299	. . . . . . . . . . . . . . 15
89	82, 88	oveq12d 6299	. . . . . . . . . . . . . 14
90	89	cbvmptv 4528	. . . . . . . . . . . . 13
91	31, 90	eqtri 2472	. . . . . . . . . . . 12
92	91	a1i 11	. . . . . . . . . . 11
93		fveq2 5856	. . . . . . . . . . . . 13
94		oveq2 6289	. . . . . . . . . . . . . . 15
95	94	fveq2d 5860	. . . . . . . . . . . . . 14
96		oveq1 6288	. . . . . . . . . . . . . . 15
97		id 22	. . . . . . . . . . . . . . 15
98	96, 97	oveq12d 6299	. . . . . . . . . . . . . 14
99	95, 98	oveq12d 6299	. . . . . . . . . . . . 13
100	93, 99	oveq12d 6299	. . . . . . . . . . . 12
101	100	adantl 466	. . . . . . . . . . 11 $/\$
102		2nn 10700	. . . . . . . . . . . . 13
103	102	a1i 11	. . . . . . . . . . . 12
104		id 22	. . . . . . . . . . . 12
105	103, 104	nnmulcld 10590	. . . . . . . . . . 11
106	57, 63, 75	divcld 10327	. . . . . . . . . . 11
107	92, 101, 105, 106	fvmptd 5946	. . . . . . . . . 10
108	107	oveq1d 6296	. . . . . . . . 9
109	108	eqcomd 2451	. . . . . . . 8
110	109	oveq1d 6296	. . . . . . 7
111		eqidd 2444	. . . . . . . . . . 11
112	99	adantl 466	. . . . . . . . . . 11 $/\$
113	111, 112, 105, 63	fvmptd 5946	. . . . . . . . . 10
114	113	oveq1d 6296	. . . . . . . . 9
115	114	eqcomd 2451	. . . . . . . 8
116	115	oveq2d 6297	. . . . . . 7
117	81, 110, 116	3eqtrd 2488	. . . . . 6
118	88	cbvmptv 4528	. . . . . . . . . . 11
119	118	a1i 11	. . . . . . . . . 10
120	119	fveq1d 5858	. . . . . . . . 9
121	120	eqcomd 2451	. . . . . . . 8
122	121	oveq1d 6296	. . . . . . 7
123	122	oveq2d 6297	. . . . . 6
124	107, 106	eqeltrd 2531	. . . . . . . . . 10
125		stirlinglem3.2	. . . . . . . . . . 11
126	125	fvmpt2 5948	. . . . . . . . . 10 $/\$
127	124, 126	mpdan 668	. . . . . . . . 9
128	127	eqcomd 2451	. . . . . . . 8
129	128	oveq1d 6296	. . . . . . 7
130	35	a1i 11	. . . . . . . . . 10
131	130	fveq1d 5858	. . . . . . . . 9
132	131	eqcomd 2451	. . . . . . . 8
133	132	oveq1d 6296	. . . . . . 7
134	129, 133	oveq12d 6299	. . . . . 6
135	117, 123, 134	3eqtrd 2488	. . . . 5
136	51, 135	oveq12d 6299	. . . 4
137	136	oveq1d 6296	. . 3
138	137	mpteq2ia 4519	. 2
139	41, 2	nn0mulcld 10864	. . . . . . . 8
140	6, 139	expcld 12292	. . . . . . 7
141	49, 44	eqeltrd 2531	. . . . . . 7
142	140, 141	mulcomd 9620	. . . . . 6
143	142	oveq1d 6296	. . . . 5
144	143	oveq1d 6296	. . . 4
145	127, 124	eqeltrd 2531	. . . . . . . 8
146	145	sqcld 12290	. . . . . . 7
147	130, 119	eqtrd 2484	. . . . . . . . . 10
148	147, 112, 105, 63	fvmptd 5946	. . . . . . . . 9
149	148, 63	eqeltrd 2531	. . . . . . . 8
150	149	sqcld 12290	. . . . . . 7
151		nnne0 10575	. . . . . . . . . . . 12
152	54, 55, 151	3syl 20	. . . . . . . . . . 11
153	57, 63, 152, 75	divne0d 10343	. . . . . . . . . 10
154	107, 153	eqnetrd 2736	. . . . . . . . 9
155	127, 154	eqnetrd 2736	. . . . . . . 8
156	145, 155, 72	expne0d 12298	. . . . . . 7
157	148, 75	eqnetrd 2736	. . . . . . . 8
158	149, 157, 72	expne0d 12298	. . . . . . 7
159	141, 146, 140, 150, 156, 158	divmuldivd 10368	. . . . . 6
160	159	eqcomd 2451	. . . . 5
161	160	oveq1d 6296	. . . 4
162	33, 30	eqeltrd 2531	. . . . . . . . 9
163	162, 41	expcld 12292	. . . . . . . 8
164	38, 45	eqeltrd 2531	. . . . . . . 8
165	163, 164, 146, 156	div23d 10364	. . . . . . 7
166	165	oveq1d 6296	. . . . . 6
167	166	oveq1d 6296	. . . . 5
168	163, 146, 156	divcld 10327	. . . . . . 7
169	140, 150, 158	divcld 10327	. . . . . . 7
170	168, 164, 169	mulassd 9622	. . . . . 6
171	170	oveq1d 6296	. . . . 5
172	164, 169	mulcld 9619	. . . . . . 7
173		1cnd 9615	. . . . . . . 8
174	8, 173	addcld 9618	. . . . . . 7
175		0red 9600	. . . . . . . . 9
176	105	nnred 10558	. . . . . . . . 9
177		2re 10612	. . . . . . . . . . . 12
178	177	a1i 11	. . . . . . . . . . 11
179		nnre 10550	. . . . . . . . . . 11
180	178, 179	remulcld 9627	. . . . . . . . . 10
181		1red 9614	. . . . . . . . . 10
182	180, 181	readdcld 9626	. . . . . . . . 9
183	105	nngt0d 10586	. . . . . . . . 9
184	176	ltp1d 10483	. . . . . . . . 9
185	175, 176, 182, 183, 184	lttrd 9746	. . . . . . . 8
186	185	gt0ne0d 10124	. . . . . . 7
187	168, 172, 174, 186	divassd 10362	. . . . . 6
188	164, 140, 150, 158	div12d 10363	. . . . . . . . . 10
189	9, 17, 41	mulexpd 12307	. . . . . . . . . . . . 13
190	60, 62	sqmuld 12304	. . . . . . . . . . . . 13
191	189, 190	oveq12d 6299	. . . . . . . . . . . 12
192	148	oveq1d 6296	. . . . . . . . . . . . 13
193	38, 192	oveq12d 6299	. . . . . . . . . . . 12
194	9, 41	expcld 12292	. . . . . . . . . . . . 13
195	60	sqcld 12290	. . . . . . . . . . . . 13
196	17, 41	expcld 12292	. . . . . . . . . . . . 13
197	62	sqcld 12290	. . . . . . . . . . . . 13
198	60, 67, 72	expne0d 12298	. . . . . . . . . . . . 13
199	62, 74, 72	expne0d 12298	. . . . . . . . . . . . 13
200	194, 195, 196, 197, 198, 199	divmuldivd 10368	. . . . . . . . . . . 12
201	191, 193, 200	3eqtr4d 2494	. . . . . . . . . . 11
202	201	oveq2d 6297	. . . . . . . . . 10
203	65	rprege0d 11274	. . . . . . . . . . . . . . . 16 $/\$
204		resqrtth 13071	. . . . . . . . . . . . . . . 16 $/\$
205	203, 204	syl 16	. . . . . . . . . . . . . . 15
206	205	oveq2d 6297	. . . . . . . . . . . . . 14
207		2t2e4 10692	. . . . . . . . . . . . . . . . . . 19
208	207	eqcomi 2456	. . . . . . . . . . . . . . . . . 18
209	208	a1i 11	. . . . . . . . . . . . . . . . 17
210	209	oveq2d 6297	. . . . . . . . . . . . . . . 16
211	9, 53, 53	expmuld 12295	. . . . . . . . . . . . . . . 16
212	22	rprege0d 11274	. . . . . . . . . . . . . . . . . 18 $/\$
213		resqrtth 13071	. . . . . . . . . . . . . . . . . 18 $/\$
214	212, 213	syl 16	. . . . . . . . . . . . . . . . 17
215	214	oveq1d 6296	. . . . . . . . . . . . . . . 16
216	210, 211, 215	3eqtrd 2488	. . . . . . . . . . . . . . 15
217	6, 6, 7	mulassd 9622	. . . . . . . . . . . . . . . 16
218	207	a1i 11	. . . . . . . . . . . . . . . . 17
219	218	oveq1d 6296	. . . . . . . . . . . . . . . 16
220	217, 219	eqtr3d 2486	. . . . . . . . . . . . . . 15
221	216, 220	oveq12d 6299	. . . . . . . . . . . . . 14
222	6, 7	sqmuld 12304	. . . . . . . . . . . . . . . . 17
223		sq2 12246	. . . . . . . . . . . . . . . . . . 19
224	223	a1i 11	. . . . . . . . . . . . . . . . . 18
225	224	oveq1d 6296	. . . . . . . . . . . . . . . . 17
226	222, 225	eqtrd 2484	. . . . . . . . . . . . . . . 16
227	226	oveq1d 6296	. . . . . . . . . . . . . . 15
228		4cn 10620	. . . . . . . . . . . . . . . . . . 19
229		4ne0 10639	. . . . . . . . . . . . . . . . . . 19
230	228, 229	dividi 10284	. . . . . . . . . . . . . . . . . 18
231	230	a1i 11	. . . . . . . . . . . . . . . . 17
232	7	sqvald 12289	. . . . . . . . . . . . . . . . . . 19
233	232	oveq1d 6296	. . . . . . . . . . . . . . . . . 18
234	7, 7, 25	divcan4d 10333	. . . . . . . . . . . . . . . . . 18
235	233, 234	eqtrd 2484	. . . . . . . . . . . . . . . . 17
236	231, 235	oveq12d 6299	. . . . . . . . . . . . . . . 16
237	41	nn0cnd 10861	. . . . . . . . . . . . . . . . 17
238	7	sqcld 12290	. . . . . . . . . . . . . . . . 17
239	229	a1i 11	. . . . . . . . . . . . . . . . 17
240	237, 237, 238, 7, 239, 25	divmuldivd 10368	. . . . . . . . . . . . . . . 16
241	7	mulid2d 9617	. . . . . . . . . . . . . . . 16
242	236, 240, 241	3eqtr3d 2492	. . . . . . . . . . . . . . 15
243	227, 242	eqtrd 2484	. . . . . . . . . . . . . 14
244	206, 221, 243	3eqtrd 2488	. . . . . . . . . . . . 13
245	7, 237	mulcomd 9620	. . . . . . . . . . . . . . . . 17
246	245	oveq2d 6297	. . . . . . . . . . . . . . . 16
247	16, 41, 2	expmuld 12295	. . . . . . . . . . . . . . . 16
248	7, 12, 15, 139	expdivd 12306	. . . . . . . . . . . . . . . 16
249	246, 247, 248	3eqtr3d 2492	. . . . . . . . . . . . . . 15
250	6, 7, 6	mul32d 9793	. . . . . . . . . . . . . . . . . 18
251	250, 219	eqtrd 2484	. . . . . . . . . . . . . . . . 17
252	251	oveq2d 6297	. . . . . . . . . . . . . . . 16
253	61, 53, 54	expmuld 12295	. . . . . . . . . . . . . . . 16
254	8, 12, 15, 139	expdivd 12306	. . . . . . . . . . . . . . . 16
255	252, 253, 254	3eqtr3d 2492	. . . . . . . . . . . . . . 15
256	249, 255	oveq12d 6299	. . . . . . . . . . . . . 14
257	249, 196	eqeltrrd 2532	. . . . . . . . . . . . . . 15
258	8, 139	expcld 12292	. . . . . . . . . . . . . . 15
259	12, 139	expcld 12292	. . . . . . . . . . . . . . 15
260	46, 27	zmulcld 10982	. . . . . . . . . . . . . . . 16
261	8, 69, 260	expne0d 12298	. . . . . . . . . . . . . . 15
262	12, 15, 260	expne0d 12298	. . . . . . . . . . . . . . 15
263	257, 258, 259, 261, 262	divdiv2d 10359	. . . . . . . . . . . . . 14
264	7, 139	expcld 12292	. . . . . . . . . . . . . . . . 17
265	264, 259, 262	divcan1d 10328	. . . . . . . . . . . . . . . 16
266	265	oveq1d 6296	. . . . . . . . . . . . . . 15
267	6, 7, 139	mulexpd 12307	. . . . . . . . . . . . . . . 16
268	267	oveq2d 6297	. . . . . . . . . . . . . . 15
269	140, 264	mulcomd 9620	. . . . . . . . . . . . . . . . 17
270	269	oveq2d 6297	. . . . . . . . . . . . . . . 16
271	7, 25, 260	expne0d 12298	. . . . . . . . . . . . . . . . 17
272	6, 68, 260	expne0d 12298	. . . . . . . . . . . . . . . . 17
273	264, 264, 140, 271, 272	divdiv1d 10358	. . . . . . . . . . . . . . . 16
274	264, 271	dividd 10325	. . . . . . . . . . . . . . . . 17
275	274	oveq1d 6296	. . . . . . . . . . . . . . . 16
276	270, 273, 275	3eqtr2d 2490	. . . . . . . . . . . . . . 15
277	266, 268, 276	3eqtrd 2488	. . . . . . . . . . . . . 14
278	256, 263, 277	3eqtrd 2488	. . . . . . . . . . . . 13
279	244, 278	oveq12d 6299	. . . . . . . . . . . 12
280	279	oveq2d 6297	. . . . . . . . . . 11
281	140, 272	reccld 10320	. . . . . . . . . . . 12
282	140, 7, 281	mul12d 9792	. . . . . . . . . . 11
283	7	mulid1d 9616	. . . . . . . . . . . 12
284	140, 272	recidd 10322	. . . . . . . . . . . . 13
285	284	oveq2d 6297	. . . . . . . . . . . 12
286	283, 285, 235	3eqtr4d 2494	. . . . . . . . . . 11
287	280, 282, 286	3eqtrd 2488	. . . . . . . . . 10
288	188, 202, 287	3eqtrd 2488	. . . . . . . . 9
289	288	oveq1d 6296	. . . . . . . 8
290	238, 7, 174, 25, 186	divdiv1d 10358	. . . . . . . 8
291	289, 290	eqtrd 2484	. . . . . . 7
292	291	oveq2d 6297	. . . . . 6
293	187, 292	eqtrd 2484	. . . . 5
294	167, 171, 293	3eqtrd 2488	. . . 4
295	144, 161, 294	3eqtrd 2488	. . 3
296	295	mpteq2ia 4519	. 2
297	1, 138, 296	3eqtri 2476	1

Colors of variables: wff setvar class

Syntax hints: $/\$ wa 369

wceq 1383

wcel 1804

wne 2638 class class class wbr 4437

cmpt 4495

cfv 5578 (class class class)co 6281

cc 9493

cr 9494

cc0 9495

c1 9496

caddc 9498

cmul 9500

cle 9632

cdiv 10213

cn 10543

c2 10592

c4 10594

cn0 10802

cz 10871

crp 11231

cexp 12148

cfa 12335

csqrt 13048

ceu 13780

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1605 ax-4 1618 ax-5 1691 ax-6 1734 ax-7 1776 ax-8 1806 ax-9 1808 ax-10 1823 ax-11 1828 ax-12 1840 ax-13 1985 ax-ext 2421 ax-rep 4548 ax-sep 4558 ax-nul 4566 ax-pow 4615 ax-pr 4676 ax-un 6577 ax-inf2 8061 ax-cnex 9551 ax-resscn 9552 ax-1cn 9553 ax-icn 9554 ax-addcl 9555 ax-addrcl 9556 ax-mulcl 9557 ax-mulrcl 9558 ax-mulcom 9559 ax-addass 9560 ax-mulass 9561 ax-distr 9562 ax-i2m1 9563 ax-1ne0 9564 ax-1rid 9565 ax-rnegex 9566 ax-rrecex 9567 ax-cnre 9568 ax-pre-lttri 9569 ax-pre-lttrn 9570 ax-pre-ltadd 9571 ax-pre-mulgt0 9572 ax-pre-sup 9573 ax-addf 9574 ax-mulf 9575

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 975 df-3an 976 df-tru 1386 df-fal 1389 df-ex 1600 df-nf 1604 df-sb 1727 df-eu 2272 df-mo 2273 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2593 df-ne 2640 df-nel 2641 df-ral 2798 df-rex 2799 df-reu 2800 df-rmo 2801 df-rab 2802 df-v 3097 df-sbc 3314 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3771 df-if 3927 df-pw 3999 df-sn 4015 df-pr 4017 df-tp 4019 df-op 4021 df-uni 4235 df-int 4272 df-iun 4317 df-br 4438 df-opab 4496 df-mpt 4497 df-tr 4531 df-eprel 4781 df-id 4785 df-po 4790 df-so 4791 df-fr 4828 df-se 4829 df-we 4830 df-ord 4871 df-on 4872 df-lim 4873 df-suc 4874 df-xp 4995 df-rel 4996 df-cnv 4997 df-co 4998 df-dm 4999 df-rn 5000 df-res 5001 df-ima 5002 df-iota 5541 df-fun 5580 df-fn 5581 df-f 5582 df-f1 5583 df-fo 5584 df-f1o 5585 df-fv 5586 df-isom 5587 df-riota 6242 df-ov 6284 df-oprab 6285 df-mpt2 6286 df-om 6686 df-1st 6785 df-2nd 6786 df-recs 7044 df-rdg 7078 df-1o 7132 df-oadd 7136 df-er 7313 df-pm 7425 df-en 7519 df-dom 7520 df-sdom 7521 df-fin 7522 df-sup 7903 df-oi 7938 df-card 8323 df-pnf 9633 df-mnf 9634 df-xr 9635 df-ltxr 9636 df-le 9637 df-sub 9812 df-neg 9813 df-div 10214 df-nn 10544 df-2 10601 df-3 10602 df-4 10603 df-n0 10803 df-z 10872 df-uz 11093 df-q 11194 df-rp 11232 df-ico 11546 df-fz 11684 df-fzo 11807 df-fl 11911 df-seq 12090 df-exp 12149 df-fac 12336 df-bc 12363 df-hash 12388 df-shft 12882 df-cj 12914 df-re 12915 df-im 12916 df-sqrt 13050 df-abs 13051 df-limsup 13276 df-clim 13293 df-rlim 13294 df-sum 13491 df-ef 13785 df-e 13786

This theorem is referenced by: stirlinglem15 31824

W3C validator