Theorem fprodp1

Description: Multiply in the last term in a finite product. (Contributed by Scott Fenton, 24-Dec-2017)

	Ref	Expression
Hypotheses	fprodp1.1	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
	fprodp1.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → 𝐴 ∈ ℂ )
	fprodp1.3	⊢ ( 𝑘 = ( 𝑁 + 1 ) → 𝐴 = 𝐵 )
Assertion	fprodp1	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐴 = ( ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 · 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fprodp1.1	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2		fprodp1.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → 𝐴 ∈ ℂ )
3		fprodp1.3	⊢ ( 𝑘 = ( 𝑁 + 1 ) → 𝐴 = 𝐵 )
4		peano2uz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
5	1 4	syl	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
6	5 2 3	fprodm1	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐴 = ( ∏ 𝑘 ∈ ( 𝑀 ... ( ( 𝑁 + 1 ) − 1 ) ) 𝐴 · 𝐵 ) )
7		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
8	1 7	syl	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
9	8	zcnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
10		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
11	9 10	pncand	⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
12	11	oveq2d	⊢ ( 𝜑 → ( 𝑀 ... ( ( 𝑁 + 1 ) − 1 ) ) = ( 𝑀 ... 𝑁 ) )
13	12	prodeq1d	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑀 ... ( ( 𝑁 + 1 ) − 1 ) ) 𝐴 = ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 )
14	13	oveq1d	⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( 𝑀 ... ( ( 𝑁 + 1 ) − 1 ) ) 𝐴 · 𝐵 ) = ( ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 · 𝐵 ) )
15	6 14	eqtrd	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) 𝐴 = ( ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 · 𝐵 ) )