![]() |
Metamath
Proof Explorer Theorem List (p. 156 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 | climmo 15501* | An infinite sequence of complex numbers converges to at most one limit. (Contributed by Mario Carneiro, 13-Jul-2013.) |
β’ β*π₯ πΉ β π₯ | ||
Theorem | rlimres 15502 | The restriction of a function converges if the original converges. (Contributed by Mario Carneiro, 16-Sep-2014.) |
β’ (πΉ βπ π΄ β (πΉ βΎ π΅) βπ π΄) | ||
Theorem | lo1res 15503 | The restriction of an eventually upper bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ (πΉ β β€π(1) β (πΉ βΎ π΄) β β€π(1)) | ||
Theorem | o1res 15504 | 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 15505* | The restriction of a function converges if the original converges. (Contributed by Mario Carneiro, 16-Sep-2014.) |
β’ (π β π΄ β π΅) & β’ (π β (π₯ β π΅ β¦ πΆ) βπ π·) β β’ (π β (π₯ β π΄ β¦ πΆ) βπ π·) | ||
Theorem | lo1res2 15506* | The restriction of a function is eventually bounded if the original is. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ (π β π΄ β π΅) & β’ (π β (π₯ β π΅ β¦ πΆ) β β€π(1)) β β’ (π β (π₯ β π΄ β¦ πΆ) β β€π(1)) | ||
Theorem | o1res2 15507* | The restriction of a function is eventually bounded if the original is. (Contributed by Mario Carneiro, 21-May-2016.) |
β’ (π β π΄ β π΅) & β’ (π β (π₯ β π΅ β¦ πΆ) β π(1)) β β’ (π β (π₯ β π΄ β¦ πΆ) β π(1)) | ||
Theorem | lo1resb 15508 | 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 15509 | The restriction of a function to an unbounded-above interval converges iff the original converges. (Contributed by Mario Carneiro, 16-Sep-2014.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (πΉ βπ πΆ β (πΉ βΎ (π΅[,)+β)) βπ πΆ)) | ||
Theorem | o1resb 15510 | 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 15511* | 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 15512* | 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 15513* | Two functions that are eventually equal to one another have the same limit. (Contributed by Mario Carneiro, 16-Sep-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ (π β π· β β) & β’ ((π β§ (π₯ β π΄ β§ π· β€ π₯)) β π΅ = πΆ) β β’ (π β ((π₯ β π΄ β¦ π΅) βπ πΈ β (π₯ β π΄ β¦ πΆ) βπ πΈ)) | ||
Theorem | o1eq 15514* | 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 15515* | Exhibit a function πΊ with the same convergence properties as the not-quite-function πΉ. (Contributed by Mario Carneiro, 31-Jan-2014.) |
β’ π = (β€β₯βπ) & β’ πΊ = (π β π β¦ (πΉβπ)) β β’ ((π β β€ β§ πΉ β π) β (πΉ β π΄ β πΊ β π΄)) | ||
Theorem | 2clim 15516* | 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 15517* | Relate an integer limit on a not-quite-function to a real limit. (Contributed by Mario Carneiro, 17-Sep-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π) & β’ ((π β§ π β π) β (πΉβπ) β β) β β’ (π β (πΉ β π΄ β (π β π β¦ (πΉβπ)) βπ π΄)) | ||
Theorem | climshftlem 15518 | A shifted function converges if the original function converges. (Contributed by Mario Carneiro, 5-Nov-2013.) |
β’ πΉ β V β β’ (π β β€ β (πΉ β π΄ β (πΉ shift π) β π΄)) | ||
Theorem | climres 15519 | 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 15520 | 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 15521 | 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 15522* | 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 15523* | 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 15524* | The limit of a real sequence is real. (Contributed by Mario Carneiro, 9-May-2016.) |
β’ (π β sup(π΄, β*, < ) = +β) & β’ (π β (π₯ β π΄ β¦ π΅) βπ πΆ) & β’ ((π β§ π₯ β π΄) β π΅ β β) β β’ (π β πΆ β β) | ||
Theorem | rlimge0 15525* | The limit of a sequence of nonnegative reals is nonnegative. (Contributed by Mario Carneiro, 10-May-2016.) |
β’ (π β sup(π΄, β*, < ) = +β) & β’ (π β (π₯ β π΄ β¦ π΅) βπ πΆ) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β 0 β€ π΅) β β’ (π β 0 β€ πΆ) | ||
Theorem | climshft2 15526* | 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 15527* | 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 15528* | 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 15529* | 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 15530* | Sufficient condition for transforming the index set of an eventually bounded function. (Contributed by Mario Carneiro, 12-May-2016.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β πΉ β π(1)) & β’ (π β πΊ:π΅βΆπ΄) & β’ (π β π΅ β β) & β’ ((π β§ π β β) β βπ₯ β β βπ¦ β π΅ (π₯ β€ π¦ β π β€ (πΊβπ¦))) β β’ (π β (πΉ β πΊ) β π(1)) | ||
Theorem | o1compt 15531* | Sufficient condition for transforming the index set of an eventually bounded function. (Contributed by Mario Carneiro, 12-May-2016.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β πΉ β π(1)) & β’ ((π β§ π¦ β π΅) β πΆ β π΄) & β’ (π β π΅ β β) & β’ ((π β§ π β β) β βπ₯ β β βπ¦ β π΅ (π₯ β€ π¦ β π β€ πΆ)) β β’ (π β (πΉ β (π¦ β π΅ β¦ πΆ)) β π(1)) | ||
Theorem | rlimcn1 15532* | Image of a limit under a continuous map. (Contributed by Mario Carneiro, 17-Sep-2014.) |
β’ (π β πΊ:π΄βΆπ) & β’ (π β πΆ β π) & β’ (π β πΊ βπ πΆ) & β’ (π β πΉ:πβΆβ) & β’ ((π β§ π₯ β β+) β βπ¦ β β+ βπ§ β π ((absβ(π§ β πΆ)) < π¦ β (absβ((πΉβπ§) β (πΉβπΆ))) < π₯)) β β’ (π β (πΉ β πΊ) βπ (πΉβπΆ)) | ||
Theorem | rlimcn1b 15533* | Image of a limit under a continuous map. (Contributed by Mario Carneiro, 10-May-2016.) |
β’ ((π β§ π β π΄) β π΅ β π) & β’ (π β πΆ β π) & β’ (π β (π β π΄ β¦ π΅) βπ πΆ) & β’ (π β πΉ:πβΆβ) & β’ ((π β§ π₯ β β+) β βπ¦ β β+ βπ§ β π ((absβ(π§ β πΆ)) < π¦ β (absβ((πΉβπ§) β (πΉβπΆ))) < π₯)) β β’ (π β (π β π΄ β¦ (πΉβπ΅)) βπ (πΉβπΆ)) | ||
Theorem | rlimcn3 15534* | Image of a limit under a continuous map, two-arg version. Originally a subproof of rlimcn2 15535. (Contributed by SN, 27-Sep-2024.) |
β’ ((π β§ π§ β π΄) β π΅ β π) & β’ ((π β§ π§ β π΄) β πΆ β π) & β’ ((π β§ π§ β π΄) β (π΅πΉπΆ) β β) & β’ (π β (π πΉπ) β β) & β’ (π β (π§ β π΄ β¦ π΅) βπ π ) & β’ (π β (π§ β π΄ β¦ πΆ) βπ π) & β’ ((π β§ π₯ β β+) β βπ β β+ βπ β β+ βπ’ β π βπ£ β π (((absβ(π’ β π )) < π β§ (absβ(π£ β π)) < π ) β (absβ((π’πΉπ£) β (π πΉπ))) < π₯)) β β’ (π β (π§ β π΄ β¦ (π΅πΉπΆ)) βπ (π πΉπ)) | ||
Theorem | rlimcn2 15535* | Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 17-Sep-2014.) |
β’ ((π β§ π§ β π΄) β π΅ β π) & β’ ((π β§ π§ β π΄) β πΆ β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π§ β π΄ β¦ π΅) βπ π ) & β’ (π β (π§ β π΄ β¦ πΆ) βπ π) & β’ (π β πΉ:(π Γ π)βΆβ) & β’ ((π β§ π₯ β β+) β βπ β β+ βπ β β+ βπ’ β π βπ£ β π (((absβ(π’ β π )) < π β§ (absβ(π£ β π)) < π ) β (absβ((π’πΉπ£) β (π πΉπ))) < π₯)) β β’ (π β (π§ β π΄ β¦ (π΅πΉπΆ)) βπ (π πΉπ)) | ||
Theorem | climcn1 15536* | Image of a limit under a continuous map. (Contributed by Mario Carneiro, 31-Jan-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π΄ β π΅) & β’ ((π β§ π§ β π΅) β (πΉβπ§) β β) & β’ (π β πΊ β π΄) & β’ (π β π» β π) & β’ ((π β§ π₯ β β+) β βπ¦ β β+ βπ§ β π΅ ((absβ(π§ β π΄)) < π¦ β (absβ((πΉβπ§) β (πΉβπ΄))) < π₯)) & β’ ((π β§ π β π) β (πΊβπ) β π΅) & β’ ((π β§ π β π) β (π»βπ) = (πΉβ(πΊβπ))) β β’ (π β π» β (πΉβπ΄)) | ||
Theorem | climcn2 15537* | Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 31-Jan-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π΄ β πΆ) & β’ (π β π΅ β π·) & β’ ((π β§ (π’ β πΆ β§ π£ β π·)) β (π’πΉπ£) β β) & β’ (π β πΊ β π΄) & β’ (π β π» β π΅) & β’ (π β πΎ β π) & β’ ((π β§ π₯ β β+) β βπ¦ β β+ βπ§ β β+ βπ’ β πΆ βπ£ β π· (((absβ(π’ β π΄)) < π¦ β§ (absβ(π£ β π΅)) < π§) β (absβ((π’πΉπ£) β (π΄πΉπ΅))) < π₯)) & β’ ((π β§ π β π) β (πΊβπ) β πΆ) & β’ ((π β§ π β π) β (π»βπ) β π·) & β’ ((π β§ π β π) β (πΎβπ) = ((πΊβπ)πΉ(π»βπ))) β β’ (π β πΎ β (π΄πΉπ΅)) | ||
Theorem | addcn2 15538* | 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 22731 and df-cncf 24394 are not yet available to us. See addcn 24381 for the abbreviated version.) (Contributed by Mario Carneiro, 31-Jan-2014.) |
β’ ((π΄ β β+ β§ π΅ β β β§ πΆ β β) β βπ¦ β β+ βπ§ β β+ βπ’ β β βπ£ β β (((absβ(π’ β π΅)) < π¦ β§ (absβ(π£ β πΆ)) < π§) β (absβ((π’ + π£) β (π΅ + πΆ))) < π΄)) | ||
Theorem | subcn2 15539* | 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 15540* | 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 15541* | 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 15542* | A sufficient condition for a function to be continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ πΉ:ββΆβ & β’ ((π§ β β β§ π΄ β β) β (absβ((πΉβπ§) β (πΉβπ΄))) β€ (absβ(π§ β π΄))) β β’ ((π΄ β β β§ π₯ β β+) β βπ¦ β β+ βπ§ β β ((absβ(π§ β π΄)) < π¦ β (absβ((πΉβπ§) β (πΉβπ΄))) < π₯)) | ||
Theorem | abscn2 15543* | The absolute value function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ ((π΄ β β β§ π₯ β β+) β βπ¦ β β+ βπ§ β β ((absβ(π§ β π΄)) < π¦ β (absβ((absβπ§) β (absβπ΄))) < π₯)) | ||
Theorem | cjcn2 15544* | The complex conjugate function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ ((π΄ β β β§ π₯ β β+) β βπ¦ β β+ βπ§ β β ((absβ(π§ β π΄)) < π¦ β (absβ((ββπ§) β (ββπ΄))) < π₯)) | ||
Theorem | recn2 15545* | The real part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ ((π΄ β β β§ π₯ β β+) β βπ¦ β β+ βπ§ β β ((absβ(π§ β π΄)) < π¦ β (absβ((ββπ§) β (ββπ΄))) < π₯)) | ||
Theorem | imcn2 15546* | The imaginary part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ ((π΄ β β β§ π₯ β β+) β βπ¦ β β+ βπ§ β β ((absβ(π§ β π΄)) < π¦ β (absβ((ββπ§) β (ββπ΄))) < π₯)) | ||
Theorem | climcn1lem 15547* | The limit of a continuous function, theorem form. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β πΉ β π΄) & β’ (π β πΊ β π) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ π»:ββΆβ & β’ ((π΄ β β β§ π₯ β β+) β βπ¦ β β+ βπ§ β β ((absβ(π§ β π΄)) < π¦ β (absβ((π»βπ§) β (π»βπ΄))) < π₯)) & β’ ((π β§ π β π) β (πΊβπ) = (π»β(πΉβπ))) β β’ (π β πΊ β (π»βπ΄)) | ||
Theorem | climabs 15548* | 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 15549* | 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 15550* | 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 15551* | 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 15552* | Reverse closure for a real limit. (Contributed by Mario Carneiro, 10-May-2016.) |
β’ ((π β§ π β π΄) β π΅ β π) & β’ (π β (π β π΄ β¦ π΅) βπ πΆ) β β’ ((π β§ π β π΄) β π΅ β β) | ||
Theorem | rlimabs 15553* | 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 15554* | 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 15555* | 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 15556* | 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 15557* | Show that a binary operation preserves eventual boundedness. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ ((π β β β§ π β β) β π β β) & β’ ((π₯ β β β§ π¦ β β) β (π₯π π¦) β β) & β’ (((π β β β§ π β β) β§ (π₯ β β β§ π¦ β β)) β (((absβπ₯) β€ π β§ (absβπ¦) β€ π) β (absβ(π₯π π¦)) β€ π)) β β’ ((πΉ β π(1) β§ πΊ β π(1)) β (πΉ βf π πΊ) β π(1)) | ||
Theorem | o1add 15558 | 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 15559 | 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 15560 | 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 15561 | Any function with a finite limit is eventually bounded. (Contributed by Mario Carneiro, 18-Sep-2014.) |
β’ (πΉ βπ π΄ β πΉ β π(1)) | ||
Theorem | rlimdmo1 15562 | A convergent function is eventually bounded. (Contributed by Mario Carneiro, 12-May-2016.) |
β’ (πΉ β dom βπ β πΉ β π(1)) | ||
Theorem | o1rlimmul 15563 | 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 15564* | A constant function is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) (Proof shortened by Mario Carneiro, 26-May-2016.) |
β’ ((π΄ β β β§ π΅ β β) β (π₯ β π΄ β¦ π΅) β π(1)) | ||
Theorem | lo1const 15565* | A constant function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π΄ β β β§ π΅ β β) β (π₯ β π΄ β¦ π΅) β β€π(1)) | ||
Theorem | lo1mptrcl 15566* | Reverse closure for an eventually upper bounded function. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β β€π(1)) β β’ ((π β§ π₯ β π΄) β π΅ β β) | ||
Theorem | o1mptrcl 15567* | Reverse closure for an eventually bounded function. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β π(1)) β β’ ((π β§ π₯ β π΄) β π΅ β β) | ||
Theorem | o1add2 15568* | The sum of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β π(1)) & β’ (π β (π₯ β π΄ β¦ πΆ) β π(1)) β β’ (π β (π₯ β π΄ β¦ (π΅ + πΆ)) β π(1)) | ||
Theorem | o1mul2 15569* | The product of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β π(1)) & β’ (π β (π₯ β π΄ β¦ πΆ) β π(1)) β β’ (π β (π₯ β π΄ β¦ (π΅ Β· πΆ)) β π(1)) | ||
Theorem | o1sub2 15570* | The product of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β π(1)) & β’ (π β (π₯ β π΄ β¦ πΆ) β π(1)) β β’ (π β (π₯ β π΄ β¦ (π΅ β πΆ)) β π(1)) | ||
Theorem | lo1add 15571* | The sum of two eventually upper bounded functions is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β β€π(1)) & β’ (π β (π₯ β π΄ β¦ πΆ) β β€π(1)) β β’ (π β (π₯ β π΄ β¦ (π΅ + πΆ)) β β€π(1)) | ||
Theorem | lo1mul 15572* | 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 15573* | 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 15574* | 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 15575* | 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 15571. (Contributed by Mario Carneiro, 31-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ (π β (π₯ β π΄ β¦ π΅) β β€π(1)) & β’ (π β (π₯ β π΄ β¦ πΆ) β π(1)) β β’ (π β (π₯ β π΄ β¦ (π΅ β πΆ)) β β€π(1)) | ||
Theorem | climadd 15576* | 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 15577* | 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 15578* | 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 15579* | 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 15580* | 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 15581* | 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 15582* | Limit of a constant πΆ subtracted from each term of a sequence. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ (π β πΆ β β) & β’ (π β πΊ β π) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) = ((πΉβπ) β πΆ)) β β’ (π β πΊ β (π΄ β πΆ)) | ||
Theorem | climsubc2 15583* | 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 15584* | Comparison of the limits of two sequences. (Contributed by Paul Chapman, 10-Sep-2007.) (Revised by Mario Carneiro, 1-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ (π β πΊ β π΅) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) β β) & β’ ((π β§ π β π) β (πΉβπ) β€ (πΊβπ)) β β’ (π β π΄ β€ π΅) | ||
Theorem | climsqz 15585* | 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 15586* | 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 15587* | 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 15588* | Obsolete version of rlimadd 15587 as of 27-Sep-2024. (Contributed by Mario Carneiro, 22-Sep-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) βπ π·) & β’ (π β (π₯ β π΄ β¦ πΆ) βπ πΈ) β β’ (π β (π₯ β π΄ β¦ (π΅ + πΆ)) βπ (π· + πΈ)) | ||
Theorem | rlimsub 15589* | 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 15590* | 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 15591* | Obsolete version of rlimmul 15590 as of 27-Sep-2024. (Contributed by Mario Carneiro, 22-Sep-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) βπ π·) & β’ (π β (π₯ β π΄ β¦ πΆ) βπ πΈ) β β’ (π β (π₯ β π΄ β¦ (π΅ Β· πΆ)) βπ (π· Β· πΈ)) | ||
Theorem | rlimdiv 15592* | 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 15593* | Limit of the negative of a sequence. (Contributed by Mario Carneiro, 18-May-2016.) |
β’ ((π β§ π β π΄) β π΅ β π) & β’ (π β (π β π΄ β¦ π΅) βπ πΆ) β β’ (π β (π β π΄ β¦ -π΅) βπ -πΆ) | ||
Theorem | rlimle 15594* | Comparison of the limits of two sequences. (Contributed by Mario Carneiro, 10-May-2016.) |
β’ (π β sup(π΄, β*, < ) = +β) & β’ (π β (π₯ β π΄ β¦ π΅) βπ π·) & β’ (π β (π₯ β π΄ β¦ πΆ) βπ πΈ) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ ((π β§ π₯ β π΄) β π΅ β€ πΆ) β β’ (π β π· β€ πΈ) | ||
Theorem | rlimsqzlem 15595* | Lemma for rlimsqz 15596 and rlimsqz2 15597. (Contributed by Mario Carneiro, 18-Sep-2014.) (Revised by Mario Carneiro, 20-May-2016.) |
β’ (π β π β β) & β’ (π β πΈ β β) & β’ (π β (π₯ β π΄ β¦ π΅) βπ π·) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ ((π β§ (π₯ β π΄ β§ π β€ π₯)) β (absβ(πΆ β πΈ)) β€ (absβ(π΅ β π·))) β β’ (π β (π₯ β π΄ β¦ πΆ) βπ πΈ) | ||
Theorem | rlimsqz 15596* | Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by Mario Carneiro, 18-Sep-2014.) (Revised by Mario Carneiro, 20-May-2016.) |
β’ (π β π· β β) & β’ (π β π β β) & β’ (π β (π₯ β π΄ β¦ π΅) βπ π·) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ ((π β§ (π₯ β π΄ β§ π β€ π₯)) β π΅ β€ πΆ) & β’ ((π β§ (π₯ β π΄ β§ π β€ π₯)) β πΆ β€ π·) β β’ (π β (π₯ β π΄ β¦ πΆ) βπ π·) | ||
Theorem | rlimsqz2 15597* | Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by Mario Carneiro, 3-Feb-2014.) (Revised by Mario Carneiro, 20-May-2016.) |
β’ (π β π· β β) & β’ (π β π β β) & β’ (π β (π₯ β π΄ β¦ π΅) βπ π·) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ ((π β§ (π₯ β π΄ β§ π β€ π₯)) β πΆ β€ π΅) & β’ ((π β§ (π₯ β π΄ β§ π β€ π₯)) β π· β€ πΆ) β β’ (π β (π₯ β π΄ β¦ πΆ) βπ π·) | ||
Theorem | lo1le 15598* | Transfer eventual upper boundedness from a larger function to a smaller function. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ (π β π β β) & β’ (π β (π₯ β π΄ β¦ π΅) β β€π(1)) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ ((π β§ (π₯ β π΄ β§ π β€ π₯)) β πΆ β€ π΅) β β’ (π β (π₯ β π΄ β¦ πΆ) β β€π(1)) | ||
Theorem | o1le 15599* | Transfer eventual boundedness from a larger function to a smaller function. (Contributed by Mario Carneiro, 25-Sep-2014.) (Proof shortened by Mario Carneiro, 26-May-2016.) |
β’ (π β π β β) & β’ (π β (π₯ β π΄ β¦ π΅) β π(1)) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ ((π β§ (π₯ β π΄ β§ π β€ π₯)) β (absβπΆ) β€ (absβπ΅)) β β’ (π β (π₯ β π΄ β¦ πΆ) β π(1)) | ||
Theorem | rlimno1 15600* | A function whose inverse converges to zero is unbounded. (Contributed by Mario Carneiro, 30-May-2016.) |
β’ (π β sup(π΄, β*, < ) = +β) & β’ (π β (π₯ β π΄ β¦ (1 / π΅)) βπ 0) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β π΅ β 0) β β’ (π β Β¬ (π₯ β π΄ β¦ π΅) β π(1)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |