P. 373 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37201-37300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	iccdifprioo 37201	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 37202	Biconditional form of ioossioo 11726 (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 37203*	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 37204	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 37205	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 37206	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 37207*	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 37208	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 37209	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 37210	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 37211	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 37212	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 37213	+oo is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- +oo e. ( 0 [,] +oo )
Theorem	ge0nemnf2 37214	A nonnegative extended real is not -oo (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( A e. ( 0 [,] +oo ) -> A =/= -oo )
Theorem	eliccnelico 37215	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 37216	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 37217	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 )
21.30.5  Finite sums
Theorem	sumeq2ad 37218*	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 37219*	Closure of a finite sum of complex numbers A ( k ). A version of fsumcl 13777 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 37220*	Split a sum into two parts. A version of fsumsplit 13784 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 37221*	Closure of a finite sum of complex numbers A ( k ). A version of fsummulc1 13824 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 37222*	A sum of a singleton is the term. A version of sumsn 13785 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 37223*	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 37224*	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 37225*	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 37226*	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 37227*	Re-index a finite sum using a bijection. Same as fsumf1o 13767, 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 37228*	Sum over a disjoint indexed union, intersected with a finite set D. Similar to fsumiun 13859, 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 )
21.30.6  Finite multiplication of numbers and finite multiplication of functions
Theorem	fmul01 37229*	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 37230*	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 37231*	induction step for the proof of fmuldfeq 37232. (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 37232*	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 37233*	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 37234*	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 )
Theorem	fmul01lt1 37235*	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   &    |- F/_ j A   &    |- A = seq 1 ( x. , B )   &    |- ( ph -> M e. NN )   &    |- ( ph -> B : ( 1 ... M ) --> RR )   &    |- ( ( ph /\ i e. ( 1 ... M ) ) -> 0 <_ ( B ` i ) )   &    |- ( ( ph /\ i e. ( 1 ... M ) ) -> ( B ` i ) <_ 1 )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> E. j e. ( 1 ... M ) ( B ` j ) < E )   =>    |- ( ph -> ( A ` M ) < E )
Theorem	cncfmptss 37236*	A continuous complex function restricted to a subset is continuous, using "map to" notation. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- F/_ x F   &    |- ( ph -> F e. ( A -cn-> B ) )   &    |- ( ph -> C C_ A )   =>    |- ( ph -> ( x e. C |-> ( F ` x ) ) e. ( C -cn-> B ) )
Theorem	rrpsscn 37237	The positive reals are a subset of the complex numbers. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- RR+ C_ CC
Theorem	mulc1cncfg 37238*	A version of mulc1cncf 21833 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 30-Jun-2017.)
|- F/_ x F   &    |- F/ x ph   &    |- ( ph -> F e. ( A -cn-> CC ) )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( x e. A |-> ( B x. ( F ` x ) ) ) e. ( A -cn-> CC ) )
Theorem	infrglb 37239*	The infimum of a nonempty bounded set of reals is the greatest lower bound. (Contributed by Glauco Siliprandi, 29-Jun-2017.) (Revised by AV, 15-Sep-2020.)
|- ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) /\ B e. RR ) -> (inf ( A , RR , < ) < B <-> E. z e. A z < B ) )
Theorem	infrglbOLD 37240*	The infimum of a nonempty bounded set of reals is the greatest lower bound. (Contributed by Glauco Siliprandi, 29-Jun-2017.) Obsolete version of infrglb 37239 as of 15-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) /\ B e. RR ) -> ( sup ( A , RR , `' < ) < B <-> E. z e. A z < B ) )
Theorem	m1expevenOLD 37241	Obsolete as of 18-Jul-2020. Use more general m1expeven 12316 instead. Exponentiation of negative one to an even power. (Contributed by Glauco Siliprandi, 29-Jun-2017.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( N e. NN0 -> ( -u 1 ^ ( 2 x. N ) ) = 1 )
Theorem	expcnfg 37242*	If F is a complex continuous function and N is a fixed number, then F^N is continuous too. A generalization of expcncf 21850. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- F/_ x F   &    |- ( ph -> F e. ( A -cn-> CC ) )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( x e. A |-> ( ( F ` x ) ^ N ) ) e. ( A -cn-> CC ) )
Theorem	prodeq2ad 37243*	Equality deduction for product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> B = C )   =>    |- ( ph -> prod_ k e. A B = prod_ k e. A C )
Theorem	fprodsplit1 37244*	Separate out a term in a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ph -> C e. A )   &    |- ( ( ph /\ k = C ) -> B = D )   =>    |- ( ph -> prod_ k e. A B = ( D x. prod_ k e. ( A \ { C } ) B ) )
Theorem	fprodexp 37245*	Positive integer exponentiation of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> prod_ k e. A ( B ^ N ) = ( prod_ k e. A B ^ N ) )
Theorem	fprodabs2 37246*	The absolute value of a finite product . (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> ( abs ` prod_ k e. A B ) = prod_ k e. A ( abs ` B ) )
Theorem	fprod0 37247*	A finite product with a zero term is zero. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- F/_ k C   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( k = K -> B = C )   &    |- ( ph -> K e. A )   &    |- ( ph -> C = 0 )   =>    |- ( ph -> prod_ k e. A B = 0 )
Theorem	mccllem 37248*	* Induction step for mccl 37249. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> A e. Fin )   &    |- ( ph -> C C_ A )   &    |- ( ph -> D e. ( A \ C ) )   &    |- ( ph -> B e. ( NN0 ^m ( C u. { D } ) ) )   &    |- ( ph -> A. b e. ( NN0 ^m C ) ( ( ! ` sum_ k e. C ( b ` k ) ) / prod_ k e. C ( ! ` ( b ` k ) ) ) e. NN )   =>    |- ( ph -> ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / prod_ k e. ( C u. { D } ) ( ! ` ( B ` k ) ) ) e. NN )
Theorem	mccl 37249*	A multinomial coefficient, in its standard domain, is a positive integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/_ k B   &    |- ( ph -> A e. Fin )   &    |- ( ph -> B e. ( NN0 ^m A ) )   =>    |- ( ph -> ( ( ! ` sum_ k e. A ( B ` k ) ) / prod_ k e. A ( ! ` ( B ` k ) ) ) e. NN )
21.30.7  Limits
Theorem	clim1fr1 37250*	A class of sequences of fractions that converge to 1 (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- F = ( n e. NN |-> ( ( ( A x. n ) + B ) / ( A x. n ) ) )   &    |- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> F ~~> 1 )
Theorem	isumneg 37251*	Negation of a converging sum. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> sum_ k e. Z A e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ( ph /\ k e. Z ) -> A e. CC )   &    |- ( ph -> seq M ( + , F ) e. dom ~~> )   =>    |- ( ph -> sum_ k e. Z -u A = -u sum_ k e. Z A )
Theorem	climrec 37252*	Limit of the reciprocal of a converging sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> G ~~> A )   &    |- ( ph -> A =/= 0 )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. ( CC \ { 0 } ) )   &    |- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( 1 / ( G ` k ) ) )   &    |- ( ph -> H e. W )   =>    |- ( ph -> H ~~> ( 1 / A ) )
Theorem	climmulf 37253*	A version of climmul 13674 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- F/ k ph   &    |- F/_ k F   &    |- F/_ k G   &    |- F/_ k H   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> H e. X )   &    |- ( ph -> G ~~> B )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) x. ( G ` k ) ) )   =>    |- ( ph -> H ~~> ( A x. B ) )
Theorem	climexp 37254*	The limit of natural powers, is the natural power of the limit. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- F/ k ph   &    |- F/_ k F   &    |- F/_ k H   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F : Z --> CC )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> H e. V )   &    |- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) ^ N ) )   =>    |- ( ph -> H ~~> ( A ^ N ) )
Theorem	climinf 37255*	A bounded monotonic non increasing sequence converges to the infimum of its range. (Contributed by Glauco Siliprandi, 29-Jun-2017.) (Revised by AV, 15-Sep-2020.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F : Z --> RR )   &    |- ( ( ph /\ k e. Z ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )   &    |- ( ph -> E. x e. RR A. k e. Z x <_ ( F ` k ) )   =>    |- ( ph -> F ~~> inf ( ran F , RR , < ) )
Theorem	climinfOLD 37256*	A bounded monotonic non increasing sequence converges to the infimum of its range. (Contributed by Glauco Siliprandi, 29-Jun-2017.) Obsolete version of climinf 37255 as of 15-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F : Z --> RR )   &    |- ( ( ph /\ k e. Z ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )   &    |- ( ph -> E. x e. RR A. k e. Z x <_ ( F ` k ) )   =>    |- ( ph -> F ~~> sup ( ran F , RR , `' < ) )
Theorem	climsuselem1 37257*	The subsequence index I has the expected properties: it belongs to the same upper integers as the original index, and it is always larger or equal than the original index. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> ( I ` M ) e. Z )   &    |- ( ( ph /\ k e. Z ) -> ( I ` ( k + 1 ) ) e. ( ZZ>= ` ( ( I ` k ) + 1 ) ) )   =>    |- ( ( ph /\ K e. Z ) -> ( I ` K ) e. ( ZZ>= ` K ) )
Theorem	climsuse 37258*	A subsequence G of a converging sequence F, converges to the same limit. I is the strictly increasing and it is used to index the subsequence (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- F/ k ph   &    |- F/_ k F   &    |- F/_ k G   &    |- F/_ k I   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F e. X )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> ( I ` M ) e. Z )   &    |- ( ( ph /\ k e. Z ) -> ( I ` ( k + 1 ) ) e. ( ZZ>= ` ( ( I ` k ) + 1 ) ) )   &    |- ( ph -> G e. Y )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( F ` ( I ` k ) ) )   =>    |- ( ph -> G ~~> A )
Theorem	climrecf 37259*	A version of climrec 37252 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- F/ k ph   &    |- F/_ k G   &    |- F/_ k H   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> G ~~> A )   &    |- ( ph -> A =/= 0 )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. ( CC \ { 0 } ) )   &    |- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( 1 / ( G ` k ) ) )   &    |- ( ph -> H e. W )   =>    |- ( ph -> H ~~> ( 1 / A ) )
Theorem	climneg 37260*	Complex limit of the negative of a sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- F/ k ph   &    |- F/_ k F   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   =>    |- ( ph -> ( k e. Z |-> -u ( F ` k ) ) ~~> -u A )
Theorem	climinff 37261*	A version of climinf 37255 using bound-variable hypotheses instead of distinct variable conditions (Contributed by Glauco Siliprandi, 29-Jun-2017.) (Revised by AV, 15-Sep-2020.)
|- F/ k ph   &    |- F/_ k F   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F : Z --> RR )   &    |- ( ( ph /\ k e. Z ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )   &    |- ( ph -> E. x e. RR A. k e. Z x <_ ( F ` k ) )   =>    |- ( ph -> F ~~> inf ( ran F , RR , < ) )
Theorem	climinffOLD 37262*	A version of climinf 37255 using bound-variable hypotheses instead of distinct variable conditions (Contributed by Glauco Siliprandi, 29-Jun-2017.) Obsolete version of climinf 37255 as of 15-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- F/ k ph   &    |- F/_ k F   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F : Z --> RR )   &    |- ( ( ph /\ k e. Z ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )   &    |- ( ph -> E. x e. RR A. k e. Z x <_ ( F ` k ) )   =>    |- ( ph -> F ~~> sup ( ran F , RR , `' < ) )
Theorem	climdivf 37263*	Limit of the ratio of two converging sequences. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- F/ k ph   &    |- F/_ k F   &    |- F/_ k G   &    |- F/_ k H   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> H e. X )   &    |- ( ph -> G ~~> B )   &    |- ( ph -> B =/= 0 )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. ( CC \ { 0 } ) )   &    |- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) / ( G ` k ) ) )   =>    |- ( ph -> H ~~> ( A / B ) )
Theorem	climreeq 37264	If F is a real function, then F converges to A with respect to the standard topology on the reals if and only if it converges to A with respect to the standard topology on complex numbers. In the theorem, R is defined to be convergence w.r.t. the standard topology on the reals and then F R A represents the statement " F converges to A, with respect to the standard topology on the reals". Notice that there is no need for the hypothesis that A is a real number. (Contributed by Glauco Siliprandi, 2-Jul-2017.)
|- R = ( ~~> t ` ( topGen ` ran (,) ) )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F : Z --> RR )   =>    |- ( ph -> ( F R A <-> F ~~> A ) )
Theorem	ellimciota 37265*	An explicit value for the limit, when the limit exists at a limit point. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> B e. ( ( limPt ` K ) ` A ) )   &    |- ( ph -> ( F lim CC B ) =/= (/) )   &    |- K = ( TopOpen ` ℂfld )   =>    |- ( ph -> ( iota x x e. ( F lim CC B ) ) e. ( F lim CC B ) )
Theorem	climaddf 37266*	A version of climadd 13673 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F/ k ph   &    |- F/_ k F   &    |- F/_ k G   &    |- F/_ k H   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> H e. X )   &    |- ( ph -> G ~~> B )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) + ( G ` k ) ) )   =>    |- ( ph -> H ~~> ( A + B ) )
Theorem	mullimc 37267*	Limit of the product of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F = ( x e. A |-> B )   &    |- G = ( x e. A |-> C )   &    |- H = ( x e. A |-> ( B x. C ) )   &    |- ( ( ph /\ x e. A ) -> B e. CC )   &    |- ( ( ph /\ x e. A ) -> C e. CC )   &    |- ( ph -> X e. ( F lim CC D ) )   &    |- ( ph -> Y e. ( G lim CC D ) )   =>    |- ( ph -> ( X x. Y ) e. ( H lim CC D ) )
Theorem	ellimcabssub0 37268*	An equivalent condition for being a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F = ( x e. A |-> B )   &    |- G = ( x e. A |-> ( B - C ) )   &    |- ( ph -> A C_ CC )   &    |- ( ( ph /\ x e. A ) -> B e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( C e. ( F lim CC D ) <-> 0 e. ( G lim CC D ) ) )
Theorem	limcdm0 37269	If a function has empty domain, every complex number is a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : (/) --> CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( F lim CC B ) = CC )
Theorem	islptre 37270*	An equivalence condition for a limit point w.r.t. the standard topology on the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- J = ( topGen ` ran (,) )   &    |- ( ph -> A C_ RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( B e. ( ( limPt ` J ) ` A ) <-> A. a e. RR* A. b e. RR* ( B e. ( a (,) b ) -> ( ( a (,) b ) i^i ( A \ { B } ) ) =/= (/) ) ) )
Theorem	limccog 37271	Limit of the composition of two functions. If the limit of F at A is B and the limit of G at B is C, then the limit of G o. F at A is C. With respect to limcco 22725 and limccnp 22723, here we drop continuity assumptions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> ran F C_ ( dom G \ { B } ) )   &    |- ( ph -> B e. ( F lim CC A ) )   &    |- ( ph -> C e. ( G lim CC B ) )   =>    |- ( ph -> C e. ( ( G o. F ) lim CC A ) )
Theorem	limciccioolb 37272	The limit of a function at the lower bound of a closed interval only depends on the values in the inner open interval (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> F : ( A [,] B ) --> CC )   =>    |- ( ph -> ( ( F |` ( A (,) B ) ) lim CC A ) = ( F lim CC A ) )
Theorem	climf 37273*	Express the predicate: The limit of complex number sequence F is A, or F converges to A. Similar to clim 13536, but without the disjoint var constraint F k. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F/_ k F   &    |- ( ph -> F e. V )   &    |- ( ( ph /\ k e. ZZ ) -> ( F ` k ) = B )   =>    |- ( ph -> ( F ~~> A <-> ( A e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) ) )
Theorem	mullimcf 37274*	Limit of the multiplication of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> G : A --> CC )   &    |- H = ( x e. A |-> ( ( F ` x ) x. ( G ` x ) ) )   &    |- ( ph -> B e. ( F lim CC D ) )   &    |- ( ph -> C e. ( G lim CC D ) )   =>    |- ( ph -> ( B x. C ) e. ( H lim CC D ) )
Theorem	constlimc 37275*	Limit of constant function (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F = ( x e. A |-> B )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> B e. ( F lim CC C ) )
Theorem	rexlim2d 37276*	Inference removing two restricted quantifiers. Same as rexlimdvv 2930, but with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F/ x ph   &    |- F/ y ph   &    |- ( ph -> ( ( x e. A /\ y e. B ) -> ( ps -> ch ) ) )   =>    |- ( ph -> ( E. x e. A E. y e. B ps -> ch ) )
Theorem	idlimc 37277*	Limit of the identity function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A C_ CC )   &    |- F = ( x e. A |-> x )   &    |- ( ph -> X e. CC )   =>    |- ( ph -> X e. ( F lim CC X ) )
Theorem	divcnvg 37278*	The sequence of reciprocals of positive integers, multiplied by the factor A, converges to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. CC /\ M e. NN ) -> ( n e. ( ZZ>= ` M ) |-> ( A / n ) ) ~~> 0 )
Theorem	limcperiod 37279*	If F is a periodic function with period T, the limit doesn't change if we shift the limiting point by T. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : dom F --> CC )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> A C_ dom F )   &    |- ( ph -> T e. CC )   &    |- B = { x e. CC | E. y e. A x = ( y + T ) }   &    |- ( ph -> B C_ dom F )   &    |- ( ( ph /\ y e. A ) -> ( F ` ( y + T ) ) = ( F ` y ) )   &    |- ( ph -> C e. ( ( F |` A ) lim CC D ) )   =>    |- ( ph -> C e. ( ( F |` B ) lim CC ( D + T ) ) )
Theorem	limcrecl 37280	If F is a real valued function, B is a limit point of its domain, and the limit of F at B exists, then this limit is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : A --> RR )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> B e. ( ( limPt ` ( TopOpen ` ℂfld ) ) ` A ) )   &    |- ( ph -> L e. ( F lim CC B ) )   =>    |- ( ph -> L e. RR )
Theorem	sumnnodd 37281*	A series indexed by NN with only odd terms. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : NN --> CC )   &    |- ( ( ph /\ k e. NN /\ ( k / 2 ) e. NN ) -> ( F ` k ) = 0 )   &    |- ( ph -> seq 1 ( + , F ) ~~> B )   =>    |- ( ph -> ( seq 1 ( + , ( k e. NN |-> ( F ` ( ( 2 x. k ) - 1 ) ) ) ) ~~> B /\ sum_ k e. NN ( F ` k ) = sum_ k e. NN ( F ` ( ( 2 x. k ) - 1 ) ) ) )
Theorem	lptioo2 37282	The upper bound of an open interval is a limit point of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- J = ( topGen ` ran (,) )   &    |- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> B e. ( ( limPt ` J ) ` ( A (,) B ) ) )
Theorem	lptioo1 37283	The lower bound of an open interval is a limit point of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- J = ( topGen ` ran (,) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> A < B )   =>    |- ( ph -> A e. ( ( limPt ` J ) ` ( A (,) B ) ) )
Theorem	elprn1 37284	A member of an unordered pair that is not the "first", must be the "second". (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. { B , C } /\ A =/= B ) -> A = C )
Theorem	elprn2 37285	A member of an unordered pair that is not the "second", must be the "first". (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. { B , C } /\ A =/= C ) -> A = B )
Theorem	limcmptdm 37286*	The domain of a map-to function with a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F = ( x e. A |-> B )   &    |- ( ( ph /\ x e. A ) -> B e. CC )   &    |- ( ph -> C e. ( F lim CC D ) )   =>    |- ( ph -> A C_ CC )
Theorem	clim2f 37287*	Express the predicate: The limit of complex number sequence F is A, or F converges to A, with more general quantifier restrictions than clim 13536. Similar to clim2 13546, but without the disjoint var constraint F k. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F/_ k F   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F e. V )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )   =>    |- ( ph -> ( F ~~> A <-> ( A e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) ) )
Theorem	limcicciooub 37288	The limit of a function at the upper bound of a closed interval only depends on the values in the inner open interval (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> F : ( A [,] B ) --> CC )   =>    |- ( ph -> ( ( F |` ( A (,) B ) ) lim CC B ) = ( F lim CC B ) )
Theorem	ltmod 37289	A sufficient condition for a "less than" relationship for the mod operator. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> C e. ( ( A - ( A mod B ) ) [,) A ) )   =>    |- ( ph -> ( C mod B ) < ( A mod B ) )
Theorem	islpcn 37290*	A characterization for a limit point for the standard topology on the complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> S C_ CC )   &    |- ( ph -> P e. CC )   =>    |- ( ph -> ( P e. ( ( limPt ` ( TopOpen ` ℂfld ) ) ` S ) <-> A. e e. RR+ E. x e. ( S \ { P } ) ( abs ` ( x - P ) ) < e ) )
Theorem	lptre2pt 37291*	If a set in the real line has a limit point than it contains two distinct points that are closer than a given distance. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- J = ( topGen ` ran (,) )   &    |- ( ph -> A C_ RR )   &    |- ( ph -> ( ( limPt ` J ) ` A ) =/= (/) )   &    |- ( ph -> E e. RR+ )   =>    |- ( ph -> E. x e. A E. y e. A ( x =/= y /\ ( abs ` ( x - y ) ) < E ) )
Theorem	limsupre 37292*	If a sequence is bounded, then the limsup is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 13-Sep-2020.)
|- ( ph -> B C_ RR )   &    |- ( ph -> sup ( B , RR* , < ) = +oo )   &    |- ( ph -> F : B --> RR )   &    |- ( ph -> E. b e. RR E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) )   =>    |- ( ph -> ( limsup ` F ) e. RR )
Theorem	limsupreOLD 37293*	If a sequence is bounded, then the limsup is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) Obsolete version of limsupre 37292 as of 13-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> B C_ RR )   &    |- ( ph -> sup ( B , RR* , < ) = +oo )   &    |- ( ph -> F : B --> RR )   &    |- ( ph -> E. b e. RR E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) )   =>    |- ( ph -> ( limsup ` F ) e. RR )
Theorem	limcresiooub 37294	The left limit doesn't change if the function is restricted to a smaller open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. RR )   &    |- ( ph -> B < C )   &    |- ( ph -> ( B (,) C ) C_ A )   &    |- ( ph -> D e. RR* )   &    |- ( ph -> D <_ B )   =>    |- ( ph -> ( ( F |` ( B (,) C ) ) lim CC C ) = ( ( F |` ( D (,) C ) ) lim CC C ) )
Theorem	limcresioolb 37295	The right limit doesn't change if the function is restricted to a smaller open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> B < C )   &    |- ( ph -> ( B (,) C ) C_ A )   &    |- ( ph -> D e. RR* )   &    |- ( ph -> C <_ D )   =>    |- ( ph -> ( ( F |` ( B (,) C ) ) lim CC B ) = ( ( F |` ( B (,) D ) ) lim CC B ) )
Theorem	limcleqr 37296	If the left and the right limits are equal, the limit of the function exits and the three limits coincide. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- K = ( TopOpen ` ℂfld )   &    |- ( ph -> A C_ RR )   &    |- J = ( topGen ` ran (,) )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> B e. RR )   &    |- ( ph -> L e. ( ( F |` ( -oo (,) B ) ) lim CC B ) )   &    |- ( ph -> R e. ( ( F |` ( B (,) +oo ) ) lim CC B ) )   &    |- ( ph -> L = R )   =>    |- ( ph -> L e. ( F lim CC B ) )
Theorem	lptioo2cn 37297	The upper bound of an open interval is a limit point of the interval, wirth respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- J = ( TopOpen ` ℂfld )   &    |- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> B e. ( ( limPt ` J ) ` ( A (,) B ) ) )
Theorem	lptioo1cn 37298	The lower bound of an open interval is a limit point of the interval, wirth respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- J = ( TopOpen ` ℂfld )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> A e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> A e. ( ( limPt ` J ) ` ( A (,) B ) ) )
Theorem	neglimc 37299*	Limit of the negative function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F = ( x e. A |-> B )   &    |- G = ( x e. A |-> -u B )   &    |- ( ( ph /\ x e. A ) -> B e. CC )   &    |- ( ph -> C e. ( F lim CC D ) )   =>    |- ( ph -> -u C e. ( G lim CC D ) )
Theorem	addlimc 37300*	Sum of two limits. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F = ( x e. A |-> B )   &    |- G = ( x e. A |-> C )   &    |- H = ( x e. A |-> ( B + C ) )   &    |- ( ( ph /\ x e. A ) -> B e. CC )   &    |- ( ( ph /\ x e. A ) -> C e. CC )   &    |- ( ph -> E e. ( F lim CC D ) )   &    |- ( ph -> I e. ( G lim CC D ) )   =>    |- ( ph -> ( E + I ) e. ( H lim CC D ) )