![]() |
Metamath
Proof Explorer Theorem List (p. 159 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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | climcndslem2 15801* | Lemma for climcnds 15802: 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 15802* | 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 15803* | The sequence of reciprocals of real numbers, multiplied by the factor ๐ด, converges to zero. (Contributed by Mario Carneiro, 18-Sep-2014.) |
โข (๐ด โ โ โ (๐ โ โ+ โฆ (๐ด / ๐)) โ๐ 0) | ||
Theorem | divcnv 15804* | 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 15805 | The floor function satisfies โ(๐ฅ) = ๐ฅ + ๐(1). (Contributed by Mario Carneiro, 21-May-2016.) |
โข (๐ฅ โ โ โฆ (๐ฅ โ (โโ๐ฅ))) โ ๐(1) | ||
Theorem | divcnvshft 15806* | Limit of a ratio function. (Contributed by Scott Fenton, 16-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โค) & โข (๐ โ ๐น โ ๐) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = (๐ด / (๐ + ๐ต))) โ โข (๐ โ ๐น โ 0) | ||
Theorem | supcvg 15807* | 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 10433. (Contributed by Mario Carneiro, 15-Feb-2013.) (Proof shortened by Mario Carneiro, 26-Apr-2014.) |
โข ๐ โ V & โข ๐ = sup(๐ด, โ, < ) & โข ๐ = (๐ โ โ โฆ (๐ โ (1 / ๐))) & โข (๐ โ ๐ โ โ ) & โข (๐ โ ๐น:๐โontoโ๐ด) & โข (๐ โ ๐ด โ โ) & โข (๐ โ โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โ โข (๐ โ โ๐(๐:โโถ๐ โง (๐น โ ๐) โ ๐)) | ||
Theorem | infcvgaux1i 15808* | Auxiliary theorem for applications of supcvg 15807. Hypothesis for several supremum theorems. (Contributed by NM, 8-Feb-2008.) |
โข ๐ = {๐ฅ โฃ โ๐ฆ โ ๐ ๐ฅ = -๐ด} & โข (๐ฆ โ ๐ โ ๐ด โ โ) & โข ๐ โ ๐ & โข โ๐ง โ โ โ๐ค โ ๐ ๐ค โค ๐ง โ โข (๐ โ โ โง ๐ โ โ โง โ๐ง โ โ โ๐ค โ ๐ ๐ค โค ๐ง) | ||
Theorem | infcvgaux2i 15809* | Auxiliary theorem for applications of supcvg 15807. (Contributed by NM, 4-Mar-2008.) |
โข ๐ = {๐ฅ โฃ โ๐ฆ โ ๐ ๐ฅ = -๐ด} & โข (๐ฆ โ ๐ โ ๐ด โ โ) & โข ๐ โ ๐ & โข โ๐ง โ โ โ๐ค โ ๐ ๐ค โค ๐ง & โข ๐ = -sup(๐ , โ, < ) & โข (๐ฆ = ๐ถ โ ๐ด = ๐ต) โ โข (๐ถ โ ๐ โ ๐ โค ๐ต) | ||
Theorem | harmonic 15810 | The harmonic series ๐ป diverges. This fact follows from the stronger emcl 26740, 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 15811* | 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 15812* | 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 15813 | Lemma for trirecip 15814. 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 15814 | 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 15815* | 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 15816* | 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 15817* | The value of the finite geometric series ๐ดโ๐ + ๐ดโ(๐ + 1) +... + ๐ดโ(๐ โ 1). (Contributed by Mario Carneiro, 2-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 1) & โข (๐ โ ๐ โ โ0) & โข (๐ โ ๐ โ (โคโฅโ๐)) โ โข (๐ โ ฮฃ๐ โ (๐..^๐)(๐ดโ๐) = (((๐ดโ๐) โ (๐ดโ๐)) / (1 โ ๐ด))) | ||
Theorem | geoser 15818* | 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 15819* | The difference of two numbers to the same power is the difference of the two numbers multiplied with a finite sum. Generalization of subsq 14179. See Wikipedia "Fermat number", section "Other theorems about Fermat numbers", https://en.wikipedia.org/wiki/Fermat_number 14179, 5-Aug-2021. (Contributed by AV, 6-Aug-2021.) (Revised by AV, 19-Aug-2021.) |
โข ((๐ โ โ0 โง ๐ด โ โ โง ๐ต โ โ) โ ((๐ดโ๐) โ (๐ตโ๐)) = ((๐ด โ ๐ต) ยท ฮฃ๐ โ (0..^๐)((๐ดโ๐) ยท (๐ตโ((๐ โ ๐) โ 1))))) | ||
Theorem | pwm1geoser 15820* | 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 15821* | 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 15822* | 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 15823* | 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 15824* | 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 15825* | 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 15826* | 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 15827* | 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 15828* | 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 15829* | 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 15830* | 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 15831* | 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... 15832 | 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 15833 | Prove that the infinite geometric series of 1/2, 1/2 + 1/4 + 1/8 + ... = 1. Uses geoisum1 15830. This is a representation of .111... in binary with an infinite number of 1's. Theorem 0.999... 15832 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 15834* | 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 15835* | Lemma for mertens 15837. (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 15836* | Lemma for mertens 15837. (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 15837* | 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 15838* | 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 15839* | The limit of an infinite product with an initial segment added. (Contributed by Scott Fenton, 18-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ ๐) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) โ โ) & โข (๐ โ seq(๐ + 1)( ยท , ๐น) โ ๐ด) โ โข (๐ โ seq๐( ยท , ๐น) โ ((seq๐( ยท , ๐น)โ๐) ยท ๐ด)) | ||
Theorem | clim2div 15840* | 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 15841* | The product of two infinite products. (Contributed by Scott Fenton, 18-Dec-2017.) |
โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐นโ๐) โ โ) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐บโ๐) โ โ) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐ปโ๐) = ((๐นโ๐) ยท (๐บโ๐))) โ โข (๐ โ (seq๐( ยท , ๐ป)โ๐) = ((seq๐( ยท , ๐น)โ๐) ยท (seq๐( ยท , ๐บ)โ๐))) | ||
Theorem | prodf1 15842 | The value of the partial products in a one-valued infinite product. (Contributed by Scott Fenton, 5-Dec-2017.) |
โข ๐ = (โคโฅโ๐) โ โข (๐ โ ๐ โ (seq๐( ยท , (๐ ร {1}))โ๐) = 1) | ||
Theorem | prodf1f 15843 | A one-valued infinite product is equal to the constant one function. (Contributed by Scott Fenton, 5-Dec-2017.) |
โข ๐ = (โคโฅโ๐) โ โข (๐ โ โค โ seq๐( ยท , (๐ ร {1})) = (๐ ร {1})) | ||
Theorem | prodfclim1 15844 | The constant one product converges to one. (Contributed by Scott Fenton, 5-Dec-2017.) |
โข ๐ = (โคโฅโ๐) โ โข (๐ โ โค โ seq๐( ยท , (๐ ร {1})) โ 1) | ||
Theorem | prodfn0 15845* | No term of a nonzero infinite product is zero. (Contributed by Scott Fenton, 14-Jan-2018.) |
โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐นโ๐) โ โ) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐นโ๐) โ 0) โ โข (๐ โ (seq๐( ยท , ๐น)โ๐) โ 0) | ||
Theorem | prodfrec 15846* | The reciprocal of an infinite product. (Contributed by Scott Fenton, 15-Jan-2018.) |
โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐นโ๐) โ โ) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐นโ๐) โ 0) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐บโ๐) = (1 / (๐นโ๐))) โ โข (๐ โ (seq๐( ยท , ๐บ)โ๐) = (1 / (seq๐( ยท , ๐น)โ๐))) | ||
Theorem | prodfdiv 15847* | The quotient of two infinite products. (Contributed by Scott Fenton, 15-Jan-2018.) |
โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐นโ๐) โ โ) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐บโ๐) โ โ) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐บโ๐) โ 0) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐ปโ๐) = ((๐นโ๐) / (๐บโ๐))) โ โข (๐ โ (seq๐( ยท , ๐ป)โ๐) = ((seq๐( ยท , ๐น)โ๐) / (seq๐( ยท , ๐บ)โ๐))) | ||
Theorem | ntrivcvg 15848* | A non-trivially converging infinite product converges. (Contributed by Scott Fenton, 18-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ โ๐ โ ๐ โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ)) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) โ โ) โ โข (๐ โ seq๐( ยท , ๐น) โ dom โ ) | ||
Theorem | ntrivcvgn0 15849* | A product that converges to a nonzero value converges non-trivially. (Contributed by Scott Fenton, 18-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ seq๐( ยท , ๐น) โ ๐) & โข (๐ โ ๐ โ 0) โ โข (๐ โ โ๐ โ ๐ โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ)) | ||
Theorem | ntrivcvgfvn0 15850* | 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 15851* | 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 15852* | Lemma for ntrivcvgmul 15853. (Contributed by Scott Fenton, 19-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ โ 0) & โข (๐ โ ๐ โ 0) & โข (๐ โ seq๐( ยท , ๐น) โ ๐) & โข (๐ โ seq๐( ยท , ๐บ) โ ๐) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) โ โ) & โข ((๐ โง ๐ โ ๐) โ (๐บโ๐) โ โ) & โข (๐ โ ๐ โค ๐) & โข ((๐ โง ๐ โ ๐) โ (๐ปโ๐) = ((๐นโ๐) ยท (๐บโ๐))) โ โข (๐ โ โ๐ โ ๐ โ๐ค(๐ค โ 0 โง seq๐( ยท , ๐ป) โ ๐ค)) | ||
Theorem | ntrivcvgmul 15853* | 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 15854 | Extend class notation to include complex products. |
class โ๐ โ ๐ด ๐ต | ||
Definition | df-prod 15855* | Define the product of a series with an index set of integers ๐ด. This definition takes most of the aspects of df-sum 15638 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 15856 | A product is a set. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข โ๐ โ ๐ด ๐ต โ V | ||
Theorem | prodeq1f 15857 | Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017.) |
โข โฒ๐๐ด & โข โฒ๐๐ต โ โข (๐ด = ๐ต โ โ๐ โ ๐ด ๐ถ = โ๐ โ ๐ต ๐ถ) | ||
Theorem | prodeq1 15858* | Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017.) |
โข (๐ด = ๐ต โ โ๐ โ ๐ด ๐ถ = โ๐ โ ๐ต ๐ถ) | ||
Theorem | nfcprod1 15859* | Bound-variable hypothesis builder for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข โฒ๐๐ด โ โข โฒ๐โ๐ โ ๐ด ๐ต | ||
Theorem | nfcprod 15860* | 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 15861* | 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 15862* | 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 15863* | Equality theorem for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข (โ๐ โ ๐ด ๐ต = ๐ถ โ โ๐ โ ๐ด ๐ต = โ๐ โ ๐ด ๐ถ) | ||
Theorem | cbvprod 15864* | Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข (๐ = ๐ โ ๐ต = ๐ถ) & โข โฒ๐๐ด & โข โฒ๐๐ด & โข โฒ๐๐ต & โข โฒ๐๐ถ โ โข โ๐ โ ๐ด ๐ต = โ๐ โ ๐ด ๐ถ | ||
Theorem | cbvprodv 15865* | Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข (๐ = ๐ โ ๐ต = ๐ถ) โ โข โ๐ โ ๐ด ๐ต = โ๐ โ ๐ด ๐ถ | ||
Theorem | cbvprodi 15866* | Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข โฒ๐๐ต & โข โฒ๐๐ถ & โข (๐ = ๐ โ ๐ต = ๐ถ) โ โข โ๐ โ ๐ด ๐ต = โ๐ โ ๐ด ๐ถ | ||
Theorem | prodeq1i 15867* | Equality inference for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข ๐ด = ๐ต โ โข โ๐ โ ๐ด ๐ถ = โ๐ โ ๐ต ๐ถ | ||
Theorem | prodeq2i 15868* | Equality inference for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข (๐ โ ๐ด โ ๐ต = ๐ถ) โ โข โ๐ โ ๐ด ๐ต = โ๐ โ ๐ด ๐ถ | ||
Theorem | prodeq12i 15869* | Equality inference for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข ๐ด = ๐ต & โข (๐ โ ๐ด โ ๐ถ = ๐ท) โ โข โ๐ โ ๐ด ๐ถ = โ๐ โ ๐ต ๐ท | ||
Theorem | prodeq1d 15870* | Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข (๐ โ ๐ด = ๐ต) โ โข (๐ โ โ๐ โ ๐ด ๐ถ = โ๐ โ ๐ต ๐ถ) | ||
Theorem | prodeq2d 15871* | Equality deduction for product. Note that unlike prodeq2dv 15872, ๐ may occur in ๐. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข (๐ โ โ๐ โ ๐ด ๐ต = ๐ถ) โ โข (๐ โ โ๐ โ ๐ด ๐ต = โ๐ โ ๐ด ๐ถ) | ||
Theorem | prodeq2dv 15872* | Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข ((๐ โง ๐ โ ๐ด) โ ๐ต = ๐ถ) โ โข (๐ โ โ๐ โ ๐ด ๐ต = โ๐ โ ๐ด ๐ถ) | ||
Theorem | prodeq2sdv 15873* | Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข (๐ โ ๐ต = ๐ถ) โ โข (๐ โ โ๐ โ ๐ด ๐ต = โ๐ โ ๐ด ๐ถ) | ||
Theorem | 2cprodeq2dv 15874* | Equality deduction for double product. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข ((๐ โง ๐ โ ๐ด โง ๐ โ ๐ต) โ ๐ถ = ๐ท) โ โข (๐ โ โ๐ โ ๐ด โ๐ โ ๐ต ๐ถ = โ๐ โ ๐ด โ๐ โ ๐ต ๐ท) | ||
Theorem | prodeq12dv 15875* | Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข (๐ โ ๐ด = ๐ต) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ = ๐ท) โ โข (๐ โ โ๐ โ ๐ด ๐ถ = โ๐ โ ๐ต ๐ท) | ||
Theorem | prodeq12rdv 15876* | Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข (๐ โ ๐ด = ๐ต) & โข ((๐ โง ๐ โ ๐ต) โ ๐ถ = ๐ท) โ โข (๐ โ โ๐ โ ๐ด ๐ถ = โ๐ โ ๐ต ๐ท) | ||
Theorem | prod2id 15877* | The second class argument to a product can be chosen so that it is always a set. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข โ๐ โ ๐ด ๐ต = โ๐ โ ๐ด ( I โ๐ต) | ||
Theorem | prodrblem 15878* | Lemma for prodrb 15881. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข ๐น = (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1)) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข (๐ โ ๐ โ (โคโฅโ๐)) โ โข ((๐ โง ๐ด โ (โคโฅโ๐)) โ (seq๐( ยท , ๐น) โพ (โคโฅโ๐)) = seq๐( ยท , ๐น)) | ||
Theorem | fprodcvg 15879* | The sequence of partial products of a finite product converges to the whole product. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข ๐น = (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1)) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข (๐ โ ๐ โ (โคโฅโ๐)) & โข (๐ โ ๐ด โ (๐...๐)) โ โข (๐ โ seq๐( ยท , ๐น) โ (seq๐( ยท , ๐น)โ๐)) | ||
Theorem | prodrblem2 15880* | Lemma for prodrb 15881. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข ๐น = (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1)) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ด โ (โคโฅโ๐)) & โข (๐ โ ๐ด โ (โคโฅโ๐)) โ โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (seq๐( ยท , ๐น) โ ๐ถ โ seq๐( ยท , ๐น) โ ๐ถ)) | ||
Theorem | prodrb 15881* | Rebase the starting point of a product. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข ๐น = (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1)) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ด โ (โคโฅโ๐)) & โข (๐ โ ๐ด โ (โคโฅโ๐)) โ โข (๐ โ (seq๐( ยท , ๐น) โ ๐ถ โ seq๐( ยท , ๐น) โ ๐ถ)) | ||
Theorem | prodmolem3 15882* | Lemma for prodmo 15885. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข ๐น = (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1)) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข ๐บ = (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต) & โข ๐ป = (๐ โ โ โฆ โฆ(๐พโ๐) / ๐โฆ๐ต) & โข (๐ โ (๐ โ โ โง ๐ โ โ)) & โข (๐ โ ๐:(1...๐)โ1-1-ontoโ๐ด) & โข (๐ โ ๐พ:(1...๐)โ1-1-ontoโ๐ด) โ โข (๐ โ (seq1( ยท , ๐บ)โ๐) = (seq1( ยท , ๐ป)โ๐)) | ||
Theorem | prodmolem2a 15883* | Lemma for prodmo 15885. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข ๐น = (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1)) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข ๐บ = (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต) & โข ๐ป = (๐ โ โ โฆ โฆ(๐พโ๐) / ๐โฆ๐ต) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ด โ (โคโฅโ๐)) & โข (๐ โ ๐:(1...๐)โ1-1-ontoโ๐ด) & โข (๐ โ ๐พ Isom < , < ((1...(โฏโ๐ด)), ๐ด)) โ โข (๐ โ seq๐( ยท , ๐น) โ (seq1( ยท , ๐บ)โ๐)) | ||
Theorem | prodmolem2 15884* | Lemma for prodmo 15885. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข ๐น = (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1)) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข ๐บ = (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต) โ โข ((๐ โง โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ (โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ฅ)) โ (โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ง = (seq1( ยท , ๐บ)โ๐)) โ ๐ฅ = ๐ง)) | ||
Theorem | prodmo 15885* | A product has at most one limit. (Contributed by Scott Fenton, 4-Dec-2017.) |
โข ๐น = (๐ โ โค โฆ if(๐ โ ๐ด, ๐ต, 1)) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข ๐บ = (๐ โ โ โฆ โฆ(๐โ๐) / ๐โฆ๐ต) โ โข (๐ โ โ*๐ฅ(โ๐ โ โค (๐ด โ (โคโฅโ๐) โง โ๐ โ (โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ) โง seq๐( ยท , ๐น) โ ๐ฅ) โจ โ๐ โ โ โ๐(๐:(1...๐)โ1-1-ontoโ๐ด โง ๐ฅ = (seq1( ยท , ๐บ)โ๐)))) | ||
Theorem | zprod 15886* | Series product with index set a subset of the upper integers. (Contributed by Scott Fenton, 5-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ โ๐ โ ๐ โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ)) & โข (๐ โ ๐ด โ ๐) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = if(๐ โ ๐ด, ๐ต, 1)) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ โ๐ โ ๐ด ๐ต = ( โ โseq๐( ยท , ๐น))) | ||
Theorem | iprod 15887* | Series product with an upper integer index set (i.e. an infinite product.) (Contributed by Scott Fenton, 5-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ โ๐ โ ๐ โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ)) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = ๐ต) & โข ((๐ โง ๐ โ ๐) โ ๐ต โ โ) โ โข (๐ โ โ๐ โ ๐ ๐ต = ( โ โseq๐( ยท , ๐น))) | ||
Theorem | zprodn0 15888* | Nonzero series product with index set a subset of the upper integers. (Contributed by Scott Fenton, 6-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ 0) & โข (๐ โ seq๐( ยท , ๐น) โ ๐) & โข (๐ โ ๐ด โ ๐) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = if(๐ โ ๐ด, ๐ต, 1)) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ โ๐ โ ๐ด ๐ต = ๐) | ||
Theorem | iprodn0 15889* | Nonzero series product with an upper integer index set (i.e. an infinite product.) (Contributed by Scott Fenton, 6-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ 0) & โข (๐ โ seq๐( ยท , ๐น) โ ๐) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = ๐ต) & โข ((๐ โง ๐ โ ๐) โ ๐ต โ โ) โ โข (๐ โ โ๐ โ ๐ ๐ต = ๐) | ||
Theorem | fprod 15890* | The value of a product over a nonempty finite set. (Contributed by Scott Fenton, 6-Dec-2017.) |
โข (๐ = (๐นโ๐) โ ๐ต = ๐ถ) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐น:(1...๐)โ1-1-ontoโ๐ด) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข ((๐ โง ๐ โ (1...๐)) โ (๐บโ๐) = ๐ถ) โ โข (๐ โ โ๐ โ ๐ด ๐ต = (seq1( ยท , ๐บ)โ๐)) | ||
Theorem | fprodntriv 15891* | A non-triviality lemma for finite sequences. (Contributed by Scott Fenton, 16-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ด โ (๐...๐)) โ โข (๐ โ โ๐ โ ๐ โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ ๐ โฆ if(๐ โ ๐ด, ๐ต, 1))) โ ๐ฆ)) | ||
Theorem | prod0 15892 | A product over the empty set is one. (Contributed by Scott Fenton, 5-Dec-2017.) |
โข โ๐ โ โ ๐ด = 1 | ||
Theorem | prod1 15893* | Any product of one over a valid set is one. (Contributed by Scott Fenton, 7-Dec-2017.) |
โข ((๐ด โ (โคโฅโ๐) โจ ๐ด โ Fin) โ โ๐ โ ๐ด 1 = 1) | ||
Theorem | prodfc 15894* | A lemma to facilitate conversions from the function form to the class-variable form of a product. (Contributed by Scott Fenton, 7-Dec-2017.) |
โข โ๐ โ ๐ด ((๐ โ ๐ด โฆ ๐ต)โ๐) = โ๐ โ ๐ด ๐ต | ||
Theorem | fprodf1o 15895* | Re-index a finite product using a bijection. (Contributed by Scott Fenton, 7-Dec-2017.) |
โข (๐ = ๐บ โ ๐ต = ๐ท) & โข (๐ โ ๐ถ โ Fin) & โข (๐ โ ๐น:๐ถโ1-1-ontoโ๐ด) & โข ((๐ โง ๐ โ ๐ถ) โ (๐นโ๐) = ๐บ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ โ๐ โ ๐ด ๐ต = โ๐ โ ๐ถ ๐ท) | ||
Theorem | prodss 15896* | Change the index set to a subset in an upper integer product. (Contributed by Scott Fenton, 11-Dec-2017.) |
โข (๐ โ ๐ด โ ๐ต) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โ) & โข (๐ โ โ๐ โ (โคโฅโ๐)โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ (โคโฅโ๐) โฆ if(๐ โ ๐ต, ๐ถ, 1))) โ ๐ฆ)) & โข ((๐ โง ๐ โ (๐ต โ ๐ด)) โ ๐ถ = 1) & โข (๐ โ ๐ต โ (โคโฅโ๐)) โ โข (๐ โ โ๐ โ ๐ด ๐ถ = โ๐ โ ๐ต ๐ถ) | ||
Theorem | fprodss 15897* | Change the index set to a subset in a finite product. (Contributed by Scott Fenton, 16-Dec-2017.) |
โข (๐ โ ๐ด โ ๐ต) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โ) & โข ((๐ โง ๐ โ (๐ต โ ๐ด)) โ ๐ถ = 1) & โข (๐ โ ๐ต โ Fin) โ โข (๐ โ โ๐ โ ๐ด ๐ถ = โ๐ โ ๐ต ๐ถ) | ||
Theorem | fprodser 15898* | A finite product expressed in terms of a partial product of an infinite sequence. The recursive definition of a finite product follows from here. (Contributed by Scott Fenton, 14-Dec-2017.) |
โข ((๐ โง ๐ โ (๐...๐)) โ (๐นโ๐) = ๐ด) & โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) โ โข (๐ โ โ๐ โ (๐...๐)๐ด = (seq๐( ยท , ๐น)โ๐)) | ||
Theorem | fprodcl2lem 15899* | Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017.) |
โข (๐ โ ๐ โ โ) & โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (๐ฅ ยท ๐ฆ) โ ๐) & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ ๐) & โข (๐ โ ๐ด โ โ ) โ โข (๐ โ โ๐ โ ๐ด ๐ต โ ๐) | ||
Theorem | fprodcllem 15900* | Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017.) |
โข (๐ โ ๐ โ โ) & โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (๐ฅ ยท ๐ฆ) โ ๐) & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ ๐) & โข (๐ โ 1 โ ๐) โ โข (๐ โ โ๐ โ ๐ด ๐ต โ ๐) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |