fprodp1

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

Step	Hyp	Ref	Expression
1		fprodp1.1	$⊢ φ \to N \in ℤ_{\geq M}$
2		fprodp1.2	$⊢ (φ \land k \in (M \dots N + 1)) \to A \in ℂ$
3		fprodp1.3	$⊢ k = N + 1 \to A = B$
4		peano2uz	$⊢ N \in ℤ_{\geq M} \to N + 1 \in ℤ_{\geq M}$
5	1 4	syl	$⊢ φ \to N + 1 \in ℤ_{\geq M}$
6	5 2 3	fprodm1	$⊢ φ \to \prod_{k = M}^{N + 1} A = \prod_{k = M}^{N + 1 - 1} A B$
7		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
8	1 7	syl	$⊢ φ \to N \in ℤ$
9	8	zcnd	$⊢ φ \to N \in ℂ$
10		1cnd	$⊢ φ \to 1 \in ℂ$
11	9 10	pncand	$⊢ φ \to N + 1 - 1 = N$
12	11	oveq2d	$⊢ φ \to (M \dots N + 1 - 1) = (M \dots N)$
13	12	prodeq1d	$⊢ φ \to \prod_{k = M}^{N + 1 - 1} A = \prod_{k = M}^{N} A$
14	13	oveq1d	$⊢ φ \to \prod_{k = M}^{N + 1 - 1} A B = \prod_{k = M}^{N} A B$
15	6 14	eqtrd	$⊢ φ \to \prod_{k = M}^{N + 1} A = \prod_{k = M}^{N} A B$

Metamath Proof Explorer