stirlinglem3 - Mathbox for Glauco Siliprandi

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

Theorem stirlinglem3 27692

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 10184	. . . . . . . . . . . . 13
3		faccl 11531	. . . . . . . . . . . . 13
4		nncn 9964	. . . . . . . . . . . . 13
5	2, 3, 4	3syl 19	. . . . . . . . . . . 12
6		2cn 10026	. . . . . . . . . . . . . . . 16
7	6	a1i 11	. . . . . . . . . . . . . . 15
8		nncn 9964	. . . . . . . . . . . . . . 15
9	7, 8	mulcld 9064	. . . . . . . . . . . . . 14
10	9	sqrcld 12194	. . . . . . . . . . . . 13
11		ere 12646	. . . . . . . . . . . . . . . . 17
12	11	recni 9058	. . . . . . . . . . . . . . . 16
13	12	a1i 11	. . . . . . . . . . . . . . 15
14		epos 12761	. . . . . . . . . . . . . . . . 17
15	11, 14	gt0ne0ii 9519	. . . . . . . . . . . . . . . 16
16	15	a1i 11	. . . . . . . . . . . . . . 15
17	8, 13, 16	divcld 9746	. . . . . . . . . . . . . 14
18	17, 2	expcld 11478	. . . . . . . . . . . . 13
19	10, 18	mulcld 9064	. . . . . . . . . . . 12
20		2rp 10573	. . . . . . . . . . . . . . . . 17
21	20	a1i 11	. . . . . . . . . . . . . . . 16
22		nnrp 10577	. . . . . . . . . . . . . . . 16
23	21, 22	rpmulcld 10620	. . . . . . . . . . . . . . 15
24	23	sqrgt0d 12170	. . . . . . . . . . . . . 14
25	24	gt0ne0d 9547	. . . . . . . . . . . . 13
26		nnne0 9988	. . . . . . . . . . . . . . 15
27	8, 13, 26, 16	divne0d 9762	. . . . . . . . . . . . . 14
28		nnz 10259	. . . . . . . . . . . . . 14
29	17, 27, 28	expne0d 11484	. . . . . . . . . . . . 13
30	10, 18, 25, 29	mulne0d 9630	. . . . . . . . . . . 12
31	5, 19, 30	divcld 9746	. . . . . . . . . . 11
32		stirlinglem3.1	. . . . . . . . . . . 12
33	32	fvmpt2 5771	. . . . . . . . . . 11 $/\$
34	31, 33	mpdan 650	. . . . . . . . . 10
35	34	oveq1d 6055	. . . . . . . . 9
36		stirlinglem3.3	. . . . . . . . . . . 12
37	36	fvmpt2 5771	. . . . . . . . . . 11 $/\$
38	19, 37	mpdan 650	. . . . . . . . . 10
39	38	oveq1d 6055	. . . . . . . . 9
40	35, 39	oveq12d 6058	. . . . . . . 8
41		4nn0 10196	. . . . . . . . . . 11
42	41	a1i 11	. . . . . . . . . 10
43	5, 19, 30, 42	expdivd 11492	. . . . . . . . 9
44	43	oveq1d 6055	. . . . . . . 8
45	5, 42	expcld 11478	. . . . . . . . 9
46	19, 42	expcld 11478	. . . . . . . . 9
47	42	nn0zd 10329	. . . . . . . . . 10
48	19, 30, 47	expne0d 11484	. . . . . . . . 9
49	45, 46, 48	divcan1d 9747	. . . . . . . 8
50	40, 44, 49	3eqtrd 2440	. . . . . . 7
51	50	eqcomd 2409	. . . . . 6
52	51	oveq2d 6056	. . . . 5
53		2nn0 10194	. . . . . . . . . . . . 13
54	53	a1i 11	. . . . . . . . . . . 12
55	54, 2	nn0mulcld 10235	. . . . . . . . . . 11
56		faccl 11531	. . . . . . . . . . 11
57		nncn 9964	. . . . . . . . . . 11
58	55, 56, 57	3syl 19	. . . . . . . . . 10
59	58	sqcld 11476	. . . . . . . . 9
60	7, 9	mulcld 9064	. . . . . . . . . . . 12
61	60	sqrcld 12194	. . . . . . . . . . 11
62	9, 13, 16	divcld 9746	. . . . . . . . . . . 12
63	62, 55	expcld 11478	. . . . . . . . . . 11
64	61, 63	mulcld 9064	. . . . . . . . . 10
65	64	sqcld 11476	. . . . . . . . 9
66	21, 23	rpmulcld 10620	. . . . . . . . . . . . 13
67	66	sqrgt0d 12170	. . . . . . . . . . . 12
68	67	gt0ne0d 9547	. . . . . . . . . . 11
69	21	rpne0d 10609	. . . . . . . . . . . . . 14
70	7, 8, 69, 26	mulne0d 9630	. . . . . . . . . . . . 13
71	9, 13, 70, 16	divne0d 9762	. . . . . . . . . . . 12
72		2z 10268	. . . . . . . . . . . . . 14
73	72	a1i 11	. . . . . . . . . . . . 13
74	73, 28	zmulcld 10337	. . . . . . . . . . . 12
75	62, 71, 74	expne0d 11484	. . . . . . . . . . 11
76	61, 63, 68, 75	mulne0d 9630	. . . . . . . . . 10
77	64, 76, 73	expne0d 11484	. . . . . . . . 9
78	59, 65, 77	divcan1d 9747	. . . . . . . 8
79	58, 64, 76, 54	expdivd 11492	. . . . . . . . . 10
80	79	eqcomd 2409	. . . . . . . . 9
81	80	oveq1d 6055	. . . . . . . 8
82	78, 81	eqtr3d 2438	. . . . . . 7
83		fveq2 5687	. . . . . . . . . . . . . . 15
84		oveq2 6048	. . . . . . . . . . . . . . . . 17
85	84	fveq2d 5691	. . . . . . . . . . . . . . . 16
86		oveq1 6047	. . . . . . . . . . . . . . . . 17
87		id 20	. . . . . . . . . . . . . . . . 17
88	86, 87	oveq12d 6058	. . . . . . . . . . . . . . . 16
89	85, 88	oveq12d 6058	. . . . . . . . . . . . . . 15
90	83, 89	oveq12d 6058	. . . . . . . . . . . . . 14
91	90	cbvmptv 4260	. . . . . . . . . . . . 13
92	32, 91	eqtri 2424	. . . . . . . . . . . 12
93	92	a1i 11	. . . . . . . . . . 11
94		fveq2 5687	. . . . . . . . . . . . 13
95		oveq2 6048	. . . . . . . . . . . . . . 15
96	95	fveq2d 5691	. . . . . . . . . . . . . 14
97		oveq1 6047	. . . . . . . . . . . . . . 15
98		id 20	. . . . . . . . . . . . . . 15
99	97, 98	oveq12d 6058	. . . . . . . . . . . . . 14
100	96, 99	oveq12d 6058	. . . . . . . . . . . . 13
101	94, 100	oveq12d 6058	. . . . . . . . . . . 12
102	101	adantl 453	. . . . . . . . . . 11 $/\$
103		2nn 10089	. . . . . . . . . . . . 13
104	103	a1i 11	. . . . . . . . . . . 12
105		id 20	. . . . . . . . . . . 12
106	104, 105	nnmulcld 10003	. . . . . . . . . . 11
107	58, 64, 76	divcld 9746	. . . . . . . . . . 11
108	93, 102, 106, 107	fvmptd 5769	. . . . . . . . . 10
109	108	oveq1d 6055	. . . . . . . . 9
110	109	eqcomd 2409	. . . . . . . 8
111	110	oveq1d 6055	. . . . . . 7
112		eqidd 2405	. . . . . . . . . . 11
113	100	adantl 453	. . . . . . . . . . 11 $/\$
114	112, 113, 106, 64	fvmptd 5769	. . . . . . . . . 10
115	114	oveq1d 6055	. . . . . . . . 9
116	115	eqcomd 2409	. . . . . . . 8
117	116	oveq2d 6056	. . . . . . 7
118	82, 111, 117	3eqtrd 2440	. . . . . 6
119	89	cbvmptv 4260	. . . . . . . . . . 11
120	119	a1i 11	. . . . . . . . . 10
121	120	fveq1d 5689	. . . . . . . . 9
122	121	eqcomd 2409	. . . . . . . 8
123	122	oveq1d 6055	. . . . . . 7
124	123	oveq2d 6056	. . . . . 6
125	108, 107	eqeltrd 2478	. . . . . . . . . 10
126		stirlinglem3.2	. . . . . . . . . . 11
127	126	fvmpt2 5771	. . . . . . . . . 10 $/\$
128	125, 127	mpdan 650	. . . . . . . . 9
129	128	eqcomd 2409	. . . . . . . 8
130	129	oveq1d 6055	. . . . . . 7
131	36	a1i 11	. . . . . . . . . 10
132	131	fveq1d 5689	. . . . . . . . 9
133	132	eqcomd 2409	. . . . . . . 8
134	133	oveq1d 6055	. . . . . . 7
135	130, 134	oveq12d 6058	. . . . . 6
136	118, 124, 135	3eqtrd 2440	. . . . 5
137	52, 136	oveq12d 6058	. . . 4
138	137	oveq1d 6055	. . 3
139	138	mpteq2ia 4251	. 2
140	42, 2	nn0mulcld 10235	. . . . . . . 8
141	7, 140	expcld 11478	. . . . . . 7
142	50, 45	eqeltrd 2478	. . . . . . 7
143	141, 142	mulcomd 9065	. . . . . 6
144	143	oveq1d 6055	. . . . 5
145	144	oveq1d 6055	. . . 4
146	128, 125	eqeltrd 2478	. . . . . . . 8
147	146	sqcld 11476	. . . . . . 7
148	131, 120	eqtrd 2436	. . . . . . . . . 10
149	148, 113, 106, 64	fvmptd 5769	. . . . . . . . 9
150	149, 64	eqeltrd 2478	. . . . . . . 8
151	150	sqcld 11476	. . . . . . 7
152		nnne0 9988	. . . . . . . . . . . 12
153	55, 56, 152	3syl 19	. . . . . . . . . . 11
154	58, 64, 153, 76	divne0d 9762	. . . . . . . . . 10
155	108, 154	eqnetrd 2585	. . . . . . . . 9
156	128, 155	eqnetrd 2585	. . . . . . . 8
157	146, 156, 73	expne0d 11484	. . . . . . 7
158	149, 76	eqnetrd 2585	. . . . . . . 8
159	150, 158, 73	expne0d 11484	. . . . . . 7
160	142, 147, 141, 151, 157, 159	divmuldivd 9787	. . . . . 6
161	160	eqcomd 2409	. . . . 5
162	161	oveq1d 6055	. . . 4
163	34, 31	eqeltrd 2478	. . . . . . . . 9
164	163, 42	expcld 11478	. . . . . . . 8
165	39, 46	eqeltrd 2478	. . . . . . . 8
166	164, 165, 147, 157	div23d 9783	. . . . . . 7
167	166	oveq1d 6055	. . . . . 6
168	167	oveq1d 6055	. . . . 5
169	164, 147, 157	divcld 9746	. . . . . . 7
170	141, 151, 159	divcld 9746	. . . . . . 7
171	169, 165, 170	mulassd 9067	. . . . . 6
172	171	oveq1d 6055	. . . . 5
173	165, 170	mulcld 9064	. . . . . . 7
174		ax-1cn 9004	. . . . . . . . 9
175	174	a1i 11	. . . . . . . 8
176	9, 175	addcld 9063	. . . . . . 7
177		0re 9047	. . . . . . . . . 10
178	177	a1i 11	. . . . . . . . 9
179	106	nnred 9971	. . . . . . . . 9
180		2re 10025	. . . . . . . . . . . 12
181	180	a1i 11	. . . . . . . . . . 11
182		nnre 9963	. . . . . . . . . . 11
183	181, 182	remulcld 9072	. . . . . . . . . 10
184		1re 9046	. . . . . . . . . . 11
185	184	a1i 11	. . . . . . . . . 10
186	183, 185	readdcld 9071	. . . . . . . . 9
187	106	nngt0d 9999	. . . . . . . . 9
188	179	ltp1d 9897	. . . . . . . . 9
189	178, 179, 186, 187, 188	lttrd 9187	. . . . . . . 8
190	189	gt0ne0d 9547	. . . . . . 7
191	169, 173, 176, 190	divassd 9781	. . . . . 6
192	165, 141, 151, 159	div12d 9782	. . . . . . . . . 10
193	10, 18, 42	mulexpd 11493	. . . . . . . . . . . . 13
194	61, 63	sqmuld 11490	. . . . . . . . . . . . 13
195	193, 194	oveq12d 6058	. . . . . . . . . . . 12
196	149	oveq1d 6055	. . . . . . . . . . . . 13
197	39, 196	oveq12d 6058	. . . . . . . . . . . 12
198	10, 42	expcld 11478	. . . . . . . . . . . . 13
199	61	sqcld 11476	. . . . . . . . . . . . 13
200	18, 42	expcld 11478	. . . . . . . . . . . . 13
201	63	sqcld 11476	. . . . . . . . . . . . 13
202	61, 68, 73	expne0d 11484	. . . . . . . . . . . . 13
203	63, 75, 73	expne0d 11484	. . . . . . . . . . . . 13
204	198, 199, 200, 201, 202, 203	divmuldivd 9787	. . . . . . . . . . . 12
205	195, 197, 204	3eqtr4d 2446	. . . . . . . . . . 11
206	205	oveq2d 6056	. . . . . . . . . 10
207	66	rprege0d 10611	. . . . . . . . . . . . . . . 16 $/\$
208		resqrth 12016	. . . . . . . . . . . . . . . 16 $/\$
209	207, 208	syl 16	. . . . . . . . . . . . . . 15
210	209	oveq2d 6056	. . . . . . . . . . . . . 14
211		2t2e4 10083	. . . . . . . . . . . . . . . . . . 19
212	211	eqcomi 2408	. . . . . . . . . . . . . . . . . 18
213	212	a1i 11	. . . . . . . . . . . . . . . . 17
214	213	oveq2d 6056	. . . . . . . . . . . . . . . 16
215	10, 54, 54	expmuld 11481	. . . . . . . . . . . . . . . 16
216	23	rprege0d 10611	. . . . . . . . . . . . . . . . . 18 $/\$
217		resqrth 12016	. . . . . . . . . . . . . . . . . 18 $/\$
218	216, 217	syl 16	. . . . . . . . . . . . . . . . 17
219	218	oveq1d 6055	. . . . . . . . . . . . . . . 16
220	214, 215, 219	3eqtrd 2440	. . . . . . . . . . . . . . 15
221	7, 7, 8	mulassd 9067	. . . . . . . . . . . . . . . 16
222	211	a1i 11	. . . . . . . . . . . . . . . . 17
223	222	oveq1d 6055	. . . . . . . . . . . . . . . 16
224	221, 223	eqtr3d 2438	. . . . . . . . . . . . . . 15
225	220, 224	oveq12d 6058	. . . . . . . . . . . . . 14
226	7, 8	sqmuld 11490	. . . . . . . . . . . . . . . . 17
227		sq2 11432	. . . . . . . . . . . . . . . . . . 19
228	227	a1i 11	. . . . . . . . . . . . . . . . . 18
229	228	oveq1d 6055	. . . . . . . . . . . . . . . . 17
230	226, 229	eqtrd 2436	. . . . . . . . . . . . . . . 16
231	230	oveq1d 6055	. . . . . . . . . . . . . . 15
232		4cn 10030	. . . . . . . . . . . . . . . . . . 19
233		4pos 10042	. . . . . . . . . . . . . . . . . . . 20
234	177, 233	gtneii 9141	. . . . . . . . . . . . . . . . . . 19
235	232, 234	dividi 9703	. . . . . . . . . . . . . . . . . 18
236	235	a1i 11	. . . . . . . . . . . . . . . . 17
237	8	sqvald 11475	. . . . . . . . . . . . . . . . . . 19
238	237	oveq1d 6055	. . . . . . . . . . . . . . . . . 18
239	8, 8, 26	divcan4d 9752	. . . . . . . . . . . . . . . . . 18
240	238, 239	eqtrd 2436	. . . . . . . . . . . . . . . . 17
241	236, 240	oveq12d 6058	. . . . . . . . . . . . . . . 16
242	42	nn0cnd 10232	. . . . . . . . . . . . . . . . 17
243	8	sqcld 11476	. . . . . . . . . . . . . . . . 17
244	234	a1i 11	. . . . . . . . . . . . . . . . 17
245	242, 242, 243, 8, 244, 26	divmuldivd 9787	. . . . . . . . . . . . . . . 16
246	8	mulid2d 9062	. . . . . . . . . . . . . . . 16
247	241, 245, 246	3eqtr3d 2444	. . . . . . . . . . . . . . 15
248	231, 247	eqtrd 2436	. . . . . . . . . . . . . 14
249	210, 225, 248	3eqtrd 2440	. . . . . . . . . . . . 13
250	8, 242	mulcomd 9065	. . . . . . . . . . . . . . . . 17
251	250	oveq2d 6056	. . . . . . . . . . . . . . . 16
252	17, 42, 2	expmuld 11481	. . . . . . . . . . . . . . . 16
253	8, 13, 16, 140	expdivd 11492	. . . . . . . . . . . . . . . 16
254	251, 252, 253	3eqtr3d 2444	. . . . . . . . . . . . . . 15
255	7, 8, 7	mul32d 9232	. . . . . . . . . . . . . . . . . 18
256	255, 223	eqtrd 2436	. . . . . . . . . . . . . . . . 17
257	256	oveq2d 6056	. . . . . . . . . . . . . . . 16
258	62, 54, 55	expmuld 11481	. . . . . . . . . . . . . . . 16
259	9, 13, 16, 140	expdivd 11492	. . . . . . . . . . . . . . . 16
260	257, 258, 259	3eqtr3d 2444	. . . . . . . . . . . . . . 15
261	254, 260	oveq12d 6058	. . . . . . . . . . . . . 14
262	254, 200	eqeltrrd 2479	. . . . . . . . . . . . . . 15
263	9, 140	expcld 11478	. . . . . . . . . . . . . . 15
264	13, 140	expcld 11478	. . . . . . . . . . . . . . 15
265	47, 28	zmulcld 10337	. . . . . . . . . . . . . . . 16
266	9, 70, 265	expne0d 11484	. . . . . . . . . . . . . . 15
267	13, 16, 265	expne0d 11484	. . . . . . . . . . . . . . 15
268	262, 263, 264, 266, 267	divdiv2d 9778	. . . . . . . . . . . . . 14
269	8, 140	expcld 11478	. . . . . . . . . . . . . . . . 17
270	269, 264, 267	divcan1d 9747	. . . . . . . . . . . . . . . 16
271	270	oveq1d 6055	. . . . . . . . . . . . . . 15
272	7, 8, 140	mulexpd 11493	. . . . . . . . . . . . . . . 16
273	272	oveq2d 6056	. . . . . . . . . . . . . . 15
274	141, 269	mulcomd 9065	. . . . . . . . . . . . . . . . 17
275	274	oveq2d 6056	. . . . . . . . . . . . . . . 16
276	8, 26, 265	expne0d 11484	. . . . . . . . . . . . . . . . 17
277	7, 69, 265	expne0d 11484	. . . . . . . . . . . . . . . . 17
278	269, 269, 141, 276, 277	divdiv1d 9777	. . . . . . . . . . . . . . . 16
279	269, 276	dividd 9744	. . . . . . . . . . . . . . . . 17
280	279	oveq1d 6055	. . . . . . . . . . . . . . . 16
281	275, 278, 280	3eqtr2d 2442	. . . . . . . . . . . . . . 15
282	271, 273, 281	3eqtrd 2440	. . . . . . . . . . . . . 14
283	261, 268, 282	3eqtrd 2440	. . . . . . . . . . . . 13
284	249, 283	oveq12d 6058	. . . . . . . . . . . 12
285	284	oveq2d 6056	. . . . . . . . . . 11
286	141, 277	reccld 9739	. . . . . . . . . . . 12
287	141, 8, 286	mul12d 9231	. . . . . . . . . . 11
288	8	mulid1d 9061	. . . . . . . . . . . 12
289	141, 277	recidd 9741	. . . . . . . . . . . . 13
290	289	oveq2d 6056	. . . . . . . . . . . 12
291	288, 290, 240	3eqtr4d 2446	. . . . . . . . . . 11
292	285, 287, 291	3eqtrd 2440	. . . . . . . . . 10
293	192, 206, 292	3eqtrd 2440	. . . . . . . . 9
294	293	oveq1d 6055	. . . . . . . 8
295	243, 8, 176, 26, 190	divdiv1d 9777	. . . . . . . 8
296	294, 295	eqtrd 2436	. . . . . . 7
297	296	oveq2d 6056	. . . . . 6
298	191, 297	eqtrd 2436	. . . . 5
299	168, 172, 298	3eqtrd 2440	. . . 4
300	145, 162, 299	3eqtrd 2440	. . 3
301	300	mpteq2ia 4251	. 2
302	1, 139, 301	3eqtri 2428	1

Colors of variables: wff set class

Syntax hints: $/\$ wa 359

wceq 1649

wcel 1721

wne 2567 class class class wbr 4172

cmpt 4226

cfv 5413 (class class class)co 6040

cc 8944

cr 8945

cc0 8946

c1 8947

caddc 8949

cmul 8951

cle 9077

cdiv 9633

cn 9956

c2 10005

c4 10007

cn0 10177

cz 10238

crp 10568

cexp 11337

cfa 11521

csqr 11993

ceu 12620

This theorem is referenced by: stirlinglem15 27704

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-inf2 7552 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024 ax-addf 9025 ax-mulf 9026

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-se 4502 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 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-ov 6043 df-oprab 6044 df-mpt2 6045 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-oadd 6687 df-er 6864 df-pm 6980 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-sup 7404 df-oi 7435 df-card 7782 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-2 10014 df-3 10015 df-4 10016 df-n0 10178 df-z 10239 df-uz 10445 df-q 10531 df-rp 10569 df-ico 10878 df-fz 11000 df-fzo 11091 df-fl 11157 df-seq 11279 df-exp 11338 df-fac 11522 df-bc 11549 df-hash 11574 df-shft 11837 df-cj 11859 df-re 11860 df-im 11861 df-sqr 11995 df-abs 11996 df-limsup 12220 df-clim 12237 df-rlim 12238 df-sum 12435 df-ef 12625 df-e 12626

W3C validator