Theorem iprodclim2

Description: A converging product converges to its infinite product. (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 )
Assertion	iprodclim2	|- ( ph -> seq M ( x. , F ) ~~> prod_ k e. Z A )

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	4 5	eqeltrd	|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
7	1 3 6	ntrivcvg	|- ( ph -> seq M ( x. , F ) e. dom ~~> )
8		climdm	|- ( seq M ( x. , F ) e. dom ~~> <-> seq M ( x. , F ) ~~> ( ~~> ` seq M ( x. , F ) ) )
9	7 8	sylib	|- ( ph -> seq M ( x. , F ) ~~> ( ~~> ` seq M ( x. , F ) ) )
10	1 2 3 4 5	iprod	|- ( ph -> prod_ k e. Z A = ( ~~> ` seq M ( x. , F ) ) )
11	9 10	breqtrrd	|- ( ph -> seq M ( x. , F ) ~~> prod_ k e. Z A )