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

Definition df-quot 22414
 Description: Define the quotient function on polynomials. This is the of the expression in the division algorithm. (Contributed by Mario Carneiro, 23-Jul-2014.)
Assertion
Ref Expression
df-quot quot Poly Poly Poly deg deg
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-quot
StepHypRef Expression
1 cquot 22413 . 2 quot
2 vf . . 3
3 vg . . 3
4 cc 9479 . . . 4
5 cply 22309 . . . 4 Poly
64, 5cfv 5579 . . 3 Poly
7 c0p 21804 . . . . 5
87csn 4020 . . . 4
96, 8cdif 3466 . . 3 Poly
10 vr . . . . . . . 8
1110cv 1373 . . . . . . 7
1211, 7wceq 1374 . . . . . 6
13 cdgr 22312 . . . . . . . 8 deg
1411, 13cfv 5579 . . . . . . 7 deg
153cv 1373 . . . . . . . 8
1615, 13cfv 5579 . . . . . . 7 deg
17 clt 9617 . . . . . . 7
1814, 16, 17wbr 4440 . . . . . 6 deg deg
1912, 18wo 368 . . . . 5 deg deg
202cv 1373 . . . . . 6
21 vq . . . . . . . 8
2221cv 1373 . . . . . . 7
23 cmul 9486 . . . . . . . 8
2423cof 6513 . . . . . . 7
2515, 22, 24co 6275 . . . . . 6
26 cmin 9794 . . . . . . 7
2726cof 6513 . . . . . 6
2820, 25, 27co 6275 . . . . 5
2919, 10, 28wsbc 3324 . . . 4 deg deg
3029, 21, 6crio 6235 . . 3 Poly deg deg
312, 3, 6, 9, 30cmpt2 6277 . 2 Poly Poly Poly deg deg
321, 31wceq 1374 1 quot Poly Poly Poly deg deg
 Colors of variables: wff setvar class This definition is referenced by:  quotval  22415
 Copyright terms: Public domain W3C validator