Theorem fprodp1s

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

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

Proof

Step	Hyp	Ref	Expression
1		fprodp1s.1	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
2		fprodp1s.2	$$⊢\left(\phi \wedge k\in \left(M\dots N+1\right)\right)\to A\in ℂ$$
3	2	ralrimiva	$$⊢\phi \to \forall k\in \left(M\dots N+1\right)A\in ℂ$$
4		nfcsb1v	$$⊢\underset{\_}{Ⅎ}k⦋m/k⦌A$$
5	4	nfel1	$$⊢Ⅎk⦋m/k⦌A\in ℂ$$
6		csbeq1a	$$⊢k=m\to A=⦋m/k⦌A$$
7	6	eleq1d	$$⊢k=m\to \left(A\in ℂ\leftrightarrow ⦋m/k⦌A\in ℂ\right)$$
8	5 7	rspc	$$⊢m\in \left(M\dots N+1\right)\to \left(\forall k\in \left(M\dots N+1\right)A\in ℂ\to ⦋m/k⦌A\in ℂ\right)$$
9	3 8	mpan9	$$⊢\left(\phi \wedge m\in \left(M\dots N+1\right)\right)\to ⦋m/k⦌A\in ℂ$$
10		csbeq1	$$⊢m=N+1\to ⦋m/k⦌A=⦋\left(N+1\right)/k⦌A$$
11	1 9 10	fprodp1	$$⊢\phi \to \prod _{m=M}^{N+1}⦋m/k⦌A=\prod _{m=M}^N⦋m/k⦌A⦋\left(N+1\right)/k⦌A$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}mA$$
13	12 4 6	cbvprodi	$$⊢\prod _{k=M}^{N+1}A=\prod _{m=M}^{N+1}⦋m/k⦌A$$
14	12 4 6	cbvprodi	$$⊢\prod _{k=M}^{N}A=\prod _{m=M}^N⦋m/k⦌A$$
15	14	oveq1i	$$⊢\prod _{k=M}^{N}A⦋\left(N+1\right)/k⦌A=\prod _{m=M}^N⦋m/k⦌A⦋\left(N+1\right)/k⦌A$$
16	11 13 15	3eqtr4g	$$⊢\phi \to \prod _{k=M}^{N+1}A=\prod _{k=M}^{N}A⦋\left(N+1\right)/k⦌A$$