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	xlesubadd 10301	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 10302	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 10303	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 10304	Rearrangement of 4 terms in a sum for extended addition of extended nonnegative integers, analogous to xadd4d 10303. (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 10305	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 10306	Extend class notation with the set of open intervals of extended reals.
class (,)
Syntax	cioc 10307	Extend class notation with the set of open-below, closed-above intervals of extended reals.
class (,]
Syntax	cico 10308	Extend class notation with the set of closed-below, open-above intervals of extended reals.
class [,)
Syntax	cicc 10309	Extend class notation with the set of closed intervals of extended reals.
class [,]
Definition	df-ioo 10310*	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 10311*	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 10312*	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 10313*	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 10314*	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 10315*	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 10316*	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 10317*	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 10318*	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 10319*	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 10320*	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 10321*	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 10322*	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 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 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 10324*	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 10325	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 10326*	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 10327	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 10328	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 10329	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 10330	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 10331	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 10332	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 10333*	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 10334	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 10335	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 10336*	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 10337*	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 10338*	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 10339	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 10340	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 10341	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 10342	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 10343	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 10344	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 10345	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 10346	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 10347	The upper bound belongs to an open-below, closed-above interval. See ubicc2 10403. (Contributed by FL, 29-May-2014.)
|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> B e. ( A (,] B ) )
Theorem	lbico1 10348	The lower bound belongs to a closed-below, open-above interval. See lbicc2 10402. (Contributed by FL, 29-May-2014.)
|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> A e. ( A [,) B ) )
Theorem	iccleub 10349	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 10350	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 10351	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 10352	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 10353	An open interval is a set of reals. (Contributed by NM, 31-May-2007.)
|- ( A (,) B ) C_ RR
Theorem	elioc2 10354	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 10355	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 10356	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 10357	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 10358	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 10359	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 10360	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 10361	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 10362	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 10363	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 10364	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 10365	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 10366	The open interval from minus to plus infinity. (Contributed by NM, 6-Feb-2007.)
|- ( -oo (,) +oo ) = RR
Theorem	iccmax 10367	The closed interval from minus to plus infinity. (Contributed by Mario Carneiro, 4-Jul-2014.)
|- ( -oo [,] +oo ) = RR*
Theorem	ioopos 10368	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 10369	The set of positive reals expressed as an open interval. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( 0 (,) +oo ) = RR+
Theorem	iooshf 10370	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 10371	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 10372	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 10373	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 10374	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 10375	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 10376	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 10377	An open interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.)
|- ( A (,) B ) C_ ( A [,] B )
Theorem	icossicc 10378	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 10379	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 10380	An open interval is a subset of its closure-below. (Contributed by Thierry Arnoux, 3-Mar-2017.)
|- ( A (,) B ) C_ ( A [,) B )
Theorem	iocssioo 10381	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 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	ioossioo 10383	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 10384*	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 10385	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 10386	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 10387	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 10388	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 10389	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 10390	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 10391	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 10392*	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 10393	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 10394	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 10395	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 10396	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 10397	0 is a member of ( 0 [,) +oo ) (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 0 e. ( 0 [,) +oo )
Theorem	0e0iccpnf 10398	0 is a member of ( 0 [,] +oo ) (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 0 e. ( 0 [,] +oo )
Theorem	ge0addcl 10399	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 10400	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 ) )