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