P. 104 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 10301-10400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	xposdif 10301	Extended real version of posdif 8790. (Contributed by Mario Carneiro, 24-Aug-2015.) (Revised by Jim Kingdon, 17-Apr-2023.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A < B <-> 0 < ( B +e -e A ) ) )
Theorem	xlesubadd 10302	Under certain conditions, the conclusion of lesubadd 8769 is true even in the extended reals. (Contributed by Mario Carneiro, 4-Sep-2015.)
|- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) -> ( ( A +e -e B ) <_ C <-> A <_ ( C +e B ) ) )
Theorem	xaddcld 10303	The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   =>    |- ( ph -> ( A +e B ) e. RR* )
Theorem	xadd4d 10304	Rearrangement of 4 terms in a sum for extended addition, analogous to add4d 8502. (Contributed by Alexander van der Vekens, 21-Dec-2017.)
|- ( ph -> ( A e. RR* /\ A =/= -oo ) )   &    |- ( ph -> ( B e. RR* /\ B =/= -oo ) )   &    |- ( ph -> ( C e. RR* /\ C =/= -oo ) )   &    |- ( ph -> ( D e. RR* /\ D =/= -oo ) )   =>    |- ( ph -> ( ( A +e B ) +e ( C +e D ) ) = ( ( A +e C ) +e ( B +e D ) ) )
Theorem	xnn0add4d 10305	Rearrangement of 4 terms in a sum for extended addition of extended nonnegative integers, analogous to xadd4d 10304. (Contributed by AV, 12-Dec-2020.)
|- ( ph -> A e. NN0* )   &    |- ( ph -> B e. NN0* )   &    |- ( ph -> C e. NN0* )   &    |- ( ph -> D e. NN0* )   =>    |- ( ph -> ( ( A +e B ) +e ( C +e D ) ) = ( ( A +e C ) +e ( B +e D ) ) )
Theorem	xleaddadd 10306	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.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B <-> ( A +e A ) <_ ( B +e B ) ) )
4.5.3  Real number intervals
Syntax	cioo 10307	Extend class notation with the set of open intervals of extended reals.
class (,)
Syntax	cioc 10308	Extend class notation with the set of open-below, closed-above intervals of extended reals.
class (,]
Syntax	cico 10309	Extend class notation with the set of closed-below, open-above intervals of extended reals.
class [,)
Syntax	cicc 10310	Extend class notation with the set of closed intervals of extended reals.
class [,]
Definition	df-ioo 10311*	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 10312*	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 10313*	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 10314*	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 10315*	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 10316*	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 10317*	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 10318*	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 10319*	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 10320*	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 10321*	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 10322*	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 10323*	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 10324*	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 10325*	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 10326	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 10327*	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 10328	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 10329	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 10330	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 10331	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 10332	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 10333	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 10334*	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 10335	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 10336	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 10337*	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 10338*	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 10339*	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 10340	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 10341	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 10342	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 10343	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 10344	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 10345	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 10346	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 10347	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 10348	The upper bound belongs to an open-below, closed-above interval. See ubicc2 10404. (Contributed by FL, 29-May-2014.)
|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> B e. ( A (,] B ) )
Theorem	lbico1 10349	The lower bound belongs to a closed-below, open-above interval. See lbicc2 10403. (Contributed by FL, 29-May-2014.)
|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> A e. ( A [,) B ) )
Theorem	iccleub 10350	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 10351	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 10352	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 10353	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 10354	An open interval is a set of reals. (Contributed by NM, 31-May-2007.)
|- ( A (,) B ) C_ RR
Theorem	elioc2 10355	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 10356	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 10357	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 10358	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 10359	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 10360	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 10361	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 10362	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 10363	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 10364	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 10365	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 10366	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 10367	The open interval from minus to plus infinity. (Contributed by NM, 6-Feb-2007.)
|- ( -oo (,) +oo ) = RR
Theorem	iccmax 10368	The closed interval from minus to plus infinity. (Contributed by Mario Carneiro, 4-Jul-2014.)
|- ( -oo [,] +oo ) = RR*
Theorem	ioopos 10369	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 10370	The set of positive reals expressed as an open interval. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( 0 (,) +oo ) = RR+
Theorem	iooshf 10371	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 10372	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 10373	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 10374	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 10375	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 10376	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 10377	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 10378	An open interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.)
|- ( A (,) B ) C_ ( A [,] B )
Theorem	icossicc 10379	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 10380	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 10381	An open interval is a subset of its closure-below. (Contributed by Thierry Arnoux, 3-Mar-2017.)
|- ( A (,) B ) C_ ( A [,) B )
Theorem	iocssioo 10382	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 10383	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 10384	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 10385*	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 10386	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 10387	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 10388	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 10389	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 10390	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 10391	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 10392	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 10393*	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 10394	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 10395	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 10396	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 10397	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 10398	0 is a member of ( 0 [,) +oo ) (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 0 e. ( 0 [,) +oo )
Theorem	0e0iccpnf 10399	0 is a member of ( 0 [,] +oo ) (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 0 e. ( 0 [,] +oo )
Theorem	ge0addcl 10400	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 ) )