P. 109 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 10801-10900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fxnn0nninf 10801*	A function from NN0* into ℕ∞. (Contributed by Jim Kingdon, 16-Jul-2022.) TODO: use infnninf 7415 instead of infnninfOLD 7416. More generally, this theorem and most theorems in this section could use an extended G defined by G = (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) u. <. om , +oo >. ) and F = ( n e. suc om |-> ( i e. om |-> if ( i e. n , 1o , (/) ) ) ) as in nnnninf2 7418.
|- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- F = ( n e. om |-> ( i e. om |-> if ( i e. n , 1o , (/) ) ) )   &    |- I = ( ( F o. `' G ) u. { <. +oo , ( om X. { 1o } ) >. } )   =>    |- I :NN0* -->ℕ∞
Theorem	0tonninf 10802*	The mapping of zero into ℕ∞ is the sequence of all zeroes. (Contributed by Jim Kingdon, 17-Jul-2022.)
|- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- F = ( n e. om |-> ( i e. om |-> if ( i e. n , 1o , (/) ) ) )   &    |- I = ( ( F o. `' G ) u. { <. +oo , ( om X. { 1o } ) >. } )   =>    |- ( I ` 0 ) = ( x e. om |-> (/) )
Theorem	1tonninf 10803*	The mapping of one into ℕ∞ is a sequence which is a one followed by zeroes. (Contributed by Jim Kingdon, 17-Jul-2022.)
|- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- F = ( n e. om |-> ( i e. om |-> if ( i e. n , 1o , (/) ) ) )   &    |- I = ( ( F o. `' G ) u. { <. +oo , ( om X. { 1o } ) >. } )   =>    |- ( I ` 1 ) = ( x e. om |-> if ( x = (/) , 1o , (/) ) )
Theorem	inftonninf 10804*	The mapping of +oo into ℕ∞ is the sequence of all ones. (Contributed by Jim Kingdon, 17-Jul-2022.)
|- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- F = ( n e. om |-> ( i e. om |-> if ( i e. n , 1o , (/) ) ) )   &    |- I = ( ( F o. `' G ) u. { <. +oo , ( om X. { 1o } ) >. } )   =>    |- ( I ` +oo ) = ( x e. om |-> 1o )
Theorem	nninfinf 10805	ℕ∞ is infinte. (Contributed by Jim Kingdon, 8-Jul-2025.)
|- om ~<_ ℕ∞
4.6.4  Strong induction over upper sets of integers
Theorem	uzsinds 10806*	Strong (or "total") induction principle over an upper set of integers. (Contributed by Scott Fenton, 16-May-2014.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ( x = N -> ( ph <-> ch ) )   &    |- ( x e. ( ZZ>= ` M ) -> ( A. y e. ( M ... ( x - 1 ) ) ps -> ph ) )   =>    |- ( N e. ( ZZ>= ` M ) -> ch )
Theorem	nnsinds 10807*	Strong (or "total") induction principle over the naturals. (Contributed by Scott Fenton, 16-May-2014.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ( x = N -> ( ph <-> ch ) )   &    |- ( x e. NN -> ( A. y e. ( 1 ... ( x - 1 ) ) ps -> ph ) )   =>    |- ( N e. NN -> ch )
Theorem	nn0sinds 10808*	Strong (or "total") induction principle over the nonnegative integers. (Contributed by Scott Fenton, 16-May-2014.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ( x = N -> ( ph <-> ch ) )   &    |- ( x e. NN0 -> ( A. y e. ( 0 ... ( x - 1 ) ) ps -> ph ) )   =>    |- ( N e. NN0 -> ch )
4.6.5  The infinite sequence builder "seq"
Syntax	cseq 10809	Extend class notation with recursive sequence builder.
class seq M ( .+ , F )
Definition	df-seqfrec 10810*	Define a general-purpose operation that builds a recursive sequence (i.e., a function on an upper integer set such as NN or NN0) whose value at an index is a function of its previous value and the value of an input sequence at that index. This definition is complicated, but fortunately it is not intended to be used directly. Instead, the only purpose of this definition is to provide us with an object that has the properties expressed by seqf 10826, seq3-1 10824 and seq3p1 10827. Typically, those are the main theorems that would be used in practice. The first operand in the parentheses is the operation that is applied to the previous value and the value of the input sequence (second operand). The operand to the left of the parenthesis is the integer to start from. For example, for the operation +, an input sequence F with values 1, 1/2, 1/4, 1/8,... would be transformed into the output sequence seq 1 ( + , F ) with values 1, 3/2, 7/4, 15/8,.., so that ( seq 1 ( + , F ) ` 1 ) = 1, ( seq 1 ( + , F ) ` 2 ) = 3/2, etc. In other words, seq M ( + , F ) transforms a sequence F into an infinite series. seq M ( + , F ) ~~> 2 means "the sum of F(n) from n = M to infinity is 2". Since limits are unique (climuni 11978), by climdm 11980 the "sum of F(n) from n = 1 to infinity" can be expressed as ( ~~> ` seq 1 ( + , F ) ) (provided the sequence converges) and evaluates to 2 in this example. Internally, the frec function generates as its values a set of ordered pairs starting at <. M , ( F ` M ) >., with the first member of each pair incremented by one in each successive value. So, the range of frec is exactly the sequence we want, and we just extract the range and throw away the domain. (Contributed by NM, 18-Apr-2005.) (Revised by Jim Kingdon, 4-Nov-2022.)
|- seq M ( .+ , F ) = ran frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
Theorem	seqex 10811	Existence of the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.)
|- seq M ( .+ , F ) e. _V
Theorem	seqeq1 10812	Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.)
|- ( M = N -> seq M ( .+ , F ) = seq N ( .+ , F ) )
Theorem	seqeq2 10813	Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.)
|- ( .+ = Q -> seq M ( .+ , F ) = seq M ( Q , F ) )
Theorem	seqeq3 10814	Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013.)
|- ( F = G -> seq M ( .+ , F ) = seq M ( .+ , G ) )
Theorem	seqeq1d 10815	Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.)
|- ( ph -> A = B )   =>    |- ( ph -> seq A ( .+ , F ) = seq B ( .+ , F ) )
Theorem	seqeq2d 10816	Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.)
|- ( ph -> A = B )   =>    |- ( ph -> seq M ( A , F ) = seq M ( B , F ) )
Theorem	seqeq3d 10817	Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.)
|- ( ph -> A = B )   =>    |- ( ph -> seq M ( .+ , A ) = seq M ( .+ , B ) )
Theorem	seqeq123d 10818	Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7-Sep-2013.)
|- ( ph -> M = N )   &    |- ( ph -> .+ = Q )   &    |- ( ph -> F = G )   =>    |- ( ph -> seq M ( .+ , F ) = seq N ( Q , G ) )
Theorem	nfseq 10819	Hypothesis builder for the sequence builder operation. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)
|- F/_ x M   &    |- F/_ x .+   &    |- F/_ x F   =>    |- F/_ x seq M ( .+ , F )
Theorem	iseqovex 10820*	Closure of a function used in proving sequence builder theorems. This can be thought of as a lemma for the small number of sequence builder theorems which need it. (Contributed by Jim Kingdon, 31-May-2020.)
|- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   =>    |- ( ( ph /\ ( x e. ( ZZ>= ` M ) /\ y e. S ) ) -> ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) e. S )
Theorem	iseqvalcbv 10821*	Changing the bound variables in an expression which appears in some seq related proofs. (Contributed by Jim Kingdon, 28-Apr-2022.)
|- frec ( ( x e. ( ZZ>= ` M ) , y e. T |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) = frec ( ( a e. ( ZZ>= ` M ) , b e. T |-> <. ( a + 1 ) , ( a ( c e. ( ZZ>= ` M ) , d e. S |-> ( d .+ ( F ` ( c + 1 ) ) ) ) b ) >. ) , <. M , ( F ` M ) >. )
Theorem	seq3val 10822*	Value of the sequence builder function. This helps expand the definition although there should be little need for it once we have proved seqf 10826, seq3-1 10824 and seq3p1 10827, as further development can be done in terms of those. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 4-Nov-2022.)
|- ( ph -> M e. ZZ )   &    |- R = frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. S |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   =>    |- ( ph -> seq M ( .+ , F ) = ran R )
Theorem	seqvalcd 10823*	Value of the sequence builder function. Similar to seq3val 10822 but the classes D (type of each term) and C (type of the value we are accumulating) do not need to be the same. (Contributed by Jim Kingdon, 9-Jul-2023.)
|- ( ph -> M e. ZZ )   &    |- R = frec ( ( x e. ( ZZ>= ` M ) , y e. _V |-> <. ( x + 1 ) , ( x ( z e. ( ZZ>= ` M ) , w e. C |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. )   &    |- ( ph -> ( F ` M ) e. C )   &    |- ( ( ph /\ ( x e. C /\ y e. D ) ) -> ( x .+ y ) e. C )   &    |- ( ( ph /\ x e. ( ZZ>= ` ( M + 1 ) ) ) -> ( F ` x ) e. D )   =>    |- ( ph -> seq M ( .+ , F ) = ran R )
Theorem	seq3-1 10824*	Value of the sequence builder function at its initial value. (Contributed by Jim Kingdon, 3-Oct-2022.)
|- ( ph -> M e. ZZ )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   =>    |- ( ph -> ( seq M ( .+ , F ) ` M ) = ( F ` M ) )
Theorem	seq1g 10825	Value of the sequence builder function at its initial value. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 19-Aug-2025.)
|- ( ( M e. ZZ /\ F e. V /\ .+ e. W ) -> ( seq M ( .+ , F ) ` M ) = ( F ` M ) )
Theorem	seqf 10826*	Range of the recursive sequence builder. (Contributed by Mario Carneiro, 24-Jun-2013.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ x e. Z ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   =>    |- ( ph -> seq M ( .+ , F ) : Z --> S )
Theorem	seq3p1 10827*	Value of the sequence builder function at a successor. (Contributed by Jim Kingdon, 30-Apr-2022.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   =>    |- ( ph -> ( seq M ( .+ , F ) ` ( N + 1 ) ) = ( ( seq M ( .+ , F ) ` N ) .+ ( F ` ( N + 1 ) ) ) )
Theorem	seqp1g 10828	Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 19-Aug-2025.)
|- ( ( N e. ( ZZ>= ` M ) /\ F e. V /\ .+ e. W ) -> ( seq M ( .+ , F ) ` ( N + 1 ) ) = ( ( seq M ( .+ , F ) ` N ) .+ ( F ` ( N + 1 ) ) ) )
Theorem	seqovcd 10829*	A closure law for the recursive sequence builder. This is a lemma for theorems such as seqf2 10830 and seq1cd 10831 and is unlikely to be needed once such theorems are proved. (Contributed by Jim Kingdon, 20-Jul-2023.)
|- ( ( ph /\ x e. ( ZZ>= ` ( M + 1 ) ) ) -> ( F ` x ) e. D )   &    |- ( ( ph /\ ( x e. C /\ y e. D ) ) -> ( x .+ y ) e. C )   =>    |- ( ( ph /\ ( x e. ( ZZ>= ` M ) /\ y e. C ) ) -> ( x ( z e. ( ZZ>= ` M ) , w e. C |-> ( w .+ ( F ` ( z + 1 ) ) ) ) y ) e. C )
Theorem	seqf2 10830*	Range of the recursive sequence builder. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 7-Jul-2023.)
|- ( ph -> ( F ` M ) e. C )   &    |- ( ( ph /\ ( x e. C /\ y e. D ) ) -> ( x .+ y ) e. C )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ x e. ( ZZ>= ` ( M + 1 ) ) ) -> ( F ` x ) e. D )   =>    |- ( ph -> seq M ( .+ , F ) : Z --> C )
Theorem	seq1cd 10831*	Initial value of the recursive sequence builder. A version of seq3-1 10824 which provides two classes D and C for the terms and the value being accumulated, respectively. (Contributed by Jim Kingdon, 19-Jul-2023.)
|- ( ph -> ( F ` M ) e. C )   &    |- ( ( ph /\ ( x e. C /\ y e. D ) ) -> ( x .+ y ) e. C )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ x e. ( ZZ>= ` ( M + 1 ) ) ) -> ( F ` x ) e. D )   =>    |- ( ph -> ( seq M ( .+ , F ) ` M ) = ( F ` M ) )
Theorem	seqp1cd 10832*	Value of the sequence builder function at a successor. A version of seq3p1 10827 which provides two classes D and C for the terms and the value being accumulated, respectively. (Contributed by Jim Kingdon, 20-Jul-2023.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> ( F ` M ) e. C )   &    |- ( ( ph /\ ( x e. C /\ y e. D ) ) -> ( x .+ y ) e. C )   &    |- ( ( ph /\ x e. ( ZZ>= ` ( M + 1 ) ) ) -> ( F ` x ) e. D )   =>    |- ( ph -> ( seq M ( .+ , F ) ` ( N + 1 ) ) = ( ( seq M ( .+ , F ) ` N ) .+ ( F ` ( N + 1 ) ) ) )
Theorem	seq3clss 10833*	Closure property of the recursive sequence builder. (Contributed by Jim Kingdon, 28-Sep-2022.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. T )   &    |- ( ( ph /\ x e. ( M ... N ) ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ph -> S C_ T )   &    |- ( ( ph /\ ( x e. T /\ y e. T ) ) -> ( x .+ y ) e. T )   =>    |- ( ph -> ( seq M ( .+ , F ) ` N ) e. S )
Theorem	seqclg 10834*	Closure properties of the recursive sequence builder. (Contributed by Mario Carneiro, 2-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ x e. ( M ... N ) ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ph -> F e. V )   &    |- ( ph -> .+ e. W )   =>    |- ( ph -> ( seq M ( .+ , F ) ` N ) e. S )
Theorem	seq3m1 10835*	Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 3-Nov-2022.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ( ZZ>= ` ( M + 1 ) ) )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   =>    |- ( ph -> ( seq M ( .+ , F ) ` N ) = ( ( seq M ( .+ , F ) ` ( N - 1 ) ) .+ ( F ` N ) ) )
Theorem	seqm1g 10836	Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 30-Aug-2025.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ( ZZ>= ` ( M + 1 ) ) )   &    |- ( ph -> .+ e. V )   &    |- ( ph -> F e. W )   =>    |- ( ph -> ( seq M ( .+ , F ) ` N ) = ( ( seq M ( .+ , F ) ` ( N - 1 ) ) .+ ( F ` N ) ) )
Theorem	seq3fveq2 10837*	Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.)
|- ( ph -> K e. ( ZZ>= ` M ) )   &    |- ( ph -> ( seq M ( .+ , F ) ` K ) = ( G ` K ) )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ x e. ( ZZ>= ` K ) ) -> ( G ` x ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ph -> N e. ( ZZ>= ` K ) )   &    |- ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( F ` k ) = ( G ` k ) )   =>    |- ( ph -> ( seq M ( .+ , F ) ` N ) = ( seq K ( .+ , G ) ` N ) )
Theorem	seq3feq2 10838*	Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.)
|- ( ph -> K e. ( ZZ>= ` M ) )   &    |- ( ph -> ( seq M ( .+ , F ) ` K ) = ( G ` K ) )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ x e. ( ZZ>= ` K ) ) -> ( G ` x ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ k e. ( ZZ>= ` ( K + 1 ) ) ) -> ( F ` k ) = ( G ` k ) )   =>    |- ( ph -> ( seq M ( .+ , F ) |` ( ZZ>= ` K ) ) = seq K ( .+ , G ) )
Theorem	seqfveq2g 10839*	Equality of sequences. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.)
|- ( ph -> K e. ( ZZ>= ` M ) )   &    |- ( ph -> ( seq M ( .+ , F ) ` K ) = ( G ` K ) )   &    |- ( ph -> .+ e. V )   &    |- ( ph -> F e. W )   &    |- ( ph -> G e. X )   &    |- ( ph -> N e. ( ZZ>= ` K ) )   &    |- ( ( ph /\ k e. ( ( K + 1 ) ... N ) ) -> ( F ` k ) = ( G ` k ) )   =>    |- ( ph -> ( seq M ( .+ , F ) ` N ) = ( seq K ( .+ , G ) ` N ) )
Theorem	seqfveqg 10840*	Equality of sequences. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) = ( G ` k ) )   &    |- ( ph -> .+ e. V )   &    |- ( ph -> F e. W )   &    |- ( ph -> G e. X )   =>    |- ( ph -> ( seq M ( .+ , F ) ` N ) = ( seq M ( .+ , G ) ` N ) )
Theorem	seq3fveq 10841*	Equality of sequences. (Contributed by Jim Kingdon, 4-Jun-2020.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) = ( G ` k ) )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( G ` x ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   =>    |- ( ph -> ( seq M ( .+ , F ) ` N ) = ( seq M ( .+ , G ) ` N ) )
Theorem	seq3feq 10842*	Equality of sequences. (Contributed by Jim Kingdon, 15-Aug-2021.) (Revised by Jim Kingdon, 7-Apr-2023.)
|- ( ph -> M e. ZZ )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = ( G ` k ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   =>    |- ( ph -> seq M ( .+ , F ) = seq M ( .+ , G ) )
Theorem	seq3shft2 10843*	Shifting the index set of a sequence. (Contributed by Jim Kingdon, 15-Aug-2021.) (Revised by Jim Kingdon, 7-Apr-2023.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> K e. ZZ )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) = ( G ` ( k + K ) ) )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ x e. ( ZZ>= ` ( M + K ) ) ) -> ( G ` x ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   =>    |- ( ph -> ( seq M ( .+ , F ) ` N ) = ( seq ( M + K ) ( .+ , G ) ` ( N + K ) ) )
Theorem	seqshft2g 10844*	Shifting the index set of a sequence. (Contributed by Mario Carneiro, 27-Feb-2014.) (Revised by Mario Carneiro, 27-May-2014.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> K e. ZZ )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) = ( G ` ( k + K ) ) )   &    |- ( ph -> .+ e. V )   &    |- ( ph -> F e. W )   &    |- ( ph -> G e. X )   =>    |- ( ph -> ( seq M ( .+ , F ) ` N ) = ( seq ( M + K ) ( .+ , G ) ` ( N + K ) ) )
Theorem	serf 10845*	An infinite series of complex terms is a function from NN to CC. (Contributed by NM, 18-Apr-2005.) (Revised by Mario Carneiro, 27-May-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   =>    |- ( ph -> seq M ( + , F ) : Z --> CC )
Theorem	serfre 10846*	An infinite series of real numbers is a function from NN to RR. (Contributed by NM, 18-Apr-2005.) (Revised by Mario Carneiro, 27-May-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )   =>    |- ( ph -> seq M ( + , F ) : Z --> RR )
Theorem	monoord 10847*	Ordering relation for a monotonic sequence, increasing case. (Contributed by NM, 13-Mar-2005.) (Revised by Mario Carneiro, 9-Feb-2014.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) -> ( F ` k ) <_ ( F ` ( k + 1 ) ) )   =>    |- ( ph -> ( F ` M ) <_ ( F ` N ) )
Theorem	monoord2 10848*	Ordering relation for a monotonic sequence, decreasing case. (Contributed by Mario Carneiro, 18-Jul-2014.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )   =>    |- ( ph -> ( F ` N ) <_ ( F ` M ) )
Theorem	ser3mono 10849*	The partial sums in an infinite series of positive terms form a monotonic sequence. (Contributed by NM, 17-Mar-2005.) (Revised by Jim Kingdon, 22-Apr-2023.)
|- ( ph -> K e. ( ZZ>= ` M ) )   &    |- ( ph -> N e. ( ZZ>= ` K ) )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. RR )   &    |- ( ( ph /\ x e. ( ( K + 1 ) ... N ) ) -> 0 <_ ( F ` x ) )   =>    |- ( ph -> ( seq M ( + , F ) ` K ) <_ ( seq M ( + , F ) ` N ) )
Theorem	seq3split 10850*	Split a sequence into two sequences. (Contributed by Jim Kingdon, 16-Aug-2021.) (Revised by Jim Kingdon, 21-Oct-2022.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ph -> N e. ( ZZ>= ` ( M + 1 ) ) )   &    |- ( ph -> M e. ( ZZ>= ` K ) )   &    |- ( ( ph /\ x e. ( ZZ>= ` K ) ) -> ( F ` x ) e. S )   =>    |- ( ph -> ( seq K ( .+ , F ) ` N ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` N ) ) )
Theorem	seqsplitg 10851*	Split a sequence into two sequences. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ph -> N e. ( ZZ>= ` ( M + 1 ) ) )   &    |- ( ph -> .+ e. V )   &    |- ( ph -> F e. W )   &    |- ( ph -> M e. ( ZZ>= ` K ) )   &    |- ( ( ph /\ x e. ( K ... N ) ) -> ( F ` x ) e. S )   =>    |- ( ph -> ( seq K ( .+ , F ) ` N ) = ( ( seq K ( .+ , F ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` N ) ) )
Theorem	seq3-1p 10852*	Removing the first term from a sequence. (Contributed by Jim Kingdon, 16-Aug-2021.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ph -> N e. ( ZZ>= ` ( M + 1 ) ) )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   =>    |- ( ph -> ( seq M ( .+ , F ) ` N ) = ( ( F ` M ) .+ ( seq ( M + 1 ) ( .+ , F ) ` N ) ) )
Theorem	seq3caopr3 10853*	Lemma for seq3caopr2 10855. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by Jim Kingdon, 22-Apr-2023.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x Q y ) e. S )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. S )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( G ` k ) e. S )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( H ` k ) = ( ( F ` k ) Q ( G ` k ) ) )   &    |- ( ( ph /\ n e. ( M..^ N ) ) -> ( ( ( seq M ( .+ , F ) ` n ) Q ( seq M ( .+ , G ) ` n ) ) .+ ( ( F ` ( n + 1 ) ) Q ( G ` ( n + 1 ) ) ) ) = ( ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) Q ( ( seq M ( .+ , G ) ` n ) .+ ( G ` ( n + 1 ) ) ) ) )   =>    |- ( ph -> ( seq M ( .+ , H ) ` N ) = ( ( seq M ( .+ , F ) ` N ) Q ( seq M ( .+ , G ) ` N ) ) )
Theorem	seqcaopr3g 10854*	Lemma for seqcaopr2g 10856. (Contributed by Mario Carneiro, 25-Apr-2016.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x Q y ) e. S )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. S )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) e. S )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( H ` k ) = ( ( F ` k ) Q ( G ` k ) ) )   &    |- ( ph -> .+ e. V )   &    |- ( ph -> F e. W )   &    |- ( ph -> G e. X )   &    |- ( ph -> H e. Y )   &    |- ( ( ph /\ n e. ( M..^ N ) ) -> ( ( ( seq M ( .+ , F ) ` n ) Q ( seq M ( .+ , G ) ` n ) ) .+ ( ( F ` ( n + 1 ) ) Q ( G ` ( n + 1 ) ) ) ) = ( ( ( seq M ( .+ , F ) ` n ) .+ ( F ` ( n + 1 ) ) ) Q ( ( seq M ( .+ , G ) ` n ) .+ ( G ` ( n + 1 ) ) ) ) )   =>    |- ( ph -> ( seq M ( .+ , H ) ` N ) = ( ( seq M ( .+ , F ) ` N ) Q ( seq M ( .+ , G ) ` N ) ) )
Theorem	seq3caopr2 10855*	The sum of two infinite series (generalized to an arbitrary commutative and associative operation). (Contributed by Mario Carneiro, 30-May-2014.) (Revised by Jim Kingdon, 23-Apr-2023.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x Q y ) e. S )   &    |- ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) ) -> ( ( x Q z ) .+ ( y Q w ) ) = ( ( x .+ y ) Q ( z .+ w ) ) )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. S )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( G ` k ) e. S )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( H ` k ) = ( ( F ` k ) Q ( G ` k ) ) )   =>    |- ( ph -> ( seq M ( .+ , H ) ` N ) = ( ( seq M ( .+ , F ) ` N ) Q ( seq M ( .+ , G ) ` N ) ) )
Theorem	seqcaopr2g 10856*	The sum of two infinite series (generalized to an arbitrary commutative and associative operation). (Contributed by Mario Carneiro, 30-May-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x Q y ) e. S )   &    |- ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) ) -> ( ( x Q z ) .+ ( y Q w ) ) = ( ( x .+ y ) Q ( z .+ w ) ) )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. S )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) e. S )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( H ` k ) = ( ( F ` k ) Q ( G ` k ) ) )   &    |- ( ph -> .+ e. V )   &    |- ( ph -> F e. W )   &    |- ( ph -> G e. X )   &    |- ( ph -> H e. Y )   =>    |- ( ph -> ( seq M ( .+ , H ) ` N ) = ( ( seq M ( .+ , F ) ` N ) Q ( seq M ( .+ , G ) ` N ) ) )
Theorem	seq3caopr 10857*	The sum of two infinite series (generalized to an arbitrary commutative and associative operation). (Contributed by NM, 17-Mar-2005.) (Revised by Jim Kingdon, 23-Apr-2023.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) = ( y .+ x ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. S )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( G ` k ) e. S )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( H ` k ) = ( ( F ` k ) .+ ( G ` k ) ) )   =>    |- ( ph -> ( seq M ( .+ , H ) ` N ) = ( ( seq M ( .+ , F ) ` N ) .+ ( seq M ( .+ , G ) ` N ) ) )
Theorem	seqcaoprg 10858*	The sum of two infinite series (generalized to an arbitrary commutative and associative operation). (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 30-May-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) = ( y .+ x ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. S )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) e. S )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( H ` k ) = ( ( F ` k ) .+ ( G ` k ) ) )   &    |- ( ph -> .+ e. V )   &    |- ( ph -> F e. W )   &    |- ( ph -> G e. X )   &    |- ( ph -> H e. Y )   =>    |- ( ph -> ( seq M ( .+ , H ) ` N ) = ( ( seq M ( .+ , F ) ` N ) .+ ( seq M ( .+ , G ) ` N ) ) )
Theorem	iseqf1olemkle 10859*	Lemma for seq3f1o 10879. (Contributed by Jim Kingdon, 21-Aug-2022.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> K e. ( M ... N ) )   &    |- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |- ( ph -> A. x e. ( M..^ K ) ( J ` x ) = x )   =>    |- ( ph -> K <_ ( `' J ` K ) )
Theorem	iseqf1olemklt 10860*	Lemma for seq3f1o 10879. (Contributed by Jim Kingdon, 21-Aug-2022.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> K e. ( M ... N ) )   &    |- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |- ( ph -> A. x e. ( M..^ K ) ( J ` x ) = x )   &    |- ( ph -> K =/= ( `' J ` K ) )   =>    |- ( ph -> K < ( `' J ` K ) )
Theorem	iseqf1olemqcl 10861	Lemma for seq3f1o 10879. (Contributed by Jim Kingdon, 27-Aug-2022.)
|- ( ph -> K e. ( M ... N ) )   &    |- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |- ( ph -> A e. ( M ... N ) )   =>    |- ( ph -> if ( A e. ( K ... ( `' J ` K ) ) , if ( A = K , K , ( J ` ( A - 1 ) ) ) , ( J ` A ) ) e. ( M ... N ) )
Theorem	iseqf1olemqval 10862*	Lemma for seq3f1o 10879. Value of the function Q. (Contributed by Jim Kingdon, 28-Aug-2022.)
|- ( ph -> K e. ( M ... N ) )   &    |- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |- ( ph -> A e. ( M ... N ) )   &    |- Q = ( u e. ( M ... N ) |-> if ( u e. ( K ... ( `' J ` K ) ) , if ( u = K , K , ( J ` ( u - 1 ) ) ) , ( J ` u ) ) )   =>    |- ( ph -> ( Q ` A ) = if ( A e. ( K ... ( `' J ` K ) ) , if ( A = K , K , ( J ` ( A - 1 ) ) ) , ( J ` A ) ) )
Theorem	iseqf1olemnab 10863*	Lemma for seq3f1o 10879. (Contributed by Jim Kingdon, 27-Aug-2022.)
|- ( ph -> K e. ( M ... N ) )   &    |- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |- ( ph -> A e. ( M ... N ) )   &    |- ( ph -> B e. ( M ... N ) )   &    |- ( ph -> ( Q ` A ) = ( Q ` B ) )   &    |- Q = ( u e. ( M ... N ) |-> if ( u e. ( K ... ( `' J ` K ) ) , if ( u = K , K , ( J ` ( u - 1 ) ) ) , ( J ` u ) ) )   =>    |- ( ph -> -. ( A e. ( K ... ( `' J ` K ) ) /\ -. B e. ( K ... ( `' J ` K ) ) ) )
Theorem	iseqf1olemab 10864*	Lemma for seq3f1o 10879. (Contributed by Jim Kingdon, 27-Aug-2022.)
|- ( ph -> K e. ( M ... N ) )   &    |- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |- ( ph -> A e. ( M ... N ) )   &    |- ( ph -> B e. ( M ... N ) )   &    |- ( ph -> ( Q ` A ) = ( Q ` B ) )   &    |- Q = ( u e. ( M ... N ) |-> if ( u e. ( K ... ( `' J ` K ) ) , if ( u = K , K , ( J ` ( u - 1 ) ) ) , ( J ` u ) ) )   &    |- ( ph -> A e. ( K ... ( `' J ` K ) ) )   &    |- ( ph -> B e. ( K ... ( `' J ` K ) ) )   =>    |- ( ph -> A = B )
Theorem	iseqf1olemnanb 10865*	Lemma for seq3f1o 10879. (Contributed by Jim Kingdon, 27-Aug-2022.)
|- ( ph -> K e. ( M ... N ) )   &    |- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |- ( ph -> A e. ( M ... N ) )   &    |- ( ph -> B e. ( M ... N ) )   &    |- ( ph -> ( Q ` A ) = ( Q ` B ) )   &    |- Q = ( u e. ( M ... N ) |-> if ( u e. ( K ... ( `' J ` K ) ) , if ( u = K , K , ( J ` ( u - 1 ) ) ) , ( J ` u ) ) )   &    |- ( ph -> -. A e. ( K ... ( `' J ` K ) ) )   &    |- ( ph -> -. B e. ( K ... ( `' J ` K ) ) )   =>    |- ( ph -> A = B )
Theorem	iseqf1olemqf 10866*	Lemma for seq3f1o 10879. Domain and codomain of Q. (Contributed by Jim Kingdon, 26-Aug-2022.)
|- ( ph -> K e. ( M ... N ) )   &    |- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |- Q = ( u e. ( M ... N ) |-> if ( u e. ( K ... ( `' J ` K ) ) , if ( u = K , K , ( J ` ( u - 1 ) ) ) , ( J ` u ) ) )   =>    |- ( ph -> Q : ( M ... N ) --> ( M ... N ) )
Theorem	iseqf1olemmo 10867*	Lemma for seq3f1o 10879. Showing that Q is one-to-one. (Contributed by Jim Kingdon, 27-Aug-2022.)
|- ( ph -> K e. ( M ... N ) )   &    |- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |- Q = ( u e. ( M ... N ) |-> if ( u e. ( K ... ( `' J ` K ) ) , if ( u = K , K , ( J ` ( u - 1 ) ) ) , ( J ` u ) ) )   &    |- ( ph -> A e. ( M ... N ) )   &    |- ( ph -> B e. ( M ... N ) )   &    |- ( ph -> ( Q ` A ) = ( Q ` B ) )   =>    |- ( ph -> A = B )
Theorem	iseqf1olemqf1o 10868*	Lemma for seq3f1o 10879. Q is a permutation of ( M ... N ). Q is formed from the constant portion of J, followed by the single element K (at position K), followed by the rest of J (with the K deleted and the elements before K moved one position later to fill the gap). (Contributed by Jim Kingdon, 21-Aug-2022.)
|- ( ph -> K e. ( M ... N ) )   &    |- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |- Q = ( u e. ( M ... N ) |-> if ( u e. ( K ... ( `' J ` K ) ) , if ( u = K , K , ( J ` ( u - 1 ) ) ) , ( J ` u ) ) )   =>    |- ( ph -> Q : ( M ... N ) -1-1-onto-> ( M ... N ) )
Theorem	iseqf1olemqk 10869*	Lemma for seq3f1o 10879. Q is constant for one more position than J is. (Contributed by Jim Kingdon, 21-Aug-2022.)
|- ( ph -> K e. ( M ... N ) )   &    |- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |- Q = ( u e. ( M ... N ) |-> if ( u e. ( K ... ( `' J ` K ) ) , if ( u = K , K , ( J ` ( u - 1 ) ) ) , ( J ` u ) ) )   &    |- ( ph -> A. x e. ( M..^ K ) ( J ` x ) = x )   =>    |- ( ph -> A. x e. ( M ... K ) ( Q ` x ) = x )
Theorem	iseqf1olemjpcl 10870*	Lemma for seq3f1o 10879. A closure lemma involving J and P. (Contributed by Jim Kingdon, 29-Aug-2022.)
|- ( ph -> K e. ( M ... N ) )   &    |- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |- Q = ( u e. ( M ... N ) |-> if ( u e. ( K ... ( `' J ` K ) ) , if ( u = K , K , ( J ` ( u - 1 ) ) ) , ( J ` u ) ) )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( G ` x ) e. S )   &    |- P = ( x e. ( ZZ>= ` M ) |-> if ( x <_ N , ( G ` ( f ` x ) ) , ( G ` M ) ) )   =>    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( [_ J / f ]_ P ` x ) e. S )
Theorem	iseqf1olemqpcl 10871*	Lemma for seq3f1o 10879. A closure lemma involving Q and P. (Contributed by Jim Kingdon, 29-Aug-2022.)
|- ( ph -> K e. ( M ... N ) )   &    |- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |- Q = ( u e. ( M ... N ) |-> if ( u e. ( K ... ( `' J ` K ) ) , if ( u = K , K , ( J ` ( u - 1 ) ) ) , ( J ` u ) ) )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( G ` x ) e. S )   &    |- P = ( x e. ( ZZ>= ` M ) |-> if ( x <_ N , ( G ` ( f ` x ) ) , ( G ` M ) ) )   =>    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( [_ Q / f ]_ P ` x ) e. S )
Theorem	iseqf1olemfvp 10872*	Lemma for seq3f1o 10879. (Contributed by Jim Kingdon, 30-Aug-2022.)
|- ( ph -> K e. ( M ... N ) )   &    |- ( ph -> T : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |- ( ph -> A e. ( M ... N ) )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( G ` x ) e. S )   &    |- P = ( x e. ( ZZ>= ` M ) |-> if ( x <_ N , ( G ` ( f ` x ) ) , ( G ` M ) ) )   =>    |- ( ph -> ( [_ T / f ]_ P ` A ) = ( G ` ( T ` A ) ) )
Theorem	seq3f1olemqsumkj 10873*	Lemma for seq3f1o 10879. Q gives the same sum as J in the range ( K ... ( `' J ` K ) ). (Contributed by Jim Kingdon, 29-Aug-2022.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) = ( y .+ x ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> F : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( G ` x ) e. S )   &    |- ( ph -> K e. ( M ... N ) )   &    |- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |- ( ph -> A. x e. ( M..^ K ) ( J ` x ) = x )   &    |- ( ph -> K =/= ( `' J ` K ) )   &    |- Q = ( u e. ( M ... N ) |-> if ( u e. ( K ... ( `' J ` K ) ) , if ( u = K , K , ( J ` ( u - 1 ) ) ) , ( J ` u ) ) )   &    |- P = ( x e. ( ZZ>= ` M ) |-> if ( x <_ N , ( G ` ( f ` x ) ) , ( G ` M ) ) )   =>    |- ( ph -> ( seq K ( .+ , [_ J / f ]_ P ) ` ( `' J ` K ) ) = ( seq K ( .+ , [_ Q / f ]_ P ) ` ( `' J ` K ) ) )
Theorem	seq3f1olemqsumk 10874*	Lemma for seq3f1o 10879. Q gives the same sum as J in the range ( K ... N ). (Contributed by Jim Kingdon, 22-Aug-2022.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) = ( y .+ x ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> F : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( G ` x ) e. S )   &    |- ( ph -> K e. ( M ... N ) )   &    |- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |- ( ph -> A. x e. ( M..^ K ) ( J ` x ) = x )   &    |- ( ph -> K =/= ( `' J ` K ) )   &    |- Q = ( u e. ( M ... N ) |-> if ( u e. ( K ... ( `' J ` K ) ) , if ( u = K , K , ( J ` ( u - 1 ) ) ) , ( J ` u ) ) )   &    |- P = ( x e. ( ZZ>= ` M ) |-> if ( x <_ N , ( G ` ( f ` x ) ) , ( G ` M ) ) )   =>    |- ( ph -> ( seq K ( .+ , [_ J / f ]_ P ) ` N ) = ( seq K ( .+ , [_ Q / f ]_ P ) ` N ) )
Theorem	seq3f1olemqsum 10875*	Lemma for seq3f1o 10879. Q gives the same sum as J. (Contributed by Jim Kingdon, 21-Aug-2022.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) = ( y .+ x ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> F : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( G ` x ) e. S )   &    |- ( ph -> K e. ( M ... N ) )   &    |- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |- ( ph -> A. x e. ( M..^ K ) ( J ` x ) = x )   &    |- ( ph -> K =/= ( `' J ` K ) )   &    |- Q = ( u e. ( M ... N ) |-> if ( u e. ( K ... ( `' J ` K ) ) , if ( u = K , K , ( J ` ( u - 1 ) ) ) , ( J ` u ) ) )   &    |- P = ( x e. ( ZZ>= ` M ) |-> if ( x <_ N , ( G ` ( f ` x ) ) , ( G ` M ) ) )   =>    |- ( ph -> ( seq M ( .+ , [_ J / f ]_ P ) ` N ) = ( seq M ( .+ , [_ Q / f ]_ P ) ` N ) )
Theorem	seq3f1olemstep 10876*	Lemma for seq3f1o 10879. Given a permutation which is constant up to a point, supply a new one which is constant for one more position. (Contributed by Jim Kingdon, 19-Aug-2022.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) = ( y .+ x ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> F : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( G ` x ) e. S )   &    |- ( ph -> K e. ( M ... N ) )   &    |- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |- ( ph -> A. x e. ( M..^ K ) ( J ` x ) = x )   &    |- ( ph -> ( seq M ( .+ , [_ J / f ]_ P ) ` N ) = ( seq M ( .+ , L ) ` N ) )   &    |- P = ( x e. ( ZZ>= ` M ) |-> if ( x <_ N , ( G ` ( f ` x ) ) , ( G ` M ) ) )   =>    |- ( ph -> E. f ( f : ( M ... N ) -1-1-onto-> ( M ... N ) /\ A. x e. ( M ... K ) ( f ` x ) = x /\ ( seq M ( .+ , P ) ` N ) = ( seq M ( .+ , L ) ` N ) ) )
Theorem	seq3f1olemp 10877*	Lemma for seq3f1o 10879. Existence of a constant permutation of ( M ... N ) which leads to the same sum as the permutation F itself. (Contributed by Jim Kingdon, 18-Aug-2022.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) = ( y .+ x ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> F : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( G ` x ) e. S )   &    |- L = ( x e. ( ZZ>= ` M ) |-> if ( x <_ N , ( G ` ( F ` x ) ) , ( G ` M ) ) )   &    |- P = ( x e. ( ZZ>= ` M ) |-> if ( x <_ N , ( G ` ( f ` x ) ) , ( G ` M ) ) )   =>    |- ( ph -> E. f ( f : ( M ... N ) -1-1-onto-> ( M ... N ) /\ A. x e. ( M ... N ) ( f ` x ) = x /\ ( seq M ( .+ , P ) ` N ) = ( seq M ( .+ , L ) ` N ) ) )
Theorem	seq3f1oleml 10878*	Lemma for seq3f1o 10879. This is more or less the result, but stated in terms of F and G without H. L and H may differ in terms of what happens to terms after N. The terms after N don't matter for the value at N but we need some definition given the way our theorems concerning seq work. (Contributed by Jim Kingdon, 17-Aug-2022.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) = ( y .+ x ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> F : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( G ` x ) e. S )   &    |- L = ( x e. ( ZZ>= ` M ) |-> if ( x <_ N , ( G ` ( F ` x ) ) , ( G ` M ) ) )   =>    |- ( ph -> ( seq M ( .+ , L ) ` N ) = ( seq M ( .+ , G ) ` N ) )
Theorem	seq3f1o 10879*	Rearrange a sum via an arbitrary bijection on ( M ... N ). (Contributed by Mario Carneiro, 27-Feb-2014.) (Revised by Jim Kingdon, 3-Nov-2022.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) = ( y .+ x ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> F : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( G ` x ) e. S )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( H ` x ) e. S )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( H ` k ) = ( G ` ( F ` k ) ) )   =>    |- ( ph -> ( seq M ( .+ , H ) ` N ) = ( seq M ( .+ , G ) ` N ) )
Theorem	seqf1oglem2a 10880*	Lemma for seqf1og 10883. (Contributed by Mario Carneiro, 24-Apr-2016.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x .+ y ) = ( y .+ x ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> C C_ S )   &    |- ( ph -> .+ e. V )   &    |- ( ph -> G : A --> C )   &    |- ( ph -> K e. A )   &    |- ( ph -> ( M ... N ) C_ A )   &    |- ( ph -> A e. W )   =>    |- ( ph -> ( ( G ` K ) .+ ( seq M ( .+ , G ) ` N ) ) = ( ( seq M ( .+ , G ) ` N ) .+ ( G ` K ) ) )
Theorem	seqf1oglem1 10881*	Lemma for seqf1og 10883. (Contributed by Mario Carneiro, 26-Feb-2014.) (Revised by Mario Carneiro, 27-May-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x .+ y ) = ( y .+ x ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> C C_ S )   &    |- ( ph -> .+ e. V )   &    |- ( ph -> F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )   &    |- ( ph -> G : ( M ... ( N + 1 ) ) --> C )   &    |- J = ( k e. ( M ... N ) |-> ( F ` if ( k < K , k , ( k + 1 ) ) ) )   &    |- K = ( `' F ` ( N + 1 ) )   =>    |- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )
Theorem	seqf1oglem2 10882*	Lemma for seqf1og 10883. (Contributed by Mario Carneiro, 27-Feb-2014.) (Revised by Mario Carneiro, 24-Apr-2016.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x .+ y ) = ( y .+ x ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> C C_ S )   &    |- ( ph -> .+ e. V )   &    |- ( ph -> F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )   &    |- ( ph -> G : ( M ... ( N + 1 ) ) --> C )   &    |- J = ( k e. ( M ... N ) |-> ( F ` if ( k < K , k , ( k + 1 ) ) ) )   &    |- K = ( `' F ` ( N + 1 ) )   &    |- ( ph -> A. g A. f ( ( f : ( M ... N ) -1-1-onto-> ( M ... N ) /\ g : ( M ... N ) --> C ) -> ( seq M ( .+ , ( g o. f ) ) ` N ) = ( seq M ( .+ , g ) ` N ) ) )   =>    |- ( ph -> ( seq M ( .+ , ( G o. F ) ) ` ( N + 1 ) ) = ( seq M ( .+ , G ) ` ( N + 1 ) ) )
Theorem	seqf1og 10883*	Rearrange a sum via an arbitrary bijection on ( M ... N ). (Contributed by Mario Carneiro, 27-Feb-2014.) (Revised by Jim Kingdon, 29-Aug-2025.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x .+ y ) = ( y .+ x ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> C C_ S )   &    |- ( ph -> .+ e. V )   &    |- ( ph -> F : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |- ( ( ph /\ x e. ( M ... N ) ) -> ( G ` x ) e. C )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( H ` k ) = ( G ` ( F ` k ) ) )   &    |- ( ph -> G e. W )   &    |- ( ph -> H e. X )   =>    |- ( ph -> ( seq M ( .+ , H ) ` N ) = ( seq M ( .+ , G ) ` N ) )
Theorem	ser3add 10884*	The sum of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Jim Kingdon, 4-Oct-2022.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( G ` k ) e. CC )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( H ` k ) = ( ( F ` k ) + ( G ` k ) ) )   =>    |- ( ph -> ( seq M ( + , H ) ` N ) = ( ( seq M ( + , F ) ` N ) + ( seq M ( + , G ) ` N ) ) )
Theorem	ser3sub 10885*	The difference of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Jim Kingdon, 22-Apr-2023.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( G ` k ) e. CC )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( H ` k ) = ( ( F ` k ) - ( G ` k ) ) )   =>    |- ( ph -> ( seq M ( + , H ) ` N ) = ( ( seq M ( + , F ) ` N ) - ( seq M ( + , G ) ` N ) ) )
Theorem	seq3id3 10886*	A sequence that consists entirely of "zeroes" sums to "zero". More precisely, a constant sequence with value an element which is a .+ -idempotent sums (or " .+'s") to that element. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Jim Kingdon, 8-Apr-2023.)
|- ( ph -> ( Z .+ Z ) = Z )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ x e. ( M ... N ) ) -> ( F ` x ) = Z )   &    |- ( ph -> Z e. S )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   =>    |- ( ph -> ( seq M ( .+ , F ) ` N ) = Z )
Theorem	seq3id 10887*	Discarding the first few terms of a sequence that starts with all zeroes (or any element which is a left-identity for .+) has no effect on its sum. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Jim Kingdon, 8-Apr-2023.)
|- ( ( ph /\ x e. S ) -> ( Z .+ x ) = x )   &    |- ( ph -> Z e. S )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> ( F ` N ) e. S )   &    |- ( ( ph /\ x e. ( M ... ( N - 1 ) ) ) -> ( F ` x ) = Z )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   =>    |- ( ph -> ( seq M ( .+ , F ) |` ( ZZ>= ` N ) ) = seq N ( .+ , F ) )
Theorem	seq3id2 10888*	The last few partial sums of a sequence that ends with all zeroes (or any element which is a right-identity for .+) are all the same. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Jim Kingdon, 12-Nov-2022.)
|- ( ( ph /\ x e. S ) -> ( x .+ Z ) = x )   &    |- ( ph -> K e. ( ZZ>= ` M ) )   &    |- ( ph -> N e. ( ZZ>= ` K ) )   &    |- ( ph -> ( seq M ( .+ , F ) ` K ) e. S )   &    |- ( ( ph /\ x e. ( ( K + 1 ) ... N ) ) -> ( F ` x ) = Z )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   =>    |- ( ph -> ( seq M ( .+ , F ) ` K ) = ( seq M ( .+ , F ) ` N ) )
Theorem	seq3homo 10889*	Apply a homomorphism to a sequence. (Contributed by Jim Kingdon, 10-Oct-2022.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( H ` ( x .+ y ) ) = ( ( H ` x ) Q ( H ` y ) ) )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( H ` ( F ` x ) ) = ( G ` x ) )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( G ` x ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x Q y ) e. S )   =>    |- ( ph -> ( H ` ( seq M ( .+ , F ) ` N ) ) = ( seq M ( Q , G ) ` N ) )
Theorem	seq3z 10890*	If the operation .+ has an absorbing element Z (a.k.a. zero element), then any sequence containing a Z evaluates to Z. (Contributed by Mario Carneiro, 27-May-2014.) (Revised by Jim Kingdon, 23-Apr-2023.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ x e. S ) -> ( Z .+ x ) = Z )   &    |- ( ( ph /\ x e. S ) -> ( x .+ Z ) = Z )   &    |- ( ph -> K e. ( M ... N ) )   &    |- ( ph -> ( F ` K ) = Z )   =>    |- ( ph -> ( seq M ( .+ , F ) ` N ) = Z )
Theorem	seqfeq3 10891*	Equality of series under different addition operations which agree on an additively closed subset. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 25-Apr-2016.)
|- ( ph -> M e. ZZ )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) = ( x Q y ) )   =>    |- ( ph -> seq M ( .+ , F ) = seq M ( Q , F ) )
Theorem	seqhomog 10892*	Apply a homomorphism to a sequence. (Contributed by Mario Carneiro, 28-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ x e. ( M ... N ) ) -> ( F ` x ) e. S )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( H ` ( x .+ y ) ) = ( ( H ` x ) Q ( H ` y ) ) )   &    |- ( ( ph /\ x e. ( M ... N ) ) -> ( H ` ( F ` x ) ) = ( G ` x ) )   &    |- ( ph -> F e. V )   &    |- ( ph -> G e. W )   &    |- ( ph -> .+ e. X )   &    |- ( ph -> Q e. Y )   =>    |- ( ph -> ( H ` ( seq M ( .+ , F ) ` N ) ) = ( seq M ( Q , G ) ` N ) )
Theorem	seqfeq4g 10893*	Equality of series under different addition operations which agree on an additively closed subset. (Contributed by Mario Carneiro, 25-Apr-2016.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ x e. ( M ... N ) ) -> ( F ` x ) e. S )   &    |- ( ph -> F e. V )   &    |- ( ph -> .+ e. W )   &    |- ( ph -> Q e. X )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) = ( x Q y ) )   =>    |- ( ph -> ( seq M ( .+ , F ) ` N ) = ( seq M ( Q , F ) ` N ) )
Theorem	seq3distr 10894*	The distributive property for series. (Contributed by Jim Kingdon, 10-Oct-2022.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( C T ( x .+ y ) ) = ( ( C T x ) .+ ( C T y ) ) )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( G ` x ) e. S )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) = ( C T ( G ` x ) ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x T y ) e. S )   &    |- ( ph -> C e. S )   =>    |- ( ph -> ( seq M ( .+ , F ) ` N ) = ( C T ( seq M ( .+ , G ) ` N ) ) )
Theorem	ser0 10895	The value of the partial sums in a zero-valued infinite series. (Contributed by Mario Carneiro, 31-Aug-2013.) (Revised by Mario Carneiro, 15-Dec-2014.)
|- Z = ( ZZ>= ` M )   =>    |- ( N e. Z -> ( seq M ( + , ( Z X. { 0 } ) ) ` N ) = 0 )
Theorem	ser0f 10896	A zero-valued infinite series is equal to the constant zero function. (Contributed by Mario Carneiro, 8-Feb-2014.)
|- Z = ( ZZ>= ` M )   =>    |- ( M e. ZZ -> seq M ( + , ( Z X. { 0 } ) ) = ( Z X. { 0 } ) )
Theorem	fser0const 10897*	Simplifying an expression which turns out just to be a constant zero sequence. (Contributed by Jim Kingdon, 16-Sep-2022.)
|- Z = ( ZZ>= ` M )   =>    |- ( N e. Z -> ( n e. Z |-> if ( n <_ N , ( ( Z X. { 0 } ) ` n ) , 0 ) ) = ( Z X. { 0 } ) )
Theorem	ser3ge0 10898*	A finite sum of nonnegative terms is nonnegative. (Contributed by Mario Carneiro, 8-Feb-2014.) (Revised by Mario Carneiro, 27-May-2014.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> 0 <_ ( F ` k ) )   =>    |- ( ph -> 0 <_ ( seq M ( + , F ) ` N ) )
Theorem	ser3le 10899*	Comparison of partial sums of two infinite series of reals. (Contributed by NM, 27-Dec-2005.) (Revised by Jim Kingdon, 23-Apr-2023.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( G ` k ) e. RR )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) <_ ( G ` k ) )   =>    |- ( ph -> ( seq M ( + , F ) ` N ) <_ ( seq M ( + , G ) ` N ) )
4.6.6  Integer powers
Syntax	cexp 10900	Extend class notation to include exponentiation of a complex number to an integer power.
class ^