P. 102 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 10101-10200   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-ioc 10101*	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 10102*	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 10103*	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 10104*	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 10105*	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 10106*	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 10107*	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 10108*	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 10109*	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 10110*	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 10111*	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 10112*	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 10113*	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 10114*	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 10115	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 10116*	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 10117	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 10118	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 10119	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 10120	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 10121	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 10122	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 10123*	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 10124	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 10125	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 10126*	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 10127*	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 10128*	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 10129	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 10130	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 10131	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 10132	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 10133	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 10134	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 10135	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 10136	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 10137	The upper bound belongs to an open-below, closed-above interval. See ubicc2 10193. (Contributed by FL, 29-May-2014.)
|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> B e. ( A (,] B ) )
Theorem	lbico1 10138	The lower bound belongs to a closed-below, open-above interval. See lbicc2 10192. (Contributed by FL, 29-May-2014.)
|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> A e. ( A [,) B ) )
Theorem	iccleub 10139	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 10140	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 10141	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 10142	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 10143	An open interval is a set of reals. (Contributed by NM, 31-May-2007.)
|- ( A (,) B ) C_ RR
Theorem	elioc2 10144	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 10145	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 10146	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 10147	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 10148	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 10149	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 10150	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 10151	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 10152	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 10153	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 10154	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 10155	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 10156	The open interval from minus to plus infinity. (Contributed by NM, 6-Feb-2007.)
|- ( -oo (,) +oo ) = RR
Theorem	iccmax 10157	The closed interval from minus to plus infinity. (Contributed by Mario Carneiro, 4-Jul-2014.)
|- ( -oo [,] +oo ) = RR*
Theorem	ioopos 10158	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 10159	The set of positive reals expressed as an open interval. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( 0 (,) +oo ) = RR+
Theorem	iooshf 10160	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 10161	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 10162	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 10163	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 10164	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 10165	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 10166	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 10167	An open interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.)
|- ( A (,) B ) C_ ( A [,] B )
Theorem	icossicc 10168	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 10169	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 10170	An open interval is a subset of its closure-below. (Contributed by Thierry Arnoux, 3-Mar-2017.)
|- ( A (,) B ) C_ ( A [,) B )
Theorem	iocssioo 10171	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 10172	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 10173	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 10174*	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 10175	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 10176	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 10177	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 10178	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 10179	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 10180	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 10181	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 10182*	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 10183	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 10184	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 10185	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 10186	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 10187	0 is a member of ( 0 [,) +oo ) (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 0 e. ( 0 [,) +oo )
Theorem	0e0iccpnf 10188	0 is a member of ( 0 [,] +oo ) (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 0 e. ( 0 [,] +oo )
Theorem	ge0addcl 10189	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 10190	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 10191	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 10192	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 10193	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 10194	Zero is an element of the closed unit. (Contributed by Scott Fenton, 11-Jun-2013.)
|- 0 e. ( 0 [,] 1 )
Theorem	1elunit 10195	One is an element of the closed unit. (Contributed by Scott Fenton, 11-Jun-2013.)
|- 1 e. ( 0 [,] 1 )
Theorem	iooneg 10196	Membership in a negated open real interval. (Contributed by Paul Chapman, 26-Nov-2007.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C e. ( A (,) B ) <-> -u C e. ( -u B (,) -u A ) ) )
Theorem	iccneg 10197	Membership in a negated closed real interval. (Contributed by Paul Chapman, 26-Nov-2007.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C e. ( A [,] B ) <-> -u C e. ( -u B [,] -u A ) ) )
Theorem	icoshft 10198	A shifted real is a member of a shifted, closed-below, open-above real interval. (Contributed by Paul Chapman, 25-Mar-2008.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( X e. ( A [,) B ) -> ( X + C ) e. ( ( A + C ) [,) ( B + C ) ) ) )
Theorem	icoshftf1o 10199*	Shifting a closed-below, open-above interval is one-to-one onto. (Contributed by Paul Chapman, 25-Mar-2008.) (Proof shortened by Mario Carneiro, 1-Sep-2015.)
|- F = ( x e. ( A [,) B ) |-> ( x + C ) )   =>    |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> F : ( A [,) B ) -1-1-onto-> ( ( A + C ) [,) ( B + C ) ) )
Theorem	icodisj 10200	End-to-end closed-below, open-above real intervals are disjoint. (Contributed by Mario Carneiro, 16-Jun-2014.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A [,) B ) i^i ( B [,) C ) ) = (/) )