Type | Label | Description |
Statement |
|
Theorem | xsubge0 9901 |
Extended real version of subge0 8452. (Contributed by Mario Carneiro,
24-Aug-2015.)
|
β’ ((π΄ β β* β§ π΅ β β*)
β (0 β€ (π΄
+π -ππ΅) β π΅ β€ π΄)) |
|
Theorem | xposdif 9902 |
Extended real version of posdif 8432. (Contributed by Mario Carneiro,
24-Aug-2015.) (Revised by Jim Kingdon, 17-Apr-2023.)
|
β’ ((π΄ β β* β§ π΅ β β*)
β (π΄ < π΅ β 0 < (π΅ +π
-ππ΄))) |
|
Theorem | xlesubadd 9903 |
Under certain conditions, the conclusion of lesubadd 8411 is true even in the
extended reals. (Contributed by Mario Carneiro, 4-Sep-2015.)
|
β’ (((π΄ β β* β§ π΅ β β*
β§ πΆ β
β*) β§ (0 β€ π΄ β§ π΅ β -β β§ 0 β€ πΆ)) β ((π΄ +π
-ππ΅)
β€ πΆ β π΄ β€ (πΆ +π π΅))) |
|
Theorem | xaddcld 9904 |
The extended real addition operation is closed in extended reals.
(Contributed by Mario Carneiro, 28-May-2016.)
|
β’ (π β π΄ β β*) & β’ (π β π΅ β
β*) β β’ (π β (π΄ +π π΅) β
β*) |
|
Theorem | xadd4d 9905 |
Rearrangement of 4 terms in a sum for extended addition, analogous to
add4d 8146. (Contributed by Alexander van der Vekens,
21-Dec-2017.)
|
β’ (π β (π΄ β β* β§ π΄ β -β)) & β’ (π β (π΅ β β* β§ π΅ β -β)) & β’ (π β (πΆ β β* β§ πΆ β -β)) & β’ (π β (π· β β* β§ π· β
-β)) β β’ (π β ((π΄ +π π΅) +π (πΆ +π π·)) = ((π΄ +π πΆ) +π (π΅ +π π·))) |
|
Theorem | xnn0add4d 9906 |
Rearrangement of 4 terms in a sum for extended addition of extended
nonnegative integers, analogous to xadd4d 9905. (Contributed by AV,
12-Dec-2020.)
|
β’ (π β π΄ β
β0*)
& β’ (π β π΅ β
β0*)
& β’ (π β πΆ β
β0*)
& β’ (π β π· β
β0*) β β’ (π β ((π΄ +π π΅) +π (πΆ +π π·)) = ((π΄ +π πΆ) +π (π΅ +π π·))) |
|
Theorem | xleaddadd 9907 |
Cancelling a factor of two in β€ (expressed as
addition rather than
as a factor to avoid extended real multiplication). (Contributed by Jim
Kingdon, 18-Apr-2023.)
|
β’ ((π΄ β β* β§ π΅ β β*)
β (π΄ β€ π΅ β (π΄ +π π΄) β€ (π΅ +π π΅))) |
|
4.5.3 Real number intervals
|
|
Syntax | cioo 9908 |
Extend class notation with the set of open intervals of extended reals.
|
class (,) |
|
Syntax | cioc 9909 |
Extend class notation with the set of open-below, closed-above intervals
of extended reals.
|
class (,] |
|
Syntax | cico 9910 |
Extend class notation with the set of closed-below, open-above intervals
of extended reals.
|
class [,) |
|
Syntax | cicc 9911 |
Extend class notation with the set of closed intervals of extended
reals.
|
class [,] |
|
Definition | df-ioo 9912* |
Define the set of open intervals of extended reals. (Contributed by NM,
24-Dec-2006.)
|
β’ (,) = (π₯ β β*, π¦ β β*
β¦ {π§ β
β* β£ (π₯ < π§ β§ π§ < π¦)}) |
|
Definition | df-ioc 9913* |
Define the set of open-below, closed-above intervals of extended reals.
(Contributed by NM, 24-Dec-2006.)
|
β’ (,] = (π₯ β β*, π¦ β β*
β¦ {π§ β
β* β£ (π₯ < π§ β§ π§ β€ π¦)}) |
|
Definition | df-ico 9914* |
Define the set of closed-below, open-above intervals of extended reals.
(Contributed by NM, 24-Dec-2006.)
|
β’ [,) = (π₯ β β*, π¦ β β*
β¦ {π§ β
β* β£ (π₯ β€ π§ β§ π§ < π¦)}) |
|
Definition | df-icc 9915* |
Define the set of closed intervals of extended reals. (Contributed by
NM, 24-Dec-2006.)
|
β’ [,] = (π₯ β β*, π¦ β β*
β¦ {π§ β
β* β£ (π₯ β€ π§ β§ π§ β€ π¦)}) |
|
Theorem | ixxval 9916* |
Value of the interval function. (Contributed by Mario Carneiro,
3-Nov-2013.)
|
β’ π = (π₯ β β*, π¦ β β*
β¦ {π§ β
β* β£ (π₯π
π§ β§ π§ππ¦)}) β β’ ((π΄ β β* β§ π΅ β β*)
β (π΄ππ΅) = {π§ β β* β£ (π΄π
π§ β§ π§ππ΅)}) |
|
Theorem | elixx1 9917* |
Membership in an interval of extended reals. (Contributed by Mario
Carneiro, 3-Nov-2013.)
|
β’ π = (π₯ β β*, π¦ β β*
β¦ {π§ β
β* β£ (π₯π
π§ β§ π§ππ¦)}) β β’ ((π΄ β β* β§ π΅ β β*)
β (πΆ β (π΄ππ΅) β (πΆ β β* β§ π΄π
πΆ β§ πΆππ΅))) |
|
Theorem | ixxf 9918* |
The set of intervals of extended reals maps to subsets of extended
reals. (Contributed by FL, 14-Jun-2007.) (Revised by Mario Carneiro,
16-Nov-2013.)
|
β’ π = (π₯ β β*, π¦ β β*
β¦ {π§ β
β* β£ (π₯π
π§ β§ π§ππ¦)}) β β’ π:(β* Γ
β*)βΆπ« β* |
|
Theorem | ixxex 9919* |
The set of intervals of extended reals exists. (Contributed by Mario
Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
|
β’ π = (π₯ β β*, π¦ β β*
β¦ {π§ β
β* β£ (π₯π
π§ β§ π§ππ¦)}) β β’ π β V |
|
Theorem | ixxssxr 9920* |
The set of intervals of extended reals maps to subsets of extended
reals. (Contributed by Mario Carneiro, 4-Jul-2014.)
|
β’ π = (π₯ β β*, π¦ β β*
β¦ {π§ β
β* β£ (π₯π
π§ β§ π§ππ¦)}) β β’ (π΄ππ΅) β
β* |
|
Theorem | elixx3g 9921* |
Membership in a set of open intervals of extended reals. We use the
fact that an operation's value is empty outside of its domain to show
π΄
β β* and π΅ β β*.
(Contributed by Mario Carneiro,
3-Nov-2013.)
|
β’ π = (π₯ β β*, π¦ β β*
β¦ {π§ β
β* β£ (π₯π
π§ β§ π§ππ¦)}) β β’ (πΆ β (π΄ππ΅) β ((π΄ β β* β§ π΅ β β*
β§ πΆ β
β*) β§ (π΄π
πΆ β§ πΆππ΅))) |
|
Theorem | ixxssixx 9922* |
An interval is a subset of its closure. (Contributed by Paul Chapman,
18-Oct-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
β’ π = (π₯ β β*, π¦ β β*
β¦ {π§ β
β* β£ (π₯π
π§ β§ π§ππ¦)}) & β’ π = (π₯ β β*, π¦ β β*
β¦ {π§ β
β* β£ (π₯ππ§ β§ π§ππ¦)}) & β’ ((π΄ β β*
β§ π€ β
β*) β (π΄π
π€ β π΄ππ€))
& β’ ((π€ β β* β§ π΅ β β*)
β (π€ππ΅ β π€ππ΅)) β β’ (π΄ππ΅) β (π΄ππ΅) |
|
Theorem | ixxdisj 9923* |
Split an interval into disjoint pieces. (Contributed by Mario
Carneiro, 16-Jun-2014.)
|
β’ π = (π₯ β β*, π¦ β β*
β¦ {π§ β
β* β£ (π₯π
π§ β§ π§ππ¦)}) & β’ π = (π₯ β β*, π¦ β β*
β¦ {π§ β
β* β£ (π₯ππ§ β§ π§ππ¦)}) & β’ ((π΅ β β*
β§ π€ β
β*) β (π΅ππ€ β Β¬ π€ππ΅)) β β’ ((π΄ β β* β§ π΅ β β*
β§ πΆ β
β*) β ((π΄ππ΅) β© (π΅ππΆ)) = β
) |
|
Theorem | ixxss1 9924* |
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
β’ π = (π₯ β β*, π¦ β β*
β¦ {π§ β
β* β£ (π₯π
π§ β§ π§ππ¦)}) & β’ π = (π₯ β β*, π¦ β β*
β¦ {π§ β
β* β£ (π₯ππ§ β§ π§ππ¦)}) & β’ ((π΄ β β*
β§ π΅ β
β* β§ π€ β β*) β ((π΄ππ΅ β§ π΅ππ€) β π΄π
π€)) β β’ ((π΄ β β* β§ π΄ππ΅) β (π΅ππΆ) β (π΄ππΆ)) |
|
Theorem | ixxss2 9925* |
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
β’ π = (π₯ β β*, π¦ β β*
β¦ {π§ β
β* β£ (π₯π
π§ β§ π§ππ¦)}) & β’ π = (π₯ β β*, π¦ β β*
β¦ {π§ β
β* β£ (π₯π
π§ β§ π§ππ¦)}) & β’ ((π€ β β*
β§ π΅ β
β* β§ πΆ β β*) β ((π€ππ΅ β§ π΅ππΆ) β π€ππΆ)) β β’ ((πΆ β β* β§ π΅ππΆ) β (π΄ππ΅) β (π΄ππΆ)) |
|
Theorem | ixxss12 9926* |
Subset relationship for intervals of extended reals. (Contributed by
Mario Carneiro, 20-Feb-2015.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
β’ π = (π₯ β β*, π¦ β β*
β¦ {π§ β
β* β£ (π₯π
π§ β§ π§ππ¦)}) & β’ π = (π₯ β β*, π¦ β β*
β¦ {π§ β
β* β£ (π₯ππ§ β§ π§ππ¦)}) & β’ ((π΄ β β*
β§ πΆ β
β* β§ π€ β β*) β ((π΄ππΆ β§ πΆππ€) β π΄π
π€))
& β’ ((π€ β β* β§ π· β β*
β§ π΅ β
β*) β ((π€ππ· β§ π·ππ΅) β π€ππ΅)) β β’ (((π΄ β β* β§ π΅ β β*)
β§ (π΄ππΆ β§ π·ππ΅)) β (πΆππ·) β (π΄ππ΅)) |
|
Theorem | iooex 9927 |
The set of open intervals of extended reals exists. (Contributed by NM,
6-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
β’ (,) β V |
|
Theorem | iooval 9928* |
Value of the open interval function. (Contributed by NM, 24-Dec-2006.)
(Revised by Mario Carneiro, 3-Nov-2013.)
|
β’ ((π΄ β β* β§ π΅ β β*)
β (π΄(,)π΅) = {π₯ β β* β£ (π΄ < π₯ β§ π₯ < π΅)}) |
|
Theorem | iooidg 9929 |
An open interval with identical lower and upper bounds is empty.
(Contributed by Jim Kingdon, 29-Mar-2020.)
|
β’ (π΄ β β* β (π΄(,)π΄) = β
) |
|
Theorem | elioo3g 9930 |
Membership in a set of open intervals of extended reals. We use the
fact that an operation's value is empty outside of its domain to show
π΄
β β* and π΅ β β*.
(Contributed by NM, 24-Dec-2006.)
(Revised by Mario Carneiro, 3-Nov-2013.)
|
β’ (πΆ β (π΄(,)π΅) β ((π΄ β β* β§ π΅ β β*
β§ πΆ β
β*) β§ (π΄ < πΆ β§ πΆ < π΅))) |
|
Theorem | elioo1 9931 |
Membership in an open interval of extended reals. (Contributed by NM,
24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
β’ ((π΄ β β* β§ π΅ β β*)
β (πΆ β (π΄(,)π΅) β (πΆ β β* β§ π΄ < πΆ β§ πΆ < π΅))) |
|
Theorem | elioore 9932 |
A member of an open interval of reals is a real. (Contributed by NM,
17-Aug-2008.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
β’ (π΄ β (π΅(,)πΆ) β π΄ β β) |
|
Theorem | lbioog 9933 |
An open interval does not contain its left endpoint. (Contributed by
Jim Kingdon, 30-Mar-2020.)
|
β’ ((π΄ β β* β§ π΅ β β*)
β Β¬ π΄ β
(π΄(,)π΅)) |
|
Theorem | ubioog 9934 |
An open interval does not contain its right endpoint. (Contributed by
Jim Kingdon, 30-Mar-2020.)
|
β’ ((π΄ β β* β§ π΅ β β*)
β Β¬ π΅ β
(π΄(,)π΅)) |
|
Theorem | iooval2 9935* |
Value of the open interval function. (Contributed by NM, 6-Feb-2007.)
(Revised by Mario Carneiro, 3-Nov-2013.)
|
β’ ((π΄ β β* β§ π΅ β β*)
β (π΄(,)π΅) = {π₯ β β β£ (π΄ < π₯ β§ π₯ < π΅)}) |
|
Theorem | iooss1 9936 |
Subset relationship for open intervals of extended reals. (Contributed
by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 20-Feb-2015.)
|
β’ ((π΄ β β* β§ π΄ β€ π΅) β (π΅(,)πΆ) β (π΄(,)πΆ)) |
|
Theorem | iooss2 9937 |
Subset relationship for open intervals of extended reals. (Contributed
by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
β’ ((πΆ β β* β§ π΅ β€ πΆ) β (π΄(,)π΅) β (π΄(,)πΆ)) |
|
Theorem | iocval 9938* |
Value of the open-below, closed-above interval function. (Contributed
by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
β’ ((π΄ β β* β§ π΅ β β*)
β (π΄(,]π΅) = {π₯ β β* β£ (π΄ < π₯ β§ π₯ β€ π΅)}) |
|
Theorem | icoval 9939* |
Value of the closed-below, open-above interval function. (Contributed
by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
β’ ((π΄ β β* β§ π΅ β β*)
β (π΄[,)π΅) = {π₯ β β* β£ (π΄ β€ π₯ β§ π₯ < π΅)}) |
|
Theorem | iccval 9940* |
Value of the closed interval function. (Contributed by NM,
24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
β’ ((π΄ β β* β§ π΅ β β*)
β (π΄[,]π΅) = {π₯ β β* β£ (π΄ β€ π₯ β§ π₯ β€ π΅)}) |
|
Theorem | elioo2 9941 |
Membership in an open interval of extended reals. (Contributed by NM,
6-Feb-2007.)
|
β’ ((π΄ β β* β§ π΅ β β*)
β (πΆ β (π΄(,)π΅) β (πΆ β β β§ π΄ < πΆ β§ πΆ < π΅))) |
|
Theorem | elioc1 9942 |
Membership in an open-below, closed-above interval of extended reals.
(Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro,
3-Nov-2013.)
|
β’ ((π΄ β β* β§ π΅ β β*)
β (πΆ β (π΄(,]π΅) β (πΆ β β* β§ π΄ < πΆ β§ πΆ β€ π΅))) |
|
Theorem | elico1 9943 |
Membership in a closed-below, open-above interval of extended reals.
(Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro,
3-Nov-2013.)
|
β’ ((π΄ β β* β§ π΅ β β*)
β (πΆ β (π΄[,)π΅) β (πΆ β β* β§ π΄ β€ πΆ β§ πΆ < π΅))) |
|
Theorem | elicc1 9944 |
Membership in a closed interval of extended reals. (Contributed by NM,
24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|
β’ ((π΄ β β* β§ π΅ β β*)
β (πΆ β (π΄[,]π΅) β (πΆ β β* β§ π΄ β€ πΆ β§ πΆ β€ π΅))) |
|
Theorem | iccid 9945 |
A closed interval with identical lower and upper bounds is a singleton.
(Contributed by Jeff Hankins, 13-Jul-2009.)
|
β’ (π΄ β β* β (π΄[,]π΄) = {π΄}) |
|
Theorem | icc0r 9946 |
An empty closed interval of extended reals. (Contributed by Jim
Kingdon, 30-Mar-2020.)
|
β’ ((π΄ β β* β§ π΅ β β*)
β (π΅ < π΄ β (π΄[,]π΅) = β
)) |
|
Theorem | eliooxr 9947 |
An inhabited open interval spans an interval of extended reals.
(Contributed by NM, 17-Aug-2008.)
|
β’ (π΄ β (π΅(,)πΆ) β (π΅ β β* β§ πΆ β
β*)) |
|
Theorem | eliooord 9948 |
Ordering implied by a member of an open interval of reals. (Contributed
by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 9-May-2014.)
|
β’ (π΄ β (π΅(,)πΆ) β (π΅ < π΄ β§ π΄ < πΆ)) |
|
Theorem | ubioc1 9949 |
The upper bound belongs to an open-below, closed-above interval. See
ubicc2 10005. (Contributed by FL, 29-May-2014.)
|
β’ ((π΄ β β* β§ π΅ β β*
β§ π΄ < π΅) β π΅ β (π΄(,]π΅)) |
|
Theorem | lbico1 9950 |
The lower bound belongs to a closed-below, open-above interval. See
lbicc2 10004. (Contributed by FL, 29-May-2014.)
|
β’ ((π΄ β β* β§ π΅ β β*
β§ π΄ < π΅) β π΄ β (π΄[,)π΅)) |
|
Theorem | iccleub 9951 |
An element of a closed interval is less than or equal to its upper bound.
(Contributed by Jeff Hankins, 14-Jul-2009.)
|
β’ ((π΄ β β* β§ π΅ β β*
β§ πΆ β (π΄[,]π΅)) β πΆ β€ π΅) |
|
Theorem | iccgelb 9952 |
An element of a closed interval is more than or equal to its lower bound
(Contributed by Thierry Arnoux, 23-Dec-2016.)
|
β’ ((π΄ β β* β§ π΅ β β*
β§ πΆ β (π΄[,]π΅)) β π΄ β€ πΆ) |
|
Theorem | elioo5 9953 |
Membership in an open interval of extended reals. (Contributed by NM,
17-Aug-2008.)
|
β’ ((π΄ β β* β§ π΅ β β*
β§ πΆ β
β*) β (πΆ β (π΄(,)π΅) β (π΄ < πΆ β§ πΆ < π΅))) |
|
Theorem | elioo4g 9954 |
Membership in an open interval of extended reals. (Contributed by NM,
8-Jun-2007.) (Revised by Mario Carneiro, 28-Apr-2015.)
|
β’ (πΆ β (π΄(,)π΅) β ((π΄ β β* β§ π΅ β β*
β§ πΆ β β)
β§ (π΄ < πΆ β§ πΆ < π΅))) |
|
Theorem | ioossre 9955 |
An open interval is a set of reals. (Contributed by NM,
31-May-2007.)
|
β’ (π΄(,)π΅) β β |
|
Theorem | elioc2 9956 |
Membership in an open-below, closed-above real interval. (Contributed by
Paul Chapman, 30-Dec-2007.) (Revised by Mario Carneiro, 14-Jun-2014.)
|
β’ ((π΄ β β* β§ π΅ β β) β (πΆ β (π΄(,]π΅) β (πΆ β β β§ π΄ < πΆ β§ πΆ β€ π΅))) |
|
Theorem | elico2 9957 |
Membership in a closed-below, open-above real interval. (Contributed by
Paul Chapman, 21-Jan-2008.) (Revised by Mario Carneiro, 14-Jun-2014.)
|
β’ ((π΄ β β β§ π΅ β β*) β (πΆ β (π΄[,)π΅) β (πΆ β β β§ π΄ β€ πΆ β§ πΆ < π΅))) |
|
Theorem | elicc2 9958 |
Membership in a closed real interval. (Contributed by Paul Chapman,
21-Sep-2007.) (Revised by Mario Carneiro, 14-Jun-2014.)
|
β’ ((π΄ β β β§ π΅ β β) β (πΆ β (π΄[,]π΅) β (πΆ β β β§ π΄ β€ πΆ β§ πΆ β€ π΅))) |
|
Theorem | elicc2i 9959 |
Inference for membership in a closed interval. (Contributed by Scott
Fenton, 3-Jun-2013.)
|
β’ π΄ β β & β’ π΅ β
β β β’ (πΆ β (π΄[,]π΅) β (πΆ β β β§ π΄ β€ πΆ β§ πΆ β€ π΅)) |
|
Theorem | elicc4 9960 |
Membership in a closed real interval. (Contributed by Stefan O'Rear,
16-Nov-2014.) (Proof shortened by Mario Carneiro, 1-Jan-2017.)
|
β’ ((π΄ β β* β§ π΅ β β*
β§ πΆ β
β*) β (πΆ β (π΄[,]π΅) β (π΄ β€ πΆ β§ πΆ β€ π΅))) |
|
Theorem | iccss 9961 |
Condition for a closed interval to be a subset of another closed
interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario
Carneiro, 20-Feb-2015.)
|
β’ (((π΄ β β β§ π΅ β β) β§ (π΄ β€ πΆ β§ π· β€ π΅)) β (πΆ[,]π·) β (π΄[,]π΅)) |
|
Theorem | iccssioo 9962 |
Condition for a closed interval to be a subset of an open interval.
(Contributed by Mario Carneiro, 20-Feb-2015.)
|
β’ (((π΄ β β* β§ π΅ β β*)
β§ (π΄ < πΆ β§ π· < π΅)) β (πΆ[,]π·) β (π΄(,)π΅)) |
|
Theorem | icossico 9963 |
Condition for a closed-below, open-above interval to be a subset of a
closed-below, open-above interval. (Contributed by Thierry Arnoux,
21-Sep-2017.)
|
β’ (((π΄ β β* β§ π΅ β β*)
β§ (π΄ β€ πΆ β§ π· β€ π΅)) β (πΆ[,)π·) β (π΄[,)π΅)) |
|
Theorem | iccss2 9964 |
Condition for a closed interval to be a subset of another closed
interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario
Carneiro, 28-Apr-2015.)
|
β’ ((πΆ β (π΄[,]π΅) β§ π· β (π΄[,]π΅)) β (πΆ[,]π·) β (π΄[,]π΅)) |
|
Theorem | iccssico 9965 |
Condition for a closed interval to be a subset of a half-open interval.
(Contributed by Mario Carneiro, 9-Sep-2015.)
|
β’ (((π΄ β β* β§ π΅ β β*)
β§ (π΄ β€ πΆ β§ π· < π΅)) β (πΆ[,]π·) β (π΄[,)π΅)) |
|
Theorem | iccssioo2 9966 |
Condition for a closed interval to be a subset of an open interval.
(Contributed by Mario Carneiro, 20-Feb-2015.)
|
β’ ((πΆ β (π΄(,)π΅) β§ π· β (π΄(,)π΅)) β (πΆ[,]π·) β (π΄(,)π΅)) |
|
Theorem | iccssico2 9967 |
Condition for a closed interval to be a subset of a closed-below,
open-above interval. (Contributed by Mario Carneiro, 20-Feb-2015.)
|
β’ ((πΆ β (π΄[,)π΅) β§ π· β (π΄[,)π΅)) β (πΆ[,]π·) β (π΄[,)π΅)) |
|
Theorem | ioomax 9968 |
The open interval from minus to plus infinity. (Contributed by NM,
6-Feb-2007.)
|
β’ (-β(,)+β) =
β |
|
Theorem | iccmax 9969 |
The closed interval from minus to plus infinity. (Contributed by Mario
Carneiro, 4-Jul-2014.)
|
β’ (-β[,]+β) =
β* |
|
Theorem | ioopos 9970 |
The set of positive reals expressed as an open interval. (Contributed by
NM, 7-May-2007.)
|
β’ (0(,)+β) = {π₯ β β β£ 0 < π₯} |
|
Theorem | ioorp 9971 |
The set of positive reals expressed as an open interval. (Contributed by
Steve Rodriguez, 25-Nov-2007.)
|
β’ (0(,)+β) =
β+ |
|
Theorem | iooshf 9972 |
Shift the arguments of the open interval function. (Contributed by NM,
17-Aug-2008.)
|
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ β π΅) β (πΆ(,)π·) β π΄ β ((πΆ + π΅)(,)(π· + π΅)))) |
|
Theorem | iocssre 9973 |
A closed-above interval with real upper bound is a set of reals.
(Contributed by FL, 29-May-2014.)
|
β’ ((π΄ β β* β§ π΅ β β) β (π΄(,]π΅) β β) |
|
Theorem | icossre 9974 |
A closed-below interval with real lower bound is a set of reals.
(Contributed by Mario Carneiro, 14-Jun-2014.)
|
β’ ((π΄ β β β§ π΅ β β*) β (π΄[,)π΅) β β) |
|
Theorem | iccssre 9975 |
A closed real interval is a set of reals. (Contributed by FL,
6-Jun-2007.) (Proof shortened by Paul Chapman, 21-Jan-2008.)
|
β’ ((π΄ β β β§ π΅ β β) β (π΄[,]π΅) β β) |
|
Theorem | iccssxr 9976 |
A closed interval is a set of extended reals. (Contributed by FL,
28-Jul-2008.) (Revised by Mario Carneiro, 4-Jul-2014.)
|
β’ (π΄[,]π΅) β
β* |
|
Theorem | iocssxr 9977 |
An open-below, closed-above interval is a subset of the extended reals.
(Contributed by FL, 29-May-2014.) (Revised by Mario Carneiro,
4-Jul-2014.)
|
β’ (π΄(,]π΅) β
β* |
|
Theorem | icossxr 9978 |
A closed-below, open-above interval is a subset of the extended reals.
(Contributed by FL, 29-May-2014.) (Revised by Mario Carneiro,
4-Jul-2014.)
|
β’ (π΄[,)π΅) β
β* |
|
Theorem | ioossicc 9979 |
An open interval is a subset of its closure. (Contributed by Paul
Chapman, 18-Oct-2007.)
|
β’ (π΄(,)π΅) β (π΄[,]π΅) |
|
Theorem | icossicc 9980 |
A closed-below, open-above interval is a subset of its closure.
(Contributed by Thierry Arnoux, 25-Oct-2016.)
|
β’ (π΄[,)π΅) β (π΄[,]π΅) |
|
Theorem | iocssicc 9981 |
A closed-above, open-below interval is a subset of its closure.
(Contributed by Thierry Arnoux, 1-Apr-2017.)
|
β’ (π΄(,]π΅) β (π΄[,]π΅) |
|
Theorem | ioossico 9982 |
An open interval is a subset of its closure-below. (Contributed by
Thierry Arnoux, 3-Mar-2017.)
|
β’ (π΄(,)π΅) β (π΄[,)π΅) |
|
Theorem | iocssioo 9983 |
Condition for a closed interval to be a subset of an open interval.
(Contributed by Thierry Arnoux, 29-Mar-2017.)
|
β’ (((π΄ β β* β§ π΅ β β*)
β§ (π΄ β€ πΆ β§ π· < π΅)) β (πΆ(,]π·) β (π΄(,)π΅)) |
|
Theorem | icossioo 9984 |
Condition for a closed interval to be a subset of an open interval.
(Contributed by Thierry Arnoux, 29-Mar-2017.)
|
β’ (((π΄ β β* β§ π΅ β β*)
β§ (π΄ < πΆ β§ π· β€ π΅)) β (πΆ[,)π·) β (π΄(,)π΅)) |
|
Theorem | ioossioo 9985 |
Condition for an open interval to be a subset of an open interval.
(Contributed by Thierry Arnoux, 26-Sep-2017.)
|
β’ (((π΄ β β* β§ π΅ β β*)
β§ (π΄ β€ πΆ β§ π· β€ π΅)) β (πΆ(,)π·) β (π΄(,)π΅)) |
|
Theorem | iccsupr 9986* |
A nonempty subset of a closed real interval satisfies the conditions for
the existence of its supremum. To be useful without excluded middle,
we'll probably need to change not equal to apart, and perhaps make other
changes, but the theorem does hold as stated here. (Contributed by Paul
Chapman, 21-Jan-2008.)
|
β’ (((π΄ β β β§ π΅ β β) β§ π β (π΄[,]π΅) β§ πΆ β π) β (π β β β§ π β β
β§ βπ₯ β β βπ¦ β π π¦ β€ π₯)) |
|
Theorem | elioopnf 9987 |
Membership in an unbounded interval of extended reals. (Contributed by
Mario Carneiro, 18-Jun-2014.)
|
β’ (π΄ β β* β (π΅ β (π΄(,)+β) β (π΅ β β β§ π΄ < π΅))) |
|
Theorem | elioomnf 9988 |
Membership in an unbounded interval of extended reals. (Contributed by
Mario Carneiro, 18-Jun-2014.)
|
β’ (π΄ β β* β (π΅ β (-β(,)π΄) β (π΅ β β β§ π΅ < π΄))) |
|
Theorem | elicopnf 9989 |
Membership in a closed unbounded interval of reals. (Contributed by
Mario Carneiro, 16-Sep-2014.)
|
β’ (π΄ β β β (π΅ β (π΄[,)+β) β (π΅ β β β§ π΄ β€ π΅))) |
|
Theorem | repos 9990 |
Two ways of saying that a real number is positive. (Contributed by NM,
7-May-2007.)
|
β’ (π΄ β (0(,)+β) β (π΄ β β β§ 0 <
π΄)) |
|
Theorem | ioof 9991 |
The set of open intervals of extended reals maps to subsets of reals.
(Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro,
16-Nov-2013.)
|
β’ (,):(β* Γ
β*)βΆπ« β |
|
Theorem | iccf 9992 |
The set of closed intervals of extended reals maps to subsets of
extended reals. (Contributed by FL, 14-Jun-2007.) (Revised by Mario
Carneiro, 3-Nov-2013.)
|
β’ [,]:(β* Γ
β*)βΆπ« β* |
|
Theorem | unirnioo 9993 |
The union of the range of the open interval function. (Contributed by
NM, 7-May-2007.) (Revised by Mario Carneiro, 30-Jan-2014.)
|
β’ β = βͺ ran
(,) |
|
Theorem | dfioo2 9994* |
Alternate definition of the set of open intervals of extended reals.
(Contributed by NM, 1-Mar-2007.) (Revised by Mario Carneiro,
1-Sep-2015.)
|
β’ (,) = (π₯ β β*, π¦ β β*
β¦ {π€ β β
β£ (π₯ < π€ β§ π€ < π¦)}) |
|
Theorem | ioorebasg 9995 |
Open intervals are elements of the set of all open intervals.
(Contributed by Jim Kingdon, 4-Apr-2020.)
|
β’ ((π΄ β β* β§ π΅ β β*)
β (π΄(,)π΅) β ran
(,)) |
|
Theorem | elrege0 9996 |
The predicate "is a nonnegative real". (Contributed by Jeff Madsen,
2-Sep-2009.) (Proof shortened by Mario Carneiro, 18-Jun-2014.)
|
β’ (π΄ β (0[,)+β) β (π΄ β β β§ 0 β€
π΄)) |
|
Theorem | rge0ssre 9997 |
Nonnegative real numbers are real numbers. (Contributed by Thierry
Arnoux, 9-Sep-2018.) (Proof shortened by AV, 8-Sep-2019.)
|
β’ (0[,)+β) β
β |
|
Theorem | elxrge0 9998 |
Elementhood in the set of nonnegative extended reals. (Contributed by
Mario Carneiro, 28-Jun-2014.)
|
β’ (π΄ β (0[,]+β) β (π΄ β β*
β§ 0 β€ π΄)) |
|
Theorem | 0e0icopnf 9999 |
0 is a member of (0[,)+β) (common case).
(Contributed by David
A. Wheeler, 8-Dec-2018.)
|
β’ 0 β (0[,)+β) |
|
Theorem | 0e0iccpnf 10000 |
0 is a member of (0[,]+β) (common case).
(Contributed by David
A. Wheeler, 8-Dec-2018.)
|
β’ 0 β (0[,]+β) |