Theorem fzdif2

Description: Split the last element of a finite set of sequential integers. More generic than fzsuc . (Contributed by Thierry Arnoux, 22-Aug-2020)

	Ref	Expression
Assertion	fzdif2	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(M\dots N\right)\setminus \left\{N\right\}=\left(M\dots N-1\right)$$

Proof

Step	Hyp	Ref	Expression
1		fzspl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(M\dots N\right)=\left(M\dots N-1\right)\cup \left\{N\right\}$$
2	1	difeq1d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(M\dots N\right)\setminus \left\{N\right\}=\left(\left(M\dots N-1\right)\cup \left\{N\right\}\right)\setminus \left\{N\right\}$$
3		difun2	$$⊢\left(\left(M\dots N-1\right)\cup \left\{N\right\}\right)\setminus \left\{N\right\}=\left(M\dots N-1\right)\setminus \left\{N\right\}$$
4	2 3	eqtrdi	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(M\dots N\right)\setminus \left\{N\right\}=\left(M\dots N-1\right)\setminus \left\{N\right\}$$
5		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in \mathbb{Z}$$
6		uzid	$$⊢N\in \mathbb{Z}\to N\in {\mathbb{Z}}_{\ge N}$$
7		uznfz	$$⊢N\in {\mathbb{Z}}_{\ge N}\to \neg N\in \left(M\dots N-1\right)$$
8	5 6 7	3syl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \neg N\in \left(M\dots N-1\right)$$
9		disjsn	$$⊢\left(M\dots N-1\right)\cap \left\{N\right\}=\varnothing \leftrightarrow \neg N\in \left(M\dots N-1\right)$$
10	8 9	sylibr	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(M\dots N-1\right)\cap \left\{N\right\}=\varnothing$$
11		disjdif2	$$⊢\left(M\dots N-1\right)\cap \left\{N\right\}=\varnothing \to \left(M\dots N-1\right)\setminus \left\{N\right\}=\left(M\dots N-1\right)$$
12	10 11	syl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(M\dots N-1\right)\setminus \left\{N\right\}=\left(M\dots N-1\right)$$
13	4 12	eqtrd	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(M\dots N\right)\setminus \left\{N\right\}=\left(M\dots N-1\right)$$