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	⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐵 )
Assertion	fprod1	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐵 ∈ ℂ ) → ∏ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		prodsn.1	⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐵 )
2		fzsn	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
3	2	prodeq1d	⊢ ( 𝑀 ∈ ℤ → ∏ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐴 = ∏ 𝑘 ∈ { 𝑀 } 𝐴 )
4	3	adantr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐵 ∈ ℂ ) → ∏ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐴 = ∏ 𝑘 ∈ { 𝑀 } 𝐴 )
5	1	prodsn	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐵 ∈ ℂ ) → ∏ 𝑘 ∈ { 𝑀 } 𝐴 = 𝐵 )
6	4 5	eqtrd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐵 ∈ ℂ ) → ∏ 𝑘 ∈ ( 𝑀 ... 𝑀 ) 𝐴 = 𝐵 )