Theorem fprod1p

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

	Ref	Expression
Hypotheses	fprod1p.1	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
	fprod1p.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
	fprod1p.3	⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐵 )
Assertion	fprod1p	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = ( 𝐵 · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		fprod1p.1	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2		fprod1p.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
3		fprod1p.3	⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐵 )
4		eluzfz1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
5	1 4	syl	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
6	5	elfzelzd	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
7		fzsn	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
8	6 7	syl	⊢ ( 𝜑 → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
9	8	ineq1d	⊢ ( 𝜑 → ( ( 𝑀 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) = ( { 𝑀 } ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
10	6	zred	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
11	10	ltp1d	⊢ ( 𝜑 → 𝑀 < ( 𝑀 + 1 ) )
12		fzdisj	⊢ ( 𝑀 < ( 𝑀 + 1 ) → ( ( 𝑀 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) = ∅ )
13	11 12	syl	⊢ ( 𝜑 → ( ( 𝑀 ... 𝑀 ) ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) = ∅ )
14	9 13	eqtr3d	⊢ ( 𝜑 → ( { 𝑀 } ∩ ( ( 𝑀 + 1 ) ... 𝑁 ) ) = ∅ )
15		fzsplit	⊢ ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
16	5 15	syl	⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
17	8	uneq1d	⊢ ( 𝜑 → ( ( 𝑀 ... 𝑀 ) ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) = ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
18	16 17	eqtrd	⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) = ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
19		fzfid	⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) ∈ Fin )
20	14 18 19 2	fprodsplit	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = ( ∏ 𝑘 ∈ { 𝑀 } 𝐴 · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 ) )
21	3	eleq1d	⊢ ( 𝑘 = 𝑀 → ( 𝐴 ∈ ℂ ↔ 𝐵 ∈ ℂ ) )
22	2	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ∈ ℂ )
23	21 22 5	rspcdva	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
24	3	prodsn	⊢ ( ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝐵 ∈ ℂ ) → ∏ 𝑘 ∈ { 𝑀 } 𝐴 = 𝐵 )
25	5 23 24	syl2anc	⊢ ( 𝜑 → ∏ 𝑘 ∈ { 𝑀 } 𝐴 = 𝐵 )
26	25	oveq1d	⊢ ( 𝜑 → ( ∏ 𝑘 ∈ { 𝑀 } 𝐴 · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 ) = ( 𝐵 · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 ) )
27	20 26	eqtrd	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = ( 𝐵 · ∏ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) 𝐴 ) )