![]() |
Metamath
Proof Explorer Theorem List (p. 446 of 480) | < 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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cvgcau 44501* | A convergent function is Cauchy. (Contributed by Glauco Siliprandi, 15-Feb-2025.) |
β’ β²ππΉ & β’ β²ππΉ & β’ (π β π β π) & β’ (π β πΉ β π) & β’ π = (β€β₯βπ) & β’ (π β πΉ β dom β ) & β’ (π β π β β+) β β’ (π β βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π)) | ||
Theorem | cvgcaule 44502* | A convergent function is Cauchy. (Contributed by Glauco Siliprandi, 15-Feb-2025.) |
β’ β²ππΉ & β’ β²ππΉ & β’ (π β π β π) & β’ (π β πΉ β π) & β’ π = (β€β₯βπ) & β’ (π β πΉ β dom β ) & β’ (π β π β β+) β β’ (π β βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) β€ π)) | ||
Theorem | rexanuz2nf 44503* | A simple counterexample related to theorem rexanuz2 15301, demonstrating the necessity of its disjoint variable constraints. Here, π appears free in π, showing that without these constraints, rexanuz2 15301 and similar theorems would not hold (see rexanre 15298 and rexanuz 15297). (Contributed by Glauco Siliprandi, 15-Feb-2025.) |
β’ π = β0 & β’ (π β (π = 0 β§ π β€ π)) & β’ (π β 0 < π) β β’ Β¬ (βπ β π βπ β (β€β₯βπ)(π β§ π) β (βπ β π βπ β (β€β₯βπ)π β§ βπ β π βπ β (β€β₯βπ)π)) | ||
Theorem | gtnelioc 44504 | A real number larger than the upper bound of a left-open right-closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β) & β’ (π β πΆ β β*) & β’ (π β π΅ < πΆ) β β’ (π β Β¬ πΆ β (π΄(,]π΅)) | ||
Theorem | ioossioc 44505 | An open interval is a subset of its right closure. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄(,)π΅) β (π΄(,]π΅) | ||
Theorem | ioondisj2 44506 | A condition for two open intervals not to be disjoint. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((((π΄ β β* β§ π΅ β β* β§ π΄ < π΅) β§ (πΆ β β* β§ π· β β* β§ πΆ < π·)) β§ (π΄ < π· β§ π· β€ π΅)) β ((π΄(,)π΅) β© (πΆ(,)π·)) β β ) | ||
Theorem | ioondisj1 44507 | A condition for two open intervals not to be disjoint. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((((π΄ β β* β§ π΅ β β* β§ π΄ < π΅) β§ (πΆ β β* β§ π· β β* β§ πΆ < π·)) β§ (π΄ β€ πΆ β§ πΆ < π΅)) β ((π΄(,)π΅) β© (πΆ(,)π·)) β β ) | ||
Theorem | ioogtlb 44508 | An element of a closed interval is greater than its lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β (π΄(,)π΅)) β π΄ < πΆ) | ||
Theorem | evthiccabs 44509* | Extreme Value Theorem on y closed interval, for the absolute value of y continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β πΉ β ((π΄[,]π΅)βcnββ)) β β’ (π β (βπ₯ β (π΄[,]π΅)βπ¦ β (π΄[,]π΅)(absβ(πΉβπ¦)) β€ (absβ(πΉβπ₯)) β§ βπ§ β (π΄[,]π΅)βπ€ β (π΄[,]π΅)(absβ(πΉβπ§)) β€ (absβ(πΉβπ€)))) | ||
Theorem | ltnelicc 44510 | A real number smaller than the lower bound of a closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β*) & β’ (π β πΆ β β*) & β’ (π β πΆ < π΄) β β’ (π β Β¬ πΆ β (π΄[,]π΅)) | ||
Theorem | eliood 44511 | Membership in an open real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β β) & β’ (π β π΄ < πΆ) & β’ (π β πΆ < π΅) β β’ (π β πΆ β (π΄(,)π΅)) | ||
Theorem | iooabslt 44512 | An upper bound for the distance from the center of an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β ((π΄ β π΅)(,)(π΄ + π΅))) β β’ (π β (absβ(π΄ β πΆ)) < π΅) | ||
Theorem | gtnelicc 44513 | A real number greater than the upper bound of a closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β) & β’ (π β πΆ β β*) & β’ (π β π΅ < πΆ) β β’ (π β Β¬ πΆ β (π΄[,]π΅)) | ||
Theorem | iooinlbub 44514 | An open interval has empty intersection with its bounds. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄(,)π΅) β© {π΄, π΅}) = β | ||
Theorem | iocgtlb 44515 | An element of a left-open right-closed interval is larger than its lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β (π΄(,]π΅)) β π΄ < πΆ) | ||
Theorem | iocleub 44516 | An element of a left-open right-closed interval is smaller than or equal to its upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β (π΄(,]π΅)) β πΆ β€ π΅) | ||
Theorem | eliccd 44517 | Membership in a closed real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΄ β€ πΆ) & β’ (π β πΆ β€ π΅) β β’ (π β πΆ β (π΄[,]π΅)) | ||
Theorem | eliccre 44518 | A member of a closed interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β (π΄[,]π΅)) β πΆ β β) | ||
Theorem | eliooshift 44519 | Element of an open interval shifted by a displacement. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) β β’ (π β (π΄ β (π΅(,)πΆ) β (π΄ + π·) β ((π΅ + π·)(,)(πΆ + π·)))) | ||
Theorem | eliocd 44520 | Membership in a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β β*) & β’ (π β π΄ < πΆ) & β’ (π β πΆ β€ π΅) β β’ (π β πΆ β (π΄(,]π΅)) | ||
Theorem | icoltub 44521 | An element of a left-closed right-open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β (π΄[,)π΅)) β πΆ < π΅) | ||
Theorem | eliocre 44522 | A member of a left-open right-closed interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΅ β β β§ πΆ β (π΄(,]π΅)) β πΆ β β) | ||
Theorem | iooltub 44523 | An element of an open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β (π΄(,)π΅)) β πΆ < π΅) | ||
Theorem | ioontr 44524 | The interior of an interval in the standard topology on β is the open interval itself. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((intβ(topGenβran (,)))β(π΄(,)π΅)) = (π΄(,)π΅) | ||
Theorem | snunioo1 44525 | The closure of one end of an open real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β* β§ π΅ β β* β§ π΄ < π΅) β ((π΄(,)π΅) βͺ {π΄}) = (π΄[,)π΅)) | ||
Theorem | lbioc 44526 | A left-open right-closed interval does not contain its left endpoint. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ Β¬ π΄ β (π΄(,]π΅) | ||
Theorem | ioomidp 44527 | The midpoint is an element of the open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ < π΅) β ((π΄ + π΅) / 2) β (π΄(,)π΅)) | ||
Theorem | iccdifioo 44528 | If the open inverval is removed from the closed interval, only the bounds are left. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β* β§ π΅ β β* β§ π΄ β€ π΅) β ((π΄[,]π΅) β (π΄(,)π΅)) = {π΄, π΅}) | ||
Theorem | iccdifprioo 44529 | An open interval is the closed interval without the bounds. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β* β§ π΅ β β*) β ((π΄[,]π΅) β {π΄, π΅}) = (π΄(,)π΅)) | ||
Theorem | ioossioobi 44530 | Biconditional form of ioossioo 13423. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β β*) & β’ (π β π· β β*) & β’ (π β πΆ < π·) β β’ (π β ((πΆ(,)π·) β (π΄(,)π΅) β (π΄ β€ πΆ β§ π· β€ π΅))) | ||
Theorem | iccshift 44531* | A closed interval shifted by a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β) β β’ (π β ((π΄ + π)[,](π΅ + π)) = {π€ β β β£ βπ§ β (π΄[,]π΅)π€ = (π§ + π)}) | ||
Theorem | iccsuble 44532 | An upper bound to the distance of two elements in a closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β (π΄[,]π΅)) & β’ (π β π· β (π΄[,]π΅)) β β’ (π β (πΆ β π·) β€ (π΅ β π΄)) | ||
Theorem | iocopn 44533 | A left-open right-closed interval is an open set of the standard topology restricted to an interval that contains the original interval and has the same upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β πΆ β β*) & β’ (π β π΅ β β) & β’ πΎ = (topGenβran (,)) & β’ π½ = (πΎ βΎt (π΄(,]π΅)) & β’ (π β π΄ β€ πΆ) & β’ (π β π΅ β β) β β’ (π β (πΆ(,]π΅) β π½) | ||
Theorem | eliccelioc 44534 | Membership in a closed interval and in a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β*) β β’ (π β (πΆ β (π΄(,]π΅) β (πΆ β (π΄[,]π΅) β§ πΆ β π΄))) | ||
Theorem | iooshift 44535* | An open interval shifted by a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β) β β’ (π β ((π΄ + π)(,)(π΅ + π)) = {π€ β β β£ βπ§ β (π΄(,)π΅)π€ = (π§ + π)}) | ||
Theorem | iccintsng 44536 | Intersection of two adiacent closed intervals is a singleton. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ (π΄ β€ π΅ β§ π΅ β€ πΆ)) β ((π΄[,]π΅) β© (π΅[,]πΆ)) = {π΅}) | ||
Theorem | icoiccdif 44537 | Left-closed right-open interval gotten by a closed iterval taking away the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄[,)π΅) = ((π΄[,]π΅) β {π΅})) | ||
Theorem | icoopn 44538 | A left-closed right-open interval is an open set of the standard topology restricted to an interval that contains the original interval and has the same lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β πΆ β β*) & β’ (π β π΅ β β*) & β’ πΎ = (topGenβran (,)) & β’ π½ = (πΎ βΎt (π΄[,)π΅)) & β’ (π β πΆ β€ π΅) β β’ (π β (π΄[,)πΆ) β π½) | ||
Theorem | icoub 44539 | A left-closed, right-open interval does not contain its upper bound. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π΄ β β* β Β¬ π΅ β (π΄[,)π΅)) | ||
Theorem | eliccxrd 44540 | Membership in a closed real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β β*) & β’ (π β π΄ β€ πΆ) & β’ (π β πΆ β€ π΅) β β’ (π β πΆ β (π΄[,]π΅)) | ||
Theorem | pnfel0pnf 44541 | +β is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ +β β (0[,]+β) | ||
Theorem | eliccnelico 44542 | An element of a closed interval that is not a member of the left-closed right-open interval, must be the upper bound. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄[,]π΅)) & β’ (π β Β¬ πΆ β (π΄[,)π΅)) β β’ (π β πΆ = π΅) | ||
Theorem | eliccelicod 44543 | A member of a closed interval that is not the upper bound, is a member of the left-closed, right-open interval. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄[,]π΅)) & β’ (π β πΆ β π΅) β β’ (π β πΆ β (π΄[,)π΅)) | ||
Theorem | ge0xrre 44544 | A nonnegative extended real that is not +β is a real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ ((π΄ β (0[,]+β) β§ π΄ β +β) β π΄ β β) | ||
Theorem | ge0lere 44545 | A nonnegative extended Real number smaller than or equal to a Real number, is a Real number. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β (0[,]+β)) & β’ (π β π΅ β€ π΄) β β’ (π β π΅ β β) | ||
Theorem | elicores 44546* | Membership in a left-closed, right-open interval with real bounds. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π΄ β ran ([,) βΎ (β Γ β)) β βπ₯ β β βπ¦ β β π΄ = (π₯[,)π¦)) | ||
Theorem | inficc 44547 | The infimum of a nonempty set, included in a closed interval, is a member of the interval. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π β (π΄[,]π΅)) & β’ (π β π β β ) β β’ (π β inf(π, β*, < ) β (π΄[,]π΅)) | ||
Theorem | qinioo 44548 | The rational numbers are dense in β. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) β β’ (π β ((β β© (π΄(,)π΅)) = β β π΅ β€ π΄)) | ||
Theorem | lenelioc 44549 | A real number smaller than or equal to the lower bound of a left-open right-closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β β*) & β’ (π β πΆ β€ π΄) β β’ (π β Β¬ πΆ β (π΄(,]π΅)) | ||
Theorem | ioonct 44550 | A nonempty open interval is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π΄ < π΅) & β’ πΆ = (π΄(,)π΅) β β’ (π β Β¬ πΆ βΌ Ο) | ||
Theorem | xrgtnelicc 44551 | A real number greater than the upper bound of a closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β β*) & β’ (π β π΅ < πΆ) β β’ (π β Β¬ πΆ β (π΄[,]π΅)) | ||
Theorem | iccdificc 44552 | The difference of two closed intervals with the same lower bound. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β β*) & β’ (π β π΄ β€ π΅) β β’ (π β ((π΄[,]πΆ) β (π΄[,]π΅)) = (π΅(,]πΆ)) | ||
Theorem | iocnct 44553 | A nonempty left-open, right-closed interval is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π΄ < π΅) & β’ πΆ = (π΄(,]π΅) β β’ (π β Β¬ πΆ βΌ Ο) | ||
Theorem | iccnct 44554 | A closed interval, with more than one element is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π΄ < π΅) & β’ πΆ = (π΄[,]π΅) β β’ (π β Β¬ πΆ βΌ Ο) | ||
Theorem | iooiinicc 44555* | A closed interval expressed as the indexed intersection of open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β β© π β β ((π΄ β (1 / π))(,)(π΅ + (1 / π))) = (π΄[,]π΅)) | ||
Theorem | iccgelbd 44556 | An element of a closed interval is more than or equal to its lower bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄[,]π΅)) β β’ (π β π΄ β€ πΆ) | ||
Theorem | iooltubd 44557 | An element of an open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄(,)π΅)) β β’ (π β πΆ < π΅) | ||
Theorem | icoltubd 44558 | An element of a left-closed right-open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄[,)π΅)) β β’ (π β πΆ < π΅) | ||
Theorem | qelioo 44559* | The rational numbers are dense in β*: any two extended real numbers have a rational between them. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π΄ < π΅) β β’ (π β βπ₯ β β π₯ β (π΄(,)π΅)) | ||
Theorem | tgqioo2 44560* | Every open set of reals is the (countable) union of open interval with rational bounds. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π½ = (topGenβran (,)) & β’ (π β π΄ β π½) β β’ (π β βπ(π β ((,) β (β Γ β)) β§ π΄ = βͺ π)) | ||
Theorem | iccleubd 44561 | An element of a closed interval is less than or equal to its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄[,]π΅)) β β’ (π β πΆ β€ π΅) | ||
Theorem | elioored 44562 | A member of an open interval of reals is a real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β (π΅(,)πΆ)) β β’ (π β π΄ β β) | ||
Theorem | ioogtlbd 44563 | An element of a closed interval is greater than its lower bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄(,)π΅)) β β’ (π β π΄ < πΆ) | ||
Theorem | ioofun 44564 | (,) is a function. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ Fun (,) | ||
Theorem | icomnfinre 44565 | A left-closed, right-open, interval of extended reals, intersected with the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) β β’ (π β ((-β[,)π΄) β© β) = (-β(,)π΄)) | ||
Theorem | sqrlearg 44566 | The square compared with its argument. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) β β’ (π β ((π΄β2) β€ π΄ β π΄ β (0[,]1))) | ||
Theorem | ressiocsup 44567 | If the supremum belongs to a set of reals, the set is a subset of the unbounded below, right-closed interval, with upper bound equal to the supremum. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) & β’ π = sup(π΄, β*, < ) & β’ (π β π β π΄) & β’ πΌ = (-β(,]π) β β’ (π β π΄ β πΌ) | ||
Theorem | ressioosup 44568 | If the supremum does not belong to a set of reals, the set is a subset of the unbounded below, right-open interval, with upper bound equal to the supremum. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) & β’ π = sup(π΄, β*, < ) & β’ (π β Β¬ π β π΄) & β’ πΌ = (-β(,)π) β β’ (π β π΄ β πΌ) | ||
Theorem | iooiinioc 44569* | A left-open, right-closed interval expressed as the indexed intersection of open intervals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β) β β’ (π β β© π β β (π΄(,)(π΅ + (1 / π))) = (π΄(,]π΅)) | ||
Theorem | ressiooinf 44570 | If the infimum does not belong to a set of reals, the set is a subset of the unbounded above, left-open interval, with lower bound equal to the infimum. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) & β’ π = inf(π΄, β*, < ) & β’ (π β Β¬ π β π΄) & β’ πΌ = (π(,)+β) β β’ (π β π΄ β πΌ) | ||
Theorem | icogelbd 44571 | An element of a left-closed right-open interval is greater than or equal to its lower bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄[,)π΅)) β β’ (π β π΄ β€ πΆ) | ||
Theorem | iocleubd 44572 | An element of a left-open right-closed interval is smaller than or equal to its upper bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄(,]π΅)) β β’ (π β πΆ β€ π΅) | ||
Theorem | uzinico 44573 | An upper interval of integers is the intersection of the integers with an upper part of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) β β’ (π β π = (β€ β© (π[,)+β))) | ||
Theorem | preimaiocmnf 44574* | Preimage of a right-closed interval, unbounded below. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β π΅ β β*) β β’ (π β (β‘πΉ β (-β(,]π΅)) = {π₯ β π΄ β£ (πΉβπ₯) β€ π΅}) | ||
Theorem | uzinico2 44575 | An upper interval of integers is the intersection of a larger upper interval of integers with an upper part of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β (β€β₯βπ)) β β’ (π β (β€β₯βπ) = ((β€β₯βπ) β© (π[,)+β))) | ||
Theorem | uzinico3 44576 | An upper interval of integers doesn't change when it's intersected with a left-closed, unbounded above interval, with the same lower bound. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) β β’ (π β π = (π β© (π[,)+β))) | ||
Theorem | icossico2 44577 | Condition for a closed-below, open-above interval to be a subset of a closed-below, open-above interval. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΅ β β*) & β’ (π β πΆ β β*) & β’ (π β π΅ β€ π΄) β β’ (π β (π΄[,)πΆ) β (π΅[,)πΆ)) | ||
Theorem | dmico 44578 | The domain of the closed-below, open-above interval function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ dom [,) = (β* Γ β*) | ||
Theorem | ndmico 44579 | The closed-below, open-above interval function's value is empty outside of its domain. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (Β¬ (π΄ β β* β§ π΅ β β*) β (π΄[,)π΅) = β ) | ||
Theorem | uzubioo 44580* | The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β β) β β’ (π β βπ β (π(,)+β)π β π) | ||
Theorem | uzubico 44581* | The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β β) β β’ (π β βπ β (π[,)+β)π β π) | ||
Theorem | uzubioo2 44582* | The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) β β’ (π β βπ₯ β β βπ β (π₯(,)+β)π β π) | ||
Theorem | uzubico2 44583* | The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) β β’ (π β βπ₯ β β βπ β (π₯[,)+β)π β π) | ||
Theorem | iocgtlbd 44584 | An element of a left-open right-closed interval is larger than its lower bound. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄(,]π΅)) β β’ (π β π΄ < πΆ) | ||
Theorem | xrtgioo2 44585 | The topology on the extended reals coincides with the standard topology on the reals, when restricted to β. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (topGenβran (,)) = ((ordTopβ β€ ) βΎt β) | ||
Theorem | tgioo4 44586 | The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (topGenβran (,)) = ((TopOpenββfld) βΎt β) | ||
Theorem | fsummulc1f 44587* | Closure of a finite sum of complex numbers π΄(π). A version of fsummulc1 15736 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ (π β πΆ β β) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β (Ξ£π β π΄ π΅ Β· πΆ) = Ξ£π β π΄ (π΅ Β· πΆ)) | ||
Theorem | fsumnncl 44588* | Closure of a nonempty, finite sum of positive integers. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΄ β β ) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ β β) | ||
Theorem | fsumge0cl 44589* | The finite sum of nonnegative reals is a nonnegative real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β (0[,)+β)) β β’ (π β Ξ£π β π΄ π΅ β (0[,)+β)) | ||
Theorem | fsumf1of 44590* | Re-index a finite sum using a bijection. Same as fsumf1o 15674, but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²ππ & β’ β²ππ & β’ (π = πΊ β π΅ = π·) & β’ (π β πΆ β Fin) & β’ (π β πΉ:πΆβ1-1-ontoβπ΄) & β’ ((π β§ π β πΆ) β (πΉβπ) = πΊ) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ = Ξ£π β πΆ π·) | ||
Theorem | fsumiunss 44591* | Sum over a disjoint indexed union, intersected with a finite set π·. Similar to fsumiun 15772, but here π΄ and π΅ need not be finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β Disj π₯ β π΄ π΅) & β’ ((π β§ π₯ β π΄ β§ π β π΅) β πΆ β β) & β’ (π β π· β Fin) β β’ (π β Ξ£π β βͺ π₯ β π΄ (π΅ β© π·)πΆ = Ξ£π₯ β {π₯ β π΄ β£ (π΅ β© π·) β β }Ξ£π β (π΅ β© π·)πΆ) | ||
Theorem | fsumreclf 44592* | Closure of a finite sum of reals. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ β β) | ||
Theorem | fsumlessf 44593* | A shorter sum of nonnegative terms is smaller than a longer one. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β 0 β€ π΅) & β’ (π β πΆ β π΄) β β’ (π β Ξ£π β πΆ π΅ β€ Ξ£π β π΄ π΅) | ||
Theorem | fsumsupp0 44594* | Finite sum of function values, for a function of finite support. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π΄ β Fin) & β’ (π β πΉ:π΄βΆβ) β β’ (π β Ξ£π β (πΉ supp 0)(πΉβπ) = Ξ£π β π΄ (πΉβπ)) | ||
Theorem | fsumsermpt 44595* | A finite sum expressed in terms of a partial sum of an infinite series. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ ((π β§ π β π) β π΄ β β) & β’ πΉ = (π β π β¦ Ξ£π β (π...π)π΄) & β’ πΊ = seqπ( + , (π β π β¦ π΄)) β β’ (π β πΉ = πΊ) | ||
Theorem | fmul01 44596* | Multiplying a finite number of values in [ 0 , 1 ] , gives the final product itself a number in [ 0 , 1 ]. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππ΅ & β’ β²ππ & β’ π΄ = seqπΏ( Β· , π΅) & β’ (π β πΏ β β€) & β’ (π β π β (β€β₯βπΏ)) & β’ (π β πΎ β (πΏ...π)) & β’ ((π β§ π β (πΏ...π)) β (π΅βπ) β β) & β’ ((π β§ π β (πΏ...π)) β 0 β€ (π΅βπ)) & β’ ((π β§ π β (πΏ...π)) β (π΅βπ) β€ 1) β β’ (π β (0 β€ (π΄βπΎ) β§ (π΄βπΎ) β€ 1)) | ||
Theorem | fmulcl 44597* | If ' Y ' is closed under the multiplication of two functions, then Y is closed under the multiplication ( ' X ' ) of a finite number of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ π = (π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) & β’ π = (seq1(π, π)βπ) & β’ (π β π β (1...π)) & β’ (π β π:(1...π)βΆπ) & β’ ((π β§ π β π β§ π β π) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π) & β’ (π β π β V) β β’ (π β π β π) | ||
Theorem | fmuldfeqlem1 44598* | induction step for the proof of fmuldfeq 44599. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππ & β’ β²ππ & β’ β²π‘π & β’ π = (π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) & β’ πΉ = (π‘ β π β¦ (π β (1...π) β¦ ((πβπ)βπ‘))) & β’ (π β π β V) & β’ (π β π:(1...π)βΆπ) & β’ ((π β§ π β π β§ π β π) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π) & β’ (π β π β (1...π)) & β’ (π β (π + 1) β (1...π)) & β’ (π β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) & β’ ((π β§ π β π) β π:πβΆβ) β β’ ((π β§ π‘ β π) β ((seq1(π, π)β(π + 1))βπ‘) = (seq1( Β· , (πΉβπ‘))β(π + 1))) | ||
Theorem | fmuldfeq 44599* | X and Z are two equivalent definitions of the finite product of real functions. Y is a set of real functions from a common domain T, Y is closed under function multiplication and U is a finite sequence of functions in Y. M is the number of functions multiplied together. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππ & β’ β²π‘π & β’ π = (π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) & β’ π = (seq1(π, π)βπ) & β’ πΉ = (π‘ β π β¦ (π β (1...π) β¦ ((πβπ)βπ‘))) & β’ π = (π‘ β π β¦ (seq1( Β· , (πΉβπ‘))βπ)) & β’ (π β π β V) & β’ (π β π β β) & β’ (π β π:(1...π)βΆπ) & β’ ((π β§ π β π) β π:πβΆβ) & β’ ((π β§ π β π β§ π β π) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π) β β’ ((π β§ π‘ β π) β (πβπ‘) = (πβπ‘)) | ||
Theorem | fmul01lt1lem1 44600* | Given a finite multiplication of values betweeen 0 and 1, a value larger than its first element is larger the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππ΅ & β’ β²ππ & β’ π΄ = seqπΏ( Β· , π΅) & β’ (π β πΏ β β€) & β’ (π β π β (β€β₯βπΏ)) & β’ ((π β§ π β (πΏ...π)) β (π΅βπ) β β) & β’ ((π β§ π β (πΏ...π)) β 0 β€ (π΅βπ)) & β’ ((π β§ π β (πΏ...π)) β (π΅βπ) β€ 1) & β’ (π β πΈ β β+) & β’ (π β (π΅βπΏ) < πΈ) β β’ (π β (π΄βπ) < πΈ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |