fprod1p

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

	Ref	Expression
Hypotheses	fprod1p.1	$⊢ φ \to N \in ℤ_{\geq M}$
	fprod1p.2	$⊢ (φ \land k \in (M \dots N)) \to A \in ℂ$
	fprod1p.3	$⊢ k = M \to A = B$
Assertion	fprod1p	$⊢ φ \to \prod_{k = M}^{N} A = B \prod_{k = M + 1}^{N} A$

Proof

Step	Hyp	Ref	Expression
1		fprod1p.1	$⊢ φ \to N \in ℤ_{\geq M}$
2		fprod1p.2	$⊢ (φ \land k \in (M \dots N)) \to A \in ℂ$
3		fprod1p.3	$⊢ k = M \to A = B$
4		eluzfz1	$⊢ N \in ℤ_{\geq M} \to M \in (M \dots N)$
5	1 4	syl	$⊢ φ \to M \in (M \dots N)$
6	5	elfzelzd	$⊢ φ \to M \in ℤ$
7		fzsn	$⊢ M \in ℤ \to (M \dots M) = \{M\}$
8	6 7	syl	$⊢ φ \to (M \dots M) = \{M\}$
9	8	ineq1d	$⊢ φ \to (M \dots M) \cap (M + 1 \dots N) = \{M\} \cap (M + 1 \dots N)$
10	6	zred	$⊢ φ \to M \in ℝ$
11	10	ltp1d	$⊢ φ \to M < M + 1$
12		fzdisj	$⊢ M < M + 1 \to (M \dots M) \cap (M + 1 \dots N) = \emptyset$
13	11 12	syl	$⊢ φ \to (M \dots M) \cap (M + 1 \dots N) = \emptyset$
14	9 13	eqtr3d	$⊢ φ \to \{M\} \cap (M + 1 \dots N) = \emptyset$
15		fzsplit	$⊢ M \in (M \dots N) \to (M \dots N) = (M \dots M) \cup (M + 1 \dots N)$
16	5 15	syl	$⊢ φ \to (M \dots N) = (M \dots M) \cup (M + 1 \dots N)$
17	8	uneq1d	$⊢ φ \to (M \dots M) \cup (M + 1 \dots N) = \{M\} \cup (M + 1 \dots N)$
18	16 17	eqtrd	$⊢ φ \to (M \dots N) = \{M\} \cup (M + 1 \dots N)$
19		fzfid	$⊢ φ \to (M \dots N) \in Fin$
20	14 18 19 2	fprodsplit	$⊢ φ \to \prod_{k = M}^{N} A = \prod_{k \in \{M\}} A \prod_{k = M + 1}^{N} A$
21	3	eleq1d	$⊢ k = M \to (A \in ℂ \leftrightarrow B \in ℂ)$
22	2	ralrimiva	$⊢ φ \to \forall k \in (M \dots N) A \in ℂ$
23	21 22 5	rspcdva	$⊢ φ \to B \in ℂ$
24	3	prodsn	$⊢ (M \in (M \dots N) \land B \in ℂ) \to \prod_{k \in \{M\}} A = B$
25	5 23 24	syl2anc	$⊢ φ \to \prod_{k \in \{M\}} A = B$
26	25	oveq1d	$⊢ φ \to \prod_{k \in \{M\}} A \prod_{k = M + 1}^{N} A = B \prod_{k = M + 1}^{N} A$
27	20 26	eqtrd	$⊢ φ \to \prod_{k = M}^{N} A = B \prod_{k = M + 1}^{N} A$

Metamath Proof Explorer

Theorem fprod1p

Proof