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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fsumshftm 15601* | Negative index shift of a finite sum. (Contributed by NM, 28-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
โข (๐ โ ๐พ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) & โข (๐ = (๐ + ๐พ) โ ๐ด = ๐ต) โ โข (๐ โ ฮฃ๐ โ (๐...๐)๐ด = ฮฃ๐ โ ((๐ โ ๐พ)...(๐ โ ๐พ))๐ต) | ||
Theorem | fsumrev2 15602* | Reversal of a finite sum. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 13-Apr-2016.) |
โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) & โข (๐ = ((๐ + ๐) โ ๐) โ ๐ด = ๐ต) โ โข (๐ โ ฮฃ๐ โ (๐...๐)๐ด = ฮฃ๐ โ (๐...๐)๐ต) | ||
Theorem | fsum0diag2 15603* | 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 15604* | A finite sum multiplied by a constant. (Contributed by NM, 12-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ถ โ โ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ (๐ถ ยท ฮฃ๐ โ ๐ด ๐ต) = ฮฃ๐ โ ๐ด (๐ถ ยท ๐ต)) | ||
Theorem | fsummulc1 15605* | A finite sum multiplied by a constant. (Contributed by NM, 13-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ถ โ โ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ (ฮฃ๐ โ ๐ด ๐ต ยท ๐ถ) = ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)) | ||
Theorem | fsumdivc 15606* | A finite sum divided by a constant. (Contributed by NM, 2-Jan-2006.) (Revised by Mario Carneiro, 24-Apr-2014.) |
โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ถ โ โ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข (๐ โ ๐ถ โ 0) โ โข (๐ โ (ฮฃ๐ โ ๐ด ๐ต / ๐ถ) = ฮฃ๐ โ ๐ด (๐ต / ๐ถ)) | ||
Theorem | fsumneg 15607* | Negation of a finite sum. (Contributed by Scott Fenton, 12-Jun-2013.) (Revised by Mario Carneiro, 24-Apr-2014.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ ฮฃ๐ โ ๐ด -๐ต = -ฮฃ๐ โ ๐ด ๐ต) | ||
Theorem | fsumsub 15608* | Split a finite sum over a subtraction. (Contributed by Scott Fenton, 12-Jun-2013.) (Revised by Mario Carneiro, 24-Apr-2014.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โ) โ โข (๐ โ ฮฃ๐ โ ๐ด (๐ต โ ๐ถ) = (ฮฃ๐ โ ๐ด ๐ต โ ฮฃ๐ โ ๐ด ๐ถ)) | ||
Theorem | fsum2mul 15609* | Separate the nested sum of the product ๐ถ(๐) ยท ๐ท(๐). (Contributed by NM, 13-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ต โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โ) & โข ((๐ โง ๐ โ ๐ต) โ ๐ท โ โ) โ โข (๐ โ ฮฃ๐ โ ๐ด ฮฃ๐ โ ๐ต (๐ถ ยท ๐ท) = (ฮฃ๐ โ ๐ด ๐ถ ยท ฮฃ๐ โ ๐ต ๐ท)) | ||
Theorem | fsumconst 15610* | 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 15611* | 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 15612* | Lemma 1 for modfsummods 15613. (Contributed by Alexander van der Vekens, 1-Sep-2018.) |
โข (โ๐ โ (๐ด โช {๐ง})๐ต โ โค โ โฆ๐ง / ๐โฆ๐ต โ โค) | ||
Theorem | modfsummods 15613* | Induction step for modfsummod 15614. (Contributed by Alexander van der Vekens, 1-Sep-2018.) |
โข ((๐ด โ Fin โง ๐ โ โ โง โ๐ โ (๐ด โช {๐ง})๐ต โ โค) โ ((ฮฃ๐ โ ๐ด ๐ต mod ๐) = (ฮฃ๐ โ ๐ด (๐ต mod ๐) mod ๐) โ (ฮฃ๐ โ (๐ด โช {๐ง})๐ต mod ๐) = (ฮฃ๐ โ (๐ด โช {๐ง})(๐ต mod ๐) mod ๐))) | ||
Theorem | modfsummod 15614* | 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 15615* | 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 15616* | 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 15617* | 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 15618* | 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 15619* | 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 15620* | 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 15621* | 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 15622* | Sum of a telescoping series, using half-open intervals. (Contributed by Mario Carneiro, 2-May-2016.) |
โข (๐ = ๐ โ ๐ด = ๐ต) & โข (๐ = (๐ + 1) โ ๐ด = ๐ถ) & โข (๐ = ๐ โ ๐ด = ๐ท) & โข (๐ = ๐ โ ๐ด = ๐ธ) & โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) โ โข (๐ โ ฮฃ๐ โ (๐..^๐)(๐ต โ ๐ถ) = (๐ท โ ๐ธ)) | ||
Theorem | telfsumo2 15623* | Sum of a telescoping series. (Contributed by Mario Carneiro, 2-May-2016.) |
โข (๐ = ๐ โ ๐ด = ๐ต) & โข (๐ = (๐ + 1) โ ๐ด = ๐ถ) & โข (๐ = ๐ โ ๐ด = ๐ท) & โข (๐ = ๐ โ ๐ด = ๐ธ) & โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) โ โข (๐ โ ฮฃ๐ โ (๐..^๐)(๐ถ โ ๐ต) = (๐ธ โ ๐ท)) | ||
Theorem | telfsum 15624* | 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 15625* | 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 15626* | Summation by parts. (Contributed by Mario Carneiro, 13-Apr-2016.) |
โข (๐ = ๐ โ (๐ด = ๐ต โง ๐ = ๐)) & โข (๐ = (๐ + 1) โ (๐ด = ๐ถ โง ๐ = ๐)) & โข (๐ = ๐ โ (๐ด = ๐ท โง ๐ = ๐)) & โข (๐ = ๐ โ (๐ด = ๐ธ โง ๐ = ๐)) & โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) & โข ((๐ โง ๐ โ (๐...๐)) โ ๐ โ โ) โ โข (๐ โ ฮฃ๐ โ (๐..^๐)(๐ต ยท (๐ โ ๐)) = (((๐ธ ยท ๐) โ (๐ท ยท ๐)) โ ฮฃ๐ โ (๐..^๐)((๐ถ โ ๐ต) ยท ๐))) | ||
Theorem | fsumrelem 15627* | Lemma for fsumre 15628, fsumim 15629, and fsumcj 15630. (Contributed by Mario Carneiro, 25-Jul-2014.) (Revised by Mario Carneiro, 27-Dec-2014.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข ๐น:โโถโ & โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐นโ(๐ฅ + ๐ฆ)) = ((๐นโ๐ฅ) + (๐นโ๐ฆ))) โ โข (๐ โ (๐นโฮฃ๐ โ ๐ด ๐ต) = ฮฃ๐ โ ๐ด (๐นโ๐ต)) | ||
Theorem | fsumre 15628* | The real part of a sum. (Contributed by Paul Chapman, 9-Nov-2007.) (Revised by Mario Carneiro, 25-Jul-2014.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ (โโฮฃ๐ โ ๐ด ๐ต) = ฮฃ๐ โ ๐ด (โโ๐ต)) | ||
Theorem | fsumim 15629* | The imaginary part of a sum. (Contributed by Paul Chapman, 9-Nov-2007.) (Revised by Mario Carneiro, 25-Jul-2014.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ (โโฮฃ๐ โ ๐ด ๐ต) = ฮฃ๐ โ ๐ด (โโ๐ต)) | ||
Theorem | fsumcj 15630* | The complex conjugate of a sum. (Contributed by Paul Chapman, 9-Nov-2007.) (Revised by Mario Carneiro, 25-Jul-2014.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ (โโฮฃ๐ โ ๐ด ๐ต) = ฮฃ๐ โ ๐ด (โโ๐ต)) | ||
Theorem | fsumrlim 15631* | 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 15632* | 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 15633* | If ๐ด(๐) is O(1), then ฮฃ๐ โค ๐ฅ, ๐ด(๐) is O(๐ฅ). (Contributed by Mario Carneiro, 23-May-2016.) |
โข ((๐ โง ๐ โ โ) โ ๐ด โ ๐) & โข (๐ โ (๐ โ โ โฆ ๐ด) โ ๐(1)) โ โข (๐ โ (๐ฅ โ โ+ โฆ (ฮฃ๐ โ (1...(โโ๐ฅ))๐ด / ๐ฅ)) โ ๐(1)) | ||
Theorem | seqabs 15634* | 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 15635* | 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 15636* | 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 15637* | 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 15638* | 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 15639* | An absolutely convergent series is convergent. (Contributed by Mario Carneiro, 28-Apr-2014.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = (absโ(๐บโ๐))) & โข ((๐ โง ๐ โ ๐) โ (๐บโ๐) โ โ) & โข (๐ โ seq๐( + , ๐น) โ dom โ ) โ โข (๐ โ seq๐( + , ๐บ) โ dom โ ) | ||
Theorem | climfsum 15640* | 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 15641* | 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 15642* | 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 15643* | The cardinality of a nested disjoint indexed union. (Contributed by AV, 9-Jan-2022.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ Fin) & โข ((๐ โง ๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โ ๐ถ โ Fin) & โข (๐ โ Disj ๐ฅ โ ๐ด โช ๐ฆ โ ๐ต ๐ถ) & โข ((๐ โง ๐ฅ โ ๐ด) โ Disj ๐ฆ โ ๐ต ๐ถ) โ โข (๐ โ (โฏโโช ๐ฅ โ ๐ด โช ๐ฆ โ ๐ต ๐ถ) = ฮฃ๐ฅ โ ๐ด ฮฃ๐ฆ โ ๐ต (โฏโ๐ถ)) | ||
Theorem | hash2iun1dif1 15644* | The cardinality of a nested disjoint indexed union. (Contributed by AV, 9-Jan-2022.) |
โข (๐ โ ๐ด โ Fin) & โข ๐ต = (๐ด โ {๐ฅ}) & โข ((๐ โง ๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โ ๐ถ โ Fin) & โข (๐ โ Disj ๐ฅ โ ๐ด โช ๐ฆ โ ๐ต ๐ถ) & โข ((๐ โง ๐ฅ โ ๐ด) โ Disj ๐ฆ โ ๐ต ๐ถ) & โข ((๐ โง ๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โ (โฏโ๐ถ) = 1) โ โข (๐ โ (โฏโโช ๐ฅ โ ๐ด โช ๐ฆ โ ๐ต ๐ถ) = ((โฏโ๐ด) ยท ((โฏโ๐ด) โ 1))) | ||
Theorem | hashrabrex 15645* | 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 15646* | The cardinality of a disjoint union. (Contributed by Mario Carneiro, 24-Jan-2015.) |
โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ด โ Fin) & โข (๐ โ Disj ๐ฅ โ ๐ด ๐ฅ) โ โข (๐ โ (โฏโโช ๐ด) = ฮฃ๐ฅ โ ๐ด (โฏโ๐ฅ)) | ||
Theorem | qshash 15647* | 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 15648* | Translate the Ackermann bijection ackbij1 10108 onto the positive integers. (Contributed by Mario Carneiro, 16-Jan-2015.) |
โข ๐น = (๐ฅ โ (๐ซ โ0 โฉ Fin) โฆ ฮฃ๐ฆ โ ๐ฅ (2โ๐ฆ)) โ โข ๐น:(๐ซ โ0 โฉ Fin)โ1-1-ontoโโ0 | ||
Theorem | binomlem 15649* | Lemma for binom 15650 (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 15650* | 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 15649. 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 15651* | Special case of the binomial theorem for (1 + ๐ด)โ๐. (Contributed by Paul Chapman, 10-May-2007.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ ((1 + ๐ด)โ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท (๐ดโ๐))) | ||
Theorem | binom11 15652* | Special case of the binomial theorem for 2โ๐. (Contributed by Mario Carneiro, 13-Mar-2014.) |
โข (๐ โ โ0 โ (2โ๐) = ฮฃ๐ โ (0...๐)(๐C๐)) | ||
Theorem | binom1dif 15653* | 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 15654 | Lemma for bcxmas 15655. (Contributed by Paul Chapman, 18-May-2007.) |
โข (๐ด = ๐ต โ ((๐ + ๐ด)C๐ด) = ((๐ + ๐ต)C๐ต)) | ||
Theorem | bcxmas 15655* | 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 15656* | Lemma for incexc 15657. (Contributed by Mario Carneiro, 7-Aug-2017.) |
โข ((๐ด โ Fin โง ๐ต โ Fin) โ ((โฏโ๐ต) โ (โฏโ(๐ต โฉ โช ๐ด))) = ฮฃ๐ โ ๐ซ ๐ด((-1โ(โฏโ๐ )) ยท (โฏโ(๐ต โฉ โฉ ๐ )))) | ||
Theorem | incexc 15657* | 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 15658* | 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 15659* | Index shift of an infinite sum. (Contributed by Paul Chapman, 31-Oct-2007.) (Revised by Mario Carneiro, 24-Apr-2014.) |
โข ๐ = (โคโฅโ๐) & โข ๐ = (โคโฅโ(๐ + ๐พ)) & โข (๐ = (๐พ + ๐) โ ๐ด = ๐ต) & โข (๐ โ ๐พ โ โค) & โข (๐ โ ๐ โ โค) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) โ โข (๐ โ ฮฃ๐ โ ๐ ๐ด = ฮฃ๐ โ ๐ ๐ต) | ||
Theorem | isumsplit 15660* | 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 15661* | 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 15662* | 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 15663* | 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 15664* | 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 15665* | 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 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 | isumsup 15667* | 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 15668* | 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 15669* | Lemma for climcnds 15671: 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 15670* | Lemma for climcnds 15671: 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 15671* | 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 15672* | The sequence of reciprocals of real numbers, multiplied by the factor ๐ด, converges to zero. (Contributed by Mario Carneiro, 18-Sep-2014.) |
โข (๐ด โ โ โ (๐ โ โ+ โฆ (๐ด / ๐)) โ๐ 0) | ||
Theorem | divcnv 15673* | 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 15674 | The floor function satisfies โ(๐ฅ) = ๐ฅ + ๐(1). (Contributed by Mario Carneiro, 21-May-2016.) |
โข (๐ฅ โ โ โฆ (๐ฅ โ (โโ๐ฅ))) โ ๐(1) | ||
Theorem | divcnvshft 15675* | Limit of a ratio function. (Contributed by Scott Fenton, 16-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โค) & โข (๐ โ ๐น โ ๐) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = (๐ด / (๐ + ๐ต))) โ โข (๐ โ ๐น โ 0) | ||
Theorem | supcvg 15676* | 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 10305. (Contributed by Mario Carneiro, 15-Feb-2013.) (Proof shortened by Mario Carneiro, 26-Apr-2014.) |
โข ๐ โ V & โข ๐ = sup(๐ด, โ, < ) & โข ๐ = (๐ โ โ โฆ (๐ โ (1 / ๐))) & โข (๐ โ ๐ โ โ ) & โข (๐ โ ๐น:๐โontoโ๐ด) & โข (๐ โ ๐ด โ โ) & โข (๐ โ โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โ โข (๐ โ โ๐(๐:โโถ๐ โง (๐น โ ๐) โ ๐)) | ||
Theorem | infcvgaux1i 15677* | Auxiliary theorem for applications of supcvg 15676. Hypothesis for several supremum theorems. (Contributed by NM, 8-Feb-2008.) |
โข ๐ = {๐ฅ โฃ โ๐ฆ โ ๐ ๐ฅ = -๐ด} & โข (๐ฆ โ ๐ โ ๐ด โ โ) & โข ๐ โ ๐ & โข โ๐ง โ โ โ๐ค โ ๐ ๐ค โค ๐ง โ โข (๐ โ โ โง ๐ โ โ โง โ๐ง โ โ โ๐ค โ ๐ ๐ค โค ๐ง) | ||
Theorem | infcvgaux2i 15678* | Auxiliary theorem for applications of supcvg 15676. (Contributed by NM, 4-Mar-2008.) |
โข ๐ = {๐ฅ โฃ โ๐ฆ โ ๐ ๐ฅ = -๐ด} & โข (๐ฆ โ ๐ โ ๐ด โ โ) & โข ๐ โ ๐ & โข โ๐ง โ โ โ๐ค โ ๐ ๐ค โค ๐ง & โข ๐ = -sup(๐ , โ, < ) & โข (๐ฆ = ๐ถ โ ๐ด = ๐ต) โ โข (๐ถ โ ๐ โ ๐ โค ๐ต) | ||
Theorem | harmonic 15679 | 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 15680* | 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 15681* | 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 15682 | Lemma for trirecip 15683. 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 15683 | 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 15684* | 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 15685* | 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 15686* | The value of the finite geometric series ๐ดโ๐ + ๐ดโ(๐ + 1) +... + ๐ดโ(๐ โ 1). (Contributed by Mario Carneiro, 2-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 1) & โข (๐ โ ๐ โ โ0) & โข (๐ โ ๐ โ (โคโฅโ๐)) โ โข (๐ โ ฮฃ๐ โ (๐..^๐)(๐ดโ๐) = (((๐ดโ๐) โ (๐ดโ๐)) / (1 โ ๐ด))) | ||
Theorem | geoser 15687* | 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 15688* | The difference of two numbers to the same power is the difference of the two numbers multiplied with a finite sum. Generalization of subsq 14040. See Wikipedia "Fermat number", section "Other theorems about Fermat numbers", https://en.wikipedia.org/wiki/Fermat_number 14040, 5-Aug-2021. (Contributed by AV, 6-Aug-2021.) (Revised by AV, 19-Aug-2021.) |
โข ((๐ โ โ0 โง ๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ๐) โ (๐ตโ๐)) = ((๐ด โ ๐ต) ยท ฮฃ๐ โ (0..^๐)((๐ดโ๐) ยท (๐ตโ((๐ โ ๐) โ 1))))) | ||
Theorem | pwm1geoser 15689* | 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 15690* | 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 15691* | 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 15692* | 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 15693* | 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 15694* | 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 15695* | 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 15696* | 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 15697* | 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 15698* | 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 15699* | 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 15700* | The infinite sum of ๐ด ยท (๐ โ1) + ๐ด ยท (๐ โ2)... is (๐ด ยท ๐ ) / (1 โ ๐ ). (Contributed by NM, 2-Nov-2007.) (Revised by Mario Carneiro, 26-Apr-2014.) |
โข ((๐ด โ โ โง ๐ โ โ โง (absโ๐ ) < 1) โ ฮฃ๐ โ โ (๐ด ยท (๐ โ๐)) = ((๐ด ยท ๐ ) / (1 โ ๐ ))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |