![]() |
Metamath
Proof Explorer Theorem List (p. 160 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-30439) |
![]() (30440-31962) |
![]() (31963-47940) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fprodcl 15901* | Closure of a finite product of complex numbers. (Contributed by Scott Fenton, 14-Dec-2017.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ โ๐ โ ๐ด ๐ต โ โ) | ||
Theorem | fprodrecl 15902* | Closure of a finite product of real numbers. (Contributed by Scott Fenton, 14-Dec-2017.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ โ๐ โ ๐ด ๐ต โ โ) | ||
Theorem | fprodzcl 15903* | Closure of a finite product of integers. (Contributed by Scott Fenton, 14-Dec-2017.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โค) โ โข (๐ โ โ๐ โ ๐ด ๐ต โ โค) | ||
Theorem | fprodnncl 15904* | Closure of a finite product of positive integers. (Contributed by Scott Fenton, 14-Dec-2017.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ โ๐ โ ๐ด ๐ต โ โ) | ||
Theorem | fprodrpcl 15905* | Closure of a finite product of positive reals. (Contributed by Scott Fenton, 14-Dec-2017.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ+) โ โข (๐ โ โ๐ โ ๐ด ๐ต โ โ+) | ||
Theorem | fprodnn0cl 15906* | Closure of a finite product of nonnegative integers. (Contributed by Scott Fenton, 14-Dec-2017.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ0) โ โข (๐ โ โ๐ โ ๐ด ๐ต โ โ0) | ||
Theorem | fprodcllemf 15907* | Finite product closure lemma. A version of fprodcllem 15900 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ & โข (๐ โ ๐ โ โ) & โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (๐ฅ ยท ๐ฆ) โ ๐) & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ ๐) & โข (๐ โ 1 โ ๐) โ โข (๐ โ โ๐ โ ๐ด ๐ต โ ๐) | ||
Theorem | fprodreclf 15908* | Closure of a finite product of real numbers. A version of fprodrecl 15902 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ โ๐ โ ๐ด ๐ต โ โ) | ||
Theorem | fprodmul 15909* | The product of two finite products. (Contributed by Scott Fenton, 14-Dec-2017.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โ) โ โข (๐ โ โ๐ โ ๐ด (๐ต ยท ๐ถ) = (โ๐ โ ๐ด ๐ต ยท โ๐ โ ๐ด ๐ถ)) | ||
Theorem | fproddiv 15910* | The quotient of two finite products. (Contributed by Scott Fenton, 15-Jan-2018.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ 0) โ โข (๐ โ โ๐ โ ๐ด (๐ต / ๐ถ) = (โ๐ โ ๐ด ๐ต / โ๐ โ ๐ด ๐ถ)) | ||
Theorem | prodsn 15911* | A product of a singleton is the term. (Contributed by Scott Fenton, 14-Dec-2017.) |
โข (๐ = ๐ โ ๐ด = ๐ต) โ โข ((๐ โ ๐ โง ๐ต โ โ) โ โ๐ โ {๐}๐ด = ๐ต) | ||
Theorem | fprod1 15912* | A finite product of only one term is the term itself. (Contributed by Scott Fenton, 14-Dec-2017.) |
โข (๐ = ๐ โ ๐ด = ๐ต) โ โข ((๐ โ โค โง ๐ต โ โ) โ โ๐ โ (๐...๐)๐ด = ๐ต) | ||
Theorem | prodsnf 15913* | A product of a singleton is the term. A version of prodsn 15911 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ต & โข (๐ = ๐ โ ๐ด = ๐ต) โ โข ((๐ โ ๐ โง ๐ต โ โ) โ โ๐ โ {๐}๐ด = ๐ต) | ||
Theorem | climprod1 15914 | The limit of a product over one. (Contributed by Scott Fenton, 15-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) โ โข (๐ โ seq๐( ยท , (๐ ร {1})) โ 1) | ||
Theorem | fprodsplit 15915* | Split a finite product into two parts. (Contributed by Scott Fenton, 16-Dec-2017.) |
โข (๐ โ (๐ด โฉ ๐ต) = โ ) & โข (๐ โ ๐ = (๐ด โช ๐ต)) & โข (๐ โ ๐ โ Fin) & โข ((๐ โง ๐ โ ๐) โ ๐ถ โ โ) โ โข (๐ โ โ๐ โ ๐ ๐ถ = (โ๐ โ ๐ด ๐ถ ยท โ๐ โ ๐ต ๐ถ)) | ||
Theorem | fprodm1 15916* | Separate out the last term in a finite product. (Contributed by Scott Fenton, 16-Dec-2017.) |
โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) & โข (๐ = ๐ โ ๐ด = ๐ต) โ โข (๐ โ โ๐ โ (๐...๐)๐ด = (โ๐ โ (๐...(๐ โ 1))๐ด ยท ๐ต)) | ||
Theorem | fprod1p 15917* | Separate out the first term in a finite product. (Contributed by Scott Fenton, 24-Dec-2017.) |
โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) & โข (๐ = ๐ โ ๐ด = ๐ต) โ โข (๐ โ โ๐ โ (๐...๐)๐ด = (๐ต ยท โ๐ โ ((๐ + 1)...๐)๐ด)) | ||
Theorem | fprodp1 15918* | Multiply in the last term in a finite product. (Contributed by Scott Fenton, 24-Dec-2017.) |
โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...(๐ + 1))) โ ๐ด โ โ) & โข (๐ = (๐ + 1) โ ๐ด = ๐ต) โ โข (๐ โ โ๐ โ (๐...(๐ + 1))๐ด = (โ๐ โ (๐...๐)๐ด ยท ๐ต)) | ||
Theorem | fprodm1s 15919* | Separate out the last term in a finite product. (Contributed by Scott Fenton, 27-Dec-2017.) |
โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) โ โข (๐ โ โ๐ โ (๐...๐)๐ด = (โ๐ โ (๐...(๐ โ 1))๐ด ยท โฆ๐ / ๐โฆ๐ด)) | ||
Theorem | fprodp1s 15920* | Multiply in the last term in a finite product. (Contributed by Scott Fenton, 27-Dec-2017.) |
โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...(๐ + 1))) โ ๐ด โ โ) โ โข (๐ โ โ๐ โ (๐...(๐ + 1))๐ด = (โ๐ โ (๐...๐)๐ด ยท โฆ(๐ + 1) / ๐โฆ๐ด)) | ||
Theorem | prodsns 15921* | A product of the singleton is the term. (Contributed by Scott Fenton, 25-Dec-2017.) |
โข ((๐ โ ๐ โง โฆ๐ / ๐โฆ๐ด โ โ) โ โ๐ โ {๐}๐ด = โฆ๐ / ๐โฆ๐ด) | ||
Theorem | fprodfac 15922* | Factorial using product notation. (Contributed by Scott Fenton, 15-Dec-2017.) |
โข (๐ด โ โ0 โ (!โ๐ด) = โ๐ โ (1...๐ด)๐) | ||
Theorem | fprodabs 15923* | The absolute value of a finite product. (Contributed by Scott Fenton, 25-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ ๐) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) โ โข (๐ โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) | ||
Theorem | fprodeq0 15924* | Any finite product containing a zero term is itself zero. (Contributed by Scott Fenton, 27-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ ๐) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) & โข ((๐ โง ๐ = ๐) โ ๐ด = 0) โ โข ((๐ โง ๐พ โ (โคโฅโ๐)) โ โ๐ โ (๐...๐พ)๐ด = 0) | ||
Theorem | fprodshft 15925* | Shift the index of a finite product. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข (๐ โ ๐พ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) & โข (๐ = (๐ โ ๐พ) โ ๐ด = ๐ต) โ โข (๐ โ โ๐ โ (๐...๐)๐ด = โ๐ โ ((๐ + ๐พ)...(๐ + ๐พ))๐ต) | ||
Theorem | fprodrev 15926* | Reversal of a finite product. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข (๐ โ ๐พ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) & โข (๐ = (๐พ โ ๐) โ ๐ด = ๐ต) โ โข (๐ โ โ๐ โ (๐...๐)๐ด = โ๐ โ ((๐พ โ ๐)...(๐พ โ ๐))๐ต) | ||
Theorem | fprodconst 15927* | The product of constant terms (๐ is not free in ๐ต). (Contributed by Scott Fenton, 12-Jan-2018.) |
โข ((๐ด โ Fin โง ๐ต โ โ) โ โ๐ โ ๐ด ๐ต = (๐ตโ(โฏโ๐ด))) | ||
Theorem | fprodn0 15928* | A finite product of nonzero terms is nonzero. (Contributed by Scott Fenton, 15-Jan-2018.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ 0) โ โข (๐ โ โ๐ โ ๐ด ๐ต โ 0) | ||
Theorem | fprod2dlem 15929* | Lemma for fprod2d 15930- induction step. (Contributed by Scott Fenton, 30-Jan-2018.) |
โข (๐ง = โจ๐, ๐โฉ โ ๐ท = ๐ถ) & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ Fin) & โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ถ โ โ) & โข (๐ โ ยฌ ๐ฆ โ ๐ฅ) & โข (๐ โ (๐ฅ โช {๐ฆ}) โ ๐ด) & โข (๐ โ โ๐ โ ๐ฅ โ๐ โ ๐ต ๐ถ = โ๐ง โ โช ๐ โ ๐ฅ ({๐} ร ๐ต)๐ท) โ โข ((๐ โง ๐) โ โ๐ โ (๐ฅ โช {๐ฆ})โ๐ โ ๐ต ๐ถ = โ๐ง โ โช ๐ โ (๐ฅ โช {๐ฆ})({๐} ร ๐ต)๐ท) | ||
Theorem | fprod2d 15930* | Write a double product as a product over a two-dimensional region. Compare fsum2d 15722. (Contributed by Scott Fenton, 30-Jan-2018.) |
โข (๐ง = โจ๐, ๐โฉ โ ๐ท = ๐ถ) & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ Fin) & โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ถ โ โ) โ โข (๐ โ โ๐ โ ๐ด โ๐ โ ๐ต ๐ถ = โ๐ง โ โช ๐ โ ๐ด ({๐} ร ๐ต)๐ท) | ||
Theorem | fprodxp 15931* | Combine two products into a single product over the cartesian product. (Contributed by Scott Fenton, 1-Feb-2018.) |
โข (๐ง = โจ๐, ๐โฉ โ ๐ท = ๐ถ) & โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ต โ Fin) & โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ถ โ โ) โ โข (๐ โ โ๐ โ ๐ด โ๐ โ ๐ต ๐ถ = โ๐ง โ (๐ด ร ๐ต)๐ท) | ||
Theorem | fprodcnv 15932* | Transform a product region using the converse operation. (Contributed by Scott Fenton, 1-Feb-2018.) |
โข (๐ฅ = โจ๐, ๐โฉ โ ๐ต = ๐ท) & โข (๐ฆ = โจ๐, ๐โฉ โ ๐ถ = ๐ท) & โข (๐ โ ๐ด โ Fin) & โข (๐ โ Rel ๐ด) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ โ๐ฅ โ ๐ด ๐ต = โ๐ฆ โ โก ๐ด๐ถ) | ||
Theorem | fprodcom2 15933* | Interchange order of multiplication. Note that ๐ต(๐) and ๐ท(๐) are not necessarily constant expressions. (Contributed by Scott Fenton, 1-Feb-2018.) (Proof shortened by JJ, 2-Aug-2021.) |
โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ถ โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ Fin) & โข (๐ โ ((๐ โ ๐ด โง ๐ โ ๐ต) โ (๐ โ ๐ถ โง ๐ โ ๐ท))) & โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ธ โ โ) โ โข (๐ โ โ๐ โ ๐ด โ๐ โ ๐ต ๐ธ = โ๐ โ ๐ถ โ๐ โ ๐ท ๐ธ) | ||
Theorem | fprodcom 15934* | Interchange product order. (Contributed by Scott Fenton, 2-Feb-2018.) |
โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ต โ Fin) & โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ถ โ โ) โ โข (๐ โ โ๐ โ ๐ด โ๐ โ ๐ต ๐ถ = โ๐ โ ๐ต โ๐ โ ๐ด ๐ถ) | ||
Theorem | fprod0diag 15935* | Two ways to express "the product of ๐ด(๐, ๐) over the triangular region ๐ โค ๐, ๐ โค ๐, ๐ + ๐ โค ๐. Compare fsum0diag 15728. (Contributed by Scott Fenton, 2-Feb-2018.) |
โข ((๐ โง (๐ โ (0...๐) โง ๐ โ (0...(๐ โ ๐)))) โ ๐ด โ โ) โ โข (๐ โ โ๐ โ (0...๐)โ๐ โ (0...(๐ โ ๐))๐ด = โ๐ โ (0...๐)โ๐ โ (0...(๐ โ ๐))๐ด) | ||
Theorem | fproddivf 15936* | The quotient of two finite products. A version of fproddiv 15910 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ 0) โ โข (๐ โ โ๐ โ ๐ด (๐ต / ๐ถ) = (โ๐ โ ๐ด ๐ต / โ๐ โ ๐ด ๐ถ)) | ||
Theorem | fprodsplitf 15937* | Split a finite product into two parts. A version of fprodsplit 15915 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ & โข (๐ โ (๐ด โฉ ๐ต) = โ ) & โข (๐ โ ๐ = (๐ด โช ๐ต)) & โข (๐ โ ๐ โ Fin) & โข ((๐ โง ๐ โ ๐) โ ๐ถ โ โ) โ โข (๐ โ โ๐ โ ๐ ๐ถ = (โ๐ โ ๐ด ๐ถ ยท โ๐ โ ๐ต ๐ถ)) | ||
Theorem | fprodsplitsn 15938* | Separate out a term in a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ & โข โฒ๐๐ท & โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ต โ ๐) & โข (๐ โ ยฌ ๐ต โ ๐ด) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โ) & โข (๐ = ๐ต โ ๐ถ = ๐ท) & โข (๐ โ ๐ท โ โ) โ โข (๐ โ โ๐ โ (๐ด โช {๐ต})๐ถ = (โ๐ โ ๐ด ๐ถ ยท ๐ท)) | ||
Theorem | fprodsplit1f 15939* | Separate out a term in a finite product. A version of fprodsplit1 44608 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ & โข (๐ โ โฒ๐๐ท) & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข (๐ โ ๐ถ โ ๐ด) & โข ((๐ โง ๐ = ๐ถ) โ ๐ต = ๐ท) โ โข (๐ โ โ๐ โ ๐ด ๐ต = (๐ท ยท โ๐ โ (๐ด โ {๐ถ})๐ต)) | ||
Theorem | fprodn0f 15940* | A finite product of nonzero terms is nonzero. A version of fprodn0 15928 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ 0) โ โข (๐ โ โ๐ โ ๐ด ๐ต โ 0) | ||
Theorem | fprodclf 15941* | Closure of a finite product of complex numbers. A version of fprodcl 15901 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ โ๐ โ ๐ด ๐ต โ โ) | ||
Theorem | fprodge0 15942* | If all the terms of a finite product are nonnegative, so is the product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข ((๐ โง ๐ โ ๐ด) โ 0 โค ๐ต) โ โข (๐ โ 0 โค โ๐ โ ๐ด ๐ต) | ||
Theorem | fprodeq0g 15943* | Any finite product containing a zero term is itself zero. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข (๐ โ ๐ถ โ ๐ด) & โข ((๐ โง ๐ = ๐ถ) โ ๐ต = 0) โ โข (๐ โ โ๐ โ ๐ด ๐ต = 0) | ||
Theorem | fprodge1 15944* | If all of the terms of a finite product are greater than or equal to 1, so is the product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข ((๐ โง ๐ โ ๐ด) โ 1 โค ๐ต) โ โข (๐ โ 1 โค โ๐ โ ๐ด ๐ต) | ||
Theorem | fprodle 15945* | If all the terms of two finite products are nonnegative and compare, so do the two products. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข ((๐ โง ๐ โ ๐ด) โ 0 โค ๐ต) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โค ๐ถ) โ โข (๐ โ โ๐ โ ๐ด ๐ต โค โ๐ โ ๐ด ๐ถ) | ||
Theorem | fprodmodd 15946* | If all factors of two finite products are equal modulo ๐, the products are equal modulo ๐. (Contributed by AV, 7-Jul-2021.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โค) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โค) & โข (๐ โ ๐ โ โ) & โข ((๐ โง ๐ โ ๐ด) โ (๐ต mod ๐) = (๐ถ mod ๐)) โ โข (๐ โ (โ๐ โ ๐ด ๐ต mod ๐) = (โ๐ โ ๐ด ๐ถ mod ๐)) | ||
Theorem | iprodclim 15947* | An infinite product equals the value its sequence converges to. (Contributed by Scott Fenton, 18-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ โ๐ โ ๐ โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ)) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = ๐ด) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) & โข (๐ โ seq๐( ยท , ๐น) โ ๐ต) โ โข (๐ โ โ๐ โ ๐ ๐ด = ๐ต) | ||
Theorem | iprodclim2 15948* | A converging product converges to its infinite product. (Contributed by Scott Fenton, 18-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ โ๐ โ ๐ โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ)) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = ๐ด) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) โ โข (๐ โ seq๐( ยท , ๐น) โ โ๐ โ ๐ ๐ด) | ||
Theorem | iprodclim3 15949* | The sequence of partial finite product of a converging infinite product converge to the infinite product of the series. Note that ๐ must not occur in ๐ด. (Contributed by Scott Fenton, 18-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ โ๐ โ ๐ โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , (๐ โ ๐ โฆ ๐ด)) โ ๐ฆ)) & โข (๐ โ ๐น โ dom โ ) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = โ๐ โ (๐...๐)๐ด) โ โข (๐ โ ๐น โ โ๐ โ ๐ ๐ด) | ||
Theorem | iprodcl 15950* | The product of a non-trivially converging infinite sequence is a complex number. (Contributed by Scott Fenton, 18-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ โ๐ โ ๐ โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ)) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = ๐ด) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) โ โข (๐ โ โ๐ โ ๐ ๐ด โ โ) | ||
Theorem | iprodrecl 15951* | The product of a non-trivially converging infinite real sequence is a real number. (Contributed by Scott Fenton, 18-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ โ๐ โ ๐ โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ)) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = ๐ด) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) โ โข (๐ โ โ๐ โ ๐ ๐ด โ โ) | ||
Theorem | iprodmul 15952* | Multiplication of infinite sums. (Contributed by Scott Fenton, 18-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ โ๐ โ ๐ โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ)) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = ๐ด) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) & โข (๐ โ โ๐ โ ๐ โ๐ง(๐ง โ 0 โง seq๐( ยท , ๐บ) โ ๐ง)) & โข ((๐ โง ๐ โ ๐) โ (๐บโ๐) = ๐ต) & โข ((๐ โง ๐ โ ๐) โ ๐ต โ โ) โ โข (๐ โ โ๐ โ ๐ (๐ด ยท ๐ต) = (โ๐ โ ๐ ๐ด ยท โ๐ โ ๐ ๐ต)) | ||
Syntax | cfallfac 15953 | Declare the syntax for the falling factorial. |
class FallFac | ||
Syntax | crisefac 15954 | Declare the syntax for the rising factorial. |
class RiseFac | ||
Definition | df-risefac 15955* | Define the rising factorial function. This is the function (๐ด ยท (๐ด + 1) ยท ...(๐ด + ๐)) for complex ๐ด and nonnegative integers ๐. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข RiseFac = (๐ฅ โ โ, ๐ โ โ0 โฆ โ๐ โ (0...(๐ โ 1))(๐ฅ + ๐)) | ||
Definition | df-fallfac 15956* | Define the falling factorial function. This is the function (๐ด ยท (๐ด โ 1) ยท ...(๐ด โ ๐)) for complex ๐ด and nonnegative integers ๐. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข FallFac = (๐ฅ โ โ, ๐ โ โ0 โฆ โ๐ โ (0...(๐ โ 1))(๐ฅ โ ๐)) | ||
Theorem | risefacval 15957* | The value of the rising factorial function. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด RiseFac ๐) = โ๐ โ (0...(๐ โ 1))(๐ด + ๐)) | ||
Theorem | fallfacval 15958* | The value of the falling factorial function. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด FallFac ๐) = โ๐ โ (0...(๐ โ 1))(๐ด โ ๐)) | ||
Theorem | risefacval2 15959* | One-based value of rising factorial. (Contributed by Scott Fenton, 15-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด RiseFac ๐) = โ๐ โ (1...๐)(๐ด + (๐ โ 1))) | ||
Theorem | fallfacval2 15960* | One-based value of falling factorial. (Contributed by Scott Fenton, 15-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด FallFac ๐) = โ๐ โ (1...๐)(๐ด โ (๐ โ 1))) | ||
Theorem | fallfacval3 15961* | A product representation of falling factorial when ๐ด is a nonnegative integer. (Contributed by Scott Fenton, 20-Mar-2018.) |
โข (๐ โ (0...๐ด) โ (๐ด FallFac ๐) = โ๐ โ ((๐ด โ (๐ โ 1))...๐ด)๐) | ||
Theorem | risefaccllem 15962* | Lemma for rising factorial closure laws. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ๐ โ โ & โข 1 โ ๐ & โข ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โ (๐ฅ ยท ๐ฆ) โ ๐) & โข ((๐ด โ ๐ โง ๐ โ โ0) โ (๐ด + ๐) โ ๐) โ โข ((๐ด โ ๐ โง ๐ โ โ0) โ (๐ด RiseFac ๐) โ ๐) | ||
Theorem | fallfaccllem 15963* | Lemma for falling factorial closure laws. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ๐ โ โ & โข 1 โ ๐ & โข ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โ (๐ฅ ยท ๐ฆ) โ ๐) & โข ((๐ด โ ๐ โง ๐ โ โ0) โ (๐ด โ ๐) โ ๐) โ โข ((๐ด โ ๐ โง ๐ โ โ0) โ (๐ด FallFac ๐) โ ๐) | ||
Theorem | risefaccl 15964 | Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด RiseFac ๐) โ โ) | ||
Theorem | fallfaccl 15965 | Closure law for falling factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด FallFac ๐) โ โ) | ||
Theorem | rerisefaccl 15966 | Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด RiseFac ๐) โ โ) | ||
Theorem | refallfaccl 15967 | Closure law for falling factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด FallFac ๐) โ โ) | ||
Theorem | nnrisefaccl 15968 | Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด RiseFac ๐) โ โ) | ||
Theorem | zrisefaccl 15969 | Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โค โง ๐ โ โ0) โ (๐ด RiseFac ๐) โ โค) | ||
Theorem | zfallfaccl 15970 | Closure law for falling factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โค โง ๐ โ โ0) โ (๐ด FallFac ๐) โ โค) | ||
Theorem | nn0risefaccl 15971 | Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ0 โง ๐ โ โ0) โ (๐ด RiseFac ๐) โ โ0) | ||
Theorem | rprisefaccl 15972 | Closure law for rising factorial. (Contributed by Scott Fenton, 9-Jan-2018.) |
โข ((๐ด โ โ+ โง ๐ โ โ0) โ (๐ด RiseFac ๐) โ โ+) | ||
Theorem | risefallfac 15973 | A relationship between rising and falling factorials. (Contributed by Scott Fenton, 15-Jan-2018.) |
โข ((๐ โ โ โง ๐ โ โ0) โ (๐ RiseFac ๐) = ((-1โ๐) ยท (-๐ FallFac ๐))) | ||
Theorem | fallrisefac 15974 | A relationship between falling and rising factorials. (Contributed by Scott Fenton, 17-Jan-2018.) |
โข ((๐ โ โ โง ๐ โ โ0) โ (๐ FallFac ๐) = ((-1โ๐) ยท (-๐ RiseFac ๐))) | ||
Theorem | risefall0lem 15975 | Lemma for risefac0 15976 and fallfac0 15977. Show a particular set of finite integers is empty. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข (0...(0 โ 1)) = โ | ||
Theorem | risefac0 15976 | The value of the rising factorial when ๐ = 0. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข (๐ด โ โ โ (๐ด RiseFac 0) = 1) | ||
Theorem | fallfac0 15977 | The value of the falling factorial when ๐ = 0. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข (๐ด โ โ โ (๐ด FallFac 0) = 1) | ||
Theorem | risefacp1 15978 | The value of the rising factorial at a successor. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด RiseFac (๐ + 1)) = ((๐ด RiseFac ๐) ยท (๐ด + ๐))) | ||
Theorem | fallfacp1 15979 | The value of the falling factorial at a successor. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด FallFac (๐ + 1)) = ((๐ด FallFac ๐) ยท (๐ด โ ๐))) | ||
Theorem | risefacp1d 15980 | The value of the rising factorial at a successor. (Contributed by Scott Fenton, 19-Mar-2018.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ โ โ0) โ โข (๐ โ (๐ด RiseFac (๐ + 1)) = ((๐ด RiseFac ๐) ยท (๐ด + ๐))) | ||
Theorem | fallfacp1d 15981 | The value of the falling factorial at a successor. (Contributed by Scott Fenton, 19-Mar-2018.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ โ โ0) โ โข (๐ โ (๐ด FallFac (๐ + 1)) = ((๐ด FallFac ๐) ยท (๐ด โ ๐))) | ||
Theorem | risefac1 15982 | The value of rising factorial at one. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข (๐ด โ โ โ (๐ด RiseFac 1) = ๐ด) | ||
Theorem | fallfac1 15983 | The value of falling factorial at one. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข (๐ด โ โ โ (๐ด FallFac 1) = ๐ด) | ||
Theorem | risefacfac 15984 | Relate rising factorial to factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข (๐ โ โ0 โ (1 RiseFac ๐) = (!โ๐)) | ||
Theorem | fallfacfwd 15985 | The forward difference of a falling factorial. (Contributed by Scott Fenton, 21-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ) โ (((๐ด + 1) FallFac ๐) โ (๐ด FallFac ๐)) = (๐ ยท (๐ด FallFac (๐ โ 1)))) | ||
Theorem | 0fallfac 15986 | The value of the zero falling factorial at natural ๐. (Contributed by Scott Fenton, 17-Feb-2018.) |
โข (๐ โ โ โ (0 FallFac ๐) = 0) | ||
Theorem | 0risefac 15987 | The value of the zero rising factorial at natural ๐. (Contributed by Scott Fenton, 17-Feb-2018.) |
โข (๐ โ โ โ (0 RiseFac ๐) = 0) | ||
Theorem | binomfallfaclem1 15988 | Lemma for binomfallfac 15990. Closure law. (Contributed by Scott Fenton, 13-Mar-2018.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ โ โ0) โ โข ((๐ โง ๐พ โ (0...๐)) โ ((๐C๐พ) ยท ((๐ด FallFac (๐ โ ๐พ)) ยท (๐ต FallFac (๐พ + 1)))) โ โ) | ||
Theorem | binomfallfaclem2 15989* | Lemma for binomfallfac 15990. Inductive step. (Contributed by Scott Fenton, 13-Mar-2018.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ โ โ0) & โข (๐ โ ((๐ด + ๐ต) FallFac ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)))) โ โข ((๐ โง ๐) โ ((๐ด + ๐ต) FallFac (๐ + 1)) = ฮฃ๐ โ (0...(๐ + 1))(((๐ + 1)C๐) ยท ((๐ด FallFac ((๐ + 1) โ ๐)) ยท (๐ต FallFac ๐)))) | ||
Theorem | binomfallfac 15990* | A version of the binomial theorem using falling factorials instead of exponentials. (Contributed by Scott Fenton, 13-Mar-2018.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ0) โ ((๐ด + ๐ต) FallFac ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด FallFac (๐ โ ๐)) ยท (๐ต FallFac ๐)))) | ||
Theorem | binomrisefac 15991* | A version of the binomial theorem using rising factorials instead of exponentials. (Contributed by Scott Fenton, 16-Mar-2018.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ0) โ ((๐ด + ๐ต) RiseFac ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ด RiseFac (๐ โ ๐)) ยท (๐ต RiseFac ๐)))) | ||
Theorem | fallfacval4 15992 | Represent the falling factorial via factorials when the first argument is a natural. (Contributed by Scott Fenton, 20-Mar-2018.) |
โข (๐ โ (0...๐ด) โ (๐ด FallFac ๐) = ((!โ๐ด) / (!โ(๐ด โ ๐)))) | ||
Theorem | bcfallfac 15993 | Binomial coefficient in terms of falling factorials. (Contributed by Scott Fenton, 20-Mar-2018.) |
โข (๐พ โ (0...๐) โ (๐C๐พ) = ((๐ FallFac ๐พ) / (!โ๐พ))) | ||
Theorem | fallfacfac 15994 | Relate falling factorial to factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข (๐ โ โ0 โ (๐ FallFac ๐) = (!โ๐)) | ||
Syntax | cbp 15995 | Declare the constant for the Bernoulli polynomial operator. |
class BernPoly | ||
Definition | df-bpoly 15996* | Define the Bernoulli polynomials. Here we use well-founded recursion to define the Bernoulli polynomials. This agrees with most textbook definitions, although explicit formulas do exist. (Contributed by Scott Fenton, 22-May-2014.) |
โข BernPoly = (๐ โ โ0, ๐ฅ โ โ โฆ (wrecs( < , โ0, (๐ โ V โฆ โฆ(โฏโdom ๐) / ๐โฆ((๐ฅโ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))))))โ๐)) | ||
Theorem | bpolylem 15997* | Lemma for bpolyval 15998. (Contributed by Scott Fenton, 22-May-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
โข ๐บ = (๐ โ V โฆ โฆ(โฏโdom ๐) / ๐โฆ((๐โ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))))) & โข ๐น = wrecs( < , โ0, ๐บ) โ โข ((๐ โ โ0 โง ๐ โ โ) โ (๐ BernPoly ๐) = ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))))) | ||
Theorem | bpolyval 15998* | The value of the Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014.) |
โข ((๐ โ โ0 โง ๐ โ โ) โ (๐ BernPoly ๐) = ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))))) | ||
Theorem | bpoly0 15999 | The value of the Bernoulli polynomials at zero. (Contributed by Scott Fenton, 16-May-2014.) |
โข (๐ โ โ โ (0 BernPoly ๐) = 1) | ||
Theorem | bpoly1 16000 | The value of the Bernoulli polynomials at one. (Contributed by Scott Fenton, 16-May-2014.) |
โข (๐ โ โ โ (1 BernPoly ๐) = (๐ โ (1 / 2))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |