Home | Metamath
Proof Explorer Theorem List (p. 240 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mon1pval 23901* | Value of the set of monic polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
Poly1 deg1 Monic1p coe1 | ||
Theorem | ismon1p 23902 | Being a monic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
Poly1 deg1 Monic1p coe1 | ||
Theorem | uc1pcl 23903 | Unitic polynomials are polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
Poly1 Unic1p | ||
Theorem | mon1pcl 23904 | Monic polynomials are polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
Poly1 Monic1p | ||
Theorem | uc1pn0 23905 | Unitic polynomials are not zero. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
Poly1 Unic1p | ||
Theorem | mon1pn0 23906 | Monic polynomials are not zero. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
Poly1 Monic1p | ||
Theorem | uc1pdeg 23907 | Unitic polynomials have nonnegative degrees. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
deg1 Unic1p | ||
Theorem | uc1pldg 23908 | Unitic polynomials have unit leading coefficients. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
deg1 Unit Unic1p coe1 | ||
Theorem | mon1pldg 23909 | Unitic polynomials have one leading coefficients. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
deg1 Monic1p coe1 | ||
Theorem | mon1puc1p 23910 | Monic polynomials are unitic. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
Unic1p Monic1p | ||
Theorem | uc1pmon1p 23911 | Make a unitic polynomial monic by multiplying a factor to normalize the leading coefficient. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
Unic1p Monic1p Poly1 algSc deg1 coe1 | ||
Theorem | deg1submon1p 23912 | The difference of two monic polynomials of the same degree is a polynomial of lesser degree. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
deg1 Monic1p Poly1 | ||
Theorem | q1pval 23913* | Value of the univariate polynomial quotient function. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
quot1p Poly1 deg1 | ||
Theorem | q1peqb 23914 | Characterizing property of the polynomial quotient. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
quot1p Poly1 deg1 Unic1p | ||
Theorem | q1pcl 23915 | Closure of the quotient by a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
quot1p Poly1 Unic1p | ||
Theorem | r1pval 23916 | Value of the polynomial remainder function. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
rem1p Poly1 quot1p | ||
Theorem | r1pcl 23917 | Closure of remainder following division by a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
rem1p Poly1 Unic1p | ||
Theorem | r1pdeglt 23918 | The remainder has a degree smaller than the divisor. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
rem1p Poly1 Unic1p deg1 | ||
Theorem | r1pid 23919 | Express the original polynomial as using the quotient and remainder functions for and . (Contributed by Mario Carneiro, 5-Jun-2015.) |
Poly1 Unic1p quot1p rem1p | ||
Theorem | dvdsq1p 23920 | Divisibility in a polynomial ring is witnessed by the quotient. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
Poly1 r Unic1p quot1p | ||
Theorem | dvdsr1p 23921 | Divisibility in a polynomial ring in terms of the remainder. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
Poly1 r Unic1p rem1p | ||
Theorem | ply1remlem 23922 | A term of the form is linear, monic, and has exactly one zero. (Contributed by Mario Carneiro, 12-Jun-2015.) |
Poly1 var1 algSc eval1 NzRing Monic1p deg1 | ||
Theorem | ply1rem 23923 | The polynomial remainder theorem, or little Bézout's theorem (by contrast to the regular Bézout's theorem bezout 15260). If a polynomial is divided by the linear factor , the remainder is equal to , the evaluation of the polynomial at (interpreted as a constant polynomial). (Contributed by Mario Carneiro, 12-Jun-2015.) |
Poly1 var1 algSc eval1 NzRing rem1p | ||
Theorem | facth1 23924 | The factor theorem and its converse. A polynomial has a root at iff is a factor of . (Contributed by Mario Carneiro, 12-Jun-2015.) |
Poly1 var1 algSc eval1 NzRing r | ||
Theorem | fta1glem1 23925 | Lemma for fta1g 23927. (Contributed by Mario Carneiro, 7-Jun-2016.) |
Poly1 deg1 eval1 IDomn var1 algSc quot1p | ||
Theorem | fta1glem2 23926* | Lemma for fta1g 23927. (Contributed by Mario Carneiro, 12-Jun-2015.) |
Poly1 deg1 eval1 IDomn var1 algSc | ||
Theorem | fta1g 23927 | The one-sided fundamental theorem of algebra. A polynomial of degree has at most roots. Unlike the real fundamental theorem fta 24806, which is only true in and other algebraically closed fields, this is true in any integral domain. (Contributed by Mario Carneiro, 12-Jun-2015.) |
Poly1 deg1 eval1 IDomn | ||
Theorem | fta1blem 23928 | Lemma for fta1b 23929. (Contributed by Mario Carneiro, 14-Jun-2015.) |
Poly1 deg1 eval1 var1 | ||
Theorem | fta1b 23929* | The assumption that be a domain in fta1g 23927 is necessary. Here we show that the statement is strong enough to prove that is a domain. (Contributed by Mario Carneiro, 12-Jun-2015.) |
Poly1 deg1 eval1 IDomn NzRing | ||
Theorem | drnguc1p 23930 | Over a division ring, all nonzero polynomials are unitic. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
Poly1 Unic1p | ||
Theorem | ig1peu 23931* | There is a unique monic polynomial of minimal degree in any nonzero ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Revised by AV, 25-Sep-2020.) |
Poly1 LIdeal Monic1p deg1 inf | ||
Theorem | ig1pval 23932* | Substitutions for the polynomial ideal generator function. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Revised by AV, 25-Sep-2020.) |
Poly1 idlGen1p LIdeal deg1 Monic1p inf | ||
Theorem | ig1pval2 23933 | Generator of the zero ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Proof shortened by AV, 25-Sep-2020.) |
Poly1 idlGen1p | ||
Theorem | ig1pval3 23934 | Characterizing properties of the monic generator of a nonzero ideal of polynomials. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Revised by AV, 25-Sep-2020.) |
Poly1 idlGen1p LIdeal deg1 Monic1p inf | ||
Theorem | ig1pcl 23935 | The monic generator of an ideal is always in the ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Proof shortened by AV, 25-Sep-2020.) |
Poly1 idlGen1p LIdeal | ||
Theorem | ig1pdvds 23936 | The monic generator of an ideal divides all elements of the ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Proof shortened by AV, 25-Sep-2020.) |
Poly1 idlGen1p LIdeal r | ||
Theorem | ig1prsp 23937 | Any ideal of polynomials over a division ring is generated by the ideal's canonical generator. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
Poly1 idlGen1p LIdeal RSpan | ||
Theorem | ply1lpir 23938 | The ring of polynomials over a division ring has the principal ideal property. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
Poly1 LPIR | ||
Theorem | ply1pid 23939 | The polynomials over a field are a PID. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
Poly1 Field PID | ||
Syntax | cply 23940 | Extend class notation to include the set of complex polynomials. |
Poly | ||
Syntax | cidp 23941 | Extend class notation to include the identity polynomial. |
Syntax | ccoe 23942 | Extend class notation to include the coefficient function on polynomials. |
coeff | ||
Syntax | cdgr 23943 | Extend class notation to include the degree function on polynomials. |
deg | ||
Definition | df-ply 23944* | Define the set of polynomials on the complex numbers with coefficients in the given subset. (Contributed by Mario Carneiro, 17-Jul-2014.) |
Poly | ||
Definition | df-idp 23945 | Define the identity polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.) |
Definition | df-coe 23946* | Define the coefficient function for a polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.) |
coeff Poly | ||
Definition | df-dgr 23947 | Define the degree of a polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.) |
deg Poly coeff | ||
Theorem | plyco0 23948* | Two ways to say that a function on the nonnegative integers has finite support. (Contributed by Mario Carneiro, 22-Jul-2014.) |
Theorem | plyval 23949* | Value of the polynomial set function. (Contributed by Mario Carneiro, 17-Jul-2014.) |
Poly | ||
Theorem | plybss 23950 | Reverse closure of the parameter of the polynomial set function. (Contributed by Mario Carneiro, 22-Jul-2014.) |
Poly | ||
Theorem | elply 23951* | Definition of a polynomial with coefficients in . (Contributed by Mario Carneiro, 17-Jul-2014.) |
Poly | ||
Theorem | elply2 23952* | The coefficient function can be assumed to have zeroes outside . (Contributed by Mario Carneiro, 20-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
Poly | ||
Theorem | plyun0 23953 | The set of polynomials is unaffected by the addition of zero. (This is built into the definition because all higher powers of a polynomial are effectively zero, so we require that the coefficient field contain zero to simplify some of our closure theorems.) (Contributed by Mario Carneiro, 17-Jul-2014.) |
Poly Poly | ||
Theorem | plyf 23954 | The polynomial is a function on the complex numbers. (Contributed by Mario Carneiro, 22-Jul-2014.) |
Poly | ||
Theorem | plyss 23955 | The polynomial set function preserves the subset relation. (Contributed by Mario Carneiro, 17-Jul-2014.) |
Poly Poly | ||
Theorem | plyssc 23956 | Every polynomial ring is contained in the ring of polynomials over . (Contributed by Mario Carneiro, 22-Jul-2014.) |
Poly Poly | ||
Theorem | elplyr 23957* | Sufficient condition for elementhood in the set of polynomials. (Contributed by Mario Carneiro, 17-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
Poly | ||
Theorem | elplyd 23958* | Sufficient condition for elementhood in the set of polynomials. (Contributed by Mario Carneiro, 17-Jul-2014.) |
Poly | ||
Theorem | ply1termlem 23959* | Lemma for ply1term 23960. (Contributed by Mario Carneiro, 26-Jul-2014.) |
Theorem | ply1term 23960* | A one-term polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.) |
Poly | ||
Theorem | plypow 23961* | A power is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.) |
Poly | ||
Theorem | plyconst 23962 | A constant function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.) |
Poly | ||
Theorem | ne0p 23963 | A test to show that a polynomial is nonzero. (Contributed by Mario Carneiro, 23-Jul-2014.) |
Theorem | ply0 23964 | The zero function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.) |
Poly | ||
Theorem | plyid 23965 | The identity function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014.) |
Poly | ||
Theorem | plyeq0lem 23966* | Lemma for plyeq0 23967. If is the coefficient function for a nonzero polynomial such that for every and is the nonzero leading coefficient, then the function is a sum of powers of , and so the limit of this function as is the constant term, . But everywhere, so this limit is also equal to zero so that , a contradiction. (Contributed by Mario Carneiro, 22-Jul-2014.) |
Theorem | plyeq0 23967* | If a polynomial is zero at every point (or even just zero at the positive integers), then all the coefficients must be zero. This is the basis for the method of equating coefficients of equal polynomials, and ensures that df-coe 23946 is well-defined. (Contributed by Mario Carneiro, 22-Jul-2014.) |
Theorem | plypf1 23968 | Write the set of complex polynomials in a subring in terms of the abstract polynomial construction. (Contributed by Mario Carneiro, 3-Jul-2015.) (Proof shortened by AV, 29-Sep-2019.) |
ℂfld ↾s Poly1 eval1ℂfld SubRingℂfld Poly | ||
Theorem | plyaddlem1 23969* | Derive the coefficient function for the sum of two polynomials. (Contributed by Mario Carneiro, 23-Jul-2014.) |
Poly Poly | ||
Theorem | plymullem1 23970* | Derive the coefficient function for the product of two polynomials. (Contributed by Mario Carneiro, 23-Jul-2014.) |
Poly Poly | ||
Theorem | plyaddlem 23971* | Lemma for plyadd 23973. (Contributed by Mario Carneiro, 21-Jul-2014.) |
Poly Poly Poly | ||
Theorem | plymullem 23972* | Lemma for plymul 23974. (Contributed by Mario Carneiro, 21-Jul-2014.) |
Poly Poly Poly | ||
Theorem | plyadd 23973* | The sum of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014.) |
Poly Poly Poly | ||
Theorem | plymul 23974* | The product of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014.) |
Poly Poly Poly | ||
Theorem | plysub 23975* | The difference of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014.) |
Poly Poly Poly | ||
Theorem | plyaddcl 23976 | The sum of two polynomials is a polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.) |
Poly Poly Poly | ||
Theorem | plymulcl 23977 | The product of two polynomials is a polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.) |
Poly Poly Poly | ||
Theorem | plysubcl 23978 | The difference of two polynomials is a polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.) |
Poly Poly Poly | ||
Theorem | coeval 23979* | Value of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.) |
Poly coeff | ||
Theorem | coeeulem 23980* | Lemma for coeeu 23981. (Contributed by Mario Carneiro, 22-Jul-2014.) |
Poly | ||
Theorem | coeeu 23981* | Uniqueness of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
Poly | ||
Theorem | coelem 23982* | Lemma for properties of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
Poly coeff coeff coeff | ||
Theorem | coeeq 23983* | If satisfies the properties of the coefficient function, it must be equal to the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
Poly coeff | ||
Theorem | dgrval 23984 | Value of the degree function. (Contributed by Mario Carneiro, 22-Jul-2014.) |
coeff Poly deg | ||
Theorem | dgrlem 23985* | Lemma for dgrcl 23989 and similar theorems. (Contributed by Mario Carneiro, 22-Jul-2014.) |
coeff Poly | ||
Theorem | coef 23986 | The domain and range of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.) |
coeff Poly | ||
Theorem | coef2 23987 | The domain and range of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.) |
coeff Poly | ||
Theorem | coef3 23988 | The domain and range of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014.) |
coeff Poly | ||
Theorem | dgrcl 23989 | The degree of any polynomial is a nonnegative integer. (Contributed by Mario Carneiro, 22-Jul-2014.) |
Poly deg | ||
Theorem | dgrub 23990 | If the -th coefficient of is nonzero, then the degree of is at least . (Contributed by Mario Carneiro, 22-Jul-2014.) |
coeff deg Poly | ||
Theorem | dgrub2 23991 | All the coefficients above the degree of are zero. (Contributed by Mario Carneiro, 23-Jul-2014.) |
coeff deg Poly | ||
Theorem | dgrlb 23992 | If all the coefficients above are zero, then the degree of is at most . (Contributed by Mario Carneiro, 22-Jul-2014.) |
coeff deg Poly | ||
Theorem | coeidlem 23993* | Lemma for coeid 23994. (Contributed by Mario Carneiro, 22-Jul-2014.) |
coeff deg Poly | ||
Theorem | coeid 23994* | Reconstruct a polynomial as an explicit sum of the coefficient function up to the degree of the polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.) |
coeff deg Poly | ||
Theorem | coeid2 23995* | Reconstruct a polynomial as an explicit sum of the coefficient function up to the degree of the polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.) |
coeff deg Poly | ||
Theorem | coeid3 23996* | Reconstruct a polynomial as an explicit sum of the coefficient function up to at least the degree of the polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.) |
coeff deg Poly | ||
Theorem | plyco 23997* | The composition of two polynomials is a polynomial. (Contributed by Mario Carneiro, 23-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
Poly Poly Poly | ||
Theorem | coeeq2 23998* | Compute the coefficient function given a sum expression for the polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.) |
Poly coeff | ||
Theorem | dgrle 23999* | Given an explicit expression for a polynomial, the degree is at most the highest term in the sum. (Contributed by Mario Carneiro, 24-Jul-2014.) |
Poly deg | ||
Theorem | dgreq 24000* | If the highest term in a polynomial expression is nonzero, then the polynomial's degree is completely determined. (Contributed by Mario Carneiro, 24-Jul-2014.) |
Poly deg |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |