Theorem climprod1

Description: The limit of a product over one. (Contributed by Scott Fenton, 15-Dec-2017)

	Ref	Expression
Hypotheses	climprod1.1	|- Z = ( ZZ>= ` M )
	climprod1.2	|- ( ph -> M e. ZZ )
Assertion	climprod1	|- ( ph -> seq M ( x. , ( Z X. { 1 } ) ) ~~> 1 )

Proof

Step	Hyp	Ref	Expression
1		climprod1.1	|- Z = ( ZZ>= ` M )
2		climprod1.2	|- ( ph -> M e. ZZ )
3	1	prodfclim1	|- ( M e. ZZ -> seq M ( x. , ( Z X. { 1 } ) ) ~~> 1 )
4	2 3	syl	|- ( ph -> seq M ( x. , ( Z X. { 1 } ) ) ~~> 1 )