P. 376 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37501-37600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	xaddcomd 37501	The extended real addition operation is commutative. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   =>    |- ( ph -> ( A +e B ) = ( B +e A ) )
Theorem	supxrre3 37502*	The supremum of a nonempty set of reals, is real if and only if it is bounded-above . (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ( A C_ RR /\ A =/= (/) ) -> ( sup ( A , RR* , < ) e. RR <-> E. x e. RR A. y e. A y <_ x ) )
Theorem	uzfissfz 37503*	For any finite subset of the upper integers, there is a finite set of sequential integers that includes it. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> A C_ Z )   &    |- ( ph -> A e. Fin )   =>    |- ( ph -> E. k e. Z A C_ ( M ... k ) )
Theorem	xleadd2d 37504	Addition of extended reals preserves the "less than or equal" relation, in the right slot (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( C +e A ) <_ ( C +e B ) )
Theorem	suprltrp 37505*	The supremum of a nonempty bounded set of reals can be approximated from below by elements of the set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A C_ RR )   &    |- ( ph -> A =/= (/) )   &    |- ( ph -> E. x e. RR A. y e. A y <_ x )   &    |- ( ph -> X e. RR+ )   =>    |- ( ph -> E. z e. A ( sup ( A , RR , < ) - X ) < z )
Theorem	xleadd1d 37506	Addition of extended reals preserves the "less than or equal" relation, in the left slot (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( A +e C ) <_ ( B +e C ) )
Theorem	xreqled 37507	Equality implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. RR* )   &    |- ( ph -> A = B )   =>    |- ( ph -> A <_ B )
Theorem	xrgepnfd 37508	An extended real greater or equal to +oo is +oo (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. RR* )   &    |- ( ph -> +oo <_ A )   =>    |- ( ph -> A = +oo )
Theorem	xrge0nemnfd 37509	A nonnegative extended real is not minus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. ( 0 [,] +oo ) )   =>    |- ( ph -> A =/= -oo )
Theorem	supxrgere 37510*	If a real number can be approximated from below by members of a set, then it is smaller or equal to the supremum of the set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ x ph   &    |- ( ph -> A C_ RR* )   &    |- ( ph -> B e. RR )   &    |- ( ( ph /\ x e. RR+ ) -> E. y e. A ( B - x ) < y )   =>    |- ( ph -> B <_ sup ( A , RR* , < ) )
Theorem	iuneqfzuzlem 37511*	Lemma for iuneqfzuz 37512: here, inclusion is proven; aiuneqfzuz uses this lemma twice, to prove equality. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- Z = ( ZZ>= ` N )   =>    |- ( A. m e. Z U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B -> U_ n e. Z A C_ U_ n e. Z B )
Theorem	iuneqfzuz 37512*	If two unions indexed by upper integers are equal if they agree on any partial indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- Z = ( ZZ>= ` N )   =>    |- ( A. m e. Z U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B -> U_ n e. Z A = U_ n e. Z B )
Theorem	xle2addd 37513	Adding both side of two inequalities. (Contributed by Glauco Siliprandi, 17-Aug-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 +e B ) <_ ( C +e D ) )
Theorem	supxrgelem 37514*	If an extended real number can be approximated from below by members of a set, then it is smaller or equal to the supremum of the set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ x ph   &    |- ( ph -> A C_ RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ( ph /\ x e. RR+ ) -> E. y e. A B < ( y +e x ) )   =>    |- ( ph -> B <_ sup ( A , RR* , < ) )
Theorem	supxrge 37515*	If an extended real number can be approximated from below by members of a set, then it is smaller or equal to the supremum of the set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ x ph   &    |- ( ph -> A C_ RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ( ph /\ x e. RR+ ) -> E. y e. A B <_ ( y +e x ) )   =>    |- ( ph -> B <_ sup ( A , RR* , < ) )
Theorem	suplesup 37516*	If any element of A can be approximated from below by members of B, then the supremum of A is smaller or equal to the supremum of B. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A C_ RR )   &    |- ( ph -> B C_ RR* )   &    |- ( ph -> A. x e. A A. y e. RR+ E. z e. B ( x - y ) < z )   =>    |- ( ph -> sup ( A , RR* , < ) <_ sup ( B , RR* , < ) )
Theorem	infxrglb 37517*	The infimum of a set of extended reals is less than an extended real if and only if the set contains a smaller number. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ( A C_ RR* /\ B e. RR* ) -> (inf ( A , RR* , < ) < B <-> E. x e. A x < B ) )
Theorem	xadd0ge2 37518	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 37519	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 37520	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 37521	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 37522	'Greater than' is a strict ordering on the extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- `' < Or RR*
Theorem	rpex 37523	The positive reals form a set. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- RR+ e. _V
Theorem	xrge0ge0 37524	A nonnegative extended real is nonnegative. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( A e. ( 0 [,] +oo ) -> 0 <_ A )
Theorem	xrssre 37525	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 37526	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 37527	The absolute value is a function. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- Fun abs
Theorem	infrpge 37528*	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 37529*	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 37530*	The supremum function distributes over subtraction in a sense similar to that in supaddc 10581. (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 37531*	Show that A is less than B by showing that there is no positive bound on the difference. A variant on xralrple 11505. (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 37532	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 37533	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 37534	'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 37535	Express the set of positive integers as the disjoint (see nnuzdisj 37532) 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 ) ) ) )
21.30.4  Real intervals
Theorem	gtnelioc 37536	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 37537	An open interval is a subset of its right closure. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A (,) B ) C_ ( A (,] B )
Theorem	ioondisj2 37538	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 37539	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 37540	An open interval is a set of complex numbers (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A (,) B ) C_ CC
Theorem	ioogtlb 37541	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 37542*	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 37543	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 37544	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 37545	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 37546	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 37547	An open interval has empty intersection with its bounds (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A (,) B ) i^i { A , B } ) = (/)
Theorem	iocgtlb 37548	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 37549	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 37550	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 37551	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 37552	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 37553	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 37554	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 37555	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 37556	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 37557	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 21820 instead in fourierdlem48 37958, fourierdlem49 37959, fourierdlem62 37972 then delete this.
|- J = ( TopOpen ` ℂfld )   &    |- K = ( topGen ` ran (,) )   =>    |- ( A C_ RR -> ( J ↾t A ) = ( K ↾t A ) )
Theorem	eliocre 37558	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 37559	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 37560	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 37561	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 37562	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 37563	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 37564	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 37565	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 37566	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 37567	Biconditional form of ioossioo 11733 (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 37568*	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 37569	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 37570	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 37571	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 37572*	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 37573	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 37574	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 37575	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 37576	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 37577	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 37578	+oo is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- +oo e. ( 0 [,] +oo )
Theorem	ge0nemnf2 37579	A nonnegative extended real is not -oo (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( A e. ( 0 [,] +oo ) -> A =/= -oo )
Theorem	eliccnelico 37580	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 37581	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 37582	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	elicores 37583*	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 37584	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 ) )
21.30.5  Finite sums
Theorem	sumeq2ad 37585*	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 37586*	Closure of a finite sum of complex numbers A ( k ). A version of fsumcl 13798 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 37587*	Split a sum into two parts. A version of fsumsplit 13805 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 37588*	Closure of a finite sum of complex numbers A ( k ). A version of fsummulc1 13845 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 37589*	A sum of a singleton is the term. A version of sumsn 13806 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 37590*	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 37591*	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 37592*	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 37593*	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 37594*	Re-index a finite sum using a bijection. Same as fsumf1o 13788, 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 37595*	Sum over a disjoint indexed union, intersected with a finite set D. Similar to fsumiun 13880, 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 37596*	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 37597*	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 )
21.30.6  Finite multiplication of numbers and finite multiplication of functions
Theorem	fmul01 37598*	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 37599*	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 37600*	induction step for the proof of fmuldfeq 37601. (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 ) ) )