HomeHome Intuitionistic Logic Explorer
Theorem List (p. 93 of 102)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 9201-9300   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremfrecuzrdgsuc 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 ) ) )
 
Theoremuzenom 9202 An upper integer set is denumerable. (Contributed by Mario Carneiro, 15-Oct-2015.)
 |-  Z  =  ( ZZ>= `  M )   =>    |-  ( M  e.  ZZ  ->  Z  ~~  om )
 
Theoremfrecfzennn 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 ) )
 
Theoremfrecfzen2 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 ) ) )
 
Theoremfrechashgf1o 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
 
Theoremfzfig 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 )
 
Theoremfzfigd 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 )
 
Theoremfzofig 9208 Half-open integer sets are finite. (Contributed by Jim Kingdon, 21-May-2020.)
 |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M..^ N )  e.  Fin )
 
Theoremnn0ennn 9209 The nonnegative integers are equinumerous to the positive integers. (Contributed by NM, 19-Jul-2004.)
 |- 
 NN0  ~~  NN
 
Theoremnnenom 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"
 
Syntaxcseq 9211 Extend class notation with recursive sequence builder.
 class  seq M (  .+  ,  F ,  S )
 
Definitiondf-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 ) >. )
 
Theoremiseqex 9213 Existence of the sequence builder operation. (Contributed by Jim Kingdon, 20-Aug-2021.)
 |- 
 seq M (  .+  ,  F ,  S )  e.  _V
 
Theoremiseqeq1 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 ) )
 
Theoremiseqeq2 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 ) )
 
Theoremiseqeq3 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 ) )
 
Theoremiseqeq4 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 ) )
 
Theoremnfiseq 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 )
 
Theoremiseqovex 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 )
 
Theoremiseqval 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 )
 
Theoremiseqfn 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 ) )
 
Theoremiseq1 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 ) )
 
Theoremiseqcl 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 )
 
Theoremiseqf 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 )
 
Theoremiseqp1 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
 ) ) ) )
 
Theoremiseqss 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 ) )
 
Theoremiseqm1 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 ) ) )
 
Theoremiseqfveq2 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 ) )
 
Theoremiseqfeq2 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 ) )
 
Theoremiseqfveq 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 ) )
 
Theoremiseqfeq 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 ) )
 
Theoremiseqshft2 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 )
 ) )
 
Theoremiserf 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 )
 
Theoremiserfre 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 )
 
Theoremmonoord 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 ) )
 
Theoremmonoord2 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 ) )
 
Theoremisermono 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 ) )
 
Theoremiseqsplit 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 ) ) )
 
Theoremiseq1p 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 ) ) )
 
Theoremiseqcaopr3 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 ) ) )
 
Theoremiseqcaopr2 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 ) ) )
 
Theoremiseqcaopr 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 ) ) )
 
Theoremiseradd 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 ) ) )
 
Theoremisersub 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 ) ) )
 
Theoremiseqid3 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 )
 
Theoremiseqid3s 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 )
 
Theoremiseqid 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 ) )
 
Theoremiseqhomo 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 ) )
 
Theoremiseqdistr 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 ) ) )
 
Theoremiser0 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 )
 
Theoremiser0f 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 } ) )
 
Theoremserige0 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 ) )
 
Theoremserile 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
 
Syntaxcexp 9254 Extend class notation to include exponentiation of a complex number to an integer power.
 class  ^
 
Definitiondf-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 ) ) ) ) )
 
Theoremexpivallem 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 )
 
Theoremexpival 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 ) ) ) ) )
 
Theoremexpinnval 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 ) )
 
Theoremexp0 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 )
 
Theorem0exp0e1 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
 
Theoremexp1 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 )
 
Theoremexpp1 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 ) )
 
Theoremexpnegap0 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 ) ) )
 
Theoremexpineg2 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 ) ) )
 
Theoremexpn1ap0 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 ) )
 
Theoremexpcllem 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 )
 
Theoremexpcl2lemap 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 )
 
Theoremnnexpcl 9268 Closure of exponentiation of nonnegative integers. (Contributed by NM, 16-Dec-2005.)
 |-  ( ( A  e.  NN  /\  N  e.  NN0 )  ->  ( A ^ N )  e.  NN )
 
Theoremnn0expcl 9269 Closure of exponentiation of nonnegative integers. (Contributed by NM, 14-Dec-2005.)
 |-  ( ( A  e.  NN0  /\  N  e.  NN0 )  ->  ( A ^ N )  e.  NN0 )
 
Theoremzexpcl 9270 Closure of exponentiation of integers. (Contributed by NM, 16-Dec-2005.)
 |-  ( ( A  e.  ZZ  /\  N  e.  NN0 )  ->  ( A ^ N )  e.  ZZ )
 
Theoremqexpcl 9271 Closure of exponentiation of rationals. (Contributed by NM, 16-Dec-2005.)
 |-  ( ( A  e.  QQ  /\  N  e.  NN0 )  ->  ( A ^ N )  e.  QQ )
 
Theoremreexpcl 9272 Closure of exponentiation of reals. (Contributed by NM, 14-Dec-2005.)
 |-  ( ( A  e.  RR  /\  N  e.  NN0 )  ->  ( A ^ N )  e.  RR )
 
Theoremexpcl 9273 Closure law for nonnegative integer exponentiation. (Contributed by NM, 26-May-2005.)
 |-  ( ( A  e.  CC  /\  N  e.  NN0 )  ->  ( A ^ N )  e.  CC )
 
Theoremrpexpcl 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+ )
 
Theoremreexpclzap 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 )
 
Theoremqexpclz 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 )
 
Theoremm1expcl2 9277 Closure of exponentiation of negative one. (Contributed by Mario Carneiro, 18-Jun-2015.)
 |-  ( N  e.  ZZ  ->  ( -u 1 ^ N )  e.  { -u 1 ,  1 } )
 
Theoremm1expcl 9278 Closure of exponentiation of negative one. (Contributed by Mario Carneiro, 18-Jun-2015.)
 |-  ( N  e.  ZZ  ->  ( -u 1 ^ N )  e.  ZZ )
 
Theoremexpclzaplem 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 } )
 
Theoremexpclzap 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 )
 
Theoremnn0expcli 9281 Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 17-Apr-2015.)
 |-  A  e.  NN0   &    |-  N  e.  NN0   =>    |-  ( A ^ N )  e.  NN0
 
Theoremnn0sqcl 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 )
 
Theoremexpm1t 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 ) )
 
Theorem1exp 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 )
 
Theoremexpap0 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 ) )
 
Theoremexpeq0 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
 ) )
 
Theoremexpap0i 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 )
 
Theoremexpgt0 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 ) )
 
Theoremexpnegzap 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 ) ) )
 
Theorem0exp 9290 Value of zero raised to a positive integer power. (Contributed by NM, 19-Aug-2004.)
 |-  ( N  e.  NN  ->  ( 0 ^ N )  =  0 )
 
Theoremexpge0 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 ) )
 
Theoremexpge1 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 ) )
 
Theoremexpgt1 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 ) )
 
Theoremmulexp 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 ) ) )
 
Theoremmulexpzap 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 ) ) )
 
Theoremexprecap 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 ) ) )
 
Theoremexpadd 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 ) ) )
 
Theoremexpaddzaplem 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 ) ) )
 
Theoremexpaddzap 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 ) ) )
 
Theoremexpmul 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 ) )
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10124
  Copyright terms: Public domain < Previous  Next >