Home | Metamath
Proof Explorer Theorem List (p. 435 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-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nleltd 43401 | 'Not less than or equal to' implies 'grater than'. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β Β¬ π΅ β€ π΄) β β’ (π β π΄ < π΅) | ||
Theorem | zxrd 43402 | An integer is an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΄ β β€) β β’ (π β π΄ β β*) | ||
Theorem | infxrgelbrnmpt 43403* | The infimum of an indexed set of extended reals is greater than or equal to a lower bound. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²π₯π & β’ ((π β§ π₯ β π΄) β π΅ β β*) & β’ (π β πΆ β β*) β β’ (π β (πΆ β€ inf(ran (π₯ β π΄ β¦ π΅), β*, < ) β βπ₯ β π΄ πΆ β€ π΅)) | ||
Theorem | rphalfltd 43404 | Half of a positive real is less than the original number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΄ β β+) β β’ (π β (π΄ / 2) < π΄) | ||
Theorem | uzssz2 43405 | An upper set of integers is a subset of all integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ π = (β€β₯βπ) β β’ π β β€ | ||
Theorem | leneg3d 43406 | Negative of one side of 'less than or equal to'. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (-π΄ β€ π΅ β -π΅ β€ π΄)) | ||
Theorem | max2d 43407 | A number is less than or equal to the maximum of it and another. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β π΅ β€ if(π΄ β€ π΅, π΅, π΄)) | ||
Theorem | uzn0bi 43408 | The upper integers function needs to be applied to an integer, in order to return a nonempty set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ ((β€β₯βπ) β β β π β β€) | ||
Theorem | xnegrecl2 43409 | If the extended real negative is real, then the number itself is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ ((π΄ β β* β§ -ππ΄ β β) β π΄ β β) | ||
Theorem | nfxneg 43410 | Bound-variable hypothesis builder for the negative of an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²π₯π΄ β β’ β²π₯-ππ΄ | ||
Theorem | uzxrd 43411 | An upper integer is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ π = (β€β₯βπ) & β’ (π β π΄ β π) β β’ (π β π΄ β β*) | ||
Theorem | infxrpnf2 43412 | Removing plus infinity from a set does not affect its infimum. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π΄ β β* β inf((π΄ β {+β}), β*, < ) = inf(π΄, β*, < )) | ||
Theorem | supminfxr 43413* | The extended real suprema of a set of reals is the extended real negative of the extended real infima of that set's image under negation. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΄ β β) β β’ (π β sup(π΄, β*, < ) = -πinf({π₯ β β β£ -π₯ β π΄}, β*, < )) | ||
Theorem | infrpgernmpt 43414* | The infimum of a nonempty, bounded below, indexed subset of extended reals can be approximated from above by an element of the set. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²π₯π & β’ (π β π΄ β β ) & β’ ((π β§ π₯ β π΄) β π΅ β β*) & β’ (π β βπ¦ β β βπ₯ β π΄ π¦ β€ π΅) & β’ (π β πΆ β β+) β β’ (π β βπ₯ β π΄ π΅ β€ (inf(ran (π₯ β π΄ β¦ π΅), β*, < ) +π πΆ)) | ||
Theorem | xnegre 43415 | An extended real is real if and only if its extended negative is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π΄ β β* β (π΄ β β β -ππ΄ β β)) | ||
Theorem | xnegrecl2d 43416 | If the extended real negative is real, then the number itself is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΄ β β*) & β’ (π β -ππ΄ β β) β β’ (π β π΄ β β) | ||
Theorem | uzxr 43417 | An upper integer is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π΄ β (β€β₯βπ) β π΄ β β*) | ||
Theorem | supminfxr2 43418* | The extended real suprema of a set of extended reals is the extended real negative of the extended real infima of that set's image under extended real negation. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΄ β β*) β β’ (π β sup(π΄, β*, < ) = -πinf({π₯ β β* β£ -ππ₯ β π΄}, β*, < )) | ||
Theorem | xnegred 43419 | An extended real is real if and only if its extended negative is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΄ β β*) β β’ (π β (π΄ β β β -ππ΄ β β)) | ||
Theorem | supminfxrrnmpt 43420* | The indexed supremum of a set of reals is the negation of the indexed infimum of that set's image under negation. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ β²π₯π & β’ ((π β§ π₯ β π΄) β π΅ β β*) β β’ (π β sup(ran (π₯ β π΄ β¦ π΅), β*, < ) = -πinf(ran (π₯ β π΄ β¦ -ππ΅), β*, < )) | ||
Theorem | min1d 43421 | The minimum of two numbers is less than or equal to the first. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β if(π΄ β€ π΅, π΄, π΅) β€ π΄) | ||
Theorem | min2d 43422 | The minimum of two numbers is less than or equal to the second. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β if(π΄ β€ π΅, π΄, π΅) β€ π΅) | ||
Theorem | pnfged 43423 | Plus infinity is an upper bound for extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π΄ β β*) β β’ (π β π΄ β€ +β) | ||
Theorem | xrnpnfmnf 43424 | An extended real that is neither real nor plus infinity, is minus infinity. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π΄ β β*) & β’ (π β Β¬ π΄ β β) & β’ (π β π΄ β +β) β β’ (π β π΄ = -β) | ||
Theorem | uzsscn 43425 | An upper set of integers is a subset of the complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (β€β₯βπ) β β | ||
Theorem | absimnre 43426 | The absolute value of the imaginary part of a non-real, complex number, is strictly positive. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π΄ β β) & β’ (π β Β¬ π΄ β β) β β’ (π β (absβ(ββπ΄)) β β+) | ||
Theorem | uzsscn2 43427 | An upper set of integers is a subset of the complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ π = (β€β₯βπ) β β’ π β β | ||
Theorem | xrtgcntopre 43428 | The standard topologies on the extended reals and on the complex numbers, coincide when restricted to the reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ ((ordTopβ β€ ) βΎt β) = ((TopOpenββfld) βΎt β) | ||
Theorem | absimlere 43429 | The absolute value of the imaginary part of a complex number is a lower bound of the distance to any real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (absβ(ββπ΄)) β€ (absβ(π΅ β π΄))) | ||
Theorem | rpssxr 43430 | The positive reals are a subset of the extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ β+ β β* | ||
Theorem | monoordxrv 43431* | Ordering relation for a monotonic sequence, increasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β (πΉβπ) β β*) & β’ ((π β§ π β (π...(π β 1))) β (πΉβπ) β€ (πΉβ(π + 1))) β β’ (π β (πΉβπ) β€ (πΉβπ)) | ||
Theorem | monoordxr 43432* | Ordering relation for a monotonic sequence, increasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022.) |
β’ β²ππ & β’ β²ππΉ & β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β (πΉβπ) β β*) & β’ ((π β§ π β (π...(π β 1))) β (πΉβπ) β€ (πΉβ(π + 1))) β β’ (π β (πΉβπ) β€ (πΉβπ)) | ||
Theorem | monoord2xrv 43433* | Ordering relation for a monotonic sequence, decreasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β (πΉβπ) β β*) & β’ ((π β§ π β (π...(π β 1))) β (πΉβ(π + 1)) β€ (πΉβπ)) β β’ (π β (πΉβπ) β€ (πΉβπ)) | ||
Theorem | monoord2xr 43434* | Ordering relation for a monotonic sequence, decreasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022.) |
β’ β²ππ & β’ β²ππΉ & β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β (πΉβπ) β β*) & β’ ((π β§ π β (π...(π β 1))) β (πΉβ(π + 1)) β€ (πΉβπ)) β β’ (π β (πΉβπ) β€ (πΉβπ)) | ||
Theorem | xrpnf 43435* | An extended real is plus infinity iff it's larger than all real numbers. (Contributed by Glauco Siliprandi, 13-Feb-2022.) |
β’ (π΄ β β* β (π΄ = +β β βπ₯ β β π₯ β€ π΄)) | ||
Theorem | xlenegcon1 43436 | Extended real version of lenegcon1 11593. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ ((π΄ β β* β§ π΅ β β*) β (-ππ΄ β€ π΅ β -ππ΅ β€ π΄)) | ||
Theorem | xlenegcon2 43437 | Extended real version of lenegcon2 11594. (Contributed by Glauco Siliprandi, 23-Apr-2023.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄ β€ -ππ΅ β π΅ β€ -ππ΄)) | ||
Theorem | pimxrneun 43438 | The preimage of a set of extended reals that does not contain a value πΆ is the union of the preimage of the elements smaller than πΆ and the preimage of the subset of elements larger than πΆ. (Contributed by Glauco Siliprandi, 21-Dec-2024.) |
β’ β²π₯π & β’ ((π β§ π₯ β π΄) β π΅ β β*) & β’ ((π β§ π₯ β π΄) β πΆ β β*) β β’ (π β {π₯ β π΄ β£ π΅ β πΆ} = ({π₯ β π΄ β£ π΅ < πΆ} βͺ {π₯ β π΄ β£ πΆ < π΅})) | ||
Theorem | gtnelioc 43439 | 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 43440 | An open interval is a subset of its right closure. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄(,)π΅) β (π΄(,]π΅) | ||
Theorem | ioondisj2 43441 | A condition for two open intervals not to be disjoint. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((((π΄ β β* β§ π΅ β β* β§ π΄ < π΅) β§ (πΆ β β* β§ π· β β* β§ πΆ < π·)) β§ (π΄ < π· β§ π· β€ π΅)) β ((π΄(,)π΅) β© (πΆ(,)π·)) β β ) | ||
Theorem | ioondisj1 43442 | A condition for two open intervals not to be disjoint. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((((π΄ β β* β§ π΅ β β* β§ π΄ < π΅) β§ (πΆ β β* β§ π· β β* β§ πΆ < π·)) β§ (π΄ β€ πΆ β§ πΆ < π΅)) β ((π΄(,)π΅) β© (πΆ(,)π·)) β β ) | ||
Theorem | ioogtlb 43443 | An element of a closed interval is greater than its lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β (π΄(,)π΅)) β π΄ < πΆ) | ||
Theorem | evthiccabs 43444* | 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 43445 | 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 43446 | Membership in an open real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β β) & β’ (π β π΄ < πΆ) & β’ (π β πΆ < π΅) β β’ (π β πΆ β (π΄(,)π΅)) | ||
Theorem | iooabslt 43447 | An upper bound for the distance from the center of an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β ((π΄ β π΅)(,)(π΄ + π΅))) β β’ (π β (absβ(π΄ β πΆ)) < π΅) | ||
Theorem | gtnelicc 43448 | 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 43449 | An open interval has empty intersection with its bounds. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄(,)π΅) β© {π΄, π΅}) = β | ||
Theorem | iocgtlb 43450 | An element of a left-open right-closed interval is larger than its lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β (π΄(,]π΅)) β π΄ < πΆ) | ||
Theorem | iocleub 43451 | 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 43452 | Membership in a closed real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΄ β€ πΆ) & β’ (π β πΆ β€ π΅) β β’ (π β πΆ β (π΄[,]π΅)) | ||
Theorem | eliccre 43453 | A member of a closed interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β (π΄[,]π΅)) β πΆ β β) | ||
Theorem | eliooshift 43454 | Element of an open interval shifted by a displacement. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) β β’ (π β (π΄ β (π΅(,)πΆ) β (π΄ + π·) β ((π΅ + π·)(,)(πΆ + π·)))) | ||
Theorem | eliocd 43455 | Membership in a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β β*) & β’ (π β π΄ < πΆ) & β’ (π β πΆ β€ π΅) β β’ (π β πΆ β (π΄(,]π΅)) | ||
Theorem | icoltub 43456 | An element of a left-closed right-open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β (π΄[,)π΅)) β πΆ < π΅) | ||
Theorem | eliocre 43457 | A member of a left-open right-closed interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΅ β β β§ πΆ β (π΄(,]π΅)) β πΆ β β) | ||
Theorem | iooltub 43458 | An element of an open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β (π΄(,)π΅)) β πΆ < π΅) | ||
Theorem | ioontr 43459 | 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 43460 | The closure of one end of an open real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β* β§ π΅ β β* β§ π΄ < π΅) β ((π΄(,)π΅) βͺ {π΄}) = (π΄[,)π΅)) | ||
Theorem | lbioc 43461 | A left-open right-closed interval does not contain its left endpoint. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ Β¬ π΄ β (π΄(,]π΅) | ||
Theorem | ioomidp 43462 | The midpoint is an element of the open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ < π΅) β ((π΄ + π΅) / 2) β (π΄(,)π΅)) | ||
Theorem | iccdifioo 43463 | If the open inverval is removed from the closed interval, only the bounds are left. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β* β§ π΅ β β* β§ π΄ β€ π΅) β ((π΄[,]π΅) β (π΄(,)π΅)) = {π΄, π΅}) | ||
Theorem | iccdifprioo 43464 | An open interval is the closed interval without the bounds. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β* β§ π΅ β β*) β ((π΄[,]π΅) β {π΄, π΅}) = (π΄(,)π΅)) | ||
Theorem | ioossioobi 43465 | Biconditional form of ioossioo 13287. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β β*) & β’ (π β π· β β*) & β’ (π β πΆ < π·) β β’ (π β ((πΆ(,)π·) β (π΄(,)π΅) β (π΄ β€ πΆ β§ π· β€ π΅))) | ||
Theorem | iccshift 43466* | A closed interval shifted by a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β) β β’ (π β ((π΄ + π)[,](π΅ + π)) = {π€ β β β£ βπ§ β (π΄[,]π΅)π€ = (π§ + π)}) | ||
Theorem | iccsuble 43467 | An upper bound to the distance of two elements in a closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β (π΄[,]π΅)) & β’ (π β π· β (π΄[,]π΅)) β β’ (π β (πΆ β π·) β€ (π΅ β π΄)) | ||
Theorem | iocopn 43468 | 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 43469 | Membership in a closed interval and in a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β*) β β’ (π β (πΆ β (π΄(,]π΅) β (πΆ β (π΄[,]π΅) β§ πΆ β π΄))) | ||
Theorem | iooshift 43470* | An open interval shifted by a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β) β β’ (π β ((π΄ + π)(,)(π΅ + π)) = {π€ β β β£ βπ§ β (π΄(,)π΅)π€ = (π§ + π)}) | ||
Theorem | iccintsng 43471 | Intersection of two adiacent closed intervals is a singleton. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ (π΄ β€ π΅ β§ π΅ β€ πΆ)) β ((π΄[,]π΅) β© (π΅[,]πΆ)) = {π΅}) | ||
Theorem | icoiccdif 43472 | Left-closed right-open interval gotten by a closed iterval taking away the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄[,)π΅) = ((π΄[,]π΅) β {π΅})) | ||
Theorem | icoopn 43473 | 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 43474 | A left-closed, right-open interval does not contain its upper bound. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π΄ β β* β Β¬ π΅ β (π΄[,)π΅)) | ||
Theorem | eliccxrd 43475 | Membership in a closed real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β β*) & β’ (π β π΄ β€ πΆ) & β’ (π β πΆ β€ π΅) β β’ (π β πΆ β (π΄[,]π΅)) | ||
Theorem | pnfel0pnf 43476 | +β is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ +β β (0[,]+β) | ||
Theorem | eliccnelico 43477 | 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 43478 | 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 43479 | A nonnegative extended real that is not +β is a real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ ((π΄ β (0[,]+β) β§ π΄ β +β) β π΄ β β) | ||
Theorem | ge0lere 43480 | 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 43481* | Membership in a left-closed, right-open interval with real bounds. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π΄ β ran ([,) βΎ (β Γ β)) β βπ₯ β β βπ¦ β β π΄ = (π₯[,)π¦)) | ||
Theorem | inficc 43482 | 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 43483 | The rational numbers are dense in β. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) β β’ (π β ((β β© (π΄(,)π΅)) = β β π΅ β€ π΄)) | ||
Theorem | lenelioc 43484 | 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 43485 | A nonempty open interval is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π΄ < π΅) & β’ πΆ = (π΄(,)π΅) β β’ (π β Β¬ πΆ βΌ Ο) | ||
Theorem | xrgtnelicc 43486 | 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 43487 | The difference of two closed intervals with the same lower bound. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β β*) & β’ (π β π΄ β€ π΅) β β’ (π β ((π΄[,]πΆ) β (π΄[,]π΅)) = (π΅(,]πΆ)) | ||
Theorem | iocnct 43488 | A nonempty left-open, right-closed interval is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π΄ < π΅) & β’ πΆ = (π΄(,]π΅) β β’ (π β Β¬ πΆ βΌ Ο) | ||
Theorem | iccnct 43489 | A closed interval, with more than one element is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π΄ < π΅) & β’ πΆ = (π΄[,]π΅) β β’ (π β Β¬ πΆ βΌ Ο) | ||
Theorem | iooiinicc 43490* | A closed interval expressed as the indexed intersection of open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β β© π β β ((π΄ β (1 / π))(,)(π΅ + (1 / π))) = (π΄[,]π΅)) | ||
Theorem | iccgelbd 43491 | An element of a closed interval is more than or equal to its lower bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄[,]π΅)) β β’ (π β π΄ β€ πΆ) | ||
Theorem | iooltubd 43492 | An element of an open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄(,)π΅)) β β’ (π β πΆ < π΅) | ||
Theorem | icoltubd 43493 | An element of a left-closed right-open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄[,)π΅)) β β’ (π β πΆ < π΅) | ||
Theorem | qelioo 43494* | 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 43495* | 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 43496 | An element of a closed interval is less than or equal to its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄[,]π΅)) β β’ (π β πΆ β€ π΅) | ||
Theorem | elioored 43497 | A member of an open interval of reals is a real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β (π΅(,)πΆ)) β β’ (π β π΄ β β) | ||
Theorem | ioogtlbd 43498 | An element of a closed interval is greater than its lower bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄(,)π΅)) β β’ (π β π΄ < πΆ) | ||
Theorem | ioofun 43499 | (,) is a function. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ Fun (,) | ||
Theorem | icomnfinre 43500 | A left-closed, right-open, interval of extended reals, intersected with the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) β β’ (π β ((-β[,)π΄) β© β) = (-β(,)π΄)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |