plydivex - Metamath Proof Explorer

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

Theorem plydivex 23243

Description: Lemma for plydivalg 23245. (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 23180	. . . . . 6 Poly deg
3	1, 2	syl 17	. . . . 5 deg
4	3	nn0red 10923	. . . 4 deg
5		plydiv.g	. . . . . 6 Poly
6		dgrcl 23180	. . . . . 6 Poly deg
7	5, 6	syl 17	. . . . 5 deg
8	7	nn0red 10923	. . . 4 deg
9	4, 8	resubcld 10044	. . 3 deg deg
10		arch 10863	. . 3 deg deg deg deg
11	9, 10	syl 17	. 2 deg deg
12		olc 386	. . . 4 deg deg $\/$ deg deg
13	1	adantr 467	. . . . 5 $/\$ Poly
14		nnnn0 10873	. . . . . . 7
15		breq2 4405	. . . . . . . . . . . 12 deg deg deg deg
16	15	orbi2d 707	. . . . . . . . . . 11 $\/$ deg deg $\/$ deg deg
17	16	imbi1d 319	. . . . . . . . . 10 $\/$ deg deg Poly $\/$ deg deg $\/$ deg deg Poly $\/$ deg deg
18	17	ralbidv 2826	. . . . . . . . 9 Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg
19	18	imbi2d 318	. . . . . . . 8 Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg
20		breq2 4405	. . . . . . . . . . . 12 deg deg deg deg
21	20	orbi2d 707	. . . . . . . . . . 11 $\/$ deg deg $\/$ deg deg
22	21	imbi1d 319	. . . . . . . . . 10 $\/$ deg deg Poly $\/$ deg deg $\/$ deg deg Poly $\/$ deg deg
23	22	ralbidv 2826	. . . . . . . . 9 Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg
24	23	imbi2d 318	. . . . . . . 8 Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg
25		breq2 4405	. . . . . . . . . . . 12 deg deg deg deg
26	25	orbi2d 707	. . . . . . . . . . 11 $\/$ deg deg $\/$ deg deg
27	26	imbi1d 319	. . . . . . . . . 10 $\/$ deg deg Poly $\/$ deg deg $\/$ deg deg Poly $\/$ deg deg
28	27	ralbidv 2826	. . . . . . . . 9 Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg
29	28	imbi2d 318	. . . . . . . 8 Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg
30		plydiv.pl	. . . . . . . . . . . 12 $/\$ $/\$
31	30	adantlr 720	. . . . . . . . . . 11 $/\$ Poly $/\$ $\/$ deg deg $/\$ $/\$
32		plydiv.tm	. . . . . . . . . . . 12 $/\$ $/\$
33	32	adantlr 720	. . . . . . . . . . 11 $/\$ Poly $/\$ $\/$ deg deg $/\$ $/\$
34		plydiv.rc	. . . . . . . . . . . 12 $/\$ $/\$
35	34	adantlr 720	. . . . . . . . . . 11 $/\$ Poly $/\$ $\/$ deg deg $/\$ $/\$
36		plydiv.m1	. . . . . . . . . . . 12
37	36	adantr 467	. . . . . . . . . . 11 $/\$ Poly $/\$ $\/$ deg deg
38		simprl 763	. . . . . . . . . . 11 $/\$ Poly $/\$ $\/$ deg deg Poly
39	5	adantr 467	. . . . . . . . . . 11 $/\$ Poly $/\$ $\/$ deg deg Poly
40		plydiv.z	. . . . . . . . . . . 12
41	40	adantr 467	. . . . . . . . . . 11 $/\$ Poly $/\$ $\/$ deg deg
42		eqid 2450	. . . . . . . . . . 11
43		simprr 765	. . . . . . . . . . 11 $/\$ Poly $/\$ $\/$ deg deg $\/$ deg deg
44	31, 33, 35, 37, 38, 39, 41, 42, 43	plydivlem3 23241	. . . . . . . . . 10 $/\$ Poly $/\$ $\/$ deg deg Poly $\/$ deg deg
45	44	expr 619	. . . . . . . . 9 $/\$ Poly $\/$ deg deg Poly $\/$ deg deg
46	45	ralrimiva 2801	. . . . . . . 8 Poly $\/$ deg deg Poly $\/$ deg deg
47		eqeq1 2454	. . . . . . . . . . . . . . . 16
48		fveq2 5863	. . . . . . . . . . . . . . . . . 18 deg deg
49	48	oveq1d 6303	. . . . . . . . . . . . . . . . 17 deg deg deg deg
50	49	breq1d 4411	. . . . . . . . . . . . . . . 16 deg deg deg deg
51	47, 50	orbi12d 715	. . . . . . . . . . . . . . 15 $\/$ deg deg $\/$ deg deg
52		oveq1 6295	. . . . . . . . . . . . . . . . . 18
53	52	eqeq1d 2452	. . . . . . . . . . . . . . . . 17
54	52	fveq2d 5867	. . . . . . . . . . . . . . . . . 18 deg deg
55	54	breq1d 4411	. . . . . . . . . . . . . . . . 17 deg deg deg deg
56	53, 55	orbi12d 715	. . . . . . . . . . . . . . . 16 $\/$ deg deg $\/$ deg deg
57	56	rexbidv 2900	. . . . . . . . . . . . . . 15 Poly $\/$ deg deg Poly $\/$ deg deg
58	51, 57	imbi12d 322	. . . . . . . . . . . . . 14 $\/$ deg deg Poly $\/$ deg deg $\/$ deg deg Poly $\/$ deg deg
59	58	cbvralv 3018	. . . . . . . . . . . . 13 Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg
60		simplll 767	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Poly $/\$ Poly $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg
61	60, 30	sylan 474	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Poly $/\$ Poly $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg $/\$ $/\$
62	60, 32	sylan 474	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Poly $/\$ Poly $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg $/\$ $/\$
63	60, 34	sylan 474	. . . . . . . . . . . . . . . 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 761	. . . . . . . . . . . . . . . 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 768	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Poly $/\$ Poly $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg
69		simprrr 774	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Poly $/\$ Poly $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg deg deg
70		simprrl 773	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Poly $/\$ Poly $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg
71		eqid 2450	. . . . . . . . . . . . . . . 16
72		oveq1 6295	. . . . . . . . . . . . . . . . . 18
73	72	oveq2d 6304	. . . . . . . . . . . . . . . . 17 coeffdeg coeffdeg coeffdeg coeffdeg
74	73	cbvmptv 4494	. . . . . . . . . . . . . . . 16 coeffdeg coeffdeg coeffdeg coeffdeg
75		simprl 763	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Poly $/\$ Poly $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg
76		oveq2 6296	. . . . . . . . . . . . . . . . . . . . . . 23
77	76	oveq2d 6304	. . . . . . . . . . . . . . . . . . . . . 22
78	77	eqeq1d 2452	. . . . . . . . . . . . . . . . . . . . 21
79	77	fveq2d 5867	. . . . . . . . . . . . . . . . . . . . . 22 deg deg
80	79	breq1d 4411	. . . . . . . . . . . . . . . . . . . . 21 deg deg deg deg
81	78, 80	orbi12d 715	. . . . . . . . . . . . . . . . . . . 20 $\/$ deg deg $\/$ deg deg
82	81	cbvrexv 3019	. . . . . . . . . . . . . . . . . . 19 Poly $\/$ deg deg Poly $\/$ deg deg
83	82	imbi2i 314	. . . . . . . . . . . . . . . . . 18 $\/$ deg deg Poly $\/$ deg deg $\/$ deg deg Poly $\/$ deg deg
84	83	ralbii 2818	. . . . . . . . . . . . . . . . 17 Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg
85	75, 84	sylib 200	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Poly $/\$ Poly $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg
86		eqid 2450	. . . . . . . . . . . . . . . 16 coeff coeff
87		eqid 2450	. . . . . . . . . . . . . . . 16 coeff coeff
88		eqid 2450	. . . . . . . . . . . . . . . 16 deg deg
89		eqid 2450	. . . . . . . . . . . . . . . 16 deg deg
90	61, 62, 63, 64, 65, 66, 67, 42, 68, 69, 70, 71, 74, 85, 86, 87, 88, 89	plydivlem4 23242	. . . . . . . . . . . . . . 15 $/\$ $/\$ Poly $/\$ Poly $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg Poly $\/$ deg deg
91	90	exp32 609	. . . . . . . . . . . . . 14 $/\$ $/\$ Poly Poly $\/$ deg deg Poly $\/$ deg deg $/\$ deg deg Poly $\/$ deg deg
92	91	ralrimdva 2805	. . . . . . . . . . . . 13 $/\$ Poly $\/$ deg deg Poly $\/$ deg deg Poly $/\$ deg deg Poly $\/$ deg deg
93	59, 92	syl5bi 221	. . . . . . . . . . . 12 $/\$ Poly $\/$ deg deg Poly $\/$ deg deg Poly $/\$ deg deg Poly $\/$ deg deg
94	93	ancld 556	. . . . . . . . . . 11 $/\$ Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg $/\$ Poly $/\$ deg deg Poly $\/$ deg deg
95		dgrcl 23180	. . . . . . . . . . . . . . . . . . . . . 22 Poly deg
96	95	adantl 468	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Poly deg
97	96	nn0zd 11035	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ Poly deg
98	5	ad2antrr 731	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Poly Poly
99	98, 6	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Poly deg
100	99	nn0zd 11035	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ Poly deg
101	97, 100	zsubcld 11042	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ Poly deg deg
102		nn0z 10957	. . . . . . . . . . . . . . . . . . . 20
103	102	ad2antlr 732	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ Poly
104		zleltp1 10984	. . . . . . . . . . . . . . . . . . 19 deg deg $/\$ deg deg deg deg
105	101, 103, 104	syl2anc 666	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ Poly deg deg deg deg
106	101	zred 11037	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ Poly deg deg
107		nn0re 10875	. . . . . . . . . . . . . . . . . . . 20
108	107	ad2antlr 732	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ Poly
109	106, 108	leloed 9775	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ Poly deg deg deg deg $\/$ deg deg
110	105, 109	bitr3d 259	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Poly deg deg deg deg $\/$ deg deg
111	110	orbi2d 707	. . . . . . . . . . . . . . . 16 $/\$ $/\$ Poly $\/$ deg deg $\/$ deg deg $\/$ deg deg
112		pm5.63 934	. . . . . . . . . . . . . . . . . . . 20 $\/$ deg deg $\/$ $/\$ deg deg
113		df-ne 2623	. . . . . . . . . . . . . . . . . . . . . 22
114	113	anbi1i 700	. . . . . . . . . . . . . . . . . . . . 21 $/\$ deg deg $/\$ deg deg
115	114	orbi2i 522	. . . . . . . . . . . . . . . . . . . 20 $\/$ $/\$ deg deg $\/$ $/\$ deg deg
116	112, 115	bitr4i 256	. . . . . . . . . . . . . . . . . . 19 $\/$ deg deg $\/$ $/\$ deg deg
117	116	orbi2i 522	. . . . . . . . . . . . . . . . . 18 deg deg $\/$ $\/$ deg deg deg deg $\/$ $\/$ $/\$ deg deg
118		or12 526	. . . . . . . . . . . . . . . . . 18 $\/$ deg deg $\/$ deg deg deg deg $\/$ $\/$ deg deg
119		or12 526	. . . . . . . . . . . . . . . . . 18 $\/$ deg deg $\/$ $/\$ deg deg deg deg $\/$ $\/$ $/\$ deg deg
120	117, 118, 119	3bitr4i 281	. . . . . . . . . . . . . . . . 17 $\/$ deg deg $\/$ deg deg $\/$ deg deg $\/$ $/\$ deg deg
121		orass 527	. . . . . . . . . . . . . . . . 17 $\/$ deg deg $\/$ $/\$ deg deg $\/$ deg deg $\/$ $/\$ deg deg
122	120, 121	bitr4i 256	. . . . . . . . . . . . . . . 16 $\/$ deg deg $\/$ deg deg $\/$ deg deg $\/$ $/\$ deg deg
123	111, 122	syl6bb 265	. . . . . . . . . . . . . . 15 $/\$ $/\$ Poly $\/$ deg deg $\/$ deg deg $\/$ $/\$ deg deg
124	123	imbi1d 319	. . . . . . . . . . . . . 14 $/\$ $/\$ Poly $\/$ deg deg Poly $\/$ deg deg $\/$ deg deg $\/$ $/\$ deg deg Poly $\/$ deg deg
125		jaob 791	. . . . . . . . . . . . . 14 $\/$ deg deg $\/$ $/\$ deg deg Poly $\/$ deg deg $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg Poly $\/$ deg deg
126	124, 125	syl6bb 265	. . . . . . . . . . . . 13 $/\$ $/\$ Poly $\/$ deg deg Poly $\/$ deg deg $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg Poly $\/$ deg deg
127	126	ralbidva 2823	. . . . . . . . . . . 12 $/\$ Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg $/\$ $/\$ deg deg Poly $\/$ deg deg
128		r19.26 2916	. . . . . . . . . . . 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 265	. . . . . . . . . . 11 $/\$ Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg $/\$ Poly $/\$ deg deg Poly $\/$ deg deg
130	94, 129	sylibrd 238	. . . . . . . . . 10 $/\$ Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg Poly $\/$ deg deg
131	130	expcom 437	. . . . . . . . 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 11027	. . . . . . 7 Poly $\/$ deg deg Poly $\/$ deg deg
134	14, 133	syl 17	. . . . . 6 Poly $\/$ deg deg Poly $\/$ deg deg
135	134	impcom 432	. . . . 5 $/\$ Poly $\/$ deg deg Poly $\/$ deg deg
136		eqeq1 2454	. . . . . . . 8
137		fveq2 5863	. . . . . . . . . 10 deg deg
138	137	oveq1d 6303	. . . . . . . . 9 deg deg deg deg
139	138	breq1d 4411	. . . . . . . 8 deg deg deg deg
140	136, 139	orbi12d 715	. . . . . . 7 $\/$ deg deg $\/$ deg deg
141		oveq1 6295	. . . . . . . . . . 11
142		plydiv.r	. . . . . . . . . . 11
143	141, 142	syl6eqr 2502	. . . . . . . . . 10
144	143	eqeq1d 2452	. . . . . . . . 9
145	143	fveq2d 5867	. . . . . . . . . 10 deg deg
146	145	breq1d 4411	. . . . . . . . 9 deg deg deg deg
147	144, 146	orbi12d 715	. . . . . . . 8 $\/$ deg deg $\/$ deg deg
148	147	rexbidv 2900	. . . . . . 7 Poly $\/$ deg deg Poly $\/$ deg deg
149	140, 148	imbi12d 322	. . . . . 6 $\/$ deg deg Poly $\/$ deg deg $\/$ deg deg Poly $\/$ deg deg
150	149	rspcv 3145	. . . . 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 2878	. 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 188 $\/$ wo 370 $/\$ wa 371

wceq 1443

wcel 1886

wne 2621

wral 2736

wrex 2737 class class class wbr 4401

cmpt 4460

cfv 5581 (class class class)co 6288

cof 6526

cc 9534

cr 9535

cc0 9536

c1 9537

caddc 9539

cmul 9541

clt 9672

cle 9673

cmin 9857

cneg 9858

cdiv 10266

cn 10606

cn0 10866

cz 10934

cexp 12269

c0p 22620 Polycply 23131 coeffccoe 23133 degcdgr 23134

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-rep 4514 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580 ax-inf2 8143 ax-cnex 9592 ax-resscn 9593 ax-1cn 9594 ax-icn 9595 ax-addcl 9596 ax-addrcl 9597 ax-mulcl 9598 ax-mulrcl 9599 ax-mulcom 9600 ax-addass 9601 ax-mulass 9602 ax-distr 9603 ax-i2m1 9604 ax-1ne0 9605 ax-1rid 9606 ax-rnegex 9607 ax-rrecex 9608 ax-cnre 9609 ax-pre-lttri 9610 ax-pre-lttrn 9611 ax-pre-ltadd 9612 ax-pre-mulgt0 9613 ax-pre-sup 9614 ax-addf 9615

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 985 df-3an 986 df-tru 1446 df-fal 1449 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-pss 3419 df-nul 3731 df-if 3881 df-pw 3952 df-sn 3968 df-pr 3970 df-tp 3972 df-op 3974 df-uni 4198 df-int 4234 df-iun 4279 df-br 4402 df-opab 4461 df-mpt 4462 df-tr 4497 df-eprel 4744 df-id 4748 df-po 4754 df-so 4755 df-fr 4792 df-se 4793 df-we 4794 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-res 4845 df-ima 4846 df-pred 5379 df-ord 5425 df-on 5426 df-lim 5427 df-suc 5428 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-isom 5590 df-riota 6250 df-ov 6291 df-oprab 6292 df-mpt2 6293 df-of 6528 df-om 6690 df-1st 6790 df-2nd 6791 df-wrecs 7025 df-recs 7087 df-rdg 7125 df-1o 7179 df-oadd 7183 df-er 7360 df-map 7471 df-pm 7472 df-en 7567 df-dom 7568 df-sdom 7569 df-fin 7570 df-sup 7953 df-inf 7954 df-oi 8022 df-card 8370 df-pnf 9674 df-mnf 9675 df-xr 9676 df-ltxr 9677 df-le 9678 df-sub 9859 df-neg 9860 df-div 10267 df-nn 10607 df-2 10665 df-3 10666 df-n0 10867 df-z 10935 df-uz 11157 df-rp 11300 df-fz 11782 df-fzo 11913 df-fl 12025 df-seq 12211 df-exp 12270 df-hash 12513 df-cj 13155 df-re 13156 df-im 13157 df-sqrt 13291 df-abs 13292 df-clim 13545 df-rlim 13546 df-sum 13746 df-0p 22621 df-ply 23135 df-coe 23137 df-dgr 23138

This theorem is referenced by: plydivalg 23245

W3C validator