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 29842

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 10578	. . . . . . . . . . . . 13
3		faccl 12053	. . . . . . . . . . . . 13
4		nncn 10322	. . . . . . . . . . . . 13
5	2, 3, 4	3syl 20	. . . . . . . . . . . 12
6		2cnd 10386	. . . . . . . . . . . . . . 15
7		nncn 10322	. . . . . . . . . . . . . . 15
8	6, 7	mulcld 9398	. . . . . . . . . . . . . 14
9	8	sqrcld 12915	. . . . . . . . . . . . 13
10		ere 13366	. . . . . . . . . . . . . . . . 17
11	10	recni 9390	. . . . . . . . . . . . . . . 16
12	11	a1i 11	. . . . . . . . . . . . . . 15
13		epos 13481	. . . . . . . . . . . . . . . . 17
14	10, 13	gt0ne0ii 9868	. . . . . . . . . . . . . . . 16
15	14	a1i 11	. . . . . . . . . . . . . . 15
16	7, 12, 15	divcld 10099	. . . . . . . . . . . . . 14
17	16, 2	expcld 12000	. . . . . . . . . . . . 13
18	9, 17	mulcld 9398	. . . . . . . . . . . 12
19		2rp 10988	. . . . . . . . . . . . . . . . 17
20	19	a1i 11	. . . . . . . . . . . . . . . 16
21		nnrp 10992	. . . . . . . . . . . . . . . 16
22	20, 21	rpmulcld 11035	. . . . . . . . . . . . . . 15
23	22	sqrgt0d 12891	. . . . . . . . . . . . . 14
24	23	gt0ne0d 9896	. . . . . . . . . . . . 13
25		nnne0 10346	. . . . . . . . . . . . . . 15
26	7, 12, 25, 15	divne0d 10115	. . . . . . . . . . . . . 14
27		nnz 10660	. . . . . . . . . . . . . 14
28	16, 26, 27	expne0d 12006	. . . . . . . . . . . . 13
29	9, 17, 24, 28	mulne0d 9980	. . . . . . . . . . . 12
30	5, 18, 29	divcld 10099	. . . . . . . . . . 11
31		stirlinglem3.1	. . . . . . . . . . . 12
32	31	fvmpt2 5776	. . . . . . . . . . 11 $/\$
33	30, 32	mpdan 668	. . . . . . . . . 10
34	33	oveq1d 6101	. . . . . . . . 9
35		stirlinglem3.3	. . . . . . . . . . . 12
36	35	fvmpt2 5776	. . . . . . . . . . 11 $/\$
37	18, 36	mpdan 668	. . . . . . . . . 10
38	37	oveq1d 6101	. . . . . . . . 9
39	34, 38	oveq12d 6104	. . . . . . . 8
40		4nn0 10590	. . . . . . . . . . 11
41	40	a1i 11	. . . . . . . . . 10
42	5, 18, 29, 41	expdivd 12014	. . . . . . . . 9
43	42	oveq1d 6101	. . . . . . . 8
44	5, 41	expcld 12000	. . . . . . . . 9
45	18, 41	expcld 12000	. . . . . . . . 9
46	41	nn0zd 10737	. . . . . . . . . 10
47	18, 29, 46	expne0d 12006	. . . . . . . . 9
48	44, 45, 47	divcan1d 10100	. . . . . . . 8
49	39, 43, 48	3eqtrd 2474	. . . . . . 7
50	49	eqcomd 2443	. . . . . 6
51	50	oveq2d 6102	. . . . 5
52		2nn0 10588	. . . . . . . . . . . . 13
53	52	a1i 11	. . . . . . . . . . . 12
54	53, 2	nn0mulcld 10633	. . . . . . . . . . 11
55		faccl 12053	. . . . . . . . . . 11
56		nncn 10322	. . . . . . . . . . 11
57	54, 55, 56	3syl 20	. . . . . . . . . 10
58	57	sqcld 11998	. . . . . . . . 9
59	6, 8	mulcld 9398	. . . . . . . . . . . 12
60	59	sqrcld 12915	. . . . . . . . . . 11
61	8, 12, 15	divcld 10099	. . . . . . . . . . . 12
62	61, 54	expcld 12000	. . . . . . . . . . 11
63	60, 62	mulcld 9398	. . . . . . . . . 10
64	63	sqcld 11998	. . . . . . . . 9
65	20, 22	rpmulcld 11035	. . . . . . . . . . . . 13
66	65	sqrgt0d 12891	. . . . . . . . . . . 12
67	66	gt0ne0d 9896	. . . . . . . . . . 11
68	20	rpne0d 11024	. . . . . . . . . . . . . 14
69	6, 7, 68, 25	mulne0d 9980	. . . . . . . . . . . . 13
70	8, 12, 69, 15	divne0d 10115	. . . . . . . . . . . 12
71		2z 10670	. . . . . . . . . . . . . 14
72	71	a1i 11	. . . . . . . . . . . . 13
73	72, 27	zmulcld 10745	. . . . . . . . . . . 12
74	61, 70, 73	expne0d 12006	. . . . . . . . . . 11
75	60, 62, 67, 74	mulne0d 9980	. . . . . . . . . 10
76	63, 75, 72	expne0d 12006	. . . . . . . . 9
77	58, 64, 76	divcan1d 10100	. . . . . . . 8
78	57, 63, 75, 53	expdivd 12014	. . . . . . . . . 10
79	78	eqcomd 2443	. . . . . . . . 9
80	79	oveq1d 6101	. . . . . . . 8
81	77, 80	eqtr3d 2472	. . . . . . 7
82		fveq2 5686	. . . . . . . . . . . . . . 15
83		oveq2 6094	. . . . . . . . . . . . . . . . 17
84	83	fveq2d 5690	. . . . . . . . . . . . . . . 16
85		oveq1 6093	. . . . . . . . . . . . . . . . 17
86		id 22	. . . . . . . . . . . . . . . . 17
87	85, 86	oveq12d 6104	. . . . . . . . . . . . . . . 16
88	84, 87	oveq12d 6104	. . . . . . . . . . . . . . 15
89	82, 88	oveq12d 6104	. . . . . . . . . . . . . 14
90	89	cbvmptv 4378	. . . . . . . . . . . . 13
91	31, 90	eqtri 2458	. . . . . . . . . . . 12
92	91	a1i 11	. . . . . . . . . . 11
93		fveq2 5686	. . . . . . . . . . . . 13
94		oveq2 6094	. . . . . . . . . . . . . . 15
95	94	fveq2d 5690	. . . . . . . . . . . . . 14
96		oveq1 6093	. . . . . . . . . . . . . . 15
97		id 22	. . . . . . . . . . . . . . 15
98	96, 97	oveq12d 6104	. . . . . . . . . . . . . 14
99	95, 98	oveq12d 6104	. . . . . . . . . . . . 13
100	93, 99	oveq12d 6104	. . . . . . . . . . . 12
101	100	adantl 466	. . . . . . . . . . 11 $/\$
102		2nn 10471	. . . . . . . . . . . . 13
103	102	a1i 11	. . . . . . . . . . . 12
104		id 22	. . . . . . . . . . . 12
105	103, 104	nnmulcld 10361	. . . . . . . . . . 11
106	57, 63, 75	divcld 10099	. . . . . . . . . . 11
107	92, 101, 105, 106	fvmptd 5774	. . . . . . . . . 10
108	107	oveq1d 6101	. . . . . . . . 9
109	108	eqcomd 2443	. . . . . . . 8
110	109	oveq1d 6101	. . . . . . 7
111		eqidd 2439	. . . . . . . . . . 11
112	99	adantl 466	. . . . . . . . . . 11 $/\$
113	111, 112, 105, 63	fvmptd 5774	. . . . . . . . . 10
114	113	oveq1d 6101	. . . . . . . . 9
115	114	eqcomd 2443	. . . . . . . 8
116	115	oveq2d 6102	. . . . . . 7
117	81, 110, 116	3eqtrd 2474	. . . . . 6
118	88	cbvmptv 4378	. . . . . . . . . . 11
119	118	a1i 11	. . . . . . . . . 10
120	119	fveq1d 5688	. . . . . . . . 9
121	120	eqcomd 2443	. . . . . . . 8
122	121	oveq1d 6101	. . . . . . 7
123	122	oveq2d 6102	. . . . . 6
124	107, 106	eqeltrd 2512	. . . . . . . . . 10
125		stirlinglem3.2	. . . . . . . . . . 11
126	125	fvmpt2 5776	. . . . . . . . . 10 $/\$
127	124, 126	mpdan 668	. . . . . . . . 9
128	127	eqcomd 2443	. . . . . . . 8
129	128	oveq1d 6101	. . . . . . 7
130	35	a1i 11	. . . . . . . . . 10
131	130	fveq1d 5688	. . . . . . . . 9
132	131	eqcomd 2443	. . . . . . . 8
133	132	oveq1d 6101	. . . . . . 7
134	129, 133	oveq12d 6104	. . . . . 6
135	117, 123, 134	3eqtrd 2474	. . . . 5
136	51, 135	oveq12d 6104	. . . 4
137	136	oveq1d 6101	. . 3
138	137	mpteq2ia 4369	. 2
139	41, 2	nn0mulcld 10633	. . . . . . . 8
140	6, 139	expcld 12000	. . . . . . 7
141	49, 44	eqeltrd 2512	. . . . . . 7
142	140, 141	mulcomd 9399	. . . . . 6
143	142	oveq1d 6101	. . . . 5
144	143	oveq1d 6101	. . . 4
145	127, 124	eqeltrd 2512	. . . . . . . 8
146	145	sqcld 11998	. . . . . . 7
147	130, 119	eqtrd 2470	. . . . . . . . . 10
148	147, 112, 105, 63	fvmptd 5774	. . . . . . . . 9
149	148, 63	eqeltrd 2512	. . . . . . . 8
150	149	sqcld 11998	. . . . . . 7
151		nnne0 10346	. . . . . . . . . . . 12
152	54, 55, 151	3syl 20	. . . . . . . . . . 11
153	57, 63, 152, 75	divne0d 10115	. . . . . . . . . 10
154	107, 153	eqnetrd 2621	. . . . . . . . 9
155	127, 154	eqnetrd 2621	. . . . . . . 8
156	145, 155, 72	expne0d 12006	. . . . . . 7
157	148, 75	eqnetrd 2621	. . . . . . . 8
158	149, 157, 72	expne0d 12006	. . . . . . 7
159	141, 146, 140, 150, 156, 158	divmuldivd 10140	. . . . . 6
160	159	eqcomd 2443	. . . . 5
161	160	oveq1d 6101	. . . 4
162	33, 30	eqeltrd 2512	. . . . . . . . 9
163	162, 41	expcld 12000	. . . . . . . 8
164	38, 45	eqeltrd 2512	. . . . . . . 8
165	163, 164, 146, 156	div23d 10136	. . . . . . 7
166	165	oveq1d 6101	. . . . . 6
167	166	oveq1d 6101	. . . . 5
168	163, 146, 156	divcld 10099	. . . . . . 7
169	140, 150, 158	divcld 10099	. . . . . . 7
170	168, 164, 169	mulassd 9401	. . . . . 6
171	170	oveq1d 6101	. . . . 5
172	164, 169	mulcld 9398	. . . . . . 7
173		ax-1cn 9332	. . . . . . . . 9
174	173	a1i 11	. . . . . . . 8
175	8, 174	addcld 9397	. . . . . . 7
176		0re 9378	. . . . . . . . . 10
177	176	a1i 11	. . . . . . . . 9
178	105	nnred 10329	. . . . . . . . 9
179		2re 10383	. . . . . . . . . . . 12
180	179	a1i 11	. . . . . . . . . . 11
181		nnre 10321	. . . . . . . . . . 11
182	180, 181	remulcld 9406	. . . . . . . . . 10
183		1re 9377	. . . . . . . . . . 11
184	183	a1i 11	. . . . . . . . . 10
185	182, 184	readdcld 9405	. . . . . . . . 9
186	105	nngt0d 10357	. . . . . . . . 9
187	178	ltp1d 10255	. . . . . . . . 9
188	177, 178, 185, 186, 187	lttrd 9524	. . . . . . . 8
189	188	gt0ne0d 9896	. . . . . . 7
190	168, 172, 175, 189	divassd 10134	. . . . . 6
191	164, 140, 150, 158	div12d 10135	. . . . . . . . . 10
192	9, 17, 41	mulexpd 12015	. . . . . . . . . . . . 13
193	60, 62	sqmuld 12012	. . . . . . . . . . . . 13
194	192, 193	oveq12d 6104	. . . . . . . . . . . 12
195	148	oveq1d 6101	. . . . . . . . . . . . 13
196	38, 195	oveq12d 6104	. . . . . . . . . . . 12
197	9, 41	expcld 12000	. . . . . . . . . . . . 13
198	60	sqcld 11998	. . . . . . . . . . . . 13
199	17, 41	expcld 12000	. . . . . . . . . . . . 13
200	62	sqcld 11998	. . . . . . . . . . . . 13
201	60, 67, 72	expne0d 12006	. . . . . . . . . . . . 13
202	62, 74, 72	expne0d 12006	. . . . . . . . . . . . 13
203	197, 198, 199, 200, 201, 202	divmuldivd 10140	. . . . . . . . . . . 12
204	194, 196, 203	3eqtr4d 2480	. . . . . . . . . . 11
205	204	oveq2d 6102	. . . . . . . . . 10
206	65	rprege0d 11026	. . . . . . . . . . . . . . . 16 $/\$
207		resqrth 12737	. . . . . . . . . . . . . . . 16 $/\$
208	206, 207	syl 16	. . . . . . . . . . . . . . 15
209	208	oveq2d 6102	. . . . . . . . . . . . . 14
210		2t2e4 10463	. . . . . . . . . . . . . . . . . . 19
211	210	eqcomi 2442	. . . . . . . . . . . . . . . . . 18
212	211	a1i 11	. . . . . . . . . . . . . . . . 17
213	212	oveq2d 6102	. . . . . . . . . . . . . . . 16
214	9, 53, 53	expmuld 12003	. . . . . . . . . . . . . . . 16
215	22	rprege0d 11026	. . . . . . . . . . . . . . . . . 18 $/\$
216		resqrth 12737	. . . . . . . . . . . . . . . . . 18 $/\$
217	215, 216	syl 16	. . . . . . . . . . . . . . . . 17
218	217	oveq1d 6101	. . . . . . . . . . . . . . . 16
219	213, 214, 218	3eqtrd 2474	. . . . . . . . . . . . . . 15
220	6, 6, 7	mulassd 9401	. . . . . . . . . . . . . . . 16
221	210	a1i 11	. . . . . . . . . . . . . . . . 17
222	221	oveq1d 6101	. . . . . . . . . . . . . . . 16
223	220, 222	eqtr3d 2472	. . . . . . . . . . . . . . 15
224	219, 223	oveq12d 6104	. . . . . . . . . . . . . 14
225	6, 7	sqmuld 12012	. . . . . . . . . . . . . . . . 17
226		sq2 11954	. . . . . . . . . . . . . . . . . . 19
227	226	a1i 11	. . . . . . . . . . . . . . . . . 18
228	227	oveq1d 6101	. . . . . . . . . . . . . . . . 17
229	225, 228	eqtrd 2470	. . . . . . . . . . . . . . . 16
230	229	oveq1d 6101	. . . . . . . . . . . . . . 15
231		4cn 10391	. . . . . . . . . . . . . . . . . . 19
232		4ne0 10410	. . . . . . . . . . . . . . . . . . 19
233	231, 232	dividi 10056	. . . . . . . . . . . . . . . . . 18
234	233	a1i 11	. . . . . . . . . . . . . . . . 17
235	7	sqvald 11997	. . . . . . . . . . . . . . . . . . 19
236	235	oveq1d 6101	. . . . . . . . . . . . . . . . . 18
237	7, 7, 25	divcan4d 10105	. . . . . . . . . . . . . . . . . 18
238	236, 237	eqtrd 2470	. . . . . . . . . . . . . . . . 17
239	234, 238	oveq12d 6104	. . . . . . . . . . . . . . . 16
240	41	nn0cnd 10630	. . . . . . . . . . . . . . . . 17
241	7	sqcld 11998	. . . . . . . . . . . . . . . . 17
242	232	a1i 11	. . . . . . . . . . . . . . . . 17
243	240, 240, 241, 7, 242, 25	divmuldivd 10140	. . . . . . . . . . . . . . . 16
244	7	mulid2d 9396	. . . . . . . . . . . . . . . 16
245	239, 243, 244	3eqtr3d 2478	. . . . . . . . . . . . . . 15
246	230, 245	eqtrd 2470	. . . . . . . . . . . . . 14
247	209, 224, 246	3eqtrd 2474	. . . . . . . . . . . . 13
248	7, 240	mulcomd 9399	. . . . . . . . . . . . . . . . 17
249	248	oveq2d 6102	. . . . . . . . . . . . . . . 16
250	16, 41, 2	expmuld 12003	. . . . . . . . . . . . . . . 16
251	7, 12, 15, 139	expdivd 12014	. . . . . . . . . . . . . . . 16
252	249, 250, 251	3eqtr3d 2478	. . . . . . . . . . . . . . 15
253	6, 7, 6	mul32d 9571	. . . . . . . . . . . . . . . . . 18
254	253, 222	eqtrd 2470	. . . . . . . . . . . . . . . . 17
255	254	oveq2d 6102	. . . . . . . . . . . . . . . 16
256	61, 53, 54	expmuld 12003	. . . . . . . . . . . . . . . 16
257	8, 12, 15, 139	expdivd 12014	. . . . . . . . . . . . . . . 16
258	255, 256, 257	3eqtr3d 2478	. . . . . . . . . . . . . . 15
259	252, 258	oveq12d 6104	. . . . . . . . . . . . . 14
260	252, 199	eqeltrrd 2513	. . . . . . . . . . . . . . 15
261	8, 139	expcld 12000	. . . . . . . . . . . . . . 15
262	12, 139	expcld 12000	. . . . . . . . . . . . . . 15
263	46, 27	zmulcld 10745	. . . . . . . . . . . . . . . 16
264	8, 69, 263	expne0d 12006	. . . . . . . . . . . . . . 15
265	12, 15, 263	expne0d 12006	. . . . . . . . . . . . . . 15
266	260, 261, 262, 264, 265	divdiv2d 10131	. . . . . . . . . . . . . 14
267	7, 139	expcld 12000	. . . . . . . . . . . . . . . . 17
268	267, 262, 265	divcan1d 10100	. . . . . . . . . . . . . . . 16
269	268	oveq1d 6101	. . . . . . . . . . . . . . 15
270	6, 7, 139	mulexpd 12015	. . . . . . . . . . . . . . . 16
271	270	oveq2d 6102	. . . . . . . . . . . . . . 15
272	140, 267	mulcomd 9399	. . . . . . . . . . . . . . . . 17
273	272	oveq2d 6102	. . . . . . . . . . . . . . . 16
274	7, 25, 263	expne0d 12006	. . . . . . . . . . . . . . . . 17
275	6, 68, 263	expne0d 12006	. . . . . . . . . . . . . . . . 17
276	267, 267, 140, 274, 275	divdiv1d 10130	. . . . . . . . . . . . . . . 16
277	267, 274	dividd 10097	. . . . . . . . . . . . . . . . 17
278	277	oveq1d 6101	. . . . . . . . . . . . . . . 16
279	273, 276, 278	3eqtr2d 2476	. . . . . . . . . . . . . . 15
280	269, 271, 279	3eqtrd 2474	. . . . . . . . . . . . . 14
281	259, 266, 280	3eqtrd 2474	. . . . . . . . . . . . 13
282	247, 281	oveq12d 6104	. . . . . . . . . . . 12
283	282	oveq2d 6102	. . . . . . . . . . 11
284	140, 275	reccld 10092	. . . . . . . . . . . 12
285	140, 7, 284	mul12d 9570	. . . . . . . . . . 11
286	7	mulid1d 9395	. . . . . . . . . . . 12
287	140, 275	recidd 10094	. . . . . . . . . . . . 13
288	287	oveq2d 6102	. . . . . . . . . . . 12
289	286, 288, 238	3eqtr4d 2480	. . . . . . . . . . 11
290	283, 285, 289	3eqtrd 2474	. . . . . . . . . 10
291	191, 205, 290	3eqtrd 2474	. . . . . . . . 9
292	291	oveq1d 6101	. . . . . . . 8
293	241, 7, 175, 25, 189	divdiv1d 10130	. . . . . . . 8
294	292, 293	eqtrd 2470	. . . . . . 7
295	294	oveq2d 6102	. . . . . 6
296	190, 295	eqtrd 2470	. . . . 5
297	167, 171, 296	3eqtrd 2474	. . . 4
298	144, 161, 297	3eqtrd 2474	. . 3
299	298	mpteq2ia 4369	. 2
300	1, 138, 299	3eqtri 2462	1

Colors of variables: wff setvar class

Syntax hints: $/\$ wa 369

wceq 1369

wcel 1756

wne 2601 class class class wbr 4287

cmpt 4345

cfv 5413 (class class class)co 6086

cc 9272

cr 9273

cc0 9274

c1 9275

caddc 9277

cmul 9279

cle 9411

cdiv 9985

cn 10314

c2 10363

c4 10365

cn0 10571

cz 10638

crp 10983

cexp 11857

cfa 12043

csqr 12714

ceu 13340

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2419 ax-rep 4398 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367 ax-inf2 7839 ax-cnex 9330 ax-resscn 9331 ax-1cn 9332 ax-icn 9333 ax-addcl 9334 ax-addrcl 9335 ax-mulcl 9336 ax-mulrcl 9337 ax-mulcom 9338 ax-addass 9339 ax-mulass 9340 ax-distr 9341 ax-i2m1 9342 ax-1ne0 9343 ax-1rid 9344 ax-rnegex 9345 ax-rrecex 9346 ax-cnre 9347 ax-pre-lttri 9348 ax-pre-lttrn 9349 ax-pre-ltadd 9350 ax-pre-mulgt0 9351 ax-pre-sup 9352 ax-addf 9353 ax-mulf 9354

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-fal 1375 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-nel 2604 df-ral 2715 df-rex 2716 df-reu 2717 df-rmo 2718 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-pss 3339 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-tp 3877 df-op 3879 df-uni 4087 df-int 4124 df-iun 4168 df-br 4288 df-opab 4346 df-mpt 4347 df-tr 4381 df-eprel 4627 df-id 4631 df-po 4636 df-so 4637 df-fr 4674 df-se 4675 df-we 4676 df-ord 4717 df-on 4718 df-lim 4719 df-suc 4720 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-riota 6047 df-ov 6089 df-oprab 6090 df-mpt2 6091 df-om 6472 df-1st 6572 df-2nd 6573 df-recs 6824 df-rdg 6858 df-1o 6912 df-oadd 6916 df-er 7093 df-pm 7209 df-en 7303 df-dom 7304 df-sdom 7305 df-fin 7306 df-sup 7683 df-oi 7716 df-card 8101 df-pnf 9412 df-mnf 9413 df-xr 9414 df-ltxr 9415 df-le 9416 df-sub 9589 df-neg 9590 df-div 9986 df-nn 10315 df-2 10372 df-3 10373 df-4 10374 df-n0 10572 df-z 10639 df-uz 10854 df-q 10946 df-rp 10984 df-ico 11298 df-fz 11430 df-fzo 11541 df-fl 11634 df-seq 11799 df-exp 11858 df-fac 12044 df-bc 12071 df-hash 12096 df-shft 12548 df-cj 12580 df-re 12581 df-im 12582 df-sqr 12716 df-abs 12717 df-limsup 12941 df-clim 12958 df-rlim 12959 df-sum 13156 df-ef 13345 df-e 13346

This theorem is referenced by: stirlinglem15 29854

W3C validator