Theorem fzsplit

Description: Split a finite interval of integers into two parts. (Contributed by Jeff Madsen, 17-Jun-2010) (Revised by Mario Carneiro, 13-Apr-2016)

	Ref	Expression
Assertion	fzsplit	$$⊢K\in \left(M\dots N\right)\to \left(M\dots N\right)=\left(M\dots K\right)\cup \left(K+1\dots N\right)$$

Proof

Step	Hyp	Ref	Expression
1		elfzuz	$$⊢K\in \left(M\dots N\right)\to K\in {\mathbb{Z}}_{\ge M}$$
2		peano2uz	$$⊢K\in {\mathbb{Z}}_{\ge M}\to K+1\in {\mathbb{Z}}_{\ge M}$$
3	1 2	syl	$$⊢K\in \left(M\dots N\right)\to K+1\in {\mathbb{Z}}_{\ge M}$$
4		elfzuz3	$$⊢K\in \left(M\dots N\right)\to N\in {\mathbb{Z}}_{\ge K}$$
5		fzsplit2	$$⊢\left(K+1\in {\mathbb{Z}}_{\ge M}\wedge N\in {\mathbb{Z}}_{\ge K}\right)\to \left(M\dots N\right)=\left(M\dots K\right)\cup \left(K+1\dots N\right)$$
6	3 4 5	syl2anc	$$⊢K\in \left(M\dots N\right)\to \left(M\dots N\right)=\left(M\dots K\right)\cup \left(K+1\dots N\right)$$