plydivex - Metamath Proof Explorer

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

Theorem plydivex 23144

Description: Lemma for plydivalg 23146. (Contributed by Mario Carneiro, 24-Jul-2014.)

**Hypotheses**
Ref	Expression
plydiv.pl	$/\$ $/\$
plydiv.tm	$/\$ $/\$
plydiv.rc	$/\$ $/\$
plydiv.m1
plydiv.f	Poly
plydiv.g	Poly
plydiv.z
plydiv.r

**Assertion**
Ref	Expression
plydivex	Poly $\/$ deg deg

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

Proof of Theorem plydivex Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		plydiv.f	. . . . . 6 Poly
2		dgrcl 23081	. . . . . 6 Poly deg
3	1, 2	syl 17	. . . . 5 deg
4	3	nn0red 10915	. . . 4 deg
5		plydiv.g	. . . . . 6 Poly
6		dgrcl 23081	. . . . . 6 Poly deg
7	5, 6	syl 17	. . . . 5 deg
8	7	nn0red 10915	. . . 4 deg
9	4, 8	resubcld 10036	. . 3 deg deg
10		arch 10855	. . 3 deg deg deg deg
11	9, 10	syl 17	. 2 deg deg
12		olc 385	. . . 4 deg deg $\/$ deg deg
13	1	adantr 466	. . . . 5 $/\$ Poly
14		nnnn0 10865	. . . . . . 7
15		breq2 4421	. . . . . . . . . . . 12 deg deg deg deg
16	15	orbi2d 706	. . . . . . . . . . 11 $\/$ deg deg $\/$ deg deg
17	16	imbi1d 318	. . . . . . . . . 10 $\/$ deg deg Poly $\/$ deg deg $\/$ deg deg Poly $\/$ deg deg
18	17	ralbidv 2862	. . . . . . . . 9 Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg
19	18	imbi2d 317	. . . . . . . 8 Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg
20		breq2 4421	. . . . . . . . . . . 12 deg deg deg deg
21	20	orbi2d 706	. . . . . . . . . . 11 $\/$ deg deg $\/$ deg deg
22	21	imbi1d 318	. . . . . . . . . 10 $\/$ deg deg Poly $\/$ deg deg $\/$ deg deg Poly $\/$ deg deg
23	22	ralbidv 2862	. . . . . . . . 9 Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg
24	23	imbi2d 317	. . . . . . . 8 Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg
25		breq2 4421	. . . . . . . . . . . 12 deg deg deg deg
26	25	orbi2d 706	. . . . . . . . . . 11 $\/$ deg deg $\/$ deg deg
27	26	imbi1d 318	. . . . . . . . . 10 $\/$ deg deg Poly $\/$ deg deg $\/$ deg deg Poly $\/$ deg deg
28	27	ralbidv 2862	. . . . . . . . 9 Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg
29	28	imbi2d 317	. . . . . . . 8 Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg
30		plydiv.pl	. . . . . . . . . . . 12 $/\$ $/\$
31	30	adantlr 719	. . . . . . . . . . 11 $/\$ Poly $/\$ $\/$ deg deg $/\$ $/\$
32		plydiv.tm	. . . . . . . . . . . 12 $/\$ $/\$
33	32	adantlr 719	. . . . . . . . . . 11 $/\$ Poly $/\$ $\/$ deg deg $/\$ $/\$
34		plydiv.rc	. . . . . . . . . . . 12 $/\$ $/\$
35	34	adantlr 719	. . . . . . . . . . 11 $/\$ Poly $/\$ $\/$ deg deg $/\$ $/\$
36		plydiv.m1	. . . . . . . . . . . 12
37	36	adantr 466	. . . . . . . . . . 11 $/\$ Poly $/\$ $\/$ deg deg
38		simprl 762	. . . . . . . . . . 11 $/\$ Poly $/\$ $\/$ deg deg Poly
39	5	adantr 466	. . . . . . . . . . 11 $/\$ Poly $/\$ $\/$ deg deg Poly
40		plydiv.z	. . . . . . . . . . . 12
41	40	adantr 466	. . . . . . . . . . 11 $/\$ Poly $/\$ $\/$ deg deg
42		eqid 2420	. . . . . . . . . . 11
43		simprr 764	. . . . . . . . . . 11 $/\$ Poly $/\$ $\/$ deg deg $\/$ deg deg
44	31, 33, 35, 37, 38, 39, 41, 42, 43	plydivlem3 23142	. . . . . . . . . 10 $/\$ Poly $/\$ $\/$ deg deg Poly $\/$ deg deg
45	44	expr 618	. . . . . . . . 9 $/\$ Poly $\/$ deg deg Poly $\/$ deg deg
46	45	ralrimiva 2837	. . . . . . . 8 Poly $\/$ deg deg Poly $\/$ deg deg
47		eqeq1 2424	. . . . . . . . . . . . . . . 16
48		fveq2 5872	. . . . . . . . . . . . . . . . . 18 deg deg
49	48	oveq1d 6311	. . . . . . . . . . . . . . . . 17 deg deg deg deg
50	49	breq1d 4427	. . . . . . . . . . . . . . . 16 deg deg deg deg
51	47, 50	orbi12d 714	. . . . . . . . . . . . . . 15 $\/$ deg deg $\/$ deg deg
52		oveq1 6303	. . . . . . . . . . . . . . . . . 18
53	52	eqeq1d 2422	. . . . . . . . . . . . . . . . 17
54	52	fveq2d 5876	. . . . . . . . . . . . . . . . . 18 deg deg
55	54	breq1d 4427	. . . . . . . . . . . . . . . . 17 deg deg deg deg
56	53, 55	orbi12d 714	. . . . . . . . . . . . . . . 16 $\/$ deg deg $\/$ deg deg
57	56	rexbidv 2937	. . . . . . . . . . . . . . 15 Poly $\/$ deg deg Poly $\/$ deg deg
58	51, 57	imbi12d 321	. . . . . . . . . . . . . 14 $\/$ deg deg Poly $\/$ deg deg $\/$ deg deg Poly $\/$ deg deg
59	58	cbvralv 3053	. . . . . . . . . . . . 13 Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg
60		simplll 766	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Poly $/\$ Poly $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg
61	60, 30	sylan 473	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Poly $/\$ Poly $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg $/\$ $/\$
62	60, 32	sylan 473	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Poly $/\$ Poly $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg $/\$ $/\$
63	60, 34	sylan 473	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Poly $/\$ Poly $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg $/\$ $/\$
64	60, 36	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Poly $/\$ Poly $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg
65		simplr 760	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Poly $/\$ Poly $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg Poly
66	60, 5	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Poly $/\$ Poly $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg Poly
67	60, 40	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Poly $/\$ Poly $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg
68		simpllr 767	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Poly $/\$ Poly $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg
69		simprrr 773	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Poly $/\$ Poly $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg deg deg
70		simprrl 772	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Poly $/\$ Poly $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg
71		eqid 2420	. . . . . . . . . . . . . . . 16
72		oveq1 6303	. . . . . . . . . . . . . . . . . 18
73	72	oveq2d 6312	. . . . . . . . . . . . . . . . 17 coeffdeg coeffdeg coeffdeg coeffdeg
74	73	cbvmptv 4509	. . . . . . . . . . . . . . . 16 coeffdeg coeffdeg coeffdeg coeffdeg
75		simprl 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Poly $/\$ Poly $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg
76		oveq2 6304	. . . . . . . . . . . . . . . . . . . . . . 23
77	76	oveq2d 6312	. . . . . . . . . . . . . . . . . . . . . 22
78	77	eqeq1d 2422	. . . . . . . . . . . . . . . . . . . . 21
79	77	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . 22 deg deg
80	79	breq1d 4427	. . . . . . . . . . . . . . . . . . . . 21 deg deg deg deg
81	78, 80	orbi12d 714	. . . . . . . . . . . . . . . . . . . 20 $\/$ deg deg $\/$ deg deg
82	81	cbvrexv 3054	. . . . . . . . . . . . . . . . . . 19 Poly $\/$ deg deg Poly $\/$ deg deg
83	82	imbi2i 313	. . . . . . . . . . . . . . . . . 18 $\/$ deg deg Poly $\/$ deg deg $\/$ deg deg Poly $\/$ deg deg
84	83	ralbii 2854	. . . . . . . . . . . . . . . . 17 Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg
85	75, 84	sylib 199	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Poly $/\$ Poly $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg
86		eqid 2420	. . . . . . . . . . . . . . . 16 coeff coeff
87		eqid 2420	. . . . . . . . . . . . . . . 16 coeff coeff
88		eqid 2420	. . . . . . . . . . . . . . . 16 deg deg
89		eqid 2420	. . . . . . . . . . . . . . . 16 deg deg
90	61, 62, 63, 64, 65, 66, 67, 42, 68, 69, 70, 71, 74, 85, 86, 87, 88, 89	plydivlem4 23143	. . . . . . . . . . . . . . 15 $/\$ $/\$ Poly $/\$ Poly $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg Poly $\/$ deg deg
91	90	exp32 608	. . . . . . . . . . . . . 14 $/\$ $/\$ Poly Poly $\/$ deg deg Poly $\/$ deg deg $/\$ deg deg Poly $\/$ deg deg
92	91	ralrimdva 2841	. . . . . . . . . . . . 13 $/\$ Poly $\/$ deg deg Poly $\/$ deg deg Poly $/\$ deg deg Poly $\/$ deg deg
93	59, 92	syl5bi 220	. . . . . . . . . . . 12 $/\$ Poly $\/$ deg deg Poly $\/$ deg deg Poly $/\$ deg deg Poly $\/$ deg deg
94	93	ancld 555	. . . . . . . . . . 11 $/\$ Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg $/\$ Poly $/\$ deg deg Poly $\/$ deg deg
95		dgrcl 23081	. . . . . . . . . . . . . . . . . . . . . 22 Poly deg
96	95	adantl 467	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Poly deg
97	96	nn0zd 11027	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ Poly deg
98	5	ad2antrr 730	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Poly Poly
99	98, 6	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Poly deg
100	99	nn0zd 11027	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ Poly deg
101	97, 100	zsubcld 11034	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ Poly deg deg
102		nn0z 10949	. . . . . . . . . . . . . . . . . . . 20
103	102	ad2antlr 731	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ Poly
104		zleltp1 10976	. . . . . . . . . . . . . . . . . . 19 deg deg $/\$ deg deg deg deg
105	101, 103, 104	syl2anc 665	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ Poly deg deg deg deg
106	101	zred 11029	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ Poly deg deg
107		nn0re 10867	. . . . . . . . . . . . . . . . . . . 20
108	107	ad2antlr 731	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ Poly
109	106, 108	leloed 9767	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ Poly deg deg deg deg $\/$ deg deg
110	105, 109	bitr3d 258	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Poly deg deg deg deg $\/$ deg deg
111	110	orbi2d 706	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Poly $\/$ deg deg $\/$ deg deg $\/$ deg deg
112		pm5.63 932	. . . . . . . . . . . . . . . . . . . 20 $\/$ deg deg $\/$ $/\$ deg deg
113		df-ne 2618	. . . . . . . . . . . . . . . . . . . . . 22
114	113	anbi1i 699	. . . . . . . . . . . . . . . . . . . . 21 $/\$ deg deg $/\$ deg deg
115	114	orbi2i 521	. . . . . . . . . . . . . . . . . . . 20 $\/$ $/\$ deg deg $\/$ $/\$ deg deg
116	112, 115	bitr4i 255	. . . . . . . . . . . . . . . . . . 19 $\/$ deg deg $\/$ $/\$ deg deg
117	116	orbi2i 521	. . . . . . . . . . . . . . . . . 18 deg deg $\/$ $\/$ deg deg deg deg $\/$ $\/$ $/\$ deg deg
118		or12 525	. . . . . . . . . . . . . . . . . 18 $\/$ deg deg $\/$ deg deg deg deg $\/$ $\/$ deg deg
119		or12 525	. . . . . . . . . . . . . . . . . 18 $\/$ deg deg $\/$ $/\$ deg deg deg deg $\/$ $\/$ $/\$ deg deg
120	117, 118, 119	3bitr4i 280	. . . . . . . . . . . . . . . . 17 $\/$ deg deg $\/$ deg deg $\/$ deg deg $\/$ $/\$ deg deg
121		orass 526	. . . . . . . . . . . . . . . . 17 $\/$ deg deg $\/$ $/\$ deg deg $\/$ deg deg $\/$ $/\$ deg deg
122	120, 121	bitr4i 255	. . . . . . . . . . . . . . . 16 $\/$ deg deg $\/$ deg deg $\/$ deg deg $\/$ $/\$ deg deg
123	111, 122	syl6bb 264	. . . . . . . . . . . . . . 15 $/\$ $/\$ Poly $\/$ deg deg $\/$ deg deg $\/$ $/\$ deg deg
124	123	imbi1d 318	. . . . . . . . . . . . . 14 $/\$ $/\$ Poly $\/$ deg deg Poly $\/$ deg deg $\/$ deg deg $\/$ $/\$ deg deg Poly $\/$ deg deg
125		jaob 790	. . . . . . . . . . . . . 14 $\/$ deg deg $\/$ $/\$ deg deg Poly $\/$ deg deg $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg Poly $\/$ deg deg
126	124, 125	syl6bb 264	. . . . . . . . . . . . 13 $/\$ $/\$ Poly $\/$ deg deg Poly $\/$ deg deg $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg Poly $\/$ deg deg
127	126	ralbidva 2859	. . . . . . . . . . . 12 $/\$ Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg Poly $\/$ deg deg
128		r19.26 2953	. . . . . . . . . . . 12 Poly $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg $/\$ Poly $/\$ deg deg Poly $\/$ deg deg
129	127, 128	syl6bb 264	. . . . . . . . . . 11 $/\$ Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg $/\$ Poly $/\$ deg deg Poly $\/$ deg deg
130	94, 129	sylibrd 237	. . . . . . . . . 10 $/\$ Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg
131	130	expcom 436	. . . . . . . . 9 Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg
132	131	a2d 29	. . . . . . . 8 Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg
133	19, 24, 29, 24, 46, 132	nn0ind 11019	. . . . . . 7 Poly $\/$ deg deg Poly $\/$ deg deg
134	14, 133	syl 17	. . . . . 6 Poly $\/$ deg deg Poly $\/$ deg deg
135	134	impcom 431	. . . . 5 $/\$ Poly $\/$ deg deg Poly $\/$ deg deg
136		eqeq1 2424	. . . . . . . 8
137		fveq2 5872	. . . . . . . . . 10 deg deg
138	137	oveq1d 6311	. . . . . . . . 9 deg deg deg deg
139	138	breq1d 4427	. . . . . . . 8 deg deg deg deg
140	136, 139	orbi12d 714	. . . . . . 7 $\/$ deg deg $\/$ deg deg
141		oveq1 6303	. . . . . . . . . . 11
142		plydiv.r	. . . . . . . . . . 11
143	141, 142	syl6eqr 2479	. . . . . . . . . 10
144	143	eqeq1d 2422	. . . . . . . . 9
145	143	fveq2d 5876	. . . . . . . . . 10 deg deg
146	145	breq1d 4427	. . . . . . . . 9 deg deg deg deg
147	144, 146	orbi12d 714	. . . . . . . 8 $\/$ deg deg $\/$ deg deg
148	147	rexbidv 2937	. . . . . . 7 Poly $\/$ deg deg Poly $\/$ deg deg
149	140, 148	imbi12d 321	. . . . . 6 $\/$ deg deg Poly $\/$ deg deg $\/$ deg deg Poly $\/$ deg deg
150	149	rspcv 3175	. . . . 5 Poly Poly $\/$ deg deg Poly $\/$ deg deg $\/$ deg deg Poly $\/$ deg deg
151	13, 135, 150	sylc 62	. . . 4 $/\$ $\/$ deg deg Poly $\/$ deg deg
152	12, 151	syl5 33	. . 3 $/\$ deg deg Poly $\/$ deg deg
153	152	rexlimdva 2915	. 2 deg deg Poly $\/$ deg deg
154	11, 153	mpd 15	1 Poly $\/$ deg deg

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $\/$ wo 369 $/\$ wa 370

wceq 1437

wcel 1867

wne 2616

wral 2773

wrex 2774 class class class wbr 4417

cmpt 4475

cfv 5592 (class class class)co 6296

cof 6534

cc 9526

cr 9527

cc0 9528

c1 9529

caddc 9531

cmul 9533

clt 9664

cle 9665

cmin 9849

cneg 9850

cdiv 10258

cn 10598

cn0 10858

cz 10926

cexp 12258

c0p 22521 Polycply 23032 coeffccoe 23034 degcdgr 23035

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1838 ax-8 1869 ax-9 1871 ax-10 1886 ax-11 1891 ax-12 1904 ax-13 2052 ax-ext 2398 ax-rep 4529 ax-sep 4539 ax-nul 4547 ax-pow 4594 ax-pr 4652 ax-un 6588 ax-inf2 8137 ax-cnex 9584 ax-resscn 9585 ax-1cn 9586 ax-icn 9587 ax-addcl 9588 ax-addrcl 9589 ax-mulcl 9590 ax-mulrcl 9591 ax-mulcom 9592 ax-addass 9593 ax-mulass 9594 ax-distr 9595 ax-i2m1 9596 ax-1ne0 9597 ax-1rid 9598 ax-rnegex 9599 ax-rrecex 9600 ax-cnre 9601 ax-pre-lttri 9602 ax-pre-lttrn 9603 ax-pre-ltadd 9604 ax-pre-mulgt0 9605 ax-pre-sup 9606 ax-addf 9607

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-fal 1443 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2267 df-mo 2268 df-clab 2406 df-cleq 2412 df-clel 2415 df-nfc 2570 df-ne 2618 df-nel 2619 df-ral 2778 df-rex 2779 df-reu 2780 df-rmo 2781 df-rab 2782 df-v 3080 df-sbc 3297 df-csb 3393 df-dif 3436 df-un 3438 df-in 3440 df-ss 3447 df-pss 3449 df-nul 3759 df-if 3907 df-pw 3978 df-sn 3994 df-pr 3996 df-tp 3998 df-op 4000 df-uni 4214 df-int 4250 df-iun 4295 df-br 4418 df-opab 4476 df-mpt 4477 df-tr 4512 df-eprel 4756 df-id 4760 df-po 4766 df-so 4767 df-fr 4804 df-se 4805 df-we 4806 df-xp 4851 df-rel 4852 df-cnv 4853 df-co 4854 df-dm 4855 df-rn 4856 df-res 4857 df-ima 4858 df-pred 5390 df-ord 5436 df-on 5437 df-lim 5438 df-suc 5439 df-iota 5556 df-fun 5594 df-fn 5595 df-f 5596 df-f1 5597 df-fo 5598 df-f1o 5599 df-fv 5600 df-isom 5601 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-of 6536 df-om 6698 df-1st 6798 df-2nd 6799 df-wrecs 7027 df-recs 7089 df-rdg 7127 df-1o 7181 df-oadd 7185 df-er 7362 df-map 7473 df-pm 7474 df-en 7569 df-dom 7570 df-sdom 7571 df-fin 7572 df-sup 7953 df-inf 7954 df-oi 8016 df-card 8363 df-pnf 9666 df-mnf 9667 df-xr 9668 df-ltxr 9669 df-le 9670 df-sub 9851 df-neg 9852 df-div 10259 df-nn 10599 df-2 10657 df-3 10658 df-n0 10859 df-z 10927 df-uz 11149 df-rp 11292 df-fz 11772 df-fzo 11903 df-fl 12014 df-seq 12200 df-exp 12259 df-hash 12502 df-cj 13130 df-re 13131 df-im 13132 df-sqrt 13266 df-abs 13267 df-clim 13519 df-rlim 13520 df-sum 13720 df-0p 22522 df-ply 23036 df-coe 23038 df-dgr 23039

This theorem is referenced by: plydivalg 23146

W3C validator