Theorem fprod1

Description: A finite product of only one term is the term itself. (Contributed by Scott Fenton, 14-Dec-2017)

	Ref	Expression
Hypothesis	prodsn.1	|- ( k = M -> A = B )
Assertion	fprod1	|- ( ( M e. ZZ /\ B e. CC ) -> prod_ k e. ( M ... M ) A = B )

Proof

Step	Hyp	Ref	Expression
1		prodsn.1	|- ( k = M -> A = B )
2		fzsn	|- ( M e. ZZ -> ( M ... M ) = { M } )
3	2	prodeq1d	|- ( M e. ZZ -> prod_ k e. ( M ... M ) A = prod_ k e. { M } A )
4	3	adantr	|- ( ( M e. ZZ /\ B e. CC ) -> prod_ k e. ( M ... M ) A = prod_ k e. { M } A )
5	1	prodsn	|- ( ( M e. ZZ /\ B e. CC ) -> prod_ k e. { M } A = B )
6	4 5	eqtrd	|- ( ( M e. ZZ /\ B e. CC ) -> prod_ k e. ( M ... M ) A = B )