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