Theorem fzodif1

Description: Set difference of two half-open range of sequential integers sharing the same starting value. (Contributed by Thierry Arnoux, 2-Oct-2023)

	Ref	Expression
Assertion	fzodif1	|- ( K e. ( M ... N ) -> ( ( M ..^ N ) \ ( M ..^ K ) ) = ( K ..^ N ) )

Proof

Step	Hyp	Ref	Expression
1		fzosplit	|- ( K e. ( M ... N ) -> ( M ..^ N ) = ( ( M ..^ K ) u. ( K ..^ N ) ) )
2	1	difeq1d	|- ( K e. ( M ... N ) -> ( ( M ..^ N ) \ ( M ..^ K ) ) = ( ( ( M ..^ K ) u. ( K ..^ N ) ) \ ( M ..^ K ) ) )
3		difundir	|- ( ( ( M ..^ K ) u. ( K ..^ N ) ) \ ( M ..^ K ) ) = ( ( ( M ..^ K ) \ ( M ..^ K ) ) u. ( ( K ..^ N ) \ ( M ..^ K ) ) )
4		difid	|- ( ( M ..^ K ) \ ( M ..^ K ) ) = (/)
5		incom	|- ( ( K ..^ N ) i^i ( M ..^ K ) ) = ( ( M ..^ K ) i^i ( K ..^ N ) )
6		fzodisj	|- ( ( M ..^ K ) i^i ( K ..^ N ) ) = (/)
7	5 6	eqtri	|- ( ( K ..^ N ) i^i ( M ..^ K ) ) = (/)
8		disj3	|- ( ( ( K ..^ N ) i^i ( M ..^ K ) ) = (/) <-> ( K ..^ N ) = ( ( K ..^ N ) \ ( M ..^ K ) ) )
9	7 8	mpbi	|- ( K ..^ N ) = ( ( K ..^ N ) \ ( M ..^ K ) )
10	9	eqcomi	|- ( ( K ..^ N ) \ ( M ..^ K ) ) = ( K ..^ N )
11	4 10	uneq12i	|- ( ( ( M ..^ K ) \ ( M ..^ K ) ) u. ( ( K ..^ N ) \ ( M ..^ K ) ) ) = ( (/) u. ( K ..^ N ) )
12		0un	|- ( (/) u. ( K ..^ N ) ) = ( K ..^ N )
13	3 11 12	3eqtri	|- ( ( ( M ..^ K ) u. ( K ..^ N ) ) \ ( M ..^ K ) ) = ( K ..^ N )
14	2 13	eqtrdi	|- ( K e. ( M ... N ) -> ( ( M ..^ N ) \ ( M ..^ K ) ) = ( K ..^ N ) )