![]() |
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-30439) |
![]() (30440-31962) |
![]() (31963-47940) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | coeadd 26001 | 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 | coemul 26002* | A coefficient of a product of polynomials. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ π΄ = (coeffβπΉ) & β’ π΅ = (coeffβπΊ) β β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π β β0) β ((coeffβ(πΉ βf Β· πΊ))βπ) = Ξ£π β (0...π)((π΄βπ) Β· (π΅β(π β π)))) | ||
Theorem | coe11 26003 | 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 26004 | 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 26005 | The coefficient function is linear under scalar multiplication. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ ((π΄ β β β§ πΉ β (Polyβπ)) β (coeffβ((β Γ {π΄}) βf Β· πΉ)) = ((β0 Γ {π΄}) βf Β· (coeffβπΉ))) | ||
Theorem | coe0 26006 | The coefficients of the zero polynomial are zero. (Contributed by Mario Carneiro, 22-Jul-2014.) |
β’ (coeffβ0π) = (β0 Γ {0}) | ||
Theorem | coesub 26007 | 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 26008* | 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 26009* | The coefficient function of a monomial. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ πΉ = (π§ β β β¦ (π΄ Β· (π§βπ))) β β’ ((π΄ β β β§ π β β0 β§ π β β0) β ((coeffβπΉ)βπ) = if(π = π, π΄, 0)) | ||
Theorem | dgr1term 26010* | The degree of a monomial. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ πΉ = (π§ β β β¦ (π΄ Β· (π§βπ))) β β’ ((π΄ β β β§ π΄ β 0 β§ π β β0) β (degβπΉ) = π) | ||
Theorem | plycn 26011 | A polynomial is a continuous function. (Contributed by Mario Carneiro, 23-Jul-2014.) Avoid ax-mulf 11194. (Revised by GG, 16-Mar-2025.) |
β’ (πΉ β (Polyβπ) β πΉ β (ββcnββ)) | ||
Theorem | plycnOLD 26012 | Obsolete version of plycn 26011 as of 10-Apr-2025. (Contributed by Mario Carneiro, 23-Jul-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (πΉ β (Polyβπ) β πΉ β (ββcnββ)) | ||
Theorem | dgr0 26013 | 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 25983, dgreq0 26016 and coeid 25988 without having to special-case zero, although plydivalg 26049 is a little more complicated as a result. (Contributed by Mario Carneiro, 22-Jul-2014.) |
β’ (degβ0π) = 0 | ||
Theorem | coeidp 26014 | The coefficients of the identity function. (Contributed by Mario Carneiro, 28-Jul-2014.) |
β’ (π΄ β β0 β ((coeffβXp)βπ΄) = if(π΄ = 1, 1, 0)) | ||
Theorem | dgrid 26015 | The degree of the identity function. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ (degβXp) = 1 | ||
Theorem | dgreq0 26016 | 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 26017 | 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 26018 | 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 26019 | 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 26020 | 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 26021 | 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 26022 | 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 26023 | 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 26024* | The degree of a composition of a monomial with a polynomial. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ π = (degβπΊ) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β πΊ β (Polyβπ)) β β’ (π β (degβ(π₯ β β β¦ ((πΊβπ₯)βπ))) = (π Β· π)) | ||
Theorem | dgrcolem2 26025* | Lemma for dgrco 26026. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ π = (degβπΉ) & β’ π = (degβπΊ) & β’ (π β πΉ β (Polyβπ)) & β’ (π β πΊ β (Polyβπ)) & β’ π΄ = (coeffβπΉ) & β’ (π β π· β β0) & β’ (π β π = (π· + 1)) & β’ (π β βπ β (Polyββ)((degβπ) β€ π· β (degβ(π β πΊ)) = ((degβπ) Β· π))) β β’ (π β (degβ(πΉ β πΊ)) = (π Β· π)) | ||
Theorem | dgrco 26026 | 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 26027* | Lemma for plycj 26028 and coecj 26029. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ π = (degβπΉ) & β’ πΊ = ((β β πΉ) β β) & β’ π΄ = (coeffβπΉ) β β’ (πΉ β (Polyβπ) β πΊ = (π§ β β β¦ Ξ£π β (0...π)(((β β π΄)βπ) Β· (π§βπ)))) | ||
Theorem | plycj 26028* | 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 26029 | Double conjugation of a polynomial causes the coefficients to be conjugated. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ π = (degβπΉ) & β’ πΊ = ((β β πΉ) β β) & β’ π΄ = (coeffβπΉ) β β’ (πΉ β (Polyβπ) β (coeffβπΊ) = (β β π΄)) | ||
Theorem | plyrecj 26030 | A polynomial with real coefficients distributes under conjugation. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ ((πΉ β (Polyββ) β§ π΄ β β) β (ββ(πΉβπ΄)) = (πΉβ(ββπ΄))) | ||
Theorem | plymul0or 26031 | Polynomial multiplication has no zero divisors. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β ((πΉ βf Β· πΊ) = 0π β (πΉ = 0π β¨ πΊ = 0π))) | ||
Theorem | ofmulrt 26032 | 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 26033 | Real-coefficient polynomials restrict to real functions. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ (πΉ β (Polyββ) β (πΉ βΎ β):ββΆβ) | ||
Theorem | dvply1 26034* | 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 26035 | 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 26036 | 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 26037 | Polynomials have polynomials as derivatives of all orders. (Contributed by Mario Carneiro, 1-Jan-2017.) |
β’ ((π β (SubRingββfld) β§ πΉ β (Polyβπ) β§ π β β0) β ((β Dπ πΉ)βπ) β (Polyβπ)) | ||
Theorem | dvnply 26038 | 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 26039 | Polynomials are smooth. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
β’ (πΉ β (Polyβπ) β πΉ β β© ran (πCπββ)) | ||
Syntax | cquot 26040 | Extend class notation to include the quotient of a polynomial division. |
class quot | ||
Definition | df-quot 26041* | 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 26042* | Value of the quotient function. (Contributed by Mario Carneiro, 23-Jul-2014.) |
β’ π = (πΉ βf β (πΊ βf Β· π)) β β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ πΊ β 0π) β (πΉ quot πΊ) = (β©π β (Polyββ)(π = 0π β¨ (degβπ ) < (degβπΊ)))) | ||
Theorem | plydivlem1 26043* | Lemma for plydivalg 26049. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ Β· π¦) β π) & β’ ((π β§ (π₯ β π β§ π₯ β 0)) β (1 / π₯) β π) & β’ (π β -1 β π) β β’ (π β 0 β π) | ||
Theorem | plydivlem2 26044* | Lemma for plydivalg 26049. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ Β· π¦) β π) & β’ ((π β§ (π₯ β π β§ π₯ β 0)) β (1 / π₯) β π) & β’ (π β -1 β π) & β’ (π β πΉ β (Polyβπ)) & β’ (π β πΊ β (Polyβπ)) & β’ (π β πΊ β 0π) & β’ π = (πΉ βf β (πΊ βf Β· π)) β β’ ((π β§ π β (Polyβπ)) β π β (Polyβπ)) | ||
Theorem | plydivlem3 26045* | Lemma for plydivex 26047. 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 26046* | Lemma for plydivex 26047. 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 26047* | Lemma for plydivalg 26049. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ Β· π¦) β π) & β’ ((π β§ (π₯ β π β§ π₯ β 0)) β (1 / π₯) β π) & β’ (π β -1 β π) & β’ (π β πΉ β (Polyβπ)) & β’ (π β πΊ β (Polyβπ)) & β’ (π β πΊ β 0π) & β’ π = (πΉ βf β (πΊ βf Β· π)) β β’ (π β βπ β (Polyβπ)(π = 0π β¨ (degβπ ) < (degβπΊ))) | ||
Theorem | plydiveu 26048* | Lemma for plydivalg 26049. (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 26049* | 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 26050* | 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 26051* | 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 26052 | Closure of the quotient function. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ πΊ β 0π) β (πΉ quot πΊ) β (Polyββ)) | ||
Theorem | quotdgr 26053 | Remainder property of the quotient function. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ π = (πΉ βf β (πΊ βf Β· (πΉ quot πΊ))) β β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ πΊ β 0π) β (π = 0π β¨ (degβπ ) < (degβπΊ))) | ||
Theorem | plyremlem 26054 | Closure of a linear factor. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ πΊ = (Xp βf β (β Γ {π΄})) β β’ (π΄ β β β (πΊ β (Polyββ) β§ (degβπΊ) = 1 β§ (β‘πΊ β {0}) = {π΄})) | ||
Theorem | plyrem 26055 | The polynomial remainder theorem, or little BΓ©zout's theorem (by contrast to the regular BΓ©zout's theorem bezout 16490). 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 26056 | 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 26057* | Lemma for fta1 26058. (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 26058 | 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 26059 | Exact division with a multiple. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ π» = (πΉ βf Β· πΊ) β β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ πΊ β 0π) β (π» quot πΊ) = πΉ) | ||
Theorem | vieta1lem1 26060* | Lemma for vieta1 26062. (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 26061* | Lemma for vieta1 26062: 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 26062* | 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 26063* | 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 26064 | Extend class notation to include the set of algebraic numbers. |
class πΈ | ||
Definition | df-aa 26065 | 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 26066* | Elementhood in the set of algebraic numbers. (Contributed by Mario Carneiro, 22-Jul-2014.) |
β’ (π΄ β πΈ β (π΄ β β β§ βπ β ((Polyββ€) β {0π})(πβπ΄) = 0)) | ||
Theorem | aacn 26067 | An algebraic number is a complex number. (Contributed by Mario Carneiro, 23-Jul-2014.) |
β’ (π΄ β πΈ β π΄ β β) | ||
Theorem | aasscn 26068 | The algebraic numbers are a subset of the complex numbers. (Contributed by Mario Carneiro, 23-Jul-2014.) |
β’ πΈ β β | ||
Theorem | elqaalem1 26069* | Lemma for elqaa 26072. 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 26070* | Lemma for elqaa 26072. (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 26071* | Lemma for elqaa 26072. (Contributed by Mario Carneiro, 23-Jul-2014.) (Revised by AV, 3-Oct-2020.) |
β’ (π β π΄ β β) & β’ (π β πΉ β ((Polyββ) β {0π})) & β’ (π β (πΉβπ΄) = 0) & β’ π΅ = (coeffβπΉ) & β’ π = (π β β0 β¦ inf({π β β β£ ((π΅βπ) Β· π) β β€}, β, < )) & β’ π = (seq0( Β· , π)β(degβπΉ)) β β’ (π β π΄ β πΈ) | ||
Theorem | elqaa 26072* | 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 26066 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 26073 | Every rational number is algebraic. (Contributed by Mario Carneiro, 23-Jul-2014.) |
β’ (π΄ β β β π΄ β πΈ) | ||
Theorem | qssaa 26074 | The rational numbers are contained in the algebraic numbers. (Contributed by Mario Carneiro, 23-Jul-2014.) |
β’ β β πΈ | ||
Theorem | iaa 26075 | The imaginary unit is algebraic. (Contributed by Mario Carneiro, 23-Jul-2014.) |
β’ i β πΈ | ||
Theorem | aareccl 26076 | The reciprocal of an algebraic number is algebraic. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ ((π΄ β πΈ β§ π΄ β 0) β (1 / π΄) β πΈ) | ||
Theorem | aacjcl 26077 | The conjugate of an algebraic number is algebraic. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ (π΄ β πΈ β (ββπ΄) β πΈ) | ||
Theorem | aannenlem1 26078* | Lemma for aannen 26081. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ π» = (π β β0 β¦ {π β β β£ βπ β {π β (Polyββ€) β£ (π β 0π β§ (degβπ) β€ π β§ βπ β β0 (absβ((coeffβπ)βπ)) β€ π)} (πβπ) = 0}) β β’ (π΄ β β0 β (π»βπ΄) β Fin) | ||
Theorem | aannenlem2 26079* | Lemma for aannen 26081. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ π» = (π β β0 β¦ {π β β β£ βπ β {π β (Polyββ€) β£ (π β 0π β§ (degβπ) β€ π β§ βπ β β0 (absβ((coeffβπ)βπ)) β€ π)} (πβπ) = 0}) β β’ πΈ = βͺ ran π» | ||
Theorem | aannenlem3 26080* | The algebraic numbers are countable. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ π» = (π β β0 β¦ {π β β β£ βπ β {π β (Polyββ€) β£ (π β 0π β§ (degβπ) β€ π β§ βπ β β0 (absβ((coeffβπ)βπ)) β€ π)} (πβπ) = 0}) β β’ πΈ β β | ||
Theorem | aannen 26081 | The algebraic numbers are countable. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΈ β β | ||
Theorem | aalioulem1 26082 | Lemma for aaliou 26088. 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 26083* | Lemma for aaliou 26088. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Proof shortened by AV, 28-Sep-2020.) |
β’ π = (degβπΉ) & β’ (π β πΉ β (Polyββ€)) & β’ (π β π β β) & β’ (π β π΄ β β) β β’ (π β βπ₯ β β+ βπ β β€ βπ β β ((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π)))))) | ||
Theorem | aalioulem3 26084* | Lemma for aaliou 26088. (Contributed by Stefan O'Rear, 15-Nov-2014.) |
β’ π = (degβπΉ) & β’ (π β πΉ β (Polyββ€)) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β (πΉβπ΄) = 0) β β’ (π β βπ₯ β β+ βπ β β ((absβ(π΄ β π)) β€ 1 β (π₯ Β· (absβ(πΉβπ))) β€ (absβ(π΄ β π)))) | ||
Theorem | aalioulem4 26085* | Lemma for aaliou 26088. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ π = (degβπΉ) & β’ (π β πΉ β (Polyββ€)) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β (πΉβπ΄) = 0) β β’ (π β βπ₯ β β+ βπ β β€ βπ β β (((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1) β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π)))))) | ||
Theorem | aalioulem5 26086* | Lemma for aaliou 26088. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ π = (degβπΉ) & β’ (π β πΉ β (Polyββ€)) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β (πΉβπ΄) = 0) β β’ (π β βπ₯ β β+ βπ β β€ βπ β β ((πΉβ(π / π)) β 0 β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π)))))) | ||
Theorem | aalioulem6 26087* | Lemma for aaliou 26088. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ π = (degβπΉ) & β’ (π β πΉ β (Polyββ€)) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β (πΉβπ΄) = 0) β β’ (π β βπ₯ β β+ βπ β β€ βπ β β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π))))) | ||
Theorem | aaliou 26088* | 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 26089* | Geometric series convergence with arbitrary shift, radix, and multiplicative constant. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ (π β π΄ β β€) & β’ (π β π΅ β β) & β’ (π β (absβπ΅) < 1) & β’ (π β πΆ β β) & β’ πΉ = (π β (β€β₯βπ΄) β¦ (πΆ Β· (π΅β(π β π΄)))) β β’ (π β seqπ΄( + , πΉ) β (πΆ / (1 β π΅))) | ||
Theorem | aaliou2 26090* | Liouville's approximation theorem for algebraic numbers per se. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ (π΄ β (πΈ β© β) β βπ β β βπ₯ β β+ βπ β β€ βπ β β (π΄ = (π / π) β¨ (π₯ / (πβπ)) < (absβ(π΄ β (π / π))))) | ||
Theorem | aaliou2b 26091* | Liouville's approximation theorem extended to complex π΄. (Contributed by Stefan O'Rear, 20-Nov-2014.) |
β’ (π΄ β πΈ β βπ β β βπ₯ β β+ βπ β β€ βπ β β (π΄ = (π / π) β¨ (π₯ / (πβπ)) < (absβ(π΄ β (π / π))))) | ||
Theorem | aaliou3lem1 26092* | Lemma for aaliou3 26101. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΊ = (π β (β€β₯βπ΄) β¦ ((2β-(!βπ΄)) Β· ((1 / 2)β(π β π΄)))) β β’ ((π΄ β β β§ π΅ β (β€β₯βπ΄)) β (πΊβπ΅) β β) | ||
Theorem | aaliou3lem2 26093* | Lemma for aaliou3 26101. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΊ = (π β (β€β₯βπ΄) β¦ ((2β-(!βπ΄)) Β· ((1 / 2)β(π β π΄)))) & β’ πΉ = (π β β β¦ (2β-(!βπ))) β β’ ((π΄ β β β§ π΅ β (β€β₯βπ΄)) β (πΉβπ΅) β (0(,](πΊβπ΅))) | ||
Theorem | aaliou3lem3 26094* | Lemma for aaliou3 26101. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΊ = (π β (β€β₯βπ΄) β¦ ((2β-(!βπ΄)) Β· ((1 / 2)β(π β π΄)))) & β’ πΉ = (π β β β¦ (2β-(!βπ))) β β’ (π΄ β β β (seqπ΄( + , πΉ) β dom β β§ Ξ£π β (β€β₯βπ΄)(πΉβπ) β β+ β§ Ξ£π β (β€β₯βπ΄)(πΉβπ) β€ (2 Β· (2β-(!βπ΄))))) | ||
Theorem | aaliou3lem8 26095* | Lemma for aaliou3 26101. (Contributed by Stefan O'Rear, 20-Nov-2014.) |
β’ ((π΄ β β β§ π΅ β β+) β βπ₯ β β (2 Β· (2β-(!β(π₯ + 1)))) β€ (π΅ / ((2β(!βπ₯))βπ΄))) | ||
Theorem | aaliou3lem4 26096* | Lemma for aaliou3 26101. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΉ = (π β β β¦ (2β-(!βπ))) & β’ πΏ = Ξ£π β β (πΉβπ) & β’ π» = (π β β β¦ Ξ£π β (1...π)(πΉβπ)) β β’ πΏ β β | ||
Theorem | aaliou3lem5 26097* | Lemma for aaliou3 26101. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΉ = (π β β β¦ (2β-(!βπ))) & β’ πΏ = Ξ£π β β (πΉβπ) & β’ π» = (π β β β¦ Ξ£π β (1...π)(πΉβπ)) β β’ (π΄ β β β (π»βπ΄) β β) | ||
Theorem | aaliou3lem6 26098* | Lemma for aaliou3 26101. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΉ = (π β β β¦ (2β-(!βπ))) & β’ πΏ = Ξ£π β β (πΉβπ) & β’ π» = (π β β β¦ Ξ£π β (1...π)(πΉβπ)) β β’ (π΄ β β β ((π»βπ΄) Β· (2β(!βπ΄))) β β€) | ||
Theorem | aaliou3lem7 26099* | Lemma for aaliou3 26101. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΉ = (π β β β¦ (2β-(!βπ))) & β’ πΏ = Ξ£π β β (πΉβπ) & β’ π» = (π β β β¦ Ξ£π β (1...π)(πΉβπ)) β β’ (π΄ β β β ((π»βπ΄) β πΏ β§ (absβ(πΏ β (π»βπ΄))) β€ (2 Β· (2β-(!β(π΄ + 1)))))) | ||
Theorem | aaliou3lem9 26100* | Example of a "Liouville number", a very simple definable transcendental real. (Contributed by Stefan O'Rear, 20-Nov-2014.) |
β’ πΉ = (π β β β¦ (2β-(!βπ))) & β’ πΏ = Ξ£π β β (πΉβπ) & β’ π» = (π β β β¦ Ξ£π β (1...π)(πΉβπ)) β β’ Β¬ πΏ β πΈ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |