P. 399 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39801-39900   *Has distinct variable group(s)

Type	Label	Description
Statement
20.32.5  Finite sums
Theorem	fsumclf 39801*	Closure of a finite sum of complex numbers A ( k ). A version of fsumcl 14464 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	fsummulc1f 39802*	Closure of a finite sum of complex numbers A ( k ). A version of fsummulc1 14517 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	fsumnncl 39803*	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 39804*	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 39805*	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 39806*	Re-index a finite sum using a bijection. Same as fsumf1o 14454, 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 39807*	Sum over a disjoint indexed union, intersected with a finite set D. Similar to fsumiun 14553, 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 39808*	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 39809*	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 39810*	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 ) )
Theorem	fsumsermpt 39811*	A finite sum expressed in terms of a partial sum of an infinite series. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ( ph /\ k e. Z ) -> A e. CC )   &    |- F = ( n e. Z |-> sum_ k e. ( M ... n ) A )   &    |- G = seq M ( + , ( k e. Z |-> A ) )   =>    |- ( ph -> F = G )
20.32.6  Finite multiplication of numbers and finite multiplication of functions
Theorem	fmul01 39812*	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 39813*	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 39814*	induction step for the proof of fmuldfeq 39815. (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 39815*	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 39816*	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 39817*	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 39818*	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 39819*	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 39820	The positive reals are a subset of the complex numbers. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- RR+ C_ CC
Theorem	mulc1cncfg 39821*	A version of mulc1cncf 22708 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 39822*	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	expcnfg 39823*	If F is a complex continuous function and N is a fixed number, then F^N is continuous too. A generalization of expcncf 22725. (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 39824*	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 39825*	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 39826*	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 39827*	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 39828*	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 39829*	* Induction step for mccl 39830. (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 39830*	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 )
Theorem	fprodcnlem 39831*	A finite product of functions to complex numbers from a common topological space is continuous. Induction step. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- F/ k ph   &    |- K = ( TopOpen ` ℂfld )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> ( x e. X |-> B ) e. ( J Cn K ) )   &    |- ( ph -> Z C_ A )   &    |- ( ph -> W e. ( A \ Z ) )   &    |- ( ph -> ( x e. X |-> prod_ k e. Z B ) e. ( J Cn K ) )   =>    |- ( ph -> ( x e. X |-> prod_ k e. ( Z u. { W } ) B ) e. ( J Cn K ) )
Theorem	fprodcn 39832*	A finite product of functions to complex numbers from a common topological space is continuous. The class expression for B normally contains free variables k and x to index it. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- F/ k ph   &    |- K = ( TopOpen ` ℂfld )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> ( x e. X |-> B ) e. ( J Cn K ) )   =>    |- ( ph -> ( x e. X |-> prod_ k e. A B ) e. ( J Cn K ) )
20.32.7  Limits
Theorem	clim1fr1 39833*	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 39834*	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 39835*	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 39836*	A version of climmul 14363 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 39837*	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 39838*	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	climsuselem1 39839*	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 39840*	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 39841*	A version of climrec 39835 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 39842*	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 39843*	A version of climinf 39838 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	climdivf 39844*	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 39845	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 39846*	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 39847*	A version of climadd 14362 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 39848*	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 39849*	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 39850	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 39851*	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 39852	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 23657 and limccnp 23655, 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 39853	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 39854*	Express the predicate: The limit of complex number sequence F is A, or F converges to A. Similar to clim 14225, 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 39855*	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 39856*	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 39857*	Inference removing two restricted quantifiers. Same as rexlimdvv 3037, 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 39858*	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 39859*	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 39860*	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 39861	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 39862*	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 39863	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 39864	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 39865	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 39866	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 39867*	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 39868*	Express the predicate: The limit of complex number sequence F is A, or F converges to A, with more general quantifier restrictions than clim 14225. Similar to clim2 14235, 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 39869	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 39870	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 39871*	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 39872*	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 39873*	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	limcresiooub 39874	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 39875	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 39876	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 39877	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 39878	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 39879*	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 39880*	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 ) )
Theorem	0ellimcdiv 39881*	If the numerator converges to 0 and the denominator converges to non zero then the fraction converges to 0. (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 \ { 0 } ) )   &    |- ( ph -> 0 e. ( F lim CC E ) )   &    |- ( ph -> D e. ( G lim CC E ) )   &    |- ( ph -> D =/= 0 )   =>    |- ( ph -> 0 e. ( H lim CC E ) )
Theorem	clim2cf 39882*	Express the predicate F converges to A. Similar to clim2 14235, 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 -> A e. CC )   &    |- ( ( ph /\ k e. Z ) -> B e. CC )   =>    |- ( ph -> ( F ~~> A <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( B - A ) ) < x ) )
Theorem	limclner 39883	For a limit point, both from the left and from the right, of the domain, the limit of the function exits only if the left and the right limits are equal. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- K = ( TopOpen ` ℂfld )   &    |- ( ph -> A C_ RR )   &    |- J = ( topGen ` ran (,) )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> B e. ( ( limPt ` J ) ` ( A i^i ( -oo (,) B ) ) ) )   &    |- ( ph -> B e. ( ( limPt ` J ) ` ( A i^i ( B (,) +oo ) ) ) )   &    |- ( ph -> L e. ( ( F |` ( -oo (,) B ) ) lim CC B ) )   &    |- ( ph -> R e. ( ( F |` ( B (,) +oo ) ) lim CC B ) )   &    |- ( ph -> L =/= R )   =>    |- ( ph -> ( F lim CC B ) = (/) )
Theorem	sublimc 39884*	Subtraction 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 ) )
Theorem	reclimc 39885*	Limit of the reciprocal of a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F = ( x e. A |-> B )   &    |- G = ( x e. A |-> ( 1 / B ) )   &    |- ( ( ph /\ x e. A ) -> B e. ( CC \ { 0 } ) )   &    |- ( ph -> C e. ( F lim CC D ) )   &    |- ( ph -> C =/= 0 )   =>    |- ( ph -> ( 1 / C ) e. ( G lim CC D ) )
Theorem	clim0cf 39886*	Express the predicate F converges to 0. Similar to clim 14225, 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 /\ k e. Z ) -> B e. CC )   =>    |- ( ph -> ( F ~~> 0 <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` B ) < x ) )
Theorem	limclr 39887	For a limit point, both from the left and from the right, of the domain, the limit of the function exits only if the left and the right limits are equal. In this case, 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. ( ( limPt ` J ) ` ( A i^i ( -oo (,) B ) ) ) )   &    |- ( ph -> B e. ( ( limPt ` J ) ` ( A i^i ( B (,) +oo ) ) ) )   &    |- ( ph -> L e. ( ( F |` ( -oo (,) B ) ) lim CC B ) )   &    |- ( ph -> R e. ( ( F |` ( B (,) +oo ) ) lim CC B ) )   =>    |- ( ph -> ( ( ( F lim CC B ) =/= (/) <-> L = R ) /\ ( L = R -> L e. ( F lim CC B ) ) ) )
Theorem	divlimc 39888*	Limit of the quotient 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 / C ) )   &    |- ( ( ph /\ x e. A ) -> B e. CC )   &    |- ( ( ph /\ x e. A ) -> C e. ( CC \ { 0 } ) )   &    |- ( ph -> X e. ( F lim CC D ) )   &    |- ( ph -> Y e. ( G lim CC D ) )   &    |- ( ph -> Y =/= 0 )   &    |- ( ( ph /\ x e. A ) -> C =/= 0 )   =>    |- ( ph -> ( X / Y ) e. ( H lim CC D ) )
Theorem	expfac 39889*	Factorial grows faster than exponential. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )   =>    |- ( A e. CC -> F ~~> 0 )
Theorem	climconstmpt 39890*	A constant sequence converges to its value. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> A e. CC )   =>    |- ( ph -> ( x e. Z |-> A ) ~~> A )
Theorem	climresmpt 39891*	A function restricted to upper integers converges iff the original function converges. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- Z = ( ZZ>= ` M )   &    |- F = ( x e. Z |-> A )   &    |- ( ph -> N e. Z )   &    |- G = ( x e. ( ZZ>= ` N ) |-> A )   =>    |- ( ph -> ( G ~~> B <-> F ~~> B ) )
Theorem	climsubmpt 39892*	Limit of the difference of two converging sequences. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- F/ k ph   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> A e. CC )   &    |- ( ( ph /\ k e. Z ) -> B e. CC )   &    |- ( ph -> ( k e. Z |-> A ) ~~> C )   &    |- ( ph -> ( k e. Z |-> B ) ~~> D )   =>    |- ( ph -> ( k e. Z |-> ( A - B ) ) ~~> ( C - D ) )
Theorem	climsubc2mpt 39893*	Limit of the difference of two converging sequences. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- F/ k ph   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> A e. CC )   &    |- ( ph -> ( k e. Z |-> A ) ~~> C )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( k e. Z |-> ( A - B ) ) ~~> ( C - B ) )
Theorem	climsubc1mpt 39894*	Limit of the difference of two converging sequences. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- F/ k ph   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> A e. CC )   &    |- ( ( ph /\ k e. Z ) -> B e. CC )   &    |- ( ph -> ( k e. Z |-> B ) ~~> C )   =>    |- ( ph -> ( k e. Z |-> ( A - B ) ) ~~> ( A - C ) )
Theorem	fnlimfv 39895*	The value of the limit function G at any point of its domain D. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/_ x D   &    |- F/_ x F   &    |- G = ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )   &    |- ( ph -> X e. D )   =>    |- ( ph -> ( G ` X ) = ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` X ) ) ) )
Theorem	climreclf 39896*	The limit of a convergent real sequence is real. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/ k ph   &    |- F/_ k F   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   =>    |- ( ph -> A e. RR )
Theorem	climeldmeq 39897*	Two functions that are eventually equal, either both are convergent or both are divergent. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> F e. V )   &    |- ( ph -> G e. W )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = ( G ` k ) )   =>    |- ( ph -> ( F e. dom ~~> <-> G e. dom ~~> ) )
Theorem	climf2 39898*	Express the predicate: The limit of complex number sequence F is A, or F converges to A. Similar to clim 14225, but without the disjoint var constraint ph k and F k. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/ k ph   &    |- 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	fnlimcnv 39899*	The sequence of function values converges to the value of the limit function G at any point of its domain D. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/_ x F   &    |- D = { x e. U_ n e. Z |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | ( m e. Z |-> ( ( F ` m ) ` x ) ) e. dom ~~> }   &    |- G = ( x e. D |-> ( ~~> ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) )   &    |- ( ph -> X e. D )   =>    |- ( ph -> ( m e. Z |-> ( ( F ` m ) ` X ) ) ~~> ( G ` X ) )
Theorem	climeldmeqmpt 39900*	Two functions that are eventually equal, either both are convergent or both are divergent. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/ k ph   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> A e. R )   &    |- ( ph -> Z C_ A )   &    |- ( ( ph /\ k e. A ) -> B e. V )   &    |- ( ph -> C e. S )   &    |- ( ph -> Z C_ C )   &    |- ( ( ph /\ k e. C ) -> D e. W )   &    |- ( ( ph /\ k e. Z ) -> B = D )   =>    |- ( ph -> ( ( k e. A |-> B ) e. dom ~~> <-> ( k e. C |-> D ) e. dom ~~> ) )