![]() |
Metamath
Proof Explorer Theorem List (p. 160 of 481) | < 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-30640) |
![]() (30641-32163) |
![]() (32164-48040) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fprodmul 15901* | The product of two finite products. (Contributed by Scott Fenton, 14-Dec-2017.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โ) โ โข (๐ โ โ๐ โ ๐ด (๐ต ยท ๐ถ) = (โ๐ โ ๐ด ๐ต ยท โ๐ โ ๐ด ๐ถ)) | ||
Theorem | fproddiv 15902* | The quotient of two finite products. (Contributed by Scott Fenton, 15-Jan-2018.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ 0) โ โข (๐ โ โ๐ โ ๐ด (๐ต / ๐ถ) = (โ๐ โ ๐ด ๐ต / โ๐ โ ๐ด ๐ถ)) | ||
Theorem | prodsn 15903* | A product of a singleton is the term. (Contributed by Scott Fenton, 14-Dec-2017.) |
โข (๐ = ๐ โ ๐ด = ๐ต) โ โข ((๐ โ ๐ โง ๐ต โ โ) โ โ๐ โ {๐}๐ด = ๐ต) | ||
Theorem | fprod1 15904* | A finite product of only one term is the term itself. (Contributed by Scott Fenton, 14-Dec-2017.) |
โข (๐ = ๐ โ ๐ด = ๐ต) โ โข ((๐ โ โค โง ๐ต โ โ) โ โ๐ โ (๐...๐)๐ด = ๐ต) | ||
Theorem | prodsnf 15905* | A product of a singleton is the term. A version of prodsn 15903 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ต & โข (๐ = ๐ โ ๐ด = ๐ต) โ โข ((๐ โ ๐ โง ๐ต โ โ) โ โ๐ โ {๐}๐ด = ๐ต) | ||
Theorem | climprod1 15906 | The limit of a product over one. (Contributed by Scott Fenton, 15-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) โ โข (๐ โ seq๐( ยท , (๐ ร {1})) โ 1) | ||
Theorem | fprodsplit 15907* | Split a finite product into two parts. (Contributed by Scott Fenton, 16-Dec-2017.) |
โข (๐ โ (๐ด โฉ ๐ต) = โ ) & โข (๐ โ ๐ = (๐ด โช ๐ต)) & โข (๐ โ ๐ โ Fin) & โข ((๐ โง ๐ โ ๐) โ ๐ถ โ โ) โ โข (๐ โ โ๐ โ ๐ ๐ถ = (โ๐ โ ๐ด ๐ถ ยท โ๐ โ ๐ต ๐ถ)) | ||
Theorem | fprodm1 15908* | Separate out the last term in a finite product. (Contributed by Scott Fenton, 16-Dec-2017.) |
โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) & โข (๐ = ๐ โ ๐ด = ๐ต) โ โข (๐ โ โ๐ โ (๐...๐)๐ด = (โ๐ โ (๐...(๐ โ 1))๐ด ยท ๐ต)) | ||
Theorem | fprod1p 15909* | Separate out the first term in a finite product. (Contributed by Scott Fenton, 24-Dec-2017.) |
โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) & โข (๐ = ๐ โ ๐ด = ๐ต) โ โข (๐ โ โ๐ โ (๐...๐)๐ด = (๐ต ยท โ๐ โ ((๐ + 1)...๐)๐ด)) | ||
Theorem | fprodp1 15910* | Multiply in the last term in a finite product. (Contributed by Scott Fenton, 24-Dec-2017.) |
โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...(๐ + 1))) โ ๐ด โ โ) & โข (๐ = (๐ + 1) โ ๐ด = ๐ต) โ โข (๐ โ โ๐ โ (๐...(๐ + 1))๐ด = (โ๐ โ (๐...๐)๐ด ยท ๐ต)) | ||
Theorem | fprodm1s 15911* | Separate out the last term in a finite product. (Contributed by Scott Fenton, 27-Dec-2017.) |
โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) โ โข (๐ โ โ๐ โ (๐...๐)๐ด = (โ๐ โ (๐...(๐ โ 1))๐ด ยท โฆ๐ / ๐โฆ๐ด)) | ||
Theorem | fprodp1s 15912* | Multiply in the last term in a finite product. (Contributed by Scott Fenton, 27-Dec-2017.) |
โข (๐ โ ๐ โ (โคโฅโ๐)) & โข ((๐ โง ๐ โ (๐...(๐ + 1))) โ ๐ด โ โ) โ โข (๐ โ โ๐ โ (๐...(๐ + 1))๐ด = (โ๐ โ (๐...๐)๐ด ยท โฆ(๐ + 1) / ๐โฆ๐ด)) | ||
Theorem | prodsns 15913* | A product of the singleton is the term. (Contributed by Scott Fenton, 25-Dec-2017.) |
โข ((๐ โ ๐ โง โฆ๐ / ๐โฆ๐ด โ โ) โ โ๐ โ {๐}๐ด = โฆ๐ / ๐โฆ๐ด) | ||
Theorem | fprodfac 15914* | Factorial using product notation. (Contributed by Scott Fenton, 15-Dec-2017.) |
โข (๐ด โ โ0 โ (!โ๐ด) = โ๐ โ (1...๐ด)๐) | ||
Theorem | fprodabs 15915* | The absolute value of a finite product. (Contributed by Scott Fenton, 25-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ ๐) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) โ โข (๐ โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) | ||
Theorem | fprodeq0 15916* | Any finite product containing a zero term is itself zero. (Contributed by Scott Fenton, 27-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ ๐) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) & โข ((๐ โง ๐ = ๐) โ ๐ด = 0) โ โข ((๐ โง ๐พ โ (โคโฅโ๐)) โ โ๐ โ (๐...๐พ)๐ด = 0) | ||
Theorem | fprodshft 15917* | Shift the index of a finite product. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข (๐ โ ๐พ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) & โข (๐ = (๐ โ ๐พ) โ ๐ด = ๐ต) โ โข (๐ โ โ๐ โ (๐...๐)๐ด = โ๐ โ ((๐ + ๐พ)...(๐ + ๐พ))๐ต) | ||
Theorem | fprodrev 15918* | Reversal of a finite product. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข (๐ โ ๐พ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) & โข (๐ = (๐พ โ ๐) โ ๐ด = ๐ต) โ โข (๐ โ โ๐ โ (๐...๐)๐ด = โ๐ โ ((๐พ โ ๐)...(๐พ โ ๐))๐ต) | ||
Theorem | fprodconst 15919* | The product of constant terms (๐ is not free in ๐ต). (Contributed by Scott Fenton, 12-Jan-2018.) |
โข ((๐ด โ Fin โง ๐ต โ โ) โ โ๐ โ ๐ด ๐ต = (๐ตโ(โฏโ๐ด))) | ||
Theorem | fprodn0 15920* | A finite product of nonzero terms is nonzero. (Contributed by Scott Fenton, 15-Jan-2018.) |
โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ 0) โ โข (๐ โ โ๐ โ ๐ด ๐ต โ 0) | ||
Theorem | fprod2dlem 15921* | Lemma for fprod2d 15922- induction step. (Contributed by Scott Fenton, 30-Jan-2018.) |
โข (๐ง = โจ๐, ๐โฉ โ ๐ท = ๐ถ) & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ Fin) & โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ถ โ โ) & โข (๐ โ ยฌ ๐ฆ โ ๐ฅ) & โข (๐ โ (๐ฅ โช {๐ฆ}) โ ๐ด) & โข (๐ โ โ๐ โ ๐ฅ โ๐ โ ๐ต ๐ถ = โ๐ง โ โช ๐ โ ๐ฅ ({๐} ร ๐ต)๐ท) โ โข ((๐ โง ๐) โ โ๐ โ (๐ฅ โช {๐ฆ})โ๐ โ ๐ต ๐ถ = โ๐ง โ โช ๐ โ (๐ฅ โช {๐ฆ})({๐} ร ๐ต)๐ท) | ||
Theorem | fprod2d 15922* | Write a double product as a product over a two-dimensional region. Compare fsum2d 15714. (Contributed by Scott Fenton, 30-Jan-2018.) |
โข (๐ง = โจ๐, ๐โฉ โ ๐ท = ๐ถ) & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ Fin) & โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ถ โ โ) โ โข (๐ โ โ๐ โ ๐ด โ๐ โ ๐ต ๐ถ = โ๐ง โ โช ๐ โ ๐ด ({๐} ร ๐ต)๐ท) | ||
Theorem | fprodxp 15923* | Combine two products into a single product over the cartesian product. (Contributed by Scott Fenton, 1-Feb-2018.) |
โข (๐ง = โจ๐, ๐โฉ โ ๐ท = ๐ถ) & โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ต โ Fin) & โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ถ โ โ) โ โข (๐ โ โ๐ โ ๐ด โ๐ โ ๐ต ๐ถ = โ๐ง โ (๐ด ร ๐ต)๐ท) | ||
Theorem | fprodcnv 15924* | Transform a product region using the converse operation. (Contributed by Scott Fenton, 1-Feb-2018.) |
โข (๐ฅ = โจ๐, ๐โฉ โ ๐ต = ๐ท) & โข (๐ฆ = โจ๐, ๐โฉ โ ๐ถ = ๐ท) & โข (๐ โ ๐ด โ Fin) & โข (๐ โ Rel ๐ด) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ โ๐ฅ โ ๐ด ๐ต = โ๐ฆ โ โก ๐ด๐ถ) | ||
Theorem | fprodcom2 15925* | 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 15926* | Interchange product order. (Contributed by Scott Fenton, 2-Feb-2018.) |
โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ต โ Fin) & โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ถ โ โ) โ โข (๐ โ โ๐ โ ๐ด โ๐ โ ๐ต ๐ถ = โ๐ โ ๐ต โ๐ โ ๐ด ๐ถ) | ||
Theorem | fprod0diag 15927* | Two ways to express "the product of ๐ด(๐, ๐) over the triangular region ๐ โค ๐, ๐ โค ๐, ๐ + ๐ โค ๐. Compare fsum0diag 15720. (Contributed by Scott Fenton, 2-Feb-2018.) |
โข ((๐ โง (๐ โ (0...๐) โง ๐ โ (0...(๐ โ ๐)))) โ ๐ด โ โ) โ โข (๐ โ โ๐ โ (0...๐)โ๐ โ (0...(๐ โ ๐))๐ด = โ๐ โ (0...๐)โ๐ โ (0...(๐ โ ๐))๐ด) | ||
Theorem | fproddivf 15928* | The quotient of two finite products. A version of fproddiv 15902 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ 0) โ โข (๐ โ โ๐ โ ๐ด (๐ต / ๐ถ) = (โ๐ โ ๐ด ๐ต / โ๐ โ ๐ด ๐ถ)) | ||
Theorem | fprodsplitf 15929* | Split a finite product into two parts. A version of fprodsplit 15907 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ & โข (๐ โ (๐ด โฉ ๐ต) = โ ) & โข (๐ โ ๐ = (๐ด โช ๐ต)) & โข (๐ โ ๐ โ Fin) & โข ((๐ โง ๐ โ ๐) โ ๐ถ โ โ) โ โข (๐ โ โ๐ โ ๐ ๐ถ = (โ๐ โ ๐ด ๐ถ ยท โ๐ โ ๐ต ๐ถ)) | ||
Theorem | fprodsplitsn 15930* | Separate out a term in a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ & โข โฒ๐๐ท & โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ต โ ๐) & โข (๐ โ ยฌ ๐ต โ ๐ด) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โ) & โข (๐ = ๐ต โ ๐ถ = ๐ท) & โข (๐ โ ๐ท โ โ) โ โข (๐ โ โ๐ โ (๐ด โช {๐ต})๐ถ = (โ๐ โ ๐ด ๐ถ ยท ๐ท)) | ||
Theorem | fprodsplit1f 15931* | Separate out a term in a finite product. A version of fprodsplit1 44794 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ & โข (๐ โ โฒ๐๐ท) & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข (๐ โ ๐ถ โ ๐ด) & โข ((๐ โง ๐ = ๐ถ) โ ๐ต = ๐ท) โ โข (๐ โ โ๐ โ ๐ด ๐ต = (๐ท ยท โ๐ โ (๐ด โ {๐ถ})๐ต)) | ||
Theorem | fprodn0f 15932* | A finite product of nonzero terms is nonzero. A version of fprodn0 15920 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ 0) โ โข (๐ โ โ๐ โ ๐ด ๐ต โ 0) | ||
Theorem | fprodclf 15933* | Closure of a finite product of complex numbers. A version of fprodcl 15893 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ โ๐ โ ๐ด ๐ต โ โ) | ||
Theorem | fprodge0 15934* | 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 15935* | Any finite product containing a zero term is itself zero. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข (๐ โ ๐ถ โ ๐ด) & โข ((๐ โง ๐ = ๐ถ) โ ๐ต = 0) โ โข (๐ โ โ๐ โ ๐ด ๐ต = 0) | ||
Theorem | fprodge1 15936* | 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 15937* | 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 15938* | 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 15939* | An infinite product equals the value its sequence converges to. (Contributed by Scott Fenton, 18-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ โ๐ โ ๐ โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ)) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = ๐ด) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) & โข (๐ โ seq๐( ยท , ๐น) โ ๐ต) โ โข (๐ โ โ๐ โ ๐ ๐ด = ๐ต) | ||
Theorem | iprodclim2 15940* | A converging product converges to its infinite product. (Contributed by Scott Fenton, 18-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ โ๐ โ ๐ โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ)) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = ๐ด) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) โ โข (๐ โ seq๐( ยท , ๐น) โ โ๐ โ ๐ ๐ด) | ||
Theorem | iprodclim3 15941* | 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 15942* | The product of a non-trivially converging infinite sequence is a complex number. (Contributed by Scott Fenton, 18-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ โ๐ โ ๐ โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ)) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = ๐ด) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) โ โข (๐ โ โ๐ โ ๐ ๐ด โ โ) | ||
Theorem | iprodrecl 15943* | 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 15944* | Multiplication of infinite sums. (Contributed by Scott Fenton, 18-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ โ๐ โ ๐ โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ)) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = ๐ด) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) & โข (๐ โ โ๐ โ ๐ โ๐ง(๐ง โ 0 โง seq๐( ยท , ๐บ) โ ๐ง)) & โข ((๐ โง ๐ โ ๐) โ (๐บโ๐) = ๐ต) & โข ((๐ โง ๐ โ ๐) โ ๐ต โ โ) โ โข (๐ โ โ๐ โ ๐ (๐ด ยท ๐ต) = (โ๐ โ ๐ ๐ด ยท โ๐ โ ๐ ๐ต)) | ||
Syntax | cfallfac 15945 | Declare the syntax for the falling factorial. |
class FallFac | ||
Syntax | crisefac 15946 | Declare the syntax for the rising factorial. |
class RiseFac | ||
Definition | df-risefac 15947* | 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 15948* | 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 15949* | The value of the rising factorial function. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด RiseFac ๐) = โ๐ โ (0...(๐ โ 1))(๐ด + ๐)) | ||
Theorem | fallfacval 15950* | The value of the falling factorial function. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด FallFac ๐) = โ๐ โ (0...(๐ โ 1))(๐ด โ ๐)) | ||
Theorem | risefacval2 15951* | One-based value of rising factorial. (Contributed by Scott Fenton, 15-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด RiseFac ๐) = โ๐ โ (1...๐)(๐ด + (๐ โ 1))) | ||
Theorem | fallfacval2 15952* | One-based value of falling factorial. (Contributed by Scott Fenton, 15-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด FallFac ๐) = โ๐ โ (1...๐)(๐ด โ (๐ โ 1))) | ||
Theorem | fallfacval3 15953* | A product representation of falling factorial when ๐ด is a nonnegative integer. (Contributed by Scott Fenton, 20-Mar-2018.) |
โข (๐ โ (0...๐ด) โ (๐ด FallFac ๐) = โ๐ โ ((๐ด โ (๐ โ 1))...๐ด)๐) | ||
Theorem | risefaccllem 15954* | Lemma for rising factorial closure laws. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ๐ โ โ & โข 1 โ ๐ & โข ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โ (๐ฅ ยท ๐ฆ) โ ๐) & โข ((๐ด โ ๐ โง ๐ โ โ0) โ (๐ด + ๐) โ ๐) โ โข ((๐ด โ ๐ โง ๐ โ โ0) โ (๐ด RiseFac ๐) โ ๐) | ||
Theorem | fallfaccllem 15955* | Lemma for falling factorial closure laws. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ๐ โ โ & โข 1 โ ๐ & โข ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โ (๐ฅ ยท ๐ฆ) โ ๐) & โข ((๐ด โ ๐ โง ๐ โ โ0) โ (๐ด โ ๐) โ ๐) โ โข ((๐ด โ ๐ โง ๐ โ โ0) โ (๐ด FallFac ๐) โ ๐) | ||
Theorem | risefaccl 15956 | Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด RiseFac ๐) โ โ) | ||
Theorem | fallfaccl 15957 | Closure law for falling factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด FallFac ๐) โ โ) | ||
Theorem | rerisefaccl 15958 | Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด RiseFac ๐) โ โ) | ||
Theorem | refallfaccl 15959 | Closure law for falling factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด FallFac ๐) โ โ) | ||
Theorem | nnrisefaccl 15960 | Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด RiseFac ๐) โ โ) | ||
Theorem | zrisefaccl 15961 | Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โค โง ๐ โ โ0) โ (๐ด RiseFac ๐) โ โค) | ||
Theorem | zfallfaccl 15962 | Closure law for falling factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โค โง ๐ โ โ0) โ (๐ด FallFac ๐) โ โค) | ||
Theorem | nn0risefaccl 15963 | Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ0 โง ๐ โ โ0) โ (๐ด RiseFac ๐) โ โ0) | ||
Theorem | rprisefaccl 15964 | Closure law for rising factorial. (Contributed by Scott Fenton, 9-Jan-2018.) |
โข ((๐ด โ โ+ โง ๐ โ โ0) โ (๐ด RiseFac ๐) โ โ+) | ||
Theorem | risefallfac 15965 | A relationship between rising and falling factorials. (Contributed by Scott Fenton, 15-Jan-2018.) |
โข ((๐ โ โ โง ๐ โ โ0) โ (๐ RiseFac ๐) = ((-1โ๐) ยท (-๐ FallFac ๐))) | ||
Theorem | fallrisefac 15966 | A relationship between falling and rising factorials. (Contributed by Scott Fenton, 17-Jan-2018.) |
โข ((๐ โ โ โง ๐ โ โ0) โ (๐ FallFac ๐) = ((-1โ๐) ยท (-๐ RiseFac ๐))) | ||
Theorem | risefall0lem 15967 | Lemma for risefac0 15968 and fallfac0 15969. Show a particular set of finite integers is empty. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข (0...(0 โ 1)) = โ | ||
Theorem | risefac0 15968 | The value of the rising factorial when ๐ = 0. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข (๐ด โ โ โ (๐ด RiseFac 0) = 1) | ||
Theorem | fallfac0 15969 | The value of the falling factorial when ๐ = 0. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข (๐ด โ โ โ (๐ด FallFac 0) = 1) | ||
Theorem | risefacp1 15970 | The value of the rising factorial at a successor. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด RiseFac (๐ + 1)) = ((๐ด RiseFac ๐) ยท (๐ด + ๐))) | ||
Theorem | fallfacp1 15971 | The value of the falling factorial at a successor. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด FallFac (๐ + 1)) = ((๐ด FallFac ๐) ยท (๐ด โ ๐))) | ||
Theorem | risefacp1d 15972 | The value of the rising factorial at a successor. (Contributed by Scott Fenton, 19-Mar-2018.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ โ โ0) โ โข (๐ โ (๐ด RiseFac (๐ + 1)) = ((๐ด RiseFac ๐) ยท (๐ด + ๐))) | ||
Theorem | fallfacp1d 15973 | The value of the falling factorial at a successor. (Contributed by Scott Fenton, 19-Mar-2018.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ โ โ0) โ โข (๐ โ (๐ด FallFac (๐ + 1)) = ((๐ด FallFac ๐) ยท (๐ด โ ๐))) | ||
Theorem | risefac1 15974 | The value of rising factorial at one. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข (๐ด โ โ โ (๐ด RiseFac 1) = ๐ด) | ||
Theorem | fallfac1 15975 | The value of falling factorial at one. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข (๐ด โ โ โ (๐ด FallFac 1) = ๐ด) | ||
Theorem | risefacfac 15976 | Relate rising factorial to factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข (๐ โ โ0 โ (1 RiseFac ๐) = (!โ๐)) | ||
Theorem | fallfacfwd 15977 | The forward difference of a falling factorial. (Contributed by Scott Fenton, 21-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ) โ (((๐ด + 1) FallFac ๐) โ (๐ด FallFac ๐)) = (๐ ยท (๐ด FallFac (๐ โ 1)))) | ||
Theorem | 0fallfac 15978 | The value of the zero falling factorial at natural ๐. (Contributed by Scott Fenton, 17-Feb-2018.) |
โข (๐ โ โ โ (0 FallFac ๐) = 0) | ||
Theorem | 0risefac 15979 | The value of the zero rising factorial at natural ๐. (Contributed by Scott Fenton, 17-Feb-2018.) |
โข (๐ โ โ โ (0 RiseFac ๐) = 0) | ||
Theorem | binomfallfaclem1 15980 | Lemma for binomfallfac 15982. Closure law. (Contributed by Scott Fenton, 13-Mar-2018.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ โ โ0) โ โข ((๐ โง ๐พ โ (0...๐)) โ ((๐C๐พ) ยท ((๐ด FallFac (๐ โ ๐พ)) ยท (๐ต FallFac (๐พ + 1)))) โ โ) | ||
Theorem | binomfallfaclem2 15981* | Lemma for binomfallfac 15982. 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 15982* | 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 15983* | 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 15984 | Represent the falling factorial via factorials when the first argument is a natural. (Contributed by Scott Fenton, 20-Mar-2018.) |
โข (๐ โ (0...๐ด) โ (๐ด FallFac ๐) = ((!โ๐ด) / (!โ(๐ด โ ๐)))) | ||
Theorem | bcfallfac 15985 | Binomial coefficient in terms of falling factorials. (Contributed by Scott Fenton, 20-Mar-2018.) |
โข (๐พ โ (0...๐) โ (๐C๐พ) = ((๐ FallFac ๐พ) / (!โ๐พ))) | ||
Theorem | fallfacfac 15986 | Relate falling factorial to factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข (๐ โ โ0 โ (๐ FallFac ๐) = (!โ๐)) | ||
Syntax | cbp 15987 | Declare the constant for the Bernoulli polynomial operator. |
class BernPoly | ||
Definition | df-bpoly 15988* | 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 15989* | Lemma for bpolyval 15990. (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 15990* | The value of the Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014.) |
โข ((๐ โ โ0 โง ๐ โ โ) โ (๐ BernPoly ๐) = ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))))) | ||
Theorem | bpoly0 15991 | The value of the Bernoulli polynomials at zero. (Contributed by Scott Fenton, 16-May-2014.) |
โข (๐ โ โ โ (0 BernPoly ๐) = 1) | ||
Theorem | bpoly1 15992 | The value of the Bernoulli polynomials at one. (Contributed by Scott Fenton, 16-May-2014.) |
โข (๐ โ โ โ (1 BernPoly ๐) = (๐ โ (1 / 2))) | ||
Theorem | bpolycl 15993 | Closure law for Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014.) (Proof shortened by Mario Carneiro, 22-May-2014.) |
โข ((๐ โ โ0 โง ๐ โ โ) โ (๐ BernPoly ๐) โ โ) | ||
Theorem | bpolysum 15994* | A sum for Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014.) (Proof shortened by Mario Carneiro, 22-May-2014.) |
โข ((๐ โ โ0 โง ๐ โ โ) โ ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))) = (๐โ๐)) | ||
Theorem | bpolydiflem 15995* | Lemma for bpolydif 15996. (Contributed by Scott Fenton, 12-Jun-2014.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ โ) & โข ((๐ โง ๐ โ (1...(๐ โ 1))) โ ((๐ BernPoly (๐ + 1)) โ (๐ BernPoly ๐)) = (๐ ยท (๐โ(๐ โ 1)))) โ โข (๐ โ ((๐ BernPoly (๐ + 1)) โ (๐ BernPoly ๐)) = (๐ ยท (๐โ(๐ โ 1)))) | ||
Theorem | bpolydif 15996 | Calculate the difference between successive values of the Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014.) (Proof shortened by Mario Carneiro, 26-May-2014.) |
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ BernPoly (๐ + 1)) โ (๐ BernPoly ๐)) = (๐ ยท (๐โ(๐ โ 1)))) | ||
Theorem | fsumkthpow 15997* | A closed-form expression for the sum of ๐พ-th powers. (Contributed by Scott Fenton, 16-May-2014.) This is Metamath 100 proof #77. (Revised by Mario Carneiro, 16-Jun-2014.) |
โข ((๐พ โ โ0 โง ๐ โ โ0) โ ฮฃ๐ โ (0...๐)(๐โ๐พ) = ((((๐พ + 1) BernPoly (๐ + 1)) โ ((๐พ + 1) BernPoly 0)) / (๐พ + 1))) | ||
Theorem | bpoly2 15998 | The Bernoulli polynomials at two. (Contributed by Scott Fenton, 8-Jul-2015.) |
โข (๐ โ โ โ (2 BernPoly ๐) = (((๐โ2) โ ๐) + (1 / 6))) | ||
Theorem | bpoly3 15999 | The Bernoulli polynomials at three. (Contributed by Scott Fenton, 8-Jul-2015.) |
โข (๐ โ โ โ (3 BernPoly ๐) = (((๐โ3) โ ((3 / 2) ยท (๐โ2))) + ((1 / 2) ยท ๐))) | ||
Theorem | bpoly4 16000 | The Bernoulli polynomials at four. (Contributed by Scott Fenton, 8-Jul-2015.) |
โข (๐ โ โ โ (4 BernPoly ๐) = ((((๐โ4) โ (2 ยท (๐โ3))) + (๐โ2)) โ (1 / ;30))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |