![]() |
Metamath
Proof Explorer Theorem List (p. 158 of 473) | < 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-29863) |
![]() (29864-31386) |
![]() (31387-47259) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | iserabs 15701* | 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 15702* | 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 15703* | 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 15704* | 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 15705* | An absolutely convergent series is convergent. (Contributed by Mario Carneiro, 28-Apr-2014.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = (absโ(๐บโ๐))) & โข ((๐ โง ๐ โ ๐) โ (๐บโ๐) โ โ) & โข (๐ โ seq๐( + , ๐น) โ dom โ ) โ โข (๐ โ seq๐( + , ๐บ) โ dom โ ) | ||
Theorem | climfsum 15706* | 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 15707* | 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 15708* | 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 15709* | The cardinality of a nested disjoint indexed union. (Contributed by AV, 9-Jan-2022.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ Fin) & โข ((๐ โง ๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โ ๐ถ โ Fin) & โข (๐ โ Disj ๐ฅ โ ๐ด โช ๐ฆ โ ๐ต ๐ถ) & โข ((๐ โง ๐ฅ โ ๐ด) โ Disj ๐ฆ โ ๐ต ๐ถ) โ โข (๐ โ (โฏโโช ๐ฅ โ ๐ด โช ๐ฆ โ ๐ต ๐ถ) = ฮฃ๐ฅ โ ๐ด ฮฃ๐ฆ โ ๐ต (โฏโ๐ถ)) | ||
Theorem | hash2iun1dif1 15710* | The cardinality of a nested disjoint indexed union. (Contributed by AV, 9-Jan-2022.) |
โข (๐ โ ๐ด โ Fin) & โข ๐ต = (๐ด โ {๐ฅ}) & โข ((๐ โง ๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โ ๐ถ โ Fin) & โข (๐ โ Disj ๐ฅ โ ๐ด โช ๐ฆ โ ๐ต ๐ถ) & โข ((๐ โง ๐ฅ โ ๐ด) โ Disj ๐ฆ โ ๐ต ๐ถ) & โข ((๐ โง ๐ฅ โ ๐ด โง ๐ฆ โ ๐ต) โ (โฏโ๐ถ) = 1) โ โข (๐ โ (โฏโโช ๐ฅ โ ๐ด โช ๐ฆ โ ๐ต ๐ถ) = ((โฏโ๐ด) ยท ((โฏโ๐ด) โ 1))) | ||
Theorem | hashrabrex 15711* | 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 15712* | The cardinality of a disjoint union. (Contributed by Mario Carneiro, 24-Jan-2015.) |
โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ด โ Fin) & โข (๐ โ Disj ๐ฅ โ ๐ด ๐ฅ) โ โข (๐ โ (โฏโโช ๐ด) = ฮฃ๐ฅ โ ๐ด (โฏโ๐ฅ)) | ||
Theorem | qshash 15713* | 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 15714* | Translate the Ackermann bijection ackbij1 10175 onto the positive integers. (Contributed by Mario Carneiro, 16-Jan-2015.) |
โข ๐น = (๐ฅ โ (๐ซ โ0 โฉ Fin) โฆ ฮฃ๐ฆ โ ๐ฅ (2โ๐ฆ)) โ โข ๐น:(๐ซ โ0 โฉ Fin)โ1-1-ontoโโ0 | ||
Theorem | binomlem 15715* | Lemma for binom 15716 (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 15716* | 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 15715. 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 15717* | Special case of the binomial theorem for (1 + ๐ด)โ๐. (Contributed by Paul Chapman, 10-May-2007.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ ((1 + ๐ด)โ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท (๐ดโ๐))) | ||
Theorem | binom11 15718* | Special case of the binomial theorem for 2โ๐. (Contributed by Mario Carneiro, 13-Mar-2014.) |
โข (๐ โ โ0 โ (2โ๐) = ฮฃ๐ โ (0...๐)(๐C๐)) | ||
Theorem | binom1dif 15719* | 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 15720 | Lemma for bcxmas 15721. (Contributed by Paul Chapman, 18-May-2007.) |
โข (๐ด = ๐ต โ ((๐ + ๐ด)C๐ด) = ((๐ + ๐ต)C๐ต)) | ||
Theorem | bcxmas 15721* | 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 15722* | Lemma for incexc 15723. (Contributed by Mario Carneiro, 7-Aug-2017.) |
โข ((๐ด โ Fin โง ๐ต โ Fin) โ ((โฏโ๐ต) โ (โฏโ(๐ต โฉ โช ๐ด))) = ฮฃ๐ โ ๐ซ ๐ด((-1โ(โฏโ๐ )) ยท (โฏโ(๐ต โฉ โฉ ๐ )))) | ||
Theorem | incexc 15723* | 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 15724* | 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 15725* | Index shift of an infinite sum. (Contributed by Paul Chapman, 31-Oct-2007.) (Revised by Mario Carneiro, 24-Apr-2014.) |
โข ๐ = (โคโฅโ๐) & โข ๐ = (โคโฅโ(๐ + ๐พ)) & โข (๐ = (๐พ + ๐) โ ๐ด = ๐ต) & โข (๐ โ ๐พ โ โค) & โข (๐ โ ๐ โ โค) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) โ โข (๐ โ ฮฃ๐ โ ๐ ๐ด = ฮฃ๐ โ ๐ ๐ต) | ||
Theorem | isumsplit 15726* | 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 15727* | 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 15728* | 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 15729* | 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 15730* | 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 15731* | 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 15732* | 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 15733* | 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 15734* | 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 15735* | Lemma for climcnds 15737: 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 15736* | Lemma for climcnds 15737: 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 15737* | 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 15738* | The sequence of reciprocals of real numbers, multiplied by the factor ๐ด, converges to zero. (Contributed by Mario Carneiro, 18-Sep-2014.) |
โข (๐ด โ โ โ (๐ โ โ+ โฆ (๐ด / ๐)) โ๐ 0) | ||
Theorem | divcnv 15739* | The sequence of reciprocals of positive integers, multiplied by the factor ๐ด, converges to zero. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 18-Sep-2014.) |
โข (๐ด โ โ โ (๐ โ โ โฆ (๐ด / ๐)) โ 0) | ||
Theorem | flo1 15740 | The floor function satisfies โ(๐ฅ) = ๐ฅ + ๐(1). (Contributed by Mario Carneiro, 21-May-2016.) |
โข (๐ฅ โ โ โฆ (๐ฅ โ (โโ๐ฅ))) โ ๐(1) | ||
Theorem | divcnvshft 15741* | Limit of a ratio function. (Contributed by Scott Fenton, 16-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โค) & โข (๐ โ ๐น โ ๐) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = (๐ด / (๐ + ๐ต))) โ โข (๐ โ ๐น โ 0) | ||
Theorem | supcvg 15742* | Extract a sequence ๐ in ๐ such that the image of the points in the bounded set ๐ด converges to the supremum ๐ of the set. Similar to Equation 4 of [Kreyszig] p. 144. The proof uses countable choice ax-cc 10372. (Contributed by Mario Carneiro, 15-Feb-2013.) (Proof shortened by Mario Carneiro, 26-Apr-2014.) |
โข ๐ โ V & โข ๐ = sup(๐ด, โ, < ) & โข ๐ = (๐ โ โ โฆ (๐ โ (1 / ๐))) & โข (๐ โ ๐ โ โ ) & โข (๐ โ ๐น:๐โontoโ๐ด) & โข (๐ โ ๐ด โ โ) & โข (๐ โ โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โ โข (๐ โ โ๐(๐:โโถ๐ โง (๐น โ ๐) โ ๐)) | ||
Theorem | infcvgaux1i 15743* | Auxiliary theorem for applications of supcvg 15742. Hypothesis for several supremum theorems. (Contributed by NM, 8-Feb-2008.) |
โข ๐ = {๐ฅ โฃ โ๐ฆ โ ๐ ๐ฅ = -๐ด} & โข (๐ฆ โ ๐ โ ๐ด โ โ) & โข ๐ โ ๐ & โข โ๐ง โ โ โ๐ค โ ๐ ๐ค โค ๐ง โ โข (๐ โ โ โง ๐ โ โ โง โ๐ง โ โ โ๐ค โ ๐ ๐ค โค ๐ง) | ||
Theorem | infcvgaux2i 15744* | Auxiliary theorem for applications of supcvg 15742. (Contributed by NM, 4-Mar-2008.) |
โข ๐ = {๐ฅ โฃ โ๐ฆ โ ๐ ๐ฅ = -๐ด} & โข (๐ฆ โ ๐ โ ๐ด โ โ) & โข ๐ โ ๐ & โข โ๐ง โ โ โ๐ค โ ๐ ๐ค โค ๐ง & โข ๐ = -sup(๐ , โ, < ) & โข (๐ฆ = ๐ถ โ ๐ด = ๐ต) โ โข (๐ถ โ ๐ โ ๐ โค ๐ต) | ||
Theorem | harmonic 15745 | The harmonic series ๐ป diverges. This fact follows from the stronger emcl 26355, which establishes that the harmonic series grows as log๐ + ฮณ + o(1), but this uses a more elementary method, attributed to Nicole Oresme (1323-1382). This is Metamath 100 proof #34. (Contributed by Mario Carneiro, 11-Jul-2014.) |
โข ๐น = (๐ โ โ โฆ (1 / ๐)) & โข ๐ป = seq1( + , ๐น) โ โข ยฌ ๐ป โ dom โ | ||
Theorem | arisum 15746* | Arithmetic series sum of the first ๐ positive integers. This is Metamath 100 proof #68. (Contributed by FL, 16-Nov-2006.) (Proof shortened by Mario Carneiro, 22-May-2014.) |
โข (๐ โ โ0 โ ฮฃ๐ โ (1...๐)๐ = (((๐โ2) + ๐) / 2)) | ||
Theorem | arisum2 15747* | Arithmetic series sum of the first ๐ nonnegative integers. (Contributed by Mario Carneiro, 17-Apr-2015.) (Proof shortened by AV, 2-Aug-2021.) |
โข (๐ โ โ0 โ ฮฃ๐ โ (0...(๐ โ 1))๐ = (((๐โ2) โ ๐) / 2)) | ||
Theorem | trireciplem 15748 | Lemma for trirecip 15749. Show that the sum converges. (Contributed by Scott Fenton, 22-Apr-2014.) (Revised by Mario Carneiro, 22-May-2014.) |
โข ๐น = (๐ โ โ โฆ (1 / (๐ ยท (๐ + 1)))) โ โข seq1( + , ๐น) โ 1 | ||
Theorem | trirecip 15749 | The sum of the reciprocals of the triangle numbers converge to two. This is Metamath 100 proof #42. (Contributed by Scott Fenton, 23-Apr-2014.) (Revised by Mario Carneiro, 22-May-2014.) |
โข ฮฃ๐ โ โ (2 / (๐ ยท (๐ + 1))) = 2 | ||
Theorem | expcnv 15750* | A sequence of powers of a complex number ๐ด with absolute value smaller than 1 converges to zero. (Contributed by NM, 8-May-2006.) (Proof shortened by Mario Carneiro, 26-Apr-2014.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ (absโ๐ด) < 1) โ โข (๐ โ (๐ โ โ0 โฆ (๐ดโ๐)) โ 0) | ||
Theorem | explecnv 15751* | A sequence of terms converges to zero when it is less than powers of a number ๐ด whose absolute value is smaller than 1. (Contributed by NM, 19-Jul-2008.) (Revised by Mario Carneiro, 26-Apr-2014.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐น โ ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ด โ โ) & โข (๐ โ (absโ๐ด) < 1) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) โ โ) & โข ((๐ โง ๐ โ ๐) โ (absโ(๐นโ๐)) โค (๐ดโ๐)) โ โข (๐ โ ๐น โ 0) | ||
Theorem | geoserg 15752* | The value of the finite geometric series ๐ดโ๐ + ๐ดโ(๐ + 1) +... + ๐ดโ(๐ โ 1). (Contributed by Mario Carneiro, 2-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 1) & โข (๐ โ ๐ โ โ0) & โข (๐ โ ๐ โ (โคโฅโ๐)) โ โข (๐ โ ฮฃ๐ โ (๐..^๐)(๐ดโ๐) = (((๐ดโ๐) โ (๐ดโ๐)) / (1 โ ๐ด))) | ||
Theorem | geoser 15753* | The value of the finite geometric series 1 + ๐ดโ1 + ๐ดโ2 +... + ๐ดโ(๐ โ 1). This is Metamath 100 proof #66. (Contributed by NM, 12-May-2006.) (Proof shortened by Mario Carneiro, 15-Jun-2014.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 1) & โข (๐ โ ๐ โ โ0) โ โข (๐ โ ฮฃ๐ โ (0...(๐ โ 1))(๐ดโ๐) = ((1 โ (๐ดโ๐)) / (1 โ ๐ด))) | ||
Theorem | pwdif 15754* | The difference of two numbers to the same power is the difference of the two numbers multiplied with a finite sum. Generalization of subsq 14115. See Wikipedia "Fermat number", section "Other theorems about Fermat numbers", https://en.wikipedia.org/wiki/Fermat_number 14115, 5-Aug-2021. (Contributed by AV, 6-Aug-2021.) (Revised by AV, 19-Aug-2021.) |
โข ((๐ โ โ0 โง ๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ๐) โ (๐ตโ๐)) = ((๐ด โ ๐ต) ยท ฮฃ๐ โ (0..^๐)((๐ดโ๐) ยท (๐ตโ((๐ โ ๐) โ 1))))) | ||
Theorem | pwm1geoser 15755* | The n-th power of a number decreased by 1 expressed by the finite geometric series 1 + ๐ดโ1 + ๐ดโ2 +... + ๐ดโ(๐ โ 1). (Contributed by AV, 14-Aug-2021.) (Proof shortened by AV, 19-Aug-2021.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ โ โ0) โ โข (๐ โ ((๐ดโ๐) โ 1) = ((๐ด โ 1) ยท ฮฃ๐ โ (0...(๐ โ 1))(๐ดโ๐))) | ||
Theorem | geolim 15756* | The partial sums in the infinite series 1 + ๐ดโ1 + ๐ดโ2... converge to (1 / (1 โ ๐ด)). (Contributed by NM, 15-May-2006.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ (absโ๐ด) < 1) & โข ((๐ โง ๐ โ โ0) โ (๐นโ๐) = (๐ดโ๐)) โ โข (๐ โ seq0( + , ๐น) โ (1 / (1 โ ๐ด))) | ||
Theorem | geolim2 15757* | The partial sums in the geometric series ๐ดโ๐ + ๐ดโ(๐ + 1)... converge to ((๐ดโ๐) / (1 โ ๐ด)). (Contributed by NM, 6-Jun-2006.) (Revised by Mario Carneiro, 26-Apr-2014.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ (absโ๐ด) < 1) & โข (๐ โ ๐ โ โ0) & โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (๐นโ๐) = (๐ดโ๐)) โ โข (๐ โ seq๐( + , ๐น) โ ((๐ดโ๐) / (1 โ ๐ด))) | ||
Theorem | georeclim 15758* | The limit of a geometric series of reciprocals. (Contributed by Paul Chapman, 28-Dec-2007.) (Revised by Mario Carneiro, 26-Apr-2014.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ 1 < (absโ๐ด)) & โข ((๐ โง ๐ โ โ0) โ (๐นโ๐) = ((1 / ๐ด)โ๐)) โ โข (๐ โ seq0( + , ๐น) โ (๐ด / (๐ด โ 1))) | ||
Theorem | geo2sum 15759* | The value of the finite geometric series 2โ-1 + 2โ-2 +... + 2โ-๐, multiplied by a constant. (Contributed by Mario Carneiro, 17-Mar-2014.) (Revised by Mario Carneiro, 26-Apr-2014.) |
โข ((๐ โ โ โง ๐ด โ โ) โ ฮฃ๐ โ (1...๐)(๐ด / (2โ๐)) = (๐ด โ (๐ด / (2โ๐)))) | ||
Theorem | geo2sum2 15760* | The value of the finite geometric series 1 + 2 + 4 + 8 +... + 2โ(๐ โ 1). (Contributed by Mario Carneiro, 7-Sep-2016.) |
โข (๐ โ โ0 โ ฮฃ๐ โ (0..^๐)(2โ๐) = ((2โ๐) โ 1)) | ||
Theorem | geo2lim 15761* | The value of the infinite geometric series 2โ-1 + 2โ-2 +... , multiplied by a constant. (Contributed by Mario Carneiro, 15-Jun-2014.) |
โข ๐น = (๐ โ โ โฆ (๐ด / (2โ๐))) โ โข (๐ด โ โ โ seq1( + , ๐น) โ ๐ด) | ||
Theorem | geomulcvg 15762* | The geometric series converges even if it is multiplied by ๐ to result in the larger series ๐ ยท ๐ดโ๐. (Contributed by Mario Carneiro, 27-Mar-2015.) |
โข ๐น = (๐ โ โ0 โฆ (๐ ยท (๐ดโ๐))) โ โข ((๐ด โ โ โง (absโ๐ด) < 1) โ seq0( + , ๐น) โ dom โ ) | ||
Theorem | geoisum 15763* | The infinite sum of 1 + ๐ดโ1 + ๐ดโ2... is (1 / (1 โ ๐ด)). (Contributed by NM, 15-May-2006.) (Revised by Mario Carneiro, 26-Apr-2014.) |
โข ((๐ด โ โ โง (absโ๐ด) < 1) โ ฮฃ๐ โ โ0 (๐ดโ๐) = (1 / (1 โ ๐ด))) | ||
Theorem | geoisumr 15764* | The infinite sum of reciprocals 1 + (1 / ๐ด)โ1 + (1 / ๐ด)โ2... is ๐ด / (๐ด โ 1). (Contributed by rpenner, 3-Nov-2007.) (Revised by Mario Carneiro, 26-Apr-2014.) |
โข ((๐ด โ โ โง 1 < (absโ๐ด)) โ ฮฃ๐ โ โ0 ((1 / ๐ด)โ๐) = (๐ด / (๐ด โ 1))) | ||
Theorem | geoisum1 15765* | The infinite sum of ๐ดโ1 + ๐ดโ2... is (๐ด / (1 โ ๐ด)). (Contributed by NM, 1-Nov-2007.) (Revised by Mario Carneiro, 26-Apr-2014.) |
โข ((๐ด โ โ โง (absโ๐ด) < 1) โ ฮฃ๐ โ โ (๐ดโ๐) = (๐ด / (1 โ ๐ด))) | ||
Theorem | geoisum1c 15766* | The infinite sum of ๐ด ยท (๐ โ1) + ๐ด ยท (๐ โ2)... is (๐ด ยท ๐ ) / (1 โ ๐ ). (Contributed by NM, 2-Nov-2007.) (Revised by Mario Carneiro, 26-Apr-2014.) |
โข ((๐ด โ โ โง ๐ โ โ โง (absโ๐ ) < 1) โ ฮฃ๐ โ โ (๐ด ยท (๐ โ๐)) = ((๐ด ยท ๐ ) / (1 โ ๐ ))) | ||
Theorem | 0.999... 15767 | The recurring decimal 0.999..., which is defined as the infinite sum 0.9 + 0.09 + 0.009 + ... i.e. 9 / 10โ1 + 9 / 10โ2 + 9 / 10โ3 + ..., is exactly equal to 1, according to ZF set theory. Interestingly, about 40% of the people responding to a poll at http://forum.physorg.com/index.php?showtopic=13177 disagree. (Contributed by NM, 2-Nov-2007.) (Revised by AV, 8-Sep-2021.) |
โข ฮฃ๐ โ โ (9 / (;10โ๐)) = 1 | ||
Theorem | geoihalfsum 15768 | Prove that the infinite geometric series of 1/2, 1/2 + 1/4 + 1/8 + ... = 1. Uses geoisum1 15765. This is a representation of .111... in binary with an infinite number of 1's. Theorem 0.999... 15767 proves a similar claim for .999... in base 10. (Contributed by David A. Wheeler, 4-Jan-2017.) (Proof shortened by AV, 9-Jul-2022.) |
โข ฮฃ๐ โ โ (1 / (2โ๐)) = 1 | ||
Theorem | cvgrat 15769* | Ratio test for convergence of a complex infinite series. If the ratio ๐ด of the absolute values of successive terms in an infinite sequence ๐น is less than 1 for all terms beyond some index ๐ต, then the infinite sum of the terms of ๐น converges to a complex number. Equivalent to first part of Exercise 4 of [Gleason] p. 182. (Contributed by NM, 26-Apr-2005.) (Proof shortened by Mario Carneiro, 27-Apr-2014.) |
โข ๐ = (โคโฅโ๐) & โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด < 1) & โข (๐ โ ๐ โ ๐) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) โ โ) & โข ((๐ โง ๐ โ ๐) โ (absโ(๐นโ(๐ + 1))) โค (๐ด ยท (absโ(๐นโ๐)))) โ โข (๐ โ seq๐( + , ๐น) โ dom โ ) | ||
Theorem | mertenslem1 15770* | Lemma for mertens 15772. (Contributed by Mario Carneiro, 29-Apr-2014.) |
โข ((๐ โง ๐ โ โ0) โ (๐นโ๐) = ๐ด) & โข ((๐ โง ๐ โ โ0) โ (๐พโ๐) = (absโ๐ด)) & โข ((๐ โง ๐ โ โ0) โ ๐ด โ โ) & โข ((๐ โง ๐ โ โ0) โ (๐บโ๐) = ๐ต) & โข ((๐ โง ๐ โ โ0) โ ๐ต โ โ) & โข ((๐ โง ๐ โ โ0) โ (๐ปโ๐) = ฮฃ๐ โ (0...๐)(๐ด ยท (๐บโ(๐ โ ๐)))) & โข (๐ โ seq0( + , ๐พ) โ dom โ ) & โข (๐ โ seq0( + , ๐บ) โ dom โ ) & โข (๐ โ ๐ธ โ โ+) & โข ๐ = {๐ง โฃ โ๐ โ (0...(๐ โ 1))๐ง = (absโฮฃ๐ โ (โคโฅโ(๐ + 1))(๐บโ๐))} & โข (๐ โ (๐ โ โ โง โ๐ โ (โคโฅโ๐ )(absโฮฃ๐ โ (โคโฅโ(๐ + 1))(๐บโ๐)) < ((๐ธ / 2) / (ฮฃ๐ โ โ0 (๐พโ๐) + 1)))) & โข (๐ โ (๐ โง (๐ก โ โ0 โง โ๐ โ (โคโฅโ๐ก)(๐พโ๐) < (((๐ธ / 2) / ๐ ) / (sup(๐, โ, < ) + 1))))) & โข (๐ โ (0 โค sup(๐, โ, < ) โง (๐ โ โ โง ๐ โ โ โง โ๐ง โ โ โ๐ค โ ๐ ๐ค โค ๐ง))) โ โข (๐ โ โ๐ฆ โ โ0 โ๐ โ (โคโฅโ๐ฆ)(absโฮฃ๐ โ (0...๐)(๐ด ยท ฮฃ๐ โ (โคโฅโ((๐ โ ๐) + 1))๐ต)) < ๐ธ) | ||
Theorem | mertenslem2 15771* | Lemma for mertens 15772. (Contributed by Mario Carneiro, 28-Apr-2014.) |
โข ((๐ โง ๐ โ โ0) โ (๐นโ๐) = ๐ด) & โข ((๐ โง ๐ โ โ0) โ (๐พโ๐) = (absโ๐ด)) & โข ((๐ โง ๐ โ โ0) โ ๐ด โ โ) & โข ((๐ โง ๐ โ โ0) โ (๐บโ๐) = ๐ต) & โข ((๐ โง ๐ โ โ0) โ ๐ต โ โ) & โข ((๐ โง ๐ โ โ0) โ (๐ปโ๐) = ฮฃ๐ โ (0...๐)(๐ด ยท (๐บโ(๐ โ ๐)))) & โข (๐ โ seq0( + , ๐พ) โ dom โ ) & โข (๐ โ seq0( + , ๐บ) โ dom โ ) & โข (๐ โ ๐ธ โ โ+) & โข ๐ = {๐ง โฃ โ๐ โ (0...(๐ โ 1))๐ง = (absโฮฃ๐ โ (โคโฅโ(๐ + 1))(๐บโ๐))} & โข (๐ โ (๐ โ โ โง โ๐ โ (โคโฅโ๐ )(absโฮฃ๐ โ (โคโฅโ(๐ + 1))(๐บโ๐)) < ((๐ธ / 2) / (ฮฃ๐ โ โ0 (๐พโ๐) + 1)))) โ โข (๐ โ โ๐ฆ โ โ0 โ๐ โ (โคโฅโ๐ฆ)(absโฮฃ๐ โ (0...๐)(๐ด ยท ฮฃ๐ โ (โคโฅโ((๐ โ ๐) + 1))๐ต)) < ๐ธ) | ||
Theorem | mertens 15772* | Mertens' theorem. If ๐ด(๐) is an absolutely convergent series and ๐ต(๐) is convergent, then (ฮฃ๐ โ โ0๐ด(๐) ยท ฮฃ๐ โ โ0๐ต(๐)) = ฮฃ๐ โ โ0ฮฃ๐ โ (0...๐)(๐ด(๐) ยท ๐ต(๐ โ ๐)) (and this latter series is convergent). This latter sum is commonly known as the Cauchy product of the sequences. The proof follows the outline at http://en.wikipedia.org/wiki/Cauchy_product#Proof_of_Mertens.27_theorem. (Contributed by Mario Carneiro, 29-Apr-2014.) |
โข ((๐ โง ๐ โ โ0) โ (๐นโ๐) = ๐ด) & โข ((๐ โง ๐ โ โ0) โ (๐พโ๐) = (absโ๐ด)) & โข ((๐ โง ๐ โ โ0) โ ๐ด โ โ) & โข ((๐ โง ๐ โ โ0) โ (๐บโ๐) = ๐ต) & โข ((๐ โง ๐ โ โ0) โ ๐ต โ โ) & โข ((๐ โง ๐ โ โ0) โ (๐ปโ๐) = ฮฃ๐ โ (0...๐)(๐ด ยท (๐บโ(๐ โ ๐)))) & โข (๐ โ seq0( + , ๐พ) โ dom โ ) & โข (๐ โ seq0( + , ๐บ) โ dom โ ) โ โข (๐ โ seq0( + , ๐ป) โ (ฮฃ๐ โ โ0 ๐ด ยท ฮฃ๐ โ โ0 ๐ต)) | ||
Theorem | prodf 15773* | An infinite product of complex terms is a function from an upper set of integers to โ. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) โ โ) โ โข (๐ โ seq๐( ยท , ๐น):๐โถโ) | ||
Theorem | clim2prod 15774* | The limit of an infinite product with an initial segment added. (Contributed by Scott Fenton, 18-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ ๐) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) โ โ) & โข (๐ โ seq(๐ + 1)( ยท , ๐น) โ ๐ด) โ โข (๐ โ seq๐( ยท , ๐น) โ ((seq๐( ยท , ๐น)โ๐) ยท ๐ด)) | ||
Theorem | clim2div 15775* | The limit of an infinite product with an initial segment removed. (Contributed by Scott Fenton, 20-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ ๐) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) โ โ) & โข (๐ โ seq๐( ยท , ๐น) โ ๐ด) & โข (๐ โ (seq๐( ยท , ๐น)โ๐) โ 0) โ โข (๐ โ seq(๐ + 1)( ยท , ๐น) โ (๐ด / (seq๐( ยท , ๐น)โ๐))) | ||
Theorem | prodfmul 15776* | The product of two infinite products. (Contributed by Scott Fenton, 18-Dec-2017.) |
โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐นโ๐) โ โ) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐บโ๐) โ โ) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐ปโ๐) = ((๐นโ๐) ยท (๐บโ๐))) โ โข (๐ โ (seq๐( ยท , ๐ป)โ๐) = ((seq๐( ยท , ๐น)โ๐) ยท (seq๐( ยท , ๐บ)โ๐))) | ||
Theorem | prodf1 15777 | The value of the partial products in a one-valued infinite product. (Contributed by Scott Fenton, 5-Dec-2017.) |
โข ๐ = (โคโฅโ๐) โ โข (๐ โ ๐ โ (seq๐( ยท , (๐ ร {1}))โ๐) = 1) | ||
Theorem | prodf1f 15778 | A one-valued infinite product is equal to the constant one function. (Contributed by Scott Fenton, 5-Dec-2017.) |
โข ๐ = (โคโฅโ๐) โ โข (๐ โ โค โ seq๐( ยท , (๐ ร {1})) = (๐ ร {1})) | ||
Theorem | prodfclim1 15779 | The constant one product converges to one. (Contributed by Scott Fenton, 5-Dec-2017.) |
โข ๐ = (โคโฅโ๐) โ โข (๐ โ โค โ seq๐( ยท , (๐ ร {1})) โ 1) | ||
Theorem | prodfn0 15780* | No term of a nonzero infinite product is zero. (Contributed by Scott Fenton, 14-Jan-2018.) |
โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐นโ๐) โ โ) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐นโ๐) โ 0) โ โข (๐ โ (seq๐( ยท , ๐น)โ๐) โ 0) | ||
Theorem | prodfrec 15781* | The reciprocal of an infinite product. (Contributed by Scott Fenton, 15-Jan-2018.) |
โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐นโ๐) โ โ) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐นโ๐) โ 0) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐บโ๐) = (1 / (๐นโ๐))) โ โข (๐ โ (seq๐( ยท , ๐บ)โ๐) = (1 / (seq๐( ยท , ๐น)โ๐))) | ||
Theorem | prodfdiv 15782* | The quotient of two infinite products. (Contributed by Scott Fenton, 15-Jan-2018.) |
โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐นโ๐) โ โ) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐บโ๐) โ โ) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐บโ๐) โ 0) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐ปโ๐) = ((๐นโ๐) / (๐บโ๐))) โ โข (๐ โ (seq๐( ยท , ๐ป)โ๐) = ((seq๐( ยท , ๐น)โ๐) / (seq๐( ยท , ๐บ)โ๐))) | ||
Theorem | ntrivcvg 15783* | A non-trivially converging infinite product converges. (Contributed by Scott Fenton, 18-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ โ๐ โ ๐ โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ)) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) โ โ) โ โข (๐ โ seq๐( ยท , ๐น) โ dom โ ) | ||
Theorem | ntrivcvgn0 15784* | A product that converges to a nonzero value converges non-trivially. (Contributed by Scott Fenton, 18-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ seq๐( ยท , ๐น) โ ๐) & โข (๐ โ ๐ โ 0) โ โข (๐ โ โ๐ โ ๐ โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ)) | ||
Theorem | ntrivcvgfvn0 15785* | Any value of a product sequence that converges to a nonzero value is itself nonzero. (Contributed by Scott Fenton, 20-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ ๐) & โข (๐ โ seq๐( ยท , ๐น) โ ๐) & โข (๐ โ ๐ โ 0) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) โ โ) โ โข (๐ โ (seq๐( ยท , ๐น)โ๐) โ 0) | ||
Theorem | ntrivcvgtail 15786* | A tail of a non-trivially convergent sequence converges non-trivially. (Contributed by Scott Fenton, 20-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ ๐) & โข (๐ โ seq๐( ยท , ๐น) โ ๐) & โข (๐ โ ๐ โ 0) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) โ โ) โ โข (๐ โ (( โ โseq๐( ยท , ๐น)) โ 0 โง seq๐( ยท , ๐น) โ ( โ โseq๐( ยท , ๐น)))) | ||
Theorem | ntrivcvgmullem 15787* | Lemma for ntrivcvgmul 15788. (Contributed by Scott Fenton, 19-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ โ 0) & โข (๐ โ ๐ โ 0) & โข (๐ โ seq๐( ยท , ๐น) โ ๐) & โข (๐ โ seq๐( ยท , ๐บ) โ ๐) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) โ โ) & โข ((๐ โง ๐ โ ๐) โ (๐บโ๐) โ โ) & โข (๐ โ ๐ โค ๐) & โข ((๐ โง ๐ โ ๐) โ (๐ปโ๐) = ((๐นโ๐) ยท (๐บโ๐))) โ โข (๐ โ โ๐ โ ๐ โ๐ค(๐ค โ 0 โง seq๐( ยท , ๐ป) โ ๐ค)) | ||
Theorem | ntrivcvgmul 15788* | The product of two non-trivially converging products converges non-trivially. (Contributed by Scott Fenton, 18-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ โ๐ โ ๐ โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ)) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) โ โ) & โข (๐ โ โ๐ โ ๐ โ๐ง(๐ง โ 0 โง seq๐( ยท , ๐บ) โ ๐ง)) & โข ((๐ โง ๐ โ ๐) โ (๐บโ๐) โ โ) & โข ((๐ โง ๐ โ ๐) โ (๐ปโ๐) = ((๐นโ๐) ยท (๐บโ๐))) โ โข (๐ โ โ๐ โ ๐ โ๐ค(๐ค โ 0 โง seq๐( ยท , ๐ป) โ ๐ค)) | ||
Syntax | cprod 15789 | Extend class notation to include complex products. |
class โ๐ โ ๐ด ๐ต | ||
Definition | df-prod 15790* | Define the product of a series with an index set of integers ๐ด. This definition takes most of the aspects of df-sum 15572 and adapts them for multiplication instead of addition. However, we insist that in the infinite case, there is a nonzero tail of the sequence. This ensures that the convergence criteria match those of infinite sums. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข โ๐ โ ๐ด ๐ต = (โฉ๐ฅ(โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ (โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ) โง seq๐( ยท , (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต))โ๐)))) | ||
Theorem | prodex 15791 | A product is a set. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข โ๐ โ ๐ด ๐ต โ V | ||
Theorem | prodeq1f 15792 | Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017.) |
โข โฒ๐๐ด & โข โฒ๐๐ต โ โข (๐ด = ๐ต โ โ๐ โ ๐ด ๐ถ = โ๐ โ ๐ต ๐ถ) | ||
Theorem | prodeq1 15793* | Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017.) |
โข (๐ด = ๐ต โ โ๐ โ ๐ด ๐ถ = โ๐ โ ๐ต ๐ถ) | ||
Theorem | nfcprod1 15794* | Bound-variable hypothesis builder for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข โฒ๐๐ด โ โข โฒ๐โ๐ โ ๐ด ๐ต | ||
Theorem | nfcprod 15795* | Bound-variable hypothesis builder for product: if ๐ฅ is (effectively) not free in ๐ด and ๐ต, it is not free in โ๐ โ ๐ด๐ต. (Contributed by Scott Fenton, 1-Dec-2017.) |
โข โฒ๐ฅ๐ด & โข โฒ๐ฅ๐ต โ โข โฒ๐ฅโ๐ โ ๐ด ๐ต | ||
Theorem | prodeq2w 15796* | Equality theorem for product, when the class expressions ๐ต and ๐ถ are equal everywhere. Proved using only Extensionality. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข (โ๐ ๐ต = ๐ถ โ โ๐ โ ๐ด ๐ต = โ๐ โ ๐ด ๐ถ) | ||
Theorem | prodeq2ii 15797* | Equality theorem for product, with the class expressions ๐ต and ๐ถ guarded by I to be always sets. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข (โ๐ โ ๐ด ( I โ๐ต) = ( I โ๐ถ) โ โ๐ โ ๐ด ๐ต = โ๐ โ ๐ด ๐ถ) | ||
Theorem | prodeq2 15798* | Equality theorem for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข (โ๐ โ ๐ด ๐ต = ๐ถ โ โ๐ โ ๐ด ๐ต = โ๐ โ ๐ด ๐ถ) | ||
Theorem | cbvprod 15799* | Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข (๐ = ๐ โ ๐ต = ๐ถ) & โข โฒ๐๐ด & โข โฒ๐๐ด & โข โฒ๐๐ต & โข โฒ๐๐ถ โ โข โ๐ โ ๐ด ๐ต = โ๐ โ ๐ด ๐ถ | ||
Theorem | cbvprodv 15800* | Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข (๐ = ๐ โ ๐ต = ๐ถ) โ โข โ๐ โ ๐ด ๐ต = โ๐ โ ๐ด ๐ถ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |