Theorem fprodm1s

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

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

Proof

Step	Hyp	Ref	Expression
1		fprodm1s.1	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
2		fprodm1s.2	$$⊢\left(\phi \wedge k\in \left(M\dots N\right)\right)\to A\in ℂ$$
3	2	ralrimiva	$$⊢\phi \to \forall k\in \left(M\dots N\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\right)\to \left(\forall k\in \left(M\dots N\right)A\in ℂ\to ⦋m/k⦌A\in ℂ\right)$$
9	3 8	mpan9	$$⊢\left(\phi \wedge m\in \left(M\dots N\right)\right)\to ⦋m/k⦌A\in ℂ$$
10		csbeq1	$$⊢m=N\to ⦋m/k⦌A=⦋N/k⦌A$$
11	1 9 10	fprodm1	$$⊢\phi \to \prod _{m=M}^N⦋m/k⦌A=\prod _{m=M}^{N-1}⦋m/k⦌A⦋N/k⦌A$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}mA$$
13	12 4 6	cbvprodi	$$⊢\prod _{k=M}^{N}A=\prod _{m=M}^N⦋m/k⦌A$$
14	12 4 6	cbvprodi	$$⊢\prod _{k=M}^{N-1}A=\prod _{m=M}^{N-1}⦋m/k⦌A$$
15	14	oveq1i	$$⊢\prod _{k=M}^{N-1}A⦋N/k⦌A=\prod _{m=M}^{N-1}⦋m/k⦌A⦋N/k⦌A$$
16	11 13 15	3eqtr4g	$$⊢\phi \to \prod _{k=M}^{N}A=\prod _{k=M}^{N-1}A⦋N/k⦌A$$