![]() |
Metamath
Proof Explorer Theorem List (p. 157 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | clim2ser 15601* | The limit of an infinite series with an initial segment removed. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 1-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ (π β seqπ( + , πΉ) β π΄) β β’ (π β seq(π + 1)( + , πΉ) β (π΄ β (seqπ( + , πΉ)βπ))) | ||
Theorem | clim2ser2 15602* | The limit of an infinite series with an initial segment added. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 1-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ (π β seq(π + 1)( + , πΉ) β π΄) β β’ (π β seqπ( + , πΉ) β (π΄ + (seqπ( + , πΉ)βπ))) | ||
Theorem | iserex 15603* | An infinite series converges, if and only if the series does with initial terms removed. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 27-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ ((π β§ π β π) β (πΉβπ) β β) β β’ (π β (seqπ( + , πΉ) β dom β β seqπ( + , πΉ) β dom β )) | ||
Theorem | isermulc2 15604* | Multiplication of an infinite series by a constant. (Contributed by Paul Chapman, 14-Nov-2007.) (Revised by Mario Carneiro, 1-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΆ β β) & β’ (π β seqπ( + , πΉ) β π΄) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) = (πΆ Β· (πΉβπ))) β β’ (π β seqπ( + , πΊ) β (πΆ Β· π΄)) | ||
Theorem | climlec2 15605* | Comparison of a constant to the limit of a sequence. (Contributed by NM, 28-Feb-2008.) (Revised by Mario Carneiro, 1-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π΄ β β) & β’ (π β πΉ β π΅) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β π΄ β€ (πΉβπ)) β β’ (π β π΄ β€ π΅) | ||
Theorem | iserle 15606* | Comparison of the limits of two infinite series. (Contributed by Paul Chapman, 12-Nov-2007.) (Revised by Mario Carneiro, 3-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β seqπ( + , πΉ) β π΄) & β’ (π β seqπ( + , πΊ) β π΅) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) β β) & β’ ((π β§ π β π) β (πΉβπ) β€ (πΊβπ)) β β’ (π β π΄ β€ π΅) | ||
Theorem | iserge0 15607* | The limit of an infinite series of nonnegative reals is nonnegative. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 3-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β seqπ( + , πΉ) β π΄) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β 0 β€ (πΉβπ)) β β’ (π β 0 β€ π΄) | ||
Theorem | climub 15608* | The limit of a monotonic sequence is an upper bound. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 10-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ (π β πΉ β π΄) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΉβπ) β€ (πΉβ(π + 1))) β β’ (π β (πΉβπ) β€ π΄) | ||
Theorem | climserle 15609* | The partial sums of a converging infinite series with nonnegative terms are bounded by its limit. (Contributed by NM, 27-Dec-2005.) (Revised by Mario Carneiro, 9-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ (π β seqπ( + , πΉ) β π΄) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β 0 β€ (πΉβπ)) β β’ (π β (seqπ( + , πΉ)βπ) β€ π΄) | ||
Theorem | isershft 15610 | Index shift of the limit of an infinite series. (Contributed by Mario Carneiro, 6-Sep-2013.) (Revised by Mario Carneiro, 5-Nov-2013.) |
β’ πΉ β V β β’ ((π β β€ β§ π β β€) β (seqπ( + , πΉ) β π΄ β seq(π + π)( + , (πΉ shift π)) β π΄)) | ||
Theorem | isercolllem1 15611* | Lemma for isercoll 15614. (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ:ββΆπ) & β’ ((π β§ π β β) β (πΊβπ) < (πΊβ(π + 1))) β β’ ((π β§ π β β) β (πΊ βΎ π) Isom < , < (π, (πΊ β π))) | ||
Theorem | isercolllem2 15612* | Lemma for isercoll 15614. (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ:ββΆπ) & β’ ((π β§ π β β) β (πΊβπ) < (πΊβ(π + 1))) β β’ ((π β§ π β (β€β₯β(πΊβ1))) β (1...(β―β(πΊ β (β‘πΊ β (π...π))))) = (β‘πΊ β (π...π))) | ||
Theorem | isercolllem3 15613* | Lemma for isercoll 15614. (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ:ββΆπ) & β’ ((π β§ π β β) β (πΊβπ) < (πΊβ(π + 1))) & β’ ((π β§ π β (π β ran πΊ)) β (πΉβπ) = 0) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β β) β (π»βπ) = (πΉβ(πΊβπ))) β β’ ((π β§ π β (β€β₯β(πΊβ1))) β (seqπ( + , πΉ)βπ) = (seq1( + , π»)β(β―β(πΊ β (β‘πΊ β (π...π)))))) | ||
Theorem | isercoll 15614* | Rearrange an infinite series by spacing out the terms using an order isomorphism. (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ:ββΆπ) & β’ ((π β§ π β β) β (πΊβπ) < (πΊβ(π + 1))) & β’ ((π β§ π β (π β ran πΊ)) β (πΉβπ) = 0) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β β) β (π»βπ) = (πΉβ(πΊβπ))) β β’ (π β (seq1( + , π») β π΄ β seqπ( + , πΉ) β π΄)) | ||
Theorem | isercoll2 15615* | Generalize isercoll 15614 so that both sequences have arbitrary starting point. (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β πΊ:πβΆπ) & β’ ((π β§ π β π) β (πΊβπ) < (πΊβ(π + 1))) & β’ ((π β§ π β (π β ran πΊ)) β (πΉβπ) = 0) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (π»βπ) = (πΉβ(πΊβπ))) β β’ (π β (seqπ( + , π») β π΄ β seqπ( + , πΉ) β π΄)) | ||
Theorem | climsup 15616* | A bounded monotonic sequence converges to the supremum of its range. Theorem 12-5.1 of [Gleason] p. 180. (Contributed by NM, 13-Mar-2005.) (Revised by Mario Carneiro, 10-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆβ) & β’ ((π β§ π β π) β (πΉβπ) β€ (πΉβ(π + 1))) & β’ (π β βπ₯ β β βπ β π (πΉβπ) β€ π₯) β β’ (π β πΉ β sup(ran πΉ, β, < )) | ||
Theorem | climcau 15617* | A converging sequence of complex numbers is a Cauchy sequence. Theorem 12-5.3 of [Gleason] p. 180 (necessity part). (Contributed by NM, 16-Apr-2005.) (Revised by Mario Carneiro, 26-Apr-2014.) |
β’ π = (β€β₯βπ) β β’ ((π β β€ β§ πΉ β dom β ) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯) | ||
Theorem | climbdd 15618* | A converging sequence of complex numbers is bounded. (Contributed by Mario Carneiro, 9-Jul-2017.) |
β’ π = (β€β₯βπ) β β’ ((π β β€ β§ πΉ β dom β β§ βπ β π (πΉβπ) β β) β βπ₯ β β βπ β π (absβ(πΉβπ)) β€ π₯) | ||
Theorem | caucvgrlem 15619* | Lemma for caurcvgr 15620. (Contributed by Mario Carneiro, 15-Feb-2014.) (Revised by AV, 12-Sep-2020.) |
β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β sup(π΄, β*, < ) = +β) & β’ (π β βπ₯ β β+ βπ β π΄ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π₯)) & β’ (π β π β β+) β β’ (π β βπ β π΄ ((lim supβπΉ) β β β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· π )))) | ||
Theorem | caurcvgr 15620* | A Cauchy sequence of real numbers converges to its limit supremum. The third hypothesis specifies that πΉ is a Cauchy sequence. (Contributed by Mario Carneiro, 7-May-2016.) (Revised by AV, 12-Sep-2020.) |
β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β sup(π΄, β*, < ) = +β) & β’ (π β βπ₯ β β+ βπ β π΄ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π₯)) β β’ (π β πΉ βπ (lim supβπΉ)) | ||
Theorem | caucvgrlem2 15621* | Lemma for caucvgr 15622. (Contributed by NM, 4-Apr-2005.) (Proof shortened by Mario Carneiro, 8-May-2016.) |
β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β sup(π΄, β*, < ) = +β) & β’ (π β βπ₯ β β+ βπ β π΄ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π₯)) & β’ π»:ββΆβ & β’ (((πΉβπ) β β β§ (πΉβπ) β β) β (absβ((π»β(πΉβπ)) β (π»β(πΉβπ)))) β€ (absβ((πΉβπ) β (πΉβπ)))) β β’ (π β (π β π΄ β¦ (π»β(πΉβπ))) βπ ( βπ β(π» β πΉ))) | ||
Theorem | caucvgr 15622* | A Cauchy sequence of complex numbers converges to a complex number. Theorem 12-5.3 of [Gleason] p. 180 (sufficiency part). (Contributed by NM, 20-Dec-2006.) (Revised by Mario Carneiro, 8-May-2016.) |
β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β sup(π΄, β*, < ) = +β) & β’ (π β βπ₯ β β+ βπ β π΄ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π₯)) β β’ (π β πΉ β dom βπ ) | ||
Theorem | caurcvg 15623* | A Cauchy sequence of real numbers converges to its limit supremum. The fourth hypothesis specifies that πΉ is a Cauchy sequence. (Contributed by NM, 4-Apr-2005.) (Revised by AV, 12-Sep-2020.) |
β’ π = (β€β₯βπ) & β’ (π β πΉ:πβΆβ) & β’ (π β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯) β β’ (π β πΉ β (lim supβπΉ)) | ||
Theorem | caurcvg2 15624* | A Cauchy sequence of real numbers converges, existence version. (Contributed by NM, 4-Apr-2005.) (Revised by Mario Carneiro, 7-Sep-2014.) |
β’ π = (β€β₯βπ) & β’ (π β πΉ β π) & β’ (π β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯)) β β’ (π β πΉ β dom β ) | ||
Theorem | caucvg 15625* | A Cauchy sequence of complex numbers converges to a complex number. Theorem 12-5.3 of [Gleason] p. 180 (sufficiency part). (Contributed by NM, 20-Dec-2006.) (Proof shortened by Mario Carneiro, 15-Feb-2014.) (Revised by Mario Carneiro, 8-May-2016.) |
β’ π = (β€β₯βπ) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ (π β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β (πΉβπ))) < π₯) & β’ (π β πΉ β π) β β’ (π β πΉ β dom β ) | ||
Theorem | caucvgb 15626* | A function is convergent if and only if it is Cauchy. Theorem 12-5.3 of [Gleason] p. 180. (Contributed by Mario Carneiro, 15-Feb-2014.) |
β’ π = (β€β₯βπ) β β’ ((π β β€ β§ πΉ β π) β (πΉ β dom β β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯))) | ||
Theorem | serf0 15627* | If an infinite series converges, its underlying sequence converges to zero. (Contributed by NM, 2-Sep-2005.) (Revised by Mario Carneiro, 16-Feb-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π) & β’ (π β seqπ( + , πΉ) β dom β ) & β’ ((π β§ π β π) β (πΉβπ) β β) β β’ (π β πΉ β 0) | ||
Theorem | iseraltlem1 15628* | Lemma for iseralt 15631. A decreasing sequence with limit zero consists of positive terms. (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π β π) β (πΊβ(π + 1)) β€ (πΊβπ)) & β’ (π β πΊ β 0) β β’ ((π β§ π β π) β 0 β€ (πΊβπ)) | ||
Theorem | iseraltlem2 15629* | Lemma for iseralt 15631. The terms of an alternating series form a chain of inequalities in alternate terms, so that for example π(1) β€ π(3) β€ π(5) β€ ... and ... β€ π(4) β€ π(2) β€ π(0) (assuming π = 0 so that these terms are defined). (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π β π) β (πΊβ(π + 1)) β€ (πΊβπ)) & β’ (π β πΊ β 0) & β’ ((π β§ π β π) β (πΉβπ) = ((-1βπ) Β· (πΊβπ))) β β’ ((π β§ π β π β§ πΎ β β0) β ((-1βπ) Β· (seqπ( + , πΉ)β(π + (2 Β· πΎ)))) β€ ((-1βπ) Β· (seqπ( + , πΉ)βπ))) | ||
Theorem | iseraltlem3 15630* | Lemma for iseralt 15631. From iseraltlem2 15629, we have (-1βπ) Β· π(π + 2π) β€ (-1βπ) Β· π(π) and (-1βπ) Β· π(π + 1) β€ (-1βπ) Β· π(π + 2π + 1), and we also have (-1βπ) Β· π(π + 1) = (-1βπ) Β· π(π) β πΊ(π + 1) for each π by the definition of the partial sum π, so combining the inequalities we get (-1βπ) Β· π(π) β πΊ(π + 1) = (-1βπ) Β· π(π + 1) β€ (-1βπ) Β· π(π + 2π + 1) = (-1βπ) Β· π(π + 2π) β πΊ(π + 2π + 1) β€ (-1βπ) Β· π(π + 2π) β€ (-1βπ) Β· π(π) β€ (-1βπ) Β· π(π) + πΊ(π + 1), so β£ (-1βπ) Β· π(π + 2π + 1) β (-1βπ) Β· π(π) β£ = β£ π(π + 2π + 1) β π(π) β£ β€ πΊ(π + 1) and β£ (-1βπ) Β· π(π + 2π) β (-1βπ) Β· π(π) β£ = β£ π(π + 2π) β π(π) β£ β€ πΊ(π + 1). Thus, both even and odd partial sums are Cauchy if πΊ converges to 0. (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π β π) β (πΊβ(π + 1)) β€ (πΊβπ)) & β’ (π β πΊ β 0) & β’ ((π β§ π β π) β (πΉβπ) = ((-1βπ) Β· (πΊβπ))) β β’ ((π β§ π β π β§ πΎ β β0) β ((absβ((seqπ( + , πΉ)β(π + (2 Β· πΎ))) β (seqπ( + , πΉ)βπ))) β€ (πΊβ(π + 1)) β§ (absβ((seqπ( + , πΉ)β((π + (2 Β· πΎ)) + 1)) β (seqπ( + , πΉ)βπ))) β€ (πΊβ(π + 1)))) | ||
Theorem | iseralt 15631* | The alternating series test. If πΊ(π) is a decreasing sequence that converges to 0, then Ξ£π β π(-1βπ) Β· πΊ(π) is a convergent series. (Note that the first term is positive if π is even, and negative if π is odd. If the parity of your series does not match up with this, you will need to post-compose the series with multiplication by -1 using isermulc2 15604.) (Contributed by Mario Carneiro, 7-Apr-2015.) (Proof shortened by AV, 9-Jul-2022.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π β π) β (πΊβ(π + 1)) β€ (πΊβπ)) & β’ (π β πΊ β 0) & β’ ((π β§ π β π) β (πΉβπ) = ((-1βπ) Β· (πΊβπ))) β β’ (π β seqπ( + , πΉ) β dom β ) | ||
Syntax | csu 15632 | Extend class notation to include finite and infinite summations. (An underscore was added to the ASCII token in order to facilitate set.mm text searches, since "sum" is a commonly used word in comments.) |
class Ξ£π β π΄ π΅ | ||
Definition | df-sum 15633* | Define the sum of a series with an index set of integers π΄. The variable π is normally a free variable in π΅, i.e., π΅ can be thought of as π΅(π). This definition is the result of a collection of discussions over the most general definition for a sum that does not need the index set to have a specified ordering. This definition is in two parts, one for finite sums and one for subsets of the upper integers. When summing over a subset of the upper integers, we extend the index set to the upper integers by adding zero outside the domain, and then sum the set in order, setting the result to the limit of the partial sums, if it exists. This means that conditionally convergent sums can be evaluated meaningfully. For finite sums, we are explicitly order-independent, by picking any bijection to a 1-based finite sequence and summing in the induced order. These two methods of summation produce the same result on their common region of definition (i.e., finite sets of integers) by summo 15663. Examples: Ξ£π β {1, 2, 4}π means 1 + 2 + 4 = 7, and Ξ£π β β(1 / (2βπ)) = 1 means 1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum 15828). (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
β’ Ξ£π β π΄ π΅ = (β©π₯(βπ β β€ (π΄ β (β€β₯βπ) β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ β¦(πβπ) / πβ¦π΅))βπ)))) | ||
Theorem | sumex 15634 | A sum is a set. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
β’ Ξ£π β π΄ π΅ β V | ||
Theorem | sumeq1 15635 | Equality theorem for a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
β’ (π΄ = π΅ β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ) | ||
Theorem | nfsum1 15636 | Bound-variable hypothesis builder for sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
β’ β²ππ΄ β β’ β²πΞ£π β π΄ π΅ | ||
Theorem | nfsum 15637* | Bound-variable hypothesis builder for sum: if π₯ is (effectively) not free in π΄ and π΅, it is not free in Ξ£π β π΄π΅. Version of nfsum 15637 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 11-Dec-2005.) (Revised by Gino Giotto, 24-Feb-2024.) |
β’ β²π₯π΄ & β’ β²π₯π΅ β β’ β²π₯Ξ£π β π΄ π΅ | ||
Theorem | sumeq2w 15638 | Equality theorem for sum, when the class expressions π΅ and πΆ are equal everywhere. Proved using only Extensionality. (Contributed by Mario Carneiro, 24-Jun-2014.) (Revised by Mario Carneiro, 13-Jun-2019.) |
β’ (βπ π΅ = πΆ β Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ) | ||
Theorem | sumeq2ii 15639* | Equality theorem for sum, with the class expressions π΅ and πΆ guarded by I to be always sets. (Contributed by Mario Carneiro, 13-Jun-2019.) |
β’ (βπ β π΄ ( I βπ΅) = ( I βπΆ) β Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ) | ||
Theorem | sumeq2 15640* | Equality theorem for sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.) |
β’ (βπ β π΄ π΅ = πΆ β Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ) | ||
Theorem | cbvsum 15641* | Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
β’ (π = π β π΅ = πΆ) & β’ β²ππ΄ & β’ β²ππ΄ & β’ β²ππ΅ & β’ β²ππΆ β β’ Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ | ||
Theorem | cbvsumv 15642* | Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.) |
β’ (π = π β π΅ = πΆ) β β’ Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ | ||
Theorem | cbvsumi 15643* | Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) |
β’ β²ππ΅ & β’ β²ππΆ & β’ (π = π β π΅ = πΆ) β β’ Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ | ||
Theorem | sumeq1i 15644* | Equality inference for sum. (Contributed by NM, 2-Jan-2006.) |
β’ π΄ = π΅ β β’ Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ | ||
Theorem | sumeq2i 15645* | Equality inference for sum. (Contributed by NM, 3-Dec-2005.) |
β’ (π β π΄ β π΅ = πΆ) β β’ Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ | ||
Theorem | sumeq12i 15646* | Equality inference for sum. (Contributed by FL, 10-Dec-2006.) |
β’ π΄ = π΅ & β’ (π β π΄ β πΆ = π·) β β’ Ξ£π β π΄ πΆ = Ξ£π β π΅ π· | ||
Theorem | sumeq1d 15647* | Equality deduction for sum. (Contributed by NM, 1-Nov-2005.) |
β’ (π β π΄ = π΅) β β’ (π β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ) | ||
Theorem | sumeq2d 15648* | Equality deduction for sum. Note that unlike sumeq2dv 15649, π may occur in π. (Contributed by NM, 1-Nov-2005.) |
β’ (π β βπ β π΄ π΅ = πΆ) β β’ (π β Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ) | ||
Theorem | sumeq2dv 15649* | Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2014.) |
β’ ((π β§ π β π΄) β π΅ = πΆ) β β’ (π β Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ) | ||
Theorem | sumeq2sdv 15650* | Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Proof shortened by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΅ = πΆ) β β’ (π β Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ) | ||
Theorem | 2sumeq2dv 15651* | Equality deduction for double sum. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2014.) |
β’ ((π β§ π β π΄ β§ π β π΅) β πΆ = π·) β β’ (π β Ξ£π β π΄ Ξ£π β π΅ πΆ = Ξ£π β π΄ Ξ£π β π΅ π·) | ||
Theorem | sumeq12dv 15652* | Equality deduction for sum. (Contributed by NM, 1-Dec-2005.) |
β’ (π β π΄ = π΅) & β’ ((π β§ π β π΄) β πΆ = π·) β β’ (π β Ξ£π β π΄ πΆ = Ξ£π β π΅ π·) | ||
Theorem | sumeq12rdv 15653* | Equality deduction for sum. (Contributed by NM, 1-Dec-2005.) |
β’ (π β π΄ = π΅) & β’ ((π β§ π β π΅) β πΆ = π·) β β’ (π β Ξ£π β π΄ πΆ = Ξ£π β π΅ π·) | ||
Theorem | sum2id 15654* | The second class argument to a sum can be chosen so that it is always a set. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.) |
β’ Ξ£π β π΄ π΅ = Ξ£π β π΄ ( I βπ΅) | ||
Theorem | sumfc 15655* | A lemma to facilitate conversions from the function form to the class-variable form of a sum. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Mario Carneiro, 23-Apr-2014.) |
β’ Ξ£π β π΄ ((π β π΄ β¦ π΅)βπ) = Ξ£π β π΄ π΅ | ||
Theorem | fz1f1o 15656* | A lemma for working with finite sums. (Contributed by Mario Carneiro, 22-Apr-2014.) |
β’ (π΄ β Fin β (π΄ = β β¨ ((β―βπ΄) β β β§ βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄))) | ||
Theorem | sumrblem 15657* | Lemma for sumrb 15659. (Contributed by Mario Carneiro, 12-Aug-2013.) |
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β π β (β€β₯βπ)) β β’ ((π β§ π΄ β (β€β₯βπ)) β (seqπ( + , πΉ) βΎ (β€β₯βπ)) = seqπ( + , πΉ)) | ||
Theorem | fsumcvg 15658* | The sequence of partial sums of a finite sum converges to the whole sum. (Contributed by Mario Carneiro, 20-Apr-2014.) |
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β π β (β€β₯βπ)) & β’ (π β π΄ β (π...π)) β β’ (π β seqπ( + , πΉ) β (seqπ( + , πΉ)βπ)) | ||
Theorem | sumrb 15659* | Rebase the starting point of a sum. (Contributed by Mario Carneiro, 14-Jul-2013.) (Revised by Mario Carneiro, 9-Apr-2014.) |
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β π΄ β (β€β₯βπ)) & β’ (π β π΄ β (β€β₯βπ)) β β’ (π β (seqπ( + , πΉ) β πΆ β seqπ( + , πΉ) β πΆ)) | ||
Theorem | summolem3 15660* | Lemma for summo 15663. (Contributed by Mario Carneiro, 29-Mar-2014.) |
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ πΊ = (π β β β¦ β¦(πβπ) / πβ¦π΅) & β’ π» = (π β β β¦ β¦(πΎβπ) / πβ¦π΅) & β’ (π β (π β β β§ π β β)) & β’ (π β π:(1...π)β1-1-ontoβπ΄) & β’ (π β πΎ:(1...π)β1-1-ontoβπ΄) β β’ (π β (seq1( + , πΊ)βπ) = (seq1( + , π»)βπ)) | ||
Theorem | summolem2a 15661* | Lemma for summo 15663. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Mario Carneiro, 20-Apr-2014.) |
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ πΊ = (π β β β¦ β¦(πβπ) / πβ¦π΅) & β’ π» = (π β β β¦ β¦(πΎβπ) / πβ¦π΅) & β’ (π β π β β) & β’ (π β π β β€) & β’ (π β π΄ β (β€β₯βπ)) & β’ (π β π:(1...π)β1-1-ontoβπ΄) & β’ (π β πΎ Isom < , < ((1...(β―βπ΄)), π΄)) β β’ (π β seqπ( + , πΉ) β (seq1( + , πΊ)βπ)) | ||
Theorem | summolem2 15662* | Lemma for summo 15663. (Contributed by Mario Carneiro, 3-Apr-2014.) |
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ πΊ = (π β β β¦ β¦(πβπ) / πβ¦π΅) β β’ ((π β§ βπ β β€ (π΄ β (β€β₯βπ) β§ seqπ( + , πΉ) β π₯)) β (βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π¦ = (seq1( + , πΊ)βπ)) β π₯ = π¦)) | ||
Theorem | summo 15663* | A sum has at most one limit. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ πΊ = (π β β β¦ β¦(πβπ) / πβ¦π΅) β β’ (π β β*π₯(βπ β β€ (π΄ β (β€β₯βπ) β§ seqπ( + , πΉ) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , πΊ)βπ)))) | ||
Theorem | zsum 15664* | Series sum with index set a subset of the upper integers. (Contributed by Mario Carneiro, 13-Jun-2019.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π΄ β π) & β’ ((π β§ π β π) β (πΉβπ) = if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ = ( β βseqπ( + , πΉ))) | ||
Theorem | isum 15665* | Series sum with an upper integer index set (i.e. an infinite series). (Contributed by Mario Carneiro, 15-Jul-2013.) (Revised by Mario Carneiro, 7-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΅) & β’ ((π β§ π β π) β π΅ β β) β β’ (π β Ξ£π β π π΅ = ( β βseqπ( + , πΉ))) | ||
Theorem | fsum 15666* | The value of a sum over a nonempty finite set. (Contributed by Mario Carneiro, 20-Apr-2014.) (Revised by Mario Carneiro, 13-Jun-2019.) |
β’ (π = (πΉβπ) β π΅ = πΆ) & β’ (π β π β β) & β’ (π β πΉ:(1...π)β1-1-ontoβπ΄) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β (1...π)) β (πΊβπ) = πΆ) β β’ (π β Ξ£π β π΄ π΅ = (seq1( + , πΊ)βπ)) | ||
Theorem | sum0 15667 | Any sum over the empty set is zero. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Mario Carneiro, 20-Apr-2014.) |
β’ Ξ£π β β π΄ = 0 | ||
Theorem | sumz 15668* | Any sum of zero over a summable set is zero. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Mario Carneiro, 20-Apr-2014.) |
β’ ((π΄ β (β€β₯βπ) β¨ π΄ β Fin) β Ξ£π β π΄ 0 = 0) | ||
Theorem | fsumf1o 15669* | Re-index a finite sum using a bijection. (Contributed by Mario Carneiro, 20-Apr-2014.) |
β’ (π = πΊ β π΅ = π·) & β’ (π β πΆ β Fin) & β’ (π β πΉ:πΆβ1-1-ontoβπ΄) & β’ ((π β§ π β πΆ) β (πΉβπ) = πΊ) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ = Ξ£π β πΆ π·) | ||
Theorem | sumss 15670* | Change the index set to a subset in an upper integer sum. (Contributed by Mario Carneiro, 21-Apr-2014.) |
β’ (π β π΄ β π΅) & β’ ((π β§ π β π΄) β πΆ β β) & β’ ((π β§ π β (π΅ β π΄)) β πΆ = 0) & β’ (π β π΅ β (β€β₯βπ)) β β’ (π β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ) | ||
Theorem | fsumss 15671* | Change the index set to a subset in a finite sum. (Contributed by Mario Carneiro, 21-Apr-2014.) |
β’ (π β π΄ β π΅) & β’ ((π β§ π β π΄) β πΆ β β) & β’ ((π β§ π β (π΅ β π΄)) β πΆ = 0) & β’ (π β π΅ β Fin) β β’ (π β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ) | ||
Theorem | sumss2 15672* | Change the index set of a sum by adding zeroes. (Contributed by Mario Carneiro, 15-Jul-2013.) (Revised by Mario Carneiro, 20-Apr-2014.) |
β’ (((π΄ β π΅ β§ βπ β π΄ πΆ β β) β§ (π΅ β (β€β₯βπ) β¨ π΅ β Fin)) β Ξ£π β π΄ πΆ = Ξ£π β π΅ if(π β π΄, πΆ, 0)) | ||
Theorem | fsumcvg2 15673* | The sequence of partial sums of a finite sum converges to the whole sum. (Contributed by Mario Carneiro, 20-Apr-2014.) |
β’ ((π β§ π β (β€β₯βπ)) β (πΉβπ) = if(π β π΄, π΅, 0)) & β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β π΄ β (π...π)) β β’ (π β seqπ( + , πΉ) β (seqπ( + , πΉ)βπ)) | ||
Theorem | fsumsers 15674* | Special case of series sum over a finite upper integer index set. (Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Mario Carneiro, 21-Apr-2014.) |
β’ ((π β§ π β (β€β₯βπ)) β (πΉβπ) = if(π β π΄, π΅, 0)) & β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β π΄ β (π...π)) β β’ (π β Ξ£π β π΄ π΅ = (seqπ( + , πΉ)βπ)) | ||
Theorem | fsumcvg3 15675* | A finite sum is convergent. (Contributed by Mario Carneiro, 24-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π΄ β Fin) & β’ (π β π΄ β π) & β’ ((π β§ π β π) β (πΉβπ) = if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β seqπ( + , πΉ) β dom β ) | ||
Theorem | fsumser 15676* | A finite sum expressed in terms of a partial sum of an infinite series. The recursive definition follows as fsum1 15693 and fsump1i 15715, which should make our notation clear and from which, along with closure fsumcl 15679, we will derive the basic properties of finite sums. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 21-Apr-2014.) |
β’ ((π β§ π β (π...π)) β (πΉβπ) = π΄) & β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β π΄ β β) β β’ (π β Ξ£π β (π...π)π΄ = (seqπ( + , πΉ)βπ)) | ||
Theorem | fsumcl2lem 15677* | - Lemma for finite sum closures. (The "-" before "Lemma" forces the math content to be displayed in the Statement List - NM 11-Feb-2008.) (Contributed by Mario Carneiro, 3-Jun-2014.) |
β’ (π β π β β) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β π) & β’ (π β π΄ β β ) β β’ (π β Ξ£π β π΄ π΅ β π) | ||
Theorem | fsumcllem 15678* | - Lemma for finite sum closures. (The "-" before "Lemma" forces the math content to be displayed in the Statement List - NM 11-Feb-2008.) (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 3-Jun-2014.) |
β’ (π β π β β) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β π) & β’ (π β 0 β π) β β’ (π β Ξ£π β π΄ π΅ β π) | ||
Theorem | fsumcl 15679* | Closure of a finite sum of complex numbers π΄(π). (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ β β) | ||
Theorem | fsumrecl 15680* | Closure of a finite sum of reals. (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ β β) | ||
Theorem | fsumzcl 15681* | Closure of a finite sum of integers. (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β€) β β’ (π β Ξ£π β π΄ π΅ β β€) | ||
Theorem | fsumnn0cl 15682* | Closure of a finite sum of nonnegative integers. (Contributed by Mario Carneiro, 23-Apr-2015.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β0) β β’ (π β Ξ£π β π΄ π΅ β β0) | ||
Theorem | fsumrpcl 15683* | Closure of a finite sum of positive reals. (Contributed by Mario Carneiro, 3-Jun-2014.) |
β’ (π β π΄ β Fin) & β’ (π β π΄ β β ) & β’ ((π β§ π β π΄) β π΅ β β+) β β’ (π β Ξ£π β π΄ π΅ β β+) | ||
Theorem | fsumclf 15684* | Closure of a finite sum of complex numbers π΄(π). A version of fsumcl 15679 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ β β) | ||
Theorem | fsumzcl2 15685* | A finite sum with integer summands is an integer. (Contributed by Alexander van der Vekens, 31-Aug-2018.) |
β’ ((π΄ β Fin β§ βπ β π΄ π΅ β β€) β Ξ£π β π΄ π΅ β β€) | ||
Theorem | fsumadd 15686* | The sum of two finite sums. (Contributed by NM, 14-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β πΆ β β) β β’ (π β Ξ£π β π΄ (π΅ + πΆ) = (Ξ£π β π΄ π΅ + Ξ£π β π΄ πΆ)) | ||
Theorem | fsumsplit 15687* | Split a sum into two parts. (Contributed by Mario Carneiro, 18-Aug-2013.) (Revised by Mario Carneiro, 22-Apr-2014.) |
β’ (π β (π΄ β© π΅) = β ) & β’ (π β π = (π΄ βͺ π΅)) & β’ (π β π β Fin) & β’ ((π β§ π β π) β πΆ β β) β β’ (π β Ξ£π β π πΆ = (Ξ£π β π΄ πΆ + Ξ£π β π΅ πΆ)) | ||
Theorem | fsumsplitf 15688* | Split a sum into two parts. A version of fsumsplit 15687 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ (π β (π΄ β© π΅) = β ) & β’ (π β π = (π΄ βͺ π΅)) & β’ (π β π β Fin) & β’ ((π β§ π β π) β πΆ β β) β β’ (π β Ξ£π β π πΆ = (Ξ£π β π΄ πΆ + Ξ£π β π΅ πΆ)) | ||
Theorem | sumsnf 15689* | A sum of a singleton is the term. A version of sumsn 15692 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ΅ & β’ (π = π β π΄ = π΅) β β’ ((π β π β§ π΅ β β) β Ξ£π β {π}π΄ = π΅) | ||
Theorem | fsumsplitsn 15690* | Separate out a term in a finite sum. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ β²ππ· & β’ (π β π΄ β Fin) & β’ (π β π΅ β π) & β’ (π β Β¬ π΅ β π΄) & β’ ((π β§ π β π΄) β πΆ β β) & β’ (π = π΅ β πΆ = π·) & β’ (π β π· β β) β β’ (π β Ξ£π β (π΄ βͺ {π΅})πΆ = (Ξ£π β π΄ πΆ + π·)) | ||
Theorem | fsumsplit1 15691* | Separate out a term in a finite sum. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ β²ππ· & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β πΆ β π΄) & β’ (π = πΆ β π΅ = π·) β β’ (π β Ξ£π β π΄ π΅ = (π· + Ξ£π β (π΄ β {πΆ})π΅)) | ||
Theorem | sumsn 15692* | A sum of a singleton is the term. (Contributed by Mario Carneiro, 22-Apr-2014.) |
β’ (π = π β π΄ = π΅) β β’ ((π β π β§ π΅ β β) β Ξ£π β {π}π΄ = π΅) | ||
Theorem | fsum1 15693* | The finite sum of π΄(π) from π = π to π (i.e. a sum with only one term) is π΅ i.e. π΄(π). (Contributed by NM, 8-Nov-2005.) (Revised by Mario Carneiro, 21-Apr-2014.) |
β’ (π = π β π΄ = π΅) β β’ ((π β β€ β§ π΅ β β) β Ξ£π β (π...π)π΄ = π΅) | ||
Theorem | sumpr 15694* | A sum over a pair is the sum of the elements. (Contributed by Thierry Arnoux, 12-Dec-2016.) |
β’ (π = π΄ β πΆ = π·) & β’ (π = π΅ β πΆ = πΈ) & β’ (π β (π· β β β§ πΈ β β)) & β’ (π β (π΄ β π β§ π΅ β π)) & β’ (π β π΄ β π΅) β β’ (π β Ξ£π β {π΄, π΅}πΆ = (π· + πΈ)) | ||
Theorem | sumtp 15695* | A sum over a triple is the sum of the elements. (Contributed by AV, 24-Jul-2020.) |
β’ (π = π΄ β π· = πΈ) & β’ (π = π΅ β π· = πΉ) & β’ (π = πΆ β π· = πΊ) & β’ (π β (πΈ β β β§ πΉ β β β§ πΊ β β)) & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) & β’ (π β π΄ β π΅) & β’ (π β π΄ β πΆ) & β’ (π β π΅ β πΆ) β β’ (π β Ξ£π β {π΄, π΅, πΆ}π· = ((πΈ + πΉ) + πΊ)) | ||
Theorem | sumsns 15696* | A sum of a singleton is the term. (Contributed by Mario Carneiro, 22-Apr-2014.) |
β’ ((π β π β§ β¦π / πβ¦π΄ β β) β Ξ£π β {π}π΄ = β¦π / πβ¦π΄) | ||
Theorem | fsumm1 15697* | Separate out the last term in a finite sum. (Contributed by Mario Carneiro, 26-Apr-2014.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β π΄ β β) & β’ (π = π β π΄ = π΅) β β’ (π β Ξ£π β (π...π)π΄ = (Ξ£π β (π...(π β 1))π΄ + π΅)) | ||
Theorem | fzosump1 15698* | Separate out the last term in a finite sum. (Contributed by Mario Carneiro, 13-Apr-2016.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β π΄ β β) & β’ (π = π β π΄ = π΅) β β’ (π β Ξ£π β (π..^(π + 1))π΄ = (Ξ£π β (π..^π)π΄ + π΅)) | ||
Theorem | fsum1p 15699* | 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 15700* | 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 β§ βπ β (π΄ βͺ {π})π΅ β β€) β Ξ£π β (π΄ βͺ {π})π΅ β β€) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |