P. 138 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 13701-13800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	climshft2 13701*	A shifted function converges iff the original function converges. (Contributed by Paul Chapman, 21-Nov-2007.) (Revised by Mario Carneiro, 6-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> K e. ZZ )   &    |- ( ph -> F e. W )   &    |- ( ph -> G e. X )   &    |- ( ( ph /\ k e. Z ) -> ( G ` ( k + K ) ) = ( F ` k ) )   =>    |- ( ph -> ( F ~~> A <-> G ~~> A ) )
Theorem	climrecl 13702*	The limit of a convergent real sequence is real. Corollary 12-2.5 of [Gleason] p. 172. (Contributed by NM, 10-Sep-2005.) (Proof shortened by Mario Carneiro, 10-May-2016.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   =>    |- ( ph -> A e. RR )
Theorem	climge0 13703*	A nonnegative sequence converges to a nonnegative number. (Contributed by NM, 11-Sep-2005.) (Proof shortened by Mario Carneiro, 10-May-2016.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> 0 <_ ( F ` k ) )   =>    |- ( ph -> 0 <_ A )
Theorem	climabs0 13704*	Convergence to zero of the absolute value is equivalent to convergence to zero. (Contributed by NM, 8-Jul-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F e. V )   &    |- ( ph -> G e. W )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( abs ` ( F ` k ) ) )   =>    |- ( ph -> ( F ~~> 0 <-> G ~~> 0 ) )
Theorem	o1co 13705*	Sufficient condition for transforming the index set of an eventually bounded function. (Contributed by Mario Carneiro, 12-May-2016.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> F e. O(1) )   &    |- ( ph -> G : B --> A )   &    |- ( ph -> B C_ RR )   &    |- ( ( ph /\ m e. RR ) -> E. x e. RR A. y e. B ( x <_ y -> m <_ ( G ` y ) ) )   =>    |- ( ph -> ( F o. G ) e. O(1) )
Theorem	o1compt 13706*	Sufficient condition for transforming the index set of an eventually bounded function. (Contributed by Mario Carneiro, 12-May-2016.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> F e. O(1) )   &    |- ( ( ph /\ y e. B ) -> C e. A )   &    |- ( ph -> B C_ RR )   &    |- ( ( ph /\ m e. RR ) -> E. x e. RR A. y e. B ( x <_ y -> m <_ C ) )   =>    |- ( ph -> ( F o. ( y e. B |-> C ) ) e. O(1) )
Theorem	rlimcn1 13707*	Image of a limit under a continuous map. (Contributed by Mario Carneiro, 17-Sep-2014.)
|- ( ph -> G : A --> X )   &    |- ( ph -> C e. X )   &    |- ( ph -> G ~~> r C )   &    |- ( ph -> F : X --> CC )   &    |- ( ( ph /\ x e. RR+ ) -> E. y e. RR+ A. z e. X ( ( abs ` ( z - C ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` C ) ) ) < x ) )   =>    |- ( ph -> ( F o. G ) ~~> r ( F ` C ) )
Theorem	rlimcn1b 13708*	Image of a limit under a continuous map. (Contributed by Mario Carneiro, 10-May-2016.)
|- ( ( ph /\ k e. A ) -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> ( k e. A |-> B ) ~~> r C )   &    |- ( ph -> F : X --> CC )   &    |- ( ( ph /\ x e. RR+ ) -> E. y e. RR+ A. z e. X ( ( abs ` ( z - C ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` C ) ) ) < x ) )   =>    |- ( ph -> ( k e. A |-> ( F ` B ) ) ~~> r ( F ` C ) )
Theorem	rlimcn2 13709*	Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 17-Sep-2014.)
|- ( ( ph /\ z e. A ) -> B e. X )   &    |- ( ( ph /\ z e. A ) -> C e. Y )   &    |- ( ph -> R e. X )   &    |- ( ph -> S e. Y )   &    |- ( ph -> ( z e. A |-> B ) ~~> r R )   &    |- ( ph -> ( z e. A |-> C ) ~~> r S )   &    |- ( ph -> F : ( X X. Y ) --> CC )   &    |- ( ( ph /\ x e. RR+ ) -> E. r e. RR+ E. s e. RR+ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) )   =>    |- ( ph -> ( z e. A |-> ( B F C ) ) ~~> r ( R F S ) )
Theorem	climcn1 13710*	Image of a limit under a continuous map. (Contributed by Mario Carneiro, 31-Jan-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> A e. B )   &    |- ( ( ph /\ z e. B ) -> ( F ` z ) e. CC )   &    |- ( ph -> G ~~> A )   &    |- ( ph -> H e. W )   &    |- ( ( ph /\ x e. RR+ ) -> E. y e. RR+ A. z e. B ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) < x ) )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. B )   &    |- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( F ` ( G ` k ) ) )   =>    |- ( ph -> H ~~> ( F ` A ) )
Theorem	climcn2 13711*	Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 31-Jan-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> A e. C )   &    |- ( ph -> B e. D )   &    |- ( ( ph /\ ( u e. C /\ v e. D ) ) -> ( u F v ) e. CC )   &    |- ( ph -> G ~~> A )   &    |- ( ph -> H ~~> B )   &    |- ( ph -> K e. W )   &    |- ( ( ph /\ x e. RR+ ) -> E. y e. RR+ E. z e. RR+ A. u e. C A. v e. D ( ( ( abs ` ( u - A ) ) < y /\ ( abs ` ( v - B ) ) < z ) -> ( abs ` ( ( u F v ) - ( A F B ) ) ) < x ) )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. C )   &    |- ( ( ph /\ k e. Z ) -> ( H ` k ) e. D )   &    |- ( ( ph /\ k e. Z ) -> ( K ` k ) = ( ( G ` k ) F ( H ` k ) ) )   =>    |- ( ph -> K ~~> ( A F B ) )
Theorem	addcn2 13712*	Complex number addition is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (We write out the definition directly because df-cn 20298 and df-cncf 21965 are not yet available to us. See addcn 21952 for the abbreviated version.) (Contributed by Mario Carneiro, 31-Jan-2014.)
|- ( ( A e. RR+ /\ B e. CC /\ C e. CC ) -> E. y e. RR+ E. z e. RR+ A. u e. CC A. v e. CC ( ( ( abs ` ( u - B ) ) < y /\ ( abs ` ( v - C ) ) < z ) -> ( abs ` ( ( u + v ) - ( B + C ) ) ) < A ) )
Theorem	subcn2 13713*	Complex number subtraction is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by Mario Carneiro, 31-Jan-2014.)
|- ( ( A e. RR+ /\ B e. CC /\ C e. CC ) -> E. y e. RR+ E. z e. RR+ A. u e. CC A. v e. CC ( ( ( abs ` ( u - B ) ) < y /\ ( abs ` ( v - C ) ) < z ) -> ( abs ` ( ( u - v ) - ( B - C ) ) ) < A ) )
Theorem	mulcn2 13714*	Complex number multiplication is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by Mario Carneiro, 31-Jan-2014.)
|- ( ( A e. RR+ /\ B e. CC /\ C e. CC ) -> E. y e. RR+ E. z e. RR+ A. u e. CC A. v e. CC ( ( ( abs ` ( u - B ) ) < y /\ ( abs ` ( v - C ) ) < z ) -> ( abs ` ( ( u x. v ) - ( B x. C ) ) ) < A ) )
Theorem	reccn2 13715*	The reciprocal function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.) (Revised by Mario Carneiro, 22-Sep-2014.)
|- T = ( if ( 1 <_ ( ( abs ` A ) x. B ) , 1 , ( ( abs ` A ) x. B ) ) x. ( ( abs ` A ) / 2 ) )   =>    |- ( ( A e. ( CC \ { 0 } ) /\ B e. RR+ ) -> E. y e. RR+ A. z e. ( CC \ { 0 } ) ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( 1 / z ) - ( 1 / A ) ) ) < B ) )
Theorem	cn1lem 13716*	A sufficient condition for a function to be continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
|- F : CC --> CC   &    |- ( ( z e. CC /\ A e. CC ) -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) <_ ( abs ` ( z - A ) ) )   =>    |- ( ( A e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) < x ) )
Theorem	abscn2 13717*	The absolute value function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
|- ( ( A e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( abs ` z ) - ( abs ` A ) ) ) < x ) )
Theorem	cjcn2 13718*	The complex conjugate function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
|- ( ( A e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( * ` z ) - ( * ` A ) ) ) < x ) )
Theorem	recn2 13719*	The real part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
|- ( ( A e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( Re ` z ) - ( Re ` A ) ) ) < x ) )
Theorem	imcn2 13720*	The imaginary part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)
|- ( ( A e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( Im ` z ) - ( Im ` A ) ) ) < x ) )
Theorem	climcn1lem 13721*	The limit of a continuous function, theorem form. (Contributed by Mario Carneiro, 9-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> G e. W )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- H : CC --> CC   &    |- ( ( A e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( H ` z ) - ( H ` A ) ) ) < x ) )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( H ` ( F ` k ) ) )   =>    |- ( ph -> G ~~> ( H ` A ) )
Theorem	climabs 13722*	Limit of the absolute value of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> G e. W )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( abs ` ( F ` k ) ) )   =>    |- ( ph -> G ~~> ( abs ` A ) )
Theorem	climcj 13723*	Limit of the complex conjugate of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> G e. W )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( * ` ( F ` k ) ) )   =>    |- ( ph -> G ~~> ( * ` A ) )
Theorem	climre 13724*	Limit of the real part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> G e. W )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( Re ` ( F ` k ) ) )   =>    |- ( ph -> G ~~> ( Re ` A ) )
Theorem	climim 13725*	Limit of the imaginary part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> G e. W )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( Im ` ( F ` k ) ) )   =>    |- ( ph -> G ~~> ( Im ` A ) )
Theorem	rlimmptrcl 13726*	Reverse closure for a real limit. (Contributed by Mario Carneiro, 10-May-2016.)
|- ( ( ph /\ k e. A ) -> B e. V )   &    |- ( ph -> ( k e. A |-> B ) ~~> r C )   =>    |- ( ( ph /\ k e. A ) -> B e. CC )
Theorem	rlimabs 13727*	Limit of the absolute value of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by Mario Carneiro, 10-May-2016.)
|- ( ( ph /\ k e. A ) -> B e. V )   &    |- ( ph -> ( k e. A |-> B ) ~~> r C )   =>    |- ( ph -> ( k e. A |-> ( abs ` B ) ) ~~> r ( abs ` C ) )
Theorem	rlimcj 13728*	Limit of the complex conjugate of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by Mario Carneiro, 10-May-2016.)
|- ( ( ph /\ k e. A ) -> B e. V )   &    |- ( ph -> ( k e. A |-> B ) ~~> r C )   =>    |- ( ph -> ( k e. A |-> ( * ` B ) ) ~~> r ( * ` C ) )
Theorem	rlimre 13729*	Limit of the real part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by Mario Carneiro, 10-May-2016.)
|- ( ( ph /\ k e. A ) -> B e. V )   &    |- ( ph -> ( k e. A |-> B ) ~~> r C )   =>    |- ( ph -> ( k e. A |-> ( Re ` B ) ) ~~> r ( Re ` C ) )
Theorem	rlimim 13730*	Limit of the imaginary part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by Mario Carneiro, 10-May-2016.)
|- ( ( ph /\ k e. A ) -> B e. V )   &    |- ( ph -> ( k e. A |-> B ) ~~> r C )   =>    |- ( ph -> ( k e. A |-> ( Im ` B ) ) ~~> r ( Im ` C ) )
Theorem	o1of2 13731*	Show that a binary operation preserves eventual boundedness. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( ( m e. RR /\ n e. RR ) -> M e. RR )   &    |- ( ( x e. CC /\ y e. CC ) -> ( x R y ) e. CC )   &    |- ( ( ( m e. RR /\ n e. RR ) /\ ( x e. CC /\ y e. CC ) ) -> ( ( ( abs ` x ) <_ m /\ ( abs ` y ) <_ n ) -> ( abs ` ( x R y ) ) <_ M ) )   =>    |- ( ( F e. O(1) /\ G e. O(1) ) -> ( F oF R G ) e. O(1) )
Theorem	o1add 13732	The sum of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) (Proof shortened by Fan Zheng, 14-Jul-2016.)
|- ( ( F e. O(1) /\ G e. O(1) ) -> ( F oF + G ) e. O(1) )
Theorem	o1mul 13733	The product of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) (Proof shortened by Fan Zheng, 14-Jul-2016.)
|- ( ( F e. O(1) /\ G e. O(1) ) -> ( F oF x. G ) e. O(1) )
Theorem	o1sub 13734	The difference of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) (Proof shortened by Fan Zheng, 14-Jul-2016.)
|- ( ( F e. O(1) /\ G e. O(1) ) -> ( F oF - G ) e. O(1) )
Theorem	rlimo1 13735	Any function with a finite limit is eventually bounded. (Contributed by Mario Carneiro, 18-Sep-2014.)
|- ( F ~~> r A -> F e. O(1) )
Theorem	rlimdmo1 13736	A convergent function is eventually bounded. (Contributed by Mario Carneiro, 12-May-2016.)
|- ( F e. dom ~~> r -> F e. O(1) )
Theorem	o1rlimmul 13737	The product of an eventually bounded function and a function of limit zero has limit zero. (Contributed by Mario Carneiro, 18-Sep-2014.)
|- ( ( F e. O(1) /\ G ~~> r 0 ) -> ( F oF x. G ) ~~> r 0 )
Theorem	o1const 13738*	A constant function is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.) (Proof shortened by Mario Carneiro, 26-May-2016.)
|- ( ( A C_ RR /\ B e. CC ) -> ( x e. A |-> B ) e. O(1) )
Theorem	lo1const 13739*	A constant function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ( A C_ RR /\ B e. RR ) -> ( x e. A |-> B ) e. <_O(1) )
Theorem	lo1mptrcl 13740*	Reverse closure for an eventually upper bounded function. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. <_O(1) )   =>    |- ( ( ph /\ x e. A ) -> B e. RR )
Theorem	o1mptrcl 13741*	Reverse closure for an eventually bounded function. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. O(1) )   =>    |- ( ( ph /\ x e. A ) -> B e. CC )
Theorem	o1add2 13742*	The sum of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ph -> ( x e. A |-> B ) e. O(1) )   &    |- ( ph -> ( x e. A |-> C ) e. O(1) )   =>    |- ( ph -> ( x e. A |-> ( B + C ) ) e. O(1) )
Theorem	o1mul2 13743*	The product of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ph -> ( x e. A |-> B ) e. O(1) )   &    |- ( ph -> ( x e. A |-> C ) e. O(1) )   =>    |- ( ph -> ( x e. A |-> ( B x. C ) ) e. O(1) )
Theorem	o1sub2 13744*	The product of two eventually bounded functions is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ph -> ( x e. A |-> B ) e. O(1) )   &    |- ( ph -> ( x e. A |-> C ) e. O(1) )   =>    |- ( ph -> ( x e. A |-> ( B - C ) ) e. O(1) )
Theorem	lo1add 13745*	The sum of two eventually upper bounded functions is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ph -> ( x e. A |-> B ) e. <_O(1) )   &    |- ( ph -> ( x e. A |-> C ) e. <_O(1) )   =>    |- ( ph -> ( x e. A |-> ( B + C ) ) e. <_O(1) )
Theorem	lo1mul 13746*	The product of an eventually upper bounded function and a positive eventually upper bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ph -> ( x e. A |-> B ) e. <_O(1) )   &    |- ( ph -> ( x e. A |-> C ) e. <_O(1) )   &    |- ( ( ph /\ x e. A ) -> 0 <_ B )   =>    |- ( ph -> ( x e. A |-> ( B x. C ) ) e. <_O(1) )
Theorem	lo1mul2 13747*	The product of an eventually upper bounded function and a positive eventually upper bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ph -> ( x e. A |-> B ) e. <_O(1) )   &    |- ( ph -> ( x e. A |-> C ) e. <_O(1) )   &    |- ( ( ph /\ x e. A ) -> 0 <_ B )   =>    |- ( ph -> ( x e. A |-> ( C x. B ) ) e. <_O(1) )
Theorem	o1dif 13748*	If the difference of two functions is eventually bounded, eventual boundedness of either one implies the other. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ( ph /\ x e. A ) -> B e. CC )   &    |- ( ( ph /\ x e. A ) -> C e. CC )   &    |- ( ph -> ( x e. A |-> ( B - C ) ) e. O(1) )   =>    |- ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( x e. A |-> C ) e. O(1) ) )
Theorem	lo1sub 13749*	The difference of an eventually upper bounded function and an eventually bounded function is eventually upper bounded. The "correct" sharp result here takes the second function to be eventually lower bounded instead of just bounded, but our notation for this is simply ( x e. A |-> -u C ) e. <_O(1), so it is just a special case of lo1add 13745. (Contributed by Mario Carneiro, 31-May-2016.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> C e. RR )   &    |- ( ph -> ( x e. A |-> B ) e. <_O(1) )   &    |- ( ph -> ( x e. A |-> C ) e. O(1) )   =>    |- ( ph -> ( x e. A |-> ( B - C ) ) e. <_O(1) )
Theorem	climadd 13750*	Limit of the sum of two converging sequences. Proposition 12-2.1(a) of [Gleason] p. 168. (Contributed by NM, 24-Sep-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)
|- 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	climmul 13751*	Limit of the product of two converging sequences. Proposition 12-2.1(c) of [Gleason] p. 168. (Contributed by NM, 27-Dec-2005.) (Proof shortened by Mario Carneiro, 1-Feb-2014.)
|- 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	climsub 13752*	Limit of the difference of two converging sequences. Proposition 12-2.1(b) of [Gleason] p. 168. (Contributed by NM, 4-Aug-2007.) (Proof shortened by Mario Carneiro, 1-Feb-2014.)
|- 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	climaddc1 13753*	Limit of a constant C added to each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> C e. CC )   &    |- ( ph -> G e. W )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( ( F ` k ) + C ) )   =>    |- ( ph -> G ~~> ( A + C ) )
Theorem	climaddc2 13754*	Limit of a constant C added to each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> C e. CC )   &    |- ( ph -> G e. W )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( C + ( F ` k ) ) )   =>    |- ( ph -> G ~~> ( C + A ) )
Theorem	climmulc2 13755*	Limit of a sequence multiplied by a constant C. Corollary 12-2.2 of [Gleason] p. 171. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> C e. CC )   &    |- ( ph -> G e. W )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( C x. ( F ` k ) ) )   =>    |- ( ph -> G ~~> ( C x. A ) )
Theorem	climsubc1 13756*	Limit of a constant C subtracted from each term of a sequence. (Contributed by Mario Carneiro, 9-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> C e. CC )   &    |- ( ph -> G e. W )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( ( F ` k ) - C ) )   =>    |- ( ph -> G ~~> ( A - C ) )
Theorem	climsubc2 13757*	Limit of a constant C minus each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 9-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> C e. CC )   &    |- ( ph -> G e. W )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( C - ( F ` k ) ) )   =>    |- ( ph -> G ~~> ( C - A ) )
Theorem	climle 13758*	Comparison of the limits of two sequences. (Contributed by Paul Chapman, 10-Sep-2007.) (Revised by Mario Carneiro, 1-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> G ~~> B )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) <_ ( G ` k ) )   =>    |- ( ph -> A <_ B )
Theorem	climsqz 13759*	Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 3-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> G e. W )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) <_ ( G ` k ) )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) <_ A )   =>    |- ( ph -> G ~~> A )
Theorem	climsqz2 13760*	Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by NM, 14-Feb-2008.) (Revised by Mario Carneiro, 3-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ~~> A )   &    |- ( ph -> G e. W )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) <_ ( F ` k ) )   &    |- ( ( ph /\ k e. Z ) -> A <_ ( G ` k ) )   =>    |- ( ph -> G ~~> A )
Theorem	rlimadd 13761*	Limit of the sum of two converging functions. Proposition 12-2.1(a) of [Gleason] p. 168. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ph -> ( x e. A |-> B ) ~~> r D )   &    |- ( ph -> ( x e. A |-> C ) ~~> r E )   =>    |- ( ph -> ( x e. A |-> ( B + C ) ) ~~> r ( D + E ) )
Theorem	rlimsub 13762*	Limit of the difference of two converging functions. Proposition 12-2.1(b) of [Gleason] p. 168. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ph -> ( x e. A |-> B ) ~~> r D )   &    |- ( ph -> ( x e. A |-> C ) ~~> r E )   =>    |- ( ph -> ( x e. A |-> ( B - C ) ) ~~> r ( D - E ) )
Theorem	rlimmul 13763*	Limit of the product of two converging functions. Proposition 12-2.1(c) of [Gleason] p. 168. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ph -> ( x e. A |-> B ) ~~> r D )   &    |- ( ph -> ( x e. A |-> C ) ~~> r E )   =>    |- ( ph -> ( x e. A |-> ( B x. C ) ) ~~> r ( D x. E ) )
Theorem	rlimdiv 13764*	Limit of the quotient of two converging functions. Proposition 12-2.1(a) of [Gleason] p. 168. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> C e. V )   &    |- ( ph -> ( x e. A |-> B ) ~~> r D )   &    |- ( ph -> ( x e. A |-> C ) ~~> r E )   &    |- ( ph -> E =/= 0 )   &    |- ( ( ph /\ x e. A ) -> C =/= 0 )   =>    |- ( ph -> ( x e. A |-> ( B / C ) ) ~~> r ( D / E ) )
Theorem	rlimneg 13765*	Limit of the negative of a sequence. (Contributed by Mario Carneiro, 18-May-2016.)
|- ( ( ph /\ k e. A ) -> B e. V )   &    |- ( ph -> ( k e. A |-> B ) ~~> r C )   =>    |- ( ph -> ( k e. A |-> -u B ) ~~> r -u C )
Theorem	rlimle 13766*	Comparison of the limits of two sequences. (Contributed by Mario Carneiro, 10-May-2016.)
|- ( ph -> sup ( A , RR* , < ) = +oo )   &    |- ( ph -> ( x e. A |-> B ) ~~> r D )   &    |- ( ph -> ( x e. A |-> C ) ~~> r E )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ( ph /\ x e. A ) -> C e. RR )   &    |- ( ( ph /\ x e. A ) -> B <_ C )   =>    |- ( ph -> D <_ E )
Theorem	rlimsqzlem 13767*	Lemma for rlimsqz 13768 and rlimsqz2 13769. (Contributed by Mario Carneiro, 18-Sep-2014.) (Revised by Mario Carneiro, 20-May-2016.)
|- ( ph -> M e. RR )   &    |- ( ph -> E e. CC )   &    |- ( ph -> ( x e. A |-> B ) ~~> r D )   &    |- ( ( ph /\ x e. A ) -> B e. CC )   &    |- ( ( ph /\ x e. A ) -> C e. CC )   &    |- ( ( ph /\ ( x e. A /\ M <_ x ) ) -> ( abs ` ( C - E ) ) <_ ( abs ` ( B - D ) ) )   =>    |- ( ph -> ( x e. A |-> C ) ~~> r E )
Theorem	rlimsqz 13768*	Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by Mario Carneiro, 18-Sep-2014.) (Revised by Mario Carneiro, 20-May-2016.)
|- ( ph -> D e. RR )   &    |- ( ph -> M e. RR )   &    |- ( ph -> ( x e. A |-> B ) ~~> r D )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ( ph /\ x e. A ) -> C e. RR )   &    |- ( ( ph /\ ( x e. A /\ M <_ x ) ) -> B <_ C )   &    |- ( ( ph /\ ( x e. A /\ M <_ x ) ) -> C <_ D )   =>    |- ( ph -> ( x e. A |-> C ) ~~> r D )
Theorem	rlimsqz2 13769*	Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by Mario Carneiro, 3-Feb-2014.) (Revised by Mario Carneiro, 20-May-2016.)
|- ( ph -> D e. RR )   &    |- ( ph -> M e. RR )   &    |- ( ph -> ( x e. A |-> B ) ~~> r D )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ( ph /\ x e. A ) -> C e. RR )   &    |- ( ( ph /\ ( x e. A /\ M <_ x ) ) -> C <_ B )   &    |- ( ( ph /\ ( x e. A /\ M <_ x ) ) -> D <_ C )   =>    |- ( ph -> ( x e. A |-> C ) ~~> r D )
Theorem	lo1le 13770*	Transfer eventual upper boundedness from a larger function to a smaller function. (Contributed by Mario Carneiro, 26-May-2016.)
|- ( ph -> M e. RR )   &    |- ( ph -> ( x e. A |-> B ) e. <_O(1) )   &    |- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> C e. RR )   &    |- ( ( ph /\ ( x e. A /\ M <_ x ) ) -> C <_ B )   =>    |- ( ph -> ( x e. A |-> C ) e. <_O(1) )
Theorem	o1le 13771*	Transfer eventual boundedness from a larger function to a smaller function. (Contributed by Mario Carneiro, 25-Sep-2014.) (Proof shortened by Mario Carneiro, 26-May-2016.)
|- ( ph -> M e. RR )   &    |- ( ph -> ( x e. A |-> B ) e. O(1) )   &    |- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> C e. CC )   &    |- ( ( ph /\ ( x e. A /\ M <_ x ) ) -> ( abs ` C ) <_ ( abs ` B ) )   =>    |- ( ph -> ( x e. A |-> C ) e. O(1) )
Theorem	rlimno1 13772*	A function whose inverse converges to zero is unbounded. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> sup ( A , RR* , < ) = +oo )   &    |- ( ph -> ( x e. A |-> ( 1 / B ) ) ~~> r 0 )   &    |- ( ( ph /\ x e. A ) -> B e. CC )   &    |- ( ( ph /\ x e. A ) -> B =/= 0 )   =>    |- ( ph -> -. ( x e. A |-> B ) e. O(1) )
Theorem	clim2ser 13773*	The limit of an infinite series with an initial segment removed. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 1-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ph -> seq M ( + , F ) ~~> A )   =>    |- ( ph -> seq ( N + 1 ) ( + , F ) ~~> ( A - ( seq M ( + , F ) ` N ) ) )
Theorem	clim2ser2 13774*	The limit of an infinite series with an initial segment added. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 1-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ph -> seq ( N + 1 ) ( + , F ) ~~> A )   =>    |- ( ph -> seq M ( + , F ) ~~> ( A + ( seq M ( + , F ) ` N ) ) )
Theorem	iserex 13775*	An infinite series converges, if and only if the series does with initial terms removed. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 27-Apr-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   =>    |- ( ph -> ( seq M ( + , F ) e. dom ~~> <-> seq N ( + , F ) e. dom ~~> ) )
Theorem	isermulc2 13776*	Multiplication of an infinite series by a constant. (Contributed by Paul Chapman, 14-Nov-2007.) (Revised by Mario Carneiro, 1-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> C e. CC )   &    |- ( ph -> seq M ( + , F ) ~~> A )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( C x. ( F ` k ) ) )   =>    |- ( ph -> seq M ( + , G ) ~~> ( C x. A ) )
Theorem	climlec2 13777*	Comparison of a constant to the limit of a sequence. (Contributed by NM, 28-Feb-2008.) (Revised by Mario Carneiro, 1-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> A e. RR )   &    |- ( ph -> F ~~> B )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> A <_ ( F ` k ) )   =>    |- ( ph -> A <_ B )
Theorem	iserle 13778*	Comparison of the limits of two infinite series. (Contributed by Paul Chapman, 12-Nov-2007.) (Revised by Mario Carneiro, 3-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> seq M ( + , F ) ~~> A )   &    |- ( ph -> seq M ( + , G ) ~~> B )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) <_ ( G ` k ) )   =>    |- ( ph -> A <_ B )
Theorem	iserge0 13779*	The limit of an infinite series of nonnegative reals is nonnegative. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 3-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> seq M ( + , F ) ~~> A )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> 0 <_ ( F ` k ) )   =>    |- ( ph -> 0 <_ A )
Theorem	climub 13780*	The limit of a monotonic sequence is an upper bound. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 10-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ph -> F ~~> A )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) <_ ( F ` ( k + 1 ) ) )   =>    |- ( ph -> ( F ` N ) <_ A )
Theorem	climserle 13781*	The partial sums of a converging infinite series with nonnegative terms are bounded by its limit. (Contributed by NM, 27-Dec-2005.) (Revised by Mario Carneiro, 9-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ph -> seq M ( + , F ) ~~> A )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. Z ) -> 0 <_ ( F ` k ) )   =>    |- ( ph -> ( seq M ( + , F ) ` N ) <_ A )
Theorem	isershft 13782	Index shift of the limit of an infinite series. (Contributed by Mario Carneiro, 6-Sep-2013.) (Revised by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( ( M e. ZZ /\ N e. ZZ ) -> ( seq M ( .+ , F ) ~~> A <-> seq ( M + N ) ( .+ , ( F shift N ) ) ~~> A ) )
Theorem	isercolllem1 13783*	Lemma for isercoll 13786. (Contributed by Mario Carneiro, 6-Apr-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> G : NN --> Z )   &    |- ( ( ph /\ k e. NN ) -> ( G ` k ) < ( G ` ( k + 1 ) ) )   =>    |- ( ( ph /\ S C_ NN ) -> ( G |` S ) Isom < , < ( S , ( G " S ) ) )
Theorem	isercolllem2 13784*	Lemma for isercoll 13786. (Contributed by Mario Carneiro, 6-Apr-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> G : NN --> Z )   &    |- ( ( ph /\ k e. NN ) -> ( G ` k ) < ( G ` ( k + 1 ) ) )   =>    |- ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( 1 ... ( # ` ( G " ( `' G " ( M ... N ) ) ) ) ) = ( `' G " ( M ... N ) ) )
Theorem	isercolllem3 13785*	Lemma for isercoll 13786. (Contributed by Mario Carneiro, 6-Apr-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> G : NN --> Z )   &    |- ( ( ph /\ k e. NN ) -> ( G ` k ) < ( G ` ( k + 1 ) ) )   &    |- ( ( ph /\ n e. ( Z \ ran G ) ) -> ( F ` n ) = 0 )   &    |- ( ( ph /\ n e. Z ) -> ( F ` n ) e. CC )   &    |- ( ( ph /\ k e. NN ) -> ( H ` k ) = ( F ` ( G ` k ) ) )   =>    |- ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( seq M ( + , F ) ` N ) = ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... N ) ) ) ) ) )
Theorem	isercoll 13786*	Rearrange an infinite series by spacing out the terms using an order isomorphism. (Contributed by Mario Carneiro, 6-Apr-2015.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> G : NN --> Z )   &    |- ( ( ph /\ k e. NN ) -> ( G ` k ) < ( G ` ( k + 1 ) ) )   &    |- ( ( ph /\ n e. ( Z \ ran G ) ) -> ( F ` n ) = 0 )   &    |- ( ( ph /\ n e. Z ) -> ( F ` n ) e. CC )   &    |- ( ( ph /\ k e. NN ) -> ( H ` k ) = ( F ` ( G ` k ) ) )   =>    |- ( ph -> ( seq 1 ( + , H ) ~~> A <-> seq M ( + , F ) ~~> A ) )
Theorem	isercoll2 13787*	Generalize isercoll 13786 so that both sequences have arbitrary starting point. (Contributed by Mario Carneiro, 6-Apr-2015.)
|- Z = ( ZZ>= ` M )   &    |- W = ( ZZ>= ` N )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> G : Z --> W )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) < ( G ` ( k + 1 ) ) )   &    |- ( ( ph /\ n e. ( W \ ran G ) ) -> ( F ` n ) = 0 )   &    |- ( ( ph /\ n e. W ) -> ( F ` n ) e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( F ` ( G ` k ) ) )   =>    |- ( ph -> ( seq M ( + , H ) ~~> A <-> seq N ( + , F ) ~~> A ) )
Theorem	climsup 13788*	A bounded monotonic sequence converges to the supremum of its range. Theorem 12-5.1 of [Gleason] p. 180. (Contributed by NM, 13-Mar-2005.) (Revised by Mario Carneiro, 10-Feb-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F : Z --> RR )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) <_ ( F ` ( k + 1 ) ) )   &    |- ( ph -> E. x e. RR A. k e. Z ( F ` k ) <_ x )   =>    |- ( ph -> F ~~> sup ( ran F , RR , < ) )
Theorem	climcau 13789*	A converging sequence of complex numbers is a Cauchy sequence. Theorem 12-5.3 of [Gleason] p. 180 (necessity part). (Contributed by NM, 16-Apr-2005.) (Revised by Mario Carneiro, 26-Apr-2014.)
|- Z = ( ZZ>= ` M )   =>    |- ( ( M e. ZZ /\ F e. dom ~~> ) -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x )
Theorem	climbdd 13790*	A converging sequence of complex numbers is bounded. (Contributed by Mario Carneiro, 9-Jul-2017.)
|- Z = ( ZZ>= ` M )   =>    |- ( ( M e. ZZ /\ F e. dom ~~> /\ A. k e. Z ( F ` k ) e. CC ) -> E. x e. RR A. k e. Z ( abs ` ( F ` k ) ) <_ x )
Theorem	caucvgrlem 13791*	Lemma for caurcvgr 13793. (Contributed by Mario Carneiro, 15-Feb-2014.) (Revised by AV, 12-Sep-2020.)
|- ( ph -> A C_ RR )   &    |- ( ph -> F : A --> RR )   &    |- ( ph -> sup ( A , RR* , < ) = +oo )   &    |- ( ph -> A. x e. RR+ E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )   &    |- ( ph -> R e. RR+ )   =>    |- ( ph -> E. j e. A ( ( limsup ` F ) e. RR /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < ( 3 x. R ) ) ) )
Theorem	caucvgrlemOLD 13792*	Lemma for caurcvgr 13793. (Contributed by Mario Carneiro, 15-Feb-2014.) (Revised by Mario Carneiro, 8-May-2016.) Obsolete version of caucvgrlem 13791 as of 12-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> A C_ RR )   &    |- ( ph -> F : A --> RR )   &    |- ( ph -> sup ( A , RR* , < ) = +oo )   &    |- ( ph -> A. x e. RR+ E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )   &    |- ( ph -> R e. RR+ )   =>    |- ( ph -> E. j e. A ( ( limsup ` F ) e. RR /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < ( 3 x. R ) ) ) )
Theorem	caurcvgr 13793*	A Cauchy sequence of real numbers converges to its limit supremum. The third hypothesis specifies that F is a Cauchy sequence. (Contributed by Mario Carneiro, 7-May-2016.) (Revised by AV, 12-Sep-2020.)
|- ( ph -> A C_ RR )   &    |- ( ph -> F : A --> RR )   &    |- ( ph -> sup ( A , RR* , < ) = +oo )   &    |- ( ph -> A. x e. RR+ E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )   =>    |- ( ph -> F ~~> r ( limsup ` F ) )
Theorem	caurcvgrOLD 13794*	A Cauchy sequence of real numbers converges to its limit supremum. The third hypothesis specifies that F is a Cauchy sequence. (Contributed by Mario Carneiro, 7-May-2016.) Obsolete version of caurcvgr 13793 as of 12-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> A C_ RR )   &    |- ( ph -> F : A --> RR )   &    |- ( ph -> sup ( A , RR* , < ) = +oo )   &    |- ( ph -> A. x e. RR+ E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )   =>    |- ( ph -> F ~~> r ( limsup ` F ) )
Theorem	caucvgrlem2 13795*	Lemma for caucvgr 13796. (Contributed by NM, 4-Apr-2005.) (Proof shortened by Mario Carneiro, 8-May-2016.)
|- ( ph -> A C_ RR )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> sup ( A , RR* , < ) = +oo )   &    |- ( ph -> A. x e. RR+ E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )   &    |- H : CC --> RR   &    |- ( ( ( F ` k ) e. CC /\ ( F ` j ) e. CC ) -> ( abs ` ( ( H ` ( F ` k ) ) - ( H ` ( F ` j ) ) ) ) <_ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) )   =>    |- ( ph -> ( n e. A |-> ( H ` ( F ` n ) ) ) ~~> r ( ~~> r ` ( H o. F ) ) )
Theorem	caucvgr 13796*	A Cauchy sequence of complex numbers converges to a complex number. Theorem 12-5.3 of [Gleason] p. 180 (sufficiency part). (Contributed by NM, 20-Dec-2006.) (Revised by Mario Carneiro, 8-May-2016.)
|- ( ph -> A C_ RR )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> sup ( A , RR* , < ) = +oo )   &    |- ( ph -> A. x e. RR+ E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )   =>    |- ( ph -> F e. dom ~~> r )
Theorem	caurcvg 13797*	A Cauchy sequence of real numbers converges to its limit supremum. The fourth hypothesis specifies that F is a Cauchy sequence. (Contributed by NM, 4-Apr-2005.) (Revised by AV, 12-Sep-2020.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> F : Z --> RR )   &    |- ( ph -> A. x e. RR+ E. m e. Z A. k e. ( ZZ>= ` m ) ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x )   =>    |- ( ph -> F ~~> ( limsup ` F ) )
Theorem	caurcvgOLD 13798*	A Cauchy sequence of real numbers converges to its limit supremum. The fourth hypothesis specifies that F is a Cauchy sequence. (Contributed by NM, 4-Apr-2005.) (Revised by Mario Carneiro, 8-May-2016.) Obsolete version of caurcvg 13797 as of 12-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> F : Z --> RR )   &    |- ( ph -> A. x e. RR+ E. m e. Z A. k e. ( ZZ>= ` m ) ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x )   =>    |- ( ph -> F ~~> ( limsup ` F ) )
Theorem	caurcvg2 13799*	A Cauchy sequence of real numbers converges, existence version. (Contributed by NM, 4-Apr-2005.) (Revised by Mario Carneiro, 7-Sep-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> F e. V )   &    |- ( ph -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. RR /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )   =>    |- ( ph -> F e. dom ~~> )
Theorem	caucvg 13800*	A Cauchy sequence of complex numbers converges to a complex number. Theorem 12-5.3 of [Gleason] p. 180 (sufficiency part). (Contributed by NM, 20-Dec-2006.) (Proof shortened by Mario Carneiro, 15-Feb-2014.) (Revised by Mario Carneiro, 8-May-2016.)
|- Z = ( ZZ>= ` M )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   &    |- ( ph -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x )   &    |- ( ph -> F e. V )   =>    |- ( ph -> F e. dom ~~> )