Home | Metamath
Proof Explorer Theorem List (p. 155 of 470) | < 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: | Metamath Proof Explorer
(1-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | climabs0 15401* | 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 15402* | Sufficient condition for transforming the index set of an eventually bounded function. (Contributed by Mario Carneiro, 12-May-2016.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β πΉ β π(1)) & β’ (π β πΊ:π΅βΆπ΄) & β’ (π β π΅ β β) & β’ ((π β§ π β β) β βπ₯ β β βπ¦ β π΅ (π₯ β€ π¦ β π β€ (πΊβπ¦))) β β’ (π β (πΉ β πΊ) β π(1)) | ||
Theorem | o1compt 15403* | Sufficient condition for transforming the index set of an eventually bounded function. (Contributed by Mario Carneiro, 12-May-2016.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β πΉ β π(1)) & β’ ((π β§ π¦ β π΅) β πΆ β π΄) & β’ (π β π΅ β β) & β’ ((π β§ π β β) β βπ₯ β β βπ¦ β π΅ (π₯ β€ π¦ β π β€ πΆ)) β β’ (π β (πΉ β (π¦ β π΅ β¦ πΆ)) β π(1)) | ||
Theorem | rlimcn1 15404* | Image of a limit under a continuous map. (Contributed by Mario Carneiro, 17-Sep-2014.) |
β’ (π β πΊ:π΄βΆπ) & β’ (π β πΆ β π) & β’ (π β πΊ βπ πΆ) & β’ (π β πΉ:πβΆβ) & β’ ((π β§ π₯ β β+) β βπ¦ β β+ βπ§ β π ((absβ(π§ β πΆ)) < π¦ β (absβ((πΉβπ§) β (πΉβπΆ))) < π₯)) β β’ (π β (πΉ β πΊ) βπ (πΉβπΆ)) | ||
Theorem | rlimcn1b 15405* | Image of a limit under a continuous map. (Contributed by Mario Carneiro, 10-May-2016.) |
β’ ((π β§ π β π΄) β π΅ β π) & β’ (π β πΆ β π) & β’ (π β (π β π΄ β¦ π΅) βπ πΆ) & β’ (π β πΉ:πβΆβ) & β’ ((π β§ π₯ β β+) β βπ¦ β β+ βπ§ β π ((absβ(π§ β πΆ)) < π¦ β (absβ((πΉβπ§) β (πΉβπΆ))) < π₯)) β β’ (π β (π β π΄ β¦ (πΉβπ΅)) βπ (πΉβπΆ)) | ||
Theorem | rlimcn3 15406* | Image of a limit under a continuous map, two-arg version. Originally a subproof of rlimcn2 15407. (Contributed by SN, 27-Sep-2024.) |
β’ ((π β§ π§ β π΄) β π΅ β π) & β’ ((π β§ π§ β π΄) β πΆ β π) & β’ ((π β§ π§ β π΄) β (π΅πΉπΆ) β β) & β’ (π β (π πΉπ) β β) & β’ (π β (π§ β π΄ β¦ π΅) βπ π ) & β’ (π β (π§ β π΄ β¦ πΆ) βπ π) & β’ ((π β§ π₯ β β+) β βπ β β+ βπ β β+ βπ’ β π βπ£ β π (((absβ(π’ β π )) < π β§ (absβ(π£ β π)) < π ) β (absβ((π’πΉπ£) β (π πΉπ))) < π₯)) β β’ (π β (π§ β π΄ β¦ (π΅πΉπΆ)) βπ (π πΉπ)) | ||
Theorem | rlimcn2 15407* | Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 17-Sep-2014.) |
β’ ((π β§ π§ β π΄) β π΅ β π) & β’ ((π β§ π§ β π΄) β πΆ β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π§ β π΄ β¦ π΅) βπ π ) & β’ (π β (π§ β π΄ β¦ πΆ) βπ π) & β’ (π β πΉ:(π Γ π)βΆβ) & β’ ((π β§ π₯ β β+) β βπ β β+ βπ β β+ βπ’ β π βπ£ β π (((absβ(π’ β π )) < π β§ (absβ(π£ β π)) < π ) β (absβ((π’πΉπ£) β (π πΉπ))) < π₯)) β β’ (π β (π§ β π΄ β¦ (π΅πΉπΆ)) βπ (π πΉπ)) | ||
Theorem | climcn1 15408* | Image of a limit under a continuous map. (Contributed by Mario Carneiro, 31-Jan-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π΄ β π΅) & β’ ((π β§ π§ β π΅) β (πΉβπ§) β β) & β’ (π β πΊ β π΄) & β’ (π β π» β π) & β’ ((π β§ π₯ β β+) β βπ¦ β β+ βπ§ β π΅ ((absβ(π§ β π΄)) < π¦ β (absβ((πΉβπ§) β (πΉβπ΄))) < π₯)) & β’ ((π β§ π β π) β (πΊβπ) β π΅) & β’ ((π β§ π β π) β (π»βπ) = (πΉβ(πΊβπ))) β β’ (π β π» β (πΉβπ΄)) | ||
Theorem | climcn2 15409* | Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 31-Jan-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π΄ β πΆ) & β’ (π β π΅ β π·) & β’ ((π β§ (π’ β πΆ β§ π£ β π·)) β (π’πΉπ£) β β) & β’ (π β πΊ β π΄) & β’ (π β π» β π΅) & β’ (π β πΎ β π) & β’ ((π β§ π₯ β β+) β βπ¦ β β+ βπ§ β β+ βπ’ β πΆ βπ£ β π· (((absβ(π’ β π΄)) < π¦ β§ (absβ(π£ β π΅)) < π§) β (absβ((π’πΉπ£) β (π΄πΉπ΅))) < π₯)) & β’ ((π β§ π β π) β (πΊβπ) β πΆ) & β’ ((π β§ π β π) β (π»βπ) β π·) & β’ ((π β§ π β π) β (πΎβπ) = ((πΊβπ)πΉ(π»βπ))) β β’ (π β πΎ β (π΄πΉπ΅)) | ||
Theorem | addcn2 15410* | 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 22500 and df-cncf 24163 are not yet available to us. See addcn 24150 for the abbreviated version.) (Contributed by Mario Carneiro, 31-Jan-2014.) |
β’ ((π΄ β β+ β§ π΅ β β β§ πΆ β β) β βπ¦ β β+ βπ§ β β+ βπ’ β β βπ£ β β (((absβ(π’ β π΅)) < π¦ β§ (absβ(π£ β πΆ)) < π§) β (absβ((π’ + π£) β (π΅ + πΆ))) < π΄)) | ||
Theorem | subcn2 15411* | 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 15412* | 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 15413* | 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 15414* | A sufficient condition for a function to be continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ πΉ:ββΆβ & β’ ((π§ β β β§ π΄ β β) β (absβ((πΉβπ§) β (πΉβπ΄))) β€ (absβ(π§ β π΄))) β β’ ((π΄ β β β§ π₯ β β+) β βπ¦ β β+ βπ§ β β ((absβ(π§ β π΄)) < π¦ β (absβ((πΉβπ§) β (πΉβπ΄))) < π₯)) | ||
Theorem | abscn2 15415* | The absolute value function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ ((π΄ β β β§ π₯ β β+) β βπ¦ β β+ βπ§ β β ((absβ(π§ β π΄)) < π¦ β (absβ((absβπ§) β (absβπ΄))) < π₯)) | ||
Theorem | cjcn2 15416* | The complex conjugate function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ ((π΄ β β β§ π₯ β β+) β βπ¦ β β+ βπ§ β β ((absβ(π§ β π΄)) < π¦ β (absβ((ββπ§) β (ββπ΄))) < π₯)) | ||
Theorem | recn2 15417* | The real part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ ((π΄ β β β§ π₯ β β+) β βπ¦ β β+ βπ§ β β ((absβ(π§ β π΄)) < π¦ β (absβ((ββπ§) β (ββπ΄))) < π₯)) | ||
Theorem | imcn2 15418* | The imaginary part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ ((π΄ β β β§ π₯ β β+) β βπ¦ β β+ βπ§ β β ((absβ(π§ β π΄)) < π¦ β (absβ((ββπ§) β (ββπ΄))) < π₯)) | ||
Theorem | climcn1lem 15419* | The limit of a continuous function, theorem form. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β πΉ β π΄) & β’ (π β πΊ β π) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ π»:ββΆβ & β’ ((π΄ β β β§ π₯ β β+) β βπ¦ β β+ βπ§ β β ((absβ(π§ β π΄)) < π¦ β (absβ((π»βπ§) β (π»βπ΄))) < π₯)) & β’ ((π β§ π β π) β (πΊβπ) = (π»β(πΉβπ))) β β’ (π β πΊ β (π»βπ΄)) | ||
Theorem | climabs 15420* | 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 15421* | 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 15422* | 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 15423* | 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 15424* | Reverse closure for a real limit. (Contributed by Mario Carneiro, 10-May-2016.) |
β’ ((π β§ π β π΄) β π΅ β π) & β’ (π β (π β π΄ β¦ π΅) βπ πΆ) β β’ ((π β§ π β π΄) β π΅ β β) | ||
Theorem | rlimabs 15425* | 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 15426* | 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 15427* | 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 15428* | 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 15429* | Show that a binary operation preserves eventual boundedness. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ ((π β β β§ π β β) β π β β) & β’ ((π₯ β β β§ π¦ β β) β (π₯π π¦) β β) & β’ (((π β β β§ π β β) β§ (π₯ β β β§ π¦ β β)) β (((absβπ₯) β€ π β§ (absβπ¦) β€ π) β (absβ(π₯π π¦)) β€ π)) β β’ ((πΉ β π(1) β§ πΊ β π(1)) β (πΉ βf π πΊ) β π(1)) | ||
Theorem | o1add 15430 | 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 15431 | 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 15432 | 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 15433 | Any function with a finite limit is eventually bounded. (Contributed by Mario Carneiro, 18-Sep-2014.) |
β’ (πΉ βπ π΄ β πΉ β π(1)) | ||
Theorem | rlimdmo1 15434 | A convergent function is eventually bounded. (Contributed by Mario Carneiro, 12-May-2016.) |
β’ (πΉ β dom βπ β πΉ β π(1)) | ||
Theorem | o1rlimmul 15435 | 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 15436* | A constant function is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) (Proof shortened by Mario Carneiro, 26-May-2016.) |
β’ ((π΄ β β β§ π΅ β β) β (π₯ β π΄ β¦ π΅) β π(1)) | ||
Theorem | lo1const 15437* | A constant function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π΄ β β β§ π΅ β β) β (π₯ β π΄ β¦ π΅) β β€π(1)) | ||
Theorem | lo1mptrcl 15438* | Reverse closure for an eventually upper bounded function. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β β€π(1)) β β’ ((π β§ π₯ β π΄) β π΅ β β) | ||
Theorem | o1mptrcl 15439* | Reverse closure for an eventually bounded function. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β π(1)) β β’ ((π β§ π₯ β π΄) β π΅ β β) | ||
Theorem | o1add2 15440* | The sum of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β π(1)) & β’ (π β (π₯ β π΄ β¦ πΆ) β π(1)) β β’ (π β (π₯ β π΄ β¦ (π΅ + πΆ)) β π(1)) | ||
Theorem | o1mul2 15441* | The product of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β π(1)) & β’ (π β (π₯ β π΄ β¦ πΆ) β π(1)) β β’ (π β (π₯ β π΄ β¦ (π΅ Β· πΆ)) β π(1)) | ||
Theorem | o1sub2 15442* | The product of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β π(1)) & β’ (π β (π₯ β π΄ β¦ πΆ) β π(1)) β β’ (π β (π₯ β π΄ β¦ (π΅ β πΆ)) β π(1)) | ||
Theorem | lo1add 15443* | The sum of two eventually upper bounded functions is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β β€π(1)) & β’ (π β (π₯ β π΄ β¦ πΆ) β β€π(1)) β β’ (π β (π₯ β π΄ β¦ (π΅ + πΆ)) β β€π(1)) | ||
Theorem | lo1mul 15444* | 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 15445* | 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 15446* | 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 15447* | 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 15443. (Contributed by Mario Carneiro, 31-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ (π β (π₯ β π΄ β¦ π΅) β β€π(1)) & β’ (π β (π₯ β π΄ β¦ πΆ) β π(1)) β β’ (π β (π₯ β π΄ β¦ (π΅ β πΆ)) β β€π(1)) | ||
Theorem | climadd 15448* | 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 15449* | 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 15450* | 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 15451* | 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 15452* | 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 15453* | 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 15454* | Limit of a constant πΆ subtracted from each term of a sequence. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ (π β πΆ β β) & β’ (π β πΊ β π) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) = ((πΉβπ) β πΆ)) β β’ (π β πΊ β (π΄ β πΆ)) | ||
Theorem | climsubc2 15455* | 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 15456* | Comparison of the limits of two sequences. (Contributed by Paul Chapman, 10-Sep-2007.) (Revised by Mario Carneiro, 1-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ (π β πΊ β π΅) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) β β) & β’ ((π β§ π β π) β (πΉβπ) β€ (πΊβπ)) β β’ (π β π΄ β€ π΅) | ||
Theorem | climsqz 15457* | 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 15458* | 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 15459* | 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 15460* | Obsolete version of rlimadd 15459 as of 27-Sep-2024. (Contributed by Mario Carneiro, 22-Sep-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) βπ π·) & β’ (π β (π₯ β π΄ β¦ πΆ) βπ πΈ) β β’ (π β (π₯ β π΄ β¦ (π΅ + πΆ)) βπ (π· + πΈ)) | ||
Theorem | rlimsub 15461* | 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 15462* | 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 15463* | Obsolete version of rlimmul 15462 as of 27-Sep-2024. (Contributed by Mario Carneiro, 22-Sep-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) βπ π·) & β’ (π β (π₯ β π΄ β¦ πΆ) βπ πΈ) β β’ (π β (π₯ β π΄ β¦ (π΅ Β· πΆ)) βπ (π· Β· πΈ)) | ||
Theorem | rlimdiv 15464* | 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 15465* | Limit of the negative of a sequence. (Contributed by Mario Carneiro, 18-May-2016.) |
β’ ((π β§ π β π΄) β π΅ β π) & β’ (π β (π β π΄ β¦ π΅) βπ πΆ) β β’ (π β (π β π΄ β¦ -π΅) βπ -πΆ) | ||
Theorem | rlimle 15466* | Comparison of the limits of two sequences. (Contributed by Mario Carneiro, 10-May-2016.) |
β’ (π β sup(π΄, β*, < ) = +β) & β’ (π β (π₯ β π΄ β¦ π΅) βπ π·) & β’ (π β (π₯ β π΄ β¦ πΆ) βπ πΈ) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ ((π β§ π₯ β π΄) β π΅ β€ πΆ) β β’ (π β π· β€ πΈ) | ||
Theorem | rlimsqzlem 15467* | Lemma for rlimsqz 15468 and rlimsqz2 15469. (Contributed by Mario Carneiro, 18-Sep-2014.) (Revised by Mario Carneiro, 20-May-2016.) |
β’ (π β π β β) & β’ (π β πΈ β β) & β’ (π β (π₯ β π΄ β¦ π΅) βπ π·) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ ((π β§ (π₯ β π΄ β§ π β€ π₯)) β (absβ(πΆ β πΈ)) β€ (absβ(π΅ β π·))) β β’ (π β (π₯ β π΄ β¦ πΆ) βπ πΈ) | ||
Theorem | rlimsqz 15468* | 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 15469* | 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 15470* | Transfer eventual upper boundedness from a larger function to a smaller function. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ (π β π β β) & β’ (π β (π₯ β π΄ β¦ π΅) β β€π(1)) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ ((π β§ (π₯ β π΄ β§ π β€ π₯)) β πΆ β€ π΅) β β’ (π β (π₯ β π΄ β¦ πΆ) β β€π(1)) | ||
Theorem | o1le 15471* | 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 15472* | A function whose inverse converges to zero is unbounded. (Contributed by Mario Carneiro, 30-May-2016.) |
β’ (π β sup(π΄, β*, < ) = +β) & β’ (π β (π₯ β π΄ β¦ (1 / π΅)) βπ 0) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β π΅ β 0) β β’ (π β Β¬ (π₯ β π΄ β¦ π΅) β π(1)) | ||
Theorem | clim2ser 15473* | The limit of an infinite series with an initial segment removed. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 1-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ (π β seqπ( + , πΉ) β π΄) β β’ (π β seq(π + 1)( + , πΉ) β (π΄ β (seqπ( + , πΉ)βπ))) | ||
Theorem | clim2ser2 15474* | The limit of an infinite series with an initial segment added. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 1-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ (π β seq(π + 1)( + , πΉ) β π΄) β β’ (π β seqπ( + , πΉ) β (π΄ + (seqπ( + , πΉ)βπ))) | ||
Theorem | iserex 15475* | An infinite series converges, if and only if the series does with initial terms removed. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 27-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ ((π β§ π β π) β (πΉβπ) β β) β β’ (π β (seqπ( + , πΉ) β dom β β seqπ( + , πΉ) β dom β )) | ||
Theorem | isermulc2 15476* | Multiplication of an infinite series by a constant. (Contributed by Paul Chapman, 14-Nov-2007.) (Revised by Mario Carneiro, 1-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΆ β β) & β’ (π β seqπ( + , πΉ) β π΄) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) = (πΆ Β· (πΉβπ))) β β’ (π β seqπ( + , πΊ) β (πΆ Β· π΄)) | ||
Theorem | climlec2 15477* | Comparison of a constant to the limit of a sequence. (Contributed by NM, 28-Feb-2008.) (Revised by Mario Carneiro, 1-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π΄ β β) & β’ (π β πΉ β π΅) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β π΄ β€ (πΉβπ)) β β’ (π β π΄ β€ π΅) | ||
Theorem | iserle 15478* | Comparison of the limits of two infinite series. (Contributed by Paul Chapman, 12-Nov-2007.) (Revised by Mario Carneiro, 3-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β seqπ( + , πΉ) β π΄) & β’ (π β seqπ( + , πΊ) β π΅) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) β β) & β’ ((π β§ π β π) β (πΉβπ) β€ (πΊβπ)) β β’ (π β π΄ β€ π΅) | ||
Theorem | iserge0 15479* | The limit of an infinite series of nonnegative reals is nonnegative. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 3-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β seqπ( + , πΉ) β π΄) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β 0 β€ (πΉβπ)) β β’ (π β 0 β€ π΄) | ||
Theorem | climub 15480* | The limit of a monotonic sequence is an upper bound. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 10-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ (π β πΉ β π΄) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΉβπ) β€ (πΉβ(π + 1))) β β’ (π β (πΉβπ) β€ π΄) | ||
Theorem | climserle 15481* | The partial sums of a converging infinite series with nonnegative terms are bounded by its limit. (Contributed by NM, 27-Dec-2005.) (Revised by Mario Carneiro, 9-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ (π β seqπ( + , πΉ) β π΄) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β 0 β€ (πΉβπ)) β β’ (π β (seqπ( + , πΉ)βπ) β€ π΄) | ||
Theorem | isershft 15482 | Index shift of the limit of an infinite series. (Contributed by Mario Carneiro, 6-Sep-2013.) (Revised by Mario Carneiro, 5-Nov-2013.) |
β’ πΉ β V β β’ ((π β β€ β§ π β β€) β (seqπ( + , πΉ) β π΄ β seq(π + π)( + , (πΉ shift π)) β π΄)) | ||
Theorem | isercolllem1 15483* | Lemma for isercoll 15486. (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ:ββΆπ) & β’ ((π β§ π β β) β (πΊβπ) < (πΊβ(π + 1))) β β’ ((π β§ π β β) β (πΊ βΎ π) Isom < , < (π, (πΊ β π))) | ||
Theorem | isercolllem2 15484* | Lemma for isercoll 15486. (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ:ββΆπ) & β’ ((π β§ π β β) β (πΊβπ) < (πΊβ(π + 1))) β β’ ((π β§ π β (β€β₯β(πΊβ1))) β (1...(β―β(πΊ β (β‘πΊ β (π...π))))) = (β‘πΊ β (π...π))) | ||
Theorem | isercolllem3 15485* | Lemma for isercoll 15486. (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ:ββΆπ) & β’ ((π β§ π β β) β (πΊβπ) < (πΊβ(π + 1))) & β’ ((π β§ π β (π β ran πΊ)) β (πΉβπ) = 0) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β β) β (π»βπ) = (πΉβ(πΊβπ))) β β’ ((π β§ π β (β€β₯β(πΊβ1))) β (seqπ( + , πΉ)βπ) = (seq1( + , π»)β(β―β(πΊ β (β‘πΊ β (π...π)))))) | ||
Theorem | isercoll 15486* | Rearrange an infinite series by spacing out the terms using an order isomorphism. (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ:ββΆπ) & β’ ((π β§ π β β) β (πΊβπ) < (πΊβ(π + 1))) & β’ ((π β§ π β (π β ran πΊ)) β (πΉβπ) = 0) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β β) β (π»βπ) = (πΉβ(πΊβπ))) β β’ (π β (seq1( + , π») β π΄ β seqπ( + , πΉ) β π΄)) | ||
Theorem | isercoll2 15487* | Generalize isercoll 15486 so that both sequences have arbitrary starting point. (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β πΊ:πβΆπ) & β’ ((π β§ π β π) β (πΊβπ) < (πΊβ(π + 1))) & β’ ((π β§ π β (π β ran πΊ)) β (πΉβπ) = 0) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (π»βπ) = (πΉβ(πΊβπ))) β β’ (π β (seqπ( + , π») β π΄ β seqπ( + , πΉ) β π΄)) | ||
Theorem | climsup 15488* | A bounded monotonic sequence converges to the supremum of its range. Theorem 12-5.1 of [Gleason] p. 180. (Contributed by NM, 13-Mar-2005.) (Revised by Mario Carneiro, 10-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆβ) & β’ ((π β§ π β π) β (πΉβπ) β€ (πΉβ(π + 1))) & β’ (π β βπ₯ β β βπ β π (πΉβπ) β€ π₯) β β’ (π β πΉ β sup(ran πΉ, β, < )) | ||
Theorem | climcau 15489* | A converging sequence of complex numbers is a Cauchy sequence. Theorem 12-5.3 of [Gleason] p. 180 (necessity part). (Contributed by NM, 16-Apr-2005.) (Revised by Mario Carneiro, 26-Apr-2014.) |
β’ π = (β€β₯βπ) β β’ ((π β β€ β§ πΉ β dom β ) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯) | ||
Theorem | climbdd 15490* | A converging sequence of complex numbers is bounded. (Contributed by Mario Carneiro, 9-Jul-2017.) |
β’ π = (β€β₯βπ) β β’ ((π β β€ β§ πΉ β dom β β§ βπ β π (πΉβπ) β β) β βπ₯ β β βπ β π (absβ(πΉβπ)) β€ π₯) | ||
Theorem | caucvgrlem 15491* | Lemma for caurcvgr 15492. (Contributed by Mario Carneiro, 15-Feb-2014.) (Revised by AV, 12-Sep-2020.) |
β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β sup(π΄, β*, < ) = +β) & β’ (π β βπ₯ β β+ βπ β π΄ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π₯)) & β’ (π β π β β+) β β’ (π β βπ β π΄ ((lim supβπΉ) β β β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· π )))) | ||
Theorem | caurcvgr 15492* | A Cauchy sequence of real numbers converges to its limit supremum. The third hypothesis specifies that πΉ is a Cauchy sequence. (Contributed by Mario Carneiro, 7-May-2016.) (Revised by AV, 12-Sep-2020.) |
β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β sup(π΄, β*, < ) = +β) & β’ (π β βπ₯ β β+ βπ β π΄ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π₯)) β β’ (π β πΉ βπ (lim supβπΉ)) | ||
Theorem | caucvgrlem2 15493* | Lemma for caucvgr 15494. (Contributed by NM, 4-Apr-2005.) (Proof shortened by Mario Carneiro, 8-May-2016.) |
β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β sup(π΄, β*, < ) = +β) & β’ (π β βπ₯ β β+ βπ β π΄ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π₯)) & β’ π»:ββΆβ & β’ (((πΉβπ) β β β§ (πΉβπ) β β) β (absβ((π»β(πΉβπ)) β (π»β(πΉβπ)))) β€ (absβ((πΉβπ) β (πΉβπ)))) β β’ (π β (π β π΄ β¦ (π»β(πΉβπ))) βπ ( βπ β(π» β πΉ))) | ||
Theorem | caucvgr 15494* | A Cauchy sequence of complex numbers converges to a complex number. Theorem 12-5.3 of [Gleason] p. 180 (sufficiency part). (Contributed by NM, 20-Dec-2006.) (Revised by Mario Carneiro, 8-May-2016.) |
β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β sup(π΄, β*, < ) = +β) & β’ (π β βπ₯ β β+ βπ β π΄ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π₯)) β β’ (π β πΉ β dom βπ ) | ||
Theorem | caurcvg 15495* | A Cauchy sequence of real numbers converges to its limit supremum. The fourth hypothesis specifies that πΉ is a Cauchy sequence. (Contributed by NM, 4-Apr-2005.) (Revised by AV, 12-Sep-2020.) |
β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ (π β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯) β β’ (π β πΉ β (lim supβπΉ)) | ||
Theorem | caurcvg2 15496* | A Cauchy sequence of real numbers converges, existence version. (Contributed by NM, 4-Apr-2005.) (Revised by Mario Carneiro, 7-Sep-2014.) |
β’ π = (β€β₯βπ) & β’ (π β πΉ β π) & β’ (π β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯)) β β’ (π β πΉ β dom β ) | ||
Theorem | caucvg 15497* | A Cauchy sequence of complex numbers converges to a complex number. Theorem 12-5.3 of [Gleason] p. 180 (sufficiency part). (Contributed by NM, 20-Dec-2006.) (Proof shortened by Mario Carneiro, 15-Feb-2014.) (Revised by Mario Carneiro, 8-May-2016.) |
β’ π = (β€β₯βπ) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ (π β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯) & β’ (π β πΉ β π) β β’ (π β πΉ β dom β ) | ||
Theorem | caucvgb 15498* | A function is convergent if and only if it is Cauchy. Theorem 12-5.3 of [Gleason] p. 180. (Contributed by Mario Carneiro, 15-Feb-2014.) |
β’ π = (β€β₯βπ) β β’ ((π β β€ β§ πΉ β π) β (πΉ β dom β β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯))) | ||
Theorem | serf0 15499* | If an infinite series converges, its underlying sequence converges to zero. (Contributed by NM, 2-Sep-2005.) (Revised by Mario Carneiro, 16-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π) & β’ (π β seqπ( + , πΉ) β dom β ) & β’ ((π β§ π β π) β (πΉβπ) β β) β β’ (π β πΉ β 0) | ||
Theorem | iseraltlem1 15500* | Lemma for iseralt 15503. A decreasing sequence with limit zero consists of positive terms. (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π β π) β (πΊβ(π + 1)) β€ (πΊβπ)) & β’ (π β πΊ β 0) β β’ ((π β§ π β π) β 0 β€ (πΊβπ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |