P. 93 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9201-9300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	frecuzrdgsuc 9201*	Successor value of a recursive definition generator on upper integers. See comment in frec2uz0d 9185 for the description of G as the mapping from om to ( ZZ>= ` C ). (Contributed by Jim Kingdon, 28-May-2020.)
|- ( ph -> C e. ZZ )   &    |- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , C )   &    |- ( ph -> S e. V )   &    |- ( ph -> A e. S )   &    |- ( ( ph /\ ( x e. ( ZZ>= ` C ) /\ y e. S ) ) -> ( x F y ) e. S )   &    |- R = frec ( ( x e. ( ZZ>= ` C ) , y e. S |-> <. ( x + 1 ) , ( x F y ) >. ) , <. C , A >. )   &    |- ( ph -> T = ran R )   =>    |- ( ( ph /\ B e. ( ZZ>= ` C ) ) -> ( T ` ( B + 1 ) ) = ( B F ( T ` B ) ) )
Theorem	uzenom 9202	An upper integer set is denumerable. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- Z = ( ZZ>= ` M )   =>    |- ( M e. ZZ -> Z ~~ om )
Theorem	frecfzennn 9203	The cardinality of a finite set of sequential integers. (See frec2uz0d 9185 for a description of the hypothesis.) (Contributed by Jim Kingdon, 18-May-2020.)
|- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   =>    |- ( N e. NN0 -> ( 1 ... N ) ~~ ( `' G ` N ) )
Theorem	frecfzen2 9204	The cardinality of a finite set of sequential integers with arbitrary endpoints. (Contributed by Jim Kingdon, 18-May-2020.)
|- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   =>    |- ( N e. ( ZZ>= ` M ) -> ( M ... N ) ~~ ( `' G ` ( ( N + 1 ) - M ) ) )
Theorem	frechashgf1o 9205	G maps om one-to-one onto NN0. (Contributed by Jim Kingdon, 19-May-2020.)
|- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   =>    |- G : om -1-1-onto-> NN0
Theorem	fzfig 9206	A finite interval of integers is finite. (Contributed by Jim Kingdon, 19-May-2020.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M ... N ) e. Fin )
Theorem	fzfigd 9207	Deduction form of fzfig 9206. (Contributed by Jim Kingdon, 21-May-2020.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   =>    |- ( ph -> ( M ... N ) e. Fin )
Theorem	fzofig 9208	Half-open integer sets are finite. (Contributed by Jim Kingdon, 21-May-2020.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M..^ N ) e. Fin )
Theorem	nn0ennn 9209	The nonnegative integers are equinumerous to the positive integers. (Contributed by NM, 19-Jul-2004.)
|- NN0 ~~ NN
Theorem	nnenom 9210	The set of positive integers (as a subset of complex numbers) is equinumerous to omega (the set of finite ordinal numbers). (Contributed by NM, 31-Jul-2004.) (Revised by Mario Carneiro, 15-Sep-2013.)
|- NN ~~ om
3.6.4  The infinite sequence builder "seq"
Syntax	cseq 9211	Extend class notation with recursive sequence builder.
class seq M ( .+ , F , S )
Definition	df-iseq 9212*	Define a general-purpose operation that builds a recursive sequence (i.e. a function on the positive integers NN or some other upper integer set) 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 iseq1 9222 and iseqp1 9225. 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 , QQ ) with values 1, 3/2, 7/4, 15/8,.., so that ( seq 1 ( + , F , QQ ) ` 1 ) = 1, ( seq 1 ( + , F , QQ ) ` 2 ) = 3/2, etc. In other words, seq M ( + , F , QQ ) transforms a sequence F into an infinite series. 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 Jim Kingdon, 29-May-2020.)
|- seq M ( .+ , F , S ) = ran frec ( ( x e. ( ZZ>= ` M ) , y e. S |-> <. ( x + 1 ) , ( y .+ ( F ` ( x + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
Theorem	iseqex 9213	Existence of the sequence builder operation. (Contributed by Jim Kingdon, 20-Aug-2021.)
|- seq M ( .+ , F , S ) e. _V
Theorem	iseqeq1 9214	Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
|- ( M = N -> seq M ( .+ , F , S ) = seq N ( .+ , F , S ) )
Theorem	iseqeq2 9215	Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
|- ( .+ = Q -> seq M ( .+ , F , S ) = seq M ( Q , F , S ) )
Theorem	iseqeq3 9216	Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
|- ( F = G -> seq M ( .+ , F , S ) = seq M ( .+ , G , S ) )
Theorem	iseqeq4 9217	Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
|- ( S = T -> seq M ( .+ , F , S ) = seq M ( .+ , F , T ) )
Theorem	nfiseq 9218	Hypothesis builder for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
|- F/_ x M   &    |- F/_ x .+   &    |- F/_ x F   &    |- F/_ x S   =>    |- F/_ x seq M ( .+ , F , S )
Theorem	iseqovex 9219*	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	iseqval 9220*	Value of the sequence builder function. (Contributed by Jim Kingdon, 30-May-2020.)
|- R = frec ( ( x e. ( ZZ>= ` M ) , y e. S |-> <. ( 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 , S ) = ran R )
Theorem	iseqfn 9221*	The sequence builder function is a function. (Contributed by Jim Kingdon, 30-May-2020.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> S e. V )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   =>    |- ( ph -> seq M ( .+ , F , S ) Fn ( ZZ>= ` M ) )
Theorem	iseq1 9222*	Value of the sequence builder function at its initial value. (Contributed by Jim Kingdon, 31-May-2020.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> S e. V )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   =>    |- ( ph -> ( seq M ( .+ , F , S ) ` M ) = ( F ` M ) )
Theorem	iseqcl 9223*	Closure properties of the recursive sequence builder. (Contributed by Jim Kingdon, 1-Jun-2020.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> S e. V )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   =>    |- ( ph -> ( seq M ( .+ , F , S ) ` N ) e. S )
Theorem	iseqf 9224*	Range of the recursive sequence builder. (Contributed by Jim Kingdon, 23-Jul-2021.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> S e. V )   &    |- ( 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 , S ) : Z --> S )
Theorem	iseqp1 9225*	Value of the sequence builder function at a successor. (Contributed by Jim Kingdon, 31-May-2020.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> S e. V )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   =>    |- ( ph -> ( seq M ( .+ , F , S ) ` ( N + 1 ) ) = ( ( seq M ( .+ , F , S ) ` N ) .+ ( F ` ( N + 1 ) ) ) )
Theorem	iseqss 9226*	Specifying a larger universe for seq. As long as F and .+ are closed over S, then any set which contains S can be used as the last argument to seq. This theorem does not allow T to be a proper class, however. It also currently requires that .+ be closed over T (as well as S). (Contributed by Jim Kingdon, 18-Aug-2021.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> T e. V )   &    |- ( ph -> S C_ T )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ ( x e. T /\ y e. T ) ) -> ( x .+ y ) e. T )   =>    |- ( ph -> seq M ( .+ , F , S ) = seq M ( .+ , F , T ) )
Theorem	iseqm1 9227*	Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ( ZZ>= ` ( M + 1 ) ) )   &    |- ( ph -> S e. V )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   =>    |- ( ph -> ( seq M ( .+ , F , S ) ` N ) = ( ( seq M ( .+ , F , S ) ` ( N - 1 ) ) .+ ( F ` N ) ) )
Theorem	iseqfveq2 9228*	Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.)
|- ( ph -> K e. ( ZZ>= ` M ) )   &    |- ( ph -> ( seq M ( .+ , F , S ) ` K ) = ( G ` K ) )   &    |- ( ph -> S e. V )   &    |- ( ( 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 , S ) ` N ) = ( seq K ( .+ , G , S ) ` N ) )
Theorem	iseqfeq2 9229*	Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.)
|- ( ph -> K e. ( ZZ>= ` M ) )   &    |- ( ph -> ( seq M ( .+ , F , S ) ` K ) = ( G ` K ) )   &    |- ( ph -> S e. V )   &    |- ( ( 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 , S ) |` ( ZZ>= ` K ) ) = seq K ( .+ , G , S ) )
Theorem	iseqfveq 9230*	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 -> S e. V )   &    |- ( ( 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 , S ) ` N ) = ( seq M ( .+ , G , S ) ` N ) )
Theorem	iseqfeq 9231*	Equality of sequences. (Contributed by Jim Kingdon, 15-Aug-2021.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> S e. V )   &    |- ( ( 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 , S ) = seq M ( .+ , G , S ) )
Theorem	iseqshft2 9232*	Shifting the index set of a sequence. (Contributed by Jim Kingdon, 15-Aug-2021.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ph -> K e. ZZ )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) = ( G ` ( k + K ) ) )   &    |- ( ph -> S e. V )   &    |- ( ( 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 , S ) ` N ) = ( seq ( M + K ) ( .+ , G , S ) ` ( N + K ) ) )
Theorem	iserf 9233*	An infinite series of complex terms is a function from NN to CC. (Contributed by Jim Kingdon, 15-Aug-2021.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )   =>    |- ( ph -> seq M ( + , F , CC ) : Z --> CC )
Theorem	iserfre 9234*	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 , RR ) : Z --> RR )
Theorem	monoord 9235*	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 9236*	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	isermono 9237*	The partial sums in an infinite series of positive terms form a monotonic sequence. (Contributed by Jim Kingdon, 15-Aug-2021.)
|- ( 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 , RR ) ` K ) <_ ( seq M ( + , F , RR ) ` N ) )
Theorem	iseqsplit 9238*	Split a sequence into two sequences. (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 -> S e. V )   &    |- ( ph -> M e. ( ZZ>= ` K ) )   &    |- ( ( ph /\ x e. ( ZZ>= ` K ) ) -> ( F ` x ) e. S )   =>    |- ( ph -> ( seq K ( .+ , F , S ) ` N ) = ( ( seq K ( .+ , F , S ) ` M ) .+ ( seq ( M + 1 ) ( .+ , F , S ) ` N ) ) )
Theorem	iseq1p 9239*	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 -> S e. V )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   =>    |- ( ph -> ( seq M ( .+ , F , S ) ` N ) = ( ( F ` M ) .+ ( seq ( M + 1 ) ( .+ , F , S ) ` N ) ) )
Theorem	iseqcaopr3 9240*	Lemma for iseqcaopr2 . (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 ) ) -> ( 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 , S ) ` n ) Q ( seq M ( .+ , G , S ) ` n ) ) .+ ( ( F ` ( n + 1 ) ) Q ( G ` ( n + 1 ) ) ) ) = ( ( ( seq M ( .+ , F , S ) ` n ) .+ ( F ` ( n + 1 ) ) ) Q ( ( seq M ( .+ , G , S ) ` n ) .+ ( G ` ( n + 1 ) ) ) ) )   &    |- ( ph -> S e. V )   =>    |- ( ph -> ( seq M ( .+ , H , S ) ` N ) = ( ( seq M ( .+ , F , S ) ` N ) Q ( seq M ( .+ , G , S ) ` N ) ) )
Theorem	iseqcaopr2 9241*	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. ( 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 -> S e. V )   =>    |- ( ph -> ( seq M ( .+ , H , S ) ` N ) = ( ( seq M ( .+ , F , S ) ` N ) Q ( seq M ( .+ , G , S ) ` N ) ) )
Theorem	iseqcaopr 9242*	The sum of two infinite series (generalized to an arbitrary commutative and associative operation). (Contributed by Jim Kingdon, 17-Aug-2021.)
|- ( ( 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 -> S e. V )   =>    |- ( ph -> ( seq M ( .+ , H , S ) ` N ) = ( ( seq M ( .+ , F , S ) ` N ) .+ ( seq M ( .+ , G , S ) ` N ) ) )
Theorem	iseradd 9243*	The sum of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 26-May-2014.)
|- ( 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 , CC ) ` N ) = ( ( seq M ( + , F , CC ) ` N ) + ( seq M ( + , G , CC ) ` N ) ) )
Theorem	isersub 9244*	The difference of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.)
|- ( 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 , CC ) ` N ) = ( ( seq M ( + , F , CC ) ` N ) - ( seq M ( + , G , CC ) ` N ) ) )
Theorem	iseqid3 9245*	A sequence that consists entirely of zeroes (or whatever the identity Z is for operation .+) sums to zero. (Contributed by Jim Kingdon, 18-Aug-2021.)
|- ( ph -> ( Z .+ Z ) = Z )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) = Z )   &    |- ( ph -> Z e. V )   =>    |- ( ph -> ( seq M ( .+ , F , { Z } ) ` N ) = Z )
Theorem	iseqid3s 9246*	A sequence that consists of zeroes up to N sums to zero at N. In this case by "zero" we mean whatever the identity Z is for the operation .+). (Contributed by Jim Kingdon, 18-Aug-2021.)
|- ( ph -> ( Z .+ Z ) = Z )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ x e. ( M ... N ) ) -> ( F ` x ) = Z )   &    |- ( ph -> Z e. S )   &    |- ( ph -> S e. V )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   =>    |- ( ph -> ( seq M ( .+ , F , S ) ` N ) = Z )
Theorem	iseqid 9247*	Discard the first few terms of a sequence that starts with all zeroes (or whatever the identity Z is for operation .+). (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.)
|- ( ( 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 -> S e. V )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   =>    |- ( ph -> ( seq M ( .+ , F , S ) |` ( ZZ>= ` N ) ) = seq N ( .+ , F , S ) )
Theorem	iseqhomo 9248*	Apply a homomorphism to a sequence. (Contributed by Jim Kingdon, 21-Aug-2021.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   &    |- ( ph -> S e. V )   &    |- ( 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 , S ) ` N ) ) = ( seq M ( Q , G , S ) ` N ) )
Theorem	iseqdistr 9249*	The distributive property for series. (Contributed by Jim Kingdon, 21-Aug-2021.)
|- ( ( 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 -> S e. V )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x T y ) e. S )   &    |- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )   &    |- ( ph -> C e. S )   =>    |- ( ph -> ( seq M ( .+ , F , S ) ` N ) = ( C T ( seq M ( .+ , G , S ) ` N ) ) )
Theorem	iser0 9250	The value of the partial sums in a zero-valued infinite series. (Contributed by Jim Kingdon, 19-Aug-2021.)
|- Z = ( ZZ>= ` M )   =>    |- ( N e. Z -> ( seq M ( + , ( Z X. { 0 } ) , CC ) ` N ) = 0 )
Theorem	iser0f 9251	A zero-valued infinite series is equal to the constant zero function. (Contributed by Jim Kingdon, 19-Aug-2021.)
|- Z = ( ZZ>= ` M )   =>    |- ( M e. ZZ -> seq M ( + , ( Z X. { 0 } ) , CC ) = ( Z X. { 0 } ) )
Theorem	serige0 9252*	A finite sum of nonnegative terms is nonnegative. (Contributed by Jim Kingdon, 22-Aug-2021.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> 0 <_ ( F ` k ) )   =>    |- ( ph -> 0 <_ ( seq M ( + , F , CC ) ` N ) )
Theorem	serile 9253*	Comparison of partial sums of two infinite series of reals. (Contributed by Jim Kingdon, 22-Aug-2021.)
|- ( 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 , CC ) ` N ) <_ ( seq M ( + , G , CC ) ` N ) )
3.6.5  Integer powers
Syntax	cexp 9254	Extend class notation to include exponentiation of a complex number to an integer power.
class ^
Definition	df-iexp 9255*	Define exponentiation to nonnegative integer powers. This definition is not meant to be used directly; instead, exp0 9259 and expp1 9262 provide the standard recursive definition. The up-arrow notation is used by Donald Knuth for iterated exponentiation (Science 194, 1235-1242, 1976) and is convenient for us since we don't have superscripts. 10-Jun-2005: The definition was extended to include zero exponents, so that 0 ^ 0 = 1 per the convention of Definition 10-4.1 of [Gleason] p. 134. 4-Jun-2014: The definition was extended to include negative integer exponents. The case x = 0 , y < 0 gives the value ( 1 / 0 ), so we will avoid this case in our theorems. (Contributed by Jim Kingdon, 7-Jun-2020.)
|- ^ = ( x e. CC , y e. ZZ |-> if ( y = 0 , 1 , if ( 0 < y , ( seq 1 ( x. , ( NN X. { x } ) , CC ) ` y ) , ( 1 / ( seq 1 ( x. , ( NN X. { x } ) , CC ) ` -u y ) ) ) ) )
Theorem	expivallem 9256	Lemma for expival 9257. If we take a complex number apart from zero and raise it to a positive integer power, the result is apart from zero. (Contributed by Jim Kingdon, 7-Jun-2020.)
|- ( ( A e. CC /\ A # 0 /\ N e. NN ) -> ( seq 1 ( x. , ( NN X. { A } ) , CC ) ` N ) # 0 )
Theorem	expival 9257	Value of exponentiation to integer powers. (Contributed by Jim Kingdon, 7-Jun-2020.)
|- ( ( A e. CC /\ N e. ZZ /\ ( A # 0 \/ 0 <_ N ) ) -> ( A ^ N ) = if ( N = 0 , 1 , if ( 0 < N , ( seq 1 ( x. , ( NN X. { A } ) , CC ) ` N ) , ( 1 / ( seq 1 ( x. , ( NN X. { A } ) , CC ) ` -u N ) ) ) ) )
Theorem	expinnval 9258	Value of exponentiation to positive integer powers. (Contributed by Jim Kingdon, 8-Jun-2020.)
|- ( ( A e. CC /\ N e. NN ) -> ( A ^ N ) = ( seq 1 ( x. , ( NN X. { A } ) , CC ) ` N ) )
Theorem	exp0 9259	Value of a complex number raised to the 0th power. Note that under our definition, 0 ^ 0 = 1, following the convention used by Gleason. Part of Definition 10-4.1 of [Gleason] p. 134. (Contributed by NM, 20-May-2004.) (Revised by Mario Carneiro, 4-Jun-2014.)
|- ( A e. CC -> ( A ^ 0 ) = 1 )
Theorem	0exp0e1 9260	0 ^ 0 = 1 (common case). This is our convention. It follows the convention used by Gleason; see Part of Definition 10-4.1 of [Gleason] p. 134. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( 0 ^ 0 ) = 1
Theorem	exp1 9261	Value of a complex number raised to the first power. (Contributed by NM, 20-Oct-2004.) (Revised by Mario Carneiro, 2-Jul-2013.)
|- ( A e. CC -> ( A ^ 1 ) = A )
Theorem	expp1 9262	Value of a complex number raised to a nonnegative integer power plus one. Part of Definition 10-4.1 of [Gleason] p. 134. (Contributed by NM, 20-May-2005.) (Revised by Mario Carneiro, 2-Jul-2013.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( A ^ ( N + 1 ) ) = ( ( A ^ N ) x. A ) )
Theorem	expnegap0 9263	Value of a complex number raised to a negative integer power. (Contributed by Jim Kingdon, 8-Jun-2020.)
|- ( ( A e. CC /\ A # 0 /\ N e. NN0 ) -> ( A ^ -u N ) = ( 1 / ( A ^ N ) ) )
Theorem	expineg2 9264	Value of a complex number raised to a negative integer power. (Contributed by Jim Kingdon, 8-Jun-2020.)
|- ( ( ( A e. CC /\ A # 0 ) /\ ( N e. CC /\ -u N e. NN0 ) ) -> ( A ^ N ) = ( 1 / ( A ^ -u N ) ) )
Theorem	expn1ap0 9265	A number to the negative one power is the reciprocal. (Contributed by Jim Kingdon, 8-Jun-2020.)
|- ( ( A e. CC /\ A # 0 ) -> ( A ^ -u 1 ) = ( 1 / A ) )
Theorem	expcllem 9266*	Lemma for proving nonnegative integer exponentiation closure laws. (Contributed by NM, 14-Dec-2005.)
|- F C_ CC   &    |- ( ( x e. F /\ y e. F ) -> ( x x. y ) e. F )   &    |- 1 e. F   =>    |- ( ( A e. F /\ B e. NN0 ) -> ( A ^ B ) e. F )
Theorem	expcl2lemap 9267*	Lemma for proving integer exponentiation closure laws. (Contributed by Jim Kingdon, 8-Jun-2020.)
|- F C_ CC   &    |- ( ( x e. F /\ y e. F ) -> ( x x. y ) e. F )   &    |- 1 e. F   &    |- ( ( x e. F /\ x # 0 ) -> ( 1 / x ) e. F )   =>    |- ( ( A e. F /\ A # 0 /\ B e. ZZ ) -> ( A ^ B ) e. F )
Theorem	nnexpcl 9268	Closure of exponentiation of nonnegative integers. (Contributed by NM, 16-Dec-2005.)
|- ( ( A e. NN /\ N e. NN0 ) -> ( A ^ N ) e. NN )
Theorem	nn0expcl 9269	Closure of exponentiation of nonnegative integers. (Contributed by NM, 14-Dec-2005.)
|- ( ( A e. NN0 /\ N e. NN0 ) -> ( A ^ N ) e. NN0 )
Theorem	zexpcl 9270	Closure of exponentiation of integers. (Contributed by NM, 16-Dec-2005.)
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( A ^ N ) e. ZZ )
Theorem	qexpcl 9271	Closure of exponentiation of rationals. (Contributed by NM, 16-Dec-2005.)
|- ( ( A e. QQ /\ N e. NN0 ) -> ( A ^ N ) e. QQ )
Theorem	reexpcl 9272	Closure of exponentiation of reals. (Contributed by NM, 14-Dec-2005.)
|- ( ( A e. RR /\ N e. NN0 ) -> ( A ^ N ) e. RR )
Theorem	expcl 9273	Closure law for nonnegative integer exponentiation. (Contributed by NM, 26-May-2005.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( A ^ N ) e. CC )
Theorem	rpexpcl 9274	Closure law for exponentiation of positive reals. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 9-Sep-2014.)
|- ( ( A e. RR+ /\ N e. ZZ ) -> ( A ^ N ) e. RR+ )
Theorem	reexpclzap 9275	Closure of exponentiation of reals. (Contributed by Jim Kingdon, 9-Jun-2020.)
|- ( ( A e. RR /\ A # 0 /\ N e. ZZ ) -> ( A ^ N ) e. RR )
Theorem	qexpclz 9276	Closure of exponentiation of rational numbers. (Contributed by Mario Carneiro, 9-Sep-2014.)
|- ( ( A e. QQ /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ N ) e. QQ )
Theorem	m1expcl2 9277	Closure of exponentiation of negative one. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- ( N e. ZZ -> ( -u 1 ^ N ) e. { -u 1 , 1 } )
Theorem	m1expcl 9278	Closure of exponentiation of negative one. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- ( N e. ZZ -> ( -u 1 ^ N ) e. ZZ )
Theorem	expclzaplem 9279*	Closure law for integer exponentiation. Lemma for expclzap 9280 and expap0i 9287. (Contributed by Jim Kingdon, 9-Jun-2020.)
|- ( ( A e. CC /\ A # 0 /\ N e. ZZ ) -> ( A ^ N ) e. { z e. CC | z # 0 } )
Theorem	expclzap 9280	Closure law for integer exponentiation. (Contributed by Jim Kingdon, 9-Jun-2020.)
|- ( ( A e. CC /\ A # 0 /\ N e. ZZ ) -> ( A ^ N ) e. CC )
Theorem	nn0expcli 9281	Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A e. NN0   &    |- N e. NN0   =>    |- ( A ^ N ) e. NN0
Theorem	nn0sqcl 9282	The square of a nonnegative integer is a nonnegative integer. (Contributed by Stefan O'Rear, 16-Oct-2014.)
|- ( A e. NN0 -> ( A ^ 2 ) e. NN0 )
Theorem	expm1t 9283	Exponentiation in terms of predecessor exponent. (Contributed by NM, 19-Dec-2005.)
|- ( ( A e. CC /\ N e. NN ) -> ( A ^ N ) = ( ( A ^ ( N - 1 ) ) x. A ) )
Theorem	1exp 9284	Value of one raised to a nonnegative integer power. (Contributed by NM, 15-Dec-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
|- ( N e. ZZ -> ( 1 ^ N ) = 1 )
Theorem	expap0 9285	Positive integer exponentiation is apart from zero iff its mantissa is apart from zero. That it is easier to prove this first, and then prove expeq0 9286 in terms of it, rather than the other way around, is perhaps an illustration of the maxim "In constructive analysis, the apartness is more basic [ than ] equality." ([Geuvers], p. 1). (Contributed by Jim Kingdon, 10-Jun-2020.)
|- ( ( A e. CC /\ N e. NN ) -> ( ( A ^ N ) # 0 <-> A # 0 ) )
Theorem	expeq0 9286	Positive integer exponentiation is 0 iff its mantissa is 0. (Contributed by NM, 23-Feb-2005.)
|- ( ( A e. CC /\ N e. NN ) -> ( ( A ^ N ) = 0 <-> A = 0 ) )
Theorem	expap0i 9287	Integer exponentiation is apart from zero if its mantissa is apart from zero. (Contributed by Jim Kingdon, 10-Jun-2020.)
|- ( ( A e. CC /\ A # 0 /\ N e. ZZ ) -> ( A ^ N ) # 0 )
Theorem	expgt0 9288	Nonnegative integer exponentiation with a positive mantissa is positive. (Contributed by NM, 16-Dec-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
|- ( ( A e. RR /\ N e. ZZ /\ 0 < A ) -> 0 < ( A ^ N ) )
Theorem	expnegzap 9289	Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 4-Jun-2014.)
|- ( ( A e. CC /\ A # 0 /\ N e. ZZ ) -> ( A ^ -u N ) = ( 1 / ( A ^ N ) ) )
Theorem	0exp 9290	Value of zero raised to a positive integer power. (Contributed by NM, 19-Aug-2004.)
|- ( N e. NN -> ( 0 ^ N ) = 0 )
Theorem	expge0 9291	Nonnegative integer exponentiation with a nonnegative mantissa is nonnegative. (Contributed by NM, 16-Dec-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
|- ( ( A e. RR /\ N e. NN0 /\ 0 <_ A ) -> 0 <_ ( A ^ N ) )
Theorem	expge1 9292	Nonnegative integer exponentiation with a mantissa greater than or equal to 1 is greater than or equal to 1. (Contributed by NM, 21-Feb-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
|- ( ( A e. RR /\ N e. NN0 /\ 1 <_ A ) -> 1 <_ ( A ^ N ) )
Theorem	expgt1 9293	Positive integer exponentiation with a mantissa greater than 1 is greater than 1. (Contributed by NM, 13-Feb-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
|- ( ( A e. RR /\ N e. NN /\ 1 < A ) -> 1 < ( A ^ N ) )
Theorem	mulexp 9294	Positive integer exponentiation of a product. Proposition 10-4.2(c) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by NM, 13-Feb-2005.)
|- ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> ( ( A x. B ) ^ N ) = ( ( A ^ N ) x. ( B ^ N ) ) )
Theorem	mulexpzap 9295	Integer exponentiation of a product. (Contributed by Jim Kingdon, 10-Jun-2020.)
|- ( ( ( A e. CC /\ A # 0 ) /\ ( B e. CC /\ B # 0 ) /\ N e. ZZ ) -> ( ( A x. B ) ^ N ) = ( ( A ^ N ) x. ( B ^ N ) ) )
Theorem	exprecap 9296	Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 10-Jun-2020.)
|- ( ( A e. CC /\ A # 0 /\ N e. ZZ ) -> ( ( 1 / A ) ^ N ) = ( 1 / ( A ^ N ) ) )
Theorem	expadd 9297	Sum of exponents law for nonnegative integer exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135. (Contributed by NM, 30-Nov-2004.)
|- ( ( A e. CC /\ M e. NN0 /\ N e. NN0 ) -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) )
Theorem	expaddzaplem 9298	Lemma for expaddzap 9299. (Contributed by Jim Kingdon, 10-Jun-2020.)
|- ( ( ( A e. CC /\ A # 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) )
Theorem	expaddzap 9299	Sum of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 10-Jun-2020.)
|- ( ( ( A e. CC /\ A # 0 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) )
Theorem	expmul 9300	Product of exponents law for positive integer exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by NM, 4-Jan-2006.)
|- ( ( A e. CC /\ M e. NN0 /\ N e. NN0 ) -> ( A ^ ( M x. N ) ) = ( ( A ^ M ) ^ N ) )