Theorem List for Intuitionistic Logic Explorer - 11401-11500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | isumclim2 11401* |
A converging series converges to its infinite sum. (Contributed by NM,
2-Jan-2006.) (Revised by Mario Carneiro, 23-Apr-2014.)
|
       
              
      |
|
Theorem | isumclim3 11402* |
The sequence of partial finite sums of a converging infinite series
converges to the infinite sum of the series. Note that must not
occur in .
(Contributed by NM, 9-Jan-2006.) (Revised by Mario
Carneiro, 23-Apr-2014.)
|
                             |
|
Theorem | sumnul 11403* |
The sum of a non-convergent infinite series evaluates to the empty
set. (Contributed by Paul Chapman, 4-Nov-2007.) (Revised by Mario
Carneiro, 23-Apr-2014.)
|
       
          
  
    |
|
Theorem | isumcl 11404* |
The sum of a converging infinite series is a complex number.
(Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro,
23-Apr-2014.)
|
       
              
   |
|
Theorem | isummulc2 11405* |
An infinite sum multiplied by a constant. (Contributed by NM,
12-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.)
|
       
              
    
     |
|
Theorem | isummulc1 11406* |
An infinite sum multiplied by a constant. (Contributed by NM,
13-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.)
|
       
              
          |
|
Theorem | isumdivapc 11407* |
An infinite sum divided by a constant. (Contributed by NM, 2-Jan-2006.)
(Revised by Mario Carneiro, 23-Apr-2014.)
|
       
              
  #           |
|
Theorem | isumrecl 11408* |
The sum of a converging infinite real series is a real number.
(Contributed by Mario Carneiro, 24-Apr-2014.)
|
       
              
   |
|
Theorem | isumge0 11409* |
An infinite sum of nonnegative terms is nonnegative. (Contributed by
Mario Carneiro, 28-Apr-2014.)
|
       
                   
  |
|
Theorem | isumadd 11410* |
Addition of infinite sums. (Contributed by Mario Carneiro,
18-Aug-2013.) (Revised by Mario Carneiro, 23-Apr-2014.)
|
       
           
              
  
   
      |
|
Theorem | sumsplitdc 11411* |
Split a sum into two parts. (Contributed by Mario Carneiro,
18-Aug-2013.) (Revised by Mario Carneiro, 23-Apr-2014.)
|
            
   
DECID
   
DECID
               
            
  
    

  
    
      |
|
Theorem | fsump1i 11412* |
Optimized version of fsump1 11399 for making sums of a concrete number of
terms. (Contributed by Mario Carneiro, 23-Apr-2014.)
|
      
               
    
         |
|
Theorem | fsum2dlemstep 11413* |
Lemma for fsum2d 11414- induction step. (Contributed by Mario
Carneiro,
23-Apr-2014.) (Revised by Jim Kingdon, 8-Oct-2022.)
|
        
    
 
   
        
 
               

            |
|
Theorem | fsum2d 11414* |
Write a double sum as a sum over a two-dimensional region. Note that
   is a function of . (Contributed by Mario Carneiro,
27-Apr-2014.)
|
        
    
 
   

       |
|
Theorem | fsumxp 11415* |
Combine two sums into a single sum over the cartesian product.
(Contributed by Mario Carneiro, 23-Apr-2014.)
|
           
 
   
      |
|
Theorem | fsumcnv 11416* |
Transform a region of summation by using the converse operation.
(Contributed by Mario Carneiro, 23-Apr-2014.)
|
        
               |
|
Theorem | fisumcom2 11417* |
Interchange order of summation. Note that    and   
are not necessarily constant expressions. (Contributed by Mario
Carneiro, 28-Apr-2014.) (Revised by Mario Carneiro, 8-Apr-2016.)
(Proof shortened by JJ, 2-Aug-2021.)
|
     
                
 
   
    |
|
Theorem | fsumcom 11418* |
Interchange order of summation. (Contributed by NM, 15-Nov-2005.)
(Revised by Mario Carneiro, 23-Apr-2014.)
|
     
  
        |
|
Theorem | fsum0diaglem 11419* |
Lemma for fisum0diag 11420. (Contributed by Mario Carneiro,
28-Apr-2014.)
(Revised by Mario Carneiro, 8-Apr-2016.)
|
                 
         |
|
Theorem | fisum0diag 11420* |
Two ways to express "the sum of     over the
triangular
region , ,
". (Contributed
by NM,
31-Dec-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2014.)
(Revised by Mario Carneiro, 8-Apr-2016.)
|
      
                                          |
|
Theorem | mptfzshft 11421* |
1-1 onto function in maps-to notation which shifts a finite set of
sequential integers. (Contributed by AV, 24-Aug-2019.)
|
                                     |
|
Theorem | fsumrev 11422* |
Reversal of a finite sum. (Contributed by NM, 26-Nov-2005.) (Revised
by Mario Carneiro, 24-Apr-2014.)
|
            
   
       
      
     |
|
Theorem | fsumshft 11423* |
Index shift of a finite sum. (Contributed by NM, 27-Nov-2005.)
(Revised by Mario Carneiro, 24-Apr-2014.) (Proof shortened by AV,
8-Sep-2019.)
|
            
           
      
     |
|
Theorem | fsumshftm 11424* |
Negative index shift of a finite sum. (Contributed by NM,
28-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
            
           
      
     |
|
Theorem | fisumrev2 11425* |
Reversal of a finite sum. (Contributed by NM, 27-Nov-2005.) (Revised
by Mario Carneiro, 13-Apr-2016.)
|
     
    
    

       
        |
|
Theorem | fisum0diag2 11426* |
Two ways to express "the sum of     over the
triangular
region ,
,
". (Contributed by
Mario Carneiro, 21-Jul-2014.)
|
  
         
                                        |
|
Theorem | fsummulc2 11427* |
A finite sum multiplied by a constant. (Contributed by NM,
12-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
     
     
     |
|
Theorem | fsummulc1 11428* |
A finite sum multiplied by a constant. (Contributed by NM,
13-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
     
           |
|
Theorem | fsumdivapc 11429* |
A finite sum divided by a constant. (Contributed by NM, 2-Jan-2006.)
(Revised by Mario Carneiro, 24-Apr-2014.)
|
     
   #           |
|
Theorem | fsumneg 11430* |
Negation of a finite sum. (Contributed by Scott Fenton, 12-Jun-2013.)
(Revised by Mario Carneiro, 24-Apr-2014.)
|
             |
|
Theorem | fsumsub 11431* |
Split a finite sum over a subtraction. (Contributed by Scott Fenton,
12-Jun-2013.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
       
     
      |
|
Theorem | fsum2mul 11432* |
Separate the nested sum of the product       .
(Contributed by NM, 13-Nov-2005.) (Revised by Mario Carneiro,
24-Apr-2014.)
|
     
                 |
|
Theorem | fsumconst 11433* |
The sum of constant terms ( is not free in ). (Contributed
by NM, 24-Dec-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
   
 ♯     |
|
Theorem | fsumdifsnconst 11434* |
The sum of constant terms ( is not free in ) over an index
set excluding a singleton. (Contributed by AV, 7-Jan-2022.)
|
 
 
       ♯      |
|
Theorem | modfsummodlem1 11435* |
Lemma for modfsummod 11437. (Contributed by Alexander van der Vekens,
1-Sep-2018.)
|
         ![]_ ]_](_urbrack.gif)   |
|
Theorem | modfsummodlemstep 11436* |
Induction step for modfsummod 11437. (Contributed by Alexander van der
Vekens, 1-Sep-2018.) (Revised by Jim Kingdon, 12-Oct-2022.)
|
                
   
     
     
            |
|
Theorem | modfsummod 11437* |
A finite sum modulo a positive integer equals the finite sum of their
summands modulo the positive integer, modulo the positive integer.
(Contributed by Alexander van der Vekens, 1-Sep-2018.)
|
     
    
       |
|
Theorem | fsumge0 11438* |
If all of the terms of a finite sum are nonnegative, so is the sum.
(Contributed by NM, 26-Dec-2005.) (Revised by Mario Carneiro,
24-Apr-2014.)
|
       
   
  |
|
Theorem | fsumlessfi 11439* |
A shorter sum of nonnegative terms is no greater than a longer one.
(Contributed by NM, 26-Dec-2005.) (Revised by Jim Kingdon,
12-Oct-2022.)
|
       
           |
|
Theorem | fsumge1 11440* |
A sum of nonnegative numbers is greater than or equal to any one of
its terms. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof
shortened by Mario Carneiro, 4-Jun-2014.)
|
       
  
       |
|
Theorem | fsum00 11441* |
A sum of nonnegative numbers is zero iff all terms are zero.
(Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario
Carneiro, 24-Apr-2014.)
|
       
    

   |
|
Theorem | fsumle 11442* |
If all of the terms of finite sums compare, so do the sums.
(Contributed by NM, 11-Dec-2005.) (Proof shortened by Mario Carneiro,
24-Apr-2014.)
|
       
    
      |
|
Theorem | fsumlt 11443* |
If every term in one finite sum is less than the corresponding term in
another, then the first sum is less than the second. (Contributed by
Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 3-Jun-2014.)
|
         
      
    |
|
Theorem | fsumabs 11444* |
Generalized triangle inequality: the absolute value of a finite sum is
less than or equal to the sum of absolute values. (Contributed by NM,
9-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
                   |
|
Theorem | telfsumo 11445* |
Sum of a telescoping series, using half-open intervals. (Contributed by
Mario Carneiro, 2-May-2016.)
|
  
   
 
 
           
    ..^   
    |
|
Theorem | telfsumo2 11446* |
Sum of a telescoping series. (Contributed by Mario Carneiro,
2-May-2016.)
|
  
   
 
 
           
    ..^   
    |
|
Theorem | telfsum 11447* |
Sum of a telescoping series. (Contributed by Scott Fenton,
24-Apr-2014.) (Revised by Mario Carneiro, 2-May-2016.)
|
  
   
 

  
                                |
|
Theorem | telfsum2 11448* |
Sum of a telescoping series. (Contributed by Mario Carneiro,
15-Jun-2014.) (Revised by Mario Carneiro, 2-May-2016.)
|
  
   
 

  
                                |
|
Theorem | fsumparts 11449* |
Summation by parts. (Contributed by Mario Carneiro, 13-Apr-2016.)
|
      

   
                     
    
    ..^               ..^         |
|
Theorem | fsumrelem 11450* |
Lemma for fsumre 11451, fsumim 11452, and fsumcj 11453. (Contributed by Mario
Carneiro, 25-Jul-2014.) (Revised by Mario Carneiro, 27-Dec-2014.)
|
                       
           
       |
|
Theorem | fsumre 11451* |
The real part of a sum. (Contributed by Paul Chapman, 9-Nov-2007.)
(Revised by Mario Carneiro, 25-Jul-2014.)
|
           
       |
|
Theorem | fsumim 11452* |
The imaginary part of a sum. (Contributed by Paul Chapman, 9-Nov-2007.)
(Revised by Mario Carneiro, 25-Jul-2014.)
|
           
       |
|
Theorem | fsumcj 11453* |
The complex conjugate of a sum. (Contributed by Paul Chapman,
9-Nov-2007.) (Revised by Mario Carneiro, 25-Jul-2014.)
|
           
       |
|
Theorem | iserabs 11454* |
Generalized triangle inequality: the absolute value of an infinite sum
is less than or equal to the sum of absolute values. (Contributed by
Paul Chapman, 10-Sep-2007.) (Revised by Jim Kingdon, 14-Dec-2022.)
|
       
    
                                  |
|
Theorem | cvgcmpub 11455* |
An upper bound for the limit of a real infinite series. This theorem
can also be used to compare two infinite series. (Contributed by Mario
Carneiro, 24-Mar-2014.)
|
       
                 
    
  
             |
|
Theorem | fsumiun 11456* |
Sum over a disjoint indexed union. (Contributed by Mario Carneiro,
1-Jul-2015.) (Revised by Mario Carneiro, 10-Dec-2016.)
|
       Disj    
 
   
    |
|
Theorem | hashiun 11457* |
The cardinality of a disjoint indexed union. (Contributed by Mario
Carneiro, 24-Jan-2015.) (Revised by Mario Carneiro, 10-Dec-2016.)
|
       Disj   ♯  
 ♯    |
|
Theorem | hash2iun 11458* |
The cardinality of a nested disjoint indexed union. (Contributed by AV,
9-Jan-2022.)
|
       
   Disj    
 Disj   ♯   
  ♯    |
|
Theorem | hash2iun1dif1 11459* |
The cardinality of a nested disjoint indexed union. (Contributed by AV,
9-Jan-2022.)
|
       
   Disj 
    Disj   
 ♯    ♯   
 ♯   ♯      |
|
Theorem | hashrabrex 11460* |
The number of elements in a class abstraction with a restricted
existential quantification. (Contributed by Alexander van der Vekens,
29-Jul-2018.)
|
         Disj     ♯      ♯      |
|
Theorem | hashuni 11461* |
The cardinality of a disjoint union. (Contributed by Mario Carneiro,
24-Jan-2015.)
|
     Disj   ♯   
♯    |
|
4.8.3 The binomial theorem
|
|
Theorem | binomlem 11462* |
Lemma for binom 11463 (binomial theorem). Inductive step.
(Contributed by
NM, 6-Dec-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
             
                                                               |
|
Theorem | binom 11463* |
The binomial theorem:     is the sum from to
of              . Theorem
15-2.8 of [Gleason] p. 296. This part
of the proof sets up the
induction and does the base case, with the bulk of the work (the
induction step) in binomlem 11462. This is Metamath 100 proof #44.
(Contributed by NM, 7-Dec-2005.) (Proof shortened by Mario Carneiro,
24-Apr-2014.)
|
        
                        |
|
Theorem | binom1p 11464* |
Special case of the binomial theorem for     .
(Contributed by Paul Chapman, 10-May-2007.)
|
        
                |
|
Theorem | binom11 11465* |
Special case of the binomial theorem for   .
(Contributed by
Mario Carneiro, 13-Mar-2014.)
|
    
          |
|
Theorem | binom1dif 11466* |
A summation for the difference between       and
    .
(Contributed by Scott Fenton, 9-Apr-2014.) (Revised by
Mario Carneiro, 22-May-2014.)
|
                         
       |
|
Theorem | bcxmaslem1 11467 |
Lemma for bcxmas 11468. (Contributed by Paul Chapman,
18-May-2007.)
|
   
       |
|
Theorem | bcxmas 11468* |
Parallel summation (Christmas Stocking) theorem for Pascal's Triangle.
(Contributed by Paul Chapman, 18-May-2007.) (Revised by Mario Carneiro,
24-Apr-2014.)
|
       
         
   |
|
4.8.4 Infinite sums (cont.)
|
|
Theorem | isumshft 11469* |
Index shift of an infinite sum. (Contributed by Paul Chapman,
31-Oct-2007.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
            
          
   |
|
Theorem | isumsplit 11470* |
Split off the first
terms of an infinite sum. (Contributed by
Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 21-Oct-2022.)
|
                          
  
           |
|
Theorem | isum1p 11471* |
The infinite sum of a converging infinite series equals the first term
plus the infinite sum of the rest of it. (Contributed by NM,
2-Jan-2006.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
       
              
     
           |
|
Theorem | isumnn0nn 11472* |
Sum from 0 to infinity in terms of sum from 1 to infinity. (Contributed
by NM, 2-Jan-2006.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
                  


    |
|
Theorem | isumrpcl 11473* |
The infinite sum of positive reals is positive. (Contributed by Paul
Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
                          
   |
|
Theorem | isumle 11474* |
Comparison of two infinite sums. (Contributed by Paul Chapman,
13-Nov-2007.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
       
           
           
     

  
     |
|
Theorem | isumlessdc 11475* |
A finite sum of nonnegative numbers is less than or equal to its limit.
(Contributed by Mario Carneiro, 24-Apr-2014.)
|
                  
 DECID        
 
  
     |
|
4.8.5 Miscellaneous converging and diverging
sequences
|
|
Theorem | divcnv 11476* |
The sequence of reciprocals of positive integers, multiplied by the
factor ,
converges to zero. (Contributed by NM, 6-Feb-2008.)
(Revised by Jim Kingdon, 22-Oct-2022.)
|
  
 
  |
|
4.8.6 Arithmetic series
|
|
Theorem | arisum 11477* |
Arithmetic series sum of the first positive integers. This is
Metamath 100 proof #68. (Contributed by FL, 16-Nov-2006.) (Proof
shortened by Mario Carneiro, 22-May-2014.)
|
                 |
|
Theorem | arisum2 11478* |
Arithmetic series sum of the first nonnegative integers.
(Contributed by Mario Carneiro, 17-Apr-2015.) (Proof shortened by AV,
2-Aug-2021.)
|
                   |
|
Theorem | trireciplem 11479 |
Lemma for trirecip 11480. Show that the sum converges. (Contributed
by
Scott Fenton, 22-Apr-2014.) (Revised by Mario Carneiro,
22-May-2014.)
|
   
      
 |
|
Theorem | trirecip 11480 |
The sum of the reciprocals of the triangle numbers converge to two.
This is Metamath 100 proof #42. (Contributed by Scott Fenton,
23-Apr-2014.) (Revised by Mario Carneiro, 22-May-2014.)
|

       |
|
4.8.7 Geometric series
|
|
Theorem | expcnvap0 11481* |
A sequence of powers of a complex number with absolute value
smaller than 1 converges to zero. (Contributed by NM, 8-May-2006.)
(Revised by Jim Kingdon, 23-Oct-2022.)
|
         #   
       |
|
Theorem | expcnvre 11482* |
A sequence of powers of a nonnegative real number less than one
converges to zero. (Contributed by Jim Kingdon, 28-Oct-2022.)
|
       
       |
|
Theorem | expcnv 11483* |
A sequence of powers of a complex number with absolute value
smaller than 1 converges to zero. (Contributed by NM, 8-May-2006.)
(Revised by Jim Kingdon, 28-Oct-2022.)
|
         
       |
|
Theorem | explecnv 11484* |
A sequence of terms converges to zero when it is less than powers of a
number whose
absolute value is smaller than 1. (Contributed by
NM, 19-Jul-2008.) (Revised by Mario Carneiro, 26-Apr-2014.)
|
                         
                 |
|
Theorem | geosergap 11485* |
The value of the finite geometric series       ...
    . (Contributed by Mario Carneiro, 2-May-2016.)
(Revised by Jim Kingdon, 24-Oct-2022.)
|
   #             ..^                      |
|
Theorem | geoserap 11486* |
The value of the finite geometric series
    ...
    . This is Metamath 100 proof #66. (Contributed by
NM, 12-May-2006.) (Revised by Jim Kingdon, 24-Oct-2022.)
|
   #                             |
|
Theorem | pwm1geoserap1 11487* |
The n-th power of a number decreased by 1 expressed by the finite
geometric series
    ...     .
(Contributed by AV, 14-Aug-2021.) (Revised by Jim Kingdon,
24-Oct-2022.)
|
     #           
               |
|
Theorem | absltap 11488 |
Less-than of absolute value implies apartness. (Contributed by Jim
Kingdon, 29-Oct-2022.)
|
           #   |
|
Theorem | absgtap 11489 |
Greater-than of absolute value implies apartness. (Contributed by Jim
Kingdon, 29-Oct-2022.)
|
           #   |
|
Theorem | geolim 11490* |
The partial sums in the infinite series
    ...
converge to     . (Contributed by NM,
15-May-2006.)
|
                    
         |
|
Theorem | geolim2 11491* |
The partial sums in the geometric series       ...
converge to         .
(Contributed by NM,
6-Jun-2006.) (Revised by Mario Carneiro, 26-Apr-2014.)
|
                             
          |
|
Theorem | georeclim 11492* |
The limit of a geometric series of reciprocals. (Contributed by Paul
Chapman, 28-Dec-2007.) (Revised by Mario Carneiro, 26-Apr-2014.)
|
                      
         |
|
Theorem | geo2sum 11493* |
The value of the finite geometric series       ...
   ,
multiplied by a constant. (Contributed by Mario
Carneiro, 17-Mar-2014.) (Revised by Mario Carneiro, 26-Apr-2014.)
|
                
        |
|
Theorem | geo2sum2 11494* |
The value of the finite geometric series
...
    . (Contributed by Mario Carneiro, 7-Sep-2016.)
|
   ..^          
   |
|
Theorem | geo2lim 11495* |
The value of the infinite geometric series
      ... , multiplied by a constant. (Contributed
by Mario Carneiro, 15-Jun-2014.)
|
        
  
  |
|
Theorem | geoisum 11496* |
The infinite sum of     ... is
    .
(Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro,
26-Apr-2014.)
|
                  |
|
Theorem | geoisumr 11497* |
The infinite sum of reciprocals
        ... is   .
(Contributed by rpenner, 3-Nov-2007.) (Revised by Mario Carneiro,
26-Apr-2014.)
|
                    |
|
Theorem | geoisum1 11498* |
The infinite sum of     ... is     .
(Contributed by NM, 1-Nov-2007.) (Revised by Mario Carneiro,
26-Apr-2014.)
|
                  |
|
Theorem | geoisum1c 11499* |
The infinite sum of
        ... is
    . (Contributed by NM, 2-Nov-2007.) (Revised
by Mario Carneiro, 26-Apr-2014.)
|
                
     |
|
Theorem | 0.999... 11500 |
The recurring decimal 0.999..., which is defined as the infinite sum 0.9 +
0.09 + 0.009 + ... i.e.         
, is exactly equal to
1. (Contributed by NM, 2-Nov-2007.)
(Revised by AV, 8-Sep-2021.)
|

 ;      |