fprodm1

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

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

Proof

Step	Hyp	Ref	Expression
1		fprodm1.1	$⊢ φ \to N \in ℤ_{\geq M}$
2		fprodm1.2	$⊢ (φ \land k \in (M \dots N)) \to A \in ℂ$
3		fprodm1.3	$⊢ k = N \to A = B$
4		fzp1nel	$⊢ \neg N - 1 + 1 \in (M \dots N - 1)$
5		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
6	1 5	syl	$⊢ φ \to N \in ℤ$
7	6	zcnd	$⊢ φ \to N \in ℂ$
8		1cnd	$⊢ φ \to 1 \in ℂ$
9	7 8	npcand	$⊢ φ \to N - 1 + 1 = N$
10	9	eleq1d	$⊢ φ \to (N - 1 + 1 \in (M \dots N - 1) \leftrightarrow N \in (M \dots N - 1))$
11	4 10	mtbii	$⊢ φ \to \neg N \in (M \dots N - 1)$
12		disjsn	$⊢ (M \dots N - 1) \cap \{N\} = \emptyset \leftrightarrow \neg N \in (M \dots N - 1)$
13	11 12	sylibr	$⊢ φ \to (M \dots N - 1) \cap \{N\} = \emptyset$
14		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
15	1 14	syl	$⊢ φ \to M \in ℤ$
16		peano2zm	$⊢ M \in ℤ \to M - 1 \in ℤ$
17	15 16	syl	$⊢ φ \to M - 1 \in ℤ$
18	15	zcnd	$⊢ φ \to M \in ℂ$
19	18 8	npcand	$⊢ φ \to M - 1 + 1 = M$
20	19	fveq2d	$⊢ φ \to ℤ_{\geq (M - 1 + 1)} = ℤ_{\geq M}$
21	1 20	eleqtrrd	$⊢ φ \to N \in ℤ_{\geq (M - 1 + 1)}$
22		eluzp1m1	$⊢ (M - 1 \in ℤ \land N \in ℤ_{\geq (M - 1 + 1)}) \to N - 1 \in ℤ_{\geq (M - 1)}$
23	17 21 22	syl2anc	$⊢ φ \to N - 1 \in ℤ_{\geq (M - 1)}$
24		fzsuc2	$⊢ (M \in ℤ \land N - 1 \in ℤ_{\geq (M - 1)}) \to (M \dots N - 1 + 1) = (M \dots N - 1) \cup \{N - 1 + 1\}$
25	15 23 24	syl2anc	$⊢ φ \to (M \dots N - 1 + 1) = (M \dots N - 1) \cup \{N - 1 + 1\}$
26	9	oveq2d	$⊢ φ \to (M \dots N - 1 + 1) = (M \dots N)$
27	9	sneqd	$⊢ φ \to \{N - 1 + 1\} = \{N\}$
28	27	uneq2d	$⊢ φ \to (M \dots N - 1) \cup \{N - 1 + 1\} = (M \dots N - 1) \cup \{N\}$
29	25 26 28	3eqtr3d	$⊢ φ \to (M \dots N) = (M \dots N - 1) \cup \{N\}$
30		fzfid	$⊢ φ \to (M \dots N) \in Fin$
31	13 29 30 2	fprodsplit	$⊢ φ \to \prod_{k = M}^{N} A = \prod_{k = M}^{N - 1} A \prod_{k \in \{N\}} A$
32	3	eleq1d	$⊢ k = N \to (A \in ℂ \leftrightarrow B \in ℂ)$
33	2	ralrimiva	$⊢ φ \to \forall k \in (M \dots N) A \in ℂ$
34		eluzfz2	$⊢ N \in ℤ_{\geq M} \to N \in (M \dots N)$
35	1 34	syl	$⊢ φ \to N \in (M \dots N)$
36	32 33 35	rspcdva	$⊢ φ \to B \in ℂ$
37	3	prodsn	$⊢ (N \in ℤ_{\geq M} \land B \in ℂ) \to \prod_{k \in \{N\}} A = B$
38	1 36 37	syl2anc	$⊢ φ \to \prod_{k \in \{N\}} A = B$
39	38	oveq2d	$⊢ φ \to \prod_{k = M}^{N - 1} A \prod_{k \in \{N\}} A = \prod_{k = M}^{N - 1} A B$
40	31 39	eqtrd	$⊢ φ \to \prod_{k = M}^{N} A = \prod_{k = M}^{N - 1} A B$

Metamath Proof Explorer

Theorem fprodm1

Proof