Theorem fztp

Description: A finite interval of integers with three elements. (Contributed by NM, 13-Sep-2011) (Revised by Mario Carneiro, 7-Mar-2014)

	Ref	Expression
Assertion	fztp	$$⊢M\in \mathbb{Z}\to \left(M\dots M+2\right)=\left\{M,M+1,M+2\right\}$$

Proof

Step	Hyp	Ref	Expression
1		uzid	$$⊢M\in \mathbb{Z}\to M\in {\mathbb{Z}}_{\ge M}$$
2		peano2uz	$$⊢M\in {\mathbb{Z}}_{\ge M}\to M+1\in {\mathbb{Z}}_{\ge M}$$
3		fzsuc	$$⊢M+1\in {\mathbb{Z}}_{\ge M}\to \left(M\dots M+1+1\right)=\left(M\dots M+1\right)\cup \left\{M+1+1\right\}$$
4	1 2 3	3syl	$$⊢M\in \mathbb{Z}\to \left(M\dots M+1+1\right)=\left(M\dots M+1\right)\cup \left\{M+1+1\right\}$$
5		zcn	$$⊢M\in \mathbb{Z}\to M\in ℂ$$
6		ax-1cn	$$⊢1\in ℂ$$
7		addass	$$⊢\left(M\in ℂ\wedge 1\in ℂ\wedge 1\in ℂ\right)\to M+1+1=M+1+1$$
8	6 6 7	mp3an23	$$⊢M\in ℂ\to M+1+1=M+1+1$$
9	5 8	syl	$$⊢M\in \mathbb{Z}\to M+1+1=M+1+1$$
10		df-2	$$⊢2=1+1$$
11	10	oveq2i	$$⊢M+2=M+1+1$$
12	9 11	eqtr4di	$$⊢M\in \mathbb{Z}\to M+1+1=M+2$$
13	12	oveq2d	$$⊢M\in \mathbb{Z}\to \left(M\dots M+1+1\right)=\left(M\dots M+2\right)$$
14		fzpr	$$⊢M\in \mathbb{Z}\to \left(M\dots M+1\right)=\left\{M,M+1\right\}$$
15	12	sneqd	$$⊢M\in \mathbb{Z}\to \left\{M+1+1\right\}=\left\{M+2\right\}$$
16	14 15	uneq12d	$$⊢M\in \mathbb{Z}\to \left(M\dots M+1\right)\cup \left\{M+1+1\right\}=\left\{M,M+1\right\}\cup \left\{M+2\right\}$$
17		df-tp	$$⊢\left\{M,M+1,M+2\right\}=\left\{M,M+1\right\}\cup \left\{M+2\right\}$$
18	16 17	eqtr4di	$$⊢M\in \mathbb{Z}\to \left(M\dots M+1\right)\cup \left\{M+1+1\right\}=\left\{M,M+1,M+2\right\}$$
19	4 13 18	3eqtr3d	$$⊢M\in \mathbb{Z}\to \left(M\dots M+2\right)=\left\{M,M+1,M+2\right\}$$