Theorem prodfclim1

Description: The constant one product converges to one. (Contributed by Scott Fenton, 5-Dec-2017)

	Ref	Expression
Hypothesis	prodf1.1	|- Z = ( ZZ>= ` M )
Assertion	prodfclim1	|- ( M e. ZZ -> seq M ( x. , ( Z X. { 1 } ) ) ~~> 1 )

Proof

Step	Hyp	Ref	Expression
1		prodf1.1	|- Z = ( ZZ>= ` M )
2	1	prodf1f	|- ( M e. ZZ -> seq M ( x. , ( Z X. { 1 } ) ) = ( Z X. { 1 } ) )
3		ax-1cn	|- 1 e. CC
4	1	eqimss2i	|- ( ZZ>= ` M ) C_ Z
5	1	fvexi	|- Z e. _V
6	4 5	climconst2	|- ( ( 1 e. CC /\ M e. ZZ ) -> ( Z X. { 1 } ) ~~> 1 )
7	3 6	mpan	|- ( M e. ZZ -> ( Z X. { 1 } ) ~~> 1 )
8	2 7	eqbrtrd	|- ( M e. ZZ -> seq M ( x. , ( Z X. { 1 } ) ) ~~> 1 )