![]() |
Metamath
Proof Explorer Theorem List (p. 259 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dvnply 25801 | 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 25802 | Polynomials are smooth. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
β’ (πΉ β (Polyβπ) β πΉ β β© ran (πCπββ)) | ||
Syntax | cquot 25803 | Extend class notation to include the quotient of a polynomial division. |
class quot | ||
Definition | df-quot 25804* | 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 25805* | Value of the quotient function. (Contributed by Mario Carneiro, 23-Jul-2014.) |
β’ π = (πΉ βf β (πΊ βf Β· π)) β β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ πΊ β 0π) β (πΉ quot πΊ) = (β©π β (Polyββ)(π = 0π β¨ (degβπ ) < (degβπΊ)))) | ||
Theorem | plydivlem1 25806* | Lemma for plydivalg 25812. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ Β· π¦) β π) & β’ ((π β§ (π₯ β π β§ π₯ β 0)) β (1 / π₯) β π) & β’ (π β -1 β π) β β’ (π β 0 β π) | ||
Theorem | plydivlem2 25807* | Lemma for plydivalg 25812. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ Β· π¦) β π) & β’ ((π β§ (π₯ β π β§ π₯ β 0)) β (1 / π₯) β π) & β’ (π β -1 β π) & β’ (π β πΉ β (Polyβπ)) & β’ (π β πΊ β (Polyβπ)) & β’ (π β πΊ β 0π) & β’ π = (πΉ βf β (πΊ βf Β· π)) β β’ ((π β§ π β (Polyβπ)) β π β (Polyβπ)) | ||
Theorem | plydivlem3 25808* | Lemma for plydivex 25810. 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 25809* | Lemma for plydivex 25810. 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 25810* | Lemma for plydivalg 25812. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ Β· π¦) β π) & β’ ((π β§ (π₯ β π β§ π₯ β 0)) β (1 / π₯) β π) & β’ (π β -1 β π) & β’ (π β πΉ β (Polyβπ)) & β’ (π β πΊ β (Polyβπ)) & β’ (π β πΊ β 0π) & β’ π = (πΉ βf β (πΊ βf Β· π)) β β’ (π β βπ β (Polyβπ)(π = 0π β¨ (degβπ ) < (degβπΊ))) | ||
Theorem | plydiveu 25811* | Lemma for plydivalg 25812. (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 25812* | 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 25813* | 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 25814* | 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 25815 | Closure of the quotient function. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ πΊ β 0π) β (πΉ quot πΊ) β (Polyββ)) | ||
Theorem | quotdgr 25816 | Remainder property of the quotient function. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ π = (πΉ βf β (πΊ βf Β· (πΉ quot πΊ))) β β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ πΊ β 0π) β (π = 0π β¨ (degβπ ) < (degβπΊ))) | ||
Theorem | plyremlem 25817 | Closure of a linear factor. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ πΊ = (Xp βf β (β Γ {π΄})) β β’ (π΄ β β β (πΊ β (Polyββ) β§ (degβπΊ) = 1 β§ (β‘πΊ β {0}) = {π΄})) | ||
Theorem | plyrem 25818 | The polynomial remainder theorem, or little BΓ©zout's theorem (by contrast to the regular BΓ©zout's theorem bezout 16485). 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 25819 | 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 25820* | Lemma for fta1 25821. (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 25821 | 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 25822 | Exact division with a multiple. (Contributed by Mario Carneiro, 26-Jul-2014.) |
β’ π» = (πΉ βf Β· πΊ) β β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ πΊ β 0π) β (π» quot πΊ) = πΉ) | ||
Theorem | vieta1lem1 25823* | Lemma for vieta1 25825. (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 25824* | Lemma for vieta1 25825: 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 25825* | 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 25826* | 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 25827 | Extend class notation to include the set of algebraic numbers. |
class πΈ | ||
Definition | df-aa 25828 | 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 25829* | Elementhood in the set of algebraic numbers. (Contributed by Mario Carneiro, 22-Jul-2014.) |
β’ (π΄ β πΈ β (π΄ β β β§ βπ β ((Polyββ€) β {0π})(πβπ΄) = 0)) | ||
Theorem | aacn 25830 | An algebraic number is a complex number. (Contributed by Mario Carneiro, 23-Jul-2014.) |
β’ (π΄ β πΈ β π΄ β β) | ||
Theorem | aasscn 25831 | The algebraic numbers are a subset of the complex numbers. (Contributed by Mario Carneiro, 23-Jul-2014.) |
β’ πΈ β β | ||
Theorem | elqaalem1 25832* | Lemma for elqaa 25835. 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 25833* | Lemma for elqaa 25835. (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 25834* | Lemma for elqaa 25835. (Contributed by Mario Carneiro, 23-Jul-2014.) (Revised by AV, 3-Oct-2020.) |
β’ (π β π΄ β β) & β’ (π β πΉ β ((Polyββ) β {0π})) & β’ (π β (πΉβπ΄) = 0) & β’ π΅ = (coeffβπΉ) & β’ π = (π β β0 β¦ inf({π β β β£ ((π΅βπ) Β· π) β β€}, β, < )) & β’ π = (seq0( Β· , π)β(degβπΉ)) β β’ (π β π΄ β πΈ) | ||
Theorem | elqaa 25835* | 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 25829 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 25836 | Every rational number is algebraic. (Contributed by Mario Carneiro, 23-Jul-2014.) |
β’ (π΄ β β β π΄ β πΈ) | ||
Theorem | qssaa 25837 | The rational numbers are contained in the algebraic numbers. (Contributed by Mario Carneiro, 23-Jul-2014.) |
β’ β β πΈ | ||
Theorem | iaa 25838 | The imaginary unit is algebraic. (Contributed by Mario Carneiro, 23-Jul-2014.) |
β’ i β πΈ | ||
Theorem | aareccl 25839 | The reciprocal of an algebraic number is algebraic. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ ((π΄ β πΈ β§ π΄ β 0) β (1 / π΄) β πΈ) | ||
Theorem | aacjcl 25840 | The conjugate of an algebraic number is algebraic. (Contributed by Mario Carneiro, 24-Jul-2014.) |
β’ (π΄ β πΈ β (ββπ΄) β πΈ) | ||
Theorem | aannenlem1 25841* | Lemma for aannen 25844. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ π» = (π β β0 β¦ {π β β β£ βπ β {π β (Polyββ€) β£ (π β 0π β§ (degβπ) β€ π β§ βπ β β0 (absβ((coeffβπ)βπ)) β€ π)} (πβπ) = 0}) β β’ (π΄ β β0 β (π»βπ΄) β Fin) | ||
Theorem | aannenlem2 25842* | Lemma for aannen 25844. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ π» = (π β β0 β¦ {π β β β£ βπ β {π β (Polyββ€) β£ (π β 0π β§ (degβπ) β€ π β§ βπ β β0 (absβ((coeffβπ)βπ)) β€ π)} (πβπ) = 0}) β β’ πΈ = βͺ ran π» | ||
Theorem | aannenlem3 25843* | The algebraic numbers are countable. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ π» = (π β β0 β¦ {π β β β£ βπ β {π β (Polyββ€) β£ (π β 0π β§ (degβπ) β€ π β§ βπ β β0 (absβ((coeffβπ)βπ)) β€ π)} (πβπ) = 0}) β β’ πΈ β β | ||
Theorem | aannen 25844 | The algebraic numbers are countable. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΈ β β | ||
Theorem | aalioulem1 25845 | Lemma for aaliou 25851. 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 25846* | Lemma for aaliou 25851. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Proof shortened by AV, 28-Sep-2020.) |
β’ π = (degβπΉ) & β’ (π β πΉ β (Polyββ€)) & β’ (π β π β β) & β’ (π β π΄ β β) β β’ (π β βπ₯ β β+ βπ β β€ βπ β β ((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π)))))) | ||
Theorem | aalioulem3 25847* | Lemma for aaliou 25851. (Contributed by Stefan O'Rear, 15-Nov-2014.) |
β’ π = (degβπΉ) & β’ (π β πΉ β (Polyββ€)) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β (πΉβπ΄) = 0) β β’ (π β βπ₯ β β+ βπ β β ((absβ(π΄ β π)) β€ 1 β (π₯ Β· (absβ(πΉβπ))) β€ (absβ(π΄ β π)))) | ||
Theorem | aalioulem4 25848* | Lemma for aaliou 25851. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ π = (degβπΉ) & β’ (π β πΉ β (Polyββ€)) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β (πΉβπ΄) = 0) β β’ (π β βπ₯ β β+ βπ β β€ βπ β β (((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1) β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π)))))) | ||
Theorem | aalioulem5 25849* | Lemma for aaliou 25851. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ π = (degβπΉ) & β’ (π β πΉ β (Polyββ€)) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β (πΉβπ΄) = 0) β β’ (π β βπ₯ β β+ βπ β β€ βπ β β ((πΉβ(π / π)) β 0 β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π)))))) | ||
Theorem | aalioulem6 25850* | Lemma for aaliou 25851. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ π = (degβπΉ) & β’ (π β πΉ β (Polyββ€)) & β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β (πΉβπ΄) = 0) β β’ (π β βπ₯ β β+ βπ β β€ βπ β β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π))))) | ||
Theorem | aaliou 25851* | 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 25852* | Geometric series convergence with arbitrary shift, radix, and multiplicative constant. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ (π β π΄ β β€) & β’ (π β π΅ β β) & β’ (π β (absβπ΅) < 1) & β’ (π β πΆ β β) & β’ πΉ = (π β (β€β₯βπ΄) β¦ (πΆ Β· (π΅β(π β π΄)))) β β’ (π β seqπ΄( + , πΉ) β (πΆ / (1 β π΅))) | ||
Theorem | aaliou2 25853* | Liouville's approximation theorem for algebraic numbers per se. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ (π΄ β (πΈ β© β) β βπ β β βπ₯ β β+ βπ β β€ βπ β β (π΄ = (π / π) β¨ (π₯ / (πβπ)) < (absβ(π΄ β (π / π))))) | ||
Theorem | aaliou2b 25854* | Liouville's approximation theorem extended to complex π΄. (Contributed by Stefan O'Rear, 20-Nov-2014.) |
β’ (π΄ β πΈ β βπ β β βπ₯ β β+ βπ β β€ βπ β β (π΄ = (π / π) β¨ (π₯ / (πβπ)) < (absβ(π΄ β (π / π))))) | ||
Theorem | aaliou3lem1 25855* | Lemma for aaliou3 25864. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΊ = (π β (β€β₯βπ΄) β¦ ((2β-(!βπ΄)) Β· ((1 / 2)β(π β π΄)))) β β’ ((π΄ β β β§ π΅ β (β€β₯βπ΄)) β (πΊβπ΅) β β) | ||
Theorem | aaliou3lem2 25856* | Lemma for aaliou3 25864. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΊ = (π β (β€β₯βπ΄) β¦ ((2β-(!βπ΄)) Β· ((1 / 2)β(π β π΄)))) & β’ πΉ = (π β β β¦ (2β-(!βπ))) β β’ ((π΄ β β β§ π΅ β (β€β₯βπ΄)) β (πΉβπ΅) β (0(,](πΊβπ΅))) | ||
Theorem | aaliou3lem3 25857* | Lemma for aaliou3 25864. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΊ = (π β (β€β₯βπ΄) β¦ ((2β-(!βπ΄)) Β· ((1 / 2)β(π β π΄)))) & β’ πΉ = (π β β β¦ (2β-(!βπ))) β β’ (π΄ β β β (seqπ΄( + , πΉ) β dom β β§ Ξ£π β (β€β₯βπ΄)(πΉβπ) β β+ β§ Ξ£π β (β€β₯βπ΄)(πΉβπ) β€ (2 Β· (2β-(!βπ΄))))) | ||
Theorem | aaliou3lem8 25858* | Lemma for aaliou3 25864. (Contributed by Stefan O'Rear, 20-Nov-2014.) |
β’ ((π΄ β β β§ π΅ β β+) β βπ₯ β β (2 Β· (2β-(!β(π₯ + 1)))) β€ (π΅ / ((2β(!βπ₯))βπ΄))) | ||
Theorem | aaliou3lem4 25859* | Lemma for aaliou3 25864. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΉ = (π β β β¦ (2β-(!βπ))) & β’ πΏ = Ξ£π β β (πΉβπ) & β’ π» = (π β β β¦ Ξ£π β (1...π)(πΉβπ)) β β’ πΏ β β | ||
Theorem | aaliou3lem5 25860* | Lemma for aaliou3 25864. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΉ = (π β β β¦ (2β-(!βπ))) & β’ πΏ = Ξ£π β β (πΉβπ) & β’ π» = (π β β β¦ Ξ£π β (1...π)(πΉβπ)) β β’ (π΄ β β β (π»βπ΄) β β) | ||
Theorem | aaliou3lem6 25861* | Lemma for aaliou3 25864. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΉ = (π β β β¦ (2β-(!βπ))) & β’ πΏ = Ξ£π β β (πΉβπ) & β’ π» = (π β β β¦ Ξ£π β (1...π)(πΉβπ)) β β’ (π΄ β β β ((π»βπ΄) Β· (2β(!βπ΄))) β β€) | ||
Theorem | aaliou3lem7 25862* | Lemma for aaliou3 25864. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ πΉ = (π β β β¦ (2β-(!βπ))) & β’ πΏ = Ξ£π β β (πΉβπ) & β’ π» = (π β β β¦ Ξ£π β (1...π)(πΉβπ)) β β’ (π΄ β β β ((π»βπ΄) β πΏ β§ (absβ(πΏ β (π»βπ΄))) β€ (2 Β· (2β-(!β(π΄ + 1)))))) | ||
Theorem | aaliou3lem9 25863* | Example of a "Liouville number", a very simple definable transcendental real. (Contributed by Stefan O'Rear, 20-Nov-2014.) |
β’ πΉ = (π β β β¦ (2β-(!βπ))) & β’ πΏ = Ξ£π β β (πΉβπ) & β’ π» = (π β β β¦ Ξ£π β (1...π)(πΉβπ)) β β’ Β¬ πΏ β πΈ | ||
Theorem | aaliou3 25864 | Example of a "Liouville number", a very simple definable transcendental real. (Contributed by Stefan O'Rear, 23-Nov-2014.) |
β’ Ξ£π β β (2β-(!βπ)) β πΈ | ||
Syntax | ctayl 25865 | Taylor polynomial of a function. |
class Tayl | ||
Syntax | cana 25866 | The class of analytic functions. |
class Ana | ||
Definition | df-tayl 25867* | Define the Taylor polynomial or Taylor series of a function. TODO-AV: π β (β0 βͺ {+β}) should be replaced by π β β0*. (Contributed by Mario Carneiro, 30-Dec-2016.) |
β’ Tayl = (π β {β, β}, π β (β βpm π ) β¦ (π β (β0 βͺ {+β}), π β β© π β ((0[,]π) β© β€)dom ((π Dπ π)βπ) β¦ βͺ π₯ β β ({π₯} Γ (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ π)βπ)βπ) / (!βπ)) Β· ((π₯ β π)βπ))))))) | ||
Definition | df-ana 25868* | Define the set of analytic functions, which are functions such that the Taylor series of the function at each point converges to the function in some neighborhood of the point. (Contributed by Mario Carneiro, 31-Dec-2016.) |
β’ Ana = (π β {β, β} β¦ {π β (β βpm π ) β£ βπ₯ β dom π π₯ β ((intβ((TopOpenββfld) βΎt π ))βdom (π β© (+β(π Tayl π)π₯)))}) | ||
Theorem | taylfvallem1 25869* | Lemma for taylfval 25871. (Contributed by Mario Carneiro, 30-Dec-2016.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β (π β β0 β¨ π = +β)) & β’ ((π β§ π β ((0[,]π) β© β€)) β π΅ β dom ((π Dπ πΉ)βπ)) β β’ (((π β§ π β β) β§ π β ((0[,]π) β© β€)) β (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π β π΅)βπ)) β β) | ||
Theorem | taylfvallem 25870* | Lemma for taylfval 25871. (Contributed by Mario Carneiro, 30-Dec-2016.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β (π β β0 β¨ π = +β)) & β’ ((π β§ π β ((0[,]π) β© β€)) β π΅ β dom ((π Dπ πΉ)βπ)) β β’ ((π β§ π β β) β (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π β π΅)βπ)))) β β) | ||
Theorem | taylfval 25871* |
Define the Taylor polynomial of a function. The constant Tayl is a
function of five arguments: π is the base set with respect to
evaluate the derivatives (generally β or
β), πΉ is the
function we are approximating, at point π΅, to order π. The
result is a polynomial function of π₯.
This "extended" version of taylpfval 25877 additionally handles the case π = +β, in which case this is not a polynomial but an infinite series, the Taylor series of the function. (Contributed by Mario Carneiro, 30-Dec-2016.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β (π β β0 β¨ π = +β)) & β’ ((π β§ π β ((0[,]π) β© β€)) β π΅ β dom ((π Dπ πΉ)βπ)) & β’ π = (π(π Tayl πΉ)π΅) β β’ (π β π = βͺ π₯ β β ({π₯} Γ (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))))) | ||
Theorem | eltayl 25872* | Value of the Taylor series as a relation (elementhood in the domain here expresses that the series is convergent). (Contributed by Mario Carneiro, 30-Dec-2016.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β (π β β0 β¨ π = +β)) & β’ ((π β§ π β ((0[,]π) β© β€)) β π΅ β dom ((π Dπ πΉ)βπ)) & β’ π = (π(π Tayl πΉ)π΅) β β’ (π β (πππ β (π β β β§ π β (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π β π΅)βπ))))))) | ||
Theorem | taylf 25873* | The Taylor series defines a function on a subset of the complex numbers. (Contributed by Mario Carneiro, 30-Dec-2016.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β (π β β0 β¨ π = +β)) & β’ ((π β§ π β ((0[,]π) β© β€)) β π΅ β dom ((π Dπ πΉ)βπ)) & β’ π = (π(π Tayl πΉ)π΅) β β’ (π β π:dom πβΆβ) | ||
Theorem | tayl0 25874* | The Taylor series is always defined at the basepoint, with value equal to the value of the function. (Contributed by Mario Carneiro, 30-Dec-2016.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β (π β β0 β¨ π = +β)) & β’ ((π β§ π β ((0[,]π) β© β€)) β π΅ β dom ((π Dπ πΉ)βπ)) & β’ π = (π(π Tayl πΉ)π΅) β β’ (π β (π΅ β dom π β§ (πβπ΅) = (πΉβπ΅))) | ||
Theorem | taylplem1 25875* | Lemma for taylpfval 25877 and similar theorems. (Contributed by Mario Carneiro, 31-Dec-2016.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β π β β0) & β’ (π β π΅ β dom ((π Dπ πΉ)βπ)) β β’ ((π β§ π β ((0[,]π) β© β€)) β π΅ β dom ((π Dπ πΉ)βπ)) | ||
Theorem | taylplem2 25876* | Lemma for taylpfval 25877 and similar theorems. (Contributed by Mario Carneiro, 31-Dec-2016.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β π β β0) & β’ (π β π΅ β dom ((π Dπ πΉ)βπ)) β β’ (((π β§ π β β) β§ π β (0...π)) β (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π β π΅)βπ)) β β) | ||
Theorem | taylpfval 25877* | Define the Taylor polynomial of a function. The constant Tayl is a function of five arguments: π is the base set with respect to evaluate the derivatives (generally β or β), πΉ is the function we are approximating, at point π΅, to order π. The result is a polynomial function of π₯. (Contributed by Mario Carneiro, 31-Dec-2016.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β π β β0) & β’ (π β π΅ β dom ((π Dπ πΉ)βπ)) & β’ π = (π(π Tayl πΉ)π΅) β β’ (π β π = (π₯ β β β¦ Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))) | ||
Theorem | taylpf 25878 | The Taylor polynomial is a function on the complex numbers (even if the base set of the original function is the reals). (Contributed by Mario Carneiro, 31-Dec-2016.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β π β β0) & β’ (π β π΅ β dom ((π Dπ πΉ)βπ)) & β’ π = (π(π Tayl πΉ)π΅) β β’ (π β π:ββΆβ) | ||
Theorem | taylpval 25879* | Value of the Taylor polynomial. (Contributed by Mario Carneiro, 31-Dec-2016.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β π β β0) & β’ (π β π΅ β dom ((π Dπ πΉ)βπ)) & β’ π = (π(π Tayl πΉ)π΅) & β’ (π β π β β) β β’ (π β (πβπ) = Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π β π΅)βπ))) | ||
Theorem | taylply2 25880* | The Taylor polynomial is a polynomial of degree (at most) π. This version of taylply 25881 shows that the coefficients of π are in a subring of the complex numbers. (Contributed by Mario Carneiro, 1-Jan-2017.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β π β β0) & β’ (π β π΅ β dom ((π Dπ πΉ)βπ)) & β’ π = (π(π Tayl πΉ)π΅) & β’ (π β π· β (SubRingββfld)) & β’ (π β π΅ β π·) & β’ ((π β§ π β (0...π)) β ((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) β π·) β β’ (π β (π β (Polyβπ·) β§ (degβπ) β€ π)) | ||
Theorem | taylply 25881 | The Taylor polynomial is a polynomial of degree (at most) π. (Contributed by Mario Carneiro, 31-Dec-2016.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β π β β0) & β’ (π β π΅ β dom ((π Dπ πΉ)βπ)) & β’ π = (π(π Tayl πΉ)π΅) β β’ (π β (π β (Polyββ) β§ (degβπ) β€ π)) | ||
Theorem | dvtaylp 25882 | The derivative of the Taylor polynomial is the Taylor polynomial of the derivative of the function. (Contributed by Mario Carneiro, 31-Dec-2016.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β π β β0) & β’ (π β π΅ β dom ((π Dπ πΉ)β(π + 1))) β β’ (π β (β D ((π + 1)(π Tayl πΉ)π΅)) = (π(π Tayl (π D πΉ))π΅)) | ||
Theorem | dvntaylp 25883 | The π-th derivative of the Taylor polynomial is the Taylor polynomial of the π-th derivative of the function. (Contributed by Mario Carneiro, 1-Jan-2017.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β π β β0) & β’ (π β π β β0) & β’ (π β π΅ β dom ((π Dπ πΉ)β(π + π))) β β’ (π β ((β Dπ ((π + π)(π Tayl πΉ)π΅))βπ) = (π(π Tayl ((π Dπ πΉ)βπ))π΅)) | ||
Theorem | dvntaylp0 25884 | The first π derivatives of the Taylor polynomial at π΅ match the derivatives of the function from which it is derived. (Contributed by Mario Carneiro, 1-Jan-2017.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β π β (0...π)) & β’ (π β π΅ β dom ((π Dπ πΉ)βπ)) & β’ π = (π(π Tayl πΉ)π΅) β β’ (π β (((β Dπ π)βπ)βπ΅) = (((π Dπ πΉ)βπ)βπ΅)) | ||
Theorem | taylthlem1 25885* | Lemma for taylth 25887. This is the main part of Taylor's theorem, except for the induction step, which is supposed to be proven using L'HΓ΄pital's rule. However, since our proof of L'HΓ΄pital assumes that π = β, we can only do this part generically, and for taylth 25887 itself we must restrict to β. (Contributed by Mario Carneiro, 1-Jan-2017.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β dom ((π Dπ πΉ)βπ) = π΄) & β’ (π β π β β) & β’ (π β π΅ β π΄) & β’ π = (π(π Tayl πΉ)π΅) & β’ π = (π₯ β (π΄ β {π΅}) β¦ (((πΉβπ₯) β (πβπ₯)) / ((π₯ β π΅)βπ))) & β’ ((π β§ (π β (1..^π) β§ 0 β ((π¦ β (π΄ β {π΅}) β¦ (((((π Dπ πΉ)β(π β π))βπ¦) β (((β Dπ π)β(π β π))βπ¦)) / ((π¦ β π΅)βπ))) limβ π΅))) β 0 β ((π₯ β (π΄ β {π΅}) β¦ (((((π Dπ πΉ)β(π β (π + 1)))βπ₯) β (((β Dπ π)β(π β (π + 1)))βπ₯)) / ((π₯ β π΅)β(π + 1)))) limβ π΅)) β β’ (π β 0 β (π limβ π΅)) | ||
Theorem | taylthlem2 25886* | Lemma for taylth 25887. (Contributed by Mario Carneiro, 1-Jan-2017.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β β) & β’ (π β dom ((β Dπ πΉ)βπ) = π΄) & β’ (π β π β β) & β’ (π β π΅ β π΄) & β’ π = (π(β Tayl πΉ)π΅) & β’ (π β π β (1..^π)) & β’ (π β 0 β ((π₯ β (π΄ β {π΅}) β¦ (((((β Dπ πΉ)β(π β π))βπ₯) β (((β Dπ π)β(π β π))βπ₯)) / ((π₯ β π΅)βπ))) limβ π΅)) β β’ (π β 0 β ((π₯ β (π΄ β {π΅}) β¦ (((((β Dπ πΉ)β(π β (π + 1)))βπ₯) β (((β Dπ π)β(π β (π + 1)))βπ₯)) / ((π₯ β π΅)β(π + 1)))) limβ π΅)) | ||
Theorem | taylth 25887* | Taylor's theorem. The Taylor polynomial of a π-times differentiable function is such that the error term goes to zero faster than (π₯ β π΅)βπ. This is Metamath 100 proof #35. (Contributed by Mario Carneiro, 1-Jan-2017.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β β) & β’ (π β dom ((β Dπ πΉ)βπ) = π΄) & β’ (π β π β β) & β’ (π β π΅ β π΄) & β’ π = (π(β Tayl πΉ)π΅) & β’ π = (π₯ β (π΄ β {π΅}) β¦ (((πΉβπ₯) β (πβπ₯)) / ((π₯ β π΅)βπ))) β β’ (π β 0 β (π limβ π΅)) | ||
Syntax | culm 25888 | Extend class notation to include the uniform convergence predicate. |
class βπ’ | ||
Definition | df-ulm 25889* | Define the uniform convergence of a sequence of functions. Here πΉ(βπ’βπ)πΊ if πΉ is a sequence of functions πΉ(π), π β β defined on π and πΊ is a function on π, and for every 0 < π₯ there is a π such that the functions πΉ(π) for π β€ π are all uniformly within π₯ of πΊ on the domain π. Compare with df-clim 15432. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ βπ’ = (π β V β¦ {β¨π, π¦β© β£ βπ β β€ (π:(β€β₯βπ)βΆ(β βm π ) β§ π¦:π βΆβ β§ βπ₯ β β+ βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πβπ)βπ§) β (π¦βπ§))) < π₯)}) | ||
Theorem | ulmrel 25890 | The uniform limit relation is a relation. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ Rel (βπ’βπ) | ||
Theorem | ulmscl 25891 | Closure of the base set in a uniform limit. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ (πΉ(βπ’βπ)πΊ β π β V) | ||
Theorem | ulmval 25892* | Express the predicate: The sequence of functions πΉ converges uniformly to πΊ on π. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ (π β π β (πΉ(βπ’βπ)πΊ β βπ β β€ (πΉ:(β€β₯βπ)βΆ(β βm π) β§ πΊ:πβΆβ β§ βπ₯ β β+ βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < π₯))) | ||
Theorem | ulmcl 25893 | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ (πΉ(βπ’βπ)πΊ β πΊ:πβΆβ) | ||
Theorem | ulmf 25894* | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ (πΉ(βπ’βπ)πΊ β βπ β β€ πΉ:(β€β₯βπ)βΆ(β βm π)) | ||
Theorem | ulmpm 25895 | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ (πΉ(βπ’βπ)πΊ β πΉ β ((β βm π) βpm β€)) | ||
Theorem | ulmf2 25896 | Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 18-Mar-2015.) |
β’ ((πΉ Fn π β§ πΉ(βπ’βπ)πΊ) β πΉ:πβΆ(β βm π)) | ||
Theorem | ulm2 25897* | Simplify ulmval 25892 when πΉ and πΊ are known to be functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆ(β βm π)) & β’ ((π β§ (π β π β§ π§ β π)) β ((πΉβπ)βπ§) = π΅) & β’ ((π β§ π§ β π) β (πΊβπ§) = π΄) & β’ (π β πΊ:πβΆβ) & β’ (π β π β π) β β’ (π β (πΉ(βπ’βπ)πΊ β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(π΅ β π΄)) < π₯)) | ||
Theorem | ulmi 25898* | The uniform limit property. (Contributed by Mario Carneiro, 27-Feb-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆ(β βm π)) & β’ ((π β§ (π β π β§ π§ β π)) β ((πΉβπ)βπ§) = π΅) & β’ ((π β§ π§ β π) β (πΊβπ§) = π΄) & β’ (π β πΉ(βπ’βπ)πΊ) & β’ (π β πΆ β β+) β β’ (π β βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(π΅ β π΄)) < πΆ) | ||
Theorem | ulmclm 25899* | A uniform limit of functions converges pointwise. (Contributed by Mario Carneiro, 27-Feb-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆ(β βm π)) & β’ (π β π΄ β π) & β’ (π β π» β π) & β’ ((π β§ π β π) β ((πΉβπ)βπ΄) = (π»βπ)) & β’ (π β πΉ(βπ’βπ)πΊ) β β’ (π β π» β (πΊβπ΄)) | ||
Theorem | ulmres 25900 | A sequence of functions converges iff the tail of the sequence converges (for any finite cutoff). (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ (π β πΉ:πβΆ(β βm π)) β β’ (π β (πΉ(βπ’βπ)πΊ β (πΉ βΎ π)(βπ’βπ)πΊ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |