Theorem fzo1to4tp

Description: A half-open integer range from 1 to 4 is an unordered triple. (Contributed by AV, 28-Jul-2021)

	Ref	Expression
Assertion	fzo1to4tp	$$⊢\left(1..^4\right)=\left\{1,2,3\right\}$$

Proof

Step	Hyp	Ref	Expression
1		4z	$$⊢4\in \mathbb{Z}$$
2		fzoval	$$⊢4\in \mathbb{Z}\to \left(1..^4\right)=\left(1\dots 4-1\right)$$
3	1 2	ax-mp	$$⊢\left(1..^4\right)=\left(1\dots 4-1\right)$$
4		4m1e3	$$⊢4-1=3$$
5		df-3	$$⊢3=2+1$$
6		2cn	$$⊢2\in ℂ$$
7		ax-1cn	$$⊢1\in ℂ$$
8	6 7	addcomi	$$⊢2+1=1+2$$
9	4 5 8	3eqtri	$$⊢4-1=1+2$$
10	9	oveq2i	$$⊢\left(1\dots 4-1\right)=\left(1\dots 1+2\right)$$
11		1z	$$⊢1\in \mathbb{Z}$$
12		fztp	$$⊢1\in \mathbb{Z}\to \left(1\dots 1+2\right)=\left\{1,1+1,1+2\right\}$$
13		eqidd	$$⊢1\in \mathbb{Z}\to 1=1$$
14		1p1e2	$$⊢1+1=2$$
15	14	a1i	$$⊢1\in \mathbb{Z}\to 1+1=2$$
16		1p2e3	$$⊢1+2=3$$
17	16	a1i	$$⊢1\in \mathbb{Z}\to 1+2=3$$
18	13 15 17	tpeq123d	$$⊢1\in \mathbb{Z}\to \left\{1,1+1,1+2\right\}=\left\{1,2,3\right\}$$
19	12 18	eqtrd	$$⊢1\in \mathbb{Z}\to \left(1\dots 1+2\right)=\left\{1,2,3\right\}$$
20	11 19	ax-mp	$$⊢\left(1\dots 1+2\right)=\left\{1,2,3\right\}$$
21	3 10 20	3eqtri	$$⊢\left(1..^4\right)=\left\{1,2,3\right\}$$