P. 100 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9901-10000   *Has distinct variable group(s)

Type	Label	Description
Statement
4.5.3  Real number intervals
Syntax	cioo 9901	Extend class notation with the set of open intervals of extended reals.
class (,)
Syntax	cioc 9902	Extend class notation with the set of open-below, closed-above intervals of extended reals.
class (,]
Syntax	cico 9903	Extend class notation with the set of closed-below, open-above intervals of extended reals.
class [,)
Syntax	cicc 9904	Extend class notation with the set of closed intervals of extended reals.
class [,]
Definition	df-ioo 9905*	Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
Definition	df-ioc 9906*	Define the set of open-below, closed-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
|- (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
Definition	df-ico 9907*	Define the set of closed-below, open-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
|- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
Definition	df-icc 9908*	Define the set of closed intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
|- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
Theorem	ixxval 9909*	Value of the interval function. (Contributed by Mario Carneiro, 3-Nov-2013.)
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )   =>    |- ( ( A e. RR* /\ B e. RR* ) -> ( A O B ) = { z e. RR* | ( A R z /\ z S B ) } )
Theorem	elixx1 9910*	Membership in an interval of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.)
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )   =>    |- ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A O B ) <-> ( C e. RR* /\ A R C /\ C S B ) ) )
Theorem	ixxf 9911*	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.)
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )   =>    |- O : ( RR* X. RR* ) --> ~P RR*
Theorem	ixxex 9912*	The set of intervals of extended reals exists. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )   =>    |- O e. _V
Theorem	ixxssxr 9913*	The set of intervals of extended reals maps to subsets of extended reals. (Contributed by Mario Carneiro, 4-Jul-2014.)
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )   =>    |- ( A O B ) C_ RR*
Theorem	elixx3g 9914*	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 A e. RR* and B e. RR*. (Contributed by Mario Carneiro, 3-Nov-2013.)
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )   =>    |- ( C e. ( A O B ) <-> ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A R C /\ C S B ) ) )
Theorem	ixxssixx 9915*	An interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )   &    |- P = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x T z /\ z U y ) } )   &    |- ( ( A e. RR* /\ w e. RR* ) -> ( A R w -> A T w ) )   &    |- ( ( w e. RR* /\ B e. RR* ) -> ( w S B -> w U B ) )   =>    |- ( A O B ) C_ ( A P B )
Theorem	ixxdisj 9916*	Split an interval into disjoint pieces. (Contributed by Mario Carneiro, 16-Jun-2014.)
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )   &    |- P = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x T z /\ z U y ) } )   &    |- ( ( B e. RR* /\ w e. RR* ) -> ( B T w <-> -. w S B ) )   =>    |- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A O B ) i^i ( B P C ) ) = (/) )
Theorem	ixxss1 9917*	Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )   &    |- P = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x T z /\ z S y ) } )   &    |- ( ( A e. RR* /\ B e. RR* /\ w e. RR* ) -> ( ( A W B /\ B T w ) -> A R w ) )   =>    |- ( ( A e. RR* /\ A W B ) -> ( B P C ) C_ ( A O C ) )
Theorem	ixxss2 9918*	Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )   &    |- P = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z T y ) } )   &    |- ( ( w e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( w T B /\ B W C ) -> w S C ) )   =>    |- ( ( C e. RR* /\ B W C ) -> ( A P B ) C_ ( A O C ) )
Theorem	ixxss12 9919*	Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 20-Feb-2015.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )   &    |- P = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x T z /\ z U y ) } )   &    |- ( ( A e. RR* /\ C e. RR* /\ w e. RR* ) -> ( ( A W C /\ C T w ) -> A R w ) )   &    |- ( ( w e. RR* /\ D e. RR* /\ B e. RR* ) -> ( ( w U D /\ D X B ) -> w S B ) )   =>    |- ( ( ( A e. RR* /\ B e. RR* ) /\ ( A W C /\ D X B ) ) -> ( C P D ) C_ ( A O B ) )
Theorem	iooex 9920	The set of open intervals of extended reals exists. (Contributed by NM, 6-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- (,) e. _V
Theorem	iooval 9921*	Value of the open interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A (,) B ) = { x e. RR* | ( A < x /\ x < B ) } )
Theorem	iooidg 9922	An open interval with identical lower and upper bounds is empty. (Contributed by Jim Kingdon, 29-Mar-2020.)
|- ( A e. RR* -> ( A (,) A ) = (/) )
Theorem	elioo3g 9923	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 A e. RR* and B e. RR*. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( C e. ( A (,) B ) <-> ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < C /\ C < B ) ) )
Theorem	elioo1 9924	Membership in an open interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A (,) B ) <-> ( C e. RR* /\ A < C /\ C < B ) ) )
Theorem	elioore 9925	A member of an open interval of reals is a real. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( A e. ( B (,) C ) -> A e. RR )
Theorem	lbioog 9926	An open interval does not contain its left endpoint. (Contributed by Jim Kingdon, 30-Mar-2020.)
|- ( ( A e. RR* /\ B e. RR* ) -> -. A e. ( A (,) B ) )
Theorem	ubioog 9927	An open interval does not contain its right endpoint. (Contributed by Jim Kingdon, 30-Mar-2020.)
|- ( ( A e. RR* /\ B e. RR* ) -> -. B e. ( A (,) B ) )
Theorem	iooval2 9928*	Value of the open interval function. (Contributed by NM, 6-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A (,) B ) = { x e. RR | ( A < x /\ x < B ) } )
Theorem	iooss1 9929	Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 20-Feb-2015.)
|- ( ( A e. RR* /\ A <_ B ) -> ( B (,) C ) C_ ( A (,) C ) )
Theorem	iooss2 9930	Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( ( C e. RR* /\ B <_ C ) -> ( A (,) B ) C_ ( A (,) C ) )
Theorem	iocval 9931*	Value of the open-below, closed-above interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A (,] B ) = { x e. RR* | ( A < x /\ x <_ B ) } )
Theorem	icoval 9932*	Value of the closed-below, open-above interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A [,) B ) = { x e. RR* | ( A <_ x /\ x < B ) } )
Theorem	iccval 9933*	Value of the closed interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A [,] B ) = { x e. RR* | ( A <_ x /\ x <_ B ) } )
Theorem	elioo2 9934	Membership in an open interval of extended reals. (Contributed by NM, 6-Feb-2007.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A (,) B ) <-> ( C e. RR /\ A < C /\ C < B ) ) )
Theorem	elioc1 9935	Membership in an open-below, closed-above interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A (,] B ) <-> ( C e. RR* /\ A < C /\ C <_ B ) ) )
Theorem	elico1 9936	Membership in a closed-below, open-above interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A [,) B ) <-> ( C e. RR* /\ A <_ C /\ C < B ) ) )
Theorem	elicc1 9937	Membership in a closed interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A [,] B ) <-> ( C e. RR* /\ A <_ C /\ C <_ B ) ) )
Theorem	iccid 9938	A closed interval with identical lower and upper bounds is a singleton. (Contributed by Jeff Hankins, 13-Jul-2009.)
|- ( A e. RR* -> ( A [,] A ) = { A } )
Theorem	icc0r 9939	An empty closed interval of extended reals. (Contributed by Jim Kingdon, 30-Mar-2020.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( B < A -> ( A [,] B ) = (/) ) )
Theorem	eliooxr 9940	An inhabited open interval spans an interval of extended reals. (Contributed by NM, 17-Aug-2008.)
|- ( A e. ( B (,) C ) -> ( B e. RR* /\ C e. RR* ) )
Theorem	eliooord 9941	Ordering implied by a member of an open interval of reals. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 9-May-2014.)
|- ( A e. ( B (,) C ) -> ( B < A /\ A < C ) )
Theorem	ubioc1 9942	The upper bound belongs to an open-below, closed-above interval. See ubicc2 9998. (Contributed by FL, 29-May-2014.)
|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> B e. ( A (,] B ) )
Theorem	lbico1 9943	The lower bound belongs to a closed-below, open-above interval. See lbicc2 9997. (Contributed by FL, 29-May-2014.)
|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> A e. ( A [,) B ) )
Theorem	iccleub 9944	An element of a closed interval is less than or equal to its upper bound. (Contributed by Jeff Hankins, 14-Jul-2009.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. ( A [,] B ) ) -> C <_ B )
Theorem	iccgelb 9945	An element of a closed interval is more than or equal to its lower bound (Contributed by Thierry Arnoux, 23-Dec-2016.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. ( A [,] B ) ) -> A <_ C )
Theorem	elioo5 9946	Membership in an open interval of extended reals. (Contributed by NM, 17-Aug-2008.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( C e. ( A (,) B ) <-> ( A < C /\ C < B ) ) )
Theorem	elioo4g 9947	Membership in an open interval of extended reals. (Contributed by NM, 8-Jun-2007.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( C e. ( A (,) B ) <-> ( ( A e. RR* /\ B e. RR* /\ C e. RR ) /\ ( A < C /\ C < B ) ) )
Theorem	ioossre 9948	An open interval is a set of reals. (Contributed by NM, 31-May-2007.)
|- ( A (,) B ) C_ RR
Theorem	elioc2 9949	Membership in an open-below, closed-above real interval. (Contributed by Paul Chapman, 30-Dec-2007.) (Revised by Mario Carneiro, 14-Jun-2014.)
|- ( ( A e. RR* /\ B e. RR ) -> ( C e. ( A (,] B ) <-> ( C e. RR /\ A < C /\ C <_ B ) ) )
Theorem	elico2 9950	Membership in a closed-below, open-above real interval. (Contributed by Paul Chapman, 21-Jan-2008.) (Revised by Mario Carneiro, 14-Jun-2014.)
|- ( ( A e. RR /\ B e. RR* ) -> ( C e. ( A [,) B ) <-> ( C e. RR /\ A <_ C /\ C < B ) ) )
Theorem	elicc2 9951	Membership in a closed real interval. (Contributed by Paul Chapman, 21-Sep-2007.) (Revised by Mario Carneiro, 14-Jun-2014.)
|- ( ( A e. RR /\ B e. RR ) -> ( C e. ( A [,] B ) <-> ( C e. RR /\ A <_ C /\ C <_ B ) ) )
Theorem	elicc2i 9952	Inference for membership in a closed interval. (Contributed by Scott Fenton, 3-Jun-2013.)
|- A e. RR   &    |- B e. RR   =>    |- ( C e. ( A [,] B ) <-> ( C e. RR /\ A <_ C /\ C <_ B ) )
Theorem	elicc4 9953	Membership in a closed real interval. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Proof shortened by Mario Carneiro, 1-Jan-2017.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( C e. ( A [,] B ) <-> ( A <_ C /\ C <_ B ) ) )
Theorem	iccss 9954	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.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( A <_ C /\ D <_ B ) ) -> ( C [,] D ) C_ ( A [,] B ) )
Theorem	iccssioo 9955	Condition for a closed interval to be a subset of an open interval. (Contributed by Mario Carneiro, 20-Feb-2015.)
|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( A < C /\ D < B ) ) -> ( C [,] D ) C_ ( A (,) B ) )
Theorem	icossico 9956	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.)
|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( A <_ C /\ D <_ B ) ) -> ( C [,) D ) C_ ( A [,) B ) )
Theorem	iccss2 9957	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.)
|- ( ( C e. ( A [,] B ) /\ D e. ( A [,] B ) ) -> ( C [,] D ) C_ ( A [,] B ) )
Theorem	iccssico 9958	Condition for a closed interval to be a subset of a half-open interval. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( A <_ C /\ D < B ) ) -> ( C [,] D ) C_ ( A [,) B ) )
Theorem	iccssioo2 9959	Condition for a closed interval to be a subset of an open interval. (Contributed by Mario Carneiro, 20-Feb-2015.)
|- ( ( C e. ( A (,) B ) /\ D e. ( A (,) B ) ) -> ( C [,] D ) C_ ( A (,) B ) )
Theorem	iccssico2 9960	Condition for a closed interval to be a subset of a closed-below, open-above interval. (Contributed by Mario Carneiro, 20-Feb-2015.)
|- ( ( C e. ( A [,) B ) /\ D e. ( A [,) B ) ) -> ( C [,] D ) C_ ( A [,) B ) )
Theorem	ioomax 9961	The open interval from minus to plus infinity. (Contributed by NM, 6-Feb-2007.)
|- ( -oo (,) +oo ) = RR
Theorem	iccmax 9962	The closed interval from minus to plus infinity. (Contributed by Mario Carneiro, 4-Jul-2014.)
|- ( -oo [,] +oo ) = RR*
Theorem	ioopos 9963	The set of positive reals expressed as an open interval. (Contributed by NM, 7-May-2007.)
|- ( 0 (,) +oo ) = { x e. RR | 0 < x }
Theorem	ioorp 9964	The set of positive reals expressed as an open interval. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( 0 (,) +oo ) = RR+
Theorem	iooshf 9965	Shift the arguments of the open interval function. (Contributed by NM, 17-Aug-2008.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A - B ) e. ( C (,) D ) <-> A e. ( ( C + B ) (,) ( D + B ) ) ) )
Theorem	iocssre 9966	A closed-above interval with real upper bound is a set of reals. (Contributed by FL, 29-May-2014.)
|- ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) C_ RR )
Theorem	icossre 9967	A closed-below interval with real lower bound is a set of reals. (Contributed by Mario Carneiro, 14-Jun-2014.)
|- ( ( A e. RR /\ B e. RR* ) -> ( A [,) B ) C_ RR )
Theorem	iccssre 9968	A closed real interval is a set of reals. (Contributed by FL, 6-Jun-2007.) (Proof shortened by Paul Chapman, 21-Jan-2008.)
|- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
Theorem	iccssxr 9969	A closed interval is a set of extended reals. (Contributed by FL, 28-Jul-2008.) (Revised by Mario Carneiro, 4-Jul-2014.)
|- ( A [,] B ) C_ RR*
Theorem	iocssxr 9970	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.)
|- ( A (,] B ) C_ RR*
Theorem	icossxr 9971	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.)
|- ( A [,) B ) C_ RR*
Theorem	ioossicc 9972	An open interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.)
|- ( A (,) B ) C_ ( A [,] B )
Theorem	icossicc 9973	A closed-below, open-above interval is a subset of its closure. (Contributed by Thierry Arnoux, 25-Oct-2016.)
|- ( A [,) B ) C_ ( A [,] B )
Theorem	iocssicc 9974	A closed-above, open-below interval is a subset of its closure. (Contributed by Thierry Arnoux, 1-Apr-2017.)
|- ( A (,] B ) C_ ( A [,] B )
Theorem	ioossico 9975	An open interval is a subset of its closure-below. (Contributed by Thierry Arnoux, 3-Mar-2017.)
|- ( A (,) B ) C_ ( A [,) B )
Theorem	iocssioo 9976	Condition for a closed interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 29-Mar-2017.)
|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( A <_ C /\ D < B ) ) -> ( C (,] D ) C_ ( A (,) B ) )
Theorem	icossioo 9977	Condition for a closed interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 29-Mar-2017.)
|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( A < C /\ D <_ B ) ) -> ( C [,) D ) C_ ( A (,) B ) )
Theorem	ioossioo 9978	Condition for an open interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 26-Sep-2017.)
|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( A <_ C /\ D <_ B ) ) -> ( C (,) D ) C_ ( A (,) B ) )
Theorem	iccsupr 9979*	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.)
|- ( ( ( A e. RR /\ B e. RR ) /\ S C_ ( A [,] B ) /\ C e. S ) -> ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. y e. S y <_ x ) )
Theorem	elioopnf 9980	Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014.)
|- ( A e. RR* -> ( B e. ( A (,) +oo ) <-> ( B e. RR /\ A < B ) ) )
Theorem	elioomnf 9981	Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014.)
|- ( A e. RR* -> ( B e. ( -oo (,) A ) <-> ( B e. RR /\ B < A ) ) )
Theorem	elicopnf 9982	Membership in a closed unbounded interval of reals. (Contributed by Mario Carneiro, 16-Sep-2014.)
|- ( A e. RR -> ( B e. ( A [,) +oo ) <-> ( B e. RR /\ A <_ B ) ) )
Theorem	repos 9983	Two ways of saying that a real number is positive. (Contributed by NM, 7-May-2007.)
|- ( A e. ( 0 (,) +oo ) <-> ( A e. RR /\ 0 < A ) )
Theorem	ioof 9984	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.)
|- (,) : ( RR* X. RR* ) --> ~P RR
Theorem	iccf 9985	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.)
|- [,] : ( RR* X. RR* ) --> ~P RR*
Theorem	unirnioo 9986	The union of the range of the open interval function. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 30-Jan-2014.)
|- RR = U. ran (,)
Theorem	dfioo2 9987*	Alternate definition of the set of open intervals of extended reals. (Contributed by NM, 1-Mar-2007.) (Revised by Mario Carneiro, 1-Sep-2015.)
|- (,) = ( x e. RR* , y e. RR* |-> { w e. RR | ( x < w /\ w < y ) } )
Theorem	ioorebasg 9988	Open intervals are elements of the set of all open intervals. (Contributed by Jim Kingdon, 4-Apr-2020.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A (,) B ) e. ran (,) )
Theorem	elrege0 9989	The predicate "is a nonnegative real". (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 18-Jun-2014.)
|- ( A e. ( 0 [,) +oo ) <-> ( A e. RR /\ 0 <_ A ) )
Theorem	rge0ssre 9990	Nonnegative real numbers are real numbers. (Contributed by Thierry Arnoux, 9-Sep-2018.) (Proof shortened by AV, 8-Sep-2019.)
|- ( 0 [,) +oo ) C_ RR
Theorem	elxrge0 9991	Elementhood in the set of nonnegative extended reals. (Contributed by Mario Carneiro, 28-Jun-2014.)
|- ( A e. ( 0 [,] +oo ) <-> ( A e. RR* /\ 0 <_ A ) )
Theorem	0e0icopnf 9992	0 is a member of ( 0 [,) +oo ) (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 0 e. ( 0 [,) +oo )
Theorem	0e0iccpnf 9993	0 is a member of ( 0 [,] +oo ) (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 0 e. ( 0 [,] +oo )
Theorem	ge0addcl 9994	The nonnegative reals are closed under addition. (Contributed by Mario Carneiro, 19-Jun-2014.)
|- ( ( A e. ( 0 [,) +oo ) /\ B e. ( 0 [,) +oo ) ) -> ( A + B ) e. ( 0 [,) +oo ) )
Theorem	ge0mulcl 9995	The nonnegative reals are closed under multiplication. (Contributed by Mario Carneiro, 19-Jun-2014.)
|- ( ( A e. ( 0 [,) +oo ) /\ B e. ( 0 [,) +oo ) ) -> ( A x. B ) e. ( 0 [,) +oo ) )
Theorem	ge0xaddcl 9996	The nonnegative reals are closed under addition. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) -> ( A +e B ) e. ( 0 [,] +oo ) )
Theorem	lbicc2 9997	The lower bound of a closed interval is a member of it. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by FL, 29-May-2014.) (Revised by Mario Carneiro, 9-Sep-2015.)
|- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
Theorem	ubicc2 9998	The upper bound of a closed interval is a member of it. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by FL, 29-May-2014.)
|- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
Theorem	0elunit 9999	Zero is an element of the closed unit. (Contributed by Scott Fenton, 11-Jun-2013.)
|- 0 e. ( 0 [,] 1 )
Theorem	1elunit 10000	One is an element of the closed unit. (Contributed by Scott Fenton, 11-Jun-2013.)
|- 1 e. ( 0 [,] 1 )