Theorem fprodp1

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

	Ref	Expression
Hypotheses	fprodp1.1	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
	fprodp1.2	$$⊢\left(\phi \wedge k\in \left(M\dots N+1\right)\right)\to A\in ℂ$$
	fprodp1.3	$$⊢k=N+1\to A=B$$
Assertion	fprodp1	$$⊢\phi \to \prod _{k=M}^{N+1}A=\prod _{k=M}^{N}AB$$

Proof

Step	Hyp	Ref	Expression
1		fprodp1.1	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
2		fprodp1.2	$$⊢\left(\phi \wedge k\in \left(M\dots N+1\right)\right)\to A\in ℂ$$
3		fprodp1.3	$$⊢k=N+1\to A=B$$
4		peano2uz	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N+1\in {\mathbb{Z}}_{\ge M}$$
5	1 4	syl	$$⊢\phi \to N+1\in {\mathbb{Z}}_{\ge M}$$
6	5 2 3	fprodm1	$$⊢\phi \to \prod _{k=M}^{N+1}A=\prod _{k=M}^{N+1-1}AB$$
7		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in \mathbb{Z}$$
8	1 7	syl	$$⊢\phi \to N\in \mathbb{Z}$$
9	8	zcnd	$$⊢\phi \to N\in ℂ$$
10		1cnd	$$⊢\phi \to 1\in ℂ$$
11	9 10	pncand	$$⊢\phi \to N+1-1=N$$
12	11	oveq2d	$$⊢\phi \to \left(M\dots N+1-1\right)=\left(M\dots N\right)$$
13	12	prodeq1d	$$⊢\phi \to \prod _{k=M}^{N+1-1}A=\prod _{k=M}^{N}A$$
14	13	oveq1d	$$⊢\phi \to \prod _{k=M}^{N+1-1}AB=\prod _{k=M}^{N}AB$$
15	6 14	eqtrd	$$⊢\phi \to \prod _{k=M}^{N+1}A=\prod _{k=M}^{N}AB$$