Theorem List for Intuitionistic Logic Explorer - 11501-11600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | modfsummod 11501* |
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 11502* |
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 11503* |
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 11504* |
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 11505* |
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 11506* |
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 11507* |
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 11508* |
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 11509* |
Sum of a telescoping series, using half-open intervals. (Contributed by
Mario Carneiro, 2-May-2016.)
|
  
   
 
 
           
    ..^   
    |
|
Theorem | telfsumo2 11510* |
Sum of a telescoping series. (Contributed by Mario Carneiro,
2-May-2016.)
|
  
   
 
 
           
    ..^   
    |
|
Theorem | telfsum 11511* |
Sum of a telescoping series. (Contributed by Scott Fenton,
24-Apr-2014.) (Revised by Mario Carneiro, 2-May-2016.)
|
  
   
 

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

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

   
                     
    
    ..^               ..^         |
|
Theorem | fsumrelem 11514* |
Lemma for fsumre 11515, fsumim 11516, and fsumcj 11517. (Contributed by Mario
Carneiro, 25-Jul-2014.) (Revised by Mario Carneiro, 27-Dec-2014.)
|
                       
           
       |
|
Theorem | fsumre 11515* |
The real part of a sum. (Contributed by Paul Chapman, 9-Nov-2007.)
(Revised by Mario Carneiro, 25-Jul-2014.)
|
           
       |
|
Theorem | fsumim 11516* |
The imaginary part of a sum. (Contributed by Paul Chapman, 9-Nov-2007.)
(Revised by Mario Carneiro, 25-Jul-2014.)
|
           
       |
|
Theorem | fsumcj 11517* |
The complex conjugate of a sum. (Contributed by Paul Chapman,
9-Nov-2007.) (Revised by Mario Carneiro, 25-Jul-2014.)
|
           
       |
|
Theorem | iserabs 11518* |
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 11519* |
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 11520* |
Sum over a disjoint indexed union. (Contributed by Mario Carneiro,
1-Jul-2015.) (Revised by Mario Carneiro, 10-Dec-2016.)
|
       Disj    
 
   
    |
|
Theorem | hashiun 11521* |
The cardinality of a disjoint indexed union. (Contributed by Mario
Carneiro, 24-Jan-2015.) (Revised by Mario Carneiro, 10-Dec-2016.)
|
       Disj   ♯  
 ♯    |
|
Theorem | hash2iun 11522* |
The cardinality of a nested disjoint indexed union. (Contributed by AV,
9-Jan-2022.)
|
       
   Disj    
 Disj   ♯   
  ♯    |
|
Theorem | hash2iun1dif1 11523* |
The cardinality of a nested disjoint indexed union. (Contributed by AV,
9-Jan-2022.)
|
       
   Disj 
    Disj   
 ♯    ♯   
 ♯   ♯      |
|
Theorem | hashrabrex 11524* |
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 11525* |
The cardinality of a disjoint union. (Contributed by Mario Carneiro,
24-Jan-2015.)
|
     Disj   ♯   
♯    |
|
4.8.3 The binomial theorem
|
|
Theorem | binomlem 11526* |
Lemma for binom 11527 (binomial theorem). Inductive step.
(Contributed by
NM, 6-Dec-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
             
                                                               |
|
Theorem | binom 11527* |
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 11526. This is Metamath 100 proof #44.
(Contributed by NM, 7-Dec-2005.) (Proof shortened by Mario Carneiro,
24-Apr-2014.)
|
        
                        |
|
Theorem | binom1p 11528* |
Special case of the binomial theorem for     .
(Contributed by Paul Chapman, 10-May-2007.)
|
        
                |
|
Theorem | binom11 11529* |
Special case of the binomial theorem for   .
(Contributed by
Mario Carneiro, 13-Mar-2014.)
|
    
          |
|
Theorem | binom1dif 11530* |
A summation for the difference between       and
    .
(Contributed by Scott Fenton, 9-Apr-2014.) (Revised by
Mario Carneiro, 22-May-2014.)
|
                         
       |
|
Theorem | bcxmaslem1 11531 |
Lemma for bcxmas 11532. (Contributed by Paul Chapman,
18-May-2007.)
|
   
       |
|
Theorem | bcxmas 11532* |
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 11533* |
Index shift of an infinite sum. (Contributed by Paul Chapman,
31-Oct-2007.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
            
          
   |
|
Theorem | isumsplit 11534* |
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 11535* |
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 11536* |
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 11537* |
The infinite sum of positive reals is positive. (Contributed by Paul
Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
                          
   |
|
Theorem | isumle 11538* |
Comparison of two infinite sums. (Contributed by Paul Chapman,
13-Nov-2007.) (Revised by Mario Carneiro, 24-Apr-2014.)
|
       
           
           
     

  
     |
|
Theorem | isumlessdc 11539* |
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 11540* |
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 11541* |
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 11542* |
Arithmetic series sum of the first nonnegative integers.
(Contributed by Mario Carneiro, 17-Apr-2015.) (Proof shortened by AV,
2-Aug-2021.)
|
                   |
|
Theorem | trireciplem 11543 |
Lemma for trirecip 11544. Show that the sum converges. (Contributed
by
Scott Fenton, 22-Apr-2014.) (Revised by Mario Carneiro,
22-May-2014.)
|
   
      
 |
|
Theorem | trirecip 11544 |
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 11545* |
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 11546* |
A sequence of powers of a nonnegative real number less than one
converges to zero. (Contributed by Jim Kingdon, 28-Oct-2022.)
|
       
       |
|
Theorem | expcnv 11547* |
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 11548* |
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 11549* |
The value of the finite geometric series       ...
    . (Contributed by Mario Carneiro, 2-May-2016.)
(Revised by Jim Kingdon, 24-Oct-2022.)
|
   #             ..^                      |
|
Theorem | geoserap 11550* |
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 11551* |
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 11552 |
Less-than of absolute value implies apartness. (Contributed by Jim
Kingdon, 29-Oct-2022.)
|
           #   |
|
Theorem | absgtap 11553 |
Greater-than of absolute value implies apartness. (Contributed by Jim
Kingdon, 29-Oct-2022.)
|
           #   |
|
Theorem | geolim 11554* |
The partial sums in the infinite series
    ...
converge to     . (Contributed by NM,
15-May-2006.)
|
                    
         |
|
Theorem | geolim2 11555* |
The partial sums in the geometric series       ...
converge to         .
(Contributed by NM,
6-Jun-2006.) (Revised by Mario Carneiro, 26-Apr-2014.)
|
                             
          |
|
Theorem | georeclim 11556* |
The limit of a geometric series of reciprocals. (Contributed by Paul
Chapman, 28-Dec-2007.) (Revised by Mario Carneiro, 26-Apr-2014.)
|
                      
         |
|
Theorem | geo2sum 11557* |
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 11558* |
The value of the finite geometric series
...
    . (Contributed by Mario Carneiro, 7-Sep-2016.)
|
   ..^          
   |
|
Theorem | geo2lim 11559* |
The value of the infinite geometric series
      ... , multiplied by a constant. (Contributed
by Mario Carneiro, 15-Jun-2014.)
|
        
  
  |
|
Theorem | geoisum 11560* |
The infinite sum of     ... is
    .
(Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro,
26-Apr-2014.)
|
                  |
|
Theorem | geoisumr 11561* |
The infinite sum of reciprocals
        ... is   .
(Contributed by rpenner, 3-Nov-2007.) (Revised by Mario Carneiro,
26-Apr-2014.)
|
                    |
|
Theorem | geoisum1 11562* |
The infinite sum of     ... is     .
(Contributed by NM, 1-Nov-2007.) (Revised by Mario Carneiro,
26-Apr-2014.)
|
                  |
|
Theorem | geoisum1c 11563* |
The infinite sum of
        ... is
    . (Contributed by NM, 2-Nov-2007.) (Revised
by Mario Carneiro, 26-Apr-2014.)
|
                
     |
|
Theorem | 0.999... 11564 |
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.)
|

 ;      |
|
Theorem | geoihalfsum 11565 |
Prove that the infinite geometric series of 1/2, 1/2 + 1/4 + 1/8 + ... =
1. Uses geoisum1 11562. This is a representation of .111... in
binary with
an infinite number of 1's. Theorem 0.999... 11564 proves a similar claim for
.999... in base 10. (Contributed by David A. Wheeler, 4-Jan-2017.)
(Proof shortened by AV, 9-Jul-2022.)
|

       |
|
4.8.8 Ratio test for infinite series
convergence
|
|
Theorem | cvgratnnlembern 11566 |
Lemma for cvgratnn 11574. Upper bound for a geometric progression of
positive ratio less than one. (Contributed by Jim Kingdon,
24-Nov-2022.)
|
                 
     |
|
Theorem | cvgratnnlemnexp 11567* |
Lemma for cvgratnn 11574. (Contributed by Jim Kingdon, 15-Nov-2022.)
|
                                                                   |
|
Theorem | cvgratnnlemmn 11568* |
Lemma for cvgratnn 11574. (Contributed by Jim Kingdon,
15-Nov-2022.)
|
                                              
       
                  |
|
Theorem | cvgratnnlemseq 11569* |
Lemma for cvgratnn 11574. (Contributed by Jim Kingdon,
21-Nov-2022.)
|
                                              
                            |
|
Theorem | cvgratnnlemabsle 11570* |
Lemma for cvgratnn 11574. (Contributed by Jim Kingdon,
21-Nov-2022.)
|
                                              
   
                     
                |
|
Theorem | cvgratnnlemsumlt 11571* |
Lemma for cvgratnn 11574. (Contributed by Jim Kingdon,
23-Nov-2022.)
|
                                              
             
      |
|
Theorem | cvgratnnlemfm 11572* |
Lemma for cvgratnn 11574. (Contributed by Jim Kingdon, 23-Nov-2022.)
|
                                                                         |
|
Theorem | cvgratnnlemrate 11573* |
Lemma for cvgratnn 11574. (Contributed by Jim Kingdon, 21-Nov-2022.)
|
                                              
                                                |
|
Theorem | cvgratnn 11574* |
Ratio test for convergence of a complex infinite series. If the ratio
of the
absolute values of successive terms in an infinite
sequence is
less than 1 for all terms, then the infinite sum of
the terms of
converges to a complex number. Although this
theorem is similar to cvgratz 11575 and cvgratgt0 11576, the decision to
index starting at one is not merely cosmetic, as proving convergence
using climcvg1n 11393 is sensitive to how a sequence is indexed.
(Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon,
12-Nov-2022.)
|
                                         
 |
|
Theorem | cvgratz 11575* |
Ratio test for convergence of a complex infinite series. If the ratio
of the
absolute values of successive terms in an infinite sequence
is less than 1
for all terms, then the infinite sum of the terms
of converges
to a complex number. (Contributed by NM,
26-Apr-2005.) (Revised by Jim Kingdon, 11-Nov-2022.)
|
             
                                

 |
|
Theorem | cvgratgt0 11576* |
Ratio test for convergence of a complex infinite series. If the ratio
of the
absolute values of successive terms in an infinite sequence
is less than 1
for all terms beyond some index , then the
infinite sum of the terms of converges to a complex number.
(Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon,
11-Nov-2022.)
|
                                                  

 |
|
4.8.9 Mertens' theorem
|
|
Theorem | mertenslemub 11577* |
Lemma for mertensabs 11580. An upper bound for . (Contributed by
Jim Kingdon, 3-Dec-2022.)
|
               
                               
                         |
|
Theorem | mertenslemi1 11578* |
Lemma for mertensabs 11580. (Contributed by Mario Carneiro,
29-Apr-2014.) (Revised by Jim Kingdon, 2-Dec-2022.)
|
                     
                                       

  
                                                      
 
        
   
               
                                  
       |
|
Theorem | mertenslem2 11579* |
Lemma for mertensabs 11580. (Contributed by Mario Carneiro,
28-Apr-2014.)
|
                     
                                       

  
                                                      
 
        
                       
       |
|
Theorem | mertensabs 11580* |
Mertens' theorem. If    is an absolutely convergent series and
   is convergent, then
           
                (and
this latter series is convergent). This latter sum is commonly known as
the Cauchy product of the sequences. The proof follows the outline at
http://en.wikipedia.org/wiki/Cauchy_product#Proof_of_Mertens.27_theorem.
(Contributed by Mario Carneiro, 29-Apr-2014.) (Revised by Jim Kingdon,
8-Dec-2022.)
|
                     
                                       

  
    
         |
|
4.8.10 Finite and infinite
products
|
|
4.8.10.1 Product sequences
|
|
Theorem | prodf 11581* |
An infinite product of complex terms is a function from an upper set of
integers to .
(Contributed by Scott Fenton, 4-Dec-2017.)
|
       
                |
|
Theorem | clim2prod 11582* |
The limit of an infinite product with an initial segment added.
(Contributed by Scott Fenton, 18-Dec-2017.)
|
       
           
    
          |
|
Theorem | clim2divap 11583* |
The limit of an infinite product with an initial segment removed.
(Contributed by Scott Fenton, 20-Dec-2017.)
|
       
         
        #    
             |
|
Theorem | prod3fmul 11584* |
The product of two infinite products. (Contributed by Scott Fenton,
18-Dec-2017.) (Revised by Jim Kingdon, 22-Mar-2024.)
|
            
           
           
                     
                |
|
Theorem | prodf1 11585 |
The value of the partial products in a one-valued infinite product.
(Contributed by Scott Fenton, 5-Dec-2017.)
|
              
  |
|
Theorem | prodf1f 11586 |
A one-valued infinite product is equal to the constant one function.
(Contributed by Scott Fenton, 5-Dec-2017.)
|
                  |
|
Theorem | prodfclim1 11587 |
The constant one product converges to one. (Contributed by Scott
Fenton, 5-Dec-2017.)
|
              |
|
Theorem | prodfap0 11588* |
The product of finitely many terms apart from zero is apart from zero.
(Contributed by Scott Fenton, 14-Jan-2018.) (Revised by Jim Kingdon,
23-Mar-2024.)
|
            
           
    #         #   |
|
Theorem | prodfrecap 11589* |
The reciprocal of a finite product. (Contributed by Scott Fenton,
15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.)
|
            
           
    #                          
           

         |
|
Theorem | prodfdivap 11590* |
The quotient of two products. (Contributed by Scott Fenton,
15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.)
|
            
           
           
    #        
        
      
                      |
|
4.8.10.2 Non-trivial convergence
|
|
Theorem | ntrivcvgap 11591* |
A non-trivially converging infinite product converges. (Contributed by
Scott Fenton, 18-Dec-2017.)
|
         #   
             
 |
|
Theorem | ntrivcvgap0 11592* |
A product that converges to a value apart from zero converges
non-trivially. (Contributed by Scott Fenton, 18-Dec-2017.)
|
         
  #
      #   
   |
|
4.8.10.3 Complex products
|
|
Syntax | cprod 11593 |
Extend class notation to include complex products.
|
  |
|
Definition | df-proddc 11594* |
Define the product of a series with an index set of integers .
This definition takes most of the aspects of df-sumdc 11397 and adapts them
for multiplication instead of addition. However, we insist that in the
infinite case, there is a nonzero tail of the sequence. This ensures
that the convergence criteria match those of infinite sums.
(Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon,
21-Mar-2024.)
|

                DECID   
        #           
      
  
             
 

         ![]_ ]_](_urbrack.gif)            |
|
Theorem | prodeq1f 11595 |
Equality theorem for a product. (Contributed by Scott Fenton,
1-Dec-2017.)
|
     
   |
|
Theorem | prodeq1 11596* |
Equality theorem for a product. (Contributed by Scott Fenton,
1-Dec-2017.)
|
 
   |
|
Theorem | nfcprod1 11597* |
Bound-variable hypothesis builder for product. (Contributed by Scott
Fenton, 4-Dec-2017.)
|
      |
|
Theorem | nfcprod 11598* |
Bound-variable hypothesis builder for product: if is (effectively)
not free in
and , it is not free
in   .
(Contributed by Scott Fenton, 1-Dec-2017.)
|
        |
|
Theorem | prodeq2w 11599* |
Equality theorem for product, when the class expressions and
are equal everywhere. Proved using only Extensionality. (Contributed
by Scott Fenton, 4-Dec-2017.)
|
      |
|
Theorem | prodeq2 11600* |
Equality theorem for product. (Contributed by Scott Fenton,
4-Dec-2017.)
|
  
   |