Theorem iprod

Description: Series product with an upper integer index set (i.e. an infinite product.) (Contributed by Scott Fenton, 5-Dec-2017)

	Ref	Expression
Hypotheses	zprod.1	|- Z = ( ZZ>= ` M )
	zprod.2	|- ( ph -> M e. ZZ )
	zprod.3	|- ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) )
	iprod.4	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )
	iprod.5	|- ( ( ph /\ k e. Z ) -> B e. CC )
Assertion	iprod	|- ( ph -> prod_ k e. Z B = ( ~~> ` seq M ( x. , F ) ) )

Proof

Step	Hyp	Ref	Expression
1		zprod.1	|- Z = ( ZZ>= ` M )
2		zprod.2	|- ( ph -> M e. ZZ )
3		zprod.3	|- ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) )
4		iprod.4	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )
5		iprod.5	|- ( ( ph /\ k e. Z ) -> B e. CC )
6		ssidd	|- ( ph -> Z C_ Z )
7		iftrue	|- ( k e. Z -> if ( k e. Z , B , 1 ) = B )
8	7	adantl	|- ( ( ph /\ k e. Z ) -> if ( k e. Z , B , 1 ) = B )
9	4 8	eqtr4d	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = if ( k e. Z , B , 1 ) )
10	1 2 3 6 9 5	zprod	|- ( ph -> prod_ k e. Z B = ( ~~> ` seq M ( x. , F ) ) )