Theorem fzpred

Description: Join a predecessor to the beginning of a finite set of sequential integers. (Contributed by AV, 24-Aug-2019)

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

Proof

Step	Hyp	Ref	Expression
1		eluzel2	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in \mathbb{Z}$$
2		uzid	$$⊢M\in \mathbb{Z}\to M\in {\mathbb{Z}}_{\ge M}$$
3		peano2uz	$$⊢M\in {\mathbb{Z}}_{\ge M}\to M+1\in {\mathbb{Z}}_{\ge M}$$
4	1 2 3	3syl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M+1\in {\mathbb{Z}}_{\ge M}$$
5		fzsplit2	$$⊢\left(M+1\in {\mathbb{Z}}_{\ge M}\wedge N\in {\mathbb{Z}}_{\ge M}\right)\to \left(M\dots N\right)=\left(M\dots M\right)\cup \left(M+1\dots N\right)$$
6	4 5	mpancom	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(M\dots N\right)=\left(M\dots M\right)\cup \left(M+1\dots N\right)$$
7		fzsn	$$⊢M\in \mathbb{Z}\to \left(M\dots M\right)=\left\{M\right\}$$
8	1 7	syl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(M\dots M\right)=\left\{M\right\}$$
9	8	uneq1d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(M\dots M\right)\cup \left(M+1\dots N\right)=\left\{M\right\}\cup \left(M+1\dots N\right)$$
10	6 9	eqtrd	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(M\dots N\right)=\left\{M\right\}\cup \left(M+1\dots N\right)$$