fprodm1s

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

Step	Hyp	Ref	Expression
1		fprodm1s.1	$⊢ φ \to N \in ℤ_{\geq M}$
2		fprodm1s.2	$⊢ (φ \land k \in (M \dots N)) \to A \in ℂ$
3	2	ralrimiva	$⊢ φ \to \forall k \in (M \dots N) A \in ℂ$
4		nfcsb1v	$⊢ \underline{Ⅎ} 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 (A \in ℂ \leftrightarrow ⦋ m / k ⦌ A \in ℂ)$
8	5 7	rspc	$⊢ m \in (M \dots N) \to (\forall k \in (M \dots N) A \in ℂ \to ⦋ m / k ⦌ A \in ℂ)$
9	3 8	mpan9	$⊢ (φ \land m \in (M \dots N)) \to ⦋ m / k ⦌ A \in ℂ$
10		csbeq1	$⊢ m = N \to ⦋ m / k ⦌ A = ⦋ N / k ⦌ A$
11	1 9 10	fprodm1	$⊢ φ \to \prod_{m = M}^{N} ⦋ m / k ⦌ A = \prod_{m = M}^{N - 1} ⦋ m / k ⦌ A ⦋ N / k ⦌ A$
12		nfcv	$⊢ \underline{Ⅎ} m A$
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	$⊢ φ \to \prod_{k = M}^{N} A = \prod_{k = M}^{N - 1} A ⦋ N / k ⦌ A$

Metamath Proof Explorer