Theorem iprodclim

Description: An infinite product equals the value its sequence converges to. (Contributed by Scott Fenton, 18-Dec-2017)

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

Proof

Step	Hyp	Ref	Expression
1		iprodclim.1	|- Z = ( ZZ>= ` M )
2		iprodclim.2	|- ( ph -> M e. ZZ )
3		iprodclim.3	|- ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) )
4		iprodclim.4	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
5		iprodclim.5	|- ( ( ph /\ k e. Z ) -> A e. CC )
6		iprodclim.6	|- ( ph -> seq M ( x. , F ) ~~> B )
7	1 2 3 4 5	iprod	|- ( ph -> prod_ k e. Z A = ( ~~> ` seq M ( x. , F ) ) )
8		fclim	|- ~~> : dom ~~> --> CC
9		ffun	|- ( ~~> : dom ~~> --> CC -> Fun ~~> )
10	8 9	ax-mp	|- Fun ~~>
11		funbrfv	|- ( Fun ~~> -> ( seq M ( x. , F ) ~~> B -> ( ~~> ` seq M ( x. , F ) ) = B ) )
12	10 6 11	mpsyl	|- ( ph -> ( ~~> ` seq M ( x. , F ) ) = B )
13	7 12	eqtrd	|- ( ph -> prod_ k e. Z A = B )