![]() |
Metamath
Proof Explorer Theorem List (p. 156 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 | climuni 15501 | An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 2-Oct-1999.) (Proof shortened by Mario Carneiro, 31-Jan-2014.) |
β’ ((πΉ β π΄ β§ πΉ β π΅) β π΄ = π΅) | ||
Theorem | fclim 15502 | The limit relation is function-like, and with codomain the complex numbers. (Contributed by Mario Carneiro, 31-Jan-2014.) |
β’ β :dom β βΆβ | ||
Theorem | climdm 15503 | Two ways to express that a function has a limit. (The expression ( β βπΉ) is sometimes useful as a shorthand for "the unique limit of the function πΉ"). (Contributed by Mario Carneiro, 18-Mar-2014.) |
β’ (πΉ β dom β β πΉ β ( β βπΉ)) | ||
Theorem | climeu 15504* | An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.) |
β’ (πΉ β π΄ β β!π₯ πΉ β π₯) | ||
Theorem | climreu 15505* | An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.) |
β’ (πΉ β π΄ β β!π₯ β β πΉ β π₯) | ||
Theorem | climmo 15506* | An infinite sequence of complex numbers converges to at most one limit. (Contributed by Mario Carneiro, 13-Jul-2013.) |
β’ β*π₯ πΉ β π₯ | ||
Theorem | rlimres 15507 | The restriction of a function converges if the original converges. (Contributed by Mario Carneiro, 16-Sep-2014.) |
β’ (πΉ βπ π΄ β (πΉ βΎ π΅) βπ π΄) | ||
Theorem | lo1res 15508 | The restriction of an eventually upper bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ (πΉ β β€π(1) β (πΉ βΎ π΄) β β€π(1)) | ||
Theorem | o1res 15509 | The restriction of an eventually bounded function is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) (Proof shortened by Mario Carneiro, 26-May-2016.) |
β’ (πΉ β π(1) β (πΉ βΎ π΄) β π(1)) | ||
Theorem | rlimres2 15510* | The restriction of a function converges if the original converges. (Contributed by Mario Carneiro, 16-Sep-2014.) |
β’ (π β π΄ β π΅) & β’ (π β (π₯ β π΅ β¦ πΆ) βπ π·) β β’ (π β (π₯ β π΄ β¦ πΆ) βπ π·) | ||
Theorem | lo1res2 15511* | The restriction of a function is eventually bounded if the original is. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ (π β π΄ β π΅) & β’ (π β (π₯ β π΅ β¦ πΆ) β β€π(1)) β β’ (π β (π₯ β π΄ β¦ πΆ) β β€π(1)) | ||
Theorem | o1res2 15512* | The restriction of a function is eventually bounded if the original is. (Contributed by Mario Carneiro, 21-May-2016.) |
β’ (π β π΄ β π΅) & β’ (π β (π₯ β π΅ β¦ πΆ) β π(1)) β β’ (π β (π₯ β π΄ β¦ πΆ) β π(1)) | ||
Theorem | lo1resb 15513 | The restriction of a function to an unbounded-above interval is eventually upper bounded iff the original is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (πΉ β β€π(1) β (πΉ βΎ (π΅[,)+β)) β β€π(1))) | ||
Theorem | rlimresb 15514 | The restriction of a function to an unbounded-above interval converges iff the original converges. (Contributed by Mario Carneiro, 16-Sep-2014.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (πΉ βπ πΆ β (πΉ βΎ (π΅[,)+β)) βπ πΆ)) | ||
Theorem | o1resb 15515 | The restriction of a function to an unbounded-above interval is eventually bounded iff the original is eventually bounded. (Contributed by Mario Carneiro, 9-Apr-2016.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (πΉ β π(1) β (πΉ βΎ (π΅[,)+β)) β π(1))) | ||
Theorem | climeq 15516* | Two functions that are eventually equal to one another have the same limit. (Contributed by Mario Carneiro, 5-Nov-2013.) (Revised by Mario Carneiro, 31-Jan-2014.) |
β’ π = (β€β₯βπ) & β’ (π β πΉ β π) & β’ (π β πΊ β π) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = (πΊβπ)) β β’ (π β (πΉ β π΄ β πΊ β π΄)) | ||
Theorem | lo1eq 15517* | Two functions that are eventually equal to one another are eventually bounded if one of them is. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ (π β π· β β) & β’ ((π β§ (π₯ β π΄ β§ π· β€ π₯)) β π΅ = πΆ) β β’ (π β ((π₯ β π΄ β¦ π΅) β β€π(1) β (π₯ β π΄ β¦ πΆ) β β€π(1))) | ||
Theorem | rlimeq 15518* | Two functions that are eventually equal to one another have the same limit. (Contributed by Mario Carneiro, 16-Sep-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ (π β π· β β) & β’ ((π β§ (π₯ β π΄ β§ π· β€ π₯)) β π΅ = πΆ) β β’ (π β ((π₯ β π΄ β¦ π΅) βπ πΈ β (π₯ β π΄ β¦ πΆ) βπ πΈ)) | ||
Theorem | o1eq 15519* | Two functions that are eventually equal to one another are eventually bounded if one of them is. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ (π β π· β β) & β’ ((π β§ (π₯ β π΄ β§ π· β€ π₯)) β π΅ = πΆ) β β’ (π β ((π₯ β π΄ β¦ π΅) β π(1) β (π₯ β π΄ β¦ πΆ) β π(1))) | ||
Theorem | climmpt 15520* | Exhibit a function πΊ with the same convergence properties as the not-quite-function πΉ. (Contributed by Mario Carneiro, 31-Jan-2014.) |
β’ π = (β€β₯βπ) & β’ πΊ = (π β π β¦ (πΉβπ)) β β’ ((π β β€ β§ πΉ β π) β (πΉ β π΄ β πΊ β π΄)) | ||
Theorem | 2clim 15521* | If two sequences converge to each other, they converge to the same limit. (Contributed by NM, 24-Dec-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ β π) & β’ ((π β§ π β π) β (πΊβπ) β β) & β’ (π β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β (πΊβπ))) < π₯) & β’ (π β πΉ β π΄) β β’ (π β πΊ β π΄) | ||
Theorem | climmpt2 15522* | Relate an integer limit on a not-quite-function to a real limit. (Contributed by Mario Carneiro, 17-Sep-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π) & β’ ((π β§ π β π) β (πΉβπ) β β) β β’ (π β (πΉ β π΄ β (π β π β¦ (πΉβπ)) βπ π΄)) | ||
Theorem | climshftlem 15523 | A shifted function converges if the original function converges. (Contributed by Mario Carneiro, 5-Nov-2013.) |
β’ πΉ β V β β’ (π β β€ β (πΉ β π΄ β (πΉ shift π) β π΄)) | ||
Theorem | climres 15524 | A function restricted to upper integers converges iff the original function converges. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 31-Jan-2014.) |
β’ ((π β β€ β§ πΉ β π) β ((πΉ βΎ (β€β₯βπ)) β π΄ β πΉ β π΄)) | ||
Theorem | climshft 15525 | A shifted function converges iff the original function converges. (Contributed by NM, 16-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.) |
β’ ((π β β€ β§ πΉ β π) β ((πΉ shift π) β π΄ β πΉ β π΄)) | ||
Theorem | serclim0 15526 | The zero series converges to zero. (Contributed by Paul Chapman, 9-Feb-2008.) (Proof shortened by Mario Carneiro, 31-Jan-2014.) |
β’ (π β β€ β seqπ( + , ((β€β₯βπ) Γ {0})) β 0) | ||
Theorem | rlimcld2 15527* | If π· is a closed set in the topology of the complex numbers (stated here in basic form), and all the elements of the sequence lie in π·, then the limit of the sequence also lies in π·. (Contributed by Mario Carneiro, 10-May-2016.) |
β’ (π β sup(π΄, β*, < ) = +β) & β’ (π β (π₯ β π΄ β¦ π΅) βπ πΆ) & β’ (π β π· β β) & β’ ((π β§ π¦ β (β β π·)) β π β β+) & β’ (((π β§ π¦ β (β β π·)) β§ π§ β π·) β π β€ (absβ(π§ β π¦))) & β’ ((π β§ π₯ β π΄) β π΅ β π·) β β’ (π β πΆ β π·) | ||
Theorem | rlimrege0 15528* | The limit of a sequence of complex numbers with nonnegative real part has nonnegative real part. (Contributed by Mario Carneiro, 10-May-2016.) |
β’ (π β sup(π΄, β*, < ) = +β) & β’ (π β (π₯ β π΄ β¦ π΅) βπ πΆ) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β 0 β€ (ββπ΅)) β β’ (π β 0 β€ (ββπΆ)) | ||
Theorem | rlimrecl 15529* | The limit of a real sequence is real. (Contributed by Mario Carneiro, 9-May-2016.) |
β’ (π β sup(π΄, β*, < ) = +β) & β’ (π β (π₯ β π΄ β¦ π΅) βπ πΆ) & β’ ((π β§ π₯ β π΄) β π΅ β β) β β’ (π β πΆ β β) | ||
Theorem | rlimge0 15530* | The limit of a sequence of nonnegative reals is nonnegative. (Contributed by Mario Carneiro, 10-May-2016.) |
β’ (π β sup(π΄, β*, < ) = +β) & β’ (π β (π₯ β π΄ β¦ π΅) βπ πΆ) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β 0 β€ π΅) β β’ (π β 0 β€ πΆ) | ||
Theorem | climshft2 15531* | A shifted function converges iff the original function converges. (Contributed by Paul Chapman, 21-Nov-2007.) (Revised by Mario Carneiro, 6-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΎ β β€) & β’ (π β πΉ β π) & β’ (π β πΊ β π) & β’ ((π β§ π β π) β (πΊβ(π + πΎ)) = (πΉβπ)) β β’ (π β (πΉ β π΄ β πΊ β π΄)) | ||
Theorem | climrecl 15532* | The limit of a convergent real sequence is real. Corollary 12-2.5 of [Gleason] p. 172. (Contributed by NM, 10-Sep-2005.) (Proof shortened by Mario Carneiro, 10-May-2016.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ ((π β§ π β π) β (πΉβπ) β β) β β’ (π β π΄ β β) | ||
Theorem | climge0 15533* | A nonnegative sequence converges to a nonnegative number. (Contributed by NM, 11-Sep-2005.) (Proof shortened by Mario Carneiro, 10-May-2016.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β 0 β€ (πΉβπ)) β β’ (π β 0 β€ π΄) | ||
Theorem | climabs0 15534* | Convergence to zero of the absolute value is equivalent to convergence to zero. (Contributed by NM, 8-Jul-2008.) (Revised by Mario Carneiro, 31-Jan-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π) & β’ (π β πΊ β π) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) = (absβ(πΉβπ))) β β’ (π β (πΉ β 0 β πΊ β 0)) | ||
Theorem | o1co 15535* | Sufficient condition for transforming the index set of an eventually bounded function. (Contributed by Mario Carneiro, 12-May-2016.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β πΉ β π(1)) & β’ (π β πΊ:π΅βΆπ΄) & β’ (π β π΅ β β) & β’ ((π β§ π β β) β βπ₯ β β βπ¦ β π΅ (π₯ β€ π¦ β π β€ (πΊβπ¦))) β β’ (π β (πΉ β πΊ) β π(1)) | ||
Theorem | o1compt 15536* | Sufficient condition for transforming the index set of an eventually bounded function. (Contributed by Mario Carneiro, 12-May-2016.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β πΉ β π(1)) & β’ ((π β§ π¦ β π΅) β πΆ β π΄) & β’ (π β π΅ β β) & β’ ((π β§ π β β) β βπ₯ β β βπ¦ β π΅ (π₯ β€ π¦ β π β€ πΆ)) β β’ (π β (πΉ β (π¦ β π΅ β¦ πΆ)) β π(1)) | ||
Theorem | rlimcn1 15537* | Image of a limit under a continuous map. (Contributed by Mario Carneiro, 17-Sep-2014.) |
β’ (π β πΊ:π΄βΆπ) & β’ (π β πΆ β π) & β’ (π β πΊ βπ πΆ) & β’ (π β πΉ:πβΆβ) & β’ ((π β§ π₯ β β+) β βπ¦ β β+ βπ§ β π ((absβ(π§ β πΆ)) < π¦ β (absβ((πΉβπ§) β (πΉβπΆ))) < π₯)) β β’ (π β (πΉ β πΊ) βπ (πΉβπΆ)) | ||
Theorem | rlimcn1b 15538* | Image of a limit under a continuous map. (Contributed by Mario Carneiro, 10-May-2016.) |
β’ ((π β§ π β π΄) β π΅ β π) & β’ (π β πΆ β π) & β’ (π β (π β π΄ β¦ π΅) βπ πΆ) & β’ (π β πΉ:πβΆβ) & β’ ((π β§ π₯ β β+) β βπ¦ β β+ βπ§ β π ((absβ(π§ β πΆ)) < π¦ β (absβ((πΉβπ§) β (πΉβπΆ))) < π₯)) β β’ (π β (π β π΄ β¦ (πΉβπ΅)) βπ (πΉβπΆ)) | ||
Theorem | rlimcn3 15539* | Image of a limit under a continuous map, two-arg version. Originally a subproof of rlimcn2 15540. (Contributed by SN, 27-Sep-2024.) |
β’ ((π β§ π§ β π΄) β π΅ β π) & β’ ((π β§ π§ β π΄) β πΆ β π) & β’ ((π β§ π§ β π΄) β (π΅πΉπΆ) β β) & β’ (π β (π πΉπ) β β) & β’ (π β (π§ β π΄ β¦ π΅) βπ π ) & β’ (π β (π§ β π΄ β¦ πΆ) βπ π) & β’ ((π β§ π₯ β β+) β βπ β β+ βπ β β+ βπ’ β π βπ£ β π (((absβ(π’ β π )) < π β§ (absβ(π£ β π)) < π ) β (absβ((π’πΉπ£) β (π πΉπ))) < π₯)) β β’ (π β (π§ β π΄ β¦ (π΅πΉπΆ)) βπ (π πΉπ)) | ||
Theorem | rlimcn2 15540* | Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 17-Sep-2014.) |
β’ ((π β§ π§ β π΄) β π΅ β π) & β’ ((π β§ π§ β π΄) β πΆ β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π§ β π΄ β¦ π΅) βπ π ) & β’ (π β (π§ β π΄ β¦ πΆ) βπ π) & β’ (π β πΉ:(π Γ π)βΆβ) & β’ ((π β§ π₯ β β+) β βπ β β+ βπ β β+ βπ’ β π βπ£ β π (((absβ(π’ β π )) < π β§ (absβ(π£ β π)) < π ) β (absβ((π’πΉπ£) β (π πΉπ))) < π₯)) β β’ (π β (π§ β π΄ β¦ (π΅πΉπΆ)) βπ (π πΉπ)) | ||
Theorem | climcn1 15541* | Image of a limit under a continuous map. (Contributed by Mario Carneiro, 31-Jan-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π΄ β π΅) & β’ ((π β§ π§ β π΅) β (πΉβπ§) β β) & β’ (π β πΊ β π΄) & β’ (π β π» β π) & β’ ((π β§ π₯ β β+) β βπ¦ β β+ βπ§ β π΅ ((absβ(π§ β π΄)) < π¦ β (absβ((πΉβπ§) β (πΉβπ΄))) < π₯)) & β’ ((π β§ π β π) β (πΊβπ) β π΅) & β’ ((π β§ π β π) β (π»βπ) = (πΉβ(πΊβπ))) β β’ (π β π» β (πΉβπ΄)) | ||
Theorem | climcn2 15542* | Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 31-Jan-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π΄ β πΆ) & β’ (π β π΅ β π·) & β’ ((π β§ (π’ β πΆ β§ π£ β π·)) β (π’πΉπ£) β β) & β’ (π β πΊ β π΄) & β’ (π β π» β π΅) & β’ (π β πΎ β π) & β’ ((π β§ π₯ β β+) β βπ¦ β β+ βπ§ β β+ βπ’ β πΆ βπ£ β π· (((absβ(π’ β π΄)) < π¦ β§ (absβ(π£ β π΅)) < π§) β (absβ((π’πΉπ£) β (π΄πΉπ΅))) < π₯)) & β’ ((π β§ π β π) β (πΊβπ) β πΆ) & β’ ((π β§ π β π) β (π»βπ) β π·) & β’ ((π β§ π β π) β (πΎβπ) = ((πΊβπ)πΉ(π»βπ))) β β’ (π β πΎ β (π΄πΉπ΅)) | ||
Theorem | addcn2 15543* | Complex number addition is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (We write out the definition directly because df-cn 22952 and df-cncf 24619 are not yet available to us. See addcn 24602 for the abbreviated version.) (Contributed by Mario Carneiro, 31-Jan-2014.) |
β’ ((π΄ β β+ β§ π΅ β β β§ πΆ β β) β βπ¦ β β+ βπ§ β β+ βπ’ β β βπ£ β β (((absβ(π’ β π΅)) < π¦ β§ (absβ(π£ β πΆ)) < π§) β (absβ((π’ + π£) β (π΅ + πΆ))) < π΄)) | ||
Theorem | subcn2 15544* | Complex number subtraction is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by Mario Carneiro, 31-Jan-2014.) |
β’ ((π΄ β β+ β§ π΅ β β β§ πΆ β β) β βπ¦ β β+ βπ§ β β+ βπ’ β β βπ£ β β (((absβ(π’ β π΅)) < π¦ β§ (absβ(π£ β πΆ)) < π§) β (absβ((π’ β π£) β (π΅ β πΆ))) < π΄)) | ||
Theorem | mulcn2 15545* | Complex number multiplication is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by Mario Carneiro, 31-Jan-2014.) |
β’ ((π΄ β β+ β§ π΅ β β β§ πΆ β β) β βπ¦ β β+ βπ§ β β+ βπ’ β β βπ£ β β (((absβ(π’ β π΅)) < π¦ β§ (absβ(π£ β πΆ)) < π§) β (absβ((π’ Β· π£) β (π΅ Β· πΆ))) < π΄)) | ||
Theorem | reccn2 15546* | The reciprocal function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) (Revised by Mario Carneiro, 22-Sep-2014.) |
β’ π = (if(1 β€ ((absβπ΄) Β· π΅), 1, ((absβπ΄) Β· π΅)) Β· ((absβπ΄) / 2)) β β’ ((π΄ β (β β {0}) β§ π΅ β β+) β βπ¦ β β+ βπ§ β (β β {0})((absβ(π§ β π΄)) < π¦ β (absβ((1 / π§) β (1 / π΄))) < π΅)) | ||
Theorem | cn1lem 15547* | A sufficient condition for a function to be continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ πΉ:ββΆβ & β’ ((π§ β β β§ π΄ β β) β (absβ((πΉβπ§) β (πΉβπ΄))) β€ (absβ(π§ β π΄))) β β’ ((π΄ β β β§ π₯ β β+) β βπ¦ β β+ βπ§ β β ((absβ(π§ β π΄)) < π¦ β (absβ((πΉβπ§) β (πΉβπ΄))) < π₯)) | ||
Theorem | abscn2 15548* | The absolute value function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ ((π΄ β β β§ π₯ β β+) β βπ¦ β β+ βπ§ β β ((absβ(π§ β π΄)) < π¦ β (absβ((absβπ§) β (absβπ΄))) < π₯)) | ||
Theorem | cjcn2 15549* | The complex conjugate function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ ((π΄ β β β§ π₯ β β+) β βπ¦ β β+ βπ§ β β ((absβ(π§ β π΄)) < π¦ β (absβ((ββπ§) β (ββπ΄))) < π₯)) | ||
Theorem | recn2 15550* | The real part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ ((π΄ β β β§ π₯ β β+) β βπ¦ β β+ βπ§ β β ((absβ(π§ β π΄)) < π¦ β (absβ((ββπ§) β (ββπ΄))) < π₯)) | ||
Theorem | imcn2 15551* | The imaginary part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ ((π΄ β β β§ π₯ β β+) β βπ¦ β β+ βπ§ β β ((absβ(π§ β π΄)) < π¦ β (absβ((ββπ§) β (ββπ΄))) < π₯)) | ||
Theorem | climcn1lem 15552* | The limit of a continuous function, theorem form. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β πΉ β π΄) & β’ (π β πΊ β π) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ π»:ββΆβ & β’ ((π΄ β β β§ π₯ β β+) β βπ¦ β β+ βπ§ β β ((absβ(π§ β π΄)) < π¦ β (absβ((π»βπ§) β (π»βπ΄))) < π₯)) & β’ ((π β§ π β π) β (πΊβπ) = (π»β(πΉβπ))) β β’ (π β πΊ β (π»βπ΄)) | ||
Theorem | climabs 15553* | Limit of the absolute value of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β πΉ β π΄) & β’ (π β πΊ β π) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) = (absβ(πΉβπ))) β β’ (π β πΊ β (absβπ΄)) | ||
Theorem | climcj 15554* | Limit of the complex conjugate of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β πΉ β π΄) & β’ (π β πΊ β π) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) = (ββ(πΉβπ))) β β’ (π β πΊ β (ββπ΄)) | ||
Theorem | climre 15555* | Limit of the real part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β πΉ β π΄) & β’ (π β πΊ β π) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) = (ββ(πΉβπ))) β β’ (π β πΊ β (ββπ΄)) | ||
Theorem | climim 15556* | Limit of the imaginary part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β πΉ β π΄) & β’ (π β πΊ β π) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) = (ββ(πΉβπ))) β β’ (π β πΊ β (ββπ΄)) | ||
Theorem | rlimmptrcl 15557* | Reverse closure for a real limit. (Contributed by Mario Carneiro, 10-May-2016.) |
β’ ((π β§ π β π΄) β π΅ β π) & β’ (π β (π β π΄ β¦ π΅) βπ πΆ) β β’ ((π β§ π β π΄) β π΅ β β) | ||
Theorem | rlimabs 15558* | Limit of the absolute value of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by Mario Carneiro, 10-May-2016.) |
β’ ((π β§ π β π΄) β π΅ β π) & β’ (π β (π β π΄ β¦ π΅) βπ πΆ) β β’ (π β (π β π΄ β¦ (absβπ΅)) βπ (absβπΆ)) | ||
Theorem | rlimcj 15559* | Limit of the complex conjugate of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by Mario Carneiro, 10-May-2016.) |
β’ ((π β§ π β π΄) β π΅ β π) & β’ (π β (π β π΄ β¦ π΅) βπ πΆ) β β’ (π β (π β π΄ β¦ (ββπ΅)) βπ (ββπΆ)) | ||
Theorem | rlimre 15560* | Limit of the real part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by Mario Carneiro, 10-May-2016.) |
β’ ((π β§ π β π΄) β π΅ β π) & β’ (π β (π β π΄ β¦ π΅) βπ πΆ) β β’ (π β (π β π΄ β¦ (ββπ΅)) βπ (ββπΆ)) | ||
Theorem | rlimim 15561* | Limit of the imaginary part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by Mario Carneiro, 10-May-2016.) |
β’ ((π β§ π β π΄) β π΅ β π) & β’ (π β (π β π΄ β¦ π΅) βπ πΆ) β β’ (π β (π β π΄ β¦ (ββπ΅)) βπ (ββπΆ)) | ||
Theorem | o1of2 15562* | Show that a binary operation preserves eventual boundedness. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ ((π β β β§ π β β) β π β β) & β’ ((π₯ β β β§ π¦ β β) β (π₯π π¦) β β) & β’ (((π β β β§ π β β) β§ (π₯ β β β§ π¦ β β)) β (((absβπ₯) β€ π β§ (absβπ¦) β€ π) β (absβ(π₯π π¦)) β€ π)) β β’ ((πΉ β π(1) β§ πΊ β π(1)) β (πΉ βf π πΊ) β π(1)) | ||
Theorem | o1add 15563 | The sum of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) (Proof shortened by Fan Zheng, 14-Jul-2016.) |
β’ ((πΉ β π(1) β§ πΊ β π(1)) β (πΉ βf + πΊ) β π(1)) | ||
Theorem | o1mul 15564 | The product of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) (Proof shortened by Fan Zheng, 14-Jul-2016.) |
β’ ((πΉ β π(1) β§ πΊ β π(1)) β (πΉ βf Β· πΊ) β π(1)) | ||
Theorem | o1sub 15565 | The difference of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) (Proof shortened by Fan Zheng, 14-Jul-2016.) |
β’ ((πΉ β π(1) β§ πΊ β π(1)) β (πΉ βf β πΊ) β π(1)) | ||
Theorem | rlimo1 15566 | Any function with a finite limit is eventually bounded. (Contributed by Mario Carneiro, 18-Sep-2014.) |
β’ (πΉ βπ π΄ β πΉ β π(1)) | ||
Theorem | rlimdmo1 15567 | A convergent function is eventually bounded. (Contributed by Mario Carneiro, 12-May-2016.) |
β’ (πΉ β dom βπ β πΉ β π(1)) | ||
Theorem | o1rlimmul 15568 | The product of an eventually bounded function and a function of limit zero has limit zero. (Contributed by Mario Carneiro, 18-Sep-2014.) |
β’ ((πΉ β π(1) β§ πΊ βπ 0) β (πΉ βf Β· πΊ) βπ 0) | ||
Theorem | o1const 15569* | A constant function is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) (Proof shortened by Mario Carneiro, 26-May-2016.) |
β’ ((π΄ β β β§ π΅ β β) β (π₯ β π΄ β¦ π΅) β π(1)) | ||
Theorem | lo1const 15570* | A constant function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π΄ β β β§ π΅ β β) β (π₯ β π΄ β¦ π΅) β β€π(1)) | ||
Theorem | lo1mptrcl 15571* | Reverse closure for an eventually upper bounded function. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β β€π(1)) β β’ ((π β§ π₯ β π΄) β π΅ β β) | ||
Theorem | o1mptrcl 15572* | Reverse closure for an eventually bounded function. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β π(1)) β β’ ((π β§ π₯ β π΄) β π΅ β β) | ||
Theorem | o1add2 15573* | The sum of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β π(1)) & β’ (π β (π₯ β π΄ β¦ πΆ) β π(1)) β β’ (π β (π₯ β π΄ β¦ (π΅ + πΆ)) β π(1)) | ||
Theorem | o1mul2 15574* | The product of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β π(1)) & β’ (π β (π₯ β π΄ β¦ πΆ) β π(1)) β β’ (π β (π₯ β π΄ β¦ (π΅ Β· πΆ)) β π(1)) | ||
Theorem | o1sub2 15575* | The product of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β π(1)) & β’ (π β (π₯ β π΄ β¦ πΆ) β π(1)) β β’ (π β (π₯ β π΄ β¦ (π΅ β πΆ)) β π(1)) | ||
Theorem | lo1add 15576* | The sum of two eventually upper bounded functions is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β β€π(1)) & β’ (π β (π₯ β π΄ β¦ πΆ) β β€π(1)) β β’ (π β (π₯ β π΄ β¦ (π΅ + πΆ)) β β€π(1)) | ||
Theorem | lo1mul 15577* | The product of an eventually upper bounded function and a positive eventually upper bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β β€π(1)) & β’ (π β (π₯ β π΄ β¦ πΆ) β β€π(1)) & β’ ((π β§ π₯ β π΄) β 0 β€ π΅) β β’ (π β (π₯ β π΄ β¦ (π΅ Β· πΆ)) β β€π(1)) | ||
Theorem | lo1mul2 15578* | The product of an eventually upper bounded function and a positive eventually upper bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β β€π(1)) & β’ (π β (π₯ β π΄ β¦ πΆ) β β€π(1)) & β’ ((π β§ π₯ β π΄) β 0 β€ π΅) β β’ (π β (π₯ β π΄ β¦ (πΆ Β· π΅)) β β€π(1)) | ||
Theorem | o1dif 15579* | If the difference of two functions is eventually bounded, eventual boundedness of either one implies the other. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ (π β (π₯ β π΄ β¦ (π΅ β πΆ)) β π(1)) β β’ (π β ((π₯ β π΄ β¦ π΅) β π(1) β (π₯ β π΄ β¦ πΆ) β π(1))) | ||
Theorem | lo1sub 15580* | The difference of an eventually upper bounded function and an eventually bounded function is eventually upper bounded. The "correct" sharp result here takes the second function to be eventually lower bounded instead of just bounded, but our notation for this is simply (π₯ β π΄ β¦ -πΆ) β β€π(1), so it is just a special case of lo1add 15576. (Contributed by Mario Carneiro, 31-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ (π β (π₯ β π΄ β¦ π΅) β β€π(1)) & β’ (π β (π₯ β π΄ β¦ πΆ) β π(1)) β β’ (π β (π₯ β π΄ β¦ (π΅ β πΆ)) β β€π(1)) | ||
Theorem | climadd 15581* | Limit of the sum of two converging sequences. Proposition 12-2.1(a) of [Gleason] p. 168. (Contributed by NM, 24-Sep-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ (π β π» β π) & β’ (π β πΊ β π΅) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) β β) & β’ ((π β§ π β π) β (π»βπ) = ((πΉβπ) + (πΊβπ))) β β’ (π β π» β (π΄ + π΅)) | ||
Theorem | climmul 15582* | Limit of the product of two converging sequences. Proposition 12-2.1(c) of [Gleason] p. 168. (Contributed by NM, 27-Dec-2005.) (Proof shortened by Mario Carneiro, 1-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ (π β π» β π) & β’ (π β πΊ β π΅) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) β β) & β’ ((π β§ π β π) β (π»βπ) = ((πΉβπ) Β· (πΊβπ))) β β’ (π β π» β (π΄ Β· π΅)) | ||
Theorem | climsub 15583* | Limit of the difference of two converging sequences. Proposition 12-2.1(b) of [Gleason] p. 168. (Contributed by NM, 4-Aug-2007.) (Proof shortened by Mario Carneiro, 1-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ (π β π» β π) & β’ (π β πΊ β π΅) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) β β) & β’ ((π β§ π β π) β (π»βπ) = ((πΉβπ) β (πΊβπ))) β β’ (π β π» β (π΄ β π΅)) | ||
Theorem | climaddc1 15584* | Limit of a constant πΆ added to each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ (π β πΆ β β) & β’ (π β πΊ β π) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) = ((πΉβπ) + πΆ)) β β’ (π β πΊ β (π΄ + πΆ)) | ||
Theorem | climaddc2 15585* | Limit of a constant πΆ added to each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ (π β πΆ β β) & β’ (π β πΊ β π) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) = (πΆ + (πΉβπ))) β β’ (π β πΊ β (πΆ + π΄)) | ||
Theorem | climmulc2 15586* | Limit of a sequence multiplied by a constant πΆ. Corollary 12-2.2 of [Gleason] p. 171. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ (π β πΆ β β) & β’ (π β πΊ β π) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) = (πΆ Β· (πΉβπ))) β β’ (π β πΊ β (πΆ Β· π΄)) | ||
Theorem | climsubc1 15587* | Limit of a constant πΆ subtracted from each term of a sequence. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ (π β πΆ β β) & β’ (π β πΊ β π) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) = ((πΉβπ) β πΆ)) β β’ (π β πΊ β (π΄ β πΆ)) | ||
Theorem | climsubc2 15588* | Limit of a constant πΆ minus each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 9-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ (π β πΆ β β) & β’ (π β πΊ β π) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) = (πΆ β (πΉβπ))) β β’ (π β πΊ β (πΆ β π΄)) | ||
Theorem | climle 15589* | Comparison of the limits of two sequences. (Contributed by Paul Chapman, 10-Sep-2007.) (Revised by Mario Carneiro, 1-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ (π β πΊ β π΅) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) β β) & β’ ((π β§ π β π) β (πΉβπ) β€ (πΊβπ)) β β’ (π β π΄ β€ π΅) | ||
Theorem | climsqz 15590* | Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 3-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ (π β πΊ β π) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) β β) & β’ ((π β§ π β π) β (πΉβπ) β€ (πΊβπ)) & β’ ((π β§ π β π) β (πΊβπ) β€ π΄) β β’ (π β πΊ β π΄) | ||
Theorem | climsqz2 15591* | Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by NM, 14-Feb-2008.) (Revised by Mario Carneiro, 3-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ (π β πΊ β π) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) β€ (πΉβπ)) & β’ ((π β§ π β π) β π΄ β€ (πΊβπ)) β β’ (π β πΊ β π΄) | ||
Theorem | rlimadd 15592* | Limit of the sum of two converging functions. Proposition 12-2.1(a) of [Gleason] p. 168. (Contributed by Mario Carneiro, 22-Sep-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) βπ π·) & β’ (π β (π₯ β π΄ β¦ πΆ) βπ πΈ) β β’ (π β (π₯ β π΄ β¦ (π΅ + πΆ)) βπ (π· + πΈ)) | ||
Theorem | rlimaddOLD 15593* | Obsolete version of rlimadd 15592 as of 27-Sep-2024. (Contributed by Mario Carneiro, 22-Sep-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) βπ π·) & β’ (π β (π₯ β π΄ β¦ πΆ) βπ πΈ) β β’ (π β (π₯ β π΄ β¦ (π΅ + πΆ)) βπ (π· + πΈ)) | ||
Theorem | rlimsub 15594* | Limit of the difference of two converging functions. Proposition 12-2.1(b) of [Gleason] p. 168. (Contributed by Mario Carneiro, 22-Sep-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) βπ π·) & β’ (π β (π₯ β π΄ β¦ πΆ) βπ πΈ) β β’ (π β (π₯ β π΄ β¦ (π΅ β πΆ)) βπ (π· β πΈ)) | ||
Theorem | rlimmul 15595* | Limit of the product of two converging functions. Proposition 12-2.1(c) of [Gleason] p. 168. (Contributed by Mario Carneiro, 22-Sep-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) βπ π·) & β’ (π β (π₯ β π΄ β¦ πΆ) βπ πΈ) β β’ (π β (π₯ β π΄ β¦ (π΅ Β· πΆ)) βπ (π· Β· πΈ)) | ||
Theorem | rlimmulOLD 15596* | Obsolete version of rlimmul 15595 as of 27-Sep-2024. (Contributed by Mario Carneiro, 22-Sep-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) βπ π·) & β’ (π β (π₯ β π΄ β¦ πΆ) βπ πΈ) β β’ (π β (π₯ β π΄ β¦ (π΅ Β· πΆ)) βπ (π· Β· πΈ)) | ||
Theorem | rlimdiv 15597* | Limit of the quotient of two converging functions. Proposition 12-2.1(a) of [Gleason] p. 168. (Contributed by Mario Carneiro, 22-Sep-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) βπ π·) & β’ (π β (π₯ β π΄ β¦ πΆ) βπ πΈ) & β’ (π β πΈ β 0) & β’ ((π β§ π₯ β π΄) β πΆ β 0) β β’ (π β (π₯ β π΄ β¦ (π΅ / πΆ)) βπ (π· / πΈ)) | ||
Theorem | rlimneg 15598* | Limit of the negative of a sequence. (Contributed by Mario Carneiro, 18-May-2016.) |
β’ ((π β§ π β π΄) β π΅ β π) & β’ (π β (π β π΄ β¦ π΅) βπ πΆ) β β’ (π β (π β π΄ β¦ -π΅) βπ -πΆ) | ||
Theorem | rlimle 15599* | Comparison of the limits of two sequences. (Contributed by Mario Carneiro, 10-May-2016.) |
β’ (π β sup(π΄, β*, < ) = +β) & β’ (π β (π₯ β π΄ β¦ π΅) βπ π·) & β’ (π β (π₯ β π΄ β¦ πΆ) βπ πΈ) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ ((π β§ π₯ β π΄) β π΅ β€ πΆ) β β’ (π β π· β€ πΈ) | ||
Theorem | rlimsqzlem 15600* | Lemma for rlimsqz 15601 and rlimsqz2 15602. (Contributed by Mario Carneiro, 18-Sep-2014.) (Revised by Mario Carneiro, 20-May-2016.) |
β’ (π β π β β) & β’ (π β πΈ β β) & β’ (π β (π₯ β π΄ β¦ π΅) βπ π·) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ ((π β§ (π₯ β π΄ β§ π β€ π₯)) β (absβ(πΆ β πΈ)) β€ (absβ(π΅ β π·))) β β’ (π β (π₯ β π΄ β¦ πΆ) βπ πΈ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |