stirlinglem3 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > stirlinglem3		Structured version Visualization version Unicode version

Theorem stirlinglem3 38050

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 10900	. . . . . . . . . . . . 13
3		faccl 12507	. . . . . . . . . . . . 13
4		nncn 10639	. . . . . . . . . . . . 13
5	2, 3, 4	3syl 18	. . . . . . . . . . . 12
6		2cnd 10704	. . . . . . . . . . . . . . 15
7		nncn 10639	. . . . . . . . . . . . . . 15
8	6, 7	mulcld 9681	. . . . . . . . . . . . . 14
9	8	sqrtcld 13576	. . . . . . . . . . . . 13
10		ere 14220	. . . . . . . . . . . . . . . . 17
11	10	recni 9673	. . . . . . . . . . . . . . . 16
12	11	a1i 11	. . . . . . . . . . . . . . 15
13		epos 14336	. . . . . . . . . . . . . . . . 17
14	10, 13	gt0ne0ii 10171	. . . . . . . . . . . . . . . 16
15	14	a1i 11	. . . . . . . . . . . . . . 15
16	7, 12, 15	divcld 10405	. . . . . . . . . . . . . 14
17	16, 2	expcld 12454	. . . . . . . . . . . . 13
18	9, 17	mulcld 9681	. . . . . . . . . . . 12
19		2rp 11330	. . . . . . . . . . . . . . . . 17
20	19	a1i 11	. . . . . . . . . . . . . . . 16
21		nnrp 11334	. . . . . . . . . . . . . . . 16
22	20, 21	rpmulcld 11380	. . . . . . . . . . . . . . 15
23	22	sqrtgt0d 13551	. . . . . . . . . . . . . 14
24	23	gt0ne0d 10199	. . . . . . . . . . . . 13
25		nnne0 10664	. . . . . . . . . . . . . . 15
26	7, 12, 25, 15	divne0d 10421	. . . . . . . . . . . . . 14
27		nnz 10983	. . . . . . . . . . . . . 14
28	16, 26, 27	expne0d 12460	. . . . . . . . . . . . 13
29	9, 17, 24, 28	mulne0d 10286	. . . . . . . . . . . 12
30	5, 18, 29	divcld 10405	. . . . . . . . . . 11
31		stirlinglem3.1	. . . . . . . . . . . 12
32	31	fvmpt2 5972	. . . . . . . . . . 11 $/\$
33	30, 32	mpdan 681	. . . . . . . . . 10
34	33	oveq1d 6323	. . . . . . . . 9
35		stirlinglem3.3	. . . . . . . . . . . 12
36	35	fvmpt2 5972	. . . . . . . . . . 11 $/\$
37	18, 36	mpdan 681	. . . . . . . . . 10
38	37	oveq1d 6323	. . . . . . . . 9
39	34, 38	oveq12d 6326	. . . . . . . 8
40		4nn0 10912	. . . . . . . . . . 11
41	40	a1i 11	. . . . . . . . . 10
42	5, 18, 29, 41	expdivd 12468	. . . . . . . . 9
43	42	oveq1d 6323	. . . . . . . 8
44	5, 41	expcld 12454	. . . . . . . . 9
45	18, 41	expcld 12454	. . . . . . . . 9
46	41	nn0zd 11061	. . . . . . . . . 10
47	18, 29, 46	expne0d 12460	. . . . . . . . 9
48	44, 45, 47	divcan1d 10406	. . . . . . . 8
49	39, 43, 48	3eqtrd 2509	. . . . . . 7
50	49	eqcomd 2477	. . . . . 6
51	50	oveq2d 6324	. . . . 5
52		2nn0 10910	. . . . . . . . . . . . 13
53	52	a1i 11	. . . . . . . . . . . 12
54	53, 2	nn0mulcld 10954	. . . . . . . . . . 11
55		faccl 12507	. . . . . . . . . . 11
56		nncn 10639	. . . . . . . . . . 11
57	54, 55, 56	3syl 18	. . . . . . . . . 10
58	57	sqcld 12452	. . . . . . . . 9
59	6, 8	mulcld 9681	. . . . . . . . . . . 12
60	59	sqrtcld 13576	. . . . . . . . . . 11
61	8, 12, 15	divcld 10405	. . . . . . . . . . . 12
62	61, 54	expcld 12454	. . . . . . . . . . 11
63	60, 62	mulcld 9681	. . . . . . . . . 10
64	63	sqcld 12452	. . . . . . . . 9
65	20, 22	rpmulcld 11380	. . . . . . . . . . . . 13
66	65	sqrtgt0d 13551	. . . . . . . . . . . 12
67	66	gt0ne0d 10199	. . . . . . . . . . 11
68	20	rpne0d 11369	. . . . . . . . . . . . . 14
69	6, 7, 68, 25	mulne0d 10286	. . . . . . . . . . . . 13
70	8, 12, 69, 15	divne0d 10421	. . . . . . . . . . . 12
71		2z 10993	. . . . . . . . . . . . . 14
72	71	a1i 11	. . . . . . . . . . . . 13
73	72, 27	zmulcld 11069	. . . . . . . . . . . 12
74	61, 70, 73	expne0d 12460	. . . . . . . . . . 11
75	60, 62, 67, 74	mulne0d 10286	. . . . . . . . . 10
76	63, 75, 72	expne0d 12460	. . . . . . . . 9
77	58, 64, 76	divcan1d 10406	. . . . . . . 8
78	57, 63, 75, 53	expdivd 12468	. . . . . . . . . 10
79	78	eqcomd 2477	. . . . . . . . 9
80	79	oveq1d 6323	. . . . . . . 8
81	77, 80	eqtr3d 2507	. . . . . . 7
82		fveq2 5879	. . . . . . . . . . . . . . 15
83		oveq2 6316	. . . . . . . . . . . . . . . . 17
84	83	fveq2d 5883	. . . . . . . . . . . . . . . 16
85		oveq1 6315	. . . . . . . . . . . . . . . . 17
86		id 22	. . . . . . . . . . . . . . . . 17
87	85, 86	oveq12d 6326	. . . . . . . . . . . . . . . 16
88	84, 87	oveq12d 6326	. . . . . . . . . . . . . . 15
89	82, 88	oveq12d 6326	. . . . . . . . . . . . . 14
90	89	cbvmptv 4488	. . . . . . . . . . . . 13
91	31, 90	eqtri 2493	. . . . . . . . . . . 12
92	91	a1i 11	. . . . . . . . . . 11
93		fveq2 5879	. . . . . . . . . . . . 13
94		oveq2 6316	. . . . . . . . . . . . . . 15
95	94	fveq2d 5883	. . . . . . . . . . . . . 14
96		oveq1 6315	. . . . . . . . . . . . . . 15
97		id 22	. . . . . . . . . . . . . . 15
98	96, 97	oveq12d 6326	. . . . . . . . . . . . . 14
99	95, 98	oveq12d 6326	. . . . . . . . . . . . 13
100	93, 99	oveq12d 6326	. . . . . . . . . . . 12
101	100	adantl 473	. . . . . . . . . . 11 $/\$
102		2nn 10790	. . . . . . . . . . . . 13
103	102	a1i 11	. . . . . . . . . . . 12
104		id 22	. . . . . . . . . . . 12
105	103, 104	nnmulcld 10679	. . . . . . . . . . 11
106	57, 63, 75	divcld 10405	. . . . . . . . . . 11
107	92, 101, 105, 106	fvmptd 5969	. . . . . . . . . 10
108	107	oveq1d 6323	. . . . . . . . 9
109	108	eqcomd 2477	. . . . . . . 8
110	109	oveq1d 6323	. . . . . . 7
111		eqidd 2472	. . . . . . . . . . 11
112	99	adantl 473	. . . . . . . . . . 11 $/\$
113	111, 112, 105, 63	fvmptd 5969	. . . . . . . . . 10
114	113	oveq1d 6323	. . . . . . . . 9
115	114	eqcomd 2477	. . . . . . . 8
116	115	oveq2d 6324	. . . . . . 7
117	81, 110, 116	3eqtrd 2509	. . . . . 6
118	88	cbvmptv 4488	. . . . . . . . . . 11
119	118	a1i 11	. . . . . . . . . 10
120	119	fveq1d 5881	. . . . . . . . 9
121	120	eqcomd 2477	. . . . . . . 8
122	121	oveq1d 6323	. . . . . . 7
123	122	oveq2d 6324	. . . . . 6
124	107, 106	eqeltrd 2549	. . . . . . . . . 10
125		stirlinglem3.2	. . . . . . . . . . 11
126	125	fvmpt2 5972	. . . . . . . . . 10 $/\$
127	124, 126	mpdan 681	. . . . . . . . 9
128	127	eqcomd 2477	. . . . . . . 8
129	128	oveq1d 6323	. . . . . . 7
130	35	a1i 11	. . . . . . . . . 10
131	130	fveq1d 5881	. . . . . . . . 9
132	131	eqcomd 2477	. . . . . . . 8
133	132	oveq1d 6323	. . . . . . 7
134	129, 133	oveq12d 6326	. . . . . 6
135	117, 123, 134	3eqtrd 2509	. . . . 5
136	51, 135	oveq12d 6326	. . . 4
137	136	oveq1d 6323	. . 3
138	137	mpteq2ia 4478	. 2
139	41, 2	nn0mulcld 10954	. . . . . . . 8
140	6, 139	expcld 12454	. . . . . . 7
141	49, 44	eqeltrd 2549	. . . . . . 7
142	140, 141	mulcomd 9682	. . . . . 6
143	142	oveq1d 6323	. . . . 5
144	143	oveq1d 6323	. . . 4
145	127, 124	eqeltrd 2549	. . . . . . . 8
146	145	sqcld 12452	. . . . . . 7
147	130, 119	eqtrd 2505	. . . . . . . . . 10
148	147, 112, 105, 63	fvmptd 5969	. . . . . . . . 9
149	148, 63	eqeltrd 2549	. . . . . . . 8
150	149	sqcld 12452	. . . . . . 7
151		nnne0 10664	. . . . . . . . . . . 12
152	54, 55, 151	3syl 18	. . . . . . . . . . 11
153	57, 63, 152, 75	divne0d 10421	. . . . . . . . . 10
154	107, 153	eqnetrd 2710	. . . . . . . . 9
155	127, 154	eqnetrd 2710	. . . . . . . 8
156	145, 155, 72	expne0d 12460	. . . . . . 7
157	148, 75	eqnetrd 2710	. . . . . . . 8
158	149, 157, 72	expne0d 12460	. . . . . . 7
159	141, 146, 140, 150, 156, 158	divmuldivd 10446	. . . . . 6
160	159	eqcomd 2477	. . . . 5
161	160	oveq1d 6323	. . . 4
162	33, 30	eqeltrd 2549	. . . . . . . . 9
163	162, 41	expcld 12454	. . . . . . . 8
164	38, 45	eqeltrd 2549	. . . . . . . 8
165	163, 164, 146, 156	div23d 10442	. . . . . . 7
166	165	oveq1d 6323	. . . . . 6
167	166	oveq1d 6323	. . . . 5
168	163, 146, 156	divcld 10405	. . . . . . 7
169	140, 150, 158	divcld 10405	. . . . . . 7
170	168, 164, 169	mulassd 9684	. . . . . 6
171	170	oveq1d 6323	. . . . 5
172	164, 169	mulcld 9681	. . . . . . 7
173		1cnd 9677	. . . . . . . 8
174	8, 173	addcld 9680	. . . . . . 7
175		0red 9662	. . . . . . . . 9
176	105	nnred 10646	. . . . . . . . 9
177		2re 10701	. . . . . . . . . . . 12
178	177	a1i 11	. . . . . . . . . . 11
179		nnre 10638	. . . . . . . . . . 11
180	178, 179	remulcld 9689	. . . . . . . . . 10
181		1red 9676	. . . . . . . . . 10
182	180, 181	readdcld 9688	. . . . . . . . 9
183	105	nngt0d 10675	. . . . . . . . 9
184	176	ltp1d 10559	. . . . . . . . 9
185	175, 176, 182, 183, 184	lttrd 9813	. . . . . . . 8
186	185	gt0ne0d 10199	. . . . . . 7
187	168, 172, 174, 186	divassd 10440	. . . . . 6
188	164, 140, 150, 158	div12d 10441	. . . . . . . . . 10
189	9, 17, 41	mulexpd 12469	. . . . . . . . . . . . 13
190	60, 62	sqmuld 12466	. . . . . . . . . . . . 13
191	189, 190	oveq12d 6326	. . . . . . . . . . . 12
192	148	oveq1d 6323	. . . . . . . . . . . . 13
193	38, 192	oveq12d 6326	. . . . . . . . . . . 12
194	9, 41	expcld 12454	. . . . . . . . . . . . 13
195	60	sqcld 12452	. . . . . . . . . . . . 13
196	17, 41	expcld 12454	. . . . . . . . . . . . 13
197	62	sqcld 12452	. . . . . . . . . . . . 13
198	60, 67, 72	expne0d 12460	. . . . . . . . . . . . 13
199	62, 74, 72	expne0d 12460	. . . . . . . . . . . . 13
200	194, 195, 196, 197, 198, 199	divmuldivd 10446	. . . . . . . . . . . 12
201	191, 193, 200	3eqtr4d 2515	. . . . . . . . . . 11
202	201	oveq2d 6324	. . . . . . . . . 10
203	65	rprege0d 11371	. . . . . . . . . . . . . . . 16 $/\$
204		resqrtth 13396	. . . . . . . . . . . . . . . 16 $/\$
205	203, 204	syl 17	. . . . . . . . . . . . . . 15
206	205	oveq2d 6324	. . . . . . . . . . . . . 14
207		2t2e4 10782	. . . . . . . . . . . . . . . . . . 19
208	207	eqcomi 2480	. . . . . . . . . . . . . . . . . 18
209	208	a1i 11	. . . . . . . . . . . . . . . . 17
210	209	oveq2d 6324	. . . . . . . . . . . . . . . 16
211	9, 53, 53	expmuld 12457	. . . . . . . . . . . . . . . 16
212	22	rprege0d 11371	. . . . . . . . . . . . . . . . . 18 $/\$
213		resqrtth 13396	. . . . . . . . . . . . . . . . . 18 $/\$
214	212, 213	syl 17	. . . . . . . . . . . . . . . . 17
215	214	oveq1d 6323	. . . . . . . . . . . . . . . 16
216	210, 211, 215	3eqtrd 2509	. . . . . . . . . . . . . . 15
217	6, 6, 7	mulassd 9684	. . . . . . . . . . . . . . . 16
218	207	a1i 11	. . . . . . . . . . . . . . . . 17
219	218	oveq1d 6323	. . . . . . . . . . . . . . . 16
220	217, 219	eqtr3d 2507	. . . . . . . . . . . . . . 15
221	216, 220	oveq12d 6326	. . . . . . . . . . . . . 14
222	6, 7	sqmuld 12466	. . . . . . . . . . . . . . . . 17
223		sq2 12409	. . . . . . . . . . . . . . . . . . 19
224	223	a1i 11	. . . . . . . . . . . . . . . . . 18
225	224	oveq1d 6323	. . . . . . . . . . . . . . . . 17
226	222, 225	eqtrd 2505	. . . . . . . . . . . . . . . 16
227	226	oveq1d 6323	. . . . . . . . . . . . . . 15
228		4cn 10709	. . . . . . . . . . . . . . . . . . 19
229		4ne0 10728	. . . . . . . . . . . . . . . . . . 19
230	228, 229	dividi 10362	. . . . . . . . . . . . . . . . . 18
231	230	a1i 11	. . . . . . . . . . . . . . . . 17
232	7	sqvald 12451	. . . . . . . . . . . . . . . . . . 19
233	232	oveq1d 6323	. . . . . . . . . . . . . . . . . 18
234	7, 7, 25	divcan4d 10411	. . . . . . . . . . . . . . . . . 18
235	233, 234	eqtrd 2505	. . . . . . . . . . . . . . . . 17
236	231, 235	oveq12d 6326	. . . . . . . . . . . . . . . 16
237	41	nn0cnd 10951	. . . . . . . . . . . . . . . . 17
238	7	sqcld 12452	. . . . . . . . . . . . . . . . 17
239	229	a1i 11	. . . . . . . . . . . . . . . . 17
240	237, 237, 238, 7, 239, 25	divmuldivd 10446	. . . . . . . . . . . . . . . 16
241	7	mulid2d 9679	. . . . . . . . . . . . . . . 16
242	236, 240, 241	3eqtr3d 2513	. . . . . . . . . . . . . . 15
243	227, 242	eqtrd 2505	. . . . . . . . . . . . . 14
244	206, 221, 243	3eqtrd 2509	. . . . . . . . . . . . 13
245	7, 237	mulcomd 9682	. . . . . . . . . . . . . . . . 17
246	245	oveq2d 6324	. . . . . . . . . . . . . . . 16
247	16, 41, 2	expmuld 12457	. . . . . . . . . . . . . . . 16
248	7, 12, 15, 139	expdivd 12468	. . . . . . . . . . . . . . . 16
249	246, 247, 248	3eqtr3d 2513	. . . . . . . . . . . . . . 15
250	6, 7, 6	mul32d 9861	. . . . . . . . . . . . . . . . . 18
251	250, 219	eqtrd 2505	. . . . . . . . . . . . . . . . 17
252	251	oveq2d 6324	. . . . . . . . . . . . . . . 16
253	61, 53, 54	expmuld 12457	. . . . . . . . . . . . . . . 16
254	8, 12, 15, 139	expdivd 12468	. . . . . . . . . . . . . . . 16
255	252, 253, 254	3eqtr3d 2513	. . . . . . . . . . . . . . 15
256	249, 255	oveq12d 6326	. . . . . . . . . . . . . 14
257	249, 196	eqeltrrd 2550	. . . . . . . . . . . . . . 15
258	8, 139	expcld 12454	. . . . . . . . . . . . . . 15
259	12, 139	expcld 12454	. . . . . . . . . . . . . . 15
260	46, 27	zmulcld 11069	. . . . . . . . . . . . . . . 16
261	8, 69, 260	expne0d 12460	. . . . . . . . . . . . . . 15
262	12, 15, 260	expne0d 12460	. . . . . . . . . . . . . . 15
263	257, 258, 259, 261, 262	divdiv2d 10437	. . . . . . . . . . . . . 14
264	7, 139	expcld 12454	. . . . . . . . . . . . . . . . 17
265	264, 259, 262	divcan1d 10406	. . . . . . . . . . . . . . . 16
266	265	oveq1d 6323	. . . . . . . . . . . . . . 15
267	6, 7, 139	mulexpd 12469	. . . . . . . . . . . . . . . 16
268	267	oveq2d 6324	. . . . . . . . . . . . . . 15
269	140, 264	mulcomd 9682	. . . . . . . . . . . . . . . . 17
270	269	oveq2d 6324	. . . . . . . . . . . . . . . 16
271	7, 25, 260	expne0d 12460	. . . . . . . . . . . . . . . . 17
272	6, 68, 260	expne0d 12460	. . . . . . . . . . . . . . . . 17
273	264, 264, 140, 271, 272	divdiv1d 10436	. . . . . . . . . . . . . . . 16
274	264, 271	dividd 10403	. . . . . . . . . . . . . . . . 17
275	274	oveq1d 6323	. . . . . . . . . . . . . . . 16
276	270, 273, 275	3eqtr2d 2511	. . . . . . . . . . . . . . 15
277	266, 268, 276	3eqtrd 2509	. . . . . . . . . . . . . 14
278	256, 263, 277	3eqtrd 2509	. . . . . . . . . . . . 13
279	244, 278	oveq12d 6326	. . . . . . . . . . . 12
280	279	oveq2d 6324	. . . . . . . . . . 11
281	140, 272	reccld 10398	. . . . . . . . . . . 12
282	140, 7, 281	mul12d 9860	. . . . . . . . . . 11
283	7	mulid1d 9678	. . . . . . . . . . . 12
284	140, 272	recidd 10400	. . . . . . . . . . . . 13
285	284	oveq2d 6324	. . . . . . . . . . . 12
286	283, 285, 235	3eqtr4d 2515	. . . . . . . . . . 11
287	280, 282, 286	3eqtrd 2509	. . . . . . . . . 10
288	188, 202, 287	3eqtrd 2509	. . . . . . . . 9
289	288	oveq1d 6323	. . . . . . . 8
290	238, 7, 174, 25, 186	divdiv1d 10436	. . . . . . . 8
291	289, 290	eqtrd 2505	. . . . . . 7
292	291	oveq2d 6324	. . . . . 6
293	187, 292	eqtrd 2505	. . . . 5
294	167, 171, 293	3eqtrd 2509	. . . 4
295	144, 161, 294	3eqtrd 2509	. . 3
296	295	mpteq2ia 4478	. 2
297	1, 138, 296	3eqtri 2497	1

Colors of variables: wff setvar class

Syntax hints: $/\$ wa 376

wceq 1452

wcel 1904

wne 2641 class class class wbr 4395

cmpt 4454

cfv 5589 (class class class)co 6308

cc 9555

cr 9556

cc0 9557

c1 9558

caddc 9560

cmul 9562

cle 9694

cdiv 10291

cn 10631

c2 10681

c4 10683

cn0 10893

cz 10961

crp 11325

cexp 12310

cfa 12497

csqrt 13373

ceu 14192

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-inf2 8164 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635 ax-addf 9636 ax-mulf 9637

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-fal 1458 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-se 4799 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-isom 5598 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-oadd 7204 df-er 7381 df-pm 7493 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-sup 7974 df-inf 7975 df-oi 8043 df-card 8391 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-2 10690 df-3 10691 df-4 10692 df-n0 10894 df-z 10962 df-uz 11183 df-q 11288 df-rp 11326 df-ico 11666 df-fz 11811 df-fzo 11943 df-fl 12061 df-seq 12252 df-exp 12311 df-fac 12498 df-bc 12526 df-hash 12554 df-shft 13207 df-cj 13239 df-re 13240 df-im 13241 df-sqrt 13375 df-abs 13376 df-limsup 13603 df-clim 13629 df-rlim 13630 df-sum 13830 df-ef 14198 df-e 14199

This theorem is referenced by: stirlinglem15 38062

W3C validator