Theorem fzpreddisj

Description: A finite set of sequential integers is disjoint with its predecessor. (Contributed by AV, 24-Aug-2019)

	Ref	Expression
Assertion	fzpreddisj	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left\{M\right\}\cap \left(M+1\dots N\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		incom	$$⊢\left\{M\right\}\cap \left(M+1\dots N\right)=\left(M+1\dots N\right)\cap \left\{M\right\}$$
2		0lt1	$$⊢0<1$$
3		0re	$$⊢0\in ℝ$$
4		1re	$$⊢1\in ℝ$$
5	3 4	ltnlei	$$⊢0<1\leftrightarrow \neg 1\le 0$$
6	2 5	mpbi	$$⊢\neg 1\le 0$$
7		eluzel2	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in \mathbb{Z}$$
8	7	zred	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in ℝ$$
9		leaddle0	$$⊢\left(M\in ℝ\wedge 1\in ℝ\right)\to \left(M+1\le M\leftrightarrow 1\le 0\right)$$
10	8 4 9	sylancl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(M+1\le M\leftrightarrow 1\le 0\right)$$
11	6 10	mtbiri	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \neg M+1\le M$$
12	11	intnanrd	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \neg \left(M+1\le M\wedge M\le N\right)$$
13	12	intnand	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \neg \left(\left(M+1\in \mathbb{Z}\wedge N\in \mathbb{Z}\wedge M\in \mathbb{Z}\right)\wedge \left(M+1\le M\wedge M\le N\right)\right)$$
14		elfz2	$$⊢M\in \left(M+1\dots N\right)\leftrightarrow \left(\left(M+1\in \mathbb{Z}\wedge N\in \mathbb{Z}\wedge M\in \mathbb{Z}\right)\wedge \left(M+1\le M\wedge M\le N\right)\right)$$
15	13 14	sylnibr	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \neg M\in \left(M+1\dots N\right)$$
16		disjsn	$$⊢\left(M+1\dots N\right)\cap \left\{M\right\}=\varnothing \leftrightarrow \neg M\in \left(M+1\dots N\right)$$
17	15 16	sylibr	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(M+1\dots N\right)\cap \left\{M\right\}=\varnothing$$
18	1 17	eqtrid	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left\{M\right\}\cap \left(M+1\dots N\right)=\varnothing$$