P. 377 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37601-37700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	xadd0ge2 37601	A number is less than or equal to itself plus a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. ( 0 [,] +oo ) )   =>    |- ( ph -> A <_ ( B +e A ) )
Theorem	nepnfltpnf 37602	An extended real that is not +oo is less than +oo. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> A =/= +oo )   &    |- ( ph -> A e. RR* )   =>    |- ( ph -> A < +oo )
Theorem	ltadd12dd 37603	Addition to both sides of 'less than'. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A < C )   &    |- ( ph -> B < D )   =>    |- ( ph -> ( A + B ) < ( C + D ) )
Theorem	nemnftgtmnft 37604	An extended real that is not minus infinity, is larger than minus infinity. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ( A e. RR* /\ A =/= -oo ) -> -oo < A )
Theorem	xrgtso 37605	'Greater than' is a strict ordering on the extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- `' < Or RR*
Theorem	rpex 37606	The positive reals form a set. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- RR+ e. _V
Theorem	xrge0ge0 37607	A nonnegative extended real is nonnegative. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( A e. ( 0 [,] +oo ) -> 0 <_ A )
Theorem	xrssre 37608	A subset of extended reals that does not contain +oo and -oo is a subset of the reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> A C_ RR* )   &    |- ( ph -> -. +oo e. A )   &    |- ( ph -> -. -oo e. A )   =>    |- ( ph -> A C_ RR )
Theorem	ssuzfz 37609	A finite subset of the upper integers is a subset of a finite set of sequential integers. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> A C_ Z )   &    |- ( ph -> A e. Fin )   =>    |- ( ph -> A C_ ( M ... sup ( A , RR , < ) ) )
Theorem	absfun 37610	The absolute value is a function. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- Fun abs
Theorem	infrpge 37611*	The infimum of a non empty, bounded subset of extended reals can be approximated from above by an element of the set. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- F/ x ph   &    |- ( ph -> A C_ RR* )   &    |- ( ph -> A =/= (/) )   &    |- ( ph -> E. x e. RR A. y e. A x <_ y )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> E. z e. A z <_ (inf ( A , RR* , < ) +e B ) )
Theorem	xrlexaddrp 37612*	If an extended real number A can be approximated from above, adding positive reals to B, then A is smaller or equal than B. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ( ph /\ x e. RR+ ) -> A <_ ( B +e x ) )   =>    |- ( ph -> A <_ B )
Theorem	supsubc 37613*	The supremum function distributes over subtraction in a sense similar to that in supaddc 10601. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( ph -> A C_ RR )   &    |- ( ph -> A =/= (/) )   &    |- ( ph -> E. x e. RR A. y e. A y <_ x )   &    |- ( ph -> B e. RR )   &    |- C = { z | E. v e. A z = ( v - B ) }   =>    |- ( ph -> ( sup ( A , RR , < ) - B ) = sup ( C , RR , < ) )
Theorem	xralrple2 37614*	Show that A is less than B by showing that there is no positive bound on the difference. A variant on xralrple 11526. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- F/ x ph   &    |- ( ph -> A e. RR* )   &    |- ( ph -> B e. ( 0 [,) +oo ) )   =>    |- ( ph -> ( A <_ B <-> A. x e. RR+ A <_ ( ( 1 + x ) x. B ) ) )
Theorem	nnuzdisj 37615	The first N elements of the set of nonnegative integers are distinct from any later members. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( ( 1 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/)
Theorem	ltdivgt1 37616	Divsion by a number greater than 1. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( 1 < B <-> ( A / B ) < A ) )
Theorem	xrltned 37617	'Less than' implies not equal. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> A < B )   =>    |- ( ph -> A =/= B )
Theorem	nnsplit 37618	Express the set of positive integers as the disjoint (see nnuzdisj 37615) union of the first N values and the rest. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( N e. NN -> NN = ( ( 1 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
Theorem	divdiv3d 37619	Division into a fraction. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> C =/= 0 )   =>    |- ( ph -> ( ( A / B ) / C ) = ( A / ( C x. B ) ) )
Theorem	abslt2sqd 37620	Comparison of the square of two numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( abs ` A ) < ( abs ` B ) )   =>    |- ( ph -> ( A ^ 2 ) < ( B ^ 2 ) )
Theorem	rexaddd 37621	The extended real addition operation when both arguments are real. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A +e B ) = ( A + B ) )
Theorem	qenom 37622	The set of rational numbers is equinumerous to omega (the set of finite ordinal numbers). (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- QQ ~~ om
Theorem	qct 37623	The set of rational numbers is countable. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- QQ ~<_ om
21.30.4  Real intervals
Theorem	gtnelioc 37624	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 37625	An open interval is a subset of its right closure. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A (,) B ) C_ ( A (,] B )
Theorem	ioondisj2 37626	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 37627	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 37628	An open interval is a set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A (,) B ) C_ CC
Theorem	ioogtlb 37629	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 37630*	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 37631	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 37632	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 37633	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 37634	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 37635	An open interval has empty intersection with its bounds. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A (,) B ) i^i { A , B } ) = (/)
Theorem	iocgtlb 37636	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 37637	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 37638	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 37639	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 37640	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 37641	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 37642	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 37643	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 37644	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 37645	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 21870 instead in fourierdlem48 38055, fourierdlem49 38056, fourierdlem62 38069 then delete this.
|- J = ( TopOpen ` ℂfld )   &    |- K = ( topGen ` ran (,) )   =>    |- ( A C_ RR -> ( J ↾t A ) = ( K ↾t A ) )
Theorem	eliocre 37646	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 37647	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 37648	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 37649	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 37650	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 37651	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 37652	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 37653	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 37654	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 37655	Biconditional form of ioossioo 11754. (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 37656*	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 37657	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 37658	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 37659	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 37660*	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 37661	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 37662	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 37663	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 37664	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 37665	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 37666	+oo is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- +oo e. ( 0 [,] +oo )
Theorem	ge0nemnf2 37667	A nonnegative extended real is not -oo (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( A e. ( 0 [,] +oo ) -> A =/= -oo )
Theorem	eliccnelico 37668	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 37669	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 37670	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 37671	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 37672*	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 37673	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 37674	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 37675	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 37676	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 37677	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 37678	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 37679	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 37680	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 )
21.30.5  Finite sums
Theorem	sumeq2ad 37681*	Equality deduction for sum. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> B = C )   =>    |- ( ph -> sum_ k e. A B = sum_ k e. A C )
Theorem	fsumclf 37682*	Closure of a finite sum of complex numbers A ( k ). A version of fsumcl 13847 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> sum_ k e. A B e. CC )
Theorem	fsumsplitf 37683*	Split a sum into two parts. A version of fsumsplit 13854 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- ( ph -> ( A i^i B ) = (/) )   &    |- ( ph -> U = ( A u. B ) )   &    |- ( ph -> U e. Fin )   &    |- ( ( ph /\ k e. U ) -> C e. CC )   =>    |- ( ph -> sum_ k e. U C = ( sum_ k e. A C + sum_ k e. B C ) )
Theorem	fsummulc1f 37684*	Closure of a finite sum of complex numbers A ( k ). A version of fsummulc1 13894 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ph -> C e. CC )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> ( sum_ k e. A B x. C ) = sum_ k e. A ( B x. C ) )
Theorem	sumsnf 37685*	A sum of a singleton is the term. A version of sumsn 13855 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/_ k B   &    |- ( k = M -> A = B )   =>    |- ( ( M e. V /\ B e. CC ) -> sum_ k e. { M } A = B )
Theorem	fsumsplitsn 37686*	Separate out a term in a finite sum. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- F/_ k D   &    |- ( ph -> A e. Fin )   &    |- ( ph -> B e. V )   &    |- ( ph -> -. B e. A )   &    |- ( ( ph /\ k e. A ) -> C e. CC )   &    |- ( k = B -> C = D )   &    |- ( ph -> D e. CC )   =>    |- ( ph -> sum_ k e. ( A u. { B } ) C = ( sum_ k e. A C + D ) )
Theorem	fsumnncl 37687*	Closure of a non empty, finite sum of positive integers. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> A =/= (/) )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. NN )   =>    |- ( ph -> sum_ k e. A B e. NN )
Theorem	fsumsplit1 37688*	Separate out a term in a finite sum. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- F/_ k D   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ph -> C e. A )   &    |- ( k = C -> B = D )   =>    |- ( ph -> sum_ k e. A B = ( D + sum_ k e. ( A \ { C } ) B ) )
Theorem	fsumge0cl 37689*	The finite sum of nonnegative reals is a nonnegative real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,) +oo ) )   =>    |- ( ph -> sum_ k e. A B e. ( 0 [,) +oo ) )
Theorem	fsumf1of 37690*	Re-index a finite sum using a bijection. Same as fsumf1o 13837, but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ k ph   &    |- F/ n ph   &    |- ( k = G -> B = D )   &    |- ( ph -> C e. Fin )   &    |- ( ph -> F : C -1-1-onto-> A )   &    |- ( ( ph /\ n e. C ) -> ( F ` n ) = G )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> sum_ k e. A B = sum_ n e. C D )
Theorem	fsumiunss 37691*	Sum over a disjoint indexed union, intersected with a finite set D. Similar to fsumiun 13929, but here A and B need not be finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> Disj x e. A B )   &    |- ( ( ph /\ x e. A /\ k e. B ) -> C e. CC )   &    |- ( ph -> D e. Fin )   =>    |- ( ph -> sum_ k e. U_ x e. A ( B i^i D ) C = sum_ x e. { x e. A | ( B i^i D ) =/= (/) } sum_ k e. ( B i^i D ) C )
Theorem	fsumreclf 37692*	Closure of a finite sum of reals. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. RR )   =>    |- ( ph -> sum_ k e. A B e. RR )
Theorem	fsumlessf 37693*	A shorter sum of nonnegative terms is smaller than a longer one. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. RR )   &    |- ( ( ph /\ k e. A ) -> 0 <_ B )   &    |- ( ph -> C C_ A )   =>    |- ( ph -> sum_ k e. C B <_ sum_ k e. A B )
Theorem	fsumsupp0 37694*	Finite sum of function values, for a function of finite support. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> A e. Fin )   &    |- ( ph -> F : A --> CC )   =>    |- ( ph -> sum_ k e. ( F supp 0 ) ( F ` k ) = sum_ k e. A ( F ` k ) )
21.30.6  Finite multiplication of numbers and finite multiplication of functions
Theorem	fmul01 37695*	Multiplying a finite number of values in [ 0 , 1 ] , gives the final product itself a number in [ 0 , 1 ]. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ i B   &    |- F/ i ph   &    |- A = seq L ( x. , B )   &    |- ( ph -> L e. ZZ )   &    |- ( ph -> M e. ( ZZ>= ` L ) )   &    |- ( ph -> K e. ( L ... M ) )   &    |- ( ( ph /\ i e. ( L ... M ) ) -> ( B ` i ) e. RR )   &    |- ( ( ph /\ i e. ( L ... M ) ) -> 0 <_ ( B ` i ) )   &    |- ( ( ph /\ i e. ( L ... M ) ) -> ( B ` i ) <_ 1 )   =>    |- ( ph -> ( 0 <_ ( A ` K ) /\ ( A ` K ) <_ 1 ) )
Theorem	fmulcl 37696*	If ' Y ' is closed under the multiplication of two functions, then Y is closed under the multiplication ( ' X ' ) of a finite number of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- P = ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) )   &    |- X = ( seq 1 ( P , U ) ` N )   &    |- ( ph -> N e. ( 1 ... M ) )   &    |- ( ph -> U : ( 1 ... M ) --> Y )   &    |- ( ( ph /\ f e. Y /\ g e. Y ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. Y )   &    |- ( ph -> T e. _V )   =>    |- ( ph -> X e. Y )
Theorem	fmuldfeqlem1 37697*	induction step for the proof of fmuldfeq 37698. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/ f ph   &    |- F/ g ph   &    |- F/_ t Y   &    |- P = ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) )   &    |- F = ( t e. T |-> ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) )   &    |- ( ph -> T e. _V )   &    |- ( ph -> U : ( 1 ... M ) --> Y )   &    |- ( ( ph /\ f e. Y /\ g e. Y ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. Y )   &    |- ( ph -> N e. ( 1 ... M ) )   &    |- ( ph -> ( N + 1 ) e. ( 1 ... M ) )   &    |- ( ph -> ( ( seq 1 ( P , U ) ` N ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` N ) )   &    |- ( ( ph /\ f e. Y ) -> f : T --> RR )   =>    |- ( ( ph /\ t e. T ) -> ( ( seq 1 ( P , U ) ` ( N + 1 ) ) ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` ( N + 1 ) ) )
Theorem	fmuldfeq 37698*	X and Z are two equivalent definitions of the finite product of real functions. Y is a set of real functions from a common domain T, Y is closed under function multiplication and U is a finite sequence of functions in Y. M is the number of functions multiplied together. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/ i ph   &    |- F/_ t Y   &    |- P = ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) )   &    |- X = ( seq 1 ( P , U ) ` M )   &    |- F = ( t e. T |-> ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) )   &    |- Z = ( t e. T |-> ( seq 1 ( x. , ( F ` t ) ) ` M ) )   &    |- ( ph -> T e. _V )   &    |- ( ph -> M e. NN )   &    |- ( ph -> U : ( 1 ... M ) --> Y )   &    |- ( ( ph /\ f e. Y ) -> f : T --> RR )   &    |- ( ( ph /\ f e. Y /\ g e. Y ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. Y )   =>    |- ( ( ph /\ t e. T ) -> ( X ` t ) = ( Z ` t ) )
Theorem	fmul01lt1lem1 37699*	Given a finite multiplication of values betweeen 0 and 1, a value larger than its frist element is larger the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ i B   &    |- F/ i ph   &    |- A = seq L ( x. , B )   &    |- ( ph -> L e. ZZ )   &    |- ( ph -> M e. ( ZZ>= ` L ) )   &    |- ( ( ph /\ i e. ( L ... M ) ) -> ( B ` i ) e. RR )   &    |- ( ( ph /\ i e. ( L ... M ) ) -> 0 <_ ( B ` i ) )   &    |- ( ( ph /\ i e. ( L ... M ) ) -> ( B ` i ) <_ 1 )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> ( B ` L ) < E )   =>    |- ( ph -> ( A ` M ) < E )
Theorem	fmul01lt1lem2 37700*	Given a finite multiplication of values betweeen 0 and 1, a value E larger than any multiplicand, is larger than the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ i B   &    |- F/ i ph   &    |- A = seq L ( x. , B )   &    |- ( ph -> L e. ZZ )   &    |- ( ph -> M e. ( ZZ>= ` L ) )   &    |- ( ( ph /\ i e. ( L ... M ) ) -> ( B ` i ) e. RR )   &    |- ( ( ph /\ i e. ( L ... M ) ) -> 0 <_ ( B ` i ) )   &    |- ( ( ph /\ i e. ( L ... M ) ) -> ( B ` i ) <_ 1 )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> J e. ( L ... M ) )   &    |- ( ph -> ( B ` J ) < E )   =>    |- ( ph -> ( A ` M ) < E )