Theorem zprodn0

Description: Nonzero series product with index set a subset of the upper integers. (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 )
	zprodn0.5	|- ( ph -> A C_ Z )
	zprodn0.6	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = if ( k e. A , B , 1 ) )
	zprodn0.7	|- ( ( ph /\ k e. A ) -> B e. CC )
Assertion	zprodn0	|- ( ph -> prod_ k e. A 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		zprodn0.5	|- ( ph -> A C_ Z )
6		zprodn0.6	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = if ( k e. A , B , 1 ) )
7		zprodn0.7	|- ( ( ph /\ k e. A ) -> B e. CC )
8	1 2 4 3	ntrivcvgn0	|- ( ph -> E. m e. Z E. x ( x =/= 0 /\ seq m ( x. , F ) ~~> x ) )
9	1 2 8 5 6 7	zprod	|- ( ph -> prod_ k e. A B = ( ~~> ` seq M ( x. , F ) ) )
10		fclim	|- ~~> : dom ~~> --> CC
11		ffun	|- ( ~~> : dom ~~> --> CC -> Fun ~~> )
12	10 11	ax-mp	|- Fun ~~>
13		funbrfv	|- ( Fun ~~> -> ( seq M ( x. , F ) ~~> X -> ( ~~> ` seq M ( x. , F ) ) = X ) )
14	12 4 13	mpsyl	|- ( ph -> ( ~~> ` seq M ( x. , F ) ) = X )
15	9 14	eqtrd	|- ( ph -> prod_ k e. A B = X )