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 30018

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 10696	. . . . . . . . . . . . 13
3		faccl 12177	. . . . . . . . . . . . 13
4		nncn 10440	. . . . . . . . . . . . 13
5	2, 3, 4	3syl 20	. . . . . . . . . . . 12
6		2cnd 10504	. . . . . . . . . . . . . . 15
7		nncn 10440	. . . . . . . . . . . . . . 15
8	6, 7	mulcld 9516	. . . . . . . . . . . . . 14
9	8	sqrcld 13040	. . . . . . . . . . . . 13
10		ere 13491	. . . . . . . . . . . . . . . . 17
11	10	recni 9508	. . . . . . . . . . . . . . . 16
12	11	a1i 11	. . . . . . . . . . . . . . 15
13		epos 13606	. . . . . . . . . . . . . . . . 17
14	10, 13	gt0ne0ii 9986	. . . . . . . . . . . . . . . 16
15	14	a1i 11	. . . . . . . . . . . . . . 15
16	7, 12, 15	divcld 10217	. . . . . . . . . . . . . 14
17	16, 2	expcld 12124	. . . . . . . . . . . . 13
18	9, 17	mulcld 9516	. . . . . . . . . . . 12
19		2rp 11106	. . . . . . . . . . . . . . . . 17
20	19	a1i 11	. . . . . . . . . . . . . . . 16
21		nnrp 11110	. . . . . . . . . . . . . . . 16
22	20, 21	rpmulcld 11153	. . . . . . . . . . . . . . 15
23	22	sqrgt0d 13016	. . . . . . . . . . . . . 14
24	23	gt0ne0d 10014	. . . . . . . . . . . . 13
25		nnne0 10464	. . . . . . . . . . . . . . 15
26	7, 12, 25, 15	divne0d 10233	. . . . . . . . . . . . . 14
27		nnz 10778	. . . . . . . . . . . . . 14
28	16, 26, 27	expne0d 12130	. . . . . . . . . . . . 13
29	9, 17, 24, 28	mulne0d 10098	. . . . . . . . . . . 12
30	5, 18, 29	divcld 10217	. . . . . . . . . . 11
31		stirlinglem3.1	. . . . . . . . . . . 12
32	31	fvmpt2 5889	. . . . . . . . . . 11 $/\$
33	30, 32	mpdan 668	. . . . . . . . . 10
34	33	oveq1d 6214	. . . . . . . . 9
35		stirlinglem3.3	. . . . . . . . . . . 12
36	35	fvmpt2 5889	. . . . . . . . . . 11 $/\$
37	18, 36	mpdan 668	. . . . . . . . . 10
38	37	oveq1d 6214	. . . . . . . . 9
39	34, 38	oveq12d 6217	. . . . . . . 8
40		4nn0 10708	. . . . . . . . . . 11
41	40	a1i 11	. . . . . . . . . 10
42	5, 18, 29, 41	expdivd 12138	. . . . . . . . 9
43	42	oveq1d 6214	. . . . . . . 8
44	5, 41	expcld 12124	. . . . . . . . 9
45	18, 41	expcld 12124	. . . . . . . . 9
46	41	nn0zd 10855	. . . . . . . . . 10
47	18, 29, 46	expne0d 12130	. . . . . . . . 9
48	44, 45, 47	divcan1d 10218	. . . . . . . 8
49	39, 43, 48	3eqtrd 2499	. . . . . . 7
50	49	eqcomd 2462	. . . . . 6
51	50	oveq2d 6215	. . . . 5
52		2nn0 10706	. . . . . . . . . . . . 13
53	52	a1i 11	. . . . . . . . . . . 12
54	53, 2	nn0mulcld 10751	. . . . . . . . . . 11
55		faccl 12177	. . . . . . . . . . 11
56		nncn 10440	. . . . . . . . . . 11
57	54, 55, 56	3syl 20	. . . . . . . . . 10
58	57	sqcld 12122	. . . . . . . . 9
59	6, 8	mulcld 9516	. . . . . . . . . . . 12
60	59	sqrcld 13040	. . . . . . . . . . 11
61	8, 12, 15	divcld 10217	. . . . . . . . . . . 12
62	61, 54	expcld 12124	. . . . . . . . . . 11
63	60, 62	mulcld 9516	. . . . . . . . . 10
64	63	sqcld 12122	. . . . . . . . 9
65	20, 22	rpmulcld 11153	. . . . . . . . . . . . 13
66	65	sqrgt0d 13016	. . . . . . . . . . . 12
67	66	gt0ne0d 10014	. . . . . . . . . . 11
68	20	rpne0d 11142	. . . . . . . . . . . . . 14
69	6, 7, 68, 25	mulne0d 10098	. . . . . . . . . . . . 13
70	8, 12, 69, 15	divne0d 10233	. . . . . . . . . . . 12
71		2z 10788	. . . . . . . . . . . . . 14
72	71	a1i 11	. . . . . . . . . . . . 13
73	72, 27	zmulcld 10863	. . . . . . . . . . . 12
74	61, 70, 73	expne0d 12130	. . . . . . . . . . 11
75	60, 62, 67, 74	mulne0d 10098	. . . . . . . . . 10
76	63, 75, 72	expne0d 12130	. . . . . . . . 9
77	58, 64, 76	divcan1d 10218	. . . . . . . 8
78	57, 63, 75, 53	expdivd 12138	. . . . . . . . . 10
79	78	eqcomd 2462	. . . . . . . . 9
80	79	oveq1d 6214	. . . . . . . 8
81	77, 80	eqtr3d 2497	. . . . . . 7
82		fveq2 5798	. . . . . . . . . . . . . . 15
83		oveq2 6207	. . . . . . . . . . . . . . . . 17
84	83	fveq2d 5802	. . . . . . . . . . . . . . . 16
85		oveq1 6206	. . . . . . . . . . . . . . . . 17
86		id 22	. . . . . . . . . . . . . . . . 17
87	85, 86	oveq12d 6217	. . . . . . . . . . . . . . . 16
88	84, 87	oveq12d 6217	. . . . . . . . . . . . . . 15
89	82, 88	oveq12d 6217	. . . . . . . . . . . . . 14
90	89	cbvmptv 4490	. . . . . . . . . . . . 13
91	31, 90	eqtri 2483	. . . . . . . . . . . 12
92	91	a1i 11	. . . . . . . . . . 11
93		fveq2 5798	. . . . . . . . . . . . 13
94		oveq2 6207	. . . . . . . . . . . . . . 15
95	94	fveq2d 5802	. . . . . . . . . . . . . 14
96		oveq1 6206	. . . . . . . . . . . . . . 15
97		id 22	. . . . . . . . . . . . . . 15
98	96, 97	oveq12d 6217	. . . . . . . . . . . . . 14
99	95, 98	oveq12d 6217	. . . . . . . . . . . . 13
100	93, 99	oveq12d 6217	. . . . . . . . . . . 12
101	100	adantl 466	. . . . . . . . . . 11 $/\$
102		2nn 10589	. . . . . . . . . . . . 13
103	102	a1i 11	. . . . . . . . . . . 12
104		id 22	. . . . . . . . . . . 12
105	103, 104	nnmulcld 10479	. . . . . . . . . . 11
106	57, 63, 75	divcld 10217	. . . . . . . . . . 11
107	92, 101, 105, 106	fvmptd 5887	. . . . . . . . . 10
108	107	oveq1d 6214	. . . . . . . . 9
109	108	eqcomd 2462	. . . . . . . 8
110	109	oveq1d 6214	. . . . . . 7
111		eqidd 2455	. . . . . . . . . . 11
112	99	adantl 466	. . . . . . . . . . 11 $/\$
113	111, 112, 105, 63	fvmptd 5887	. . . . . . . . . 10
114	113	oveq1d 6214	. . . . . . . . 9
115	114	eqcomd 2462	. . . . . . . 8
116	115	oveq2d 6215	. . . . . . 7
117	81, 110, 116	3eqtrd 2499	. . . . . 6
118	88	cbvmptv 4490	. . . . . . . . . . 11
119	118	a1i 11	. . . . . . . . . 10
120	119	fveq1d 5800	. . . . . . . . 9
121	120	eqcomd 2462	. . . . . . . 8
122	121	oveq1d 6214	. . . . . . 7
123	122	oveq2d 6215	. . . . . 6
124	107, 106	eqeltrd 2542	. . . . . . . . . 10
125		stirlinglem3.2	. . . . . . . . . . 11
126	125	fvmpt2 5889	. . . . . . . . . 10 $/\$
127	124, 126	mpdan 668	. . . . . . . . 9
128	127	eqcomd 2462	. . . . . . . 8
129	128	oveq1d 6214	. . . . . . 7
130	35	a1i 11	. . . . . . . . . 10
131	130	fveq1d 5800	. . . . . . . . 9
132	131	eqcomd 2462	. . . . . . . 8
133	132	oveq1d 6214	. . . . . . 7
134	129, 133	oveq12d 6217	. . . . . 6
135	117, 123, 134	3eqtrd 2499	. . . . 5
136	51, 135	oveq12d 6217	. . . 4
137	136	oveq1d 6214	. . 3
138	137	mpteq2ia 4481	. 2
139	41, 2	nn0mulcld 10751	. . . . . . . 8
140	6, 139	expcld 12124	. . . . . . 7
141	49, 44	eqeltrd 2542	. . . . . . 7
142	140, 141	mulcomd 9517	. . . . . 6
143	142	oveq1d 6214	. . . . 5
144	143	oveq1d 6214	. . . 4
145	127, 124	eqeltrd 2542	. . . . . . . 8
146	145	sqcld 12122	. . . . . . 7
147	130, 119	eqtrd 2495	. . . . . . . . . 10
148	147, 112, 105, 63	fvmptd 5887	. . . . . . . . 9
149	148, 63	eqeltrd 2542	. . . . . . . 8
150	149	sqcld 12122	. . . . . . 7
151		nnne0 10464	. . . . . . . . . . . 12
152	54, 55, 151	3syl 20	. . . . . . . . . . 11
153	57, 63, 152, 75	divne0d 10233	. . . . . . . . . 10
154	107, 153	eqnetrd 2744	. . . . . . . . 9
155	127, 154	eqnetrd 2744	. . . . . . . 8
156	145, 155, 72	expne0d 12130	. . . . . . 7
157	148, 75	eqnetrd 2744	. . . . . . . 8
158	149, 157, 72	expne0d 12130	. . . . . . 7
159	141, 146, 140, 150, 156, 158	divmuldivd 10258	. . . . . 6
160	159	eqcomd 2462	. . . . 5
161	160	oveq1d 6214	. . . 4
162	33, 30	eqeltrd 2542	. . . . . . . . 9
163	162, 41	expcld 12124	. . . . . . . 8
164	38, 45	eqeltrd 2542	. . . . . . . 8
165	163, 164, 146, 156	div23d 10254	. . . . . . 7
166	165	oveq1d 6214	. . . . . 6
167	166	oveq1d 6214	. . . . 5
168	163, 146, 156	divcld 10217	. . . . . . 7
169	140, 150, 158	divcld 10217	. . . . . . 7
170	168, 164, 169	mulassd 9519	. . . . . 6
171	170	oveq1d 6214	. . . . 5
172	164, 169	mulcld 9516	. . . . . . 7
173		ax-1cn 9450	. . . . . . . . 9
174	173	a1i 11	. . . . . . . 8
175	8, 174	addcld 9515	. . . . . . 7
176		0re 9496	. . . . . . . . . 10
177	176	a1i 11	. . . . . . . . 9
178	105	nnred 10447	. . . . . . . . 9
179		2re 10501	. . . . . . . . . . . 12
180	179	a1i 11	. . . . . . . . . . 11
181		nnre 10439	. . . . . . . . . . 11
182	180, 181	remulcld 9524	. . . . . . . . . 10
183		1re 9495	. . . . . . . . . . 11
184	183	a1i 11	. . . . . . . . . 10
185	182, 184	readdcld 9523	. . . . . . . . 9
186	105	nngt0d 10475	. . . . . . . . 9
187	178	ltp1d 10373	. . . . . . . . 9
188	177, 178, 185, 186, 187	lttrd 9642	. . . . . . . 8
189	188	gt0ne0d 10014	. . . . . . 7
190	168, 172, 175, 189	divassd 10252	. . . . . 6
191	164, 140, 150, 158	div12d 10253	. . . . . . . . . 10
192	9, 17, 41	mulexpd 12139	. . . . . . . . . . . . 13
193	60, 62	sqmuld 12136	. . . . . . . . . . . . 13
194	192, 193	oveq12d 6217	. . . . . . . . . . . 12
195	148	oveq1d 6214	. . . . . . . . . . . . 13
196	38, 195	oveq12d 6217	. . . . . . . . . . . 12
197	9, 41	expcld 12124	. . . . . . . . . . . . 13
198	60	sqcld 12122	. . . . . . . . . . . . 13
199	17, 41	expcld 12124	. . . . . . . . . . . . 13
200	62	sqcld 12122	. . . . . . . . . . . . 13
201	60, 67, 72	expne0d 12130	. . . . . . . . . . . . 13
202	62, 74, 72	expne0d 12130	. . . . . . . . . . . . 13
203	197, 198, 199, 200, 201, 202	divmuldivd 10258	. . . . . . . . . . . 12
204	194, 196, 203	3eqtr4d 2505	. . . . . . . . . . 11
205	204	oveq2d 6215	. . . . . . . . . 10
206	65	rprege0d 11144	. . . . . . . . . . . . . . . 16 $/\$
207		resqrth 12862	. . . . . . . . . . . . . . . 16 $/\$
208	206, 207	syl 16	. . . . . . . . . . . . . . 15
209	208	oveq2d 6215	. . . . . . . . . . . . . 14
210		2t2e4 10581	. . . . . . . . . . . . . . . . . . 19
211	210	eqcomi 2467	. . . . . . . . . . . . . . . . . 18
212	211	a1i 11	. . . . . . . . . . . . . . . . 17
213	212	oveq2d 6215	. . . . . . . . . . . . . . . 16
214	9, 53, 53	expmuld 12127	. . . . . . . . . . . . . . . 16
215	22	rprege0d 11144	. . . . . . . . . . . . . . . . . 18 $/\$
216		resqrth 12862	. . . . . . . . . . . . . . . . . 18 $/\$
217	215, 216	syl 16	. . . . . . . . . . . . . . . . 17
218	217	oveq1d 6214	. . . . . . . . . . . . . . . 16
219	213, 214, 218	3eqtrd 2499	. . . . . . . . . . . . . . 15
220	6, 6, 7	mulassd 9519	. . . . . . . . . . . . . . . 16
221	210	a1i 11	. . . . . . . . . . . . . . . . 17
222	221	oveq1d 6214	. . . . . . . . . . . . . . . 16
223	220, 222	eqtr3d 2497	. . . . . . . . . . . . . . 15
224	219, 223	oveq12d 6217	. . . . . . . . . . . . . 14
225	6, 7	sqmuld 12136	. . . . . . . . . . . . . . . . 17
226		sq2 12078	. . . . . . . . . . . . . . . . . . 19
227	226	a1i 11	. . . . . . . . . . . . . . . . . 18
228	227	oveq1d 6214	. . . . . . . . . . . . . . . . 17
229	225, 228	eqtrd 2495	. . . . . . . . . . . . . . . 16
230	229	oveq1d 6214	. . . . . . . . . . . . . . 15
231		4cn 10509	. . . . . . . . . . . . . . . . . . 19
232		4ne0 10528	. . . . . . . . . . . . . . . . . . 19
233	231, 232	dividi 10174	. . . . . . . . . . . . . . . . . 18
234	233	a1i 11	. . . . . . . . . . . . . . . . 17
235	7	sqvald 12121	. . . . . . . . . . . . . . . . . . 19
236	235	oveq1d 6214	. . . . . . . . . . . . . . . . . 18
237	7, 7, 25	divcan4d 10223	. . . . . . . . . . . . . . . . . 18
238	236, 237	eqtrd 2495	. . . . . . . . . . . . . . . . 17
239	234, 238	oveq12d 6217	. . . . . . . . . . . . . . . 16
240	41	nn0cnd 10748	. . . . . . . . . . . . . . . . 17
241	7	sqcld 12122	. . . . . . . . . . . . . . . . 17
242	232	a1i 11	. . . . . . . . . . . . . . . . 17
243	240, 240, 241, 7, 242, 25	divmuldivd 10258	. . . . . . . . . . . . . . . 16
244	7	mulid2d 9514	. . . . . . . . . . . . . . . 16
245	239, 243, 244	3eqtr3d 2503	. . . . . . . . . . . . . . 15
246	230, 245	eqtrd 2495	. . . . . . . . . . . . . 14
247	209, 224, 246	3eqtrd 2499	. . . . . . . . . . . . 13
248	7, 240	mulcomd 9517	. . . . . . . . . . . . . . . . 17
249	248	oveq2d 6215	. . . . . . . . . . . . . . . 16
250	16, 41, 2	expmuld 12127	. . . . . . . . . . . . . . . 16
251	7, 12, 15, 139	expdivd 12138	. . . . . . . . . . . . . . . 16
252	249, 250, 251	3eqtr3d 2503	. . . . . . . . . . . . . . 15
253	6, 7, 6	mul32d 9689	. . . . . . . . . . . . . . . . . 18
254	253, 222	eqtrd 2495	. . . . . . . . . . . . . . . . 17
255	254	oveq2d 6215	. . . . . . . . . . . . . . . 16
256	61, 53, 54	expmuld 12127	. . . . . . . . . . . . . . . 16
257	8, 12, 15, 139	expdivd 12138	. . . . . . . . . . . . . . . 16
258	255, 256, 257	3eqtr3d 2503	. . . . . . . . . . . . . . 15
259	252, 258	oveq12d 6217	. . . . . . . . . . . . . 14
260	252, 199	eqeltrrd 2543	. . . . . . . . . . . . . . 15
261	8, 139	expcld 12124	. . . . . . . . . . . . . . 15
262	12, 139	expcld 12124	. . . . . . . . . . . . . . 15
263	46, 27	zmulcld 10863	. . . . . . . . . . . . . . . 16
264	8, 69, 263	expne0d 12130	. . . . . . . . . . . . . . 15
265	12, 15, 263	expne0d 12130	. . . . . . . . . . . . . . 15
266	260, 261, 262, 264, 265	divdiv2d 10249	. . . . . . . . . . . . . 14
267	7, 139	expcld 12124	. . . . . . . . . . . . . . . . 17
268	267, 262, 265	divcan1d 10218	. . . . . . . . . . . . . . . 16
269	268	oveq1d 6214	. . . . . . . . . . . . . . 15
270	6, 7, 139	mulexpd 12139	. . . . . . . . . . . . . . . 16
271	270	oveq2d 6215	. . . . . . . . . . . . . . 15
272	140, 267	mulcomd 9517	. . . . . . . . . . . . . . . . 17
273	272	oveq2d 6215	. . . . . . . . . . . . . . . 16
274	7, 25, 263	expne0d 12130	. . . . . . . . . . . . . . . . 17
275	6, 68, 263	expne0d 12130	. . . . . . . . . . . . . . . . 17
276	267, 267, 140, 274, 275	divdiv1d 10248	. . . . . . . . . . . . . . . 16
277	267, 274	dividd 10215	. . . . . . . . . . . . . . . . 17
278	277	oveq1d 6214	. . . . . . . . . . . . . . . 16
279	273, 276, 278	3eqtr2d 2501	. . . . . . . . . . . . . . 15
280	269, 271, 279	3eqtrd 2499	. . . . . . . . . . . . . 14
281	259, 266, 280	3eqtrd 2499	. . . . . . . . . . . . 13
282	247, 281	oveq12d 6217	. . . . . . . . . . . 12
283	282	oveq2d 6215	. . . . . . . . . . 11
284	140, 275	reccld 10210	. . . . . . . . . . . 12
285	140, 7, 284	mul12d 9688	. . . . . . . . . . 11
286	7	mulid1d 9513	. . . . . . . . . . . 12
287	140, 275	recidd 10212	. . . . . . . . . . . . 13
288	287	oveq2d 6215	. . . . . . . . . . . 12
289	286, 288, 238	3eqtr4d 2505	. . . . . . . . . . 11
290	283, 285, 289	3eqtrd 2499	. . . . . . . . . 10
291	191, 205, 290	3eqtrd 2499	. . . . . . . . 9
292	291	oveq1d 6214	. . . . . . . 8
293	241, 7, 175, 25, 189	divdiv1d 10248	. . . . . . . 8
294	292, 293	eqtrd 2495	. . . . . . 7
295	294	oveq2d 6215	. . . . . 6
296	190, 295	eqtrd 2495	. . . . 5
297	167, 171, 296	3eqtrd 2499	. . . 4
298	144, 161, 297	3eqtrd 2499	. . 3
299	298	mpteq2ia 4481	. 2
300	1, 138, 299	3eqtri 2487	1

Colors of variables: wff setvar class

Syntax hints: $/\$ wa 369

wceq 1370

wcel 1758

wne 2647 class class class wbr 4399

cmpt 4457

cfv 5525 (class class class)co 6199

cc 9390

cr 9391

cc0 9392

c1 9393

caddc 9395

cmul 9397

cle 9529

cdiv 10103

cn 10432

c2 10481

c4 10483

cn0 10689

cz 10756

crp 11101

cexp 11981

cfa 12167

csqr 12839

ceu 13465

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-rep 4510 ax-sep 4520 ax-nul 4528 ax-pow 4577 ax-pr 4638 ax-un 6481 ax-inf2 7957 ax-cnex 9448 ax-resscn 9449 ax-1cn 9450 ax-icn 9451 ax-addcl 9452 ax-addrcl 9453 ax-mulcl 9454 ax-mulrcl 9455 ax-mulcom 9456 ax-addass 9457 ax-mulass 9458 ax-distr 9459 ax-i2m1 9460 ax-1ne0 9461 ax-1rid 9462 ax-rnegex 9463 ax-rrecex 9464 ax-cnre 9465 ax-pre-lttri 9466 ax-pre-lttrn 9467 ax-pre-ltadd 9468 ax-pre-mulgt0 9469 ax-pre-sup 9470 ax-addf 9471 ax-mulf 9472

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-fal 1376 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2649 df-nel 2650 df-ral 2803 df-rex 2804 df-reu 2805 df-rmo 2806 df-rab 2807 df-v 3078 df-sbc 3293 df-csb 3395 df-dif 3438 df-un 3440 df-in 3442 df-ss 3449 df-pss 3451 df-nul 3745 df-if 3899 df-pw 3969 df-sn 3985 df-pr 3987 df-tp 3989 df-op 3991 df-uni 4199 df-int 4236 df-iun 4280 df-br 4400 df-opab 4458 df-mpt 4459 df-tr 4493 df-eprel 4739 df-id 4743 df-po 4748 df-so 4749 df-fr 4786 df-se 4787 df-we 4788 df-ord 4829 df-on 4830 df-lim 4831 df-suc 4832 df-xp 4953 df-rel 4954 df-cnv 4955 df-co 4956 df-dm 4957 df-rn 4958 df-res 4959 df-ima 4960 df-iota 5488 df-fun 5527 df-fn 5528 df-f 5529 df-f1 5530 df-fo 5531 df-f1o 5532 df-fv 5533 df-isom 5534 df-riota 6160 df-ov 6202 df-oprab 6203 df-mpt2 6204 df-om 6586 df-1st 6686 df-2nd 6687 df-recs 6941 df-rdg 6975 df-1o 7029 df-oadd 7033 df-er 7210 df-pm 7326 df-en 7420 df-dom 7421 df-sdom 7422 df-fin 7423 df-sup 7801 df-oi 7834 df-card 8219 df-pnf 9530 df-mnf 9531 df-xr 9532 df-ltxr 9533 df-le 9534 df-sub 9707 df-neg 9708 df-div 10104 df-nn 10433 df-2 10490 df-3 10491 df-4 10492 df-n0 10690 df-z 10757 df-uz 10972 df-q 11064 df-rp 11102 df-ico 11416 df-fz 11554 df-fzo 11665 df-fl 11758 df-seq 11923 df-exp 11982 df-fac 12168 df-bc 12195 df-hash 12220 df-shft 12673 df-cj 12705 df-re 12706 df-im 12707 df-sqr 12841 df-abs 12842 df-limsup 13066 df-clim 13083 df-rlim 13084 df-sum 13281 df-ef 13470 df-e 13471

This theorem is referenced by: stirlinglem15 30030

W3C validator