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 29717

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 10574	. . . . . . . . . . . . 13
3		faccl 12045	. . . . . . . . . . . . 13
4		nncn 10318	. . . . . . . . . . . . 13
5	2, 3, 4	3syl 20	. . . . . . . . . . . 12
6		2cnd 10382	. . . . . . . . . . . . . . 15
7		nncn 10318	. . . . . . . . . . . . . . 15
8	6, 7	mulcld 9394	. . . . . . . . . . . . . 14
9	8	sqrcld 12907	. . . . . . . . . . . . 13
10		ere 13357	. . . . . . . . . . . . . . . . 17
11	10	recni 9386	. . . . . . . . . . . . . . . 16
12	11	a1i 11	. . . . . . . . . . . . . . 15
13		epos 13472	. . . . . . . . . . . . . . . . 17
14	10, 13	gt0ne0ii 9864	. . . . . . . . . . . . . . . 16
15	14	a1i 11	. . . . . . . . . . . . . . 15
16	7, 12, 15	divcld 10095	. . . . . . . . . . . . . 14
17	16, 2	expcld 11992	. . . . . . . . . . . . 13
18	9, 17	mulcld 9394	. . . . . . . . . . . 12
19		2rp 10984	. . . . . . . . . . . . . . . . 17
20	19	a1i 11	. . . . . . . . . . . . . . . 16
21		nnrp 10988	. . . . . . . . . . . . . . . 16
22	20, 21	rpmulcld 11031	. . . . . . . . . . . . . . 15
23	22	sqrgt0d 12883	. . . . . . . . . . . . . 14
24	23	gt0ne0d 9892	. . . . . . . . . . . . 13
25		nnne0 10342	. . . . . . . . . . . . . . 15
26	7, 12, 25, 15	divne0d 10111	. . . . . . . . . . . . . 14
27		nnz 10656	. . . . . . . . . . . . . 14
28	16, 26, 27	expne0d 11998	. . . . . . . . . . . . 13
29	9, 17, 24, 28	mulne0d 9976	. . . . . . . . . . . 12
30	5, 18, 29	divcld 10095	. . . . . . . . . . 11
31		stirlinglem3.1	. . . . . . . . . . . 12
32	31	fvmpt2 5769	. . . . . . . . . . 11 $/\$
33	30, 32	mpdan 661	. . . . . . . . . 10
34	33	oveq1d 6095	. . . . . . . . 9
35		stirlinglem3.3	. . . . . . . . . . . 12
36	35	fvmpt2 5769	. . . . . . . . . . 11 $/\$
37	18, 36	mpdan 661	. . . . . . . . . 10
38	37	oveq1d 6095	. . . . . . . . 9
39	34, 38	oveq12d 6098	. . . . . . . 8
40		4nn0 10586	. . . . . . . . . . 11
41	40	a1i 11	. . . . . . . . . 10
42	5, 18, 29, 41	expdivd 12006	. . . . . . . . 9
43	42	oveq1d 6095	. . . . . . . 8
44	5, 41	expcld 11992	. . . . . . . . 9
45	18, 41	expcld 11992	. . . . . . . . 9
46	41	nn0zd 10733	. . . . . . . . . 10
47	18, 29, 46	expne0d 11998	. . . . . . . . 9
48	44, 45, 47	divcan1d 10096	. . . . . . . 8
49	39, 43, 48	3eqtrd 2469	. . . . . . 7
50	49	eqcomd 2438	. . . . . 6
51	50	oveq2d 6096	. . . . 5
52		2nn0 10584	. . . . . . . . . . . . 13
53	52	a1i 11	. . . . . . . . . . . 12
54	53, 2	nn0mulcld 10629	. . . . . . . . . . 11
55		faccl 12045	. . . . . . . . . . 11
56		nncn 10318	. . . . . . . . . . 11
57	54, 55, 56	3syl 20	. . . . . . . . . 10
58	57	sqcld 11990	. . . . . . . . 9
59	6, 8	mulcld 9394	. . . . . . . . . . . 12
60	59	sqrcld 12907	. . . . . . . . . . 11
61	8, 12, 15	divcld 10095	. . . . . . . . . . . 12
62	61, 54	expcld 11992	. . . . . . . . . . 11
63	60, 62	mulcld 9394	. . . . . . . . . 10
64	63	sqcld 11990	. . . . . . . . 9
65	20, 22	rpmulcld 11031	. . . . . . . . . . . . 13
66	65	sqrgt0d 12883	. . . . . . . . . . . 12
67	66	gt0ne0d 9892	. . . . . . . . . . 11
68	20	rpne0d 11020	. . . . . . . . . . . . . 14
69	6, 7, 68, 25	mulne0d 9976	. . . . . . . . . . . . 13
70	8, 12, 69, 15	divne0d 10111	. . . . . . . . . . . 12
71		2z 10666	. . . . . . . . . . . . . 14
72	71	a1i 11	. . . . . . . . . . . . 13
73	72, 27	zmulcld 10741	. . . . . . . . . . . 12
74	61, 70, 73	expne0d 11998	. . . . . . . . . . 11
75	60, 62, 67, 74	mulne0d 9976	. . . . . . . . . 10
76	63, 75, 72	expne0d 11998	. . . . . . . . 9
77	58, 64, 76	divcan1d 10096	. . . . . . . 8
78	57, 63, 75, 53	expdivd 12006	. . . . . . . . . 10
79	78	eqcomd 2438	. . . . . . . . 9
80	79	oveq1d 6095	. . . . . . . 8
81	77, 80	eqtr3d 2467	. . . . . . 7
82		fveq2 5679	. . . . . . . . . . . . . . 15
83		oveq2 6088	. . . . . . . . . . . . . . . . 17
84	83	fveq2d 5683	. . . . . . . . . . . . . . . 16
85		oveq1 6087	. . . . . . . . . . . . . . . . 17
86		id 22	. . . . . . . . . . . . . . . . 17
87	85, 86	oveq12d 6098	. . . . . . . . . . . . . . . 16
88	84, 87	oveq12d 6098	. . . . . . . . . . . . . . 15
89	82, 88	oveq12d 6098	. . . . . . . . . . . . . 14
90	89	cbvmptv 4371	. . . . . . . . . . . . 13
91	31, 90	eqtri 2453	. . . . . . . . . . . 12
92	91	a1i 11	. . . . . . . . . . 11
93		fveq2 5679	. . . . . . . . . . . . 13
94		oveq2 6088	. . . . . . . . . . . . . . 15
95	94	fveq2d 5683	. . . . . . . . . . . . . 14
96		oveq1 6087	. . . . . . . . . . . . . . 15
97		id 22	. . . . . . . . . . . . . . 15
98	96, 97	oveq12d 6098	. . . . . . . . . . . . . 14
99	95, 98	oveq12d 6098	. . . . . . . . . . . . 13
100	93, 99	oveq12d 6098	. . . . . . . . . . . 12
101	100	adantl 463	. . . . . . . . . . 11 $/\$
102		2nn 10467	. . . . . . . . . . . . 13
103	102	a1i 11	. . . . . . . . . . . 12
104		id 22	. . . . . . . . . . . 12
105	103, 104	nnmulcld 10357	. . . . . . . . . . 11
106	57, 63, 75	divcld 10095	. . . . . . . . . . 11
107	92, 101, 105, 106	fvmptd 5767	. . . . . . . . . 10
108	107	oveq1d 6095	. . . . . . . . 9
109	108	eqcomd 2438	. . . . . . . 8
110	109	oveq1d 6095	. . . . . . 7
111		eqidd 2434	. . . . . . . . . . 11
112	99	adantl 463	. . . . . . . . . . 11 $/\$
113	111, 112, 105, 63	fvmptd 5767	. . . . . . . . . 10
114	113	oveq1d 6095	. . . . . . . . 9
115	114	eqcomd 2438	. . . . . . . 8
116	115	oveq2d 6096	. . . . . . 7
117	81, 110, 116	3eqtrd 2469	. . . . . 6
118	88	cbvmptv 4371	. . . . . . . . . . 11
119	118	a1i 11	. . . . . . . . . 10
120	119	fveq1d 5681	. . . . . . . . 9
121	120	eqcomd 2438	. . . . . . . 8
122	121	oveq1d 6095	. . . . . . 7
123	122	oveq2d 6096	. . . . . 6
124	107, 106	eqeltrd 2507	. . . . . . . . . 10
125		stirlinglem3.2	. . . . . . . . . . 11
126	125	fvmpt2 5769	. . . . . . . . . 10 $/\$
127	124, 126	mpdan 661	. . . . . . . . 9
128	127	eqcomd 2438	. . . . . . . 8
129	128	oveq1d 6095	. . . . . . 7
130	35	a1i 11	. . . . . . . . . 10
131	130	fveq1d 5681	. . . . . . . . 9
132	131	eqcomd 2438	. . . . . . . 8
133	132	oveq1d 6095	. . . . . . 7
134	129, 133	oveq12d 6098	. . . . . 6
135	117, 123, 134	3eqtrd 2469	. . . . 5
136	51, 135	oveq12d 6098	. . . 4
137	136	oveq1d 6095	. . 3
138	137	mpteq2ia 4362	. 2
139	41, 2	nn0mulcld 10629	. . . . . . . 8
140	6, 139	expcld 11992	. . . . . . 7
141	49, 44	eqeltrd 2507	. . . . . . 7
142	140, 141	mulcomd 9395	. . . . . 6
143	142	oveq1d 6095	. . . . 5
144	143	oveq1d 6095	. . . 4
145	127, 124	eqeltrd 2507	. . . . . . . 8
146	145	sqcld 11990	. . . . . . 7
147	130, 119	eqtrd 2465	. . . . . . . . . 10
148	147, 112, 105, 63	fvmptd 5767	. . . . . . . . 9
149	148, 63	eqeltrd 2507	. . . . . . . 8
150	149	sqcld 11990	. . . . . . 7
151		nnne0 10342	. . . . . . . . . . . 12
152	54, 55, 151	3syl 20	. . . . . . . . . . 11
153	57, 63, 152, 75	divne0d 10111	. . . . . . . . . 10
154	107, 153	eqnetrd 2616	. . . . . . . . 9
155	127, 154	eqnetrd 2616	. . . . . . . 8
156	145, 155, 72	expne0d 11998	. . . . . . 7
157	148, 75	eqnetrd 2616	. . . . . . . 8
158	149, 157, 72	expne0d 11998	. . . . . . 7
159	141, 146, 140, 150, 156, 158	divmuldivd 10136	. . . . . 6
160	159	eqcomd 2438	. . . . 5
161	160	oveq1d 6095	. . . 4
162	33, 30	eqeltrd 2507	. . . . . . . . 9
163	162, 41	expcld 11992	. . . . . . . 8
164	38, 45	eqeltrd 2507	. . . . . . . 8
165	163, 164, 146, 156	div23d 10132	. . . . . . 7
166	165	oveq1d 6095	. . . . . 6
167	166	oveq1d 6095	. . . . 5
168	163, 146, 156	divcld 10095	. . . . . . 7
169	140, 150, 158	divcld 10095	. . . . . . 7
170	168, 164, 169	mulassd 9397	. . . . . 6
171	170	oveq1d 6095	. . . . 5
172	164, 169	mulcld 9394	. . . . . . 7
173		ax-1cn 9328	. . . . . . . . 9
174	173	a1i 11	. . . . . . . 8
175	8, 174	addcld 9393	. . . . . . 7
176		0re 9374	. . . . . . . . . 10
177	176	a1i 11	. . . . . . . . 9
178	105	nnred 10325	. . . . . . . . 9
179		2re 10379	. . . . . . . . . . . 12
180	179	a1i 11	. . . . . . . . . . 11
181		nnre 10317	. . . . . . . . . . 11
182	180, 181	remulcld 9402	. . . . . . . . . 10
183		1re 9373	. . . . . . . . . . 11
184	183	a1i 11	. . . . . . . . . 10
185	182, 184	readdcld 9401	. . . . . . . . 9
186	105	nngt0d 10353	. . . . . . . . 9
187	178	ltp1d 10251	. . . . . . . . 9
188	177, 178, 185, 186, 187	lttrd 9520	. . . . . . . 8
189	188	gt0ne0d 9892	. . . . . . 7
190	168, 172, 175, 189	divassd 10130	. . . . . 6
191	164, 140, 150, 158	div12d 10131	. . . . . . . . . 10
192	9, 17, 41	mulexpd 12007	. . . . . . . . . . . . 13
193	60, 62	sqmuld 12004	. . . . . . . . . . . . 13
194	192, 193	oveq12d 6098	. . . . . . . . . . . 12
195	148	oveq1d 6095	. . . . . . . . . . . . 13
196	38, 195	oveq12d 6098	. . . . . . . . . . . 12
197	9, 41	expcld 11992	. . . . . . . . . . . . 13
198	60	sqcld 11990	. . . . . . . . . . . . 13
199	17, 41	expcld 11992	. . . . . . . . . . . . 13
200	62	sqcld 11990	. . . . . . . . . . . . 13
201	60, 67, 72	expne0d 11998	. . . . . . . . . . . . 13
202	62, 74, 72	expne0d 11998	. . . . . . . . . . . . 13
203	197, 198, 199, 200, 201, 202	divmuldivd 10136	. . . . . . . . . . . 12
204	194, 196, 203	3eqtr4d 2475	. . . . . . . . . . 11
205	204	oveq2d 6096	. . . . . . . . . 10
206	65	rprege0d 11022	. . . . . . . . . . . . . . . 16 $/\$
207		resqrth 12729	. . . . . . . . . . . . . . . 16 $/\$
208	206, 207	syl 16	. . . . . . . . . . . . . . 15
209	208	oveq2d 6096	. . . . . . . . . . . . . 14
210		2t2e4 10459	. . . . . . . . . . . . . . . . . . 19
211	210	eqcomi 2437	. . . . . . . . . . . . . . . . . 18
212	211	a1i 11	. . . . . . . . . . . . . . . . 17
213	212	oveq2d 6096	. . . . . . . . . . . . . . . 16
214	9, 53, 53	expmuld 11995	. . . . . . . . . . . . . . . 16
215	22	rprege0d 11022	. . . . . . . . . . . . . . . . . 18 $/\$
216		resqrth 12729	. . . . . . . . . . . . . . . . . 18 $/\$
217	215, 216	syl 16	. . . . . . . . . . . . . . . . 17
218	217	oveq1d 6095	. . . . . . . . . . . . . . . 16
219	213, 214, 218	3eqtrd 2469	. . . . . . . . . . . . . . 15
220	6, 6, 7	mulassd 9397	. . . . . . . . . . . . . . . 16
221	210	a1i 11	. . . . . . . . . . . . . . . . 17
222	221	oveq1d 6095	. . . . . . . . . . . . . . . 16
223	220, 222	eqtr3d 2467	. . . . . . . . . . . . . . 15
224	219, 223	oveq12d 6098	. . . . . . . . . . . . . 14
225	6, 7	sqmuld 12004	. . . . . . . . . . . . . . . . 17
226		sq2 11946	. . . . . . . . . . . . . . . . . . 19
227	226	a1i 11	. . . . . . . . . . . . . . . . . 18
228	227	oveq1d 6095	. . . . . . . . . . . . . . . . 17
229	225, 228	eqtrd 2465	. . . . . . . . . . . . . . . 16
230	229	oveq1d 6095	. . . . . . . . . . . . . . 15
231		4cn 10387	. . . . . . . . . . . . . . . . . . 19
232		4ne0 10406	. . . . . . . . . . . . . . . . . . 19
233	231, 232	dividi 10052	. . . . . . . . . . . . . . . . . 18
234	233	a1i 11	. . . . . . . . . . . . . . . . 17
235	7	sqvald 11989	. . . . . . . . . . . . . . . . . . 19
236	235	oveq1d 6095	. . . . . . . . . . . . . . . . . 18
237	7, 7, 25	divcan4d 10101	. . . . . . . . . . . . . . . . . 18
238	236, 237	eqtrd 2465	. . . . . . . . . . . . . . . . 17
239	234, 238	oveq12d 6098	. . . . . . . . . . . . . . . 16
240	41	nn0cnd 10626	. . . . . . . . . . . . . . . . 17
241	7	sqcld 11990	. . . . . . . . . . . . . . . . 17
242	232	a1i 11	. . . . . . . . . . . . . . . . 17
243	240, 240, 241, 7, 242, 25	divmuldivd 10136	. . . . . . . . . . . . . . . 16
244	7	mulid2d 9392	. . . . . . . . . . . . . . . 16
245	239, 243, 244	3eqtr3d 2473	. . . . . . . . . . . . . . 15
246	230, 245	eqtrd 2465	. . . . . . . . . . . . . 14
247	209, 224, 246	3eqtrd 2469	. . . . . . . . . . . . 13
248	7, 240	mulcomd 9395	. . . . . . . . . . . . . . . . 17
249	248	oveq2d 6096	. . . . . . . . . . . . . . . 16
250	16, 41, 2	expmuld 11995	. . . . . . . . . . . . . . . 16
251	7, 12, 15, 139	expdivd 12006	. . . . . . . . . . . . . . . 16
252	249, 250, 251	3eqtr3d 2473	. . . . . . . . . . . . . . 15
253	6, 7, 6	mul32d 9567	. . . . . . . . . . . . . . . . . 18
254	253, 222	eqtrd 2465	. . . . . . . . . . . . . . . . 17
255	254	oveq2d 6096	. . . . . . . . . . . . . . . 16
256	61, 53, 54	expmuld 11995	. . . . . . . . . . . . . . . 16
257	8, 12, 15, 139	expdivd 12006	. . . . . . . . . . . . . . . 16
258	255, 256, 257	3eqtr3d 2473	. . . . . . . . . . . . . . 15
259	252, 258	oveq12d 6098	. . . . . . . . . . . . . 14
260	252, 199	eqeltrrd 2508	. . . . . . . . . . . . . . 15
261	8, 139	expcld 11992	. . . . . . . . . . . . . . 15
262	12, 139	expcld 11992	. . . . . . . . . . . . . . 15
263	46, 27	zmulcld 10741	. . . . . . . . . . . . . . . 16
264	8, 69, 263	expne0d 11998	. . . . . . . . . . . . . . 15
265	12, 15, 263	expne0d 11998	. . . . . . . . . . . . . . 15
266	260, 261, 262, 264, 265	divdiv2d 10127	. . . . . . . . . . . . . 14
267	7, 139	expcld 11992	. . . . . . . . . . . . . . . . 17
268	267, 262, 265	divcan1d 10096	. . . . . . . . . . . . . . . 16
269	268	oveq1d 6095	. . . . . . . . . . . . . . 15
270	6, 7, 139	mulexpd 12007	. . . . . . . . . . . . . . . 16
271	270	oveq2d 6096	. . . . . . . . . . . . . . 15
272	140, 267	mulcomd 9395	. . . . . . . . . . . . . . . . 17
273	272	oveq2d 6096	. . . . . . . . . . . . . . . 16
274	7, 25, 263	expne0d 11998	. . . . . . . . . . . . . . . . 17
275	6, 68, 263	expne0d 11998	. . . . . . . . . . . . . . . . 17
276	267, 267, 140, 274, 275	divdiv1d 10126	. . . . . . . . . . . . . . . 16
277	267, 274	dividd 10093	. . . . . . . . . . . . . . . . 17
278	277	oveq1d 6095	. . . . . . . . . . . . . . . 16
279	273, 276, 278	3eqtr2d 2471	. . . . . . . . . . . . . . 15
280	269, 271, 279	3eqtrd 2469	. . . . . . . . . . . . . 14
281	259, 266, 280	3eqtrd 2469	. . . . . . . . . . . . 13
282	247, 281	oveq12d 6098	. . . . . . . . . . . 12
283	282	oveq2d 6096	. . . . . . . . . . 11
284	140, 275	reccld 10088	. . . . . . . . . . . 12
285	140, 7, 284	mul12d 9566	. . . . . . . . . . 11
286	7	mulid1d 9391	. . . . . . . . . . . 12
287	140, 275	recidd 10090	. . . . . . . . . . . . 13
288	287	oveq2d 6096	. . . . . . . . . . . 12
289	286, 288, 238	3eqtr4d 2475	. . . . . . . . . . 11
290	283, 285, 289	3eqtrd 2469	. . . . . . . . . 10
291	191, 205, 290	3eqtrd 2469	. . . . . . . . 9
292	291	oveq1d 6095	. . . . . . . 8
293	241, 7, 175, 25, 189	divdiv1d 10126	. . . . . . . 8
294	292, 293	eqtrd 2465	. . . . . . 7
295	294	oveq2d 6096	. . . . . 6
296	190, 295	eqtrd 2465	. . . . 5
297	167, 171, 296	3eqtrd 2469	. . . 4
298	144, 161, 297	3eqtrd 2469	. . 3
299	298	mpteq2ia 4362	. 2
300	1, 138, 299	3eqtri 2457	1

Colors of variables: wff setvar class

Syntax hints: $/\$ wa 369

wceq 1362

wcel 1755

wne 2596 class class class wbr 4280

cmpt 4338

cfv 5406 (class class class)co 6080

cc 9268

cr 9269

cc0 9270

c1 9271

caddc 9273

cmul 9275

cle 9407

cdiv 9981

cn 10310

c2 10359

c4 10361

cn0 10567

cz 10634

crp 10979

cexp 11849

cfa 12035

csqr 12706

ceu 13331

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1594 ax-4 1605 ax-5 1669 ax-6 1707 ax-7 1727 ax-8 1757 ax-9 1759 ax-10 1774 ax-11 1779 ax-12 1791 ax-13 1942 ax-ext 2414 ax-rep 4391 ax-sep 4401 ax-nul 4409 ax-pow 4458 ax-pr 4519 ax-un 6361 ax-inf2 7835 ax-cnex 9326 ax-resscn 9327 ax-1cn 9328 ax-icn 9329 ax-addcl 9330 ax-addrcl 9331 ax-mulcl 9332 ax-mulrcl 9333 ax-mulcom 9334 ax-addass 9335 ax-mulass 9336 ax-distr 9337 ax-i2m1 9338 ax-1ne0 9339 ax-1rid 9340 ax-rnegex 9341 ax-rrecex 9342 ax-cnre 9343 ax-pre-lttri 9344 ax-pre-lttrn 9345 ax-pre-ltadd 9346 ax-pre-mulgt0 9347 ax-pre-sup 9348 ax-addf 9349 ax-mulf 9350

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 959 df-3an 960 df-tru 1365 df-fal 1368 df-ex 1590 df-nf 1593 df-sb 1700 df-eu 2258 df-mo 2259 df-clab 2420 df-cleq 2426 df-clel 2429 df-nfc 2558 df-ne 2598 df-nel 2599 df-ral 2710 df-rex 2711 df-reu 2712 df-rmo 2713 df-rab 2714 df-v 2964 df-sbc 3176 df-csb 3277 df-dif 3319 df-un 3321 df-in 3323 df-ss 3330 df-pss 3332 df-nul 3626 df-if 3780 df-pw 3850 df-sn 3866 df-pr 3868 df-tp 3870 df-op 3872 df-uni 4080 df-int 4117 df-iun 4161 df-br 4281 df-opab 4339 df-mpt 4340 df-tr 4374 df-eprel 4619 df-id 4623 df-po 4628 df-so 4629 df-fr 4666 df-se 4667 df-we 4668 df-ord 4709 df-on 4710 df-lim 4711 df-suc 4712 df-xp 4833 df-rel 4834 df-cnv 4835 df-co 4836 df-dm 4837 df-rn 4838 df-res 4839 df-ima 4840 df-iota 5369 df-fun 5408 df-fn 5409 df-f 5410 df-f1 5411 df-fo 5412 df-f1o 5413 df-fv 5414 df-isom 5415 df-riota 6039 df-ov 6083 df-oprab 6084 df-mpt2 6085 df-om 6466 df-1st 6566 df-2nd 6567 df-recs 6818 df-rdg 6852 df-1o 6908 df-oadd 6912 df-er 7089 df-pm 7205 df-en 7299 df-dom 7300 df-sdom 7301 df-fin 7302 df-sup 7679 df-oi 7712 df-card 8097 df-pnf 9408 df-mnf 9409 df-xr 9410 df-ltxr 9411 df-le 9412 df-sub 9585 df-neg 9586 df-div 9982 df-nn 10311 df-2 10368 df-3 10369 df-4 10370 df-n0 10568 df-z 10635 df-uz 10850 df-q 10942 df-rp 10980 df-ico 11294 df-fz 11425 df-fzo 11533 df-fl 11626 df-seq 11791 df-exp 11850 df-fac 12036 df-bc 12063 df-hash 12088 df-shft 12540 df-cj 12572 df-re 12573 df-im 12574 df-sqr 12708 df-abs 12709 df-limsup 12933 df-clim 12950 df-rlim 12951 df-sum 13148 df-ef 13336 df-e 13337

This theorem is referenced by: stirlinglem15 29729

W3C validator