Theorem fzodif2

Description: Split the last element of a half-open range of sequential integers. (Contributed by Thierry Arnoux, 5-Dec-2021)

	Ref	Expression
Assertion	fzodif2	|- ( N e. ( ZZ>= ` M ) -> ( ( M ..^ ( N + 1 ) ) \ { N } ) = ( M ..^ N ) )

Proof

Step	Hyp	Ref	Expression
1		fzosplitsn	|- ( N e. ( ZZ>= ` M ) -> ( M ..^ ( N + 1 ) ) = ( ( M ..^ N ) u. { N } ) )
2	1	difeq1d	|- ( N e. ( ZZ>= ` M ) -> ( ( M ..^ ( N + 1 ) ) \ { N } ) = ( ( ( M ..^ N ) u. { N } ) \ { N } ) )
3		difun2	|- ( ( ( M ..^ N ) u. { N } ) \ { N } ) = ( ( M ..^ N ) \ { N } )
4	2 3	eqtrdi	|- ( N e. ( ZZ>= ` M ) -> ( ( M ..^ ( N + 1 ) ) \ { N } ) = ( ( M ..^ N ) \ { N } ) )
5		fzonel	|- -. N e. ( M ..^ N )
6		disjsn	|- ( ( ( M ..^ N ) i^i { N } ) = (/) <-> -. N e. ( M ..^ N ) )
7	5 6	mpbir	|- ( ( M ..^ N ) i^i { N } ) = (/)
8		disjdif2	|- ( ( ( M ..^ N ) i^i { N } ) = (/) -> ( ( M ..^ N ) \ { N } ) = ( M ..^ N ) )
9	7 8	mp1i	|- ( N e. ( ZZ>= ` M ) -> ( ( M ..^ N ) \ { N } ) = ( M ..^ N ) )
10	4 9	eqtrd	|- ( N e. ( ZZ>= ` M ) -> ( ( M ..^ ( N + 1 ) ) \ { N } ) = ( M ..^ N ) )