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\in {\mathbb{Z}}_{\ge M}\to \left(M..^N+1\right)\setminus \left\{N\right\}=\left(M..^N\right)$$

Proof

Step	Hyp	Ref	Expression
1		fzosplitsn	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(M..^N+1\right)=\left(M..^N\right)\cup \left\{N\right\}$$
2	1	difeq1d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(M..^N+1\right)\setminus \left\{N\right\}=\left(\left(M..^N\right)\cup \left\{N\right\}\right)\setminus \left\{N\right\}$$
3		difun2	$$⊢\left(\left(M..^N\right)\cup \left\{N\right\}\right)\setminus \left\{N\right\}=\left(M..^N\right)\setminus \left\{N\right\}$$
4	2 3	eqtrdi	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(M..^N+1\right)\setminus \left\{N\right\}=\left(M..^N\right)\setminus \left\{N\right\}$$
5		fzonel	$$⊢\neg N\in \left(M..^N\right)$$
6		disjsn	$$⊢\left(M..^N\right)\cap \left\{N\right\}=\varnothing \leftrightarrow \neg N\in \left(M..^N\right)$$
7	5 6	mpbir	$$⊢\left(M..^N\right)\cap \left\{N\right\}=\varnothing$$
8		disjdif2	$$⊢\left(M..^N\right)\cap \left\{N\right\}=\varnothing \to \left(M..^N\right)\setminus \left\{N\right\}=\left(M..^N\right)$$
9	7 8	mp1i	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(M..^N\right)\setminus \left\{N\right\}=\left(M..^N\right)$$
10	4 9	eqtrd	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(M..^N+1\right)\setminus \left\{N\right\}=\left(M..^N\right)$$