P. 148 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 14701-14800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fprodp1s 14701*	Multiply in the last term in a finite product. (Contributed by Scott Fenton, 27-Dec-2017.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... ( N + 1 ) ) ) -> A e. CC )   =>    |- ( ph -> prod_ k e. ( M ... ( N + 1 ) ) A = ( prod_ k e. ( M ... N ) A x. [_ ( N + 1 ) / k ]_ A ) )
Theorem	prodsns 14702*	A product of the singleton is the term. (Contributed by Scott Fenton, 25-Dec-2017.)
|- ( ( M e. V /\ [_ M / k ]_ A e. CC ) -> prod_ k e. { M } A = [_ M / k ]_ A )
Theorem	fprodfac 14703*	Factorial using product notation. (Contributed by Scott Fenton, 15-Dec-2017.)
|- ( A e. NN0 -> ( ! ` A ) = prod_ k e. ( 1 ... A ) k )
Theorem	fprodabs 14704*	The absolute value of a finite product. (Contributed by Scott Fenton, 25-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ( ph /\ k e. Z ) -> A e. CC )   =>    |- ( ph -> ( abs ` prod_ k e. ( M ... N ) A ) = prod_ k e. ( M ... N ) ( abs ` A ) )
Theorem	fprodeq0 14705*	Anything finite product containing a zero term is itself zero. (Contributed by Scott Fenton, 27-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   &    |- ( ( ph /\ k e. Z ) -> A e. CC )   &    |- ( ( ph /\ k = N ) -> A = 0 )   =>    |- ( ( ph /\ K e. ( ZZ>= ` N ) ) -> prod_ k e. ( M ... K ) A = 0 )
Theorem	fprodshft 14706*	Shift the index of a finite product. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ph -> K e. ZZ )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ( ph /\ j e. ( M ... N ) ) -> A e. CC )   &    |- ( j = ( k - K ) -> A = B )   =>    |- ( ph -> prod_ j e. ( M ... N ) A = prod_ k e. ( ( M + K ) ... ( N + K ) ) B )
Theorem	fprodrev 14707*	Reversal of a finite product. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ph -> K e. ZZ )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ( ph /\ j e. ( M ... N ) ) -> A e. CC )   &    |- ( j = ( K - k ) -> A = B )   =>    |- ( ph -> prod_ j e. ( M ... N ) A = prod_ k e. ( ( K - N ) ... ( K - M ) ) B )
Theorem	fprodconst 14708*	The product of constant terms ( k is not free in B.) (Contributed by Scott Fenton, 12-Jan-2018.)
|- ( ( A e. Fin /\ B e. CC ) -> prod_ k e. A B = ( B ^ ( # ` A ) ) )
Theorem	fprodn0 14709*	A finite product of nonzero terms is nonzero. (Contributed by Scott Fenton, 15-Jan-2018.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ( ph /\ k e. A ) -> B =/= 0 )   =>    |- ( ph -> prod_ k e. A B =/= 0 )
Theorem	fprod2dlem 14710*	Lemma for fprod2d 14711- induction step. (Contributed by Scott Fenton, 30-Jan-2018.)
|- ( z = <. j , k >. -> D = C )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ j e. A ) -> B e. Fin )   &    |- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )   &    |- ( ph -> -. y e. x )   &    |- ( ph -> ( x u. { y } ) C_ A )   &    |- ( ps <-> prod_ j e. x prod_ k e. B C = prod_ z e. U_ j e. x ( { j } X. B ) D )   =>    |- ( ( ph /\ ps ) -> prod_ j e. ( x u. { y } ) prod_ k e. B C = prod_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D )
Theorem	fprod2d 14711*	Write a double product as a product over a two-dimensional region. Compare fsum2d 14502. (Contributed by Scott Fenton, 30-Jan-2018.)
|- ( z = <. j , k >. -> D = C )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ j e. A ) -> B e. Fin )   &    |- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )   =>    |- ( ph -> prod_ j e. A prod_ k e. B C = prod_ z e. U_ j e. A ( { j } X. B ) D )
Theorem	fprodxp 14712*	Combine two products into a single product over the cartesian product. (Contributed by Scott Fenton, 1-Feb-2018.)
|- ( z = <. j , k >. -> D = C )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> B e. Fin )   &    |- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )   =>    |- ( ph -> prod_ j e. A prod_ k e. B C = prod_ z e. ( A X. B ) D )
Theorem	fprodcnv 14713*	Transform a product region using the converse operation. (Contributed by Scott Fenton, 1-Feb-2018.)
|- ( x = <. j , k >. -> B = D )   &    |- ( y = <. k , j >. -> C = D )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> Rel A )   &    |- ( ( ph /\ x e. A ) -> B e. CC )   =>    |- ( ph -> prod_ x e. A B = prod_ y e. `' A C )
Theorem	fprodcom2 14714*	Interchange order of multiplication. Note that B ( j ) and D ( k ) are not necessarily constant expressions. (Contributed by Scott Fenton, 1-Feb-2018.) (Proof shortened by JJ, 2-Aug-2021.)
|- ( ph -> A e. Fin )   &    |- ( ph -> C e. Fin )   &    |- ( ( ph /\ j e. A ) -> B e. Fin )   &    |- ( ph -> ( ( j e. A /\ k e. B ) <-> ( k e. C /\ j e. D ) ) )   &    |- ( ( ph /\ ( j e. A /\ k e. B ) ) -> E e. CC )   =>    |- ( ph -> prod_ j e. A prod_ k e. B E = prod_ k e. C prod_ j e. D E )
Theorem	fprodcom2OLD 14715*	Obsolete proof of fprodcom2 14714 as of 2-Aug-2021. (Contributed by Scott Fenton, 1-Feb-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> A e. Fin )   &    |- ( ph -> C e. Fin )   &    |- ( ( ph /\ j e. A ) -> B e. Fin )   &    |- ( ph -> ( ( j e. A /\ k e. B ) <-> ( k e. C /\ j e. D ) ) )   &    |- ( ( ph /\ ( j e. A /\ k e. B ) ) -> E e. CC )   =>    |- ( ph -> prod_ j e. A prod_ k e. B E = prod_ k e. C prod_ j e. D E )
Theorem	fprodcom 14716*	Interchange product order. (Contributed by Scott Fenton, 2-Feb-2018.)
|- ( ph -> A e. Fin )   &    |- ( ph -> B e. Fin )   &    |- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )   =>    |- ( ph -> prod_ j e. A prod_ k e. B C = prod_ k e. B prod_ j e. A C )
Theorem	fprod0diag 14717*	Two ways to express "the product of A ( j , k ) over the triangular region M <_ j, M <_ k, j + k <_ N. Compare fsum0diag 14509. (Contributed by Scott Fenton, 2-Feb-2018.)
|- ( ( ph /\ ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) ) -> A e. CC )   =>    |- ( ph -> prod_ j e. ( 0 ... N ) prod_ k e. ( 0 ... ( N - j ) ) A = prod_ k e. ( 0 ... N ) prod_ j e. ( 0 ... ( N - k ) ) A )
Theorem	fproddivf 14718*	The quotient of two finite products. A version of fproddiv 14691 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ( ph /\ k e. A ) -> C e. CC )   &    |- ( ( ph /\ k e. A ) -> C =/= 0 )   =>    |- ( ph -> prod_ k e. A ( B / C ) = ( prod_ k e. A B / prod_ k e. A C ) )
Theorem	fprodsplitf 14719*	Split a finite product into two parts. A version of fprodsplit 14696 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- ( ph -> ( A i^i B ) = (/) )   &    |- ( ph -> U = ( A u. B ) )   &    |- ( ph -> U e. Fin )   &    |- ( ( ph /\ k e. U ) -> C e. CC )   =>    |- ( ph -> prod_ k e. U C = ( prod_ k e. A C x. prod_ k e. B C ) )
Theorem	fprodsplitsn 14720*	Separate out a term in a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- F/_ k D   &    |- ( ph -> A e. Fin )   &    |- ( ph -> B e. V )   &    |- ( ph -> -. B e. A )   &    |- ( ( ph /\ k e. A ) -> C e. CC )   &    |- ( k = B -> C = D )   &    |- ( ph -> D e. CC )   =>    |- ( ph -> prod_ k e. ( A u. { B } ) C = ( prod_ k e. A C x. D ) )
Theorem	fprodsplit1f 14721*	Separate out a term in a finite product. A version of fprodsplit1 39825 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- ( ph -> F/_ k D )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ph -> C e. A )   &    |- ( ( ph /\ k = C ) -> B = D )   =>    |- ( ph -> prod_ k e. A B = ( D x. prod_ k e. ( A \ { C } ) B ) )
Theorem	fprodn0f 14722*	A finite product of nonzero terms is nonzero. A version of fprodn0 14709 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ( ph /\ k e. A ) -> B =/= 0 )   =>    |- ( ph -> prod_ k e. A B =/= 0 )
Theorem	fprodclf 14723*	Closure of a finite product of complex numbers. A version of fprodcl 14682 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   =>    |- ( ph -> prod_ k e. A B e. CC )
Theorem	fprodge0 14724*	If all the terms of a finite product are nonnegative, so is the product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. RR )   &    |- ( ( ph /\ k e. A ) -> 0 <_ B )   =>    |- ( ph -> 0 <_ prod_ k e. A B )
Theorem	fprodeq0g 14725*	Any finite product containing a zero term is itself zero. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ph -> C e. A )   &    |- ( ( ph /\ k = C ) -> B = 0 )   =>    |- ( ph -> prod_ k e. A B = 0 )
Theorem	fprodge1 14726*	If all of the terms of a finite product are larger or equal to 1, so is the product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. RR )   &    |- ( ( ph /\ k e. A ) -> 1 <_ B )   =>    |- ( ph -> 1 <_ prod_ k e. A B )
Theorem	fprodle 14727*	If all the terms of two finite products are nonnegative and compare, so do the two products. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. RR )   &    |- ( ( ph /\ k e. A ) -> 0 <_ B )   &    |- ( ( ph /\ k e. A ) -> C e. RR )   &    |- ( ( ph /\ k e. A ) -> B <_ C )   =>    |- ( ph -> prod_ k e. A B <_ prod_ k e. A C )
Theorem	fprodmodd 14728*	If all factors of two finite products are equal modulo M, the products are equal modulo M. (Contributed by AV, 7-Jul-2021.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. ZZ )   &    |- ( ( ph /\ k e. A ) -> C e. ZZ )   &    |- ( ph -> M e. NN )   &    |- ( ( ph /\ k e. A ) -> ( B mod M ) = ( C mod M ) )   =>    |- ( ph -> ( prod_ k e. A B mod M ) = ( prod_ k e. A C mod M ) )
5.10.12.5  Infinite products
Theorem	iprodclim 14729*	An infinite product equals the value its sequence converges to. (Contributed by Scott Fenton, 18-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ( ph /\ k e. Z ) -> A e. CC )   &    |- ( ph -> seq M ( x. , F ) ~~> B )   =>    |- ( ph -> prod_ k e. Z A = B )
Theorem	iprodclim2 14730*	A converging product converges to its infinite product. (Contributed by Scott Fenton, 18-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ( ph /\ k e. Z ) -> A e. CC )   =>    |- ( ph -> seq M ( x. , F ) ~~> prod_ k e. Z A )
Theorem	iprodclim3 14731*	The sequence of partial finite product of a converging infinite product converge to the infinite product of the series. Note that j must not occur in A. (Contributed by Scott Fenton, 18-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , ( k e. Z |-> A ) ) ~~> y ) )   &    |- ( ph -> F e. dom ~~> )   &    |- ( ( ph /\ k e. Z ) -> A e. CC )   &    |- ( ( ph /\ j e. Z ) -> ( F ` j ) = prod_ k e. ( M ... j ) A )   =>    |- ( ph -> F ~~> prod_ k e. Z A )
Theorem	iprodcl 14732*	The product of a non-trivially converging infinite sequence is a complex number. (Contributed by Scott Fenton, 18-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ( ph /\ k e. Z ) -> A e. CC )   =>    |- ( ph -> prod_ k e. Z A e. CC )
Theorem	iprodrecl 14733*	The product of a non-trivially converging infinite real sequence is a real number. (Contributed by Scott Fenton, 18-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ( ph /\ k e. Z ) -> A e. RR )   =>    |- ( ph -> prod_ k e. Z A e. RR )
Theorem	iprodmul 14734*	Multiplication of infinite sums. (Contributed by Scott Fenton, 18-Dec-2017.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ( ph /\ k e. Z ) -> A e. CC )   &    |- ( ph -> E. m e. Z E. z ( z =/= 0 /\ seq m ( x. , G ) ~~> z ) )   &    |- ( ( ph /\ k e. Z ) -> ( G ` k ) = B )   &    |- ( ( ph /\ k e. Z ) -> B e. CC )   =>    |- ( ph -> prod_ k e. Z ( A x. B ) = ( prod_ k e. Z A x. prod_ k e. Z B ) )
5.10.13  Falling and Rising Factorial
Syntax	cfallfac 14735	Declare the syntax for the falling factorial.
class FallFac
Syntax	crisefac 14736	Declare the syntax for the rising factorial.
class RiseFac
Definition	df-risefac 14737*	Define the rising factorial function. This is the function ( A x. ( A + 1 ) x. ... ( A + N ) ) for complex A and nonnegative integers N. (Contributed by Scott Fenton, 5-Jan-2018.)
|- RiseFac = ( x e. CC , n e. NN0 |-> prod_ k e. ( 0 ... ( n - 1 ) ) ( x + k ) )
Definition	df-fallfac 14738*	Define the falling factorial function. This is the function ( A x. ( A - 1 ) x. ... ( A - N ) ) for complex A and nonnegative integers N. (Contributed by Scott Fenton, 5-Jan-2018.)
|- FallFac = ( x e. CC , n e. NN0 |-> prod_ k e. ( 0 ... ( n - 1 ) ) ( x - k ) )
Theorem	risefacval 14739*	The value of the rising factorial function. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( A RiseFac N ) = prod_ k e. ( 0 ... ( N - 1 ) ) ( A + k ) )
Theorem	fallfacval 14740*	The value of the falling factorial function. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( A FallFac N ) = prod_ k e. ( 0 ... ( N - 1 ) ) ( A - k ) )
Theorem	risefacval2 14741*	One-based value of rising factorial. (Contributed by Scott Fenton, 15-Jan-2018.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( A RiseFac N ) = prod_ k e. ( 1 ... N ) ( A + ( k - 1 ) ) )
Theorem	fallfacval2 14742*	One-based value of falling factorial. (Contributed by Scott Fenton, 15-Jan-2018.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( A FallFac N ) = prod_ k e. ( 1 ... N ) ( A - ( k - 1 ) ) )
Theorem	fallfacval3 14743*	A product representation of falling factorial when A is a nonnegative integer. (Contributed by Scott Fenton, 20-Mar-2018.)
|- ( N e. ( 0 ... A ) -> ( A FallFac N ) = prod_ k e. ( ( A - ( N - 1 ) ) ... A ) k )
Theorem	risefaccllem 14744*	Lemma for rising factorial closure laws. (Contributed by Scott Fenton, 5-Jan-2018.)
|- S C_ CC   &    |- 1 e. S   &    |- ( ( x e. S /\ y e. S ) -> ( x x. y ) e. S )   &    |- ( ( A e. S /\ k e. NN0 ) -> ( A + k ) e. S )   =>    |- ( ( A e. S /\ N e. NN0 ) -> ( A RiseFac N ) e. S )
Theorem	fallfaccllem 14745*	Lemma for falling factorial closure laws. (Contributed by Scott Fenton, 5-Jan-2018.)
|- S C_ CC   &    |- 1 e. S   &    |- ( ( x e. S /\ y e. S ) -> ( x x. y ) e. S )   &    |- ( ( A e. S /\ k e. NN0 ) -> ( A - k ) e. S )   =>    |- ( ( A e. S /\ N e. NN0 ) -> ( A FallFac N ) e. S )
Theorem	risefaccl 14746	Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( A RiseFac N ) e. CC )
Theorem	fallfaccl 14747	Closure law for falling factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( A FallFac N ) e. CC )
Theorem	rerisefaccl 14748	Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ( A e. RR /\ N e. NN0 ) -> ( A RiseFac N ) e. RR )
Theorem	refallfaccl 14749	Closure law for falling factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ( A e. RR /\ N e. NN0 ) -> ( A FallFac N ) e. RR )
Theorem	nnrisefaccl 14750	Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ( A e. NN /\ N e. NN0 ) -> ( A RiseFac N ) e. NN )
Theorem	zrisefaccl 14751	Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( A RiseFac N ) e. ZZ )
Theorem	zfallfaccl 14752	Closure law for falling factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( A FallFac N ) e. ZZ )
Theorem	nn0risefaccl 14753	Closure law for rising factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ( A e. NN0 /\ N e. NN0 ) -> ( A RiseFac N ) e. NN0 )
Theorem	rprisefaccl 14754	Closure law for rising factorial. (Contributed by Scott Fenton, 9-Jan-2018.)
|- ( ( A e. RR+ /\ N e. NN0 ) -> ( A RiseFac N ) e. RR+ )
Theorem	risefallfac 14755	A relationship between rising and falling factorials. (Contributed by Scott Fenton, 15-Jan-2018.)
|- ( ( X e. CC /\ N e. NN0 ) -> ( X RiseFac N ) = ( ( -u 1 ^ N ) x. ( -u X FallFac N ) ) )
Theorem	fallrisefac 14756	A relationship between falling and rising factorials. (Contributed by Scott Fenton, 17-Jan-2018.)
|- ( ( X e. CC /\ N e. NN0 ) -> ( X FallFac N ) = ( ( -u 1 ^ N ) x. ( -u X RiseFac N ) ) )
Theorem	risefall0lem 14757	Lemma for risefac0 14758 and fallfac0 14759. Show a particular set of finite integers is empty. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( 0 ... ( 0 - 1 ) ) = (/)
Theorem	risefac0 14758	The value of the rising factorial when N = 0. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( A e. CC -> ( A RiseFac 0 ) = 1 )
Theorem	fallfac0 14759	The value of the falling factorial when N = 0. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( A e. CC -> ( A FallFac 0 ) = 1 )
Theorem	risefacp1 14760	The value of the rising factorial at a successor. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( A RiseFac ( N + 1 ) ) = ( ( A RiseFac N ) x. ( A + N ) ) )
Theorem	fallfacp1 14761	The value of the falling factorial at a successor. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( A FallFac ( N + 1 ) ) = ( ( A FallFac N ) x. ( A - N ) ) )
Theorem	risefacp1d 14762	The value of the rising factorial at a successor. (Contributed by Scott Fenton, 19-Mar-2018.)
|- ( ph -> A e. CC )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( A RiseFac ( N + 1 ) ) = ( ( A RiseFac N ) x. ( A + N ) ) )
Theorem	fallfacp1d 14763	The value of the falling factorial at a successor. (Contributed by Scott Fenton, 19-Mar-2018.)
|- ( ph -> A e. CC )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( A FallFac ( N + 1 ) ) = ( ( A FallFac N ) x. ( A - N ) ) )
Theorem	risefac1 14764	The value of rising factorial at one. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( A e. CC -> ( A RiseFac 1 ) = A )
Theorem	fallfac1 14765	The value of falling factorial at one. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( A e. CC -> ( A FallFac 1 ) = A )
Theorem	risefacfac 14766	Relate rising factorial to factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( N e. NN0 -> ( 1 RiseFac N ) = ( ! ` N ) )
Theorem	fallfacfwd 14767	The forward difference of a falling factorial. (Contributed by Scott Fenton, 21-Jan-2018.)
|- ( ( A e. CC /\ N e. NN ) -> ( ( ( A + 1 ) FallFac N ) - ( A FallFac N ) ) = ( N x. ( A FallFac ( N - 1 ) ) ) )
Theorem	0fallfac 14768	The value of the zero falling factorial at natural N. (Contributed by Scott Fenton, 17-Feb-2018.)
|- ( N e. NN -> ( 0 FallFac N ) = 0 )
Theorem	0risefac 14769	The value of the zero rising factorial at natural N. (Contributed by Scott Fenton, 17-Feb-2018.)
|- ( N e. NN -> ( 0 RiseFac N ) = 0 )
Theorem	binomfallfaclem1 14770	Lemma for binomfallfac 14772. Closure law. (Contributed by Scott Fenton, 13-Mar-2018.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> N e. NN0 )   =>    |- ( ( ph /\ K e. ( 0 ... N ) ) -> ( ( N _C K ) x. ( ( A FallFac ( N - K ) ) x. ( B FallFac ( K + 1 ) ) ) ) e. CC )
Theorem	binomfallfaclem2 14771*	Lemma for binomfallfac 14772. Inductive step. (Contributed by Scott Fenton, 13-Mar-2018.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> N e. NN0 )   &    |- ( ps -> ( ( A + B ) FallFac N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) ) )   =>    |- ( ( ph /\ ps ) -> ( ( A + B ) FallFac ( N + 1 ) ) = sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( N + 1 ) _C k ) x. ( ( A FallFac ( ( N + 1 ) - k ) ) x. ( B FallFac k ) ) ) )
Theorem	binomfallfac 14772*	A version of the binomial theorem using falling factorials instead of exponentials. (Contributed by Scott Fenton, 13-Mar-2018.)
|- ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> ( ( A + B ) FallFac N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) ) )
Theorem	binomrisefac 14773*	A version of the binomial theorem using rising factorials instead of exponentials. (Contributed by Scott Fenton, 16-Mar-2018.)
|- ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> ( ( A + B ) RiseFac N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A RiseFac ( N - k ) ) x. ( B RiseFac k ) ) ) )
Theorem	fallfacval4 14774	Represent the falling factorial via factorials when the first argument is a natural. (Contributed by Scott Fenton, 20-Mar-2018.)
|- ( N e. ( 0 ... A ) -> ( A FallFac N ) = ( ( ! ` A ) / ( ! ` ( A - N ) ) ) )
Theorem	bcfallfac 14775	Binomial coefficient in terms of falling factorials. (Contributed by Scott Fenton, 20-Mar-2018.)
|- ( K e. ( 0 ... N ) -> ( N _C K ) = ( ( N FallFac K ) / ( ! ` K ) ) )
Theorem	fallfacfac 14776	Relate falling factorial to factorial. (Contributed by Scott Fenton, 5-Jan-2018.)
|- ( N e. NN0 -> ( N FallFac N ) = ( ! ` N ) )
5.10.14  Bernoulli polynomials and sums of k-th powers
Syntax	cbp 14777	Declare the constant for the Bernoulli polynomial operator.
class BernPoly
Definition	df-bpoly 14778*	Define the Bernoulli polynomials. Here we use well-founded recursion to define the Bernoulli polynomials. This agrees with most textbook definitions, although explicit formulae do exist. (Contributed by Scott Fenton, 22-May-2014.)
|- BernPoly = ( m e. NN0 , x e. CC |-> (wrecs ( < , NN0 , ( g e. _V |-> [_ ( # ` dom g ) / n ]_ ( ( x ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) ) ) ` m ) )
Theorem	bpolylem 14779*	Lemma for bpolyval 14780. (Contributed by Scott Fenton, 22-May-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- G = ( g e. _V |-> [_ ( # ` dom g ) / n ]_ ( ( X ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) )   &    |- F = wrecs ( < , NN0 , G )   =>    |- ( ( N e. NN0 /\ X e. CC ) -> ( N BernPoly X ) = ( ( X ^ N ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) )
Theorem	bpolyval 14780*	The value of the Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014.)
|- ( ( N e. NN0 /\ X e. CC ) -> ( N BernPoly X ) = ( ( X ^ N ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) )
Theorem	bpoly0 14781	The value of the Bernoulli polynomials at zero. (Contributed by Scott Fenton, 16-May-2014.)
|- ( X e. CC -> ( 0 BernPoly X ) = 1 )
Theorem	bpoly1 14782	The value of the Bernoulli polynomials at one. (Contributed by Scott Fenton, 16-May-2014.)
|- ( X e. CC -> ( 1 BernPoly X ) = ( X - ( 1 / 2 ) ) )
Theorem	bpolycl 14783	Closure law for Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014.) (Proof shortened by Mario Carneiro, 22-May-2014.)
|- ( ( N e. NN0 /\ X e. CC ) -> ( N BernPoly X ) e. CC )
Theorem	bpolysum 14784*	A sum for Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014.) (Proof shortened by Mario Carneiro, 22-May-2014.)
|- ( ( N e. NN0 /\ X e. CC ) -> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) = ( X ^ N ) )
Theorem	bpolydiflem 14785*	Lemma for bpolydif 14786. (Contributed by Scott Fenton, 12-Jun-2014.)
|- ( ph -> N e. NN )   &    |- ( ph -> X e. CC )   &    |- ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( k BernPoly ( X + 1 ) ) - ( k BernPoly X ) ) = ( k x. ( X ^ ( k - 1 ) ) ) )   =>    |- ( ph -> ( ( N BernPoly ( X + 1 ) ) - ( N BernPoly X ) ) = ( N x. ( X ^ ( N - 1 ) ) ) )
Theorem	bpolydif 14786	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.)
|- ( ( N e. NN /\ X e. CC ) -> ( ( N BernPoly ( X + 1 ) ) - ( N BernPoly X ) ) = ( N x. ( X ^ ( N - 1 ) ) ) )
Theorem	fsumkthpow 14787*	A closed-form expression for the sum of K-th powers. (Contributed by Scott Fenton, 16-May-2014.) This is Metamath 100 proof #77. (Revised by Mario Carneiro, 16-Jun-2014.)
|- ( ( K e. NN0 /\ M e. NN0 ) -> sum_ n e. ( 0 ... M ) ( n ^ K ) = ( ( ( ( K + 1 ) BernPoly ( M + 1 ) ) - ( ( K + 1 ) BernPoly 0 ) ) / ( K + 1 ) ) )
Theorem	bpoly2 14788	The Bernoulli polynomials at two. (Contributed by Scott Fenton, 8-Jul-2015.)
|- ( X e. CC -> ( 2 BernPoly X ) = ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) )
Theorem	bpoly3 14789	The Bernoulli polynomials at three. (Contributed by Scott Fenton, 8-Jul-2015.)
|- ( X e. CC -> ( 3 BernPoly X ) = ( ( ( X ^ 3 ) - ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) + ( ( 1 / 2 ) x. X ) ) )
Theorem	bpoly4 14790	The Bernoulli polynomials at four. (Contributed by Scott Fenton, 8-Jul-2015.)
|- ( X e. CC -> ( 4 BernPoly X ) = ( ( ( ( X ^ 4 ) - ( 2 x. ( X ^ 3 ) ) ) + ( X ^ 2 ) ) - ( 1 / ; 3 0 ) ) )
Theorem	fsumcube 14791*	Express the sum of cubes in closed terms. (Contributed by Scott Fenton, 16-Jun-2015.)
|- ( T e. NN0 -> sum_ k e. ( 0 ... T ) ( k ^ 3 ) = ( ( ( T ^ 2 ) x. ( ( T + 1 ) ^ 2 ) ) / 4 ) )
5.11  Elementary trigonometry
5.11.1  The exponential, sine, and cosine functions
Syntax	ce 14792	Extend class notation to include the exponential function.
class exp
Syntax	ceu 14793	Extend class notation to include Euler's constant = 2.7182818....
class _e
Syntax	csin 14794	Extend class notation to include the sine function.
class sin
Syntax	ccos 14795	Extend class notation to include the cosine function.
class cos
Syntax	ctan 14796	Extend class notation to include the tangent function.
class tan
Syntax	cpi 14797	Extend class notation to include pi = 3.14159....
class pi
Definition	df-ef 14798*	Define the exponential function. (Contributed by NM, 14-Mar-2005.)
|- exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )
Definition	df-e 14799	Define Euler's constant 2.71828.... (Contributed by NM, 14-Mar-2005.)
|- _e = ( exp ` 1 )
Definition	df-sin 14800	Define the sine function. (Contributed by NM, 14-Mar-2005.)
|- sin = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) )