![]() |
Metamath
Proof Explorer Theorem List (p. 158 of 480) | < 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: | ![]() (1-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fsum1p 15701* | Separate out the first term in a finite sum. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 23-Apr-2014.) |
โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) & โข (๐ = ๐ โ ๐ด = ๐ต) โ โข (๐ โ ฮฃ๐ โ (๐...๐)๐ด = (๐ต + ฮฃ๐ โ ((๐ + 1)...๐)๐ด)) | ||
Theorem | fsummsnunz 15702* | A finite sum all of whose summands are integers is itself an integer (case where the summation set is the union of a finite set and a singleton). (Contributed by Alexander van der Vekens, 1-Sep-2018.) (Revised by AV, 17-Dec-2021.) |
โข ((๐ด โ Fin โง โ๐ โ (๐ด โช {๐})๐ต โ โค) โ ฮฃ๐ โ (๐ด โช {๐})๐ต โ โค) | ||
Theorem | fsumsplitsnun 15703* | Separate out a term in a finite sum by splitting the sum into two parts. (Contributed by Alexander van der Vekens, 1-Sep-2018.) (Revised by AV, 17-Dec-2021.) |
โข ((๐ด โ Fin โง (๐ โ ๐ โง ๐ โ ๐ด) โง โ๐ โ (๐ด โช {๐})๐ต โ โค) โ ฮฃ๐ โ (๐ด โช {๐})๐ต = (ฮฃ๐ โ ๐ด ๐ต + โฆ๐ / ๐โฆ๐ต)) | ||
Theorem | fsump1 15704* | The addition of the next term in a finite sum of ๐ด(๐) is the current term plus ๐ต i.e. ๐ด(๐ + 1). (Contributed by NM, 4-Nov-2005.) (Revised by Mario Carneiro, 21-Apr-2014.) (Proof shortened by SN, 22-Mar-2025.) |
โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...(๐ + 1))) โ ๐ด โ โ) & โข (๐ = (๐ + 1) โ ๐ด = ๐ต) โ โข (๐ โ ฮฃ๐ โ (๐...(๐ + 1))๐ด = (ฮฃ๐ โ (๐...๐)๐ด + ๐ต)) | ||
Theorem | isumclim 15705* | An infinite sum equals the value its series converges to. (Contributed by NM, 25-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2014.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = ๐ด) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) & โข (๐ โ seq๐( + , ๐น) โ ๐ต) โ โข (๐ โ ฮฃ๐ โ ๐ ๐ด = ๐ต) | ||
Theorem | isumclim2 15706* | A converging series converges to its infinite sum. (Contributed by NM, 2-Jan-2006.) (Revised by Mario Carneiro, 23-Apr-2014.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = ๐ด) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) & โข (๐ โ seq๐( + , ๐น) โ dom โ ) โ โข (๐ โ seq๐( + , ๐น) โ ฮฃ๐ โ ๐ ๐ด) | ||
Theorem | isumclim3 15707* | 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.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐น โ dom โ ) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = ฮฃ๐ โ (๐...๐)๐ด) โ โข (๐ โ ๐น โ ฮฃ๐ โ ๐ ๐ด) | ||
Theorem | sumnul 15708* | 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.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = ๐ด) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) & โข (๐ โ ยฌ seq๐( + , ๐น) โ dom โ ) โ โข (๐ โ ฮฃ๐ โ ๐ ๐ด = โ ) | ||
Theorem | isumcl 15709* | The sum of a converging infinite series is a complex number. (Contributed by NM, 13-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2014.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = ๐ด) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) & โข (๐ โ seq๐( + , ๐น) โ dom โ ) โ โข (๐ โ ฮฃ๐ โ ๐ ๐ด โ โ) | ||
Theorem | isummulc2 15710* | An infinite sum multiplied by a constant. (Contributed by NM, 12-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = ๐ด) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) & โข (๐ โ seq๐( + , ๐น) โ dom โ ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (๐ต ยท ฮฃ๐ โ ๐ ๐ด) = ฮฃ๐ โ ๐ (๐ต ยท ๐ด)) | ||
Theorem | isummulc1 15711* | An infinite sum multiplied by a constant. (Contributed by NM, 13-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = ๐ด) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) & โข (๐ โ seq๐( + , ๐น) โ dom โ ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ (ฮฃ๐ โ ๐ ๐ด ยท ๐ต) = ฮฃ๐ โ ๐ (๐ด ยท ๐ต)) | ||
Theorem | isumdivc 15712* | An infinite sum divided by a constant. (Contributed by NM, 2-Jan-2006.) (Revised by Mario Carneiro, 23-Apr-2014.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = ๐ด) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) & โข (๐ โ seq๐( + , ๐น) โ dom โ ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ต โ 0) โ โข (๐ โ (ฮฃ๐ โ ๐ ๐ด / ๐ต) = ฮฃ๐ โ ๐ (๐ด / ๐ต)) | ||
Theorem | isumrecl 15713* | The sum of a converging infinite real series is a real number. (Contributed by Mario Carneiro, 24-Apr-2014.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = ๐ด) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) & โข (๐ โ seq๐( + , ๐น) โ dom โ ) โ โข (๐ โ ฮฃ๐ โ ๐ ๐ด โ โ) | ||
Theorem | isumge0 15714* | An infinite sum of nonnegative terms is nonnegative. (Contributed by Mario Carneiro, 28-Apr-2014.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = ๐ด) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) & โข (๐ โ seq๐( + , ๐น) โ dom โ ) & โข ((๐ โง ๐ โ ๐) โ 0 โค ๐ด) โ โข (๐ โ 0 โค ฮฃ๐ โ ๐ ๐ด) | ||
Theorem | isumadd 15715* | Addition of infinite sums. (Contributed by Mario Carneiro, 18-Aug-2013.) (Revised by Mario Carneiro, 23-Apr-2014.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = ๐ด) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) & โข ((๐ โง ๐ โ ๐) โ (๐บโ๐) = ๐ต) & โข ((๐ โง ๐ โ ๐) โ ๐ต โ โ) & โข (๐ โ seq๐( + , ๐น) โ dom โ ) & โข (๐ โ seq๐( + , ๐บ) โ dom โ ) โ โข (๐ โ ฮฃ๐ โ ๐ (๐ด + ๐ต) = (ฮฃ๐ โ ๐ ๐ด + ฮฃ๐ โ ๐ ๐ต)) | ||
Theorem | sumsplit 15716* | Split a sum into two parts. (Contributed by Mario Carneiro, 18-Aug-2013.) (Revised by Mario Carneiro, 23-Apr-2014.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ (๐ด โฉ ๐ต) = โ ) & โข (๐ โ (๐ด โช ๐ต) โ ๐) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = if(๐ โ ๐ด, ๐ถ, 0)) & โข ((๐ โง ๐ โ ๐) โ (๐บโ๐) = if(๐ โ ๐ต, ๐ถ, 0)) & โข ((๐ โง ๐ โ (๐ด โช ๐ต)) โ ๐ถ โ โ) & โข (๐ โ seq๐( + , ๐น) โ dom โ ) & โข (๐ โ seq๐( + , ๐บ) โ dom โ ) โ โข (๐ โ ฮฃ๐ โ (๐ด โช ๐ต)๐ถ = (ฮฃ๐ โ ๐ด ๐ถ + ฮฃ๐ โ ๐ต ๐ถ)) | ||
Theorem | fsump1i 15717* | Optimized version of fsump1 15704 for making sums of a concrete number of terms. (Contributed by Mario Carneiro, 23-Apr-2014.) |
โข ๐ = (โคโฅโ๐) & โข ๐ = (๐พ + 1) & โข (๐ = ๐ โ ๐ด = ๐ต) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) & โข (๐ โ (๐พ โ ๐ โง ฮฃ๐ โ (๐...๐พ)๐ด = ๐)) & โข (๐ โ (๐ + ๐ต) = ๐) โ โข (๐ โ (๐ โ ๐ โง ฮฃ๐ โ (๐...๐)๐ด = ๐)) | ||
Theorem | fsum2dlem 15718* | Lemma for fsum2d 15719- induction step. (Contributed by Mario Carneiro, 23-Apr-2014.) |
โข (๐ง = โจ๐, ๐โฉ โ ๐ท = ๐ถ) & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ Fin) & โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ถ โ โ) & โข (๐ โ ยฌ ๐ฆ โ ๐ฅ) & โข (๐ โ (๐ฅ โช {๐ฆ}) โ ๐ด) & โข (๐ โ ฮฃ๐ โ ๐ฅ ฮฃ๐ โ ๐ต ๐ถ = ฮฃ๐ง โ โช ๐ โ ๐ฅ ({๐} ร ๐ต)๐ท) โ โข ((๐ โง ๐) โ ฮฃ๐ โ (๐ฅ โช {๐ฆ})ฮฃ๐ โ ๐ต ๐ถ = ฮฃ๐ง โ โช ๐ โ (๐ฅ โช {๐ฆ})({๐} ร ๐ต)๐ท) | ||
Theorem | fsum2d 15719* | 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.) |
โข (๐ง = โจ๐, ๐โฉ โ ๐ท = ๐ถ) & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ Fin) & โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ถ โ โ) โ โข (๐ โ ฮฃ๐ โ ๐ด ฮฃ๐ โ ๐ต ๐ถ = ฮฃ๐ง โ โช ๐ โ ๐ด ({๐} ร ๐ต)๐ท) | ||
Theorem | fsumxp 15720* | Combine two sums into a single sum over the cartesian product. (Contributed by Mario Carneiro, 23-Apr-2014.) |
โข (๐ง = โจ๐, ๐โฉ โ ๐ท = ๐ถ) & โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ต โ Fin) & โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ถ โ โ) โ โข (๐ โ ฮฃ๐ โ ๐ด ฮฃ๐ โ ๐ต ๐ถ = ฮฃ๐ง โ (๐ด ร ๐ต)๐ท) | ||
Theorem | fsumcnv 15721* | Transform a region of summation by using the converse operation. (Contributed by Mario Carneiro, 23-Apr-2014.) |
โข (๐ฅ = โจ๐, ๐โฉ โ ๐ต = ๐ท) & โข (๐ฆ = โจ๐, ๐โฉ โ ๐ถ = ๐ท) & โข (๐ โ ๐ด โ Fin) & โข (๐ โ Rel ๐ด) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ ฮฃ๐ฅ โ ๐ด ๐ต = ฮฃ๐ฆ โ โก ๐ด๐ถ) | ||
Theorem | fsumcom2 15722* | 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.) |
โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ถ โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ Fin) & โข (๐ โ ((๐ โ ๐ด โง ๐ โ ๐ต) โ (๐ โ ๐ถ โง ๐ โ ๐ท))) & โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ธ โ โ) โ โข (๐ โ ฮฃ๐ โ ๐ด ฮฃ๐ โ ๐ต ๐ธ = ฮฃ๐ โ ๐ถ ฮฃ๐ โ ๐ท ๐ธ) | ||
Theorem | fsumcom 15723* | Interchange order of summation. (Contributed by NM, 15-Nov-2005.) (Revised by Mario Carneiro, 23-Apr-2014.) |
โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ต โ Fin) & โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ถ โ โ) โ โข (๐ โ ฮฃ๐ โ ๐ด ฮฃ๐ โ ๐ต ๐ถ = ฮฃ๐ โ ๐ต ฮฃ๐ โ ๐ด ๐ถ) | ||
Theorem | fsum0diaglem 15724* | Lemma for fsum0diag 15725. (Contributed by Mario Carneiro, 28-Apr-2014.) (Revised by Mario Carneiro, 8-Apr-2016.) |
โข ((๐ โ (0...๐) โง ๐ โ (0...(๐ โ ๐))) โ (๐ โ (0...๐) โง ๐ โ (0...(๐ โ ๐)))) | ||
Theorem | fsum0diag 15725* | 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.) |
โข ((๐ โง (๐ โ (0...๐) โง ๐ โ (0...(๐ โ ๐)))) โ ๐ด โ โ) โ โข (๐ โ ฮฃ๐ โ (0...๐)ฮฃ๐ โ (0...(๐ โ ๐))๐ด = ฮฃ๐ โ (0...๐)ฮฃ๐ โ (0...(๐ โ ๐))๐ด) | ||
Theorem | mptfzshft 15726* | 1-1 onto function in maps-to notation which shifts a finite set of sequential integers. Formerly part of proof for fsumshft 15728. (Contributed by AV, 24-Aug-2019.) |
โข (๐ โ ๐พ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) โ โข (๐ โ (๐ โ ((๐ + ๐พ)...(๐ + ๐พ)) โฆ (๐ โ ๐พ)):((๐ + ๐พ)...(๐ + ๐พ))โ1-1-ontoโ(๐...๐)) | ||
Theorem | fsumrev 15727* | Reversal of a finite sum. (Contributed by NM, 26-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
โข (๐ โ ๐พ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) & โข (๐ = (๐พ โ ๐) โ ๐ด = ๐ต) โ โข (๐ โ ฮฃ๐ โ (๐...๐)๐ด = ฮฃ๐ โ ((๐พ โ ๐)...(๐พ โ ๐))๐ต) | ||
Theorem | fsumshft 15728* | 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 15729* | Negative index shift of a finite sum. (Contributed by NM, 28-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
โข (๐ โ ๐พ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) & โข (๐ = (๐ + ๐พ) โ ๐ด = ๐ต) โ โข (๐ โ ฮฃ๐ โ (๐...๐)๐ด = ฮฃ๐ โ ((๐ โ ๐พ)...(๐ โ ๐พ))๐ต) | ||
Theorem | fsumrev2 15730* | Reversal of a finite sum. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 13-Apr-2016.) |
โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) & โข (๐ = ((๐ + ๐) โ ๐) โ ๐ด = ๐ต) โ โข (๐ โ ฮฃ๐ โ (๐...๐)๐ด = ฮฃ๐ โ (๐...๐)๐ต) | ||
Theorem | fsum0diag2 15731* | 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 15732* | A finite sum multiplied by a constant. (Contributed by NM, 12-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ถ โ โ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ (๐ถ ยท ฮฃ๐ โ ๐ด ๐ต) = ฮฃ๐ โ ๐ด (๐ถ ยท ๐ต)) | ||
Theorem | fsummulc1 15733* | A finite sum multiplied by a constant. (Contributed by NM, 13-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ถ โ โ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ (ฮฃ๐ โ ๐ด ๐ต ยท ๐ถ) = ฮฃ๐ โ ๐ด (๐ต ยท ๐ถ)) | ||
Theorem | fsumdivc 15734* | A finite sum divided by a constant. (Contributed by NM, 2-Jan-2006.) (Revised by Mario Carneiro, 24-Apr-2014.) |
โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ถ โ โ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข (๐ โ ๐ถ โ 0) โ โข (๐ โ (ฮฃ๐ โ ๐ด ๐ต / ๐ถ) = ฮฃ๐ โ ๐ด (๐ต / ๐ถ)) | ||
Theorem | fsumneg 15735* | Negation of a finite sum. (Contributed by Scott Fenton, 12-Jun-2013.) (Revised by Mario Carneiro, 24-Apr-2014.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ ฮฃ๐ โ ๐ด -๐ต = -ฮฃ๐ โ ๐ด ๐ต) | ||
Theorem | fsumsub 15736* | Split a finite sum over a subtraction. (Contributed by Scott Fenton, 12-Jun-2013.) (Revised by Mario Carneiro, 24-Apr-2014.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โ) โ โข (๐ โ ฮฃ๐ โ ๐ด (๐ต โ ๐ถ) = (ฮฃ๐ โ ๐ด ๐ต โ ฮฃ๐ โ ๐ด ๐ถ)) | ||
Theorem | fsum2mul 15737* | Separate the nested sum of the product ๐ถ(๐) ยท ๐ท(๐). (Contributed by NM, 13-Nov-2005.) (Revised by Mario Carneiro, 24-Apr-2014.) |
โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ต โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โ) & โข ((๐ โง ๐ โ ๐ต) โ ๐ท โ โ) โ โข (๐ โ ฮฃ๐ โ ๐ด ฮฃ๐ โ ๐ต (๐ถ ยท ๐ท) = (ฮฃ๐ โ ๐ด ๐ถ ยท ฮฃ๐ โ ๐ต ๐ท)) | ||
Theorem | fsumconst 15738* | 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 15739* | 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 15740* | Lemma 1 for modfsummods 15741. (Contributed by Alexander van der Vekens, 1-Sep-2018.) |
โข (โ๐ โ (๐ด โช {๐ง})๐ต โ โค โ โฆ๐ง / ๐โฆ๐ต โ โค) | ||
Theorem | modfsummods 15741* | Induction step for modfsummod 15742. (Contributed by Alexander van der Vekens, 1-Sep-2018.) |
โข ((๐ด โ Fin โง ๐ โ โ โง โ๐ โ (๐ด โช {๐ง})๐ต โ โค) โ ((ฮฃ๐ โ ๐ด ๐ต mod ๐) = (ฮฃ๐ โ ๐ด (๐ต mod ๐) mod ๐) โ (ฮฃ๐ โ (๐ด โช {๐ง})๐ต mod ๐) = (ฮฃ๐ โ (๐ด โช {๐ง})(๐ต mod ๐) mod ๐))) | ||
Theorem | modfsummod 15742* | 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 15743* | 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 15744* | 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 15745* | 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 15746* | 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 15747* | 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 15748* | 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 15749* | 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 15750* | Sum of a telescoping series, using half-open intervals. (Contributed by Mario Carneiro, 2-May-2016.) |
โข (๐ = ๐ โ ๐ด = ๐ต) & โข (๐ = (๐ + 1) โ ๐ด = ๐ถ) & โข (๐ = ๐ โ ๐ด = ๐ท) & โข (๐ = ๐ โ ๐ด = ๐ธ) & โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) โ โข (๐ โ ฮฃ๐ โ (๐..^๐)(๐ต โ ๐ถ) = (๐ท โ ๐ธ)) | ||
Theorem | telfsumo2 15751* | Sum of a telescoping series. (Contributed by Mario Carneiro, 2-May-2016.) |
โข (๐ = ๐ โ ๐ด = ๐ต) & โข (๐ = (๐ + 1) โ ๐ด = ๐ถ) & โข (๐ = ๐ โ ๐ด = ๐ท) & โข (๐ = ๐ โ ๐ด = ๐ธ) & โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) โ โข (๐ โ ฮฃ๐ โ (๐..^๐)(๐ถ โ ๐ต) = (๐ธ โ ๐ท)) | ||
Theorem | telfsum 15752* | 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 15753* | 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 15754* | Summation by parts. (Contributed by Mario Carneiro, 13-Apr-2016.) |
โข (๐ = ๐ โ (๐ด = ๐ต โง ๐ = ๐)) & โข (๐ = (๐ + 1) โ (๐ด = ๐ถ โง ๐ = ๐)) & โข (๐ = ๐ โ (๐ด = ๐ท โง ๐ = ๐)) & โข (๐ = ๐ โ (๐ด = ๐ธ โง ๐ = ๐)) & โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) & โข ((๐ โง ๐ โ (๐...๐)) โ ๐ โ โ) โ โข (๐ โ ฮฃ๐ โ (๐..^๐)(๐ต ยท (๐ โ ๐)) = (((๐ธ ยท ๐) โ (๐ท ยท ๐)) โ ฮฃ๐ โ (๐..^๐)((๐ถ โ ๐ต) ยท ๐))) | ||
Theorem | fsumrelem 15755* | Lemma for fsumre 15756, fsumim 15757, and fsumcj 15758. (Contributed by Mario Carneiro, 25-Jul-2014.) (Revised by Mario Carneiro, 27-Dec-2014.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข ๐น:โโถโ & โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐นโ(๐ฅ + ๐ฆ)) = ((๐นโ๐ฅ) + (๐นโ๐ฆ))) โ โข (๐ โ (๐นโฮฃ๐ โ ๐ด ๐ต) = ฮฃ๐ โ ๐ด (๐นโ๐ต)) | ||
Theorem | fsumre 15756* | The real part of a sum. (Contributed by Paul Chapman, 9-Nov-2007.) (Revised by Mario Carneiro, 25-Jul-2014.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ (โโฮฃ๐ โ ๐ด ๐ต) = ฮฃ๐ โ ๐ด (โโ๐ต)) | ||
Theorem | fsumim 15757* | The imaginary part of a sum. (Contributed by Paul Chapman, 9-Nov-2007.) (Revised by Mario Carneiro, 25-Jul-2014.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ (โโฮฃ๐ โ ๐ด ๐ต) = ฮฃ๐ โ ๐ด (โโ๐ต)) | ||
Theorem | fsumcj 15758* | The complex conjugate of a sum. (Contributed by Paul Chapman, 9-Nov-2007.) (Revised by Mario Carneiro, 25-Jul-2014.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ (โโฮฃ๐ โ ๐ด ๐ต) = ฮฃ๐ โ ๐ด (โโ๐ต)) | ||
Theorem | fsumrlim 15759* | 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 15760* | 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 15761* | If ๐ด(๐) is O(1), then ฮฃ๐ โค ๐ฅ, ๐ด(๐) is O(๐ฅ). (Contributed by Mario Carneiro, 23-May-2016.) |
โข ((๐ โง ๐ โ โ) โ ๐ด โ ๐) & โข (๐ โ (๐ โ โ โฆ ๐ด) โ ๐(1)) โ โข (๐ โ (๐ฅ โ โ+ โฆ (ฮฃ๐ โ (1...(โโ๐ฅ))๐ด / ๐ฅ)) โ ๐(1)) | ||
Theorem | seqabs 15762* | 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 15763* | 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 15764* | 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 15765* | 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 15766* | 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 15767* | An absolutely convergent series is convergent. (Contributed by Mario Carneiro, 28-Apr-2014.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = (absโ(๐บโ๐))) & โข ((๐ โง ๐ โ ๐) โ (๐บโ๐) โ โ) & โข (๐ โ seq๐( + , ๐น) โ dom โ ) โ โข (๐ โ seq๐( + , ๐บ) โ dom โ ) | ||
Theorem | climfsum 15768* | 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 15769* | 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 15770* | 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 15771* | The cardinality of a nested disjoint indexed union. (Contributed by AV, 9-Jan-2022.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ Fin) & โข ((๐ โง ๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โ ๐ถ โ Fin) & โข (๐ โ Disj ๐ฅ โ ๐ด โช ๐ฆ โ ๐ต ๐ถ) & โข ((๐ โง ๐ฅ โ ๐ด) โ Disj ๐ฆ โ ๐ต ๐ถ) โ โข (๐ โ (โฏโโช ๐ฅ โ ๐ด โช ๐ฆ โ ๐ต ๐ถ) = ฮฃ๐ฅ โ ๐ด ฮฃ๐ฆ โ ๐ต (โฏโ๐ถ)) | ||
Theorem | hash2iun1dif1 15772* | The cardinality of a nested disjoint indexed union. (Contributed by AV, 9-Jan-2022.) |
โข (๐ โ ๐ด โ Fin) & โข ๐ต = (๐ด โ {๐ฅ}) & โข ((๐ โง ๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โ ๐ถ โ Fin) & โข (๐ โ Disj ๐ฅ โ ๐ด โช ๐ฆ โ ๐ต ๐ถ) & โข ((๐ โง ๐ฅ โ ๐ด) โ Disj ๐ฆ โ ๐ต ๐ถ) & โข ((๐ โง ๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โ (โฏโ๐ถ) = 1) โ โข (๐ โ (โฏโโช ๐ฅ โ ๐ด โช ๐ฆ โ ๐ต ๐ถ) = ((โฏโ๐ด) ยท ((โฏโ๐ด) โ 1))) | ||
Theorem | hashrabrex 15773* | 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 15774* | The cardinality of a disjoint union. (Contributed by Mario Carneiro, 24-Jan-2015.) |
โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ด โ Fin) & โข (๐ โ Disj ๐ฅ โ ๐ด ๐ฅ) โ โข (๐ โ (โฏโโช ๐ด) = ฮฃ๐ฅ โ ๐ด (โฏโ๐ฅ)) | ||
Theorem | qshash 15775* | 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 15776* | Translate the Ackermann bijection ackbij1 10235 onto the positive integers. (Contributed by Mario Carneiro, 16-Jan-2015.) |
โข ๐น = (๐ฅ โ (๐ซ โ0 โฉ Fin) โฆ ฮฃ๐ฆ โ ๐ฅ (2โ๐ฆ)) โ โข ๐น:(๐ซ โ0 โฉ Fin)โ1-1-ontoโโ0 | ||
Theorem | binomlem 15777* | Lemma for binom 15778 (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 15778* | 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 15777. 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 15779* | Special case of the binomial theorem for (1 + ๐ด)โ๐. (Contributed by Paul Chapman, 10-May-2007.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ ((1 + ๐ด)โ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท (๐ดโ๐))) | ||
Theorem | binom11 15780* | Special case of the binomial theorem for 2โ๐. (Contributed by Mario Carneiro, 13-Mar-2014.) |
โข (๐ โ โ0 โ (2โ๐) = ฮฃ๐ โ (0...๐)(๐C๐)) | ||
Theorem | binom1dif 15781* | 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 15782 | Lemma for bcxmas 15783. (Contributed by Paul Chapman, 18-May-2007.) |
โข (๐ด = ๐ต โ ((๐ + ๐ด)C๐ด) = ((๐ + ๐ต)C๐ต)) | ||
Theorem | bcxmas 15783* | 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 15784* | Lemma for incexc 15785. (Contributed by Mario Carneiro, 7-Aug-2017.) |
โข ((๐ด โ Fin โง ๐ต โ Fin) โ ((โฏโ๐ต) โ (โฏโ(๐ต โฉ โช ๐ด))) = ฮฃ๐ โ ๐ซ ๐ด((-1โ(โฏโ๐ )) ยท (โฏโ(๐ต โฉ โฉ ๐ )))) | ||
Theorem | incexc 15785* | 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 15786* | 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 15787* | Index shift of an infinite sum. (Contributed by Paul Chapman, 31-Oct-2007.) (Revised by Mario Carneiro, 24-Apr-2014.) |
โข ๐ = (โคโฅโ๐) & โข ๐ = (โคโฅโ(๐ + ๐พ)) & โข (๐ = (๐พ + ๐) โ ๐ด = ๐ต) & โข (๐ โ ๐พ โ โค) & โข (๐ โ ๐ โ โค) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) โ โข (๐ โ ฮฃ๐ โ ๐ ๐ด = ฮฃ๐ โ ๐ ๐ต) | ||
Theorem | isumsplit 15788* | 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 15789* | 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 15790* | 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 15791* | 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 15792* | 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 15793* | 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 15794* | 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 15795* | 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 15796* | 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 15797* | Lemma for climcnds 15799: 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 15798* | Lemma for climcnds 15799: 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 15799* | 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 15800* | The sequence of reciprocals of real numbers, multiplied by the factor ๐ด, converges to zero. (Contributed by Mario Carneiro, 18-Sep-2014.) |
โข (๐ด โ โ โ (๐ โ โ+ โฆ (๐ด / ๐)) โ๐ 0) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |