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

Definition df-q1p 20055
 Description: Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 20060. We actually use the reversed version for better harmony with our divisibility df-dvdsr 15746. (Contributed by Stefan O'Rear, 28-Mar-2015.)
Assertion
Ref Expression
df-q1p quot1p Poly1 deg1 deg1
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-q1p
StepHypRef Expression
1 cq1p 20050 . 2 quot1p
2 vr . . 3
3 cvv 2956 . . 3
4 vp . . . 4
52cv 1651 . . . . 5
6 cpl1 16571 . . . . 5 Poly1
75, 6cfv 5454 . . . 4 Poly1
8 vb . . . . 5
94cv 1651 . . . . . 6
10 cbs 13469 . . . . . 6
119, 10cfv 5454 . . . . 5
12 vf . . . . . 6
13 vg . . . . . 6
148cv 1651 . . . . . 6
1512cv 1651 . . . . . . . . . 10
16 vq . . . . . . . . . . . 12
1716cv 1651 . . . . . . . . . . 11
1813cv 1651 . . . . . . . . . . 11
19 cmulr 13530 . . . . . . . . . . . 12
209, 19cfv 5454 . . . . . . . . . . 11
2117, 18, 20co 6081 . . . . . . . . . 10
22 csg 14688 . . . . . . . . . . 11
239, 22cfv 5454 . . . . . . . . . 10
2415, 21, 23co 6081 . . . . . . . . 9
25 cdg1 19977 . . . . . . . . . 10 deg1
265, 25cfv 5454 . . . . . . . . 9 deg1
2724, 26cfv 5454 . . . . . . . 8 deg1
2818, 26cfv 5454 . . . . . . . 8 deg1
29 clt 9120 . . . . . . . 8
3027, 28, 29wbr 4212 . . . . . . 7 deg1 deg1
3130, 16, 14crio 6542 . . . . . 6 deg1 deg1
3212, 13, 14, 14, 31cmpt2 6083 . . . . 5 deg1 deg1
338, 11, 32csb 3251 . . . 4 deg1 deg1
344, 7, 33csb 3251 . . 3 Poly1 deg1 deg1
352, 3, 34cmpt 4266 . 2 Poly1 deg1 deg1
361, 35wceq 1652 1 quot1p Poly1 deg1 deg1
 Colors of variables: wff set class This definition is referenced by:  q1pval  20076
 Copyright terms: Public domain W3C validator