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

Theorem stirlinglem3 26973
 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.
StepHypRef Expression
1 stirlinglem3.4 . 2
2 id 19 . . . . . . . . . . . 12
3 nnnn0 10019 . . . . . . . . . . . . . 14
4 faccl 11345 . . . . . . . . . . . . . 14
5 nncn 9799 . . . . . . . . . . . . . 14
63, 4, 53syl 18 . . . . . . . . . . . . 13
7 2cn 9861 . . . . . . . . . . . . . . . . 17
87a1i 10 . . . . . . . . . . . . . . . 16
9 nncn 9799 . . . . . . . . . . . . . . . 16
108, 9mulcld 8900 . . . . . . . . . . . . . . 15
1110sqrcld 11966 . . . . . . . . . . . . . 14
12 ere 12417 . . . . . . . . . . . . . . . . . 18
1312recni 8894 . . . . . . . . . . . . . . . . 17
1413a1i 10 . . . . . . . . . . . . . . . 16
15 epos 12532 . . . . . . . . . . . . . . . . . 18
1612, 15gt0ne0ii 9354 . . . . . . . . . . . . . . . . 17
1716a1i 10 . . . . . . . . . . . . . . . 16
189, 14, 17divcld 9581 . . . . . . . . . . . . . . 15
1918, 3expcld 11292 . . . . . . . . . . . . . 14
2011, 19mulcld 8900 . . . . . . . . . . . . 13
21 0re 8883 . . . . . . . . . . . . . . . . 17
2221a1i 10 . . . . . . . . . . . . . . . 16
23 2rp 10406 . . . . . . . . . . . . . . . . . . 19
2423a1i 10 . . . . . . . . . . . . . . . . . 18
25 nnrp 10410 . . . . . . . . . . . . . . . . . 18
2624, 25rpmulcld 10453 . . . . . . . . . . . . . . . . 17
2726sqrgt0d 11942 . . . . . . . . . . . . . . . 16
2822, 27jca 518 . . . . . . . . . . . . . . 15
29 ltne 8962 . . . . . . . . . . . . . . 15
3028, 29syl 15 . . . . . . . . . . . . . 14
31 nnne0 9823 . . . . . . . . . . . . . . . 16
329, 14, 31, 17divne0d 9597 . . . . . . . . . . . . . . 15
33 nnz 10092 . . . . . . . . . . . . . . 15
3418, 32, 33expne0d 11298 . . . . . . . . . . . . . 14
3511, 19, 30, 34mulne0d 9465 . . . . . . . . . . . . 13
366, 20, 35divcld 9581 . . . . . . . . . . . 12
372, 36jca 518 . . . . . . . . . . 11
38 stirlinglem3.1 . . . . . . . . . . . 12
3938fvmpt2 5646 . . . . . . . . . . 11
4037, 39syl 15 . . . . . . . . . 10
4140oveq1d 5915 . . . . . . . . 9
422, 20jca 518 . . . . . . . . . . 11
43 stirlinglem3.3 . . . . . . . . . . . 12
4443fvmpt2 5646 . . . . . . . . . . 11
4542, 44syl 15 . . . . . . . . . 10
4645oveq1d 5915 . . . . . . . . 9
4741, 46oveq12d 5918 . . . . . . . 8
48 4nn0 10031 . . . . . . . . . . 11
4948a1i 10 . . . . . . . . . 10
506, 20, 35, 49expdivd 11306 . . . . . . . . 9
5150oveq1d 5915 . . . . . . . 8
526, 49expcld 11292 . . . . . . . . 9
5320, 49expcld 11292 . . . . . . . . 9
5449nn0zd 10162 . . . . . . . . . 10
5520, 35, 54expne0d 11298 . . . . . . . . 9
5652, 53, 55divcan1d 9582 . . . . . . . 8
5747, 51, 563eqtrd 2352 . . . . . . 7
5857eqcomd 2321 . . . . . 6
5958oveq2d 5916 . . . . 5
60 2nn0 10029 . . . . . . . . . . . . . 14
6160a1i 10 . . . . . . . . . . . . 13
6261, 3nn0mulcld 10070 . . . . . . . . . . . 12
63 faccl 11345 . . . . . . . . . . . 12
64 nncn 9799 . . . . . . . . . . . 12
6562, 63, 643syl 18 . . . . . . . . . . 11
6665sqcld 11290 . . . . . . . . . 10
678, 10mulcld 8900 . . . . . . . . . . . . 13
6867sqrcld 11966 . . . . . . . . . . . 12
6910, 14, 17divcld 9581 . . . . . . . . . . . . 13
7069, 62expcld 11292 . . . . . . . . . . . 12
7168, 70mulcld 8900 . . . . . . . . . . 11
7271sqcld 11290 . . . . . . . . . 10
7324, 26rpmulcld 10453 . . . . . . . . . . . . . . 15
7473sqrgt0d 11942 . . . . . . . . . . . . . 14
7522, 74jca 518 . . . . . . . . . . . . 13
76 ltne 8962 . . . . . . . . . . . . 13
7775, 76syl 15 . . . . . . . . . . . 12
7824rpne0d 10442 . . . . . . . . . . . . . . 15
798, 9, 78, 31mulne0d 9465 . . . . . . . . . . . . . 14
8010, 14, 79, 17divne0d 9597 . . . . . . . . . . . . 13
81 2z 10101 . . . . . . . . . . . . . . 15
8281a1i 10 . . . . . . . . . . . . . 14
8382, 33zmulcld 10170 . . . . . . . . . . . . 13
8469, 80, 83expne0d 11298 . . . . . . . . . . . 12
8568, 70, 77, 84mulne0d 9465 . . . . . . . . . . 11
8671, 85, 82expne0d 11298 . . . . . . . . . 10
8766, 72, 86divcan1d 9582 . . . . . . . . 9
8887eqcomd 2321 . . . . . . . 8
8965, 71, 85, 61expdivd 11306 . . . . . . . . . 10
9089eqcomd 2321 . . . . . . . . 9
9190oveq1d 5915 . . . . . . . 8
9288, 91eqtrd 2348 . . . . . . 7
93 nfcv 2452 . . . . . . . . . . . . . 14
94 nfcv 2452 . . . . . . . . . . . . . 14
95 fveq2 5563 . . . . . . . . . . . . . . 15
96 oveq2 5908 . . . . . . . . . . . . . . . . 17
9796fveq2d 5567 . . . . . . . . . . . . . . . 16
98 oveq1 5907 . . . . . . . . . . . . . . . . 17
99 id 19 . . . . . . . . . . . . . . . . 17
10098, 99oveq12d 5918 . . . . . . . . . . . . . . . 16
10197, 100oveq12d 5918 . . . . . . . . . . . . . . 15
10295, 101oveq12d 5918 . . . . . . . . . . . . . 14
10393, 94, 102cbvmpt 4147 . . . . . . . . . . . . 13
10438, 103eqtri 2336 . . . . . . . . . . . 12
105104a1i 10 . . . . . . . . . . 11
106 fveq2 5563 . . . . . . . . . . . . 13
107 oveq2 5908 . . . . . . . . . . . . . . 15
108107fveq2d 5567 . . . . . . . . . . . . . 14
109 oveq1 5907 . . . . . . . . . . . . . . 15
110 id 19 . . . . . . . . . . . . . . 15
111109, 110oveq12d 5918 . . . . . . . . . . . . . 14
112108, 111oveq12d 5918 . . . . . . . . . . . . 13
113106, 112oveq12d 5918 . . . . . . . . . . . 12
114113adantl 452 . . . . . . . . . . 11
115 2nn 9924 . . . . . . . . . . . . 13
116115a1i 10 . . . . . . . . . . . 12
117116, 2nnmulcld 9838 . . . . . . . . . . 11
11865, 71, 85divcld 9581 . . . . . . . . . . 11
119105, 114, 117, 118fvmptd 5644 . . . . . . . . . 10
120119oveq1d 5915 . . . . . . . . 9
121120eqcomd 2321 . . . . . . . 8
122121oveq1d 5915 . . . . . . 7
123 eqidd 2317 . . . . . . . . . . 11
124112adantl 452 . . . . . . . . . . 11
125123, 124, 117, 71fvmptd 5644 . . . . . . . . . 10
126125oveq1d 5915 . . . . . . . . 9
127126eqcomd 2321 . . . . . . . 8
128127oveq2d 5916 . . . . . . 7
12992, 122, 1283eqtrd 2352 . . . . . 6
130 nfcv 2452 . . . . . . . . . . . 12
131 nfcv 2452 . . . . . . . . . . . 12
132130, 131, 101cbvmpt 4147 . . . . . . . . . . 11
133132a1i 10 . . . . . . . . . 10
134133fveq1d 5565 . . . . . . . . 9
135134eqcomd 2321 . . . . . . . 8
136135oveq1d 5915 . . . . . . 7
137136oveq2d 5916 . . . . . 6
138119, 118eqeltrd 2390 . . . . . . . . . . 11
1392, 138jca 518 . . . . . . . . . 10
140 stirlinglem3.2 . . . . . . . . . . 11
141140fvmpt2 5646 . . . . . . . . . 10
142139, 141syl 15 . . . . . . . . 9
143142eqcomd 2321 . . . . . . . 8
144143oveq1d 5915 . . . . . . 7
14543a1i 10 . . . . . . . . . 10
146145fveq1d 5565 . . . . . . . . 9
147146eqcomd 2321 . . . . . . . 8
148147oveq1d 5915 . . . . . . 7
149144, 148oveq12d 5918 . . . . . 6
150129, 137, 1493eqtrd 2352 . . . . 5
15159, 150oveq12d 5918 . . . 4
152151oveq1d 5915 . . 3
153152mpteq2ia 4139 . 2
15449, 3nn0mulcld 10070 . . . . . . . 8
1558, 154expcld 11292 . . . . . . 7
15657, 52eqeltrd 2390 . . . . . . 7
157155, 156mulcomd 8901 . . . . . 6
158157oveq1d 5915 . . . . 5
159158oveq1d 5915 . . . 4
160142, 138eqeltrd 2390 . . . . . . . 8
161160sqcld 11290 . . . . . . 7
162145, 133eqtrd 2348 . . . . . . . . . 10
163162, 124, 117, 71fvmptd 5644 . . . . . . . . 9
164163, 71eqeltrd 2390 . . . . . . . 8
165164sqcld 11290 . . . . . . 7
16662, 63syl 15 . . . . . . . . . . . 12
167 nnne0 9823 . . . . . . . . . . . 12
168166, 167syl 15 . . . . . . . . . . 11
16965, 71, 168, 85divne0d 9597 . . . . . . . . . 10
170119, 169eqnetrd 2497 . . . . . . . . 9
171142, 170eqnetrd 2497 . . . . . . . 8
172160, 171, 82expne0d 11298 . . . . . . 7
173163, 85eqnetrd 2497 . . . . . . . 8
174164, 173, 82expne0d 11298 . . . . . . 7
175156, 161, 155, 165, 172, 174divmuldivd 9622 . . . . . 6
176175eqcomd 2321 . . . . 5
177176oveq1d 5915 . . . 4
17840, 36eqeltrd 2390 . . . . . . . . 9
179178, 49expcld 11292 . . . . . . . 8
18046, 53eqeltrd 2390 . . . . . . . 8
181179, 180, 161, 172div23d 9618 . . . . . . 7
182181oveq1d 5915 . . . . . 6
183182oveq1d 5915 . . . . 5
184179, 161, 172divcld 9581 . . . . . . 7
185155, 165, 174divcld 9581 . . . . . . 7
186184, 180, 185mulassd 8903 . . . . . 6
187186oveq1d 5915 . . . . 5
188180, 185mulcld 8900 . . . . . . 7
189 ax-1cn 8840 . . . . . . . . 9
190189a1i 10 . . . . . . . 8
19110, 190addcld 8899 . . . . . . 7
192117nnred 9806 . . . . . . . . . 10
193 2re 9860 . . . . . . . . . . . . 13
194193a1i 10 . . . . . . . . . . . 12
195 nnre 9798 . . . . . . . . . . . 12
196194, 195remulcld 8908 . . . . . . . . . . 11
197 1re 8882 . . . . . . . . . . . 12
198197a1i 10 . . . . . . . . . . 11
199196, 198readdcld 8907 . . . . . . . . . 10
200117nngt0d 9834 . . . . . . . . . 10
201192ltp1d 9732 . . . . . . . . . 10
20222, 192, 199, 200, 201lttrd 9022 . . . . . . . . 9
20322, 202jca 518 . . . . . . . 8
204 ltne 8962 . . . . . . . 8
205203, 204syl 15 . . . . . . 7
206184, 188, 191, 205divassd 9616 . . . . . 6
207180, 155, 165, 174div12d 9617 . . . . . . . . . 10
208163oveq1d 5915 . . . . . . . . . . . . 13
20946, 208oveq12d 5918 . . . . . . . . . . . 12
21011, 19, 49mulexpd 11307 . . . . . . . . . . . . 13
21168, 70, 61mulexpd 11307 . . . . . . . . . . . . 13
212210, 211oveq12d 5918 . . . . . . . . . . . 12
21311, 49expcld 11292 . . . . . . . . . . . . . 14
21468sqcld 11290 . . . . . . . . . . . . . 14
21519, 49expcld 11292 . . . . . . . . . . . . . 14
21670sqcld 11290 . . . . . . . . . . . . . 14
21768, 77, 82expne0d 11298 . . . . . . . . . . . . . 14
21870, 84, 82expne0d 11298 . . . . . . . . . . . . . 14
219213, 214, 215, 216, 217, 218divmuldivd 9622 . . . . . . . . . . . . 13
220219eqcomd 2321 . . . . . . . . . . . 12
221209, 212, 2203eqtrd 2352 . . . . . . . . . . 11
222221oveq2d 5916 . . . . . . . . . 10
22373rprege0d 10444 . . . . . . . . . . . . . . . 16
224 resqrth 11788 . . . . . . . . . . . . . . . 16
225223, 224syl 15 . . . . . . . . . . . . . . 15
226225oveq2d 5916 . . . . . . . . . . . . . 14
227 eqid 2316 . . . . . . . . . . . . . . . . . . . 20
228 2t2e4 9918 . . . . . . . . . . . . . . . . . . . 20
229227, 228eqtr4i 2339 . . . . . . . . . . . . . . . . . . 19
230229a1i 10 . . . . . . . . . . . . . . . . . 18
231230oveq2d 5916 . . . . . . . . . . . . . . . . 17
23211, 61, 613jca 1132 . . . . . . . . . . . . . . . . . 18
233 expmul 11194 . . . . . . . . . . . . . . . . . 18
234232, 233syl 15 . . . . . . . . . . . . . . . . 17
235231, 234eqtrd 2348 . . . . . . . . . . . . . . . 16
23626rprege0d 10444 . . . . . . . . . . . . . . . . . 18
237 resqrth 11788 . . . . . . . . . . . . . . . . . 18
238236, 237syl 15 . . . . . . . . . . . . . . . . 17
239238oveq1d 5915 . . . . . . . . . . . . . . . 16
240235, 239eqtrd 2348 . . . . . . . . . . . . . . 15
2418, 8, 9mulassd 8903 . . . . . . . . . . . . . . . . 17
242241eqcomd 2321 . . . . . . . . . . . . . . . 16
243228a1i 10 . . . . . . . . . . . . . . . . 17
244243oveq1d 5915 . . . . . . . . . . . . . . . 16
245242, 244eqtrd 2348 . . . . . . . . . . . . . . 15
246240, 245oveq12d 5918 . . . . . . . . . . . . . 14
2478, 9, 61mulexpd 11307 . . . . . . . . . . . . . . . . 17
248 sq2 11246 . . . . . . . . . . . . . . . . . . 19
249248a1i 10 . . . . . . . . . . . . . . . . . 18
250249oveq1d 5915 . . . . . . . . . . . . . . . . 17
251247, 250eqtrd 2348 . . . . . . . . . . . . . . . 16
252251oveq1d 5915 . . . . . . . . . . . . . . 15
25349nn0cnd 10067 . . . . . . . . . . . . . . . . . 18
2549sqcld 11290 . . . . . . . . . . . . . . . . . 18
255 4pos 9877 . . . . . . . . . . . . . . . . . . . . 21
25621, 255pm3.2i 441 . . . . . . . . . . . . . . . . . . . 20
257 ltne 8962 . . . . . . . . . . . . . . . . . . . 20
258256, 257ax-mp 8 . . . . . . . . . . . . . . . . . . 19
259258a1i 10 . . . . . . . . . . . . . . . . . 18
260253, 253, 254, 9, 259, 31divmuldivd 9622 . . . . . . . . . . . . . . . . 17
261260eqcomd 2321 . . . . . . . . . . . . . . . 16
262 4cn 9865 . . . . . . . . . . . . . . . . . . 19
263262, 258dividi 9538 . . . . . . . . . . . . . . . . . 18
264263a1i 10 . . . . . . . . . . . . . . . . 17
2659sqvald 11289 . . . . . . . . . . . . . . . . . . 19
266265oveq1d 5915 . . . . . . . . . . . . . . . . . 18
2679, 9, 31divcan4d 9587 . . . . . . . . . . . . . . . . . 18
268266, 267eqtrd 2348 . . . . . . . . . . . . . . . . 17
269264, 268oveq12d 5918 . . . . . . . . . . . . . . . 16
2709mulid2d 8898 . . . . . . . . . . . . . . . 16
271261, 269, 2703eqtrd 2352 . . . . . . . . . . . . . . 15
272252, 271eqtrd 2348 . . . . . . . . . . . . . 14
273226, 246, 2723eqtrd 2352 . . . . . . . . . . . . 13
27418, 49, 3expmuld 11295 . . . . . . . . . . . . . . . . 17
275274eqcomd 2321 . . . . . . . . . . . . . . . 16
2769, 253mulcomd 8901 . . . . . . . . . . . . . . . . 17
277276oveq2d 5916 . . . . . . . . . . . . . . . 16
2789, 14, 17, 154expdivd 11306 . . . . . . . . . . . . . . . 16
279275, 277, 2783eqtrd 2352 . . . . . . . . . . . . . . 15
28069, 61, 62expmuld 11295 . . . . . . . . . . . . . . . . 17
281280eqcomd 2321 . . . . . . . . . . . . . . . 16
2828, 9, 8mul32d 9067 . . . . . . . . . . . . . . . . . 18
283282, 244eqtrd 2348 . . . . . . . . . . . . . . . . 17
284283oveq2d 5916 . . . . . . . . . . . . . . . 16
28510, 14, 17, 154expdivd 11306 . . . . . . . . . . . . . . . 16
286281, 284, 2853eqtrd 2352 . . . . . . . . . . . . . . 15
287279, 286oveq12d 5918 . . . . . . . . . . . . . 14
288279, 215eqeltrrd 2391 . . . . . . . . . . . . . . 15
28910, 154expcld 11292 . . . . . . . . . . . . . . 15
29014, 154expcld 11292 . . . . . . . . . . . . . . 15
29154, 33zmulcld 10170 . . . . . . . . . . . . . . . 16
29210, 79, 291expne0d 11298 . . . . . . . . . . . . . . 15
29314, 17, 291expne0d 11298 . . . . . . . . . . . . . . 15
294288, 289, 290, 292, 293divdiv2d 9613 . . . . . . . . . . . . . 14
2959, 154expcld 11292 . . . . . . . . . . . . . . . . 17
296295, 290, 293divcan1d 9582 . . . . . . . . . . . . . . . 16
297296oveq1d 5915 . . . . . . . . . . . . . . 15
2988, 9, 154mulexpd 11307 . . . . . . . . . . . . . . . 16
299298oveq2d 5916 . . . . . . . . . . . . . . 15
300155, 295mulcomd 8901 . . . . . . . . . . . . . . . . 17
301300oveq2d 5916 . . . . . . . . . . . . . . . 16
3029, 31, 291expne0d 11298 . . . . . . . . . . . . . . . . . 18
3038, 78, 291expne0d 11298 . . . . . . . . . . . . . . . . . 18
304295, 295, 155, 302, 303divdiv1d 9612 . . . . . . . . . . . . . . . . 17
305304eqcomd 2321 . . . . . . . . . . . . . . . 16
306295, 302dividd 9579 . . . . . . . . . . . . . . . . 17
307306oveq1d 5915 . . . . . . . . . . . . . . . 16
308301, 305, 3073eqtrd 2352 . . . . . . . . . . . . . . 15
309297, 299, 3083eqtrd 2352 . . . . . . . . . . . . . 14
310287, 294, 3093eqtrd 2352 . . . . . . . . . . . . 13
311273, 310oveq12d 5918 . . . . . . . . . . . 12
312311oveq2d 5916 . . . . . . . . . . 11
313155, 303reccld 9574 . . . . . . . . . . . 12
314155, 9, 313mul12d 9066 . . . . . . . . . . 11
315155, 303recidd 9576 . . . . . . . . . . . . 13
316315oveq2d 5916 . . . . . . . . . . . 12
3179mulid1d 8897 . . . . . . . . . . . 12
318268eqcomd 2321 . . . . . . . . . . . 12
319316, 317, 3183eqtrd 2352 . . . . . . . . . . 11
320312, 314, 3193eqtrd 2352 . . . . . . . . . 10
321207, 222, 3203eqtrd 2352 . . . . . . . . 9
322321oveq1d 5915 . . . . . . . 8
323254, 9, 191, 31, 205divdiv1d 9612 . . . . . . . 8
324322, 323eqtrd 2348 . . . . . . 7
325324oveq2d 5916 . . . . . 6
326206, 325eqtrd 2348 . . . . 5
327183, 187, 3263eqtrd 2352 . . . 4
328159, 177, 3273eqtrd 2352 . . 3
329328mpteq2ia 4139 . 2
3301, 153, 3293eqtri 2340 1
 Colors of variables: wff set class Syntax hints:   wa 358   w3a 934   wceq 1633   wcel 1701   wne 2479   class class class wbr 4060   cmpt 4114  cfv 5292  (class class class)co 5900  cc 8780  cr 8781  cc0 8782  c1 8783   caddc 8785   cmul 8787   clt 8912   cle 8913   cdiv 9468  cn 9791  c2 9840  c4 9842  cn0 10012  cz 10071  crp 10401  cexp 11151  cfa 11335  csqr 11765  ceu 12391 This theorem is referenced by:  stirlinglem15  26985 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-rep 4168  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251  ax-un 4549  ax-inf2 7387  ax-cnex 8838  ax-resscn 8839  ax-1cn 8840  ax-icn 8841  ax-addcl 8842  ax-addrcl 8843  ax-mulcl 8844  ax-mulrcl 8845  ax-mulcom 8846  ax-addass 8847  ax-mulass 8848  ax-distr 8849  ax-i2m1 8850  ax-1ne0 8851  ax-1rid 8852  ax-rnegex 8853  ax-rrecex 8854  ax-cnre 8855  ax-pre-lttri 8856  ax-pre-lttrn 8857  ax-pre-ltadd 8858  ax-pre-mulgt0 8859  ax-pre-sup 8860  ax-addf 8861  ax-mulf 8862 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-nel 2482  df-ral 2582  df-rex 2583  df-reu 2584  df-rmo 2585  df-rab 2586  df-v 2824  df-sbc 3026  df-csb 3116  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-pss 3202  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-tp 3682  df-op 3683  df-uni 3865  df-int 3900  df-iun 3944  df-br 4061  df-opab 4115  df-mpt 4116  df-tr 4151  df-eprel 4342  df-id 4346  df-po 4351  df-so 4352  df-fr 4389  df-se 4390  df-we 4391  df-ord 4432  df-on 4433  df-lim 4434  df-suc 4435  df-om 4694  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-f1 5297  df-fo 5298  df-f1o 5299  df-fv 5300  df-isom 5301  df-ov 5903  df-oprab 5904  df-mpt2 5905  df-1st 6164  df-2nd 6165  df-riota 6346  df-recs 6430  df-rdg 6465  df-1o 6521  df-oadd 6525  df-er 6702  df-pm 6818  df-en 6907  df-dom 6908  df-sdom 6909  df-fin 6910  df-sup 7239  df-oi 7270  df-card 7617  df-pnf 8914  df-mnf 8915  df-xr 8916  df-ltxr 8917  df-le 8918  df-sub 9084  df-neg 9085  df-div 9469  df-nn 9792  df-2 9849  df-3 9850  df-4 9851  df-n0 10013  df-z 10072  df-uz 10278  df-q 10364  df-rp 10402  df-ico 10709  df-fz 10830  df-fzo 10918  df-fl 10972  df-seq 11094  df-exp 11152  df-fac 11336  df-bc 11363  df-hash 11385  df-shft 11609  df-cj 11631  df-re 11632  df-im 11633  df-sqr 11767  df-abs 11768  df-limsup 11992  df-clim 12009  df-rlim 12010  df-sum 12206  df-ef 12396  df-e 12397
 Copyright terms: Public domain W3C validator