Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ply1divex Structured version   Unicode version

Theorem ply1divex 20059
 Description: Lemma for ply1divalg 20060: existence part. (Contributed by Stefan O'Rear, 27-Mar-2015.)
Hypotheses
Ref Expression
ply1divalg.p Poly1
ply1divalg.d deg1
ply1divalg.b
ply1divalg.m
ply1divalg.z
ply1divalg.t
ply1divalg.r1
ply1divalg.f
ply1divalg.g1
ply1divalg.g2
ply1divex.o
ply1divex.k
ply1divex.u
ply1divex.i
ply1divex.g3 coe1
Assertion
Ref Expression
ply1divex
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem ply1divex
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 5728 . . . . 5
21breq1d 4222 . . . 4
32rexbidv 2726 . . 3
4 nnssnn0 10224 . . . . 5
5 ply1divalg.r1 . . . . . . . . . 10
65adantr 452 . . . . . . . . 9
7 ply1divalg.f . . . . . . . . . 10
87adantr 452 . . . . . . . . 9
9 simpr 448 . . . . . . . . 9
10 ply1divalg.d . . . . . . . . . 10 deg1
11 ply1divalg.p . . . . . . . . . 10 Poly1
12 ply1divalg.z . . . . . . . . . 10
13 ply1divalg.b . . . . . . . . . 10
1410, 11, 12, 13deg1nn0cl 20011 . . . . . . . . 9
156, 8, 9, 14syl3anc 1184 . . . . . . . 8
1615nn0red 10275 . . . . . . 7
17 ply1divalg.g1 . . . . . . . . . 10
18 ply1divalg.g2 . . . . . . . . . 10
1910, 11, 12, 13deg1nn0cl 20011 . . . . . . . . . 10
205, 17, 18, 19syl3anc 1184 . . . . . . . . 9
2120nn0red 10275 . . . . . . . 8
2221adantr 452 . . . . . . 7
2316, 22resubcld 9465 . . . . . 6
24 arch 10218 . . . . . 6
2523, 24syl 16 . . . . 5
26 ssrexv 3408 . . . . 5
274, 25, 26mpsyl 61 . . . 4
2816adantr 452 . . . . . . 7
2921ad2antrr 707 . . . . . . 7
30 nn0re 10230 . . . . . . . 8
3130adantl 453 . . . . . . 7
3228, 29, 31ltsubadd2d 9624 . . . . . 6
3332biimpd 199 . . . . 5
3433reximdva 2818 . . . 4
3527, 34mpd 15 . . 3
36 0nn0 10236 . . . 4
3710, 11, 12deg1z 20010 . . . . . 6
385, 37syl 16 . . . . 5
39 0re 9091 . . . . . . 7
40 readdcl 9073 . . . . . . 7
4121, 39, 40sylancl 644 . . . . . 6
42 mnflt 10722 . . . . . 6
4341, 42syl 16 . . . . 5
4438, 43eqbrtrd 4232 . . . 4
45 oveq2 6089 . . . . . 6
4645breq2d 4224 . . . . 5
4746rspcev 3052 . . . 4
4836, 44, 47sylancr 645 . . 3
493, 35, 48pm2.61ne 2679 . 2
507adantr 452 . . . 4
51 oveq2 6089 . . . . . . . . . 10
5251breq2d 4224 . . . . . . . . 9
5352imbi1d 309 . . . . . . . 8
5453ralbidv 2725 . . . . . . 7
5554imbi2d 308 . . . . . 6
56 oveq2 6089 . . . . . . . . . 10
5756breq2d 4224 . . . . . . . . 9
5857imbi1d 309 . . . . . . . 8
5958ralbidv 2725 . . . . . . 7
6059imbi2d 308 . . . . . 6
61 oveq2 6089 . . . . . . . . . 10
6261breq2d 4224 . . . . . . . . 9
6362imbi1d 309 . . . . . . . 8
6463ralbidv 2725 . . . . . . 7
6564imbi2d 308 . . . . . 6
6611ply1rng 16642 . . . . . . . . . . . 12
675, 66syl 16 . . . . . . . . . . 11
6813, 12rng0cl 15685 . . . . . . . . . . 11
6967, 68syl 16 . . . . . . . . . 10
7069ad2antrr 707 . . . . . . . . 9
71 ply1divalg.t . . . . . . . . . . . . . . . . 17
7213, 71, 12rngrz 15701 . . . . . . . . . . . . . . . 16
7367, 17, 72syl2anc 643 . . . . . . . . . . . . . . 15
7473oveq2d 6097 . . . . . . . . . . . . . 14
7574adantr 452 . . . . . . . . . . . . 13
76 rnggrp 15669 . . . . . . . . . . . . . . 15
7767, 76syl 16 . . . . . . . . . . . . . 14
78 ply1divalg.m . . . . . . . . . . . . . . 15
7913, 12, 78grpsubid1 14874 . . . . . . . . . . . . . 14
8077, 79sylan 458 . . . . . . . . . . . . 13
8175, 80eqtr2d 2469 . . . . . . . . . . . 12
8281fveq2d 5732 . . . . . . . . . . 11
8320nn0cnd 10276 . . . . . . . . . . . . 13
8483addid1d 9266 . . . . . . . . . . . 12
8584adantr 452 . . . . . . . . . . 11
8682, 85breq12d 4225 . . . . . . . . . 10
8786biimpa 471 . . . . . . . . 9
88 oveq2 6089 . . . . . . . . . . . . 13
8988oveq2d 6097 . . . . . . . . . . . 12
9089fveq2d 5732 . . . . . . . . . . 11
9190breq1d 4222 . . . . . . . . . 10
9291rspcev 3052 . . . . . . . . 9
9370, 87, 92syl2anc 643 . . . . . . . 8
9493ex 424 . . . . . . 7
9594ralrimiva 2789 . . . . . 6
96 nn0addcl 10255 . . . . . . . . . . . . . . . . . 18
9720, 96sylan 458 . . . . . . . . . . . . . . . . 17
9897adantr 452 . . . . . . . . . . . . . . . 16
995ad2antrr 707 . . . . . . . . . . . . . . . 16
100 simprl 733 . . . . . . . . . . . . . . . 16
10110, 11, 13deg1cl 20006 . . . . . . . . . . . . . . . . . . . . 21
102101adantl 453 . . . . . . . . . . . . . . . . . . . 20
10320ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . 22
104 peano2nn0 10260 . . . . . . . . . . . . . . . . . . . . . . 23
105104ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . 22
106103, 105nn0addcld 10278 . . . . . . . . . . . . . . . . . . . . 21
107106nn0zd 10373 . . . . . . . . . . . . . . . . . . . 20
108 degltlem1 19995 . . . . . . . . . . . . . . . . . . . 20
109102, 107, 108syl2anc 643 . . . . . . . . . . . . . . . . . . 19
110109biimpd 199 . . . . . . . . . . . . . . . . . 18
111110impr 603 . . . . . . . . . . . . . . . . 17
11220adantr 452 . . . . . . . . . . . . . . . . . . . . 21
113112nn0cnd 10276 . . . . . . . . . . . . . . . . . . . 20
114 nn0cn 10231 . . . . . . . . . . . . . . . . . . . . . 22
115114adantl 453 . . . . . . . . . . . . . . . . . . . . 21
116 peano2cn 9238 . . . . . . . . . . . . . . . . . . . . 21
117115, 116syl 16 . . . . . . . . . . . . . . . . . . . 20
118 ax-1cn 9048 . . . . . . . . . . . . . . . . . . . . 21
119118a1i 11 . . . . . . . . . . . . . . . . . . . 20
120113, 117, 119addsubassd 9431 . . . . . . . . . . . . . . . . . . 19
121 pncan 9311 . . . . . . . . . . . . . . . . . . . . 21
122115, 118, 121sylancl 644 . . . . . . . . . . . . . . . . . . . 20
123122oveq2d 6097 . . . . . . . . . . . . . . . . . . 19
124120, 123eqtrd 2468 . . . . . . . . . . . . . . . . . 18
125124adantr 452 . . . . . . . . . . . . . . . . 17
126111, 125breqtrd 4236 . . . . . . . . . . . . . . . 16
12767ad2antrr 707 . . . . . . . . . . . . . . . . . 18
12817ad2antrr 707 . . . . . . . . . . . . . . . . . 18
1295ad2antrr 707 . . . . . . . . . . . . . . . . . . 19
130 ply1divex.i . . . . . . . . . . . . . . . . . . . . 21
131130ad2antrr 707 . . . . . . . . . . . . . . . . . . . 20
132 eqid 2436 . . . . . . . . . . . . . . . . . . . . . . 23 coe1 coe1
133 ply1divex.k . . . . . . . . . . . . . . . . . . . . . . 23
134132, 13, 11, 133coe1f 16609 . . . . . . . . . . . . . . . . . . . . . 22 coe1
135134adantl 453 . . . . . . . . . . . . . . . . . . . . 21 coe1
136 simplr 732 . . . . . . . . . . . . . . . . . . . . . 22
137103, 136nn0addcld 10278 . . . . . . . . . . . . . . . . . . . . 21
138135, 137ffvelrnd 5871 . . . . . . . . . . . . . . . . . . . 20 coe1
139 ply1divex.u . . . . . . . . . . . . . . . . . . . . 21
140133, 139rngcl 15677 . . . . . . . . . . . . . . . . . . . 20 coe1 coe1
141129, 131, 138, 140syl3anc 1184 . . . . . . . . . . . . . . . . . . 19 coe1
142 eqid 2436 . . . . . . . . . . . . . . . . . . . 20 var1 var1
143 eqid 2436 . . . . . . . . . . . . . . . . . . . 20
144 eqid 2436 . . . . . . . . . . . . . . . . . . . 20 mulGrp mulGrp
145 eqid 2436 . . . . . . . . . . . . . . . . . . . 20 .gmulGrp .gmulGrp
146133, 11, 142, 143, 144, 145, 13ply1tmcl 16664 . . . . . . . . . . . . . . . . . . 19 coe1 coe1 .gmulGrpvar1
147129, 141, 136, 146syl3anc 1184 . . . . . . . . . . . . . . . . . 18 coe1 .gmulGrpvar1
14813, 71rngcl 15677 . . . . . . . . . . . . . . . . . 18 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
149127, 128, 147, 148syl3anc 1184 . . . . . . . . . . . . . . . . 17 coe1 .gmulGrpvar1
150149adantrr 698 . . . . . . . . . . . . . . . 16 coe1 .gmulGrpvar1
151103nn0red 10275 . . . . . . . . . . . . . . . . . . 19
152151leidd 9593 . . . . . . . . . . . . . . . . . 18
15310, 133, 11, 142, 143, 144, 145deg1tmle 20040 . . . . . . . . . . . . . . . . . . 19 coe1 coe1 .gmulGrpvar1
154129, 141, 136, 153syl3anc 1184 . . . . . . . . . . . . . . . . . 18 coe1 .gmulGrpvar1
15511, 10, 129, 13, 71, 128, 147, 103, 136, 152, 154deg1mulle2 20032 . . . . . . . . . . . . . . . . 17 coe1 .gmulGrpvar1
156155adantrr 698 . . . . . . . . . . . . . . . 16 coe1 .gmulGrpvar1
157 eqid 2436 . . . . . . . . . . . . . . . 16 coe1 coe1 .gmulGrpvar1 coe1 coe1 .gmulGrpvar1
158 eqid 2436 . . . . . . . . . . . . . . . . . . 19
159158, 133, 11, 142, 143, 144, 145, 13, 71, 139, 128, 129, 141, 136, 103coe1tmmul2fv 16670 . . . . . . . . . . . . . . . . . 18 coe1 coe1 .gmulGrpvar1 coe1 coe1
160103nn0cnd 10276 . . . . . . . . . . . . . . . . . . . 20
161114ad2antlr 708 . . . . . . . . . . . . . . . . . . . 20
162160, 161addcomd 9268 . . . . . . . . . . . . . . . . . . 19
163162fveq2d 5732 . . . . . . . . . . . . . . . . . 18 coe1 coe1 .gmulGrpvar1 coe1 coe1 .gmulGrpvar1
164 ply1divex.g3 . . . . . . . . . . . . . . . . . . . . 21 coe1
165164oveq1d 6096 . . . . . . . . . . . . . . . . . . . 20 coe1 coe1 coe1
166165ad2antrr 707 . . . . . . . . . . . . . . . . . . 19 coe1 coe1 coe1
167 eqid 2436 . . . . . . . . . . . . . . . . . . . . . . . 24 coe1 coe1
168167, 13, 11, 133coe1f 16609 . . . . . . . . . . . . . . . . . . . . . . 23 coe1
16917, 168syl 16 . . . . . . . . . . . . . . . . . . . . . 22 coe1
170169ad2antrr 707 . . . . . . . . . . . . . . . . . . . . 21 coe1
171170, 103ffvelrnd 5871 . . . . . . . . . . . . . . . . . . . 20 coe1
172133, 139rngass 15680 . . . . . . . . . . . . . . . . . . . 20 coe1 coe1 coe1 coe1 coe1 coe1
173129, 171, 131, 138, 172syl13anc 1186 . . . . . . . . . . . . . . . . . . 19 coe1 coe1 coe1 coe1
174 ply1divex.o . . . . . . . . . . . . . . . . . . . . 21
175133, 139, 174rnglidm 15687 . . . . . . . . . . . . . . . . . . . 20 coe1 coe1 coe1
176129, 138, 175syl2anc 643 . . . . . . . . . . . . . . . . . . 19 coe1 coe1
177166, 173, 1763eqtr3rd 2477 . . . . . . . . . . . . . . . . . 18 coe1 coe1 coe1
178159, 163, 1773eqtr4rd 2479 . . . . . . . . . . . . . . . . 17 coe1 coe1 coe1 .gmulGrpvar1
179178adantrr 698 . . . . . . . . . . . . . . . 16 coe1 coe1 coe1 .gmulGrpvar1
18010, 11, 13, 78, 98, 99, 100, 126, 150, 156, 132, 157, 179deg1sublt 20033 . . . . . . . . . . . . . . 15 coe1 .gmulGrpvar1
181180adantlrr 702 . . . . . . . . . . . . . 14 coe1 .gmulGrpvar1
18277ad2antrr 707 . . . . . . . . . . . . . . . . . 18
183 simpr 448 . . . . . . . . . . . . . . . . . 18
18413, 78grpsubcl 14869 . . . . . . . . . . . . . . . . . 18 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
185182, 183, 149, 184syl3anc 1184 . . . . . . . . . . . . . . . . 17 coe1 .gmulGrpvar1
186185adantrr 698 . . . . . . . . . . . . . . . 16 coe1 .gmulGrpvar1
187186adantlrr 702 . . . . . . . . . . . . . . 15 coe1 .gmulGrpvar1
188 simplrr 738 . . . . . . . . . . . . . . 15
189 fveq2 5728 . . . . . . . . . . . . . . . . . 18 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
190189breq1d 4222 . . . . . . . . . . . . . . . . 17 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
191 oveq1 6088 . . . . . . . . . . . . . . . . . . . 20 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
192191fveq2d 5732 . . . . . . . . . . . . . . . . . . 19 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
193192breq1d 4222 . . . . . . . . . . . . . . . . . 18 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
194193rexbidv 2726 . . . . . . . . . . . . . . . . 17 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
195190, 194imbi12d 312 . . . . . . . . . . . . . . . 16 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
196195rspcva 3050 . . . . . . . . . . . . . . 15 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
197187, 188, 196syl2anc 643 . . . . . . . . . . . . . 14 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
198181, 197mpd 15 . . . . . . . . . . . . 13 coe1 .gmulGrpvar1
19967ad3antrrr 711 . . . . . . . . . . . . . . . . . 18
200 simpr 448 . . . . . . . . . . . . . . . . . 18
201147adantr 452 . . . . . . . . . . . . . . . . . 18 coe1 .gmulGrpvar1
202 eqid 2436 . . . . . . . . . . . . . . . . . . 19
20313, 202rngacl 15691 . . . . . . . . . . . . . . . . . 18 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
204199, 200, 201, 203syl3anc 1184 . . . . . . . . . . . . . . . . 17 coe1 .gmulGrpvar1
20577ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . 22
206 simplr 732 . . . . . . . . . . . . . . . . . . . . . 22
207149adantr 452 . . . . . . . . . . . . . . . . . . . . . 22 coe1 .gmulGrpvar1
20817ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . 23
20913, 71rngcl 15677 . . . . . . . . . . . . . . . . . . . . . . 23
210199, 208, 200, 209syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . 22
21113, 202, 78grpsubsub4 14881 . . . . . . . . . . . . . . . . . . . . . 22 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
212205, 206, 207, 210, 211syl13anc 1186 . . . . . . . . . . . . . . . . . . . . 21 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
21313, 202, 71rngdi 15682 . . . . . . . . . . . . . . . . . . . . . . 23 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
214199, 208, 200, 201, 213syl13anc 1186 . . . . . . . . . . . . . . . . . . . . . 22 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
215214oveq2d 6097 . . . . . . . . . . . . . . . . . . . . 21 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
216212, 215eqtr4d 2471 . . . . . . . . . . . . . . . . . . . 20 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
217216fveq2d 5732 . . . . . . . . . . . . . . . . . . 19 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
218217breq1d 4222 . . . . . . . . . . . . . . . . . 18 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
219218biimpd 199 . . . . . . . . . . . . . . . . 17 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
220 oveq2 6089 . . . . . . . . . . . . . . . . . . . . 21 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
221220oveq2d 6097 . . . . . . . . . . . . . . . . . . . 20 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
222221fveq2d 5732 . . . . . . . . . . . . . . . . . . 19 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
223222breq1d 4222 . . . . . . . . . . . . . . . . . 18 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
224223rspcev 3052 . . . . . . . . . . . . . . . . 17 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
225204, 219, 224ee12an 1372 . . . . . . . . . . . . . . . 16 coe1 .gmulGrpvar1
226225rexlimdva 2830 . . . . . . . . . . . . . . 15 coe1 .gmulGrpvar1
227226adantrr 698 . . . . . . . . . . . . . 14 coe1 .gmulGrpvar1
228227adantlrr 702 . . . . . . . . . . . . 13 coe1 .gmulGrpvar1
229198, 228mpd 15 . . . . . . . . . . . 12
230229expr 599 . . . . . . . . . . 11
231230ralrimiva 2789 . . . . . . . . . 10
232 fveq2 5728 . . . . . . . . . . . . 13
233232breq1d 4222 . . . . . . . . . . . 12
234 oveq1 6088 . . . . . . . . . . . . . . . 16
235234fveq2d 5732 . . . . . . . . . . . . . . 15
236235breq1d 4222 . . . . . . . . . . . . . 14
237236rexbidv 2726 . . . . . . . . . . . . 13
238 oveq2 6089 . . . . . . . . . . . . . . . . 17
239238oveq2d 6097 . . . . . . . . . . . . . . . 16
240239fveq2d 5732 . . . . . . . . . . . . . . 15
241240breq1d 4222 . . . . . . . . . . . . . 14
242241cbvrexv 2933 . . . . . . . . . . . . 13
243237, 242syl6bb 253 . . . . . . . . . . . 12
244233, 243imbi12d 312 . . . . . . . . . . 11
245244cbvralv 2932 . . . . . . . . . 10
246231, 245sylib 189 . . . . . . . . 9
247246exp32 589 . . . . . . . 8
248247com12 29 . . . . . . 7
249248a2d 24 . . . . . 6
25055, 60, 65, 60, 95, 249nn0ind 10366 . . . . 5
251250impcom 420 . . . 4
252 fveq2 5728 . . . . . . 7
253252breq1d 4222 . . . . . 6
254 oveq1 6088 . . . . . . . . 9
255254fveq2d 5732 . . . . . . . 8
256255breq1d 4222 . . . . . . 7
257256rexbidv 2726 . . . . . 6
258253, 257imbi12d 312 . . . . 5
259258rspcva 3050 . . . 4
26050, 251, 259syl2anc 643 . . 3
261260rexlimdva 2830 . 2
26249, 261mpd 15 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   wceq 1652   wcel 1725   wne 2599  wral 2705  wrex 2706   cun 3318   wss 3320  csn 3814   class class class wbr 4212  wf 5450  cfv 5454  (class class class)co 6081  cc 8988  cr 8989  cc0 8990  c1 8991   caddc 8993   cmnf 9118   clt 9120   cle 9121   cmin 9291  cn 10000  cn0 10221  cz 10282  cbs 13469   cplusg 13529  cmulr 13530  cvsca 13533  c0g 13723  cgrp 14685  csg 14688  .gcmg 14689  mulGrpcmgp 15648  crg 15660  cur 15662  var1cv1 16570  Poly1cpl1 16571  coe1cco1 16574   deg1 cdg1 19977 This theorem is referenced by:  ply1divalg  20060 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-rep 4320  ax-sep 4330  ax-nul 4338  ax-pow 4377  ax-pr 4403  ax-un 4701  ax-inf2 7596  ax-cnex 9046  ax-resscn 9047  ax-1cn 9048  ax-icn 9049  ax-addcl 9050  ax-addrcl 9051  ax-mulcl 9052  ax-mulrcl 9053  ax-mulcom 9054  ax-addass 9055  ax-mulass 9056  ax-distr 9057  ax-i2m1 9058  ax-1ne0 9059  ax-1rid 9060  ax-rnegex 9061  ax-rrecex 9062  ax-cnre 9063  ax-pre-lttri 9064  ax-pre-lttrn 9065  ax-pre-ltadd 9066  ax-pre-mulgt0 9067  ax-pre-sup 9068  ax-addf 9069  ax-mulf 9070 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-nel 2602  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2958  df-sbc 3162  df-csb 3252  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-pss 3336  df-nul 3629  df-if 3740  df-pw 3801  df-sn 3820  df-pr 3821  df-tp 3822  df-op 3823  df-uni 4016  df-int 4051  df-iun 4095  df-iin 4096  df-br 4213  df-opab 4267  df-mpt 4268  df-tr 4303  df-eprel 4494  df-id 4498  df-po 4503  df-so 4504  df-fr 4541  df-se 4542  df-we 4543  df-ord 4584  df-on 4585  df-lim 4586  df-suc 4587  df-om 4846  df-xp 4884  df-rel 4885  df-cnv 4886  df-co 4887  df-dm 4888  df-rn 4889  df-res 4890  df-ima 4891  df-iota 5418  df-fun 5456  df-fn 5457  df-f 5458  df-f1 5459  df-fo 5460  df-f1o 5461  df-fv 5462  df-isom 5463  df-ov 6084  df-oprab 6085  df-mpt2 6086  df-of 6305  df-ofr 6306  df-1st 6349  df-2nd 6350  df-tpos 6479  df-riota 6549  df-recs 6633  df-rdg 6668  df-1o 6724  df-2o 6725  df-oadd 6728  df-er 6905  df-map 7020  df-pm 7021  df-ixp 7064  df-en 7110  df-dom 7111  df-sdom 7112  df-fin 7113  df-sup 7446  df-oi 7479  df-card 7826  df-pnf 9122  df-mnf 9123  df-xr 9124  df-ltxr 9125  df-le 9126  df-sub 9293  df-neg 9294  df-nn 10001  df-2 10058  df-3 10059  df-4 10060  df-5 10061  df-6 10062  df-7 10063  df-8 10064  df-9 10065  df-10 10066  df-n0 10222  df-z 10283  df-dec 10383  df-uz 10489  df-fz 11044  df-fzo 11136  df-seq 11324  df-hash 11619  df-struct 13471  df-ndx 13472  df-slot 13473  df-base 13474  df-sets 13475  df-ress 13476  df-plusg 13542  df-mulr 13543  df-starv 13544  df-sca 13545  df-vsca 13546  df-tset 13548  df-ple 13549  df-ds 13551  df-unif 13552  df-0g 13727  df-gsum 13728  df-mre 13811  df-mrc 13812  df-acs 13814  df-mnd 14690  df-mhm 14738  df-submnd 14739  df-grp 14812  df-minusg 14813  df-sbg 14814  df-mulg 14815  df-subg 14941  df-ghm 15004  df-cntz 15116  df-cmn 15414  df-abl 15415  df-mgp 15649  df-rng 15663  df-cring 15664  df-ur 15665  df-oppr 15728  df-dvdsr 15746  df-unit 15747  df-invr 15777  df-subrg 15866  df-lmod 15952  df-lss 16009  df-rlreg 16343  df-psr 16417  df-mvr 16418  df-mpl 16419  df-opsr 16425  df-psr1 16576  df-vr1 16577  df-ply1 16578  df-coe1 16581  df-cnfld 16704  df-mdeg 19978  df-deg1 19979
 Copyright terms: Public domain W3C validator