![]() |
Metamath
Proof Explorer Theorem List (p. 157 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rlimsqz2 15601* | Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by Mario Carneiro, 3-Feb-2014.) (Revised by Mario Carneiro, 20-May-2016.) |
β’ (π β π· β β) & β’ (π β π β β) & β’ (π β (π₯ β π΄ β¦ π΅) βπ π·) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ ((π β§ (π₯ β π΄ β§ π β€ π₯)) β πΆ β€ π΅) & β’ ((π β§ (π₯ β π΄ β§ π β€ π₯)) β π· β€ πΆ) β β’ (π β (π₯ β π΄ β¦ πΆ) βπ π·) | ||
Theorem | lo1le 15602* | Transfer eventual upper boundedness from a larger function to a smaller function. (Contributed by Mario Carneiro, 26-May-2016.) |
β’ (π β π β β) & β’ (π β (π₯ β π΄ β¦ π΅) β β€π(1)) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ ((π β§ (π₯ β π΄ β§ π β€ π₯)) β πΆ β€ π΅) β β’ (π β (π₯ β π΄ β¦ πΆ) β β€π(1)) | ||
Theorem | o1le 15603* | Transfer eventual boundedness from a larger function to a smaller function. (Contributed by Mario Carneiro, 25-Sep-2014.) (Proof shortened by Mario Carneiro, 26-May-2016.) |
β’ (π β π β β) & β’ (π β (π₯ β π΄ β¦ π΅) β π(1)) & β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ ((π β§ (π₯ β π΄ β§ π β€ π₯)) β (absβπΆ) β€ (absβπ΅)) β β’ (π β (π₯ β π΄ β¦ πΆ) β π(1)) | ||
Theorem | rlimno1 15604* | A function whose inverse converges to zero is unbounded. (Contributed by Mario Carneiro, 30-May-2016.) |
β’ (π β sup(π΄, β*, < ) = +β) & β’ (π β (π₯ β π΄ β¦ (1 / π΅)) βπ 0) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β π΅ β 0) β β’ (π β Β¬ (π₯ β π΄ β¦ π΅) β π(1)) | ||
Theorem | clim2ser 15605* | 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 15606* | 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 15607* | 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 15608* | 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 15609* | 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 15610* | 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 15611* | 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 15612* | 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 15613* | 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 15614 | 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 15615* | Lemma for isercoll 15618. (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ:ββΆπ) & β’ ((π β§ π β β) β (πΊβπ) < (πΊβ(π + 1))) β β’ ((π β§ π β β) β (πΊ βΎ π) Isom < , < (π, (πΊ β π))) | ||
Theorem | isercolllem2 15616* | Lemma for isercoll 15618. (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ:ββΆπ) & β’ ((π β§ π β β) β (πΊβπ) < (πΊβ(π + 1))) β β’ ((π β§ π β (β€β₯β(πΊβ1))) β (1...(β―β(πΊ β (β‘πΊ β (π...π))))) = (β‘πΊ β (π...π))) | ||
Theorem | isercolllem3 15617* | Lemma for isercoll 15618. (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ:ββΆπ) & β’ ((π β§ π β β) β (πΊβπ) < (πΊβ(π + 1))) & β’ ((π β§ π β (π β ran πΊ)) β (πΉβπ) = 0) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β β) β (π»βπ) = (πΉβ(πΊβπ))) β β’ ((π β§ π β (β€β₯β(πΊβ1))) β (seqπ( + , πΉ)βπ) = (seq1( + , π»)β(β―β(πΊ β (β‘πΊ β (π...π)))))) | ||
Theorem | isercoll 15618* | 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 15619* | Generalize isercoll 15618 so that both sequences have arbitrary starting point. (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β πΊ:πβΆπ) & β’ ((π β§ π β π) β (πΊβπ) < (πΊβ(π + 1))) & β’ ((π β§ π β (π β ran πΊ)) β (πΉβπ) = 0) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (π»βπ) = (πΉβ(πΊβπ))) β β’ (π β (seqπ( + , π») β π΄ β seqπ( + , πΉ) β π΄)) | ||
Theorem | climsup 15620* | 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 15621* | 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 15622* | A converging sequence of complex numbers is bounded. (Contributed by Mario Carneiro, 9-Jul-2017.) |
β’ π = (β€β₯βπ) β β’ ((π β β€ β§ πΉ β dom β β§ βπ β π (πΉβπ) β β) β βπ₯ β β βπ β π (absβ(πΉβπ)) β€ π₯) | ||
Theorem | caucvgrlem 15623* | Lemma for caurcvgr 15624. (Contributed by Mario Carneiro, 15-Feb-2014.) (Revised by AV, 12-Sep-2020.) |
β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β sup(π΄, β*, < ) = +β) & β’ (π β βπ₯ β β+ βπ β π΄ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π₯)) & β’ (π β π β β+) β β’ (π β βπ β π΄ ((lim supβπΉ) β β β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· π )))) | ||
Theorem | caurcvgr 15624* | 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 15625* | Lemma for caucvgr 15626. (Contributed by NM, 4-Apr-2005.) (Proof shortened by Mario Carneiro, 8-May-2016.) |
β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β sup(π΄, β*, < ) = +β) & β’ (π β βπ₯ β β+ βπ β π΄ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π₯)) & β’ π»:ββΆβ & β’ (((πΉβπ) β β β§ (πΉβπ) β β) β (absβ((π»β(πΉβπ)) β (π»β(πΉβπ)))) β€ (absβ((πΉβπ) β (πΉβπ)))) β β’ (π β (π β π΄ β¦ (π»β(πΉβπ))) βπ ( βπ β(π» β πΉ))) | ||
Theorem | caucvgr 15626* | 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 15627* | 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 15628* | 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 15629* | 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 15630* | 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 15631* | 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 15632* | Lemma for iseralt 15635. A decreasing sequence with limit zero consists of positive terms. (Contributed by Mario Carneiro, 6-Apr-2015.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π β π) β (πΊβ(π + 1)) β€ (πΊβπ)) & β’ (π β πΊ β 0) β β’ ((π β§ π β π) β 0 β€ (πΊβπ)) | ||
Theorem | iseraltlem2 15633* | Lemma for iseralt 15635. 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 15634* | Lemma for iseralt 15635. From iseraltlem2 15633, 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 15635* | 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 15608.) (Contributed by Mario Carneiro, 7-Apr-2015.) (Proof shortened by AV, 9-Jul-2022.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ:πβΆβ) & β’ ((π β§ π β π) β (πΊβ(π + 1)) β€ (πΊβπ)) & β’ (π β πΊ β 0) & β’ ((π β§ π β π) β (πΉβπ) = ((-1βπ) Β· (πΊβπ))) β β’ (π β seqπ( + , πΉ) β dom β ) | ||
Syntax | csu 15636 | 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 15637* | 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 15667. Examples: Ξ£π β {1, 2, 4}π means 1 + 2 + 4 = 7, and Ξ£π β β(1 / (2βπ)) = 1 means 1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum 15832). (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
β’ Ξ£π β π΄ π΅ = (β©π₯(βπ β β€ (π΄ β (β€β₯βπ) β§ seqπ( + , (π β β€ β¦ if(π β π΄, β¦π / πβ¦π΅, 0))) β π₯) β¨ βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π₯ = (seq1( + , (π β β β¦ β¦(πβπ) / πβ¦π΅))βπ)))) | ||
Theorem | sumex 15638 | A sum is a set. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
β’ Ξ£π β π΄ π΅ β V | ||
Theorem | sumeq1 15639 | Equality theorem for a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
β’ (π΄ = π΅ β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ) | ||
Theorem | nfsum1 15640 | Bound-variable hypothesis builder for sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
β’ β²ππ΄ β β’ β²πΞ£π β π΄ π΅ | ||
Theorem | nfsum 15641* | Bound-variable hypothesis builder for sum: if π₯ is (effectively) not free in π΄ and π΅, it is not free in Ξ£π β π΄π΅. Version of nfsum 15641 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by NM, 11-Dec-2005.) (Revised by Gino Giotto, 24-Feb-2024.) |
β’ β²π₯π΄ & β’ β²π₯π΅ β β’ β²π₯Ξ£π β π΄ π΅ | ||
Theorem | sumeq2w 15642 | 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 15643* | 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 15644* | Equality theorem for sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.) |
β’ (βπ β π΄ π΅ = πΆ β Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ) | ||
Theorem | cbvsum 15645* | Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
β’ (π = π β π΅ = πΆ) & β’ β²ππ΄ & β’ β²ππ΄ & β’ β²ππ΅ & β’ β²ππΆ β β’ Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ | ||
Theorem | cbvsumv 15646* | Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.) |
β’ (π = π β π΅ = πΆ) β β’ Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ | ||
Theorem | cbvsumi 15647* | Change bound variable in a sum. (Contributed by NM, 11-Dec-2005.) |
β’ β²ππ΅ & β’ β²ππΆ & β’ (π = π β π΅ = πΆ) β β’ Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ | ||
Theorem | sumeq1i 15648* | Equality inference for sum. (Contributed by NM, 2-Jan-2006.) |
β’ π΄ = π΅ β β’ Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ | ||
Theorem | sumeq2i 15649* | Equality inference for sum. (Contributed by NM, 3-Dec-2005.) |
β’ (π β π΄ β π΅ = πΆ) β β’ Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ | ||
Theorem | sumeq12i 15650* | Equality inference for sum. (Contributed by FL, 10-Dec-2006.) |
β’ π΄ = π΅ & β’ (π β π΄ β πΆ = π·) β β’ Ξ£π β π΄ πΆ = Ξ£π β π΅ π· | ||
Theorem | sumeq1d 15651* | Equality deduction for sum. (Contributed by NM, 1-Nov-2005.) |
β’ (π β π΄ = π΅) β β’ (π β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ) | ||
Theorem | sumeq2d 15652* | Equality deduction for sum. Note that unlike sumeq2dv 15653, π may occur in π. (Contributed by NM, 1-Nov-2005.) |
β’ (π β βπ β π΄ π΅ = πΆ) β β’ (π β Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ) | ||
Theorem | sumeq2dv 15653* | Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2014.) |
β’ ((π β§ π β π΄) β π΅ = πΆ) β β’ (π β Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ) | ||
Theorem | sumeq2sdv 15654* | Equality deduction for sum. (Contributed by NM, 3-Jan-2006.) (Proof shortened by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΅ = πΆ) β β’ (π β Ξ£π β π΄ π΅ = Ξ£π β π΄ πΆ) | ||
Theorem | 2sumeq2dv 15655* | Equality deduction for double sum. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2014.) |
β’ ((π β§ π β π΄ β§ π β π΅) β πΆ = π·) β β’ (π β Ξ£π β π΄ Ξ£π β π΅ πΆ = Ξ£π β π΄ Ξ£π β π΅ π·) | ||
Theorem | sumeq12dv 15656* | Equality deduction for sum. (Contributed by NM, 1-Dec-2005.) |
β’ (π β π΄ = π΅) & β’ ((π β§ π β π΄) β πΆ = π·) β β’ (π β Ξ£π β π΄ πΆ = Ξ£π β π΅ π·) | ||
Theorem | sumeq12rdv 15657* | Equality deduction for sum. (Contributed by NM, 1-Dec-2005.) |
β’ (π β π΄ = π΅) & β’ ((π β§ π β π΅) β πΆ = π·) β β’ (π β Ξ£π β π΄ πΆ = Ξ£π β π΅ π·) | ||
Theorem | sum2id 15658* | 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 15659* | 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 15660* | A lemma for working with finite sums. (Contributed by Mario Carneiro, 22-Apr-2014.) |
β’ (π΄ β Fin β (π΄ = β β¨ ((β―βπ΄) β β β§ βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄))) | ||
Theorem | sumrblem 15661* | Lemma for sumrb 15663. (Contributed by Mario Carneiro, 12-Aug-2013.) |
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β π β (β€β₯βπ)) β β’ ((π β§ π΄ β (β€β₯βπ)) β (seqπ( + , πΉ) βΎ (β€β₯βπ)) = seqπ( + , πΉ)) | ||
Theorem | fsumcvg 15662* | 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 15663* | 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 15664* | Lemma for summo 15667. (Contributed by Mario Carneiro, 29-Mar-2014.) |
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ πΊ = (π β β β¦ β¦(πβπ) / πβ¦π΅) & β’ π» = (π β β β¦ β¦(πΎβπ) / πβ¦π΅) & β’ (π β (π β β β§ π β β)) & β’ (π β π:(1...π)β1-1-ontoβπ΄) & β’ (π β πΎ:(1...π)β1-1-ontoβπ΄) β β’ (π β (seq1( + , πΊ)βπ) = (seq1( + , π»)βπ)) | ||
Theorem | summolem2a 15665* | Lemma for summo 15667. (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 15666* | Lemma for summo 15667. (Contributed by Mario Carneiro, 3-Apr-2014.) |
β’ πΉ = (π β β€ β¦ if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) & β’ πΊ = (π β β β¦ β¦(πβπ) / πβ¦π΅) β β’ ((π β§ βπ β β€ (π΄ β (β€β₯βπ) β§ seqπ( + , πΉ) β π₯)) β (βπ β β βπ(π:(1...π)β1-1-ontoβπ΄ β§ π¦ = (seq1( + , πΊ)βπ)) β π₯ = π¦)) | ||
Theorem | summo 15667* | 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 15668* | Series sum with index set a subset of the upper integers. (Contributed by Mario Carneiro, 13-Jun-2019.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π΄ β π) & β’ ((π β§ π β π) β (πΉβπ) = if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ = ( β βseqπ( + , πΉ))) | ||
Theorem | isum 15669* | 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 15670* | 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 15671 | 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 15672* | 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 15673* | Re-index a finite sum using a bijection. (Contributed by Mario Carneiro, 20-Apr-2014.) |
β’ (π = πΊ β π΅ = π·) & β’ (π β πΆ β Fin) & β’ (π β πΉ:πΆβ1-1-ontoβπ΄) & β’ ((π β§ π β πΆ) β (πΉβπ) = πΊ) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ = Ξ£π β πΆ π·) | ||
Theorem | sumss 15674* | Change the index set to a subset in an upper integer sum. (Contributed by Mario Carneiro, 21-Apr-2014.) |
β’ (π β π΄ β π΅) & β’ ((π β§ π β π΄) β πΆ β β) & β’ ((π β§ π β (π΅ β π΄)) β πΆ = 0) & β’ (π β π΅ β (β€β₯βπ)) β β’ (π β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ) | ||
Theorem | fsumss 15675* | Change the index set to a subset in a finite sum. (Contributed by Mario Carneiro, 21-Apr-2014.) |
β’ (π β π΄ β π΅) & β’ ((π β§ π β π΄) β πΆ β β) & β’ ((π β§ π β (π΅ β π΄)) β πΆ = 0) & β’ (π β π΅ β Fin) β β’ (π β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ) | ||
Theorem | sumss2 15676* | 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 15677* | 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 15678* | 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 15679* | A finite sum is convergent. (Contributed by Mario Carneiro, 24-Apr-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π΄ β Fin) & β’ (π β π΄ β π) & β’ ((π β§ π β π) β (πΉβπ) = if(π β π΄, π΅, 0)) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β seqπ( + , πΉ) β dom β ) | ||
Theorem | fsumser 15680* | A finite sum expressed in terms of a partial sum of an infinite series. The recursive definition follows as fsum1 15697 and fsump1i 15719, which should make our notation clear and from which, along with closure fsumcl 15683, 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 15681* | - 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 15682* | - 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 15683* | Closure of a finite sum of complex numbers π΄(π). (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ β β) | ||
Theorem | fsumrecl 15684* | Closure of a finite sum of reals. (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ β β) | ||
Theorem | fsumzcl 15685* | Closure of a finite sum of integers. (Contributed by NM, 9-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β€) β β’ (π β Ξ£π β π΄ π΅ β β€) | ||
Theorem | fsumnn0cl 15686* | Closure of a finite sum of nonnegative integers. (Contributed by Mario Carneiro, 23-Apr-2015.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β0) β β’ (π β Ξ£π β π΄ π΅ β β0) | ||
Theorem | fsumrpcl 15687* | Closure of a finite sum of positive reals. (Contributed by Mario Carneiro, 3-Jun-2014.) |
β’ (π β π΄ β Fin) & β’ (π β π΄ β β ) & β’ ((π β§ π β π΄) β π΅ β β+) β β’ (π β Ξ£π β π΄ π΅ β β+) | ||
Theorem | fsumclf 15688* | Closure of a finite sum of complex numbers π΄(π). A version of fsumcl 15683 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ β β) | ||
Theorem | fsumzcl2 15689* | A finite sum with integer summands is an integer. (Contributed by Alexander van der Vekens, 31-Aug-2018.) |
β’ ((π΄ β Fin β§ βπ β π΄ π΅ β β€) β Ξ£π β π΄ π΅ β β€) | ||
Theorem | fsumadd 15690* | The sum of two finite sums. (Contributed by NM, 14-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β πΆ β β) β β’ (π β Ξ£π β π΄ (π΅ + πΆ) = (Ξ£π β π΄ π΅ + Ξ£π β π΄ πΆ)) | ||
Theorem | fsumsplit 15691* | Split a sum into two parts. (Contributed by Mario Carneiro, 18-Aug-2013.) (Revised by Mario Carneiro, 22-Apr-2014.) |
β’ (π β (π΄ β© π΅) = β ) & β’ (π β π = (π΄ βͺ π΅)) & β’ (π β π β Fin) & β’ ((π β§ π β π) β πΆ β β) β β’ (π β Ξ£π β π πΆ = (Ξ£π β π΄ πΆ + Ξ£π β π΅ πΆ)) | ||
Theorem | fsumsplitf 15692* | Split a sum into two parts. A version of fsumsplit 15691 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ (π β (π΄ β© π΅) = β ) & β’ (π β π = (π΄ βͺ π΅)) & β’ (π β π β Fin) & β’ ((π β§ π β π) β πΆ β β) β β’ (π β Ξ£π β π πΆ = (Ξ£π β π΄ πΆ + Ξ£π β π΅ πΆ)) | ||
Theorem | sumsnf 15693* | A sum of a singleton is the term. A version of sumsn 15696 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ΅ & β’ (π = π β π΄ = π΅) β β’ ((π β π β§ π΅ β β) β Ξ£π β {π}π΄ = π΅) | ||
Theorem | fsumsplitsn 15694* | Separate out a term in a finite sum. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ β²ππ· & β’ (π β π΄ β Fin) & β’ (π β π΅ β π) & β’ (π β Β¬ π΅ β π΄) & β’ ((π β§ π β π΄) β πΆ β β) & β’ (π = π΅ β πΆ = π·) & β’ (π β π· β β) β β’ (π β Ξ£π β (π΄ βͺ {π΅})πΆ = (Ξ£π β π΄ πΆ + π·)) | ||
Theorem | fsumsplit1 15695* | Separate out a term in a finite sum. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ β²ππ· & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β πΆ β π΄) & β’ (π = πΆ β π΅ = π·) β β’ (π β Ξ£π β π΄ π΅ = (π· + Ξ£π β (π΄ β {πΆ})π΅)) | ||
Theorem | sumsn 15696* | A sum of a singleton is the term. (Contributed by Mario Carneiro, 22-Apr-2014.) |
β’ (π = π β π΄ = π΅) β β’ ((π β π β§ π΅ β β) β Ξ£π β {π}π΄ = π΅) | ||
Theorem | fsum1 15697* | 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 15698* | A sum over a pair is the sum of the elements. (Contributed by Thierry Arnoux, 12-Dec-2016.) |
β’ (π = π΄ β πΆ = π·) & β’ (π = π΅ β πΆ = πΈ) & β’ (π β (π· β β β§ πΈ β β)) & β’ (π β (π΄ β π β§ π΅ β π)) & β’ (π β π΄ β π΅) β β’ (π β Ξ£π β {π΄, π΅}πΆ = (π· + πΈ)) | ||
Theorem | sumtp 15699* | A sum over a triple is the sum of the elements. (Contributed by AV, 24-Jul-2020.) |
β’ (π = π΄ β π· = πΈ) & β’ (π = π΅ β π· = πΉ) & β’ (π = πΆ β π· = πΊ) & β’ (π β (πΈ β β β§ πΉ β β β§ πΊ β β)) & β’ (π β (π΄ β π β§ π΅ β π β§ πΆ β π)) & β’ (π β π΄ β π΅) & β’ (π β π΄ β πΆ) & β’ (π β π΅ β πΆ) β β’ (π β Ξ£π β {π΄, π΅, πΆ}π· = ((πΈ + πΉ) + πΊ)) | ||
Theorem | sumsns 15700* | A sum of a singleton is the term. (Contributed by Mario Carneiro, 22-Apr-2014.) |
β’ ((π β π β§ β¦π / πβ¦π΄ β β) β Ξ£π β {π}π΄ = β¦π / πβ¦π΄) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |