![]() |
Metamath
Proof Explorer Theorem List (p. 155 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | absled 15401 | Absolute value and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β ((absβπ΄) β€ π΅ β (-π΅ β€ π΄ β§ π΄ β€ π΅))) | ||
Theorem | abssubge0d 15402 | Absolute value of a nonnegative difference. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) β β’ (π β (absβ(π΅ β π΄)) = (π΅ β π΄)) | ||
Theorem | abssuble0d 15403 | Absolute value of a nonpositive difference. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) β β’ (π β (absβ(π΄ β π΅)) = (π΅ β π΄)) | ||
Theorem | absdifltd 15404 | The absolute value of a difference and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β ((absβ(π΄ β π΅)) < πΆ β ((π΅ β πΆ) < π΄ β§ π΄ < (π΅ + πΆ)))) | ||
Theorem | absdifled 15405 | The absolute value of a difference and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β ((absβ(π΄ β π΅)) β€ πΆ β ((π΅ β πΆ) β€ π΄ β§ π΄ β€ (π΅ + πΆ)))) | ||
Theorem | icodiamlt 15406 | Two elements in a half-open interval have separation strictly less than the difference between the endpoints. (Contributed by Stefan O'Rear, 12-Sep-2014.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β (π΄[,)π΅) β§ π· β (π΄[,)π΅))) β (absβ(πΆ β π·)) < (π΅ β π΄)) | ||
Theorem | abscld 15407 | Real closure of absolute value. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (absβπ΄) β β) | ||
Theorem | sqrtcld 15408 | Closure of the square root function over the complex numbers. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (ββπ΄) β β) | ||
Theorem | sqrtrege0d 15409 | The real part of the square root function is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β 0 β€ (ββ(ββπ΄))) | ||
Theorem | sqsqrtd 15410 | Square root theorem. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β ((ββπ΄)β2) = π΄) | ||
Theorem | msqsqrtd 15411 | Square root theorem. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β ((ββπ΄) Β· (ββπ΄)) = π΄) | ||
Theorem | sqr00d 15412 | A square root is zero iff its argument is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β (ββπ΄) = 0) β β’ (π β π΄ = 0) | ||
Theorem | absvalsqd 15413 | Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β ((absβπ΄)β2) = (π΄ Β· (ββπ΄))) | ||
Theorem | absvalsq2d 15414 | Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β ((absβπ΄)β2) = (((ββπ΄)β2) + ((ββπ΄)β2))) | ||
Theorem | absge0d 15415 | Absolute value is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β 0 β€ (absβπ΄)) | ||
Theorem | absval2d 15416 | Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (absβπ΄) = (ββ(((ββπ΄)β2) + ((ββπ΄)β2)))) | ||
Theorem | abs00d 15417 | The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β (absβπ΄) = 0) β β’ (π β π΄ = 0) | ||
Theorem | absne0d 15418 | The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΄ β 0) β β’ (π β (absβπ΄) β 0) | ||
Theorem | absrpcld 15419 | The absolute value of a nonzero number is a positive real. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΄ β 0) β β’ (π β (absβπ΄) β β+) | ||
Theorem | absnegd 15420 | Absolute value of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (absβ-π΄) = (absβπ΄)) | ||
Theorem | abscjd 15421 | The absolute value of a number and its conjugate are the same. Proposition 10-3.7(b) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (absβ(ββπ΄)) = (absβπ΄)) | ||
Theorem | releabsd 15422 | The real part of a number is less than or equal to its absolute value. Proposition 10-3.7(d) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (ββπ΄) β€ (absβπ΄)) | ||
Theorem | absexpd 15423 | Absolute value of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π β β0) β β’ (π β (absβ(π΄βπ)) = ((absβπ΄)βπ)) | ||
Theorem | abssubd 15424 | Swapping order of subtraction doesn't change the absolute value. Example of [Apostol] p. 363. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (absβ(π΄ β π΅)) = (absβ(π΅ β π΄))) | ||
Theorem | absmuld 15425 | Absolute value distributes over multiplication. Proposition 10-3.7(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (absβ(π΄ Β· π΅)) = ((absβπ΄) Β· (absβπ΅))) | ||
Theorem | absdivd 15426 | Absolute value distributes over division. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΅ β 0) β β’ (π β (absβ(π΄ / π΅)) = ((absβπ΄) / (absβπ΅))) | ||
Theorem | abstrid 15427 | Triangle inequality for absolute value. Proposition 10-3.7(h) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (absβ(π΄ + π΅)) β€ ((absβπ΄) + (absβπ΅))) | ||
Theorem | abs2difd 15428 | Difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β ((absβπ΄) β (absβπ΅)) β€ (absβ(π΄ β π΅))) | ||
Theorem | abs2dif2d 15429 | Difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (absβ(π΄ β π΅)) β€ ((absβπ΄) + (absβπ΅))) | ||
Theorem | abs2difabsd 15430 | Absolute value of difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (absβ((absβπ΄) β (absβπ΅))) β€ (absβ(π΄ β π΅))) | ||
Theorem | abs3difd 15431 | Absolute value of differences around common element. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β (absβ(π΄ β π΅)) β€ ((absβ(π΄ β πΆ)) + (absβ(πΆ β π΅)))) | ||
Theorem | abs3lemd 15432 | Lemma involving absolute value of differences. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β (absβ(π΄ β πΆ)) < (π· / 2)) & β’ (π β (absβ(πΆ β π΅)) < (π· / 2)) β β’ (π β (absβ(π΄ β π΅)) < π·) | ||
Theorem | reusq0 15433* | A complex number is the square of exactly one complex number iff the given complex number is zero. (Contributed by AV, 21-Jun-2023.) |
β’ (π β β β (β!π₯ β β (π₯β2) = π β π = 0)) | ||
Theorem | bhmafibid1cn 15434 | The Brahmagupta-Fibonacci identity for complex numbers. Express the product of two sums of two squares as a sum of two squares. First result. (Contributed by Thierry Arnoux, 1-Feb-2020.) Generalization for complex numbers proposed by GL. (Revised by AV, 8-Jun-2023.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β (((π΄β2) + (π΅β2)) Β· ((πΆβ2) + (π·β2))) = ((((π΄ Β· πΆ) β (π΅ Β· π·))β2) + (((π΄ Β· π·) + (π΅ Β· πΆ))β2))) | ||
Theorem | bhmafibid2cn 15435 | The Brahmagupta-Fibonacci identity for complex numbers. Express the product of two sums of two squares as a sum of two squares. Second result. (Contributed by Thierry Arnoux, 1-Feb-2020.) Generalization for complex numbers proposed by GL. (Revised by AV, 8-Jun-2023.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β (((π΄β2) + (π΅β2)) Β· ((πΆβ2) + (π·β2))) = ((((π΄ Β· πΆ) + (π΅ Β· π·))β2) + (((π΄ Β· π·) β (π΅ Β· πΆ))β2))) | ||
Theorem | bhmafibid1 15436 | The Brahmagupta-Fibonacci identity. Express the product of two sums of two squares as a sum of two squares. First result. Remark: The proof uses a different approach than the proof of bhmafibid1cn 15434, and is a little bit shorter. (Contributed by Thierry Arnoux, 1-Feb-2020.) (Proof modification is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β (((π΄β2) + (π΅β2)) Β· ((πΆβ2) + (π·β2))) = ((((π΄ Β· πΆ) β (π΅ Β· π·))β2) + (((π΄ Β· π·) + (π΅ Β· πΆ))β2))) | ||
Theorem | bhmafibid2 15437 | The Brahmagupta-Fibonacci identity. Express the product of two sums of two squares as a sum of two squares. Second result. (Contributed by Thierry Arnoux, 1-Feb-2020.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β (((π΄β2) + (π΅β2)) Β· ((πΆβ2) + (π·β2))) = ((((π΄ Β· πΆ) + (π΅ Β· π·))β2) + (((π΄ Β· π·) β (π΅ Β· πΆ))β2))) | ||
Syntax | clsp 15438 | Extend class notation to include the limsup function. |
class lim sup | ||
Definition | df-limsup 15439* | Define the superior limit of an infinite sequence of extended real numbers. Definition 12-4.1 of [Gleason] p. 175. See limsupval 15442 for its value. (Contributed by NM, 26-Oct-2005.) (Revised by AV, 11-Sep-2020.) |
β’ lim sup = (π₯ β V β¦ inf(ran (π β β β¦ sup(((π₯ β (π[,)+β)) β© β*), β*, < )), β*, < )) | ||
Theorem | limsupgord 15440 | Ordering property of the superior limit function. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-May-2016.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ β€ π΅) β sup(((πΉ β (π΅[,)+β)) β© β*), β*, < ) β€ sup(((πΉ β (π΄[,)+β)) β© β*), β*, < )) | ||
Theorem | limsupcl 15441 | Closure of the superior limit. (Contributed by NM, 26-Oct-2005.) (Revised by AV, 12-Sep-2020.) |
β’ (πΉ β π β (lim supβπΉ) β β*) | ||
Theorem | limsupval 15442* | The superior limit of an infinite sequence πΉ of extended real numbers, which is the infimum of the set of suprema of all upper infinite subsequences of πΉ. Definition 12-4.1 of [Gleason] p. 175. (Contributed by NM, 26-Oct-2005.) (Revised by AV, 12-Sep-2014.) |
β’ πΊ = (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*), β*, < )) β β’ (πΉ β π β (lim supβπΉ) = inf(ran πΊ, β*, < )) | ||
Theorem | limsupgf 15443* | Closure of the superior limit function. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-May-2016.) |
β’ πΊ = (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*), β*, < )) β β’ πΊ:ββΆβ* | ||
Theorem | limsupgval 15444* | Value of the superior limit function. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-May-2016.) |
β’ πΊ = (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*), β*, < )) β β’ (π β β β (πΊβπ) = sup(((πΉ β (π[,)+β)) β© β*), β*, < )) | ||
Theorem | limsupgle 15445* | The defining property of the superior limit function. (Contributed by Mario Carneiro, 5-Sep-2014.) (Revised by Mario Carneiro, 7-May-2016.) |
β’ πΊ = (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*), β*, < )) β β’ (((π΅ β β β§ πΉ:π΅βΆβ*) β§ πΆ β β β§ π΄ β β*) β ((πΊβπΆ) β€ π΄ β βπ β π΅ (πΆ β€ π β (πΉβπ) β€ π΄))) | ||
Theorem | limsuple 15446* | The defining property of the superior limit. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 12-Sep-2020.) |
β’ πΊ = (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*), β*, < )) β β’ ((π΅ β β β§ πΉ:π΅βΆβ* β§ π΄ β β*) β (π΄ β€ (lim supβπΉ) β βπ β β π΄ β€ (πΊβπ))) | ||
Theorem | limsuplt 15447* | The defining property of the superior limit. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 12-Sep-2020.) |
β’ πΊ = (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*), β*, < )) β β’ ((π΅ β β β§ πΉ:π΅βΆβ* β§ π΄ β β*) β ((lim supβπΉ) < π΄ β βπ β β (πΊβπ) < π΄)) | ||
Theorem | limsupval2 15448* | The superior limit, relativized to an unbounded set. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 12-Sep-2020.) |
β’ πΊ = (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*), β*, < )) & β’ (π β πΉ β π) & β’ (π β π΄ β β) & β’ (π β sup(π΄, β*, < ) = +β) β β’ (π β (lim supβπΉ) = inf((πΊ β π΄), β*, < )) | ||
Theorem | limsupgre 15449* | If a sequence of real numbers has upper bounded limit supremum, then all the partial suprema are real. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 12-Sep-2020.) |
β’ πΊ = (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*), β*, < )) & β’ π = (β€β₯βπ) β β’ ((π β β€ β§ πΉ:πβΆβ β§ (lim supβπΉ) < +β) β πΊ:ββΆβ) | ||
Theorem | limsupbnd1 15450* | If a sequence is eventually at most π΄, then the limsup is also at most π΄. (The converse is only true if the less or equal is replaced by strictly less than; consider the sequence 1 / π which is never less or equal to zero even though the limsup is.) (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 12-Sep-2020.) |
β’ (π β π΅ β β) & β’ (π β πΉ:π΅βΆβ*) & β’ (π β π΄ β β*) & β’ (π β βπ β β βπ β π΅ (π β€ π β (πΉβπ) β€ π΄)) β β’ (π β (lim supβπΉ) β€ π΄) | ||
Theorem | limsupbnd2 15451* | If a sequence is eventually greater than π΄, then the limsup is also greater than π΄. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 12-Sep-2020.) |
β’ (π β π΅ β β) & β’ (π β πΉ:π΅βΆβ*) & β’ (π β π΄ β β*) & β’ (π β sup(π΅, β*, < ) = +β) & β’ (π β βπ β β βπ β π΅ (π β€ π β π΄ β€ (πΉβπ))) β β’ (π β π΄ β€ (lim supβπΉ)) | ||
Syntax | cli 15452 | Extend class notation with convergence relation for limits. |
class β | ||
Syntax | crli 15453 | Extend class notation with real convergence relation for limits. |
class βπ | ||
Syntax | co1 15454 | Extend class notation with the set of all eventually bounded functions. |
class π(1) | ||
Syntax | clo1 15455 | Extend class notation with the set of all eventually upper bounded functions. |
class β€π(1) | ||
Definition | df-clim 15456* | Define the limit relation for complex number sequences. See clim 15462 for its relational expression. (Contributed by NM, 28-Aug-2005.) |
β’ β = {β¨π, π¦β© β£ (π¦ β β β§ βπ₯ β β+ βπ β β€ βπ β (β€β₯βπ)((πβπ) β β β§ (absβ((πβπ) β π¦)) < π₯))} | ||
Definition | df-rlim 15457* | Define the limit relation for partial functions on the reals. See rlim 15463 for its relational expression. (Contributed by Mario Carneiro, 16-Sep-2014.) |
β’ βπ = {β¨π, π₯β© β£ ((π β (β βpm β) β§ π₯ β β) β§ βπ¦ β β+ βπ§ β β βπ€ β dom π(π§ β€ π€ β (absβ((πβπ€) β π₯)) < π¦))} | ||
Definition | df-o1 15458* | Define the set of eventually bounded functions. We don't bother to build the full conception of big-O notation, because we can represent any big-O in terms of π(1) and division, and any little-O in terms of a limit and division. We could also use limsup for this, but it only works on integer sequences, while this will work for real sequences or integer sequences. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ π(1) = {π β (β βpm β) β£ βπ₯ β β βπ β β βπ¦ β (dom π β© (π₯[,)+β))(absβ(πβπ¦)) β€ π} | ||
Definition | df-lo1 15459* | Define the set of eventually upper bounded real functions. This fills a gap in π(1) coverage, to express statements like π(π₯) β€ π(π₯) + π(π₯) via (π₯ β β+ β¦ (π(π₯) β π(π₯)) / π₯) β β€π(1). (Contributed by Mario Carneiro, 25-May-2016.) |
β’ β€π(1) = {π β (β βpm β) β£ βπ₯ β β βπ β β βπ¦ β (dom π β© (π₯[,)+β))(πβπ¦) β€ π} | ||
Theorem | climrel 15460 | The limit relation is a relation. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.) |
β’ Rel β | ||
Theorem | rlimrel 15461 | The limit relation is a relation. (Contributed by Mario Carneiro, 24-Sep-2014.) |
β’ Rel βπ | ||
Theorem | clim 15462* | Express the predicate: The limit of complex number sequence πΉ is π΄, or πΉ converges to π΄. This means that for any real π₯, no matter how small, there always exists an integer π such that the absolute difference of any later complex number in the sequence and the limit is less than π₯. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ (π β πΉ β π) & β’ ((π β§ π β β€) β (πΉβπ) = π΅) β β’ (π β (πΉ β π΄ β (π΄ β β β§ βπ₯ β β+ βπ β β€ βπ β (β€β₯βπ)(π΅ β β β§ (absβ(π΅ β π΄)) < π₯)))) | ||
Theorem | rlim 15463* | Express the predicate: The limit of complex number function πΉ is πΆ, or πΉ converges to πΆ, in the real sense. This means that for any real π₯, no matter how small, there always exists a number π¦ such that the absolute difference of any number in the function beyond π¦ and the limit is less than π₯. (Contributed by Mario Carneiro, 16-Sep-2014.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β β) & β’ ((π β§ π§ β π΄) β (πΉβπ§) = π΅) β β’ (π β (πΉ βπ πΆ β (πΆ β β β§ βπ₯ β β+ βπ¦ β β βπ§ β π΄ (π¦ β€ π§ β (absβ(π΅ β πΆ)) < π₯)))) | ||
Theorem | rlim2 15464* | Rewrite rlim 15463 for a mapping operation. (Contributed by Mario Carneiro, 16-Sep-2014.) (Revised by Mario Carneiro, 28-Feb-2015.) |
β’ (π β βπ§ β π΄ π΅ β β) & β’ (π β π΄ β β) & β’ (π β πΆ β β) β β’ (π β ((π§ β π΄ β¦ π΅) βπ πΆ β βπ₯ β β+ βπ¦ β β βπ§ β π΄ (π¦ β€ π§ β (absβ(π΅ β πΆ)) < π₯))) | ||
Theorem | rlim2lt 15465* | Use strictly less-than in place of less equal in the real limit predicate. (Contributed by Mario Carneiro, 18-Sep-2014.) |
β’ (π β βπ§ β π΄ π΅ β β) & β’ (π β π΄ β β) & β’ (π β πΆ β β) β β’ (π β ((π§ β π΄ β¦ π΅) βπ πΆ β βπ₯ β β+ βπ¦ β β βπ§ β π΄ (π¦ < π§ β (absβ(π΅ β πΆ)) < π₯))) | ||
Theorem | rlim3 15466* | Restrict the range of the domain bound to reals greater than some π· β β. (Contributed by Mario Carneiro, 16-Sep-2014.) |
β’ (π β βπ§ β π΄ π΅ β β) & β’ (π β π΄ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) β β’ (π β ((π§ β π΄ β¦ π΅) βπ πΆ β βπ₯ β β+ βπ¦ β (π·[,)+β)βπ§ β π΄ (π¦ β€ π§ β (absβ(π΅ β πΆ)) < π₯))) | ||
Theorem | climcl 15467 | Closure of the limit of a sequence of complex numbers. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ (πΉ β π΄ β π΄ β β) | ||
Theorem | rlimpm 15468 | Closure of a function with a limit in the complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014.) |
β’ (πΉ βπ π΄ β πΉ β (β βpm β)) | ||
Theorem | rlimf 15469 | Closure of a function with a limit in the complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014.) |
β’ (πΉ βπ π΄ β πΉ:dom πΉβΆβ) | ||
Theorem | rlimss 15470 | Domain closure of a function with a limit in the complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014.) |
β’ (πΉ βπ π΄ β dom πΉ β β) | ||
Theorem | rlimcl 15471 | Closure of the limit of a sequence of complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ (πΉ βπ π΄ β π΄ β β) | ||
Theorem | clim2 15472* | Express the predicate: The limit of complex number sequence πΉ is π΄, or πΉ converges to π΄, with more general quantifier restrictions than clim 15462. (Contributed by NM, 6-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π) & β’ ((π β§ π β π) β (πΉβπ) = π΅) β β’ (π β (πΉ β π΄ β (π΄ β β β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π΅ β β β§ (absβ(π΅ β π΄)) < π₯)))) | ||
Theorem | clim2c 15473* | Express the predicate πΉ converges to π΄. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π) & β’ ((π β§ π β π) β (πΉβπ) = π΅) & β’ (π β π΄ β β) & β’ ((π β§ π β π) β π΅ β β) β β’ (π β (πΉ β π΄ β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ(π΅ β π΄)) < π₯)) | ||
Theorem | clim0 15474* | Express the predicate πΉ converges to 0. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π) & β’ ((π β§ π β π) β (πΉβπ) = π΅) β β’ (π β (πΉ β 0 β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π΅ β β β§ (absβπ΅) < π₯))) | ||
Theorem | clim0c 15475* | Express the predicate πΉ converges to 0. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π) & β’ ((π β§ π β π) β (πΉβπ) = π΅) & β’ ((π β§ π β π) β π΅ β β) β β’ (π β (πΉ β 0 β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβπ΅) < π₯)) | ||
Theorem | rlim0 15476* | Express the predicate π΅(π§) converges to 0. (Contributed by Mario Carneiro, 16-Sep-2014.) (Revised by Mario Carneiro, 28-Feb-2015.) |
β’ (π β βπ§ β π΄ π΅ β β) & β’ (π β π΄ β β) β β’ (π β ((π§ β π΄ β¦ π΅) βπ 0 β βπ₯ β β+ βπ¦ β β βπ§ β π΄ (π¦ β€ π§ β (absβπ΅) < π₯))) | ||
Theorem | rlim0lt 15477* | Use strictly less-than in place of less equal in the real limit predicate. (Contributed by Mario Carneiro, 18-Sep-2014.) (Revised by Mario Carneiro, 28-Feb-2015.) |
β’ (π β βπ§ β π΄ π΅ β β) & β’ (π β π΄ β β) β β’ (π β ((π§ β π΄ β¦ π΅) βπ 0 β βπ₯ β β+ βπ¦ β β βπ§ β π΄ (π¦ < π§ β (absβπ΅) < π₯))) | ||
Theorem | climi 15478* | Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΆ β β+) & β’ ((π β§ π β π) β (πΉβπ) = π΅) & β’ (π β πΉ β π΄) β β’ (π β βπ β π βπ β (β€β₯βπ)(π΅ β β β§ (absβ(π΅ β π΄)) < πΆ)) | ||
Theorem | climi2 15479* | Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΆ β β+) & β’ ((π β§ π β π) β (πΉβπ) = π΅) & β’ (π β πΉ β π΄) β β’ (π β βπ β π βπ β (β€β₯βπ)(absβ(π΅ β π΄)) < πΆ) | ||
Theorem | climi0 15480* | Convergence of a sequence of complex numbers to zero. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΆ β β+) & β’ ((π β§ π β π) β (πΉβπ) = π΅) & β’ (π β πΉ β 0) β β’ (π β βπ β π βπ β (β€β₯βπ)(absβπ΅) < πΆ) | ||
Theorem | rlimi 15481* | Convergence at infinity of a function on the reals. (Contributed by Mario Carneiro, 28-Feb-2015.) |
β’ (π β βπ§ β π΄ π΅ β π) & β’ (π β π β β+) & β’ (π β (π§ β π΄ β¦ π΅) βπ πΆ) β β’ (π β βπ¦ β β βπ§ β π΄ (π¦ β€ π§ β (absβ(π΅ β πΆ)) < π )) | ||
Theorem | rlimi2 15482* | Convergence at infinity of a function on the reals. (Contributed by Mario Carneiro, 12-May-2016.) |
β’ (π β βπ§ β π΄ π΅ β π) & β’ (π β π β β+) & β’ (π β (π§ β π΄ β¦ π΅) βπ πΆ) & β’ (π β π· β β) β β’ (π β βπ¦ β (π·[,)+β)βπ§ β π΄ (π¦ β€ π§ β (absβ(π΅ β πΆ)) < π )) | ||
Theorem | ello1 15483* | Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ (πΉ β β€π(1) β (πΉ β (β βpm β) β§ βπ₯ β β βπ β β βπ¦ β (dom πΉ β© (π₯[,)+β))(πΉβπ¦) β€ π)) | ||
Theorem | ello12 15484* | Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β (πΉ β β€π(1) β βπ₯ β β βπ β β βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ π))) | ||
Theorem | ello12r 15485* | Sufficient condition for elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ (πΆ β β β§ π β β) β§ βπ₯ β π΄ (πΆ β€ π₯ β (πΉβπ₯) β€ π)) β πΉ β β€π(1)) | ||
Theorem | lo1f 15486 | An eventually upper bounded function is a function. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ (πΉ β β€π(1) β πΉ:dom πΉβΆβ) | ||
Theorem | lo1dm 15487 | An eventually upper bounded function's domain is a subset of the reals. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ (πΉ β β€π(1) β dom πΉ β β) | ||
Theorem | lo1bdd 15488* | The defining property of an eventually upper bounded function. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((πΉ β β€π(1) β§ πΉ:π΄βΆβ) β βπ₯ β β βπ β β βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ π)) | ||
Theorem | ello1mpt 15489* | Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ (π β π΄ β β) & β’ ((π β§ π₯ β π΄) β π΅ β β) β β’ (π β ((π₯ β π΄ β¦ π΅) β β€π(1) β βπ¦ β β βπ β β βπ₯ β π΄ (π¦ β€ π₯ β π΅ β€ π))) | ||
Theorem | ello1mpt2 15490* | Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ (π β π΄ β β) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β πΆ β β) β β’ (π β ((π₯ β π΄ β¦ π΅) β β€π(1) β βπ¦ β (πΆ[,)+β)βπ β β βπ₯ β π΄ (π¦ β€ π₯ β π΅ β€ π))) | ||
Theorem | ello1d 15491* | Sufficient condition for elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ (π β π΄ β β) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π β β) & β’ ((π β§ (π₯ β π΄ β§ πΆ β€ π₯)) β π΅ β€ π) β β’ (π β (π₯ β π΄ β¦ π΅) β β€π(1)) | ||
Theorem | lo1bdd2 15492* | If an eventually bounded function is bounded on every interval π΄ β© (-β, π¦) by a function π(π¦), then the function is bounded on the whole domain. (Contributed by Mario Carneiro, 9-Apr-2016.) |
β’ (π β π΄ β β) & β’ (π β πΆ β β) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β (π₯ β π΄ β¦ π΅) β β€π(1)) & β’ ((π β§ (π¦ β β β§ πΆ β€ π¦)) β π β β) & β’ (((π β§ π₯ β π΄) β§ ((π¦ β β β§ πΆ β€ π¦) β§ π₯ < π¦)) β π΅ β€ π) β β’ (π β βπ β β βπ₯ β π΄ π΅ β€ π) | ||
Theorem | lo1bddrp 15493* | Refine o1bdd2 15509 to give a strictly positive upper bound. (Contributed by Mario Carneiro, 25-May-2016.) |
β’ (π β π΄ β β) & β’ (π β πΆ β β) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β (π₯ β π΄ β¦ π΅) β β€π(1)) & β’ ((π β§ (π¦ β β β§ πΆ β€ π¦)) β π β β) & β’ (((π β§ π₯ β π΄) β§ ((π¦ β β β§ πΆ β€ π¦) β§ π₯ < π¦)) β π΅ β€ π) β β’ (π β βπ β β+ βπ₯ β π΄ π΅ β€ π) | ||
Theorem | elo1 15494* | Elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ (πΉ β π(1) β (πΉ β (β βpm β) β§ βπ₯ β β βπ β β βπ¦ β (dom πΉ β© (π₯[,)+β))(absβ(πΉβπ¦)) β€ π)) | ||
Theorem | elo12 15495* | Elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β (πΉ β π(1) β βπ₯ β β βπ β β βπ¦ β π΄ (π₯ β€ π¦ β (absβ(πΉβπ¦)) β€ π))) | ||
Theorem | elo12r 15496* | Sufficient condition for elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ (πΆ β β β§ π β β) β§ βπ₯ β π΄ (πΆ β€ π₯ β (absβ(πΉβπ₯)) β€ π)) β πΉ β π(1)) | ||
Theorem | o1f 15497 | An eventually bounded function is a function. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ (πΉ β π(1) β πΉ:dom πΉβΆβ) | ||
Theorem | o1dm 15498 | An eventually bounded function's domain is a subset of the reals. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ (πΉ β π(1) β dom πΉ β β) | ||
Theorem | o1bdd 15499* | The defining property of an eventually bounded function. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ ((πΉ β π(1) β§ πΉ:π΄βΆβ) β βπ₯ β β βπ β β βπ¦ β π΄ (π₯ β€ π¦ β (absβ(πΉβπ¦)) β€ π)) | ||
Theorem | lo1o1 15500 | A function is eventually bounded iff its absolute value is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ (πΉ:π΄βΆβ β (πΉ β π(1) β (abs β πΉ) β β€π(1))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |