Theorem fzsplitnr

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

	Ref	Expression
Hypotheses	fzsplitnr.1	|- ( ph -> M e. ZZ )
	fzsplitnr.2	|- ( ph -> N e. ZZ )
	fzsplitnr.3	|- ( ph -> K e. ZZ )
	fzsplitnr.4	|- ( ph -> M <_ K )
	fzsplitnr.5	|- ( ph -> K <_ N )
Assertion	fzsplitnr	|- ( ph -> ( M ... N ) = ( ( M ... ( K - 1 ) ) u. ( K ... N ) ) )

Proof

Step	Hyp	Ref	Expression
1		fzsplitnr.1	|- ( ph -> M e. ZZ )
2		fzsplitnr.2	|- ( ph -> N e. ZZ )
3		fzsplitnr.3	|- ( ph -> K e. ZZ )
4		fzsplitnr.4	|- ( ph -> M <_ K )
5		fzsplitnr.5	|- ( ph -> K <_ N )
6	1 2 3 4 5	elfzd	|- ( ph -> K e. ( M ... N ) )
7	6	fzsplitnd	|- ( ph -> ( M ... N ) = ( ( M ... ( K - 1 ) ) u. ( K ... N ) ) )