Home | Metamath
Proof Explorer Theorem List (p. 157 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fsumrev2 15601* | Reversal of a finite sum. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 13-Apr-2016.) |
β’ ((π β§ π β (π...π)) β π΄ β β) & β’ (π = ((π + π) β π) β π΄ = π΅) β β’ (π β Ξ£π β (π...π)π΄ = Ξ£π β (π...π)π΅) | ||
Theorem | fsum0diag2 15602* | Two ways to express "the sum of π΄(π, π) over the triangular region 0 β€ π, 0 β€ π, π + π β€ π". (Contributed by Mario Carneiro, 21-Jul-2014.) |
β’ (π₯ = π β π΅ = π΄) & β’ (π₯ = (π β π) β π΅ = πΆ) & β’ ((π β§ (π β (0...π) β§ π β (0...(π β π)))) β π΄ β β) β β’ (π β Ξ£π β (0...π)Ξ£π β (0...(π β π))π΄ = Ξ£π β (0...π)Ξ£π β (0...π)πΆ) | ||
Theorem | fsummulc2 15603* | A finite sum multiplied by a constant. (Contributed by NM, 12-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
β’ (π β π΄ β Fin) & β’ (π β πΆ β β) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β (πΆ Β· Ξ£π β π΄ π΅) = Ξ£π β π΄ (πΆ Β· π΅)) | ||
Theorem | fsummulc1 15604* | A finite sum multiplied by a constant. (Contributed by NM, 13-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
β’ (π β π΄ β Fin) & β’ (π β πΆ β β) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β (Ξ£π β π΄ π΅ Β· πΆ) = Ξ£π β π΄ (π΅ Β· πΆ)) | ||
Theorem | fsumdivc 15605* | A finite sum divided by a constant. (Contributed by NM, 2-Jan-2006.) (Revised by Mario Carneiro, 24-Apr-2014.) |
β’ (π β π΄ β Fin) & β’ (π β πΆ β β) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β πΆ β 0) β β’ (π β (Ξ£π β π΄ π΅ / πΆ) = Ξ£π β π΄ (π΅ / πΆ)) | ||
Theorem | fsumneg 15606* | Negation of a finite sum. (Contributed by Scott Fenton, 12-Jun-2013.) (Revised by Mario Carneiro, 24-Apr-2014.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ -π΅ = -Ξ£π β π΄ π΅) | ||
Theorem | fsumsub 15607* | Split a finite sum over a subtraction. (Contributed by Scott Fenton, 12-Jun-2013.) (Revised by Mario Carneiro, 24-Apr-2014.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β πΆ β β) β β’ (π β Ξ£π β π΄ (π΅ β πΆ) = (Ξ£π β π΄ π΅ β Ξ£π β π΄ πΆ)) | ||
Theorem | fsum2mul 15608* | Separate the nested sum of the product πΆ(π) Β· π·(π). (Contributed by NM, 13-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
β’ (π β π΄ β Fin) & β’ (π β π΅ β Fin) & β’ ((π β§ π β π΄) β πΆ β β) & β’ ((π β§ π β π΅) β π· β β) β β’ (π β Ξ£π β π΄ Ξ£π β π΅ (πΆ Β· π·) = (Ξ£π β π΄ πΆ Β· Ξ£π β π΅ π·)) | ||
Theorem | fsumconst 15609* | The sum of constant terms (π is not free in π΅). (Contributed by NM, 24-Dec-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
β’ ((π΄ β Fin β§ π΅ β β) β Ξ£π β π΄ π΅ = ((β―βπ΄) Β· π΅)) | ||
Theorem | fsumdifsnconst 15610* | The sum of constant terms (π is not free in πΆ) over an index set excluding a singleton. (Contributed by AV, 7-Jan-2022.) |
β’ ((π΄ β Fin β§ π΅ β π΄ β§ πΆ β β) β Ξ£π β (π΄ β {π΅})πΆ = (((β―βπ΄) β 1) Β· πΆ)) | ||
Theorem | modfsummodslem1 15611* | Lemma 1 for modfsummods 15612. (Contributed by Alexander van der Vekens, 1-Sep-2018.) |
β’ (βπ β (π΄ βͺ {π§})π΅ β β€ β β¦π§ / πβ¦π΅ β β€) | ||
Theorem | modfsummods 15612* | Induction step for modfsummod 15613. (Contributed by Alexander van der Vekens, 1-Sep-2018.) |
β’ ((π΄ β Fin β§ π β β β§ βπ β (π΄ βͺ {π§})π΅ β β€) β ((Ξ£π β π΄ π΅ mod π) = (Ξ£π β π΄ (π΅ mod π) mod π) β (Ξ£π β (π΄ βͺ {π§})π΅ mod π) = (Ξ£π β (π΄ βͺ {π§})(π΅ mod π) mod π))) | ||
Theorem | modfsummod 15613* | 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.) |
β’ (π β π β β) & β’ (π β π΄ β Fin) & β’ (π β βπ β π΄ π΅ β β€) β β’ (π β (Ξ£π β π΄ π΅ mod π) = (Ξ£π β π΄ (π΅ mod π) mod π)) | ||
Theorem | fsumge0 15614* | 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.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β 0 β€ π΅) β β’ (π β 0 β€ Ξ£π β π΄ π΅) | ||
Theorem | fsumless 15615* | A shorter sum of nonnegative terms is smaller than a longer one. (Contributed by NM, 26-Dec-2005.) (Proof shortened by Mario Carneiro, 24-Apr-2014.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β 0 β€ π΅) & β’ (π β πΆ β π΄) β β’ (π β Ξ£π β πΆ π΅ β€ Ξ£π β π΄ π΅) | ||
Theorem | fsumge1 15616* | 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.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β 0 β€ π΅) & β’ (π = π β π΅ = πΆ) & β’ (π β π β π΄) β β’ (π β πΆ β€ Ξ£π β π΄ π΅) | ||
Theorem | fsum00 15617* | 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.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β 0 β€ π΅) β β’ (π β (Ξ£π β π΄ π΅ = 0 β βπ β π΄ π΅ = 0)) | ||
Theorem | fsumle 15618* | 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.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β πΆ β β) & β’ ((π β§ π β π΄) β π΅ β€ πΆ) β β’ (π β Ξ£π β π΄ π΅ β€ Ξ£π β π΄ πΆ) | ||
Theorem | fsumlt 15619* | 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.) |
β’ (π β π΄ β Fin) & β’ (π β π΄ β β ) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β πΆ β β) & β’ ((π β§ π β π΄) β π΅ < πΆ) β β’ (π β Ξ£π β π΄ π΅ < Ξ£π β π΄ πΆ) | ||
Theorem | fsumabs 15620* | 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.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β (absβΞ£π β π΄ π΅) β€ Ξ£π β π΄ (absβπ΅)) | ||
Theorem | telfsumo 15621* | Sum of a telescoping series, using half-open intervals. (Contributed by Mario Carneiro, 2-May-2016.) |
β’ (π = π β π΄ = π΅) & β’ (π = (π + 1) β π΄ = πΆ) & β’ (π = π β π΄ = π·) & β’ (π = π β π΄ = πΈ) & β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β π΄ β β) β β’ (π β Ξ£π β (π..^π)(π΅ β πΆ) = (π· β πΈ)) | ||
Theorem | telfsumo2 15622* | Sum of a telescoping series. (Contributed by Mario Carneiro, 2-May-2016.) |
β’ (π = π β π΄ = π΅) & β’ (π = (π + 1) β π΄ = πΆ) & β’ (π = π β π΄ = π·) & β’ (π = π β π΄ = πΈ) & β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β π΄ β β) β β’ (π β Ξ£π β (π..^π)(πΆ β π΅) = (πΈ β π·)) | ||
Theorem | telfsum 15623* | Sum of a telescoping series. (Contributed by Scott Fenton, 24-Apr-2014.) (Revised by Mario Carneiro, 2-May-2016.) |
β’ (π = π β π΄ = π΅) & β’ (π = (π + 1) β π΄ = πΆ) & β’ (π = π β π΄ = π·) & β’ (π = (π + 1) β π΄ = πΈ) & β’ (π β π β β€) & β’ (π β (π + 1) β (β€β₯βπ)) & β’ ((π β§ π β (π...(π + 1))) β π΄ β β) β β’ (π β Ξ£π β (π...π)(π΅ β πΆ) = (π· β πΈ)) | ||
Theorem | telfsum2 15624* | Sum of a telescoping series. (Contributed by Mario Carneiro, 15-Jun-2014.) (Revised by Mario Carneiro, 2-May-2016.) |
β’ (π = π β π΄ = π΅) & β’ (π = (π + 1) β π΄ = πΆ) & β’ (π = π β π΄ = π·) & β’ (π = (π + 1) β π΄ = πΈ) & β’ (π β π β β€) & β’ (π β (π + 1) β (β€β₯βπ)) & β’ ((π β§ π β (π...(π + 1))) β π΄ β β) β β’ (π β Ξ£π β (π...π)(πΆ β π΅) = (πΈ β π·)) | ||
Theorem | fsumparts 15625* | Summation by parts. (Contributed by Mario Carneiro, 13-Apr-2016.) |
β’ (π = π β (π΄ = π΅ β§ π = π)) & β’ (π = (π + 1) β (π΄ = πΆ β§ π = π)) & β’ (π = π β (π΄ = π· β§ π = π)) & β’ (π = π β (π΄ = πΈ β§ π = π)) & β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β π΄ β β) & β’ ((π β§ π β (π...π)) β π β β) β β’ (π β Ξ£π β (π..^π)(π΅ Β· (π β π)) = (((πΈ Β· π) β (π· Β· π)) β Ξ£π β (π..^π)((πΆ β π΅) Β· π))) | ||
Theorem | fsumrelem 15626* | Lemma for fsumre 15627, fsumim 15628, and fsumcj 15629. (Contributed by Mario Carneiro, 25-Jul-2014.) (Revised by Mario Carneiro, 27-Dec-2014.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ πΉ:ββΆβ & β’ ((π₯ β β β§ π¦ β β) β (πΉβ(π₯ + π¦)) = ((πΉβπ₯) + (πΉβπ¦))) β β’ (π β (πΉβΞ£π β π΄ π΅) = Ξ£π β π΄ (πΉβπ΅)) | ||
Theorem | fsumre 15627* | The real part of a sum. (Contributed by Paul Chapman, 9-Nov-2007.) (Revised by Mario Carneiro, 25-Jul-2014.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β (ββΞ£π β π΄ π΅) = Ξ£π β π΄ (ββπ΅)) | ||
Theorem | fsumim 15628* | The imaginary part of a sum. (Contributed by Paul Chapman, 9-Nov-2007.) (Revised by Mario Carneiro, 25-Jul-2014.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β (ββΞ£π β π΄ π΅) = Ξ£π β π΄ (ββπ΅)) | ||
Theorem | fsumcj 15629* | The complex conjugate of a sum. (Contributed by Paul Chapman, 9-Nov-2007.) (Revised by Mario Carneiro, 25-Jul-2014.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β (ββΞ£π β π΄ π΅) = Ξ£π β π΄ (ββπ΅)) | ||
Theorem | fsumrlim 15630* | Limit of a finite sum of converging sequences. Note that πΆ(π) is a collection of functions with implicit parameter π, each of which converges to π·(π) as π β +β. (Contributed by Mario Carneiro, 22-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β Fin) & β’ ((π β§ (π₯ β π΄ β§ π β π΅)) β πΆ β π) & β’ ((π β§ π β π΅) β (π₯ β π΄ β¦ πΆ) βπ π·) β β’ (π β (π₯ β π΄ β¦ Ξ£π β π΅ πΆ) βπ Ξ£π β π΅ π·) | ||
Theorem | fsumo1 15631* | The finite sum of eventually bounded functions (where the index set π΅ does not depend on π₯) is eventually bounded. (Contributed by Mario Carneiro, 30-Apr-2016.) (Proof shortened by Mario Carneiro, 22-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β Fin) & β’ ((π β§ (π₯ β π΄ β§ π β π΅)) β πΆ β π) & β’ ((π β§ π β π΅) β (π₯ β π΄ β¦ πΆ) β π(1)) β β’ (π β (π₯ β π΄ β¦ Ξ£π β π΅ πΆ) β π(1)) | ||
Theorem | o1fsum 15632* | If π΄(π) is O(1), then Ξ£π β€ π₯, π΄(π) is O(π₯). (Contributed by Mario Carneiro, 23-May-2016.) |
β’ ((π β§ π β β) β π΄ β π) & β’ (π β (π β β β¦ π΄) β π(1)) β β’ (π β (π₯ β β+ β¦ (Ξ£π β (1...(ββπ₯))π΄ / π₯)) β π(1)) | ||
Theorem | seqabs 15633* | Generalized triangle inequality: the absolute value of a finite sum is less than or equal to the sum of absolute values. (Contributed by Mario Carneiro, 26-Mar-2014.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β (πΉβπ) β β) & β’ ((π β§ π β (π...π)) β (πΊβπ) = (absβ(πΉβπ))) β β’ (π β (absβ(seqπ( + , πΉ)βπ)) β€ (seqπ( + , πΊ)βπ)) | ||
Theorem | iserabs 15634* | 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 Mario Carneiro, 27-May-2014.) |
β’ π = (β€β₯βπ) & β’ (π β seqπ( + , πΉ) β π΄) & β’ (π β seqπ( + , πΊ) β π΅) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) = (absβ(πΉβπ))) β β’ (π β (absβπ΄) β€ π΅) | ||
Theorem | cvgcmp 15635* | A comparison test for convergence of a real infinite series. Exercise 3 of [Gleason] p. 182. (Contributed by NM, 1-May-2005.) (Revised by Mario Carneiro, 24-Mar-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) β β) & β’ (π β seqπ( + , πΉ) β dom β ) & β’ ((π β§ π β (β€β₯βπ)) β 0 β€ (πΊβπ)) & β’ ((π β§ π β (β€β₯βπ)) β (πΊβπ) β€ (πΉβπ)) β β’ (π β seqπ( + , πΊ) β dom β ) | ||
Theorem | cvgcmpub 15636* | 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.) |
β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) β β) & β’ (π β seqπ( + , πΉ) β π΄) & β’ (π β seqπ( + , πΊ) β π΅) & β’ ((π β§ π β π) β (πΊβπ) β€ (πΉβπ)) β β’ (π β π΅ β€ π΄) | ||
Theorem | cvgcmpce 15637* | A comparison test for convergence of a complex infinite series. (Contributed by NM, 25-Apr-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) β β) & β’ (π β seqπ( + , πΉ) β dom β ) & β’ (π β πΆ β β) & β’ ((π β§ π β (β€β₯βπ)) β (absβ(πΊβπ)) β€ (πΆ Β· (πΉβπ))) β β’ (π β seqπ( + , πΊ) β dom β ) | ||
Theorem | abscvgcvg 15638* | An absolutely convergent series is convergent. (Contributed by Mario Carneiro, 28-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = (absβ(πΊβπ))) & β’ ((π β§ π β π) β (πΊβπ) β β) & β’ (π β seqπ( + , πΉ) β dom β ) β β’ (π β seqπ( + , πΊ) β dom β ) | ||
Theorem | climfsum 15639* | Limit of a finite sum of converging sequences. Note that πΉ(π) is a collection of functions with implicit parameter π, each of which converges to π΅(π) as π β +β. (Contributed by Mario Carneiro, 22-Jul-2014.) (Proof shortened by Mario Carneiro, 22-May-2016.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β πΉ β π΅) & β’ (π β π» β π) & β’ ((π β§ (π β π΄ β§ π β π)) β (πΉβπ) β β) & β’ ((π β§ π β π) β (π»βπ) = Ξ£π β π΄ (πΉβπ)) β β’ (π β π» β Ξ£π β π΄ π΅) | ||
Theorem | fsumiun 15640* | Sum over a disjoint indexed union. (Contributed by Mario Carneiro, 1-Jul-2015.) (Revised by Mario Carneiro, 10-Dec-2016.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π₯ β π΄) β π΅ β Fin) & β’ (π β Disj π₯ β π΄ π΅) & β’ ((π β§ (π₯ β π΄ β§ π β π΅)) β πΆ β β) β β’ (π β Ξ£π β βͺ π₯ β π΄ π΅πΆ = Ξ£π₯ β π΄ Ξ£π β π΅ πΆ) | ||
Theorem | hashiun 15641* | The cardinality of a disjoint indexed union. (Contributed by Mario Carneiro, 24-Jan-2015.) (Revised by Mario Carneiro, 10-Dec-2016.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π₯ β π΄) β π΅ β Fin) & β’ (π β Disj π₯ β π΄ π΅) β β’ (π β (β―ββͺ π₯ β π΄ π΅) = Ξ£π₯ β π΄ (β―βπ΅)) | ||
Theorem | hash2iun 15642* | The cardinality of a nested disjoint indexed union. (Contributed by AV, 9-Jan-2022.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π₯ β π΄) β π΅ β Fin) & β’ ((π β§ π₯ β π΄ β§ π¦ β π΅) β πΆ β Fin) & β’ (π β Disj π₯ β π΄ βͺ π¦ β π΅ πΆ) & β’ ((π β§ π₯ β π΄) β Disj π¦ β π΅ πΆ) β β’ (π β (β―ββͺ π₯ β π΄ βͺ π¦ β π΅ πΆ) = Ξ£π₯ β π΄ Ξ£π¦ β π΅ (β―βπΆ)) | ||
Theorem | hash2iun1dif1 15643* | The cardinality of a nested disjoint indexed union. (Contributed by AV, 9-Jan-2022.) |
β’ (π β π΄ β Fin) & β’ π΅ = (π΄ β {π₯}) & β’ ((π β§ π₯ β π΄ β§ π¦ β π΅) β πΆ β Fin) & β’ (π β Disj π₯ β π΄ βͺ π¦ β π΅ πΆ) & β’ ((π β§ π₯ β π΄) β Disj π¦ β π΅ πΆ) & β’ ((π β§ π₯ β π΄ β§ π¦ β π΅) β (β―βπΆ) = 1) β β’ (π β (β―ββͺ π₯ β π΄ βͺ π¦ β π΅ πΆ) = ((β―βπ΄) Β· ((β―βπ΄) β 1))) | ||
Theorem | hashrabrex 15644* | The number of elements in a class abstraction with a restricted existential quantification. (Contributed by Alexander van der Vekens, 29-Jul-2018.) |
β’ (π β π β Fin) & β’ ((π β§ π¦ β π) β {π₯ β π β£ π} β Fin) & β’ (π β Disj π¦ β π {π₯ β π β£ π}) β β’ (π β (β―β{π₯ β π β£ βπ¦ β π π}) = Ξ£π¦ β π (β―β{π₯ β π β£ π})) | ||
Theorem | hashuni 15645* | The cardinality of a disjoint union. (Contributed by Mario Carneiro, 24-Jan-2015.) |
β’ (π β π΄ β Fin) & β’ (π β π΄ β Fin) & β’ (π β Disj π₯ β π΄ π₯) β β’ (π β (β―ββͺ π΄) = Ξ£π₯ β π΄ (β―βπ₯)) | ||
Theorem | qshash 15646* | The cardinality of a set with an equivalence relation is the sum of the cardinalities of its equivalence classes. (Contributed by Mario Carneiro, 16-Jan-2015.) |
β’ (π β βΌ Er π΄) & β’ (π β π΄ β Fin) β β’ (π β (β―βπ΄) = Ξ£π₯ β (π΄ / βΌ )(β―βπ₯)) | ||
Theorem | ackbijnn 15647* | Translate the Ackermann bijection ackbij1 10107 onto the positive integers. (Contributed by Mario Carneiro, 16-Jan-2015.) |
β’ πΉ = (π₯ β (π« β0 β© Fin) β¦ Ξ£π¦ β π₯ (2βπ¦)) β β’ πΉ:(π« β0 β© Fin)β1-1-ontoββ0 | ||
Theorem | binomlem 15648* | Lemma for binom 15649 (binomial theorem). Inductive step. (Contributed by NM, 6-Dec-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β0) & β’ (π β ((π΄ + π΅)βπ) = Ξ£π β (0...π)((πCπ) Β· ((π΄β(π β π)) Β· (π΅βπ)))) β β’ ((π β§ π) β ((π΄ + π΅)β(π + 1)) = Ξ£π β (0...(π + 1))(((π + 1)Cπ) Β· ((π΄β((π + 1) β π)) Β· (π΅βπ)))) | ||
Theorem | binom 15649* | The binomial theorem: (π΄ + π΅)βπ is the sum from π = 0 to π of (πCπ) Β· ((π΄βπ) Β· (π΅β(π β π)). 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 15648. This is Metamath 100 proof #44. (Contributed by NM, 7-Dec-2005.) (Proof shortened by Mario Carneiro, 24-Apr-2014.) |
β’ ((π΄ β β β§ π΅ β β β§ π β β0) β ((π΄ + π΅)βπ) = Ξ£π β (0...π)((πCπ) Β· ((π΄β(π β π)) Β· (π΅βπ)))) | ||
Theorem | binom1p 15650* | Special case of the binomial theorem for (1 + π΄)βπ. (Contributed by Paul Chapman, 10-May-2007.) |
β’ ((π΄ β β β§ π β β0) β ((1 + π΄)βπ) = Ξ£π β (0...π)((πCπ) Β· (π΄βπ))) | ||
Theorem | binom11 15651* | Special case of the binomial theorem for 2βπ. (Contributed by Mario Carneiro, 13-Mar-2014.) |
β’ (π β β0 β (2βπ) = Ξ£π β (0...π)(πCπ)) | ||
Theorem | binom1dif 15652* | A summation for the difference between ((π΄ + 1)βπ) and (π΄βπ). (Contributed by Scott Fenton, 9-Apr-2014.) (Revised by Mario Carneiro, 22-May-2014.) |
β’ ((π΄ β β β§ π β β0) β (((π΄ + 1)βπ) β (π΄βπ)) = Ξ£π β (0...(π β 1))((πCπ) Β· (π΄βπ))) | ||
Theorem | bcxmaslem1 15653 | Lemma for bcxmas 15654. (Contributed by Paul Chapman, 18-May-2007.) |
β’ (π΄ = π΅ β ((π + π΄)Cπ΄) = ((π + π΅)Cπ΅)) | ||
Theorem | bcxmas 15654* | Parallel summation (Christmas Stocking) theorem for Pascal's Triangle. (Contributed by Paul Chapman, 18-May-2007.) (Revised by Mario Carneiro, 24-Apr-2014.) |
β’ ((π β β0 β§ π β β0) β (((π + 1) + π)Cπ) = Ξ£π β (0...π)((π + π)Cπ)) | ||
Theorem | incexclem 15655* | Lemma for incexc 15656. (Contributed by Mario Carneiro, 7-Aug-2017.) |
β’ ((π΄ β Fin β§ π΅ β Fin) β ((β―βπ΅) β (β―β(π΅ β© βͺ π΄))) = Ξ£π β π« π΄((-1β(β―βπ )) Β· (β―β(π΅ β© β© π )))) | ||
Theorem | incexc 15656* | The inclusion/exclusion principle for counting the elements of a finite union of finite sets. This is Metamath 100 proof #96. (Contributed by Mario Carneiro, 7-Aug-2017.) |
β’ ((π΄ β Fin β§ π΄ β Fin) β (β―ββͺ π΄) = Ξ£π β (π« π΄ β {β })((-1β((β―βπ ) β 1)) Β· (β―ββ© π ))) | ||
Theorem | incexc2 15657* | The inclusion/exclusion principle for counting the elements of a finite union of finite sets. (Contributed by Mario Carneiro, 7-Aug-2017.) |
β’ ((π΄ β Fin β§ π΄ β Fin) β (β―ββͺ π΄) = Ξ£π β (1...(β―βπ΄))((-1β(π β 1)) Β· Ξ£π β {π β π« π΄ β£ (β―βπ) = π} (β―ββ© π ))) | ||
Theorem | isumshft 15658* | Index shift of an infinite sum. (Contributed by Paul Chapman, 31-Oct-2007.) (Revised by Mario Carneiro, 24-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ π = (β€β₯β(π + πΎ)) & β’ (π = (πΎ + π) β π΄ = π΅) & β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ ((π β§ π β π) β π΄ β β) β β’ (π β Ξ£π β π π΄ = Ξ£π β π π΅) | ||
Theorem | isumsplit 15659* | Split off the first π terms of an infinite sum. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 24-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β π΄ β β) & β’ (π β seqπ( + , πΉ) β dom β ) β β’ (π β Ξ£π β π π΄ = (Ξ£π β (π...(π β 1))π΄ + Ξ£π β π π΄)) | ||
Theorem | isum1p 15660* | 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.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β π΄ β β) & β’ (π β seqπ( + , πΉ) β dom β ) β β’ (π β Ξ£π β π π΄ = ((πΉβπ) + Ξ£π β (β€β₯β(π + 1))π΄)) | ||
Theorem | isumnn0nn 15661* | 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.) |
β’ (π = 0 β π΄ = π΅) & β’ ((π β§ π β β0) β (πΉβπ) = π΄) & β’ ((π β§ π β β0) β π΄ β β) & β’ (π β seq0( + , πΉ) β dom β ) β β’ (π β Ξ£π β β0 π΄ = (π΅ + Ξ£π β β π΄)) | ||
Theorem | isumrpcl 15662* | The infinite sum of positive reals is positive. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 24-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β π΄ β β+) & β’ (π β seqπ( + , πΉ) β dom β ) β β’ (π β Ξ£π β π π΄ β β+) | ||
Theorem | isumle 15663* | Comparison of two infinite sums. (Contributed by Paul Chapman, 13-Nov-2007.) (Revised by Mario Carneiro, 24-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β π΄ β β) & β’ ((π β§ π β π) β (πΊβπ) = π΅) & β’ ((π β§ π β π) β π΅ β β) & β’ ((π β§ π β π) β π΄ β€ π΅) & β’ (π β seqπ( + , πΉ) β dom β ) & β’ (π β seqπ( + , πΊ) β dom β ) β β’ (π β Ξ£π β π π΄ β€ Ξ£π β π π΅) | ||
Theorem | isumless 15664* | A finite sum of nonnegative numbers is less than or equal to its limit. (Contributed by Mario Carneiro, 24-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π΄ β Fin) & β’ (π β π΄ β π) & β’ ((π β§ π β π) β (πΉβπ) = π΅) & β’ ((π β§ π β π) β π΅ β β) & β’ ((π β§ π β π) β 0 β€ π΅) & β’ (π β seqπ( + , πΉ) β dom β ) β β’ (π β Ξ£π β π΄ π΅ β€ Ξ£π β π π΅) | ||
Theorem | isumsup2 15665* | An infinite sum of nonnegative terms is equal to the supremum of the partial sums. (Contributed by Mario Carneiro, 12-Jun-2014.) |
β’ π = (β€β₯βπ) & β’ πΊ = seqπ( + , πΉ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β π΄ β β) & β’ ((π β§ π β π) β 0 β€ π΄) & β’ (π β βπ₯ β β βπ β π (πΊβπ) β€ π₯) β β’ (π β πΊ β sup(ran πΊ, β, < )) | ||
Theorem | isumsup 15666* | An infinite sum of nonnegative terms is equal to the supremum of the partial sums. (Contributed by Mario Carneiro, 12-Jun-2014.) |
β’ π = (β€β₯βπ) & β’ πΊ = seqπ( + , πΉ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β π΄ β β) & β’ ((π β§ π β π) β 0 β€ π΄) & β’ (π β βπ₯ β β βπ β π (πΊβπ) β€ π₯) β β’ (π β Ξ£π β π π΄ = sup(ran πΊ, β, < )) | ||
Theorem | isumltss 15667* | A partial sum of a series with positive terms is less than the infinite sum. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Mar-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π΄ β Fin) & β’ (π β π΄ β π) & β’ ((π β§ π β π) β (πΉβπ) = π΅) & β’ ((π β§ π β π) β π΅ β β+) & β’ (π β seqπ( + , πΉ) β dom β ) β β’ (π β Ξ£π β π΄ π΅ < Ξ£π β π π΅) | ||
Theorem | climcndslem1 15668* | Lemma for climcnds 15670: bound the original series by the condensed series. (Contributed by Mario Carneiro, 18-Jul-2014.) |
β’ ((π β§ π β β) β (πΉβπ) β β) & β’ ((π β§ π β β) β 0 β€ (πΉβπ)) & β’ ((π β§ π β β) β (πΉβ(π + 1)) β€ (πΉβπ)) & β’ ((π β§ π β β0) β (πΊβπ) = ((2βπ) Β· (πΉβ(2βπ)))) β β’ ((π β§ π β β0) β (seq1( + , πΉ)β((2β(π + 1)) β 1)) β€ (seq0( + , πΊ)βπ)) | ||
Theorem | climcndslem2 15669* | Lemma for climcnds 15670: bound the condensed series by the original series. (Contributed by Mario Carneiro, 18-Jul-2014.) (Proof shortened by AV, 10-Jul-2022.) |
β’ ((π β§ π β β) β (πΉβπ) β β) & β’ ((π β§ π β β) β 0 β€ (πΉβπ)) & β’ ((π β§ π β β) β (πΉβ(π + 1)) β€ (πΉβπ)) & β’ ((π β§ π β β0) β (πΊβπ) = ((2βπ) Β· (πΉβ(2βπ)))) β β’ ((π β§ π β β) β (seq1( + , πΊ)βπ) β€ (2 Β· (seq1( + , πΉ)β(2βπ)))) | ||
Theorem | climcnds 15670* | The Cauchy condensation test. If π(π) is a decreasing sequence of nonnegative terms, then Ξ£π β βπ(π) converges iff Ξ£π β β02βπ Β· π(2βπ) converges. (Contributed by Mario Carneiro, 18-Jul-2014.) (Proof shortened by AV, 10-Jul-2022.) |
β’ ((π β§ π β β) β (πΉβπ) β β) & β’ ((π β§ π β β) β 0 β€ (πΉβπ)) & β’ ((π β§ π β β) β (πΉβ(π + 1)) β€ (πΉβπ)) & β’ ((π β§ π β β0) β (πΊβπ) = ((2βπ) Β· (πΉβ(2βπ)))) β β’ (π β (seq1( + , πΉ) β dom β β seq0( + , πΊ) β dom β )) | ||
Theorem | divrcnv 15671* | The sequence of reciprocals of real numbers, multiplied by the factor π΄, converges to zero. (Contributed by Mario Carneiro, 18-Sep-2014.) |
β’ (π΄ β β β (π β β+ β¦ (π΄ / π)) βπ 0) | ||
Theorem | divcnv 15672* | The sequence of reciprocals of positive integers, multiplied by the factor π΄, converges to zero. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 18-Sep-2014.) |
β’ (π΄ β β β (π β β β¦ (π΄ / π)) β 0) | ||
Theorem | flo1 15673 | The floor function satisfies β(π₯) = π₯ + π(1). (Contributed by Mario Carneiro, 21-May-2016.) |
β’ (π₯ β β β¦ (π₯ β (ββπ₯))) β π(1) | ||
Theorem | divcnvshft 15674* | Limit of a ratio function. (Contributed by Scott Fenton, 16-Dec-2017.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π΄ β β) & β’ (π β π΅ β β€) & β’ (π β πΉ β π) & β’ ((π β§ π β π) β (πΉβπ) = (π΄ / (π + π΅))) β β’ (π β πΉ β 0) | ||
Theorem | supcvg 15675* | Extract a sequence π in π such that the image of the points in the bounded set π΄ converges to the supremum π of the set. Similar to Equation 4 of [Kreyszig] p. 144. The proof uses countable choice ax-cc 10304. (Contributed by Mario Carneiro, 15-Feb-2013.) (Proof shortened by Mario Carneiro, 26-Apr-2014.) |
β’ π β V & β’ π = sup(π΄, β, < ) & β’ π = (π β β β¦ (π β (1 / π))) & β’ (π β π β β ) & β’ (π β πΉ:πβontoβπ΄) & β’ (π β π΄ β β) & β’ (π β βπ₯ β β βπ¦ β π΄ π¦ β€ π₯) β β’ (π β βπ(π:ββΆπ β§ (πΉ β π) β π)) | ||
Theorem | infcvgaux1i 15676* | Auxiliary theorem for applications of supcvg 15675. Hypothesis for several supremum theorems. (Contributed by NM, 8-Feb-2008.) |
β’ π = {π₯ β£ βπ¦ β π π₯ = -π΄} & β’ (π¦ β π β π΄ β β) & β’ π β π & β’ βπ§ β β βπ€ β π π€ β€ π§ β β’ (π β β β§ π β β β§ βπ§ β β βπ€ β π π€ β€ π§) | ||
Theorem | infcvgaux2i 15677* | Auxiliary theorem for applications of supcvg 15675. (Contributed by NM, 4-Mar-2008.) |
β’ π = {π₯ β£ βπ¦ β π π₯ = -π΄} & β’ (π¦ β π β π΄ β β) & β’ π β π & β’ βπ§ β β βπ€ β π π€ β€ π§ & β’ π = -sup(π , β, < ) & β’ (π¦ = πΆ β π΄ = π΅) β β’ (πΆ β π β π β€ π΅) | ||
Theorem | harmonic 15678 | The harmonic series π» diverges. This fact follows from the stronger emcl 26274, which establishes that the harmonic series grows as logπ + Ξ³ + o(1), but this uses a more elementary method, attributed to Nicole Oresme (1323-1382). This is Metamath 100 proof #34. (Contributed by Mario Carneiro, 11-Jul-2014.) |
β’ πΉ = (π β β β¦ (1 / π)) & β’ π» = seq1( + , πΉ) β β’ Β¬ π» β dom β | ||
Theorem | arisum 15679* | 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.) |
β’ (π β β0 β Ξ£π β (1...π)π = (((πβ2) + π) / 2)) | ||
Theorem | arisum2 15680* | Arithmetic series sum of the first π nonnegative integers. (Contributed by Mario Carneiro, 17-Apr-2015.) (Proof shortened by AV, 2-Aug-2021.) |
β’ (π β β0 β Ξ£π β (0...(π β 1))π = (((πβ2) β π) / 2)) | ||
Theorem | trireciplem 15681 | Lemma for trirecip 15682. Show that the sum converges. (Contributed by Scott Fenton, 22-Apr-2014.) (Revised by Mario Carneiro, 22-May-2014.) |
β’ πΉ = (π β β β¦ (1 / (π Β· (π + 1)))) β β’ seq1( + , πΉ) β 1 | ||
Theorem | trirecip 15682 | 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.) |
β’ Ξ£π β β (2 / (π Β· (π + 1))) = 2 | ||
Theorem | expcnv 15683* | A sequence of powers of a complex number π΄ with absolute value smaller than 1 converges to zero. (Contributed by NM, 8-May-2006.) (Proof shortened by Mario Carneiro, 26-Apr-2014.) |
β’ (π β π΄ β β) & β’ (π β (absβπ΄) < 1) β β’ (π β (π β β0 β¦ (π΄βπ)) β 0) | ||
Theorem | explecnv 15684* | 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.) |
β’ π = (β€β₯βπ) & β’ (π β πΉ β π) & β’ (π β π β β€) & β’ (π β π΄ β β) & β’ (π β (absβπ΄) < 1) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (absβ(πΉβπ)) β€ (π΄βπ)) β β’ (π β πΉ β 0) | ||
Theorem | geoserg 15685* | The value of the finite geometric series π΄βπ + π΄β(π + 1) +... + π΄β(π β 1). (Contributed by Mario Carneiro, 2-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΄ β 1) & β’ (π β π β β0) & β’ (π β π β (β€β₯βπ)) β β’ (π β Ξ£π β (π..^π)(π΄βπ) = (((π΄βπ) β (π΄βπ)) / (1 β π΄))) | ||
Theorem | geoser 15686* | The value of the finite geometric series 1 + π΄β1 + π΄β2 +... + π΄β(π β 1). This is Metamath 100 proof #66. (Contributed by NM, 12-May-2006.) (Proof shortened by Mario Carneiro, 15-Jun-2014.) |
β’ (π β π΄ β β) & β’ (π β π΄ β 1) & β’ (π β π β β0) β β’ (π β Ξ£π β (0...(π β 1))(π΄βπ) = ((1 β (π΄βπ)) / (1 β π΄))) | ||
Theorem | pwdif 15687* | The difference of two numbers to the same power is the difference of the two numbers multiplied with a finite sum. Generalization of subsq 14039. See Wikipedia "Fermat number", section "Other theorems about Fermat numbers", https://en.wikipedia.org/wiki/Fermat_number 14039, 5-Aug-2021. (Contributed by AV, 6-Aug-2021.) (Revised by AV, 19-Aug-2021.) |
β’ ((π β β0 β§ π΄ β β β§ π΅ β β) β ((π΄βπ) β (π΅βπ)) = ((π΄ β π΅) Β· Ξ£π β (0..^π)((π΄βπ) Β· (π΅β((π β π) β 1))))) | ||
Theorem | pwm1geoser 15688* | The n-th power of a number decreased by 1 expressed by the finite geometric series 1 + π΄β1 + π΄β2 +... + π΄β(π β 1). (Contributed by AV, 14-Aug-2021.) (Proof shortened by AV, 19-Aug-2021.) |
β’ (π β π΄ β β) & β’ (π β π β β0) β β’ (π β ((π΄βπ) β 1) = ((π΄ β 1) Β· Ξ£π β (0...(π β 1))(π΄βπ))) | ||
Theorem | geolim 15689* | The partial sums in the infinite series 1 + π΄β1 + π΄β2... converge to (1 / (1 β π΄)). (Contributed by NM, 15-May-2006.) |
β’ (π β π΄ β β) & β’ (π β (absβπ΄) < 1) & β’ ((π β§ π β β0) β (πΉβπ) = (π΄βπ)) β β’ (π β seq0( + , πΉ) β (1 / (1 β π΄))) | ||
Theorem | geolim2 15690* | The partial sums in the geometric series π΄βπ + π΄β(π + 1)... converge to ((π΄βπ) / (1 β π΄)). (Contributed by NM, 6-Jun-2006.) (Revised by Mario Carneiro, 26-Apr-2014.) |
β’ (π β π΄ β β) & β’ (π β (absβπ΄) < 1) & β’ (π β π β β0) & β’ ((π β§ π β (β€β₯βπ)) β (πΉβπ) = (π΄βπ)) β β’ (π β seqπ( + , πΉ) β ((π΄βπ) / (1 β π΄))) | ||
Theorem | georeclim 15691* | The limit of a geometric series of reciprocals. (Contributed by Paul Chapman, 28-Dec-2007.) (Revised by Mario Carneiro, 26-Apr-2014.) |
β’ (π β π΄ β β) & β’ (π β 1 < (absβπ΄)) & β’ ((π β§ π β β0) β (πΉβπ) = ((1 / π΄)βπ)) β β’ (π β seq0( + , πΉ) β (π΄ / (π΄ β 1))) | ||
Theorem | geo2sum 15692* | The value of the finite geometric series 2β-1 + 2β-2 +... + 2β-π, multiplied by a constant. (Contributed by Mario Carneiro, 17-Mar-2014.) (Revised by Mario Carneiro, 26-Apr-2014.) |
β’ ((π β β β§ π΄ β β) β Ξ£π β (1...π)(π΄ / (2βπ)) = (π΄ β (π΄ / (2βπ)))) | ||
Theorem | geo2sum2 15693* | The value of the finite geometric series 1 + 2 + 4 + 8 +... + 2β(π β 1). (Contributed by Mario Carneiro, 7-Sep-2016.) |
β’ (π β β0 β Ξ£π β (0..^π)(2βπ) = ((2βπ) β 1)) | ||
Theorem | geo2lim 15694* | The value of the infinite geometric series 2β-1 + 2β-2 +... , multiplied by a constant. (Contributed by Mario Carneiro, 15-Jun-2014.) |
β’ πΉ = (π β β β¦ (π΄ / (2βπ))) β β’ (π΄ β β β seq1( + , πΉ) β π΄) | ||
Theorem | geomulcvg 15695* | The geometric series converges even if it is multiplied by π to result in the larger series π Β· π΄βπ. (Contributed by Mario Carneiro, 27-Mar-2015.) |
β’ πΉ = (π β β0 β¦ (π Β· (π΄βπ))) β β’ ((π΄ β β β§ (absβπ΄) < 1) β seq0( + , πΉ) β dom β ) | ||
Theorem | geoisum 15696* | The infinite sum of 1 + π΄β1 + π΄β2... is (1 / (1 β π΄)). (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 26-Apr-2014.) |
β’ ((π΄ β β β§ (absβπ΄) < 1) β Ξ£π β β0 (π΄βπ) = (1 / (1 β π΄))) | ||
Theorem | geoisumr 15697* | The infinite sum of reciprocals 1 + (1 / π΄)β1 + (1 / π΄)β2... is π΄ / (π΄ β 1). (Contributed by rpenner, 3-Nov-2007.) (Revised by Mario Carneiro, 26-Apr-2014.) |
β’ ((π΄ β β β§ 1 < (absβπ΄)) β Ξ£π β β0 ((1 / π΄)βπ) = (π΄ / (π΄ β 1))) | ||
Theorem | geoisum1 15698* | The infinite sum of π΄β1 + π΄β2... is (π΄ / (1 β π΄)). (Contributed by NM, 1-Nov-2007.) (Revised by Mario Carneiro, 26-Apr-2014.) |
β’ ((π΄ β β β§ (absβπ΄) < 1) β Ξ£π β β (π΄βπ) = (π΄ / (1 β π΄))) | ||
Theorem | geoisum1c 15699* | The infinite sum of π΄ Β· (π β1) + π΄ Β· (π β2)... is (π΄ Β· π ) / (1 β π ). (Contributed by NM, 2-Nov-2007.) (Revised by Mario Carneiro, 26-Apr-2014.) |
β’ ((π΄ β β β§ π β β β§ (absβπ ) < 1) β Ξ£π β β (π΄ Β· (π βπ)) = ((π΄ Β· π ) / (1 β π ))) | ||
Theorem | 0.999... 15700 | The recurring decimal 0.999..., which is defined as the infinite sum 0.9 + 0.09 + 0.009 + ... i.e. 9 / 10β1 + 9 / 10β2 + 9 / 10β3 + ..., is exactly equal to 1, according to ZF set theory. Interestingly, about 40% of the people responding to a poll at http://forum.physorg.com/index.php?showtopic=13177 disagree. (Contributed by NM, 2-Nov-2007.) (Revised by AV, 8-Sep-2021.) |
β’ Ξ£π β β (9 / (;10βπ)) = 1 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |