Theorem prodsplit

Description: Product split into two factors, original by Steven Nguyen. (Contributed by metakunt, 21-Apr-2024)

	Ref	Expression
Hypotheses	prodsplit.1	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	prodsplit.2	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
	prodsplit.3	⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
	prodsplit.4	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
	prodsplit.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 𝐾 ) ) ) → 𝐴 ∈ ℂ )
Assertion	prodsplit	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 𝐾 ) ) 𝐴 = ( ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 · ∏ 𝑘 ∈ ( ( 𝑁 + 1 ) ... ( 𝑁 + 𝐾 ) ) 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		prodsplit.1	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		prodsplit.2	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
3		prodsplit.3	⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
4		prodsplit.4	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
5		prodsplit.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 𝐾 ) ) ) → 𝐴 ∈ ℂ )
6	2	zred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
7	6	ltp1d	⊢ ( 𝜑 → 𝑁 < ( 𝑁 + 1 ) )
8		fzdisj	⊢ ( 𝑁 < ( 𝑁 + 1 ) → ( ( 𝑀 ... 𝑁 ) ∩ ( ( 𝑁 + 1 ) ... ( 𝑁 + 𝐾 ) ) ) = ∅ )
9	7 8	syl	⊢ ( 𝜑 → ( ( 𝑀 ... 𝑁 ) ∩ ( ( 𝑁 + 1 ) ... ( 𝑁 + 𝐾 ) ) ) = ∅ )
10	4	nn0zd	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
11	2 10	zaddcld	⊢ ( 𝜑 → ( 𝑁 + 𝐾 ) ∈ ℤ )
12		nn0addge1	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝐾 ∈ ℕ0 ) → 𝑁 ≤ ( 𝑁 + 𝐾 ) )
13	6 4 12	syl2anc	⊢ ( 𝜑 → 𝑁 ≤ ( 𝑁 + 𝐾 ) )
14	1 11 2 3 13	elfzd	⊢ ( 𝜑 → 𝑁 ∈ ( 𝑀 ... ( 𝑁 + 𝐾 ) ) )
15		fzsplit	⊢ ( 𝑁 ∈ ( 𝑀 ... ( 𝑁 + 𝐾 ) ) → ( 𝑀 ... ( 𝑁 + 𝐾 ) ) = ( ( 𝑀 ... 𝑁 ) ∪ ( ( 𝑁 + 1 ) ... ( 𝑁 + 𝐾 ) ) ) )
16	14 15	syl	⊢ ( 𝜑 → ( 𝑀 ... ( 𝑁 + 𝐾 ) ) = ( ( 𝑀 ... 𝑁 ) ∪ ( ( 𝑁 + 1 ) ... ( 𝑁 + 𝐾 ) ) ) )
17		fzfid	⊢ ( 𝜑 → ( 𝑀 ... ( 𝑁 + 𝐾 ) ) ∈ Fin )
18	9 16 17 5	fprodsplit	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 𝐾 ) ) 𝐴 = ( ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 · ∏ 𝑘 ∈ ( ( 𝑁 + 1 ) ... ( 𝑁 + 𝐾 ) ) 𝐴 ) )