Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-plylt Structured version   Unicode version

Definition df-plylt 29639
 Description: Define the class of limited-degree polynomials. (Contributed by Stefan O'Rear, 8-Dec-2014.)
Assertion
Ref Expression
df-plylt Poly< Poly deg
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-plylt
StepHypRef Expression
1 cplylt 29637 . 2 Poly<
2 vs . . 3
3 vx . . 3
4 cc 9392 . . . 4
54cpw 3969 . . 3
6 cn0 10691 . . 3
7 vp . . . . . . 7
87cv 1369 . . . . . 6
9 c0p 21281 . . . . . 6
108, 9wceq 1370 . . . . 5
11 cdgr 21789 . . . . . . 7 deg
128, 11cfv 5527 . . . . . 6 deg
133cv 1369 . . . . . 6
14 clt 9530 . . . . . 6
1512, 13, 14wbr 4401 . . . . 5 deg
1610, 15wo 368 . . . 4 deg
172cv 1369 . . . . 5
18 cply 21786 . . . . 5 Poly
1917, 18cfv 5527 . . . 4 Poly
2016, 7, 19crab 2803 . . 3 Poly deg
212, 3, 5, 6, 20cmpt2 6203 . 2 Poly deg
221, 21wceq 1370 1 Poly< Poly deg
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator