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

Definition df-r1p 21490
 Description: Define the remainder after dividing two univariate polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.)
Assertion
Ref Expression
df-r1p rem1p Poly1 Poly1quot1pPoly1
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-r1p
StepHypRef Expression
1 cr1p 21485 . 2 rem1p
2 vr . . 3
3 cvv 2962 . . 3
4 vb . . . 4
52cv 1361 . . . . . 6
6 cpl1 17528 . . . . . 6 Poly1
75, 6cfv 5406 . . . . 5 Poly1
8 cbs 14157 . . . . 5
97, 8cfv 5406 . . . 4 Poly1
10 vf . . . . 5
11 vg . . . . 5
124cv 1361 . . . . 5
1310cv 1361 . . . . . 6
1411cv 1361 . . . . . . . 8
15 cq1p 21484 . . . . . . . . 9 quot1p
165, 15cfv 5406 . . . . . . . 8 quot1p
1713, 14, 16co 6080 . . . . . . 7 quot1p
18 cmulr 14222 . . . . . . . 8
197, 18cfv 5406 . . . . . . 7 Poly1
2017, 14, 19co 6080 . . . . . 6 quot1pPoly1
21 csg 15396 . . . . . . 7
227, 21cfv 5406 . . . . . 6 Poly1
2313, 20, 22co 6080 . . . . 5 Poly1quot1pPoly1
2410, 11, 12, 12, 23cmpt2 6082 . . . 4 Poly1quot1pPoly1
254, 9, 24csb 3276 . . 3 Poly1 Poly1quot1pPoly1
262, 3, 25cmpt 4338 . 2 Poly1 Poly1quot1pPoly1
271, 26wceq 1362 1 rem1p Poly1 Poly1quot1pPoly1
 Colors of variables: wff setvar class This definition is referenced by:  r1pval  21513
 Copyright terms: Public domain W3C validator