Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-uc1p | Structured version Visualization version Unicode version |
Description: Define the set of unitic univariate polynomials, as the polynomials with an invertible leading coefficient. This is not a standard concept but is useful to us as the set of polynomials which can be used as the divisor in the polynomial division theorem ply1divalg 23897. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
Ref | Expression |
---|---|
df-uc1p | Unic1p Poly1 Poly1 coe1 deg1 Unit |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cuc1p 23886 | . 2 Unic1p | |
2 | vr | . . 3 | |
3 | cvv 3200 | . . 3 | |
4 | vf | . . . . . . 7 | |
5 | 4 | cv 1482 | . . . . . 6 |
6 | 2 | cv 1482 | . . . . . . . 8 |
7 | cpl1 19547 | . . . . . . . 8 Poly1 | |
8 | 6, 7 | cfv 5888 | . . . . . . 7 Poly1 |
9 | c0g 16100 | . . . . . . 7 | |
10 | 8, 9 | cfv 5888 | . . . . . 6 Poly1 |
11 | 5, 10 | wne 2794 | . . . . 5 Poly1 |
12 | cdg1 23814 | . . . . . . . . 9 deg1 | |
13 | 6, 12 | cfv 5888 | . . . . . . . 8 deg1 |
14 | 5, 13 | cfv 5888 | . . . . . . 7 deg1 |
15 | cco1 19548 | . . . . . . . 8 coe1 | |
16 | 5, 15 | cfv 5888 | . . . . . . 7 coe1 |
17 | 14, 16 | cfv 5888 | . . . . . 6 coe1 deg1 |
18 | cui 18639 | . . . . . . 7 Unit | |
19 | 6, 18 | cfv 5888 | . . . . . 6 Unit |
20 | 17, 19 | wcel 1990 | . . . . 5 coe1 deg1 Unit |
21 | 11, 20 | wa 384 | . . . 4 Poly1 coe1 deg1 Unit |
22 | cbs 15857 | . . . . 5 | |
23 | 8, 22 | cfv 5888 | . . . 4 Poly1 |
24 | 21, 4, 23 | crab 2916 | . . 3 Poly1 Poly1 coe1 deg1 Unit |
25 | 2, 3, 24 | cmpt 4729 | . 2 Poly1 Poly1 coe1 deg1 Unit |
26 | 1, 25 | wceq 1483 | 1 Unic1p Poly1 Poly1 coe1 deg1 Unit |
Colors of variables: wff setvar class |
This definition is referenced by: uc1pval 23899 |
Copyright terms: Public domain | W3C validator |