Metamath Proof Explorer

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 \to A = B$
	Assertion	fprod1	$⊢ (M \in ℤ \land B \in ℂ) \to \prod_{k = M}^{M} A = B$

Step	Hyp	Ref	Expression
1		prodsn.1	$⊢ k = M \to A = B$
2		fzsn	$⊢ M \in ℤ \to (M \dots M) = \{M\}$
3	2	prodeq1d	$⊢ M \in ℤ \to \prod_{k = M}^{M} A = \prod_{k \in \{M\}} A$
4	3	adantr	$⊢ (M \in ℤ \land B \in ℂ) \to \prod_{k = M}^{M} A = \prod_{k \in \{M\}} A$
5	1	prodsn	$⊢ (M \in ℤ \land B \in ℂ) \to \prod_{k \in \{M\}} A = B$
6	4 5	eqtrd	$⊢ (M \in ℤ \land B \in ℂ) \to \prod_{k = M}^{M} A = B$