Theorem fzsplitnr

Description: Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024)

	Ref	Expression
Hypotheses	fzsplitnr.1	$$⊢\phi \to M\in \mathbb{Z}$$
	fzsplitnr.2	$$⊢\phi \to N\in \mathbb{Z}$$
	fzsplitnr.3	$$⊢\phi \to K\in \mathbb{Z}$$
	fzsplitnr.4	$$⊢\phi \to M\le K$$
	fzsplitnr.5	$$⊢\phi \to K\le N$$
Assertion	fzsplitnr	$$⊢\phi \to \left(M\dots N\right)=\left(M\dots K-1\right)\cup \left(K\dots N\right)$$

Proof

Step	Hyp	Ref	Expression
1		fzsplitnr.1	$$⊢\phi \to M\in \mathbb{Z}$$
2		fzsplitnr.2	$$⊢\phi \to N\in \mathbb{Z}$$
3		fzsplitnr.3	$$⊢\phi \to K\in \mathbb{Z}$$
4		fzsplitnr.4	$$⊢\phi \to M\le K$$
5		fzsplitnr.5	$$⊢\phi \to K\le N$$
6	1 2 3 4 5	elfzd	$$⊢\phi \to K\in \left(M\dots N\right)$$
7	6	fzsplitnd	$$⊢\phi \to \left(M\dots N\right)=\left(M\dots K-1\right)\cup \left(K\dots N\right)$$