Theorem iprodn0

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

	Ref	Expression
Hypotheses	zprodn0.1	|- Z = ( ZZ>= ` M )
	zprodn0.2	|- ( ph -> M e. ZZ )
	zprodn0.3	|- ( ph -> X =/= 0 )
	zprodn0.4	|- ( ph -> seq M ( x. , F ) ~~> X )
	iprodn0.5	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )
	iprodn0.6	|- ( ( ph /\ k e. Z ) -> B e. CC )
Assertion	iprodn0	|- ( ph -> prod_ k e. Z B = X )

Proof

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