![]() |
Metamath
Proof Explorer Theorem List (p. 261 of 480) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | coemul 26001* | A coefficient of a product of polynomials. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ π΄ = (coeffβπΉ) & β’ π΅ = (coeffβπΊ) β β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π β β0) β ((coeffβ(πΉ βf Β· πΊ))βπ) = Ξ£π β (0...π)((π΄βπ) Β· (π΅β(π β π)))) | ||
Theorem | coe11 26002 | The coefficient function is one-to-one, so if the coefficients are equal then the functions are equal and vice-versa. (Contributed by Mario Carneiro, 24-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ π΄ = (coeffβπΉ) & β’ π΅ = (coeffβπΊ) β β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (πΉ = πΊ β π΄ = π΅)) | ||
Theorem | coemulhi 26003 | The leading coefficient of a product of polynomials. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ π΄ = (coeffβπΉ) & β’ π΅ = (coeffβπΊ) & β’ π = (degβπΉ) & β’ π = (degβπΊ) β β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β ((coeffβ(πΉ βf Β· πΊ))β(π + π)) = ((π΄βπ) Β· (π΅βπ))) | ||
Theorem | coemulc 26004 | The coefficient function is linear under scalar multiplication. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ ((π΄ β β β§ πΉ β (Polyβπ)) β (coeffβ((β Γ {π΄}) βf Β· πΉ)) = ((β0 Γ {π΄}) βf Β· (coeffβπΉ))) | ||
Theorem | coe0 26005 | The coefficients of the zero polynomial are zero. (Contributed by Mario Carneiro, 22-Jul-2014.) |
β’ (coeffβ0π) = (β0 Γ {0}) | ||
Theorem | coesub 26006 | The coefficient function of a sum is the sum of coefficients. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ π΄ = (coeffβπΉ) & β’ π΅ = (coeffβπΊ) β β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (coeffβ(πΉ βf β πΊ)) = (π΄ βf β π΅)) | ||
Theorem | coe1termlem 26007* | The coefficient function of a monomial. (Contributed by Mario Carneiro, 26-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ πΉ = (π§ β β β¦ (π΄ Β· (π§βπ))) β β’ ((π΄ β β β§ π β β0) β ((coeffβπΉ) = (π β β0 β¦ if(π = π, π΄, 0)) β§ (π΄ β 0 β (degβπΉ) = π))) | ||
Theorem | coe1term 26008* | The coefficient function of a monomial. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ πΉ = (π§ β β β¦ (π΄ Β· (π§βπ))) β β’ ((π΄ β β β§ π β β0 β§ π β β0) β ((coeffβπΉ)βπ) = if(π = π, π΄, 0)) | ||
Theorem | dgr1term 26009* | The degree of a monomial. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ πΉ = (π§ β β β¦ (π΄ Β· (π§βπ))) β β’ ((π΄ β β β§ π΄ β 0 β§ π β β0) β (degβπΉ) = π) | ||
Theorem | plycn 26010 | A polynomial is a continuous function. (Contributed by Mario Carneiro, 23-Jul-2014.) Avoid ax-mulf 11192. (Revised by GG, 16-Mar-2025.) |
β’ (πΉ β (Polyβπ) β πΉ β (ββcnββ)) | ||
Theorem | plycnOLD 26011 | Obsolete version of plycn 26010 as of 10-Apr-2025. (Contributed by Mario Carneiro, 23-Jul-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (πΉ β (Polyβπ) β πΉ β (ββcnββ)) | ||
Theorem | dgr0 26012 | The degree of the zero polynomial is zero. Note: this differs from some other definitions of the degree of the zero polynomial, such as -1, -β or undefined. But it is convenient for us to define it this way, so that we have dgrcl 25982, dgreq0 26015 and coeid 25987 without having to special-case zero, although plydivalg 26048 is a little more complicated as a result. (Contributed by Mario Carneiro, 22-Jul-2014.) |
β’ (degβ0π) = 0 | ||
Theorem | coeidp 26013 | The coefficients of the identity function. (Contributed by Mario Carneiro, 28-Jul-2014.) |
β’ (π΄ β β0 β ((coeffβXp)βπ΄) = if(π΄ = 1, 1, 0)) | ||
Theorem | dgrid 26014 | The degree of the identity function. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ (degβXp) = 1 | ||
Theorem | dgreq0 26015 | The leading coefficient of a polynomial is nonzero, unless the entire polynomial is zero. (Contributed by Mario Carneiro, 22-Jul-2014.) (Proof shortened by Fan Zheng, 21-Jun-2016.) |
β’ π = (degβπΉ) & β’ π΄ = (coeffβπΉ) β β’ (πΉ β (Polyβπ) β (πΉ = 0π β (π΄βπ) = 0)) | ||
Theorem | dgrlt 26016 | Two ways to say that the degree of πΉ is strictly less than π. (Contributed by Mario Carneiro, 25-Jul-2014.) |
β’ π = (degβπΉ) & β’ π΄ = (coeffβπΉ) β β’ ((πΉ β (Polyβπ) β§ π β β0) β ((πΉ = 0π β¨ π < π) β (π β€ π β§ (π΄βπ) = 0))) | ||
Theorem | dgradd 26017 | The degree of a sum of polynomials is at most the maximum of the degrees. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ π = (degβπΉ) & β’ π = (degβπΊ) β β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (degβ(πΉ βf + πΊ)) β€ if(π β€ π, π, π)) | ||
Theorem | dgradd2 26018 | The degree of a sum of polynomials of unequal degrees is the degree of the larger polynomial. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ π = (degβπΉ) & β’ π = (degβπΊ) β β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π < π) β (degβ(πΉ βf + πΊ)) = π) | ||
Theorem | dgrmul2 26019 | The degree of a product of polynomials is at most the sum of degrees. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ π = (degβπΉ) & β’ π = (degβπΊ) β β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (degβ(πΉ βf Β· πΊ)) β€ (π + π)) | ||
Theorem | dgrmul 26020 | The degree of a product of nonzero polynomials is the sum of degrees. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ π = (degβπΉ) & β’ π = (degβπΊ) β β’ (((πΉ β (Polyβπ) β§ πΉ β 0π) β§ (πΊ β (Polyβπ) β§ πΊ β 0π)) β (degβ(πΉ βf Β· πΊ)) = (π + π)) | ||
Theorem | dgrmulc 26021 | Scalar multiplication by a nonzero constant does not change the degree of a function. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ ((π΄ β β β§ π΄ β 0 β§ πΉ β (Polyβπ)) β (degβ((β Γ {π΄}) βf Β· πΉ)) = (degβπΉ)) | ||
Theorem | dgrsub 26022 | The degree of a difference of polynomials is at most the maximum of the degrees. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ π = (degβπΉ) & β’ π = (degβπΊ) β β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (degβ(πΉ βf β πΊ)) β€ if(π β€ π, π, π)) | ||
Theorem | dgrcolem1 26023* | The degree of a composition of a monomial with a polynomial. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ π = (degβπΊ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β πΊ β (Polyβπ)) β β’ (π β (degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) = (π Β· π)) | ||
Theorem | dgrcolem2 26024* | Lemma for dgrco 26025. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ π = (degβπΉ) & β’ π = (degβπΊ) & β’ (π β πΉ β (Polyβπ)) & β’ (π β πΊ β (Polyβπ)) & β’ π΄ = (coeffβπΉ) & β’ (π β π· β β0) & β’ (π β π = (π· + 1)) & β’ (π β βπ β (Polyββ)((degβπ) β€ π· β (degβ(π β πΊ)) = ((degβπ) Β· π))) β β’ (π β (degβ(πΉ β πΊ)) = (π Β· π)) | ||
Theorem | dgrco 26025 | The degree of a composition of two polynomials is the product of the degrees. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ π = (degβπΉ) & β’ π = (degβπΊ) & β’ (π β πΉ β (Polyβπ)) & β’ (π β πΊ β (Polyβπ)) β β’ (π β (degβ(πΉ β πΊ)) = (π Β· π)) | ||
Theorem | plycjlem 26026* | Lemma for plycj 26027 and coecj 26028. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ π = (degβπΉ) & β’ πΊ = ((β β πΉ) β β) & β’ π΄ = (coeffβπΉ) β β’ (πΉ β (Polyβπ) β πΊ = (π§ β β β¦ Ξ£π β (0...π)(((β β π΄)βπ) Β· (π§βπ)))) | ||
Theorem | plycj 26027* | The double conjugation of a polynomial is a polynomial. (The single conjugation is not because our definition of polynomial includes only holomorphic functions, i.e. no dependence on (ββπ§) independently of π§.) (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ π = (degβπΉ) & β’ πΊ = ((β β πΉ) β β) & β’ ((π β§ π₯ β π) β (ββπ₯) β π) & β’ (π β πΉ β (Polyβπ)) β β’ (π β πΊ β (Polyβπ)) | ||
Theorem | coecj 26028 | Double conjugation of a polynomial causes the coefficients to be conjugated. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ π = (degβπΉ) & β’ πΊ = ((β β πΉ) β β) & β’ π΄ = (coeffβπΉ) β β’ (πΉ β (Polyβπ) β (coeffβπΊ) = (β β π΄)) | ||
Theorem | plyrecj 26029 | A polynomial with real coefficients distributes under conjugation. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ ((πΉ β (Polyββ) β§ π΄ β β) β (ββ(πΉβπ΄)) = (πΉβ(ββπ΄))) | ||
Theorem | plymul0or 26030 | Polynomial multiplication has no zero divisors. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β ((πΉ βf Β· πΊ) = 0π β (πΉ = 0π β¨ πΊ = 0π))) | ||
Theorem | ofmulrt 26031 | The set of roots of a product is the union of the roots of the terms. (Contributed by Mario Carneiro, 28-Jul-2014.) |
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆβ) β (β‘(πΉ βf Β· πΊ) β {0}) = ((β‘πΉ β {0}) βͺ (β‘πΊ β {0}))) | ||
Theorem | plyreres 26032 | Real-coefficient polynomials restrict to real functions. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ (πΉ β (Polyββ) β (πΉ βΎ β):ββΆβ) | ||
Theorem | dvply1 26033* | Derivative of a polynomial, explicit sum version. (Contributed by Stefan O'Rear, 13-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
β’ (π β πΉ = (π§ β β β¦ Ξ£π β (0...π)((π΄βπ) Β· (π§βπ)))) & β’ (π β πΊ = (π§ β β β¦ Ξ£π β (0...(π β 1))((π΅βπ) Β· (π§βπ)))) & β’ (π β π΄:β0βΆβ) & β’ π΅ = (π β β0 β¦ ((π + 1) Β· (π΄β(π + 1)))) & β’ (π β π β β0) β β’ (π β (β D πΉ) = πΊ) | ||
Theorem | dvply2g 26034 | The derivative of a polynomial with coefficients in a subring is a polynomial with coefficients in the same ring. (Contributed by Mario Carneiro, 1-Jan-2017.) |
β’ ((π β (SubRingββfld) β§ πΉ β (Polyβπ)) β (β D πΉ) β (Polyβπ)) | ||
Theorem | dvply2 26035 | The derivative of a polynomial is a polynomial. (Contributed by Stefan O'Rear, 14-Nov-2014.) (Proof shortened by Mario Carneiro, 1-Jan-2017.) |
β’ (πΉ β (Polyβπ) β (β D πΉ) β (Polyββ)) | ||
Theorem | dvnply2 26036 | Polynomials have polynomials as derivatives of all orders. (Contributed by Mario Carneiro, 1-Jan-2017.) |
β’ ((π β (SubRingββfld) β§ πΉ β (Polyβπ) β§ π β β0) β ((β Dπ πΉ)βπ) β (Polyβπ)) | ||
Theorem | dvnply 26037 | Polynomials have polynomials as derivatives of all orders. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Revised by Mario Carneiro, 1-Jan-2017.) |
β’ ((πΉ β (Polyβπ) β§ π β β0) β ((β Dπ πΉ)βπ) β (Polyββ)) | ||
Theorem | plycpn 26038 | Polynomials are smooth. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
β’ (πΉ β (Polyβπ) β πΉ β β© ran (πCπββ)) | ||
Syntax | cquot 26039 | Extend class notation to include the quotient of a polynomial division. |
class quot | ||
Definition | df-quot 26040* | Define the quotient function on polynomials. This is the π of the expression π = π Β· π + π in the division algorithm. (Contributed by Mario Carneiro, 23-Jul-2014.) |
β’ quot = (π β (Polyββ), π β ((Polyββ) β {0π}) β¦ (β©π β (Polyββ)[(π βf β (π βf Β· π)) / π](π = 0π β¨ (degβπ) < (degβπ)))) | ||
Theorem | quotval 26041* | Value of the quotient function. (Contributed by Mario Carneiro, 23-Jul-2014.) |
β’ π = (πΉ βf β (πΊ βf Β· π)) β β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ πΊ β 0π) β (πΉ quot πΊ) = (β©π β (Polyββ)(π = 0π β¨ (degβπ ) < (degβπΊ)))) | ||
Theorem | plydivlem1 26042* | Lemma for plydivalg 26048. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ Β· π¦) β π) & β’ ((π β§ (π₯ β π β§ π₯ β 0)) β (1 / π₯) β π) & β’ (π β -1 β π) β β’ (π β 0 β π) | ||
Theorem | plydivlem2 26043* | Lemma for plydivalg 26048. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ Β· π¦) β π) & β’ ((π β§ (π₯ β π β§ π₯ β 0)) β (1 / π₯) β π) & β’ (π β -1 β π) & β’ (π β πΉ β (Polyβπ)) & β’ (π β πΊ β (Polyβπ)) & β’ (π β πΊ β 0π) & β’ π = (πΉ βf β (πΊ βf Β· π)) β β’ ((π β§ π β (Polyβπ)) β π β (Polyβπ)) | ||
Theorem | plydivlem3 26044* | Lemma for plydivex 26046. Base case of induction. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ Β· π¦) β π) & β’ ((π β§ (π₯ β π β§ π₯ β 0)) β (1 / π₯) β π) & β’ (π β -1 β π) & β’ (π β πΉ β (Polyβπ)) & β’ (π β πΊ β (Polyβπ)) & β’ (π β πΊ β 0π) & β’ π = (πΉ βf β (πΊ βf Β· π)) & β’ (π β (πΉ = 0π β¨ ((degβπΉ) β (degβπΊ)) < 0)) β β’ (π β βπ β (Polyβπ)(π = 0π β¨ (degβπ ) < (degβπΊ))) | ||
Theorem | plydivlem4 26045* | Lemma for plydivex 26046. Induction step. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ Β· π¦) β π) & β’ ((π β§ (π₯ β π β§ π₯ β 0)) β (1 / π₯) β π) & β’ (π β -1 β π) & β’ (π β πΉ β (Polyβπ)) & β’ (π β πΊ β (Polyβπ)) & β’ (π β πΊ β 0π) & β’ π = (πΉ βf β (πΊ βf Β· π)) & β’ (π β π· β β0) & β’ (π β (π β π) = π·) & β’ (π β πΉ β 0π) & β’ π = (π βf β (πΊ βf Β· π)) & β’ π» = (π§ β β β¦ (((π΄βπ) / (π΅βπ)) Β· (π§βπ·))) & β’ (π β βπ β (Polyβπ)((π = 0π β¨ ((degβπ) β π) < π·) β βπ β (Polyβπ)(π = 0π β¨ (degβπ) < π))) & β’ π΄ = (coeffβπΉ) & β’ π΅ = (coeffβπΊ) & β’ π = (degβπΉ) & β’ π = (degβπΊ) β β’ (π β βπ β (Polyβπ)(π = 0π β¨ (degβπ ) < π)) | ||
Theorem | plydivex 26046* | Lemma for plydivalg 26048. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ Β· π¦) β π) & β’ ((π β§ (π₯ β π β§ π₯ β 0)) β (1 / π₯) β π) & β’ (π β -1 β π) & β’ (π β πΉ β (Polyβπ)) & β’ (π β πΊ β (Polyβπ)) & β’ (π β πΊ β 0π) & β’ π = (πΉ βf β (πΊ βf Β· π)) β β’ (π β βπ β (Polyβπ)(π = 0π β¨ (degβπ ) < (degβπΊ))) | ||
Theorem | plydiveu 26047* | Lemma for plydivalg 26048. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ Β· π¦) β π) & β’ ((π β§ (π₯ β π β§ π₯ β 0)) β (1 / π₯) β π) & β’ (π β -1 β π) & β’ (π β πΉ β (Polyβπ)) & β’ (π β πΊ β (Polyβπ)) & β’ (π β πΊ β 0π) & β’ π = (πΉ βf β (πΊ βf Β· π)) & β’ (π β π β (Polyβπ)) & β’ (π β (π = 0π β¨ (degβπ ) < (degβπΊ))) & β’ π = (πΉ βf β (πΊ βf Β· π)) & β’ (π β π β (Polyβπ)) & β’ (π β (π = 0π β¨ (degβπ) < (degβπΊ))) β β’ (π β π = π) | ||
Theorem | plydivalg 26048* | The division algorithm on polynomials over a subfield π of the complex numbers. If πΉ and πΊ β 0 are polynomials over π, then there is a unique quotient polynomial π such that the remainder πΉ β πΊ Β· π is either zero or has degree less than πΊ. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ Β· π¦) β π) & β’ ((π β§ (π₯ β π β§ π₯ β 0)) β (1 / π₯) β π) & β’ (π β -1 β π) & β’ (π β πΉ β (Polyβπ)) & β’ (π β πΊ β (Polyβπ)) & β’ (π β πΊ β 0π) & β’ π = (πΉ βf β (πΊ βf Β· π)) β β’ (π β β!π β (Polyβπ)(π = 0π β¨ (degβπ ) < (degβπΊ))) | ||
Theorem | quotlem 26049* | Lemma for properties of the polynomial quotient function. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ Β· π¦) β π) & β’ ((π β§ (π₯ β π β§ π₯ β 0)) β (1 / π₯) β π) & β’ (π β -1 β π) & β’ (π β πΉ β (Polyβπ)) & β’ (π β πΊ β (Polyβπ)) & β’ (π β πΊ β 0π) & β’ π = (πΉ βf β (πΊ βf Β· (πΉ quot πΊ))) β β’ (π β ((πΉ quot πΊ) β (Polyβπ) β§ (π = 0π β¨ (degβπ ) < (degβπΊ)))) | ||
Theorem | quotcl 26050* | The quotient of two polynomials in a field π is also in the field. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ Β· π¦) β π) & β’ ((π β§ (π₯ β π β§ π₯ β 0)) β (1 / π₯) β π) & β’ (π β -1 β π) & β’ (π β πΉ β (Polyβπ)) & β’ (π β πΊ β (Polyβπ)) & β’ (π β πΊ β 0π) β β’ (π β (πΉ quot πΊ) β (Polyβπ)) | ||
Theorem | quotcl2 26051 | Closure of the quotient function. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ πΊ β 0π) β (πΉ quot πΊ) β (Polyββ)) | ||
Theorem | quotdgr 26052 | Remainder property of the quotient function. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ π = (πΉ βf β (πΊ βf Β· (πΉ quot πΊ))) β β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ πΊ β 0π) β (π = 0π β¨ (degβπ ) < (degβπΊ))) | ||
Theorem | plyremlem 26053 | Closure of a linear factor. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ πΊ = (Xp βf β (β Γ {π΄})) β β’ (π΄ β β β (πΊ β (Polyββ) β§ (degβπΊ) = 1 β§ (β‘πΊ β {0}) = {π΄})) | ||
Theorem | plyrem 26054 | The polynomial remainder theorem, or little BΓ©zout's theorem (by contrast to the regular BΓ©zout's theorem bezout 16489). 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). This is part of Metamath 100 proof #89. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ πΊ = (Xp βf β (β Γ {π΄})) & β’ π = (πΉ βf β (πΊ βf Β· (πΉ quot πΊ))) β β’ ((πΉ β (Polyβπ) β§ π΄ β β) β π = (β Γ {(πΉβπ΄)})) | ||
Theorem | facth 26055 | The factor theorem. If a polynomial πΉ has a root at π΄, then πΊ = π₯ β π΄ is a factor of πΉ (and the other factor is πΉ quot πΊ). This is part of Metamath 100 proof #89. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ πΊ = (Xp βf β (β Γ {π΄})) β β’ ((πΉ β (Polyβπ) β§ π΄ β β β§ (πΉβπ΄) = 0) β πΉ = (πΊ βf Β· (πΉ quot πΊ))) | ||
Theorem | fta1lem 26056* | Lemma for fta1 26057. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ π = (β‘πΉ β {0}) & β’ (π β π· β β0) & β’ (π β πΉ β ((Polyββ) β {0π})) & β’ (π β (degβπΉ) = (π· + 1)) & β’ (π β π΄ β (β‘πΉ β {0})) & β’ (π β βπ β ((Polyββ) β {0π})((degβπ) = π· β ((β‘π β {0}) β Fin β§ (β―β(β‘π β {0})) β€ (degβπ)))) β β’ (π β (π β Fin β§ (β―βπ ) β€ (degβπΉ))) | ||
Theorem | fta1 26057 | The easy direction of the Fundamental Theorem of Algebra: A nonzero polynomial has at most deg(πΉ) roots. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ π = (β‘πΉ β {0}) β β’ ((πΉ β (Polyβπ) β§ πΉ β 0π) β (π β Fin β§ (β―βπ ) β€ (degβπΉ))) | ||
Theorem | quotcan 26058 | Exact division with a multiple. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ π» = (πΉ βf Β· πΊ) β β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ πΊ β 0π) β (π» quot πΊ) = πΉ) | ||
Theorem | vieta1lem1 26059* | Lemma for vieta1 26061. (Contributed by Mario Carneiro, 28-Jul-2014.) |
β’ π΄ = (coeffβπΉ) & β’ π = (degβπΉ) & β’ π = (β‘πΉ β {0}) & β’ (π β πΉ β (Polyβπ)) & β’ (π β (β―βπ ) = π) & β’ (π β π· β β) & β’ (π β (π· + 1) = π) & β’ (π β βπ β (Polyββ)((π· = (degβπ) β§ (β―β(β‘π β {0})) = (degβπ)) β Ξ£π₯ β (β‘π β {0})π₯ = -(((coeffβπ)β((degβπ) β 1)) / ((coeffβπ)β(degβπ))))) & β’ π = (πΉ quot (Xp βf β (β Γ {π§}))) β β’ ((π β§ π§ β π ) β (π β (Polyββ) β§ π· = (degβπ))) | ||
Theorem | vieta1lem2 26060* | Lemma for vieta1 26061: inductive step. Let π§ be a root of πΉ. Then πΉ = (Xp β π§) Β· π for some π by the factor theorem, and π is a degree- π· polynomial, so by the induction hypothesis Ξ£π₯ β (β‘π β 0)π₯ = -(coeffβπ)β(π· β 1) / (coeffβπ)βπ·, so Ξ£π₯ β π π₯ = π§ β (coeffβπ)β (π· β 1) / (coeffβπ)βπ·. Now the coefficients of πΉ are π΄β(π· + 1) = (coeffβπ)βπ· and π΄βπ· = Ξ£π β (0...π·)(coeffβXp β π§)βπ Β· (coeffβπ) β(π· β π), which works out to -π§ Β· (coeffβπ)βπ· + (coeffβπ)β(π· β 1), so putting it all together we have Ξ£π₯ β π π₯ = -π΄βπ· / π΄β(π· + 1) as we wanted to show. (Contributed by Mario Carneiro, 28-Jul-2014.) |
β’ π΄ = (coeffβπΉ) & β’ π = (degβπΉ) & β’ π = (β‘πΉ β {0}) & β’ (π β πΉ β (Polyβπ)) & β’ (π β (β―βπ ) = π) & β’ (π β π· β β) & β’ (π β (π· + 1) = π) & β’ (π β βπ β (Polyββ)((π· = (degβπ) β§ (β―β(β‘π β {0})) = (degβπ)) β Ξ£π₯ β (β‘π β {0})π₯ = -(((coeffβπ)β((degβπ) β 1)) / ((coeffβπ)β(degβπ))))) & β’ π = (πΉ quot (Xp βf β (β Γ {π§}))) β β’ (π β Ξ£π₯ β π π₯ = -((π΄β(π β 1)) / (π΄βπ))) | ||
Theorem | vieta1 26061* | The first-order Vieta's formula (see http://en.wikipedia.org/wiki/Vieta%27s_formulas). If a polynomial of degree π has π distinct roots, then the sum over these roots can be calculated as -π΄(π β 1) / π΄(π). (If the roots are not distinct, then this formula is still true but must double-count some of the roots according to their multiplicities.) (Contributed by Mario Carneiro, 28-Jul-2014.) |
β’ π΄ = (coeffβπΉ) & β’ π = (degβπΉ) & β’ π = (β‘πΉ β {0}) & β’ (π β πΉ β (Polyβπ)) & β’ (π β (β―βπ ) = π) & β’ (π β π β β) β β’ (π β Ξ£π₯ β π π₯ = -((π΄β(π β 1)) / (π΄βπ))) | ||
Theorem | plyexmo 26062* | An infinite set of values can be extended to a polynomial in at most one way. (Contributed by Stefan O'Rear, 14-Nov-2014.) |
β’ ((π· β β β§ Β¬ π· β Fin) β β*π(π β (Polyβπ) β§ (π βΎ π·) = πΉ)) | ||
Syntax | caa 26063 | Extend class notation to include the set of algebraic numbers. |
class πΈ | ||
Definition | df-aa 26064 | Define the set of algebraic numbers. An algebraic number is a root of a nonzero polynomial over the integers. Here we construct it as the union of all kernels (preimages of {0}) of all polynomials in (Polyββ€), except the zero polynomial 0π. (Contributed by Mario Carneiro, 22-Jul-2014.) |
β’ πΈ = βͺ π β ((Polyββ€) β {0π})(β‘π β {0}) | ||
Theorem | elaa 26065* | Elementhood in the set of algebraic numbers. (Contributed by Mario Carneiro, 22-Jul-2014.) |
β’ (π΄ β πΈ β (π΄ β β β§ βπ β ((Polyββ€) β {0π})(πβπ΄) = 0)) | ||
Theorem | aacn 26066 | An algebraic number is a complex number. (Contributed by Mario Carneiro, 23-Jul-2014.) |
β’ (π΄ β πΈ β π΄ β β) | ||
Theorem | aasscn 26067 | The algebraic numbers are a subset of the complex numbers. (Contributed by Mario Carneiro, 23-Jul-2014.) |
β’ πΈ β β | ||
Theorem | elqaalem1 26068* | Lemma for elqaa 26071. The function π represents the denominators of the rational coefficients π΅. By multiplying them all together to make π , we get a number big enough to clear all the denominators and make π Β· πΉ an integer polynomial. (Contributed by Mario Carneiro, 23-Jul-2014.) (Revised by AV, 3-Oct-2020.) |
β’ (π β π΄ β β) & β’ (π β πΉ β ((Polyββ) β {0π})) & β’ (π β (πΉβπ΄) = 0) & β’ π΅ = (coeffβπΉ) & β’ π = (π β β0 β¦ inf({π β β β£ ((π΅βπ) Β· π) β β€}, β, < )) & β’ π = (seq0( Β· , π)β(degβπΉ)) β β’ ((π β§ πΎ β β0) β ((πβπΎ) β β β§ ((π΅βπΎ) Β· (πβπΎ)) β β€)) | ||
Theorem | elqaalem2 26069* | Lemma for elqaa 26071. (Contributed by Mario Carneiro, 23-Jul-2014.) (Revised by AV, 3-Oct-2020.) |
β’ (π β π΄ β β) & β’ (π β πΉ β ((Polyββ) β {0π})) & β’ (π β (πΉβπ΄) = 0) & β’ π΅ = (coeffβπΉ) & β’ π = (π β β0 β¦ inf({π β β β£ ((π΅βπ) Β· π) β β€}, β, < )) & β’ π = (seq0( Β· , π)β(degβπΉ)) & β’ π = (π₯ β V, π¦ β V β¦ ((π₯ Β· π¦) mod (πβπΎ))) β β’ ((π β§ πΎ β (0...(degβπΉ))) β (π mod (πβπΎ)) = 0) | ||
Theorem | elqaalem3 26070* | Lemma for elqaa 26071. (Contributed by Mario Carneiro, 23-Jul-2014.) (Revised by AV, 3-Oct-2020.) |
β’ (π β π΄ β β) & β’ (π β πΉ β ((Polyββ) β {0π})) & β’ (π β (πΉβπ΄) = 0) & β’ π΅ = (coeffβπΉ) & β’ π = (π β β0 β¦ inf({π β β β£ ((π΅βπ) Β· π) β β€}, β, < )) & β’ π = (seq0( Β· , π)β(degβπΉ)) β β’ (π β π΄ β πΈ) | ||
Theorem | elqaa 26071* | The set of numbers generated by the roots of polynomials in the rational numbers is the same as the set of algebraic numbers, which by elaa 26065 are defined only in terms of polynomials over the integers. (Contributed by Mario Carneiro, 23-Jul-2014.) (Proof shortened by AV, 3-Oct-2020.) |
β’ (π΄ β πΈ β (π΄ β β β§ βπ β ((Polyββ) β {0π})(πβπ΄) = 0)) | ||
Theorem | qaa 26072 | Every rational number is algebraic. (Contributed by Mario Carneiro, 23-Jul-2014.) |
β’ (π΄ β β β π΄ β πΈ) | ||
Theorem | qssaa 26073 | The rational numbers are contained in the algebraic numbers. (Contributed by Mario Carneiro, 23-Jul-2014.) |
β’ β β πΈ | ||
Theorem | iaa 26074 | The imaginary unit is algebraic. (Contributed by Mario Carneiro, 23-Jul-2014.) |
β’ i β πΈ | ||
Theorem | aareccl 26075 | The reciprocal of an algebraic number is algebraic. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ ((π΄ β πΈ β§ π΄ β 0) β (1 / π΄) β πΈ) | ||
Theorem | aacjcl 26076 | The conjugate of an algebraic number is algebraic. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ (π΄ β πΈ β (ββπ΄) β πΈ) | ||
Theorem | aannenlem1 26077* | Lemma for aannen 26080. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ π» = (π β β0 β¦ {π β β β£ βπ β {π β (Polyββ€) β£ (π β 0π β§ (degβπ) β€ π β§ βπ β β0 (absβ((coeffβπ)βπ)) β€ π)} (πβπ) = 0}) β β’ (π΄ β β0 β (π»βπ΄) β Fin) | ||
Theorem | aannenlem2 26078* | Lemma for aannen 26080. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ π» = (π β β0 β¦ {π β β β£ βπ β {π β (Polyββ€) β£ (π β 0π β§ (degβπ) β€ π β§ βπ β β0 (absβ((coeffβπ)βπ)) β€ π)} (πβπ) = 0}) β β’ πΈ = βͺ ran π» | ||
Theorem | aannenlem3 26079* | The algebraic numbers are countable. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ π» = (π β β0 β¦ {π β β β£ βπ β {π β (Polyββ€) β£ (π β 0π β§ (degβπ) β€ π β§ βπ β β0 (absβ((coeffβπ)βπ)) β€ π)} (πβπ) = 0}) β β’ πΈ β β | ||
Theorem | aannen 26080 | The algebraic numbers are countable. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΈ β β | ||
Theorem | aalioulem1 26081 | Lemma for aaliou 26087. An integer polynomial cannot inflate the denominator of a rational by more than its degree. (Contributed by Stefan O'Rear, 12-Nov-2014.) |
β’ (π β πΉ β (Polyββ€)) & β’ (π β π β β€) & β’ (π β π β β) β β’ (π β ((πΉβ(π / π)) Β· (πβ(degβπΉ))) β β€) | ||
Theorem | aalioulem2 26082* | Lemma for aaliou 26087. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Proof shortened by AV, 28-Sep-2020.) |
β’ π = (degβπΉ) & β’ (π β πΉ β (Polyββ€)) & β’ (π β π β β) & β’ (π β π΄ β β) β β’ (π β βπ₯ β β+ βπ β β€ βπ β β ((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π)))))) | ||
Theorem | aalioulem3 26083* | Lemma for aaliou 26087. (Contributed by Stefan O'Rear, 15-Nov-2014.) |
β’ π = (degβπΉ) & β’ (π β πΉ β (Polyββ€)) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β (πΉβπ΄) = 0) β β’ (π β βπ₯ β β+ βπ β β ((absβ(π΄ β π)) β€ 1 β (π₯ Β· (absβ(πΉβπ))) β€ (absβ(π΄ β π)))) | ||
Theorem | aalioulem4 26084* | Lemma for aaliou 26087. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ π = (degβπΉ) & β’ (π β πΉ β (Polyββ€)) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β (πΉβπ΄) = 0) β β’ (π β βπ₯ β β+ βπ β β€ βπ β β (((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1) β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π)))))) | ||
Theorem | aalioulem5 26085* | Lemma for aaliou 26087. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ π = (degβπΉ) & β’ (π β πΉ β (Polyββ€)) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β (πΉβπ΄) = 0) β β’ (π β βπ₯ β β+ βπ β β€ βπ β β ((πΉβ(π / π)) β 0 β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π)))))) | ||
Theorem | aalioulem6 26086* | Lemma for aaliou 26087. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ π = (degβπΉ) & β’ (π β πΉ β (Polyββ€)) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β (πΉβπ΄) = 0) β β’ (π β βπ₯ β β+ βπ β β€ βπ β β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π))))) | ||
Theorem | aaliou 26087* | Liouville's theorem on diophantine approximation: Any algebraic number, being a root of a polynomial πΉ in integer coefficients, is not approximable beyond order π = deg(πΉ) by rational numbers. In this form, it also applies to rational numbers themselves, which are not well approximable by other rational numbers. This is Metamath 100 proof #18. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ π = (degβπΉ) & β’ (π β πΉ β (Polyββ€)) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β (πΉβπ΄) = 0) β β’ (π β βπ₯ β β+ βπ β β€ βπ β β (π΄ = (π / π) β¨ (π₯ / (πβπ)) < (absβ(π΄ β (π / π))))) | ||
Theorem | geolim3 26088* | Geometric series convergence with arbitrary shift, radix, and multiplicative constant. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ (π β π΄ β β€) & β’ (π β π΅ β β) & β’ (π β (absβπ΅) < 1) & β’ (π β πΆ β β) & β’ πΉ = (π β (β€β₯βπ΄) β¦ (πΆ Β· (π΅β(π β π΄)))) β β’ (π β seqπ΄( + , πΉ) β (πΆ / (1 β π΅))) | ||
Theorem | aaliou2 26089* | Liouville's approximation theorem for algebraic numbers per se. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ (π΄ β (πΈ β© β) β βπ β β βπ₯ β β+ βπ β β€ βπ β β (π΄ = (π / π) β¨ (π₯ / (πβπ)) < (absβ(π΄ β (π / π))))) | ||
Theorem | aaliou2b 26090* | Liouville's approximation theorem extended to complex π΄. (Contributed by Stefan O'Rear, 20-Nov-2014.) |
β’ (π΄ β πΈ β βπ β β βπ₯ β β+ βπ β β€ βπ β β (π΄ = (π / π) β¨ (π₯ / (πβπ)) < (absβ(π΄ β (π / π))))) | ||
Theorem | aaliou3lem1 26091* | Lemma for aaliou3 26100. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΊ = (π β (β€β₯βπ΄) β¦ ((2β-(!βπ΄)) Β· ((1 / 2)β(π β π΄)))) β β’ ((π΄ β β β§ π΅ β (β€β₯βπ΄)) β (πΊβπ΅) β β) | ||
Theorem | aaliou3lem2 26092* | Lemma for aaliou3 26100. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΊ = (π β (β€β₯βπ΄) β¦ ((2β-(!βπ΄)) Β· ((1 / 2)β(π β π΄)))) & β’ πΉ = (π β β β¦ (2β-(!βπ))) β β’ ((π΄ β β β§ π΅ β (β€β₯βπ΄)) β (πΉβπ΅) β (0(,](πΊβπ΅))) | ||
Theorem | aaliou3lem3 26093* | Lemma for aaliou3 26100. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΊ = (π β (β€β₯βπ΄) β¦ ((2β-(!βπ΄)) Β· ((1 / 2)β(π β π΄)))) & β’ πΉ = (π β β β¦ (2β-(!βπ))) β β’ (π΄ β β β (seqπ΄( + , πΉ) β dom β β§ Ξ£π β (β€β₯βπ΄)(πΉβπ) β β+ β§ Ξ£π β (β€β₯βπ΄)(πΉβπ) β€ (2 Β· (2β-(!βπ΄))))) | ||
Theorem | aaliou3lem8 26094* | Lemma for aaliou3 26100. (Contributed by Stefan O'Rear, 20-Nov-2014.) |
β’ ((π΄ β β β§ π΅ β β+) β βπ₯ β β (2 Β· (2β-(!β(π₯ + 1)))) β€ (π΅ / ((2β(!βπ₯))βπ΄))) | ||
Theorem | aaliou3lem4 26095* | Lemma for aaliou3 26100. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΉ = (π β β β¦ (2β-(!βπ))) & β’ πΏ = Ξ£π β β (πΉβπ) & β’ π» = (π β β β¦ Ξ£π β (1...π)(πΉβπ)) β β’ πΏ β β | ||
Theorem | aaliou3lem5 26096* | Lemma for aaliou3 26100. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΉ = (π β β β¦ (2β-(!βπ))) & β’ πΏ = Ξ£π β β (πΉβπ) & β’ π» = (π β β β¦ Ξ£π β (1...π)(πΉβπ)) β β’ (π΄ β β β (π»βπ΄) β β) | ||
Theorem | aaliou3lem6 26097* | Lemma for aaliou3 26100. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΉ = (π β β β¦ (2β-(!βπ))) & β’ πΏ = Ξ£π β β (πΉβπ) & β’ π» = (π β β β¦ Ξ£π β (1...π)(πΉβπ)) β β’ (π΄ β β β ((π»βπ΄) Β· (2β(!βπ΄))) β β€) | ||
Theorem | aaliou3lem7 26098* | Lemma for aaliou3 26100. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΉ = (π β β β¦ (2β-(!βπ))) & β’ πΏ = Ξ£π β β (πΉβπ) & β’ π» = (π β β β¦ Ξ£π β (1...π)(πΉβπ)) β β’ (π΄ β β β ((π»βπ΄) β πΏ β§ (absβ(πΏ β (π»βπ΄))) β€ (2 Β· (2β-(!β(π΄ + 1)))))) | ||
Theorem | aaliou3lem9 26099* | Example of a "Liouville number", a very simple definable transcendental real. (Contributed by Stefan O'Rear, 20-Nov-2014.) |
β’ πΉ = (π β β β¦ (2β-(!βπ))) & β’ πΏ = Ξ£π β β (πΉβπ) & β’ π» = (π β β β¦ Ξ£π β (1...π)(πΉβπ)) β β’ Β¬ πΏ β πΈ | ||
Theorem | aaliou3 26100 | Example of a "Liouville number", a very simple definable transcendental real. (Contributed by Stefan O'Rear, 23-Nov-2014.) |
β’ Ξ£π β β (2β-(!βπ)) β πΈ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |