Home | Metamath
Proof Explorer Theorem List (p. 159 of 470) | < 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: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fprodcnv 15801* | Transform a product region using the converse operation. (Contributed by Scott Fenton, 1-Feb-2018.) |
โข (๐ฅ = โจ๐, ๐โฉ โ ๐ต = ๐ท) & โข (๐ฆ = โจ๐, ๐โฉ โ ๐ถ = ๐ท) & โข (๐ โ ๐ด โ Fin) & โข (๐ โ Rel ๐ด) & โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ โ๐ฅ โ ๐ด ๐ต = โ๐ฆ โ โก ๐ด๐ถ) | ||
Theorem | fprodcom2 15802* | 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 15803* | Interchange product order. (Contributed by Scott Fenton, 2-Feb-2018.) |
โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ต โ Fin) & โข ((๐ โง (๐ โ ๐ด โง ๐ โ ๐ต)) โ ๐ถ โ โ) โ โข (๐ โ โ๐ โ ๐ด โ๐ โ ๐ต ๐ถ = โ๐ โ ๐ต โ๐ โ ๐ด ๐ถ) | ||
Theorem | fprod0diag 15804* | Two ways to express "the product of ๐ด(๐, ๐) over the triangular region ๐ โค ๐, ๐ โค ๐, ๐ + ๐ โค ๐. Compare fsum0diag 15597. (Contributed by Scott Fenton, 2-Feb-2018.) |
โข ((๐ โง (๐ โ (0...๐) โง ๐ โ (0...(๐ โ ๐)))) โ ๐ด โ โ) โ โข (๐ โ โ๐ โ (0...๐)โ๐ โ (0...(๐ โ ๐))๐ด = โ๐ โ (0...๐)โ๐ โ (0...(๐ โ ๐))๐ด) | ||
Theorem | fproddivf 15805* | The quotient of two finite products. A version of fproddiv 15779 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ 0) โ โข (๐ โ โ๐ โ ๐ด (๐ต / ๐ถ) = (โ๐ โ ๐ด ๐ต / โ๐ โ ๐ด ๐ถ)) | ||
Theorem | fprodsplitf 15806* | Split a finite product into two parts. A version of fprodsplit 15784 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ & โข (๐ โ (๐ด โฉ ๐ต) = โ ) & โข (๐ โ ๐ = (๐ด โช ๐ต)) & โข (๐ โ ๐ โ Fin) & โข ((๐ โง ๐ โ ๐) โ ๐ถ โ โ) โ โข (๐ โ โ๐ โ ๐ ๐ถ = (โ๐ โ ๐ด ๐ถ ยท โ๐ โ ๐ต ๐ถ)) | ||
Theorem | fprodsplitsn 15807* | Separate out a term in a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ & โข โฒ๐๐ท & โข (๐ โ ๐ด โ Fin) & โข (๐ โ ๐ต โ ๐) & โข (๐ โ ยฌ ๐ต โ ๐ด) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โ) & โข (๐ = ๐ต โ ๐ถ = ๐ท) & โข (๐ โ ๐ท โ โ) โ โข (๐ โ โ๐ โ (๐ด โช {๐ต})๐ถ = (โ๐ โ ๐ด ๐ถ ยท ๐ท)) | ||
Theorem | fprodsplit1f 15808* | Separate out a term in a finite product. A version of fprodsplit1 43556 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ & โข (๐ โ โฒ๐๐ท) & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข (๐ โ ๐ถ โ ๐ด) & โข ((๐ โง ๐ = ๐ถ) โ ๐ต = ๐ท) โ โข (๐ โ โ๐ โ ๐ด ๐ต = (๐ท ยท โ๐ โ (๐ด โ {๐ถ})๐ต)) | ||
Theorem | fprodn0f 15809* | A finite product of nonzero terms is nonzero. A version of fprodn0 15797 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ 0) โ โข (๐ โ โ๐ โ ๐ด ๐ต โ 0) | ||
Theorem | fprodclf 15810* | Closure of a finite product of complex numbers. A version of fprodcl 15770 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) โ โข (๐ โ โ๐ โ ๐ด ๐ต โ โ) | ||
Theorem | fprodge0 15811* | 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 15812* | Any finite product containing a zero term is itself zero. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข โฒ๐๐ & โข (๐ โ ๐ด โ Fin) & โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) & โข (๐ โ ๐ถ โ ๐ด) & โข ((๐ โง ๐ = ๐ถ) โ ๐ต = 0) โ โข (๐ โ โ๐ โ ๐ด ๐ต = 0) | ||
Theorem | fprodge1 15813* | 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 15814* | 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 15815* | 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 15816* | An infinite product equals the value its sequence converges to. (Contributed by Scott Fenton, 18-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ โ๐ โ ๐ โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ)) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = ๐ด) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) & โข (๐ โ seq๐( ยท , ๐น) โ ๐ต) โ โข (๐ โ โ๐ โ ๐ ๐ด = ๐ต) | ||
Theorem | iprodclim2 15817* | A converging product converges to its infinite product. (Contributed by Scott Fenton, 18-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ โ๐ โ ๐ โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ)) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = ๐ด) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) โ โข (๐ โ seq๐( ยท , ๐น) โ โ๐ โ ๐ ๐ด) | ||
Theorem | iprodclim3 15818* | 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 15819* | The product of a non-trivially converging infinite sequence is a complex number. (Contributed by Scott Fenton, 18-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ โ๐ โ ๐ โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ)) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = ๐ด) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) โ โข (๐ โ โ๐ โ ๐ ๐ด โ โ) | ||
Theorem | iprodrecl 15820* | 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 15821* | Multiplication of infinite sums. (Contributed by Scott Fenton, 18-Dec-2017.) |
โข ๐ = (โคโฅโ๐) & โข (๐ โ ๐ โ โค) & โข (๐ โ โ๐ โ ๐ โ๐ฆ(๐ฆ โ 0 โง seq๐( ยท , ๐น) โ ๐ฆ)) & โข ((๐ โง ๐ โ ๐) โ (๐นโ๐) = ๐ด) & โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) & โข (๐ โ โ๐ โ ๐ โ๐ง(๐ง โ 0 โง seq๐( ยท , ๐บ) โ ๐ง)) & โข ((๐ โง ๐ โ ๐) โ (๐บโ๐) = ๐ต) & โข ((๐ โง ๐ โ ๐) โ ๐ต โ โ) โ โข (๐ โ โ๐ โ ๐ (๐ด ยท ๐ต) = (โ๐ โ ๐ ๐ด ยท โ๐ โ ๐ ๐ต)) | ||
Syntax | cfallfac 15822 | Declare the syntax for the falling factorial. |
class FallFac | ||
Syntax | crisefac 15823 | Declare the syntax for the rising factorial. |
class RiseFac | ||
Definition | df-risefac 15824* | 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 15825* | 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 15826* | The value of the rising factorial function. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด RiseFac ๐) = โ๐ โ (0...(๐ โ 1))(๐ด + ๐)) | ||
Theorem | fallfacval 15827* | The value of the falling factorial function. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด FallFac ๐) = โ๐ โ (0...(๐ โ 1))(๐ด โ ๐)) | ||
Theorem | risefacval2 15828* | One-based value of rising factorial. (Contributed by Scott Fenton, 15-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด RiseFac ๐) = โ๐ โ (1...๐)(๐ด + (๐ โ 1))) | ||
Theorem | fallfacval2 15829* | One-based value of falling factorial. (Contributed by Scott Fenton, 15-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด FallFac ๐) = โ๐ โ (1...๐)(๐ด โ (๐ โ 1))) | ||
Theorem | fallfacval3 15830* | A product representation of falling factorial when ๐ด is a nonnegative integer. (Contributed by Scott Fenton, 20-Mar-2018.) |
โข (๐ โ (0...๐ด) โ (๐ด FallFac ๐) = โ๐ โ ((๐ด โ (๐ โ 1))...๐ด)๐) | ||
Theorem | risefaccllem 15831* | Lemma for rising factorial closure laws. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ๐ โ โ & โข 1 โ ๐ & โข ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โ (๐ฅ ยท ๐ฆ) โ ๐) & โข ((๐ด โ ๐ โง ๐ โ โ0) โ (๐ด + ๐) โ ๐) โ โข ((๐ด โ ๐ โง ๐ โ โ0) โ (๐ด RiseFac ๐) โ ๐) | ||
Theorem | fallfaccllem 15832* | Lemma for falling factorial closure laws. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ๐ โ โ & โข 1 โ ๐ & โข ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โ (๐ฅ ยท ๐ฆ) โ ๐) & โข ((๐ด โ ๐ โง ๐ โ โ0) โ (๐ด โ ๐) โ ๐) โ โข ((๐ด โ ๐ โง ๐ โ โ0) โ (๐ด FallFac ๐) โ ๐) | ||
Theorem | risefaccl 15833 | Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด RiseFac ๐) โ โ) | ||
Theorem | fallfaccl 15834 | Closure law for falling factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด FallFac ๐) โ โ) | ||
Theorem | rerisefaccl 15835 | Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด RiseFac ๐) โ โ) | ||
Theorem | refallfaccl 15836 | Closure law for falling factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด FallFac ๐) โ โ) | ||
Theorem | nnrisefaccl 15837 | Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด RiseFac ๐) โ โ) | ||
Theorem | zrisefaccl 15838 | Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โค โง ๐ โ โ0) โ (๐ด RiseFac ๐) โ โค) | ||
Theorem | zfallfaccl 15839 | Closure law for falling factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โค โง ๐ โ โ0) โ (๐ด FallFac ๐) โ โค) | ||
Theorem | nn0risefaccl 15840 | Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ0 โง ๐ โ โ0) โ (๐ด RiseFac ๐) โ โ0) | ||
Theorem | rprisefaccl 15841 | Closure law for rising factorial. (Contributed by Scott Fenton, 9-Jan-2018.) |
โข ((๐ด โ โ+ โง ๐ โ โ0) โ (๐ด RiseFac ๐) โ โ+) | ||
Theorem | risefallfac 15842 | A relationship between rising and falling factorials. (Contributed by Scott Fenton, 15-Jan-2018.) |
โข ((๐ โ โ โง ๐ โ โ0) โ (๐ RiseFac ๐) = ((-1โ๐) ยท (-๐ FallFac ๐))) | ||
Theorem | fallrisefac 15843 | A relationship between falling and rising factorials. (Contributed by Scott Fenton, 17-Jan-2018.) |
โข ((๐ โ โ โง ๐ โ โ0) โ (๐ FallFac ๐) = ((-1โ๐) ยท (-๐ RiseFac ๐))) | ||
Theorem | risefall0lem 15844 | Lemma for risefac0 15845 and fallfac0 15846. Show a particular set of finite integers is empty. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข (0...(0 โ 1)) = โ | ||
Theorem | risefac0 15845 | The value of the rising factorial when ๐ = 0. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข (๐ด โ โ โ (๐ด RiseFac 0) = 1) | ||
Theorem | fallfac0 15846 | The value of the falling factorial when ๐ = 0. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข (๐ด โ โ โ (๐ด FallFac 0) = 1) | ||
Theorem | risefacp1 15847 | The value of the rising factorial at a successor. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด RiseFac (๐ + 1)) = ((๐ด RiseFac ๐) ยท (๐ด + ๐))) | ||
Theorem | fallfacp1 15848 | The value of the falling factorial at a successor. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ0) โ (๐ด FallFac (๐ + 1)) = ((๐ด FallFac ๐) ยท (๐ด โ ๐))) | ||
Theorem | risefacp1d 15849 | The value of the rising factorial at a successor. (Contributed by Scott Fenton, 19-Mar-2018.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ โ โ0) โ โข (๐ โ (๐ด RiseFac (๐ + 1)) = ((๐ด RiseFac ๐) ยท (๐ด + ๐))) | ||
Theorem | fallfacp1d 15850 | The value of the falling factorial at a successor. (Contributed by Scott Fenton, 19-Mar-2018.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ โ โ0) โ โข (๐ โ (๐ด FallFac (๐ + 1)) = ((๐ด FallFac ๐) ยท (๐ด โ ๐))) | ||
Theorem | risefac1 15851 | The value of rising factorial at one. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข (๐ด โ โ โ (๐ด RiseFac 1) = ๐ด) | ||
Theorem | fallfac1 15852 | The value of falling factorial at one. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข (๐ด โ โ โ (๐ด FallFac 1) = ๐ด) | ||
Theorem | risefacfac 15853 | Relate rising factorial to factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข (๐ โ โ0 โ (1 RiseFac ๐) = (!โ๐)) | ||
Theorem | fallfacfwd 15854 | The forward difference of a falling factorial. (Contributed by Scott Fenton, 21-Jan-2018.) |
โข ((๐ด โ โ โง ๐ โ โ) โ (((๐ด + 1) FallFac ๐) โ (๐ด FallFac ๐)) = (๐ ยท (๐ด FallFac (๐ โ 1)))) | ||
Theorem | 0fallfac 15855 | The value of the zero falling factorial at natural ๐. (Contributed by Scott Fenton, 17-Feb-2018.) |
โข (๐ โ โ โ (0 FallFac ๐) = 0) | ||
Theorem | 0risefac 15856 | The value of the zero rising factorial at natural ๐. (Contributed by Scott Fenton, 17-Feb-2018.) |
โข (๐ โ โ โ (0 RiseFac ๐) = 0) | ||
Theorem | binomfallfaclem1 15857 | Lemma for binomfallfac 15859. Closure law. (Contributed by Scott Fenton, 13-Mar-2018.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ โ โ0) โ โข ((๐ โง ๐พ โ (0...๐)) โ ((๐C๐พ) ยท ((๐ด FallFac (๐ โ ๐พ)) ยท (๐ต FallFac (๐พ + 1)))) โ โ) | ||
Theorem | binomfallfaclem2 15858* | Lemma for binomfallfac 15859. 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 15859* | 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 15860* | 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 15861 | Represent the falling factorial via factorials when the first argument is a natural. (Contributed by Scott Fenton, 20-Mar-2018.) |
โข (๐ โ (0...๐ด) โ (๐ด FallFac ๐) = ((!โ๐ด) / (!โ(๐ด โ ๐)))) | ||
Theorem | bcfallfac 15862 | Binomial coefficient in terms of falling factorials. (Contributed by Scott Fenton, 20-Mar-2018.) |
โข (๐พ โ (0...๐) โ (๐C๐พ) = ((๐ FallFac ๐พ) / (!โ๐พ))) | ||
Theorem | fallfacfac 15863 | Relate falling factorial to factorial. (Contributed by Scott Fenton, 5-Jan-2018.) |
โข (๐ โ โ0 โ (๐ FallFac ๐) = (!โ๐)) | ||
Syntax | cbp 15864 | Declare the constant for the Bernoulli polynomial operator. |
class BernPoly | ||
Definition | df-bpoly 15865* | 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 15866* | Lemma for bpolyval 15867. (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 15867* | The value of the Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014.) |
โข ((๐ โ โ0 โง ๐ โ โ) โ (๐ BernPoly ๐) = ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))))) | ||
Theorem | bpoly0 15868 | The value of the Bernoulli polynomials at zero. (Contributed by Scott Fenton, 16-May-2014.) |
โข (๐ โ โ โ (0 BernPoly ๐) = 1) | ||
Theorem | bpoly1 15869 | The value of the Bernoulli polynomials at one. (Contributed by Scott Fenton, 16-May-2014.) |
โข (๐ โ โ โ (1 BernPoly ๐) = (๐ โ (1 / 2))) | ||
Theorem | bpolycl 15870 | Closure law for Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014.) (Proof shortened by Mario Carneiro, 22-May-2014.) |
โข ((๐ โ โ0 โง ๐ โ โ) โ (๐ BernPoly ๐) โ โ) | ||
Theorem | bpolysum 15871* | 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 15872* | Lemma for bpolydif 15873. (Contributed by Scott Fenton, 12-Jun-2014.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ โ) & โข ((๐ โง ๐ โ (1...(๐ โ 1))) โ ((๐ BernPoly (๐ + 1)) โ (๐ BernPoly ๐)) = (๐ ยท (๐โ(๐ โ 1)))) โ โข (๐ โ ((๐ BernPoly (๐ + 1)) โ (๐ BernPoly ๐)) = (๐ ยท (๐โ(๐ โ 1)))) | ||
Theorem | bpolydif 15873 | 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 15874* | 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 15875 | The Bernoulli polynomials at two. (Contributed by Scott Fenton, 8-Jul-2015.) |
โข (๐ โ โ โ (2 BernPoly ๐) = (((๐โ2) โ ๐) + (1 / 6))) | ||
Theorem | bpoly3 15876 | The Bernoulli polynomials at three. (Contributed by Scott Fenton, 8-Jul-2015.) |
โข (๐ โ โ โ (3 BernPoly ๐) = (((๐โ3) โ ((3 / 2) ยท (๐โ2))) + ((1 / 2) ยท ๐))) | ||
Theorem | bpoly4 15877 | The Bernoulli polynomials at four. (Contributed by Scott Fenton, 8-Jul-2015.) |
โข (๐ โ โ โ (4 BernPoly ๐) = ((((๐โ4) โ (2 ยท (๐โ3))) + (๐โ2)) โ (1 / ;30))) | ||
Theorem | fsumcube 15878* | Express the sum of cubes in closed terms. (Contributed by Scott Fenton, 16-Jun-2015.) |
โข (๐ โ โ0 โ ฮฃ๐ โ (0...๐)(๐โ3) = (((๐โ2) ยท ((๐ + 1)โ2)) / 4)) | ||
Syntax | ce 15879 | Extend class notation to include the exponential function. |
class exp | ||
Syntax | ceu 15880 | Extend class notation to include Euler's constant e = 2.71828.... |
class e | ||
Syntax | csin 15881 | Extend class notation to include the sine function. |
class sin | ||
Syntax | ccos 15882 | Extend class notation to include the cosine function. |
class cos | ||
Syntax | ctan 15883 | Extend class notation to include the tangent function. |
class tan | ||
Syntax | cpi 15884 | Extend class notation to include the constant pi, ฯ = 3.14159.... |
class ฯ | ||
Definition | df-ef 15885* | Define the exponential function. Its value at the complex number ๐ด is (expโ๐ด) and is called the "exponential of ๐ด"; see efval 15897. (Contributed by NM, 14-Mar-2005.) |
โข exp = (๐ฅ โ โ โฆ ฮฃ๐ โ โ0 ((๐ฅโ๐) / (!โ๐))) | ||
Definition | df-e 15886 | Define Euler's constant e = 2.71828.... (Contributed by NM, 14-Mar-2005.) |
โข e = (expโ1) | ||
Definition | df-sin 15887 | Define the sine function. (Contributed by NM, 14-Mar-2005.) |
โข sin = (๐ฅ โ โ โฆ (((expโ(i ยท ๐ฅ)) โ (expโ(-i ยท ๐ฅ))) / (2 ยท i))) | ||
Definition | df-cos 15888 | Define the cosine function. (Contributed by NM, 14-Mar-2005.) |
โข cos = (๐ฅ โ โ โฆ (((expโ(i ยท ๐ฅ)) + (expโ(-i ยท ๐ฅ))) / 2)) | ||
Definition | df-tan 15889 | Define the tangent function. We define it this way for cmpt 5187, which requires the form (๐ฅ โ ๐ด โฆ ๐ต). (Contributed by Mario Carneiro, 14-Mar-2014.) |
โข tan = (๐ฅ โ (โกcos โ (โ โ {0})) โฆ ((sinโ๐ฅ) / (cosโ๐ฅ))) | ||
Definition | df-pi 15890 | Define the constant pi, ฯ = 3.14159..., which is the smallest positive number whose sine is zero. Definition of ฯ in [Gleason] p. 311. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by AV, 14-Sep-2020.) |
โข ฯ = inf((โ+ โฉ (โกsin โ {0})), โ, < ) | ||
Theorem | eftcl 15891 | Closure of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 11-Sep-2007.) |
โข ((๐ด โ โ โง ๐พ โ โ0) โ ((๐ดโ๐พ) / (!โ๐พ)) โ โ) | ||
Theorem | reeftcl 15892 | The terms of the series expansion of the exponential function at a real number are real. (Contributed by Paul Chapman, 15-Jan-2008.) |
โข ((๐ด โ โ โง ๐พ โ โ0) โ ((๐ดโ๐พ) / (!โ๐พ)) โ โ) | ||
Theorem | eftabs 15893 | The absolute value of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 23-Nov-2007.) |
โข ((๐ด โ โ โง ๐พ โ โ0) โ (absโ((๐ดโ๐พ) / (!โ๐พ))) = (((absโ๐ด)โ๐พ) / (!โ๐พ))) | ||
Theorem | eftval 15894* | The value of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
โข ๐น = (๐ โ โ0 โฆ ((๐ดโ๐) / (!โ๐))) โ โข (๐ โ โ0 โ (๐นโ๐) = ((๐ดโ๐) / (!โ๐))) | ||
Theorem | efcllem 15895* | Lemma for efcl 15900. The series that defines the exponential function converges, in the case where its argument is nonzero. The ratio test cvgrat 15703 is used to show convergence. (Contributed by NM, 26-Apr-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2014.) (Proof shortened by AV, 9-Jul-2022.) |
โข ๐น = (๐ โ โ0 โฆ ((๐ดโ๐) / (!โ๐))) โ โข (๐ด โ โ โ seq0( + , ๐น) โ dom โ ) | ||
Theorem | ef0lem 15896* | The series defining the exponential function converges in the (trivial) case of a zero argument. (Contributed by Steve Rodriguez, 7-Jun-2006.) (Revised by Mario Carneiro, 28-Apr-2014.) |
โข ๐น = (๐ โ โ0 โฆ ((๐ดโ๐) / (!โ๐))) โ โข (๐ด = 0 โ seq0( + , ๐น) โ 1) | ||
Theorem | efval 15897* | Value of the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.) |
โข (๐ด โ โ โ (expโ๐ด) = ฮฃ๐ โ โ0 ((๐ดโ๐) / (!โ๐))) | ||
Theorem | esum 15898 | Value of Euler's constant e = 2.71828.... (Contributed by Steve Rodriguez, 5-Mar-2006.) |
โข e = ฮฃ๐ โ โ0 (1 / (!โ๐)) | ||
Theorem | eff 15899 | Domain and codomain of the exponential function. (Contributed by Paul Chapman, 22-Oct-2007.) (Proof shortened by Mario Carneiro, 28-Apr-2014.) |
โข exp:โโถโ | ||
Theorem | efcl 15900 | Closure law for the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.) |
โข (๐ด โ โ โ (expโ๐ด) โ โ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |