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

Theorem ply1divex 23085
 Description: Lemma for ply1divalg 23086: 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 5881 . . . . 5
21breq1d 4433 . . . 4
32rexbidv 2936 . . 3
4 nnssnn0 10879 . . . . 5
5 ply1divalg.r1 . . . . . . . . . 10
65adantr 466 . . . . . . . . 9
7 ply1divalg.f . . . . . . . . . 10
87adantr 466 . . . . . . . . 9
9 simpr 462 . . . . . . . . 9
10 ply1divalg.d . . . . . . . . . 10 deg1
11 ply1divalg.p . . . . . . . . . 10 Poly1
12 ply1divalg.z . . . . . . . . . 10
13 ply1divalg.b . . . . . . . . . 10
1410, 11, 12, 13deg1nn0cl 23035 . . . . . . . . 9
156, 8, 9, 14syl3anc 1264 . . . . . . . 8
1615nn0red 10933 . . . . . . 7
17 ply1divalg.g1 . . . . . . . . . 10
18 ply1divalg.g2 . . . . . . . . . 10
1910, 11, 12, 13deg1nn0cl 23035 . . . . . . . . . 10
205, 17, 18, 19syl3anc 1264 . . . . . . . . 9
2120nn0red 10933 . . . . . . . 8
2221adantr 466 . . . . . . 7
2316, 22resubcld 10054 . . . . . 6
24 arch 10873 . . . . . 6
2523, 24syl 17 . . . . 5
26 ssrexv 3526 . . . . 5
274, 25, 26mpsyl 65 . . . 4
2816adantr 466 . . . . . . 7
2921ad2antrr 730 . . . . . . 7
30 nn0re 10885 . . . . . . . 8
3130adantl 467 . . . . . . 7
3228, 29, 31ltsubadd2d 10218 . . . . . 6
3332biimpd 210 . . . . 5
3433reximdva 2897 . . . 4
3527, 34mpd 15 . . 3
36 0nn0 10891 . . . 4
3710, 11, 12deg1z 23034 . . . . . 6
385, 37syl 17 . . . . 5
39 0re 9650 . . . . . . 7
40 readdcl 9629 . . . . . . 7
4121, 39, 40sylancl 666 . . . . . 6
42 mnflt 11432 . . . . . 6
4341, 42syl 17 . . . . 5
4438, 43eqbrtrd 4444 . . . 4
45 oveq2 6313 . . . . . 6
4645breq2d 4435 . . . . 5
4746rspcev 3182 . . . 4
4836, 44, 47sylancr 667 . . 3
493, 35, 48pm2.61ne 2735 . 2
507adantr 466 . . . 4
51 oveq2 6313 . . . . . . . . . 10
5251breq2d 4435 . . . . . . . . 9
5352imbi1d 318 . . . . . . . 8
5453ralbidv 2861 . . . . . . 7
5554imbi2d 317 . . . . . 6
56 oveq2 6313 . . . . . . . . . 10
5756breq2d 4435 . . . . . . . . 9
5857imbi1d 318 . . . . . . . 8
5958ralbidv 2861 . . . . . . 7
6059imbi2d 317 . . . . . 6
61 oveq2 6313 . . . . . . . . . 10
6261breq2d 4435 . . . . . . . . 9
6362imbi1d 318 . . . . . . . 8
6463ralbidv 2861 . . . . . . 7
6564imbi2d 317 . . . . . 6
6611ply1ring 18840 . . . . . . . . . . . 12
675, 66syl 17 . . . . . . . . . . 11
6813, 12ring0cl 17801 . . . . . . . . . . 11
6967, 68syl 17 . . . . . . . . . 10
7069ad2antrr 730 . . . . . . . . 9
71 ply1divalg.t . . . . . . . . . . . . . . . . 17
7213, 71, 12ringrz 17817 . . . . . . . . . . . . . . . 16
7367, 17, 72syl2anc 665 . . . . . . . . . . . . . . 15
7473oveq2d 6321 . . . . . . . . . . . . . 14
7574adantr 466 . . . . . . . . . . . . 13
76 ringgrp 17784 . . . . . . . . . . . . . . 15
7767, 76syl 17 . . . . . . . . . . . . . 14
78 ply1divalg.m . . . . . . . . . . . . . . 15
7913, 12, 78grpsubid1 16738 . . . . . . . . . . . . . 14
8077, 79sylan 473 . . . . . . . . . . . . 13
8175, 80eqtr2d 2464 . . . . . . . . . . . 12
8281fveq2d 5885 . . . . . . . . . . 11
8320nn0cnd 10934 . . . . . . . . . . . . 13
8483addid1d 9840 . . . . . . . . . . . 12
8584adantr 466 . . . . . . . . . . 11
8682, 85breq12d 4436 . . . . . . . . . 10
8786biimpa 486 . . . . . . . . 9
88 oveq2 6313 . . . . . . . . . . . . 13
8988oveq2d 6321 . . . . . . . . . . . 12
9089fveq2d 5885 . . . . . . . . . . 11
9190breq1d 4433 . . . . . . . . . 10
9291rspcev 3182 . . . . . . . . 9
9370, 87, 92syl2anc 665 . . . . . . . 8
9493ex 435 . . . . . . 7
9594ralrimiva 2836 . . . . . 6
96 nn0addcl 10912 . . . . . . . . . . . . . . . . . 18
9720, 96sylan 473 . . . . . . . . . . . . . . . . 17
9897adantr 466 . . . . . . . . . . . . . . . 16
995ad2antrr 730 . . . . . . . . . . . . . . . 16
100 simprl 762 . . . . . . . . . . . . . . . 16
10110, 11, 13deg1cl 23030 . . . . . . . . . . . . . . . . . . . . 21
102101adantl 467 . . . . . . . . . . . . . . . . . . . 20
10320ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . 22
104 peano2nn0 10917 . . . . . . . . . . . . . . . . . . . . . . 23
105104ad2antlr 731 . . . . . . . . . . . . . . . . . . . . . 22
106103, 105nn0addcld 10936 . . . . . . . . . . . . . . . . . . . . 21
107106nn0zd 11045 . . . . . . . . . . . . . . . . . . . 20
108 degltlem1 23019 . . . . . . . . . . . . . . . . . . . 20
109102, 107, 108syl2anc 665 . . . . . . . . . . . . . . . . . . 19
110109biimpd 210 . . . . . . . . . . . . . . . . . 18
111110impr 623 . . . . . . . . . . . . . . . . 17
11220adantr 466 . . . . . . . . . . . . . . . . . . . . 21
113112nn0cnd 10934 . . . . . . . . . . . . . . . . . . . 20
114 nn0cn 10886 . . . . . . . . . . . . . . . . . . . . . 22
115114adantl 467 . . . . . . . . . . . . . . . . . . . . 21
116 peano2cn 9812 . . . . . . . . . . . . . . . . . . . . 21
117115, 116syl 17 . . . . . . . . . . . . . . . . . . . 20
118 1cnd 9666 . . . . . . . . . . . . . . . . . . . 20
119113, 117, 118addsubassd 10013 . . . . . . . . . . . . . . . . . . 19
120 ax-1cn 9604 . . . . . . . . . . . . . . . . . . . . 21
121 pncan 9888 . . . . . . . . . . . . . . . . . . . . 21
122115, 120, 121sylancl 666 . . . . . . . . . . . . . . . . . . . 20
123122oveq2d 6321 . . . . . . . . . . . . . . . . . . 19
124119, 123eqtrd 2463 . . . . . . . . . . . . . . . . . 18
125124adantr 466 . . . . . . . . . . . . . . . . 17
126111, 125breqtrd 4448 . . . . . . . . . . . . . . . 16
12767ad2antrr 730 . . . . . . . . . . . . . . . . . 18
12817ad2antrr 730 . . . . . . . . . . . . . . . . . 18
1295ad2antrr 730 . . . . . . . . . . . . . . . . . . 19
130 ply1divex.i . . . . . . . . . . . . . . . . . . . . 21
131130ad2antrr 730 . . . . . . . . . . . . . . . . . . . 20
132 eqid 2422 . . . . . . . . . . . . . . . . . . . . . . 23 coe1 coe1
133 ply1divex.k . . . . . . . . . . . . . . . . . . . . . . 23
134132, 13, 11, 133coe1f 18803 . . . . . . . . . . . . . . . . . . . . . 22 coe1
135134adantl 467 . . . . . . . . . . . . . . . . . . . . 21 coe1
136 simplr 760 . . . . . . . . . . . . . . . . . . . . . 22
137103, 136nn0addcld 10936 . . . . . . . . . . . . . . . . . . . . 21
138135, 137ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . 20 coe1
139 ply1divex.u . . . . . . . . . . . . . . . . . . . . 21
140133, 139ringcl 17793 . . . . . . . . . . . . . . . . . . . 20 coe1 coe1
141129, 131, 138, 140syl3anc 1264 . . . . . . . . . . . . . . . . . . 19 coe1
142 eqid 2422 . . . . . . . . . . . . . . . . . . . 20 var1 var1
143 eqid 2422 . . . . . . . . . . . . . . . . . . . 20
144 eqid 2422 . . . . . . . . . . . . . . . . . . . 20 mulGrp mulGrp
145 eqid 2422 . . . . . . . . . . . . . . . . . . . 20 .gmulGrp .gmulGrp
146133, 11, 142, 143, 144, 145, 13ply1tmcl 18864 . . . . . . . . . . . . . . . . . . 19 coe1 coe1 .gmulGrpvar1
147129, 141, 136, 146syl3anc 1264 . . . . . . . . . . . . . . . . . 18 coe1 .gmulGrpvar1
14813, 71ringcl 17793 . . . . . . . . . . . . . . . . . 18 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
149127, 128, 147, 148syl3anc 1264 . . . . . . . . . . . . . . . . 17 coe1 .gmulGrpvar1
150149adantrr 721 . . . . . . . . . . . . . . . 16 coe1 .gmulGrpvar1
151103nn0red 10933 . . . . . . . . . . . . . . . . . . 19
152151leidd 10187 . . . . . . . . . . . . . . . . . 18
15310, 133, 11, 142, 143, 144, 145deg1tmle 23064 . . . . . . . . . . . . . . . . . . 19 coe1 coe1 .gmulGrpvar1
154129, 141, 136, 153syl3anc 1264 . . . . . . . . . . . . . . . . . 18 coe1 .gmulGrpvar1
15511, 10, 129, 13, 71, 128, 147, 103, 136, 152, 154deg1mulle2 23056 . . . . . . . . . . . . . . . . 17 coe1 .gmulGrpvar1
156155adantrr 721 . . . . . . . . . . . . . . . 16 coe1 .gmulGrpvar1
157 eqid 2422 . . . . . . . . . . . . . . . 16 coe1 coe1 .gmulGrpvar1 coe1 coe1 .gmulGrpvar1
158 eqid 2422 . . . . . . . . . . . . . . . . . . 19
159158, 133, 11, 142, 143, 144, 145, 13, 71, 139, 128, 129, 141, 136, 103coe1tmmul2fv 18870 . . . . . . . . . . . . . . . . . 18 coe1 coe1 .gmulGrpvar1 coe1 coe1
160103nn0cnd 10934 . . . . . . . . . . . . . . . . . . . 20
161114ad2antlr 731 . . . . . . . . . . . . . . . . . . . 20
162160, 161addcomd 9842 . . . . . . . . . . . . . . . . . . 19
163162fveq2d 5885 . . . . . . . . . . . . . . . . . 18 coe1 coe1 .gmulGrpvar1 coe1 coe1 .gmulGrpvar1
164 ply1divex.g3 . . . . . . . . . . . . . . . . . . . . 21 coe1
165164oveq1d 6320 . . . . . . . . . . . . . . . . . . . 20 coe1 coe1 coe1
166165ad2antrr 730 . . . . . . . . . . . . . . . . . . 19 coe1 coe1 coe1
167 eqid 2422 . . . . . . . . . . . . . . . . . . . . . . . 24 coe1 coe1
168167, 13, 11, 133coe1f 18803 . . . . . . . . . . . . . . . . . . . . . . 23 coe1
16917, 168syl 17 . . . . . . . . . . . . . . . . . . . . . 22 coe1
170169ad2antrr 730 . . . . . . . . . . . . . . . . . . . . 21 coe1
171170, 103ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . 20 coe1
172133, 139ringass 17796 . . . . . . . . . . . . . . . . . . . 20 coe1 coe1 coe1 coe1 coe1 coe1
173129, 171, 131, 138, 172syl13anc 1266 . . . . . . . . . . . . . . . . . . 19 coe1 coe1 coe1 coe1
174 ply1divex.o . . . . . . . . . . . . . . . . . . . . 21
175133, 139, 174ringlidm 17803 . . . . . . . . . . . . . . . . . . . 20 coe1 coe1 coe1
176129, 138, 175syl2anc 665 . . . . . . . . . . . . . . . . . . 19 coe1 coe1
177166, 173, 1763eqtr3rd 2472 . . . . . . . . . . . . . . . . . 18 coe1 coe1 coe1
178159, 163, 1773eqtr4rd 2474 . . . . . . . . . . . . . . . . 17 coe1 coe1 coe1 .gmulGrpvar1
179178adantrr 721 . . . . . . . . . . . . . . . 16 coe1 coe1 coe1 .gmulGrpvar1
18010, 11, 13, 78, 98, 99, 100, 126, 150, 156, 132, 157, 179deg1sublt 23057 . . . . . . . . . . . . . . 15 coe1 .gmulGrpvar1
181180adantlrr 725 . . . . . . . . . . . . . 14 coe1 .gmulGrpvar1
18277ad2antrr 730 . . . . . . . . . . . . . . . . . 18
183 simpr 462 . . . . . . . . . . . . . . . . . 18
18413, 78grpsubcl 16733 . . . . . . . . . . . . . . . . . 18 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
185182, 183, 149, 184syl3anc 1264 . . . . . . . . . . . . . . . . 17 coe1 .gmulGrpvar1
186185adantrr 721 . . . . . . . . . . . . . . . 16 coe1 .gmulGrpvar1
187186adantlrr 725 . . . . . . . . . . . . . . 15 coe1 .gmulGrpvar1
188 simplrr 769 . . . . . . . . . . . . . . 15
189 fveq2 5881 . . . . . . . . . . . . . . . . . 18 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
190189breq1d 4433 . . . . . . . . . . . . . . . . 17 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
191 oveq1 6312 . . . . . . . . . . . . . . . . . . . 20 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
192191fveq2d 5885 . . . . . . . . . . . . . . . . . . 19 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
193192breq1d 4433 . . . . . . . . . . . . . . . . . 18 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
194193rexbidv 2936 . . . . . . . . . . . . . . . . 17 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
195190, 194imbi12d 321 . . . . . . . . . . . . . . . 16 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
196195rspcva 3180 . . . . . . . . . . . . . . 15 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
197187, 188, 196syl2anc 665 . . . . . . . . . . . . . 14 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
198181, 197mpd 15 . . . . . . . . . . . . 13 coe1 .gmulGrpvar1
19967ad3antrrr 734 . . . . . . . . . . . . . . . . . 18
200 simpr 462 . . . . . . . . . . . . . . . . . 18
201147adantr 466 . . . . . . . . . . . . . . . . . 18 coe1 .gmulGrpvar1
202 eqid 2422 . . . . . . . . . . . . . . . . . . 19
20313, 202ringacl 17807 . . . . . . . . . . . . . . . . . 18 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
204199, 200, 201, 203syl3anc 1264 . . . . . . . . . . . . . . . . 17 coe1 .gmulGrpvar1
20577ad3antrrr 734 . . . . . . . . . . . . . . . . . . . . . 22
206 simplr 760 . . . . . . . . . . . . . . . . . . . . . 22
207149adantr 466 . . . . . . . . . . . . . . . . . . . . . 22 coe1 .gmulGrpvar1
20817ad3antrrr 734 . . . . . . . . . . . . . . . . . . . . . . 23
20913, 71ringcl 17793 . . . . . . . . . . . . . . . . . . . . . . 23
210199, 208, 200, 209syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . 22
21113, 202, 78grpsubsub4 16746 . . . . . . . . . . . . . . . . . . . . . 22 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
212205, 206, 207, 210, 211syl13anc 1266 . . . . . . . . . . . . . . . . . . . . 21 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
21313, 202, 71ringdi 17798 . . . . . . . . . . . . . . . . . . . . . . 23 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
214199, 208, 200, 201, 213syl13anc 1266 . . . . . . . . . . . . . . . . . . . . . 22 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
215214oveq2d 6321 . . . . . . . . . . . . . . . . . . . . 21 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
216212, 215eqtr4d 2466 . . . . . . . . . . . . . . . . . . . 20 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
217216fveq2d 5885 . . . . . . . . . . . . . . . . . . 19 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
218217breq1d 4433 . . . . . . . . . . . . . . . . . 18 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
219218biimpd 210 . . . . . . . . . . . . . . . . 17 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
220 oveq2 6313 . . . . . . . . . . . . . . . . . . . . 21 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
221220oveq2d 6321 . . . . . . . . . . . . . . . . . . . 20 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
222221fveq2d 5885 . . . . . . . . . . . . . . . . . . 19 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
223222breq1d 4433 . . . . . . . . . . . . . . . . . 18 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
224223rspcev 3182 . . . . . . . . . . . . . . . . 17 coe1 .gmulGrpvar1 coe1 .gmulGrpvar1
225204, 219, 224syl6an 547 . . . . . . . . . . . . . . . 16 coe1 .gmulGrpvar1
226225rexlimdva 2914 . . . . . . . . . . . . . . 15 coe1 .gmulGrpvar1
227226adantrr 721 . . . . . . . . . . . . . 14 coe1 .gmulGrpvar1
228227adantlrr 725 . . . . . . . . . . . . 13 coe1 .gmulGrpvar1
229198, 228mpd 15 . . . . . . . . . . . 12
230229expr 618 . . . . . . . . . . 11
231230ralrimiva 2836 . . . . . . . . . 10
232 fveq2 5881 . . . . . . . . . . . . 13
233232breq1d 4433 . . . . . . . . . . . 12
234 oveq1 6312 . . . . . . . . . . . . . . . 16
235234fveq2d 5885 . . . . . . . . . . . . . . 15
236235breq1d 4433 . . . . . . . . . . . . . 14
237236rexbidv 2936 . . . . . . . . . . . . 13
238 oveq2 6313 . . . . . . . . . . . . . . . . 17
239238oveq2d 6321 . . . . . . . . . . . . . . . 16
240239fveq2d 5885 . . . . . . . . . . . . . . 15
241240breq1d 4433 . . . . . . . . . . . . . 14
242241cbvrexv 3055 . . . . . . . . . . . . 13
243237, 242syl6bb 264 . . . . . . . . . . . 12
244233, 243imbi12d 321 . . . . . . . . . . 11
245244cbvralv 3054 . . . . . . . . . 10
246231, 245sylib 199 . . . . . . . . 9
247246exp32 608 . . . . . . . 8
248247com12 32 . . . . . . 7
249248a2d 29 . . . . . 6
25055, 60, 65, 60, 95, 249nn0ind 11037 . . . . 5
251250impcom 431 . . . 4
252 fveq2 5881 . . . . . . 7
253252breq1d 4433 . . . . . 6
254 oveq1 6312 . . . . . . . . 9
255254fveq2d 5885 . . . . . . . 8
256255breq1d 4433 . . . . . . 7
257256rexbidv 2936 . . . . . 6
258253, 257imbi12d 321 . . . . 5
259258rspcva 3180 . . . 4
26050, 251, 259syl2anc 665 . . 3
261260rexlimdva 2914 . 2
26249, 261mpd 15 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370   wceq 1437   wcel 1872   wne 2614  wral 2771  wrex 2772   cun 3434   wss 3436  csn 3998   class class class wbr 4423  wf 5597  cfv 5601  (class class class)co 6305  cc 9544  cr 9545  cc0 9546  c1 9547   caddc 9549   cmnf 9680   clt 9682   cle 9683   cmin 9867  cn 10616  cn0 10876  cz 10944  cbs 15120   cplusg 15189  cmulr 15190  cvsca 15193  c0g 15337  cgrp 16668  csg 16670  .gcmg 16671  mulGrpcmgp 17722  cur 17734  crg 17779  var1cv1 18768  Poly1cpl1 18769  coe1cco1 18770   deg1 cdg1 23001 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-rep 4536  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597  ax-inf2 8155  ax-cnex 9602  ax-resscn 9603  ax-1cn 9604  ax-icn 9605  ax-addcl 9606  ax-addrcl 9607  ax-mulcl 9608  ax-mulrcl 9609  ax-mulcom 9610  ax-addass 9611  ax-mulass 9612  ax-distr 9613  ax-i2m1 9614  ax-1ne0 9615  ax-1rid 9616  ax-rnegex 9617  ax-rrecex 9618  ax-cnre 9619  ax-pre-lttri 9620  ax-pre-lttrn 9621  ax-pre-ltadd 9622  ax-pre-mulgt0 9623  ax-pre-sup 9624  ax-addf 9625  ax-mulf 9626 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rmo 2779  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-int 4256  df-iun 4301  df-iin 4302  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-se 4813  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-of 6545  df-ofr 6546  df-om 6707  df-1st 6807  df-2nd 6808  df-supp 6926  df-tpos 6984  df-wrecs 7039  df-recs 7101  df-rdg 7139  df-1o 7193  df-2o 7194  df-oadd 7197  df-er 7374  df-map 7485  df-pm 7486  df-ixp 7534  df-en 7581  df-dom 7582  df-sdom 7583  df-fin 7584  df-fsupp 7893  df-sup 7965  df-oi 8034  df-card 8381  df-pnf 9684  df-mnf 9685  df-xr 9686  df-ltxr 9687  df-le 9688  df-sub 9869  df-neg 9870  df-nn 10617  df-2 10675  df-3 10676  df-4 10677  df-5 10678  df-6 10679  df-7 10680  df-8 10681  df-9 10682  df-10 10683  df-n0 10877  df-z 10945  df-dec 11059  df-uz 11167  df-fz 11792  df-fzo 11923  df-seq 12220  df-hash 12522  df-struct 15122  df-ndx 15123  df-slot 15124  df-base 15125  df-sets 15126  df-ress 15127  df-plusg 15202  df-mulr 15203  df-starv 15204  df-sca 15205  df-vsca 15206  df-tset 15208  df-ple 15209  df-ds 15211  df-unif 15212  df-0g 15339  df-gsum 15340  df-mre 15491  df-mrc 15492  df-acs 15494  df-mgm 16487  df-sgrp 16526  df-mnd 16536  df-mhm 16581  df-submnd 16582  df-grp 16672  df-minusg 16673  df-sbg 16674  df-mulg 16675  df-subg 16813  df-ghm 16880  df-cntz 16970  df-cmn 17431  df-abl 17432  df-mgp 17723  df-ur 17735  df-ring 17781  df-cring 17782  df-oppr 17850  df-dvdsr 17868  df-unit 17869  df-invr 17899  df-subrg 18005  df-lmod 18092  df-lss 18155  df-rlreg 18506  df-psr 18579  df-mvr 18580  df-mpl 18581  df-opsr 18583  df-psr1 18772  df-vr1 18773  df-ply1 18774  df-coe1 18775  df-cnfld 18970  df-mdeg 23002  df-deg1 23003 This theorem is referenced by:  ply1divalg  23086
 Copyright terms: Public domain W3C validator