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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | climge0 15401* | 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 15402* | 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 15403* | Sufficient condition for transforming the index set of an eventually bounded function. (Contributed by Mario Carneiro, 12-May-2016.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β πΉ β π(1)) & β’ (π β πΊ:π΅βΆπ΄) & β’ (π β π΅ β β) & β’ ((π β§ π β β) β βπ₯ β β βπ¦ β π΅ (π₯ β€ π¦ β π β€ (πΊβπ¦))) β β’ (π β (πΉ β πΊ) β π(1)) | ||
Theorem | o1compt 15404* | Sufficient condition for transforming the index set of an eventually bounded function. (Contributed by Mario Carneiro, 12-May-2016.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β πΉ β π(1)) & β’ ((π β§ π¦ β π΅) β πΆ β π΄) & β’ (π β π΅ β β) & β’ ((π β§ π β β) β βπ₯ β β βπ¦ β π΅ (π₯ β€ π¦ β π β€ πΆ)) β β’ (π β (πΉ β (π¦ β π΅ β¦ πΆ)) β π(1)) | ||
Theorem | rlimcn1 15405* | Image of a limit under a continuous map. (Contributed by Mario Carneiro, 17-Sep-2014.) |
β’ (π β πΊ:π΄βΆπ) & β’ (π β πΆ β π) & β’ (π β πΊ βπ πΆ) & β’ (π β πΉ:πβΆβ) & β’ ((π β§ π₯ β β+) β βπ¦ β β+ βπ§ β π ((absβ(π§ β πΆ)) < π¦ β (absβ((πΉβπ§) β (πΉβπΆ))) < π₯)) β β’ (π β (πΉ β πΊ) βπ (πΉβπΆ)) | ||
Theorem | rlimcn1b 15406* | Image of a limit under a continuous map. (Contributed by Mario Carneiro, 10-May-2016.) |
β’ ((π β§ π β π΄) β π΅ β π) & β’ (π β πΆ β π) & β’ (π β (π β π΄ β¦ π΅) βπ πΆ) & β’ (π β πΉ:πβΆβ) & β’ ((π β§ π₯ β β+) β βπ¦ β β+ βπ§ β π ((absβ(π§ β πΆ)) < π¦ β (absβ((πΉβπ§) β (πΉβπΆ))) < π₯)) β β’ (π β (π β π΄ β¦ (πΉβπ΅)) βπ (πΉβπΆ)) | ||
Theorem | rlimcn3 15407* | Image of a limit under a continuous map, two-arg version. Originally a subproof of rlimcn2 15408. (Contributed by SN, 27-Sep-2024.) |
β’ ((π β§ π§ β π΄) β π΅ β π) & β’ ((π β§ π§ β π΄) β πΆ β π) & β’ ((π β§ π§ β π΄) β (π΅πΉπΆ) β β) & β’ (π β (π πΉπ) β β) & β’ (π β (π§ β π΄ β¦ π΅) βπ π ) & β’ (π β (π§ β π΄ β¦ πΆ) βπ π) & β’ ((π β§ π₯ β β+) β βπ β β+ βπ β β+ βπ’ β π βπ£ β π (((absβ(π’ β π )) < π β§ (absβ(π£ β π)) < π ) β (absβ((π’πΉπ£) β (π πΉπ))) < π₯)) β β’ (π β (π§ β π΄ β¦ (π΅πΉπΆ)) βπ (π πΉπ)) | ||
Theorem | rlimcn2 15408* | Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 17-Sep-2014.) |
β’ ((π β§ π§ β π΄) β π΅ β π) & β’ ((π β§ π§ β π΄) β πΆ β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π§ β π΄ β¦ π΅) βπ π ) & β’ (π β (π§ β π΄ β¦ πΆ) βπ π) & β’ (π β πΉ:(π Γ π)βΆβ) & β’ ((π β§ π₯ β β+) β βπ β β+ βπ β β+ βπ’ β π βπ£ β π (((absβ(π’ β π )) < π β§ (absβ(π£ β π)) < π ) β (absβ((π’πΉπ£) β (π πΉπ))) < π₯)) β β’ (π β (π§ β π΄ β¦ (π΅πΉπΆ)) βπ (π πΉπ)) | ||
Theorem | climcn1 15409* | Image of a limit under a continuous map. (Contributed by Mario Carneiro, 31-Jan-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π΄ β π΅) & β’ ((π β§ π§ β π΅) β (πΉβπ§) β β) & β’ (π β πΊ β π΄) & β’ (π β π» β π) & β’ ((π β§ π₯ β β+) β βπ¦ β β+ βπ§ β π΅ ((absβ(π§ β π΄)) < π¦ β (absβ((πΉβπ§) β (πΉβπ΄))) < π₯)) & β’ ((π β§ π β π) β (πΊβπ) β π΅) & β’ ((π β§ π β π) β (π»βπ) = (πΉβ(πΊβπ))) β β’ (π β π» β (πΉβπ΄)) | ||
Theorem | climcn2 15410* | Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 31-Jan-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π΄ β πΆ) & β’ (π β π΅ β π·) & β’ ((π β§ (π’ β πΆ β§ π£ β π·)) β (π’πΉπ£) β β) & β’ (π β πΊ β π΄) & β’ (π β π» β π΅) & β’ (π β πΎ β π) & β’ ((π β§ π₯ β β+) β βπ¦ β β+ βπ§ β β+ βπ’ β πΆ βπ£ β π· (((absβ(π’ β π΄)) < π¦ β§ (absβ(π£ β π΅)) < π§) β (absβ((π’πΉπ£) β (π΄πΉπ΅))) < π₯)) & β’ ((π β§ π β π) β (πΊβπ) β πΆ) & β’ ((π β§ π β π) β (π»βπ) β π·) & β’ ((π β§ π β π) β (πΎβπ) = ((πΊβπ)πΉ(π»βπ))) β β’ (π β πΎ β (π΄πΉπ΅)) | ||
Theorem | addcn2 15411* | 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 15412* | 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 15413* | 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 15414* | 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 15415* | A sufficient condition for a function to be continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ πΉ:ββΆβ & β’ ((π§ β β β§ π΄ β β) β (absβ((πΉβπ§) β (πΉβπ΄))) β€ (absβ(π§ β π΄))) β β’ ((π΄ β β β§ π₯ β β+) β βπ¦ β β+ βπ§ β β ((absβ(π§ β π΄)) < π¦ β (absβ((πΉβπ§) β (πΉβπ΄))) < π₯)) | ||
Theorem | abscn2 15416* | The absolute value function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ ((π΄ β β β§ π₯ β β+) β βπ¦ β β+ βπ§ β β ((absβ(π§ β π΄)) < π¦ β (absβ((absβπ§) β (absβπ΄))) < π₯)) | ||
Theorem | cjcn2 15417* | The complex conjugate function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ ((π΄ β β β§ π₯ β β+) β βπ¦ β β+ βπ§ β β ((absβ(π§ β π΄)) < π¦ β (absβ((ββπ§) β (ββπ΄))) < π₯)) | ||
Theorem | recn2 15418* | The real part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ ((π΄ β β β§ π₯ β β+) β βπ¦ β β+ βπ§ β β ((absβ(π§ β π΄)) < π¦ β (absβ((ββπ§) β (ββπ΄))) < π₯)) | ||
Theorem | imcn2 15419* | The imaginary part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ ((π΄ β β β§ π₯ β β+) β βπ¦ β β+ βπ§ β β ((absβ(π§ β π΄)) < π¦ β (absβ((ββπ§) β (ββπ΄))) < π₯)) | ||
Theorem | climcn1lem 15420* | The limit of a continuous function, theorem form. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β πΉ β π΄) & β’ (π β πΊ β π) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ π»:ββΆβ & β’ ((π΄ β β β§ π₯ β β+) β βπ¦ β β+ βπ§ β β ((absβ(π§ β π΄)) < π¦ β (absβ((π»βπ§) β (π»βπ΄))) < π₯)) & β’ ((π β§ π β π) β (πΊβπ) = (π»β(πΉβπ))) β β’ (π β πΊ β (π»βπ΄)) | ||
Theorem | climabs 15421* | 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 15422* | 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 15423* | 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 15424* | 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 15425* | Reverse closure for a real limit. (Contributed by Mario Carneiro, 10-May-2016.) |
β’ ((π β§ π β π΄) β π΅ β π) & β’ (π β (π β π΄ β¦ π΅) βπ πΆ) β β’ ((π β§ π β π΄) β π΅ β β) | ||
Theorem | rlimabs 15426* | 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 15427* | 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 15428* | 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 15429* | 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 15430* | Show that a binary operation preserves eventual boundedness. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ ((π β β β§ π β β) β π β β) & β’ ((π₯ β β β§ π¦ β β) β (π₯π π¦) β β) & β’ (((π β β β§ π β β) β§ (π₯ β β β§ π¦ β β)) β (((absβπ₯) β€ π β§ (absβπ¦) β€ π) β (absβ(π₯π π¦)) β€ π)) β β’ ((πΉ β π(1) β§ πΊ β π(1)) β (πΉ βf π πΊ) β π(1)) | ||
Theorem | o1add 15431 | 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 15432 | 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 15433 | 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 15434 | Any function with a finite limit is eventually bounded. (Contributed by Mario Carneiro, 18-Sep-2014.) |
β’ (πΉ βπ π΄ β πΉ β π(1)) | ||
Theorem | rlimdmo1 15435 | A convergent function is eventually bounded. (Contributed by Mario Carneiro, 12-May-2016.) |
β’ (πΉ β dom βπ β πΉ β π(1)) | ||
Theorem | o1rlimmul 15436 | 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 15437* | A constant function is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) (Proof shortened by Mario Carneiro, 26-May-2016.) |
β’ ((π΄ β β β§ π΅ β β) β (π₯ β π΄ β¦ π΅) β π(1)) | ||
Theorem | lo1const 15438* | A constant function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π΄ β β β§ π΅ β β) β (π₯ β π΄ β¦ π΅) β β€π(1)) | ||
Theorem | lo1mptrcl 15439* | Reverse closure for an eventually upper bounded function. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β β€π(1)) β β’ ((π β§ π₯ β π΄) β π΅ β β) | ||
Theorem | o1mptrcl 15440* | Reverse closure for an eventually bounded function. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β π(1)) β β’ ((π β§ π₯ β π΄) β π΅ β β) | ||
Theorem | o1add2 15441* | The sum of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β π(1)) & β’ (π β (π₯ β π΄ β¦ πΆ) β π(1)) β β’ (π β (π₯ β π΄ β¦ (π΅ + πΆ)) β π(1)) | ||
Theorem | o1mul2 15442* | The product of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β π(1)) & β’ (π β (π₯ β π΄ β¦ πΆ) β π(1)) β β’ (π β (π₯ β π΄ β¦ (π΅ Β· πΆ)) β π(1)) | ||
Theorem | o1sub2 15443* | The product of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β π(1)) & β’ (π β (π₯ β π΄ β¦ πΆ) β π(1)) β β’ (π β (π₯ β π΄ β¦ (π΅ β πΆ)) β π(1)) | ||
Theorem | lo1add 15444* | The sum of two eventually upper bounded functions is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) β β€π(1)) & β’ (π β (π₯ β π΄ β¦ πΆ) β β€π(1)) β β’ (π β (π₯ β π΄ β¦ (π΅ + πΆ)) β β€π(1)) | ||
Theorem | lo1mul 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 | lo1mul2 15446* | 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 15447* | 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 15448* | 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 15444. (Contributed by Mario Carneiro, 31-May-2016.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ (π β (π₯ β π΄ β¦ π΅) β β€π(1)) & β’ (π β (π₯ β π΄ β¦ πΆ) β π(1)) β β’ (π β (π₯ β π΄ β¦ (π΅ β πΆ)) β β€π(1)) | ||
Theorem | climadd 15449* | 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 15450* | 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 15451* | 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 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 | climaddc2 15453* | 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 15454* | 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 15455* | Limit of a constant πΆ subtracted from each term of a sequence. (Contributed by Mario Carneiro, 9-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ (π β πΆ β β) & β’ (π β πΊ β π) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) = ((πΉβπ) β πΆ)) β β’ (π β πΊ β (π΄ β πΆ)) | ||
Theorem | climsubc2 15456* | 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 15457* | Comparison of the limits of two sequences. (Contributed by Paul Chapman, 10-Sep-2007.) (Revised by Mario Carneiro, 1-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ (π β πΊ β π΅) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) β β) & β’ ((π β§ π β π) β (πΉβπ) β€ (πΊβπ)) β β’ (π β π΄ β€ π΅) | ||
Theorem | climsqz 15458* | 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 15459* | 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 15460* | 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 15461* | Obsolete version of rlimadd 15460 as of 27-Sep-2024. (Contributed by Mario Carneiro, 22-Sep-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) βπ π·) & β’ (π β (π₯ β π΄ β¦ πΆ) βπ πΈ) β β’ (π β (π₯ β π΄ β¦ (π΅ + πΆ)) βπ (π· + πΈ)) | ||
Theorem | rlimsub 15462* | 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 15463* | 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 15464* | Obsolete version of rlimmul 15463 as of 27-Sep-2024. (Contributed by Mario Carneiro, 22-Sep-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β π) & β’ (π β (π₯ β π΄ β¦ π΅) βπ π·) & β’ (π β (π₯ β π΄ β¦ πΆ) βπ πΈ) β β’ (π β (π₯ β π΄ β¦ (π΅ Β· πΆ)) βπ (π· Β· πΈ)) | ||
Theorem | rlimdiv 15465* | 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 15466* | Limit of the negative of a sequence. (Contributed by Mario Carneiro, 18-May-2016.) |
β’ ((π β§ π β π΄) β π΅ β π) & β’ (π β (π β π΄ β¦ π΅) βπ πΆ) β β’ (π β (π β π΄ β¦ -π΅) βπ -πΆ) | ||
Theorem | rlimle 15467* | Comparison of the limits of two sequences. (Contributed by Mario Carneiro, 10-May-2016.) |
β’ (π β sup(π΄, β*, < ) = +β) & β’ (π β (π₯ β π΄ β¦ π΅) βπ π·) & β’ (π β (π₯ β π΄ β¦ πΆ) βπ πΈ) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ ((π β§ π₯ β π΄) β π΅ β€ πΆ) β β’ (π β π· β€ πΈ) | ||
Theorem | rlimsqzlem 15468* | Lemma for rlimsqz 15469 and rlimsqz2 15470. (Contributed by Mario Carneiro, 18-Sep-2014.) (Revised by Mario Carneiro, 20-May-2016.) |
β’ (π β π β β) & β’ (π β πΈ β β) & β’ (π β (π₯ β π΄ β¦ π΅) βπ π·) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ ((π β§ (π₯ β π΄ β§ π β€ π₯)) β (absβ(πΆ β πΈ)) β€ (absβ(π΅ β π·))) β β’ (π β (π₯ β π΄ β¦ πΆ) βπ πΈ) | ||
Theorem | rlimsqz 15469* | 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 15470* | 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 15471* | Transfer eventual upper boundedness from a larger function to a smaller function. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ (π β π β β) & β’ (π β (π₯ β π΄ β¦ π΅) β β€π(1)) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ ((π β§ (π₯ β π΄ β§ π β€ π₯)) β πΆ β€ π΅) β β’ (π β (π₯ β π΄ β¦ πΆ) β β€π(1)) | ||
Theorem | o1le 15472* | 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 15473* | A function whose inverse converges to zero is unbounded. (Contributed by Mario Carneiro, 30-May-2016.) |
β’ (π β sup(π΄, β*, < ) = +β) & β’ (π β (π₯ β π΄ β¦ (1 / π΅)) βπ 0) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β π΅ β 0) β β’ (π β Β¬ (π₯ β π΄ β¦ π΅) β π(1)) | ||
Theorem | clim2ser 15474* | 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 15475* | 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 15476* | 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 15477* | 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 15478* | 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 15479* | 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 15480* | 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 15481* | 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 15482* | 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 15483 | 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 15484* | Lemma for isercoll 15487. (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ:ββΆπ) & β’ ((π β§ π β β) β (πΊβπ) < (πΊβ(π + 1))) β β’ ((π β§ π β β) β (πΊ βΎ π) Isom < , < (π, (πΊ β π))) | ||
Theorem | isercolllem2 15485* | Lemma for isercoll 15487. (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ:ββΆπ) & β’ ((π β§ π β β) β (πΊβπ) < (πΊβ(π + 1))) β β’ ((π β§ π β (β€β₯β(πΊβ1))) β (1...(β―β(πΊ β (β‘πΊ β (π...π))))) = (β‘πΊ β (π...π))) | ||
Theorem | isercolllem3 15486* | Lemma for isercoll 15487. (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ:ββΆπ) & β’ ((π β§ π β β) β (πΊβπ) < (πΊβ(π + 1))) & β’ ((π β§ π β (π β ran πΊ)) β (πΉβπ) = 0) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β β) β (π»βπ) = (πΉβ(πΊβπ))) β β’ ((π β§ π β (β€β₯β(πΊβ1))) β (seqπ( + , πΉ)βπ) = (seq1( + , π»)β(β―β(πΊ β (β‘πΊ β (π...π)))))) | ||
Theorem | isercoll 15487* | 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 15488* | Generalize isercoll 15487 so that both sequences have arbitrary starting point. (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β πΊ:πβΆπ) & β’ ((π β§ π β π) β (πΊβπ) < (πΊβ(π + 1))) & β’ ((π β§ π β (π β ran πΊ)) β (πΉβπ) = 0) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (π»βπ) = (πΉβ(πΊβπ))) β β’ (π β (seqπ( + , π») β π΄ β seqπ( + , πΉ) β π΄)) | ||
Theorem | climsup 15489* | 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 15490* | 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 15491* | A converging sequence of complex numbers is bounded. (Contributed by Mario Carneiro, 9-Jul-2017.) |
β’ π = (β€β₯βπ) β β’ ((π β β€ β§ πΉ β dom β β§ βπ β π (πΉβπ) β β) β βπ₯ β β βπ β π (absβ(πΉβπ)) β€ π₯) | ||
Theorem | caucvgrlem 15492* | Lemma for caurcvgr 15493. (Contributed by Mario Carneiro, 15-Feb-2014.) (Revised by AV, 12-Sep-2020.) |
β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β sup(π΄, β*, < ) = +β) & β’ (π β βπ₯ β β+ βπ β π΄ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π₯)) & β’ (π β π β β+) β β’ (π β βπ β π΄ ((lim supβπΉ) β β β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· π )))) | ||
Theorem | caurcvgr 15493* | 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 15494* | Lemma for caucvgr 15495. (Contributed by NM, 4-Apr-2005.) (Proof shortened by Mario Carneiro, 8-May-2016.) |
β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β sup(π΄, β*, < ) = +β) & β’ (π β βπ₯ β β+ βπ β π΄ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π₯)) & β’ π»:ββΆβ & β’ (((πΉβπ) β β β§ (πΉβπ) β β) β (absβ((π»β(πΉβπ)) β (π»β(πΉβπ)))) β€ (absβ((πΉβπ) β (πΉβπ)))) β β’ (π β (π β π΄ β¦ (π»β(πΉβπ))) βπ ( βπ β(π» β πΉ))) | ||
Theorem | caucvgr 15495* | 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 15496* | 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 15497* | 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 15498* | 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 15499* | 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 15500* | 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) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |