Theorem prodsplit

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

	Ref	Expression
Hypotheses	prodsplit.1	$$⊢\phi \to M\in \mathbb{Z}$$
	prodsplit.2	$$⊢\phi \to N\in \mathbb{Z}$$
	prodsplit.3	$$⊢\phi \to M\le N$$
	prodsplit.4	$$⊢\phi \to K\in {\mathbb{N}}_0$$
	prodsplit.5	$$⊢\left(\phi \wedge k\in \left(M\dots N+K\right)\right)\to A\in ℂ$$
Assertion	prodsplit	$$⊢\phi \to \prod _{k=M}^{N+K}A=\prod _{k=M}^{N}A\prod _{k=N+1}^{N+K}A$$

Proof

Step	Hyp	Ref	Expression
1		prodsplit.1	$$⊢\phi \to M\in \mathbb{Z}$$
2		prodsplit.2	$$⊢\phi \to N\in \mathbb{Z}$$
3		prodsplit.3	$$⊢\phi \to M\le N$$
4		prodsplit.4	$$⊢\phi \to K\in {\mathbb{N}}_0$$
5		prodsplit.5	$$⊢\left(\phi \wedge k\in \left(M\dots N+K\right)\right)\to A\in ℂ$$
6	2	zred	$$⊢\phi \to N\in ℝ$$
7	6	ltp1d	$$⊢\phi \to N<N+1$$
8		fzdisj	$$⊢N<N+1\to \left(M\dots N\right)\cap \left(N+1\dots N+K\right)=\varnothing$$
9	7 8	syl	$$⊢\phi \to \left(M\dots N\right)\cap \left(N+1\dots N+K\right)=\varnothing$$
10	4	nn0zd	$$⊢\phi \to K\in \mathbb{Z}$$
11	2 10	zaddcld	$$⊢\phi \to N+K\in \mathbb{Z}$$
12		nn0addge1	$$⊢\left(N\in ℝ\wedge K\in {\mathbb{N}}_0\right)\to N\le N+K$$
13	6 4 12	syl2anc	$$⊢\phi \to N\le N+K$$
14		elfz4	$$⊢\left(\left(M\in \mathbb{Z}\wedge N+K\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\wedge \left(M\le N\wedge N\le N+K\right)\right)\to N\in \left(M\dots N+K\right)$$
15	1 11 2 3 13 14	syl32anc	$$⊢\phi \to N\in \left(M\dots N+K\right)$$
16		fzsplit	$$⊢N\in \left(M\dots N+K\right)\to \left(M\dots N+K\right)=\left(M\dots N\right)\cup \left(N+1\dots N+K\right)$$
17	15 16	syl	$$⊢\phi \to \left(M\dots N+K\right)=\left(M\dots N\right)\cup \left(N+1\dots N+K\right)$$
18		fzfid	$$⊢\phi \to \left(M\dots N+K\right)\in \mathrm{Fin}$$
19	9 17 18 5	fprodsplit	$$⊢\phi \to \prod _{k=M}^{N+K}A=\prod _{k=M}^{N}A\prod _{k=N+1}^{N+K}A$$