![]() |
Metamath
Proof Explorer Theorem List (p. 155 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sqrtltd 15401 | Square root is strictly monotonic. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) & β’ (π β π΅ β β) & β’ (π β 0 β€ π΅) β β’ (π β (π΄ < π΅ β (ββπ΄) < (ββπ΅))) | ||
Theorem | sqr11d 15402 | The square root function is one-to-one. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) & β’ (π β π΅ β β) & β’ (π β 0 β€ π΅) & β’ (π β (ββπ΄) = (ββπ΅)) β β’ (π β π΄ = π΅) | ||
Theorem | absltd 15403 | Absolute value and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β ((absβπ΄) < π΅ β (-π΅ < π΄ β§ π΄ < π΅))) | ||
Theorem | absled 15404 | Absolute value and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β ((absβπ΄) β€ π΅ β (-π΅ β€ π΄ β§ π΄ β€ π΅))) | ||
Theorem | abssubge0d 15405 | Absolute value of a nonnegative difference. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) β β’ (π β (absβ(π΅ β π΄)) = (π΅ β π΄)) | ||
Theorem | abssuble0d 15406 | Absolute value of a nonpositive difference. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) β β’ (π β (absβ(π΄ β π΅)) = (π΅ β π΄)) | ||
Theorem | absdifltd 15407 | The absolute value of a difference and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β ((absβ(π΄ β π΅)) < πΆ β ((π΅ β πΆ) < π΄ β§ π΄ < (π΅ + πΆ)))) | ||
Theorem | absdifled 15408 | The absolute value of a difference and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β ((absβ(π΄ β π΅)) β€ πΆ β ((π΅ β πΆ) β€ π΄ β§ π΄ β€ (π΅ + πΆ)))) | ||
Theorem | icodiamlt 15409 | 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 15410 | Real closure of absolute value. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (absβπ΄) β β) | ||
Theorem | sqrtcld 15411 | Closure of the square root function over the complex numbers. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (ββπ΄) β β) | ||
Theorem | sqrtrege0d 15412 | The real part of the square root function is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β 0 β€ (ββ(ββπ΄))) | ||
Theorem | sqsqrtd 15413 | Square root theorem. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β ((ββπ΄)β2) = π΄) | ||
Theorem | msqsqrtd 15414 | Square root theorem. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β ((ββπ΄) Β· (ββπ΄)) = π΄) | ||
Theorem | sqr00d 15415 | A square root is zero iff its argument is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β (ββπ΄) = 0) β β’ (π β π΄ = 0) | ||
Theorem | absvalsqd 15416 | Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β ((absβπ΄)β2) = (π΄ Β· (ββπ΄))) | ||
Theorem | absvalsq2d 15417 | Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β ((absβπ΄)β2) = (((ββπ΄)β2) + ((ββπ΄)β2))) | ||
Theorem | absge0d 15418 | Absolute value is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β 0 β€ (absβπ΄)) | ||
Theorem | absval2d 15419 | Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (absβπ΄) = (ββ(((ββπ΄)β2) + ((ββπ΄)β2)))) | ||
Theorem | abs00d 15420 | 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 15421 | 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 15422 | The absolute value of a nonzero number is a positive real. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΄ β 0) β β’ (π β (absβπ΄) β β+) | ||
Theorem | absnegd 15423 | Absolute value of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (absβ-π΄) = (absβπ΄)) | ||
Theorem | abscjd 15424 | 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 15425 | 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 15426 | Absolute value of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π β β0) β β’ (π β (absβ(π΄βπ)) = ((absβπ΄)βπ)) | ||
Theorem | abssubd 15427 | 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 15428 | 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 15429 | Absolute value distributes over division. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΅ β 0) β β’ (π β (absβ(π΄ / π΅)) = ((absβπ΄) / (absβπ΅))) | ||
Theorem | abstrid 15430 | 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 15431 | Difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β ((absβπ΄) β (absβπ΅)) β€ (absβ(π΄ β π΅))) | ||
Theorem | abs2dif2d 15432 | Difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (absβ(π΄ β π΅)) β€ ((absβπ΄) + (absβπ΅))) | ||
Theorem | abs2difabsd 15433 | Absolute value of difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (absβ((absβπ΄) β (absβπ΅))) β€ (absβ(π΄ β π΅))) | ||
Theorem | abs3difd 15434 | Absolute value of differences around common element. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β (absβ(π΄ β π΅)) β€ ((absβ(π΄ β πΆ)) + (absβ(πΆ β π΅)))) | ||
Theorem | abs3lemd 15435 | Lemma involving absolute value of differences. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β (absβ(π΄ β πΆ)) < (π· / 2)) & β’ (π β (absβ(πΆ β π΅)) < (π· / 2)) β β’ (π β (absβ(π΄ β π΅)) < π·) | ||
Theorem | reusq0 15436* | 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 15437 | 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 15438 | 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 15439 | 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 15437, 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 15440 | 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 15441 | Extend class notation to include the limsup function. |
class lim sup | ||
Definition | df-limsup 15442* | Define the superior limit of an infinite sequence of extended real numbers. Definition 12-4.1 of [Gleason] p. 175. See limsupval 15445 for its value. (Contributed by NM, 26-Oct-2005.) (Revised by AV, 11-Sep-2020.) |
β’ lim sup = (π₯ β V β¦ inf(ran (π β β β¦ sup(((π₯ β (π[,)+β)) β© β*), β*, < )), β*, < )) | ||
Theorem | limsupgord 15443 | 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 15444 | Closure of the superior limit. (Contributed by NM, 26-Oct-2005.) (Revised by AV, 12-Sep-2020.) |
β’ (πΉ β π β (lim supβπΉ) β β*) | ||
Theorem | limsupval 15445* | 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 15446* | Closure of the superior limit function. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-May-2016.) |
β’ πΊ = (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*), β*, < )) β β’ πΊ:ββΆβ* | ||
Theorem | limsupgval 15447* | Value of the superior limit function. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-May-2016.) |
β’ πΊ = (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*), β*, < )) β β’ (π β β β (πΊβπ) = sup(((πΉ β (π[,)+β)) β© β*), β*, < )) | ||
Theorem | limsupgle 15448* | 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 15449* | 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 15450* | 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 15451* | 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 15452* | 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 15453* | 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 15454* | 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 15455 | Extend class notation with convergence relation for limits. |
class β | ||
Syntax | crli 15456 | Extend class notation with real convergence relation for limits. |
class βπ | ||
Syntax | co1 15457 | Extend class notation with the set of all eventually bounded functions. |
class π(1) | ||
Syntax | clo1 15458 | Extend class notation with the set of all eventually upper bounded functions. |
class β€π(1) | ||
Definition | df-clim 15459* | Define the limit relation for complex number sequences. See clim 15465 for its relational expression. (Contributed by NM, 28-Aug-2005.) |
β’ β = {β¨π, π¦β© β£ (π¦ β β β§ βπ₯ β β+ βπ β β€ βπ β (β€β₯βπ)((πβπ) β β β§ (absβ((πβπ) β π¦)) < π₯))} | ||
Definition | df-rlim 15460* | Define the limit relation for partial functions on the reals. See rlim 15466 for its relational expression. (Contributed by Mario Carneiro, 16-Sep-2014.) |
β’ βπ = {β¨π, π₯β© β£ ((π β (β βpm β) β§ π₯ β β) β§ βπ¦ β β+ βπ§ β β βπ€ β dom π(π§ β€ π€ β (absβ((πβπ€) β π₯)) < π¦))} | ||
Definition | df-o1 15461* | 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 15462* | 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 15463 | The limit relation is a relation. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.) |
β’ Rel β | ||
Theorem | rlimrel 15464 | The limit relation is a relation. (Contributed by Mario Carneiro, 24-Sep-2014.) |
β’ Rel βπ | ||
Theorem | clim 15465* | 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 15466* | 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 15467* | Rewrite rlim 15466 for a mapping operation. (Contributed by Mario Carneiro, 16-Sep-2014.) (Revised by Mario Carneiro, 28-Feb-2015.) |
β’ (π β βπ§ β π΄ π΅ β β) & β’ (π β π΄ β β) & β’ (π β πΆ β β) β β’ (π β ((π§ β π΄ β¦ π΅) βπ πΆ β βπ₯ β β+ βπ¦ β β βπ§ β π΄ (π¦ β€ π§ β (absβ(π΅ β πΆ)) < π₯))) | ||
Theorem | rlim2lt 15468* | Use strictly less-than in place of less equal in the real limit predicate. (Contributed by Mario Carneiro, 18-Sep-2014.) |
β’ (π β βπ§ β π΄ π΅ β β) & β’ (π β π΄ β β) & β’ (π β πΆ β β) β β’ (π β ((π§ β π΄ β¦ π΅) βπ πΆ β βπ₯ β β+ βπ¦ β β βπ§ β π΄ (π¦ < π§ β (absβ(π΅ β πΆ)) < π₯))) | ||
Theorem | rlim3 15469* | Restrict the range of the domain bound to reals greater than some π· β β. (Contributed by Mario Carneiro, 16-Sep-2014.) |
β’ (π β βπ§ β π΄ π΅ β β) & β’ (π β π΄ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) β β’ (π β ((π§ β π΄ β¦ π΅) βπ πΆ β βπ₯ β β+ βπ¦ β (π·[,)+β)βπ§ β π΄ (π¦ β€ π§ β (absβ(π΅ β πΆ)) < π₯))) | ||
Theorem | climcl 15470 | 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 15471 | Closure of a function with a limit in the complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014.) |
β’ (πΉ βπ π΄ β πΉ β (β βpm β)) | ||
Theorem | rlimf 15472 | Closure of a function with a limit in the complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014.) |
β’ (πΉ βπ π΄ β πΉ:dom πΉβΆβ) | ||
Theorem | rlimss 15473 | Domain closure of a function with a limit in the complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014.) |
β’ (πΉ βπ π΄ β dom πΉ β β) | ||
Theorem | rlimcl 15474 | 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 15475* | Express the predicate: The limit of complex number sequence πΉ is π΄, or πΉ converges to π΄, with more general quantifier restrictions than clim 15465. (Contributed by NM, 6-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π) & β’ ((π β§ π β π) β (πΉβπ) = π΅) β β’ (π β (πΉ β π΄ β (π΄ β β β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π΅ β β β§ (absβ(π΅ β π΄)) < π₯)))) | ||
Theorem | clim2c 15476* | Express the predicate πΉ converges to π΄. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π) & β’ ((π β§ π β π) β (πΉβπ) = π΅) & β’ (π β π΄ β β) & β’ ((π β§ π β π) β π΅ β β) β β’ (π β (πΉ β π΄ β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ(π΅ β π΄)) < π₯)) | ||
Theorem | clim0 15477* | Express the predicate πΉ converges to 0. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π) & β’ ((π β§ π β π) β (πΉβπ) = π΅) β β’ (π β (πΉ β 0 β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π΅ β β β§ (absβπ΅) < π₯))) | ||
Theorem | clim0c 15478* | Express the predicate πΉ converges to 0. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π) & β’ ((π β§ π β π) β (πΉβπ) = π΅) & β’ ((π β§ π β π) β π΅ β β) β β’ (π β (πΉ β 0 β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβπ΅) < π₯)) | ||
Theorem | rlim0 15479* | Express the predicate π΅(π§) converges to 0. (Contributed by Mario Carneiro, 16-Sep-2014.) (Revised by Mario Carneiro, 28-Feb-2015.) |
β’ (π β βπ§ β π΄ π΅ β β) & β’ (π β π΄ β β) β β’ (π β ((π§ β π΄ β¦ π΅) βπ 0 β βπ₯ β β+ βπ¦ β β βπ§ β π΄ (π¦ β€ π§ β (absβπ΅) < π₯))) | ||
Theorem | rlim0lt 15480* | 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 15481* | Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΆ β β+) & β’ ((π β§ π β π) β (πΉβπ) = π΅) & β’ (π β πΉ β π΄) β β’ (π β βπ β π βπ β (β€β₯βπ)(π΅ β β β§ (absβ(π΅ β π΄)) < πΆ)) | ||
Theorem | climi2 15482* | Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΆ β β+) & β’ ((π β§ π β π) β (πΉβπ) = π΅) & β’ (π β πΉ β π΄) β β’ (π β βπ β π βπ β (β€β₯βπ)(absβ(π΅ β π΄)) < πΆ) | ||
Theorem | climi0 15483* | 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 15484* | Convergence at infinity of a function on the reals. (Contributed by Mario Carneiro, 28-Feb-2015.) |
β’ (π β βπ§ β π΄ π΅ β π) & β’ (π β π β β+) & β’ (π β (π§ β π΄ β¦ π΅) βπ πΆ) β β’ (π β βπ¦ β β βπ§ β π΄ (π¦ β€ π§ β (absβ(π΅ β πΆ)) < π )) | ||
Theorem | rlimi2 15485* | Convergence at infinity of a function on the reals. (Contributed by Mario Carneiro, 12-May-2016.) |
β’ (π β βπ§ β π΄ π΅ β π) & β’ (π β π β β+) & β’ (π β (π§ β π΄ β¦ π΅) βπ πΆ) & β’ (π β π· β β) β β’ (π β βπ¦ β (π·[,)+β)βπ§ β π΄ (π¦ β€ π§ β (absβ(π΅ β πΆ)) < π )) | ||
Theorem | ello1 15486* | Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ (πΉ β β€π(1) β (πΉ β (β βpm β) β§ βπ₯ β β βπ β β βπ¦ β (dom πΉ β© (π₯[,)+β))(πΉβπ¦) β€ π)) | ||
Theorem | ello12 15487* | Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β (πΉ β β€π(1) β βπ₯ β β βπ β β βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ π))) | ||
Theorem | ello12r 15488* | Sufficient condition for elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ (πΆ β β β§ π β β) β§ βπ₯ β π΄ (πΆ β€ π₯ β (πΉβπ₯) β€ π)) β πΉ β β€π(1)) | ||
Theorem | lo1f 15489 | An eventually upper bounded function is a function. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ (πΉ β β€π(1) β πΉ:dom πΉβΆβ) | ||
Theorem | lo1dm 15490 | An eventually upper bounded function's domain is a subset of the reals. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ (πΉ β β€π(1) β dom πΉ β β) | ||
Theorem | lo1bdd 15491* | The defining property of an eventually upper bounded function. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ ((πΉ β β€π(1) β§ πΉ:π΄βΆβ) β βπ₯ β β βπ β β βπ¦ β π΄ (π₯ β€ π¦ β (πΉβπ¦) β€ π)) | ||
Theorem | ello1mpt 15492* | Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ (π β π΄ β β) & β’ ((π β§ π₯ β π΄) β π΅ β β) β β’ (π β ((π₯ β π΄ β¦ π΅) β β€π(1) β βπ¦ β β βπ β β βπ₯ β π΄ (π¦ β€ π₯ β π΅ β€ π))) | ||
Theorem | ello1mpt2 15493* | Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ (π β π΄ β β) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β πΆ β β) β β’ (π β ((π₯ β π΄ β¦ π΅) β β€π(1) β βπ¦ β (πΆ[,)+β)βπ β β βπ₯ β π΄ (π¦ β€ π₯ β π΅ β€ π))) | ||
Theorem | ello1d 15494* | Sufficient condition for elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ (π β π΄ β β) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π β β) & β’ ((π β§ (π₯ β π΄ β§ πΆ β€ π₯)) β π΅ β€ π) β β’ (π β (π₯ β π΄ β¦ π΅) β β€π(1)) | ||
Theorem | lo1bdd2 15495* | 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 15496* | Refine o1bdd2 15512 to give a strictly positive upper bound. (Contributed by Mario Carneiro, 25-May-2016.) |
β’ (π β π΄ β β) & β’ (π β πΆ β β) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β (π₯ β π΄ β¦ π΅) β β€π(1)) & β’ ((π β§ (π¦ β β β§ πΆ β€ π¦)) β π β β) & β’ (((π β§ π₯ β π΄) β§ ((π¦ β β β§ πΆ β€ π¦) β§ π₯ < π¦)) β π΅ β€ π) β β’ (π β βπ β β+ βπ₯ β π΄ π΅ β€ π) | ||
Theorem | elo1 15497* | Elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ (πΉ β π(1) β (πΉ β (β βpm β) β§ βπ₯ β β βπ β β βπ¦ β (dom πΉ β© (π₯[,)+β))(absβ(πΉβπ¦)) β€ π)) | ||
Theorem | elo12 15498* | Elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β (πΉ β π(1) β βπ₯ β β βπ β β βπ¦ β π΄ (π₯ β€ π¦ β (absβ(πΉβπ¦)) β€ π))) | ||
Theorem | elo12r 15499* | Sufficient condition for elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ (πΆ β β β§ π β β) β§ βπ₯ β π΄ (πΆ β€ π₯ β (absβ(πΉβπ₯)) β€ π)) β πΉ β π(1)) | ||
Theorem | o1f 15500 | An eventually bounded function is a function. (Contributed by Mario Carneiro, 15-Sep-2014.) |
β’ (πΉ β π(1) β πΉ:dom πΉβΆβ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |