P. 398 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39701-39800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	supminfxrrnmpt 39701*	The indexed supremum of a set of reals is the negation of the indexed infimum of that set's image under negation. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B e. RR* )   =>    |- ( ph -> sup ( ran ( x e. A |-> B ) , RR* , < ) = -einf ( ran ( x e. A |-> -e B ) , RR* , < ) )
Theorem	min1d 39702	The minimum of two numbers is less than or equal to the first. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> if ( A <_ B , A , B ) <_ A )
Theorem	min2d 39703	The minimum of two numbers is less than or equal to the second. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> if ( A <_ B , A , B ) <_ B )
Theorem	pnfged 39704	Plus infinity is an upper bound for extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
|- ( ph -> A e. RR* )   =>    |- ( ph -> A <_ +oo )
Theorem	xrnpnfmnf 39705	An extended real that is neither real nor plus infinity, is minus infinity. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
|- ( ph -> A e. RR* )   &    |- ( ph -> -. A e. RR )   &    |- ( ph -> A =/= +oo )   =>    |- ( ph -> A = -oo )
Theorem	uzsscn 39706	An upper set of integers is a subset of the complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
|- ( ZZ>= ` M ) C_ CC
Theorem	absimnre 39707	The absolute value of the imaginary part of a non real, complex number, is strictly positive. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
|- ( ph -> A e. CC )   &    |- ( ph -> -. A e. RR )   =>    |- ( ph -> ( abs ` ( Im ` A ) ) e. RR+ )
Theorem	uzsscn2 39708	An upper set of integers is a subset of the complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
|- Z = ( ZZ>= ` M )   =>    |- Z C_ CC
Theorem	xrtgcntopre 39709	The standard topologies on the extended reals and on the complex numbers, coincide when restricted to the reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
|- ( (ordTop ` <_ ) ↾t RR ) = ( ( TopOpen ` ℂfld ) ↾t RR )
Theorem	absimlere 39710	The absolute value of the imaginary part of a complex number is a lower bound of the distance to any real number. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( abs ` ( Im ` A ) ) <_ ( abs ` ( B - A ) ) )
Theorem	rpssxr 39711	The positive reals are a subset of the extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
|- RR+ C_ RR*
20.32.4  Real intervals
Theorem	gtnelioc 39712	A real number larger than the upper bound of a left open right closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> B < C )   =>    |- ( ph -> -. C e. ( A (,] B ) )
Theorem	ioossioc 39713	An open interval is a subset of its right closure. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A (,) B ) C_ ( A (,] B )
Theorem	ioondisj2 39714	A condition for two open intervals not to be disjoint. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A < D /\ D <_ B ) ) -> ( ( A (,) B ) i^i ( C (,) D ) ) =/= (/) )
Theorem	ioondisj1 39715	A condition for two open intervals not to be disjoint. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> ( ( A (,) B ) i^i ( C (,) D ) ) =/= (/) )
Theorem	ioosscn 39716	An open interval is a set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A (,) B ) C_ CC
Theorem	ioogtlb 39717	An element of a closed interval is greater than its lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. ( A (,) B ) ) -> A < C )
Theorem	evthiccabs 39718*	Extreme Value Theorem on y closed interval, for the absolute value of y continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )   =>    |- ( ph -> ( E. x e. ( A [,] B ) A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ ( abs ` ( F ` x ) ) /\ E. z e. ( A [,] B ) A. w e. ( A [,] B ) ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` w ) ) ) )
Theorem	ltnelicc 39719	A real number smaller than the lower bound of a closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> C < A )   =>    |- ( ph -> -. C e. ( A [,] B ) )
Theorem	eliood 39720	Membership in an open real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A < C )   &    |- ( ph -> C < B )   =>    |- ( ph -> C e. ( A (,) B ) )
Theorem	iooabslt 39721	An upper bound for the distance from the center of an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. ( ( A - B ) (,) ( A + B ) ) )   =>    |- ( ph -> ( abs ` ( A - C ) ) < B )
Theorem	gtnelicc 39722	A real number greater than the upper bound of a closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> B < C )   =>    |- ( ph -> -. C e. ( A [,] B ) )
Theorem	iooinlbub 39723	An open interval has empty intersection with its bounds. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A (,) B ) i^i { A , B } ) = (/)
Theorem	iocgtlb 39724	An element of a left open right closed interval is larger than its lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. ( A (,] B ) ) -> A < C )
Theorem	iocleub 39725	An element of a left open right closed interval is smaller or equal to its upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. ( A (,] B ) ) -> C <_ B )
Theorem	eliccd 39726	Membership in a closed real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A <_ C )   &    |- ( ph -> C <_ B )   =>    |- ( ph -> C e. ( A [,] B ) )
Theorem	iccssred 39727	A closed real interval is a set of reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A [,] B ) C_ RR )
Theorem	eliccre 39728	A member of a closed interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. RR /\ B e. RR /\ C e. ( A [,] B ) ) -> C e. RR )
Theorem	eliooshift 39729	Element of an open interval shifted by a displacement. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   =>    |- ( ph -> ( A e. ( B (,) C ) <-> ( A + D ) e. ( ( B + D ) (,) ( C + D ) ) ) )
Theorem	eliocd 39730	Membership in a left open, right closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> A < C )   &    |- ( ph -> C <_ B )   =>    |- ( ph -> C e. ( A (,] B ) )
Theorem	snunioo2 39731	The closure of one end of an open real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( A (,) B ) u. { B } ) = ( A (,] B ) )
Theorem	icoltub 39732	An element of a left closed right open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. ( A [,) B ) ) -> C < B )
Theorem	tgiooss 39733	The restriction of the complex topology to a subset of reals, is a restriction of the standard topology on reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) TODO (NM): Use rerest 22607 instead in fourierdlem48 40371, fourierdlem49 40372, fourierdlem62 40385 then delete this.
|- J = ( TopOpen ` ℂfld )   &    |- K = ( topGen ` ran (,) )   =>    |- ( A C_ RR -> ( J ↾t A ) = ( K ↾t A ) )
Theorem	eliocre 39734	A member of a left open, right closed interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( B e. RR /\ C e. ( A (,] B ) ) -> C e. RR )
Theorem	iooltub 39735	An element of an open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. ( A (,) B ) ) -> C < B )
Theorem	ioontr 39736	The interior of an interval in the standard topology on RR is the open interval itself. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B )
Theorem	eliccxr 39737	A member of a closed interval is a an extended real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. ( B [,] C ) -> A e. RR* )
Theorem	snunioo1 39738	The closure of one end of an open real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( A (,) B ) u. { A } ) = ( A [,) B ) )
Theorem	lbioc 39739	An left open right closed interval doesn't contain its left endpoint. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- -. A e. ( A (,] B )
Theorem	ioomidp 39740	The midpoint is an element of the open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( ( A + B ) / 2 ) e. ( A (,) B ) )
Theorem	iccdifioo 39741	If the open inverval is removed from the closed interval, only the bounds are left. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( ( A [,] B ) \ ( A (,) B ) ) = { A , B } )
Theorem	iccdifprioo 39742	An open interval is the closed interval without the bounds. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( ( A [,] B ) \ { A , B } ) = ( A (,) B ) )
Theorem	ioossioobi 39743	Biconditional form of ioossioo 12265. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> D e. RR* )   &    |- ( ph -> C < D )   =>    |- ( ph -> ( ( C (,) D ) C_ ( A (,) B ) <-> ( A <_ C /\ D <_ B ) ) )
Theorem	iccshift 39744*	A closed interval shifted by a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> T e. RR )   =>    |- ( ph -> ( ( A + T ) [,] ( B + T ) ) = { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } )
Theorem	iccsuble 39745	An upper bound to the distance of two elements in a closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. ( A [,] B ) )   &    |- ( ph -> D e. ( A [,] B ) )   =>    |- ( ph -> ( C - D ) <_ ( B - A ) )
Theorem	iocopn 39746	A left open right closed interval is an open set of the standard topology restricted to an interval that contains the original interval and has the same upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR* )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> B e. RR )   &    |- K = ( topGen ` ran (,) )   &    |- J = ( K ↾t ( A (,] B ) )   &    |- ( ph -> A <_ C )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( C (,] B ) e. J )
Theorem	eliccelioc 39747	Membership in a closed interval and in a left open right closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR* )   =>    |- ( ph -> ( C e. ( A (,] B ) <-> ( C e. ( A [,] B ) /\ C =/= A ) ) )
Theorem	iooshift 39748*	An open interval shifted by a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> T e. RR )   =>    |- ( ph -> ( ( A + T ) (,) ( B + T ) ) = { w e. CC | E. z e. ( A (,) B ) w = ( z + T ) } )
Theorem	iccintsng 39749	Intersection of two adiacent closed intervals is a singleton. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A <_ B /\ B <_ C ) ) -> ( ( A [,] B ) i^i ( B [,] C ) ) = { B } )
Theorem	icoiccdif 39750	Left closed, right open interval gotten by a closed iterval taking away the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A [,) B ) = ( ( A [,] B ) \ { B } ) )
Theorem	icoopn 39751	A left closed right open interval is an open set of the standard topology restricted to an interval that contains the original interval and has the same lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> B e. RR* )   &    |- K = ( topGen ` ran (,) )   &    |- J = ( K ↾t ( A [,) B ) )   &    |- ( ph -> C <_ B )   =>    |- ( ph -> ( A [,) C ) e. J )
Theorem	icoub 39752	A left-closed, right-open interval does not contain its upper bound. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( A e. RR* -> -. B e. ( A [,) B ) )
Theorem	eliccxrd 39753	Membership in a closed real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> A <_ C )   &    |- ( ph -> C <_ B )   =>    |- ( ph -> C e. ( A [,] B ) )
Theorem	pnfel0pnf 39754	+oo is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- +oo e. ( 0 [,] +oo )
Theorem	ge0nemnf2 39755	A nonnegative extended real is not -oo (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( A e. ( 0 [,] +oo ) -> A =/= -oo )
Theorem	eliccnelico 39756	An element of a closed interval that is not a member of the left closed right open interval, must be the upper bound. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. ( A [,] B ) )   &    |- ( ph -> -. C e. ( A [,) B ) )   =>    |- ( ph -> C = B )
Theorem	eliccelicod 39757	A member of a closed interval that is not the upper bound, is a member of the left-closed, right-open interval. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. ( A [,] B ) )   &    |- ( ph -> C =/= B )   =>    |- ( ph -> C e. ( A [,) B ) )
Theorem	ge0xrre 39758	A nonnegative extended real that is not +oo is a real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ( A e. ( 0 [,] +oo ) /\ A =/= +oo ) -> A e. RR )
Theorem	ge0lere 39759	A nonnegative extended Real number smaller than or equal to a Real number, is a Real number. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. ( 0 [,] +oo ) )   &    |- ( ph -> B <_ A )   =>    |- ( ph -> B e. RR )
Theorem	elicores 39760*	Membership in a left-closed, right-open interval with real bounds. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( A e. ran ( [,) |` ( RR X. RR ) ) <-> E. x e. RR E. y e. RR A = ( x [,) y ) )
Theorem	inficc 39761	The infimum of a nonempty set, included in a closed interval, is a member of the interval. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> S C_ ( A [,] B ) )   &    |- ( ph -> S =/= (/) )   =>    |- ( ph -> inf ( S , RR* , < ) e. ( A [,] B ) )
Theorem	qinioo 39762	The rational numbers are dense in RR. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   =>    |- ( ph -> ( ( QQ i^i ( A (,) B ) ) = (/) <-> B <_ A ) )
Theorem	lenelioc 39763	A real number smaller than or equal to the lower bound of a left open right closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> C <_ A )   =>    |- ( ph -> -. C e. ( A (,] B ) )
Theorem	ioonct 39764	C non empty open interval is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> A < B )   &    |- C = ( A (,) B )   =>    |- ( ph -> -. C ~<_ om )
Theorem	xrgtnelicc 39765	A real number greater than the upper bound of a closed interval is not an element of the interval. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> B < C )   =>    |- ( ph -> -. C e. ( A [,] B ) )
Theorem	iccdificc 39766	The difference of two closed intervals with the same lower bound. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( ( A [,] C ) \ ( A [,] B ) ) = ( B (,] C ) )
Theorem	iocnct 39767	A non empty left-open, right-closed interval is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> A < B )   &    |- C = ( A (,] B )   =>    |- ( ph -> -. C ~<_ om )
Theorem	iccnct 39768	A closed interval, with more than one element is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> A < B )   &    |- C = ( A [,] B )   =>    |- ( ph -> -. C ~<_ om )
Theorem	iooiinicc 39769*	A closed interval expressed as the indexed intersection of open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> |^|_ n e. NN ( ( A - ( 1 / n ) ) (,) ( B + ( 1 / n ) ) ) = ( A [,] B ) )
Theorem	iccgelbd 39770	An element of a closed interval is more than or equal to its lower bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. ( A [,] B ) )   =>    |- ( ph -> A <_ C )
Theorem	iooltubd 39771	An element of an open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. ( A (,) B ) )   =>    |- ( ph -> C < B )
Theorem	icoltubd 39772	An element of a left closed right open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. ( A [,) B ) )   =>    |- ( ph -> C < B )
Theorem	qelioo 39773*	The rational numbers are dense in RR*: any two extended real numbers have a rational between them. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> A < B )   =>    |- ( ph -> E. x e. QQ x e. ( A (,) B ) )
Theorem	tgqioo2 39774*	Every open set of reals is the (countable) union of open interval with rational bounds. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- J = ( topGen ` ran (,) )   &    |- ( ph -> A e. J )   =>    |- ( ph -> E. q ( q C_ ( (,) " ( QQ X. QQ ) ) /\ A = U. q ) )
Theorem	iccleubd 39775	An element of a closed interval is less than or equal to its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. ( A [,] B ) )   =>    |- ( ph -> C <_ B )
Theorem	elioored 39776	A member of an open interval of reals is a real. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. ( B (,) C ) )   =>    |- ( ph -> A e. RR )
Theorem	ioogtlbd 39777	An element of a closed interval is greater than its lower bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. ( A (,) B ) )   =>    |- ( ph -> A < C )
Theorem	ioofun 39778	(,) is a function. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- Fun (,)
Theorem	icomnfinre 39779	A left-closed, right-open, interval of extended reals, intersected with the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. RR* )   =>    |- ( ph -> ( ( -oo [,) A ) i^i RR ) = ( -oo (,) A ) )
Theorem	sqrlearg 39780	The square compared with its argument. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( ( A ^ 2 ) <_ A <-> A e. ( 0 [,] 1 ) ) )
Theorem	ressiocsup 39781	If the supremum belongs to a set of reals, the set is a subset of the unbounded below, right-closed interval, with upper bound equal to the supremum. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A C_ RR )   &    |- S = sup ( A , RR* , < )   &    |- ( ph -> S e. A )   &    |- I = ( -oo (,] S )   =>    |- ( ph -> A C_ I )
Theorem	ressioosup 39782	If the supremum does not belong to a set of reals, the set is a subset of the unbounded below, right-open interval, with upper bound equal to the supremum. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A C_ RR )   &    |- S = sup ( A , RR* , < )   &    |- ( ph -> -. S e. A )   &    |- I = ( -oo (,) S )   =>    |- ( ph -> A C_ I )
Theorem	iooiinioc 39783*	A left-open, right-closed interval expressed as the indexed intersection of open intervals. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> |^|_ n e. NN ( A (,) ( B + ( 1 / n ) ) ) = ( A (,] B ) )
Theorem	ressiooinf 39784	If the infimum does not belong to a set of reals, the set is a subset of the unbounded above, left-open interval, with lower bound equal to the infimum. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A C_ RR )   &    |- S = inf ( A , RR* , < )   &    |- ( ph -> -. S e. A )   &    |- I = ( S (,) +oo )   =>    |- ( ph -> A C_ I )
Theorem	icogelbd 39785	An element of a left closed right open interval is larger or equal to its lower bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. ( A [,) B ) )   =>    |- ( ph -> A <_ C )
Theorem	iocleubd 39786	An element of a left open right closed interval is smaller or equal to its upper bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. ( A (,] B ) )   =>    |- ( ph -> C <_ B )
Theorem	uzinico 39787	An upper interval of integers is the intersection of the integers with an upper part of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   =>    |- ( ph -> Z = ( ZZ i^i ( M [,) +oo ) ) )
Theorem	preimaiocmnf 39788*	Preimage of a right-closed interval, unbounded below. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> F : A --> RR )   &    |- ( ph -> B e. RR* )   =>    |- ( ph -> ( `' F " ( -oo (,] B ) ) = { x e. A | ( F ` x ) <_ B } )
Theorem	uzinico2 39789	An upper interval of integers is the intersection of a larger upper interval of integers with an upper part of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> N e. ( ZZ>= ` M ) )   =>    |- ( ph -> ( ZZ>= ` N ) = ( ( ZZ>= ` M ) i^i ( N [,) +oo ) ) )
Theorem	uzinico3 39790	An upper interval of integers doesn't change when it's intersected with a left-closed, unbounded above interval, with the same lower bound. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   =>    |- ( ph -> Z = ( Z i^i ( M [,) +oo ) ) )
Theorem	icossico2 39791	Condition for a closed-below, open-above interval to be a subset of a closed-below, open-above interval. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> B e. RR* )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> B <_ A )   =>    |- ( ph -> ( A [,) C ) C_ ( B [,) C ) )
Theorem	dmico 39792	The domain of the closed-below, open-above interval function. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- dom [,) = ( RR* X. RR* )
Theorem	ndmico 39793	The closed-below, open-above interval function's value is empty outside of its domain. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( -. ( A e. RR* /\ B e. RR* ) -> ( A [,) B ) = (/) )
Theorem	uzubioo 39794*	The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> X e. RR )   =>    |- ( ph -> E. k e. ( X (,) +oo ) k e. Z )
Theorem	uzubico 39795*	The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> X e. RR )   =>    |- ( ph -> E. k e. ( X [,) +oo ) k e. Z )
Theorem	uzubioo2 39796*	The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   =>    |- ( ph -> A. x e. RR E. k e. ( x (,) +oo ) k e. Z )
Theorem	uzubico2 39797*	The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   =>    |- ( ph -> A. x e. RR E. k e. ( x [,) +oo ) k e. Z )
Theorem	iocgtlbd 39798	An element of a left open right closed interval is larger than its lower bound. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. ( A (,] B ) )   =>    |- ( ph -> A < C )
Theorem	xrtgioo2 39799	The topology on the extended reals coincides with the standard topology on the reals, when restricted to RR. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
|- ( topGen ` ran (,) ) = ( (ordTop ` <_ ) ↾t RR )
Theorem	tgioo4 39800	The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
|- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )