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 e. ( M ... N ) -> ( M ... N ) = ( ( M ... K ) u. ( ( K + 1 ) ... N ) ) )

Proof

Step	Hyp	Ref	Expression
1		elfzuz	|- ( K e. ( M ... N ) -> K e. ( ZZ>= ` M ) )
2		peano2uz	|- ( K e. ( ZZ>= ` M ) -> ( K + 1 ) e. ( ZZ>= ` M ) )
3	1 2	syl	|- ( K e. ( M ... N ) -> ( K + 1 ) e. ( ZZ>= ` M ) )
4		elfzuz3	|- ( K e. ( M ... N ) -> N e. ( ZZ>= ` K ) )
5		fzsplit2	|- ( ( ( K + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) -> ( M ... N ) = ( ( M ... K ) u. ( ( K + 1 ) ... N ) ) )
6	3 4 5	syl2anc	|- ( K e. ( M ... N ) -> ( M ... N ) = ( ( M ... K ) u. ( ( K + 1 ) ... N ) ) )